Substitution revisited (Q1106190)
From MaRDI portal
scientific article
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | Substitution revisited |
scientific article |
Statements
Substitution revisited (English)
0 references
1988
0 references
Always renaming bound variables and doing this in parallel with substitution we obtain simultaneous substitution which is defined in the paper for untyped lambda-calculus (in my opinion, everything must hold also for typed lambda-calculus). Theorems relating substitution and alpha-congruence are proved, as well as the substitution lemma of denotational semantics.
0 references
cpo
0 references
structural recursion
0 references
simultaneous substitution
0 references
untyped lambda- calculus
0 references
alpha-congruence
0 references
denotational semantics
0 references
