Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 10: | Line 10: | ||
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 [[Architecture|Combinatorial logic]]. | 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 [[Architecture|Combinatorial logic]]. | ||
The integers (or any countably infinite set) can be represented via the [http://en.wikipedia.org/wiki/Church_encoding Church encoding]: | 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): | ||
* <tt>0 ≡ λf. λx. x</tt> | * <tt>0 ≡ λf. λx. x</tt> | ||
* <tt>1 ≡ λf. λx. f x</tt> | * <tt>1 ≡ λf. λx. f x</tt>, <tt>2 ≡ λf. λx. f (f x)</tt>, <tt>3 ≡ λf. λx. f (f (f x))</tt> | ||
* <tt>n ≡ λf. λx. f<sup>n</sup>x</tt> | * <tt>n ≡ λf. λx. f<sup>n</sup>x</tt> | ||
* <tt>plus ≡ λm. λn. λf. λx. m f (n f x)</tt> (from ''f<sup>(m + n)</sup>(x) = f<sup>m</sup>(f<sup>n</sup>(x))'') | * <tt>plus ≡ λm. λn. λf. λx. m f (n f x)</tt> (from ''f<sup>(m + n)</sup>(x) = f<sup>m</sup>(f<sup>n</sup>(x))'') | ||