Editing Lambda calculus (section)

=== Pairs ===
A pair (2-tuple) can be defined in terms of {{Mono|TRUE}} and {{Mono|FALSE}}, by using the [[Church encoding#Church pairs|Church encoding for pairs]]. For example, {{Mono|PAIR}} encapsulates the pair ({{Mono|''x''}},{{Mono|''y''}}), {{Mono|FIRST}} returns the first element of the pair, and {{Mono|SECOND}} returns the second.

: {{Mono|1=PAIR := λ''x''.λ''y''.λ''f''.''f'' ''x'' ''y''}}
: {{Mono|1=FIRST := λ''p''.''p'' TRUE}}
: {{Mono|1=SECOND := λ''p''.''p'' FALSE}}
: {{Mono|1=NIL := λ''x''.TRUE}}
: {{Mono|1=NULL := λ''p''.''p'' (λ''x''.λ''y''.FALSE)}}

A linked list can be defined as either NIL for the empty list, or the {{Mono|PAIR}} of an element and a smaller list. The predicate {{Mono|NULL}} tests for the value {{Mono|NIL}}. (Alternatively, with {{Mono|1=NIL := FALSE}}, the construct {{Mono|''l'' (λ''h''.λ''t''.λ''z''.deal_with_head_''h''_and_tail_''t'') (deal_with_nil)}} obviates the need for an explicit NULL test).

As an example of the use of pairs, the shift-and-increment function that maps {{Mono|(''m'', ''n'')}} to {{Mono|(''n'', ''n'' + 1)}} can be defined as
: {{Mono|1=Φ := λ''x''.PAIR (SECOND ''x'') (SUCC (SECOND ''x''))}}
which allows us to give perhaps the most transparent version of the predecessor function:
: {{Mono|1=PRED := λ''n''.FIRST (''n'' Φ (PAIR 0 0)).}}