Editing Lambda calculus (section)

=== Arithmetic in lambda calculus ===
There are several possible ways to define the [[natural number]]s in lambda calculus, but by far the most common are the [[Church numeral]]s, which can be defined as follows:
: {{Mono|1=0 := λ''f''.λ''x''.''x''}}
: {{Mono|1=1 := λ''f''.λ''x''.''f'' ''x''}}
: {{Mono|1=2 := λ''f''.λ''x''.''f'' (''f'' ''x'')}}
: {{Mono|1=3 := λ''f''.λ''x''.''f'' (''f'' (''f'' ''x''))}}
and so on. Or using the alternative syntax presented above in ''[[#Notation|Notation]]'':

: {{Mono|1=0 := λ''fx''.''x''}}
: {{Mono|1=1 := λ''fx''.''f'' ''x''}}
: {{Mono|1=2 := λ''fx''.''f'' (''f'' ''x'')}}
: {{Mono|1=3 := λ''fx''.''f'' (''f'' (''f'' ''x''))}}

A Church numeral is a [[higher-order function]]—it takes a single-argument function {{Mono|''f''}}, and returns another single-argument function. The Church numeral {{Mono|''n''}} is a function that takes a function {{Mono|''f''}} as argument and returns the {{Mono|''n''}}-th composition of {{Mono|''f''}}, i.e. the function {{Mono|''f''}} composed with itself {{Mono|''n''}} times. This is denoted {{Mono|''f''<sup>(''n'')</sup>}} and is in fact the {{Mono|''n''}}-th power of {{Mono|''f''}} (considered as an operator); {{Mono|''f''<sup>(0)</sup>}} is defined to be the identity function. Such repeated compositions (of a single function {{Mono|''f''}}) obey the [[laws of exponents]], which is why these numerals can be used for arithmetic. (In Church's original lambda calculus, the formal parameter of a lambda expression was required to occur at least once in the function body, which made the above definition of {{Mono|0}} impossible.)

One way of thinking about the Church numeral {{Mono|''n''}}, which is often useful when analysing programs, is as an instruction 'repeat ''n'' times'. For example, using the {{Mono|PAIR}} and {{Mono|NIL}} functions defined below, one can define a function that constructs a (linked) list of ''n'' elements all equal to ''x'' by repeating 'prepend another ''x'' element' ''n'' times, starting from an empty list. The lambda term is
: {{Mono|λ''n''.λ''x''.''n'' (PAIR ''x'') NIL}}
By varying what is being repeated, and varying what argument that function being repeated is applied to, a great many different effects can be achieved.

We can define a successor function, which takes a Church numeral {{Mono|''n''}} and returns {{Mono|''n'' + 1}} by adding another application of {{Mono|''f''}}, where '(mf)x' means the function 'f' is applied 'm' times on 'x':
: {{Mono|1=SUCC := λ''n''.λ''f''.λ''x''.''f'' (''n'' ''f'' ''x'')}}
Because the {{Mono|''m''}}-th composition of {{Mono|''f''}} composed with the {{Mono|''n''}}-th composition of {{Mono|''f''}} gives the {{Mono|''m''+''n''}}-th composition of {{Mono|''f''}}, addition can be defined as follows:
: {{Mono|1=PLUS := λ''m''.λ''n''.λ''f''.λ''x''.''m'' ''f'' (''n'' ''f'' ''x'')}}
{{Mono|PLUS}} can be thought of as a function taking two natural numbers as arguments and returning a natural number; it can be verified that
: {{Mono|PLUS 2 3}}
and
: {{Mono|5}}
are β-equivalent lambda expressions. Since adding {{Mono|''m''}} to a number {{Mono|''n''}} can be accomplished by adding 1 {{Mono|''m''}} times, an alternative definition is:
: {{Mono|1=PLUS := λ''m''.λ''n''.''m'' SUCC ''n ''}}<ref>{{Citation|last1=Felleisen|first1=Matthias|last2=Flatt|first2=Matthew|title=Programming Languages and Lambda Calculi|year=2006|page=26|url=http://www.cs.utah.edu/plt/publications/pllc.pdf|archive-url=https://web.archive.org/web/20090205113235/http://www.cs.utah.edu/plt/publications/pllc.pdf|archive-date=2009-02-05}}; A note (accessed 2017) at the original location suggests that the authors consider the work originally referenced to have been superseded by a book.</ref>
Similarly, multiplication can be defined as
: {{Mono|1=MULT := λ''m''.λ''n''.λ''f''.''m'' (''n'' ''f'')}}<ref name="Selinger" />
Alternatively
: {{Mono|1=MULT := λ''m''.λ''n''.''m'' (PLUS ''n'') 0}}
since multiplying {{Mono|''m''}} and {{Mono|''n''}} is the same as repeating the add {{Mono|''n''}} function {{Mono|''m''}} times and then applying it to zero.
Exponentiation has a rather simple rendering in Church numerals, namely
: {{Mono|1=POW := λ''b''.λ''e''.''e'' ''b''}}<ref name="BarendregtBarendsen" />
The predecessor function defined by {{Mono|1=PRED ''n'' = ''n'' − 1}} for a positive integer {{Mono|''n''}} and {{Mono|1=PRED 0 = 0}} is considerably more difficult. The formula
: {{Mono|1=PRED := λ''n''.λ''f''.λ''x''.''n'' (λ''g''.λ''h''.''h'' (''g'' ''f'')) (λ''u''.''x'') (λ''u''.''u'')}}
can be validated by showing inductively that if ''T'' denotes {{Mono|(λ''g''.λ''h''.''h'' (''g'' ''f''))}}, then {{Mono|1=T<sup>(''n'')</sup>(λ''u''.''x'') = (λ''h''.''h''(''f''<sup>(''n''−1)</sup>(''x'')))}} for {{Mono|''n'' > 0}}. Two other definitions of {{Mono|PRED}} are given below, one using [[#Logic and predicates|conditionals]] and the other using [[#Pairs|pairs]]. With the predecessor function, subtraction is straightforward. Defining
: {{Mono|1=SUB := λ''m''.λ''n''.''n'' PRED ''m''}},
{{Mono|SUB ''m'' ''n''}} yields {{Mono|''m'' − ''n''}} when {{Mono|''m'' > ''n''}} and {{Mono|0}} otherwise.