Programming Language Theory: Difference between revisions
No edit summary |
|||
| Line 83: | Line 83: | ||
* <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) | ||
* <tt>sub ≡ λm. λn. (n pred) m</tt> (using <tt>pred</tt> from above) | * <tt>sub ≡ λm. λn. (n pred) m</tt> (using <tt>pred</tt> from above) | ||
====Pairs==== | |||
* <tt>pair ≡ λf. λs. λb. b f s</tt> | |||
* <tt>first ≡ λp. p true</tt> | |||
* <tt>second ≡ λp. p false</tt> | |||
====Logic==== | ====Logic==== | ||
| Line 92: | Line 97: | ||
* <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>) | ||
* <tt>iszro ≡ λm. m (λx. false) true</tt> | * <tt>iszro ≡ λm. m (λx. false) true</tt> | ||
This definition of <tt>test</tt> will evaluate both arguments in a strict application, which is undesirable. Instead, define <tt>if</tt> as a function taking one argument (<tt>true/false</tt>), which evaluates to either the function <tt>first</tt> or <tt>second</tt>. | |||
====Syntactic sugar==== | ====Syntactic sugar==== | ||