Programming Language Theory: Difference between revisions
| Line 27: | Line 27: | ||
* Function application: <tt>function(''actualparam'')</tt> | * Function application: <tt>function(''actualparam'')</tt> | ||
The body is made up of ''free'' and ''bound'' variables. Those not present in the λ's list of bound variables are free. A λ-expression with no free variables is ''closed'' (closed expressions are equivalent in power to [[Programming_Language_Theory#Combinatory_Logic|combinatory logic]]). Changing the names of bound variables within a λ-expression preserves ''ɑ-equivalence''. | The body is made up of ''free'' and ''bound'' variables. Those not present in the λ's list of bound variables are free. A λ-expression with no free variables is ''closed'' (closed expressions are equivalent in power to [[Programming_Language_Theory#Combinatory_Logic|combinatory logic]]). Changing the names of bound variables within a λ-expression preserves ''ɑ-equivalence''. | ||
==== | ====Abstract grammar==== | ||
<pre>λ-term ::= λ-app | λ-abst | var | <pre>λ-term ::= λ-app | λ-abst | var | ||
λ-app ::= λ-term λ-term | λ-app ::= λ-term λ-term | ||
λ-abst ::= 'λ'var'.' λ-term</pre> | λ-abst ::= 'λ'var'.' λ-term</pre> | ||
====Encodings==== | ====Encodings==== | ||
The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding] (or [http://en.wikipedia.org/wiki/Mogensen-Scott_encoding Mogensen-Scott], or others): | The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding] (or [http://en.wikipedia.org/wiki/Mogensen-Scott_encoding Mogensen-Scott], or others): | ||