Programming Language Theory: Difference between revisions
| Line 37: | Line 37: | ||
====Evaluation==== | ====Evaluation==== | ||
* Substitution: {N / X}M reads as "substitute expression N for free instances of X in expression M" | * 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. | * ''ɑ-conversion'': λX. M →<sub>ɑ</sub> λY. {Y / X}M. Renames bound variables with any variable Y which is not free in M. | ||
* ''β-reduction'': (λX. M) N →<sub>β</sub> {N / X}M. Replaces a formal parameter with an actual parameter. | |||
====Encodings==== | ====Encodings==== | ||