Editing Lambda calculus (section)

=== Logic and predicates ===
By convention, the following two definitions (known as Church Booleans) are used for the Boolean values {{Mono|TRUE}} and {{Mono|FALSE}}:
: {{Mono|1=TRUE := λ''x''.λ''y''.''x''}}
: {{Mono|1=FALSE := λ''x''.λ''y''.''y''}}
Then, with these two lambda terms, we can define some logic operators (these are just possible formulations; other expressions could be equally correct):
: {{Mono|1=AND := λ''p''.λ''q''.''p'' ''q'' ''p''}}
: {{Mono|1=OR := λ''p''.λ''q''.''p'' ''p'' ''q''}}
: {{Mono|1=NOT := λ''p''.''p'' FALSE TRUE}}
: {{Mono|1=IFTHENELSE := λ''p''.λ''a''.λ''b''.''p'' ''a'' ''b''}}
We are now able to compute some logic functions, for example:

: {{Mono|AND TRUE FALSE}}
:: {{Mono|≡ (λ''p''.λ''q''.''p'' ''q'' ''p'') TRUE FALSE →<sub>β</sub> TRUE FALSE TRUE}}
:: {{Mono|≡ (λ''x''.λ''y''.''x'') FALSE TRUE →<sub>β</sub> FALSE}}
and we see that {{Mono|AND TRUE FALSE}} is equivalent to {{Mono|FALSE}}.

A ''predicate'' is a function that returns a Boolean value. The most fundamental predicate is {{Mono|ISZERO}}, which returns {{Mono|TRUE}} if its argument is the Church numeral {{Mono|0}}, but {{Mono|FALSE}} if its argument were any other Church numeral:
: {{Mono|1=ISZERO := λ''n''.''n'' (λ''x''.FALSE) TRUE}}
The following predicate tests whether the first argument is less-than-or-equal-to the second:
: {{Mono|1=LEQ := λ''m''.λ''n''.ISZERO (SUB ''m'' ''n'')}},
and since {{Mono|1=''m'' = ''n''}}, if {{Mono|LEQ ''m'' ''n''}} and {{Mono|LEQ ''n'' ''m''}}, it is straightforward to build a predicate for numerical equality.

The availability of predicates and the above definition of {{Mono|TRUE}} and {{Mono|FALSE}} make it convenient to write "if-then-else" expressions in lambda calculus. For example, the predecessor function can be defined as:
: {{Mono|1=PRED := λ''n''.''n'' (λ''g''.λ''k''.ISZERO (''g'' 1) ''k'' (PLUS (''g'' ''k'') 1)) (λ''v''.0) 0}}
which can be verified by showing inductively that {{Mono|''n'' (λ''g''.λ''k''.ISZERO (''g'' 1) ''k'' (PLUS (''g'' ''k'') 1)) (λ''v''.0)}} is the add {{Mono|''n''}} − 1 function for {{Mono|''n''}} > 0.