Programming Language Theory: Difference between revisions

Line 81: Line 81:
====Logic====
====Logic====
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>
Using them, we implement basic conditional logic:
Using them, we implement basic conditional logic:
* <tt>if[A, B, C] A B C</tt> (use <tt>true</tt>/<tt>false</tt> for A. Evaluates to B on <tt>true</tt>, C on <tt>false</tt>)
* <tt>test λa. λb. λc. a b c</tt> (use <tt>true</tt>/<tt>false</tt> for A. Evaluates to B on <tt>true</tt>, C on <tt>false</tt>)
* <tt>not ≡ λt. t false true</tt> (β-equivalent to <tt>if[A, false, true]</tt>)
* <tt>not ≡ λt. t false true</tt> (β-equivalent to <tt>if[A, false, true]</tt>)