Programming Language Theory: Difference between revisions
| Line 26: | Line 26: | ||
* Function definition: <tt>(λ''boundparam''. body)</tt> | * Function definition: <tt>(λ''boundparam''. body)</tt> | ||
* 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''. | ||
==== | ====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> | ||
This abstract grammar can be augmented with associativity rules and grouping syntax (parentheses) to provide a concrete grammar. If verbosity is no issue, no associativity rules need be specified for the following grammar: | |||
<pre>λ-term ::= λ-app | λ-abst | var | |||
λ-app ::= '('λ-term λ-term')' | |||
λ-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): | ||