Editing Fixed-point combinator (section)

== Recursive definitions and fixed-point combinators ==

Fixed-point combinators can be used to implement [[recursive definition]] of functions. However, they are rarely used in practical programming.<ref>{{cite web |title=For those of us who don't know what a Y-Combinator is or why it's useful, ... |url=https://news.ycombinator.com/item?id=17953711 |website=Hacker News |access-date=2 August 2020}}</ref> [[Strongly normalizing]] [[type system]]s such as the [[simply typed lambda calculus]] disallow non-termination and hence fixed-point combinators often cannot be assigned a type or require complex type system features. Furthermore fixed-point combinators are often inefficient compared to other strategies for implementing recursion, as they require more function reductions and construct and take apart a tuple for each group of mutually recursive definitions.<ref name="SPJ1987" />{{rp|page 232}}

=== 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.