Programming Language Theory: Difference between revisions
| Line 39: | Line 39: | ||
λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre> | λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre> | ||
====Evaluation via Substitution==== | ====Evaluation via Substitution==== | ||
We'll use a substitution syntax to rewrite λ-calculus strings. ''{N / X}M'' substitutes expression N for free instances of X in expression M: | We'll use a substitution syntax to rewrite λ-calculus strings. Heavyweight [http://en.wikipedia.org/wiki/De_Bruijn_notation de Bruijn indexing] is one substitution semantic, as is the ''Barendregt convention''. The following simple semantic is due Rugaber, possibly through Pierce: ''{N / X}M'' substitutes expression N for free instances of X in expression M: | ||
* If M is a variable ({N / X}V), replace M with X if and only if M is N. | * If M is a variable ({N / X}V), replace M with X if and only if M is N. | ||
* If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B)) | * If M is a λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B)) | ||