Editing Fixed-point combinator (section)

=== The factorial function ===

The [[factorial|factorial function]] provides a good example of how a fixed-point combinator may be used to define recursive functions. The standard recursive definition of the factorial function in mathematics can be written as

: <math>\operatorname{fact}\ n = \begin{cases}
1 & \text{if} ~ n = 0 \\
n \times \operatorname{fact}(n - 1) & \text{otherwise.}
\end{cases}</math>

where ''n'' is a non-negative integer.
Implementing this in lambda calculus, where integers are represented using [[Church encoding]], encounters the problem that the lambda calculus disallows the name of a function ('fact') to be used in the function's definition. This can be circumvented using a fixed-point combinator <math>\textsf{fix}</math> as follows.

Define a function ''F'' of two arguments ''f'' and ''n'':
: <math>F\ f\ n = (\operatorname{IsZero}\ n)\ 1\ (\operatorname{multiply}\ n\ (f\ (\operatorname{pred}\ n)))</math>
(Here <math>(\operatorname{IsZero}\ n)</math> is a function that takes two arguments and returns its first argument if ''n''=0, and its second argument otherwise; <math>\operatorname{pred}\ n</math> evaluates to ''n''-1.)

Now define <math>\operatorname{fact}=\textsf{fix}\ F</math>. Then <math>\operatorname{fact}</math> is a fixed-point of ''F'', which gives
: <math>\begin{align} \operatorname{fact} n 
 &= F\ \operatorname{fact}\ n \\
 &= (\operatorname{IsZero}\ n)\ 1\ (\operatorname{multiply}\ n\ (\operatorname{fact}\ (\operatorname{pred}\ n)))\ 
\end{align}</math>

as desired.