Programming Language Theory: Difference between revisions
| Line 66: | Line 66: | ||
====Numerics==== | ====Numerics==== | ||
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): | ||
* <tt>0 ≡ λf. λx. x</tt> | * <tt>0 ≡ λf. λx. x</tt> (referred to as <tt>c<sub>0</sub></tt>) | ||
* <tt>1 ≡ λf. λx. f x</tt> | * <tt>1 ≡ λf. λx. f x</tt> | ||
* <tt>2 ≡ λf. λx. f (f x)</tt> | * <tt>2 ≡ λf. λx. f (f x)</tt> | ||
* <tt>3 ≡ λf. λx. f (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> (...up thorugh <tt>c<sub>n</sub></tt>) | ||
Some basic arithmetic operations: | Some basic arithmetic operations: | ||
* <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))'') | ||
* <tt>succ ≡ λn. λf. λx. f (n f x)</tt> (β-equivalent to <tt>(plus 1)</tt> for our <tt>1</tt> from above) | * <tt>succ ≡ λn. λf. λx. f (n f x)</tt> (β-equivalent to <tt>(plus 1)</tt> for our <tt>1</tt> from above) | ||
* <tt>mult ≡ λm. λn. λf. n (m f)</tt> (from ''f<sup>(m * n)</sup>(x) = (f<sup>m</sup>(x))<sup>n</sup>'') | * <tt>mult ≡ λm. λn. λf. n (m f)</tt> (from ''f<sup>(m * n)</sup>(x) = (f<sup>m</sup>(x))<sup>n</sup>'') | ||
** alternatively, <tt>mult ≡ λm. λn. m (plus n) c<sub>0</sub></tt> | |||
* <tt>pow ≡ λm. λn. n m</tt> | * <tt>pow ≡ λm. λn. n m</tt> | ||
* <tt>pred ≡ λn. λf. λx. n (λg. λh. h (g f)) (λu. x) (λu. u)</tt> (returns 0 when applied to 0) | * <tt>pred ≡ λn. λf. λx. n (λg. λh. h (g f)) (λu. x) (λu. u)</tt> (returns 0 when applied to 0) | ||
| Line 82: | Line 83: | ||
The Church booleans evaluate to one of their two arguments: | The Church booleans evaluate to one of their two arguments: | ||
* <tt>true ≡ λa. λb. a</tt> | * <tt>true ≡ λa. λb. a</tt> | ||
* <tt>false ≡ λa. λb. b</tt> | * <tt>false ≡ λa. λb. b</tt> (note that <tt>false</tt> is ɑ-equivalent to <tt>c<sub>0</sub></tt>!) | ||
Using them, we implement basic conditional logic: | Using them, we implement basic conditional logic: | ||
* <tt>test ≡ λa. λb. λc. a b c</tt> (using <tt>true</tt>/<tt>false</tt> for a, <tt>test</tt> reduces to <tt>b</tt> on <tt>true</tt>, and <tt>c</tt> on <tt>false</tt>) | * <tt>test ≡ λa. λb. λc. a b c</tt> (using <tt>true</tt>/<tt>false</tt> for a, <tt>test</tt> reduces to <tt>b</tt> on <tt>true</tt>, and <tt>c</tt> on <tt>false</tt>) | ||
* <tt>not ≡ λt. t false true</tt> (β-equivalent to <tt>test(A, false, true)</tt>) | * <tt>not ≡ λt. t false true</tt> (β-equivalent to <tt>test(A, false, true)</tt>) | ||
====Pairs==== | |||
* <tt>pair ≡ λf. λs. λb. b f s</tt> | |||
* <tt>first ≡ λp. p true</tt> | |||
* <tt>second ≡ λp. p false</tt> | |||
====Syntactic sugar==== | ====Syntactic sugar==== | ||