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]]). A λ-expression enclosed in scopes of its free variables is ''meaningful''. Changing the names of bound variables within a λ-expression preserves ''ɑ-equivalence''. | ||
====Grammar==== | ====Grammar==== | ||
<pre>λ-term ::= λ-app | λ-abst | var | <pre>λ-term ::= λ-app | λ-abst | var | ||