Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 21: | Line 21: | ||
* <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> | ||
The Church booleans take two arguments, and evaluate to one of them: | |||
* <tt>true ≡ λa. λb . a</tt> | |||
* <tt>false ≡ λa. λb . b</tt> | |||
Some basic 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 a defined <tt>1</tt>) | * <tt>succ ≡ λn. λf. λx. f (n f x)</tt> (β-equivalent to <tt>(plus 1)</tt> for a defined <tt>1</tt>) | ||
* <tt>mult ≡ λm. λn. λf. n (m f)</tt> (from ''f<sup>(m * n)</sup> = (f<sup>m</sup>)<sup>n</sup>'') | * <tt>mult ≡ λm. λn. λf. n (m f)</tt> (from ''f<sup>(m * n)</sup> = (f<sup>m</sup>)<sup>n</sup>'') | ||
Common syntactic sugar: | Common syntactic sugar: | ||
* Left-associative application as implicit parentheses | * Left-associative application as implicit parentheses | ||