Programming Language Theory: Difference between revisions

@@ Line 44: / Line 44: @@
 λ-abst ::= '(' 'λ'var'.' λ-term ')'</pre>
 ====Evaluation via Substitution====
-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:
+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 λ-app ({N / X}(A B)), {N / X}M = (({N / X}A) ({N / X}B))