Programming Language Theory: Difference between revisions
| Line 35: | Line 35: | ||
λ-app ::= '(' λ-term λ-term ')' | λ-app ::= '(' λ-term λ-term ')' | ||
λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre> | λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre> | ||
====Evaluation==== | |||
* Substitution: {N / X}M reads as "substitute expression N for free instances of X in expression M" | |||
* ''ɑ-conversion'': {Y / X}M. Renames bound variables with any variable Y which is not free in M. | |||
====Encodings==== | ====Encodings==== | ||