Values and domains

Every expression has one value. This is true in general mathematics and it must be true in lambda calculus. This means that in lambda calculus, applying a fixed-point combinator to a function gives you an expression whose value is the fixed point of the function.

However, this is a value in the lambda calculus domain, it may not correspond to any value in the domain of the function, so in a practical sense it is not necessarily a fixed point of the function, and only in the lambda calculus domain is it a fixed point of the equation.

For example, consider

${\displaystyle x^{2}=-1\Rightarrow x={\frac {-1}{x}}\Rightarrow f\ x={\frac {-1}{x}}\land {\mathsf {Y}}\ f=x}$

Division of signed numbers may be implemented in the Church encoding, so f may be represented by a lambda term. This equation has no solution in the real numbers. But in the domain of the complex numbers i and -i are solutions. This demonstrates that there may be solutions to an equation in another domain. However, the lambda term for the solution for the above equation is weirder than that. The lambda term ${\displaystyle {\mathsf {Y}}\ f}$ represents the state where x could be either i or -i, as one value. The information distinguishing these two values has been lost, in the change of domain. Note that this may still be represented as a single value, if the logic is expanded to be paraconsistent.

For the lambda calculus mathematician, this is a consequence of the definition of lambda calculus. For the programmer, it means that the beta reduction of the lambda term will loop forever, never reaching a normal form.

Function versus implementation

The fixed-point combinator may be defined in mathematics and then implemented in other languages. General mathematics defines a function based on its extensional properties.^[3] That is, two functions are equal if they perform the same mapping. Lambda calculus and programming languages regard function identity as an intensional property. A function's identity is based on its implementation.

A lambda calculus function (or term) is an implementation of a mathematical function. In the lambda calculus there are a number of combinators (implementations) that satisfy the mathematical definition of a fixed-point combinator.

Definition of the term "combinator"

Combinatory logic is a higher-order functions theory. A combinator is a closed lambda expression, meaning that it has no free variables. The combinators may be combined to direct values to their correct places in the expression without ever naming them as variables.

The factorial function

The factorial function provides a good example of how the fixed-point combinator may be applied. The result demonstrates simple recursion, as would be implemented in a single loop in an imperative language. The definition of numbers used is explained in Church encoding.

The function taking itself as a parameter is

${\displaystyle F\ f\ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (f\ (\operatorname {pred} \ n)))\ .}$

This gives Y F n as

${\displaystyle {\begin{aligned}{\textsf {fix}}\ F\ n&=F\ ({\textsf {fix}}\ F)\ n\\&=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (({\textsf {fix}}\ F)\ (\operatorname {pred} \ n)))\ .\end{aligned}}}$

Setting ${\displaystyle {\textsf {fix}}\ F=\operatorname {fact} }$ gives

${\displaystyle \operatorname {fact} \ n=(\operatorname {IsZero} \ n)\ 1\ (\operatorname {multiply} \ n\ (\operatorname {fact} \ (\operatorname {pred} \ n)))\ .}$

This definition puts F in the role of the body of a loop to be iterated, and is equivalent to the mathematical definition of factorial:

${\displaystyle \operatorname {fact} \ n={\begin{cases}1&{\text{if}}~n=0\\n\times \operatorname {fact} \ (n-1)&{\text{otherwise.}}\end{cases}}}$

Equivalent definition of a fixed-point combinator

This fixed-point combinator may be defined as y, as in

${\displaystyle x=f\ x\land y\ f=x}$

An expression for y may be derived using rules from the definition of a let expression. Firstly, using the rule

${\displaystyle (\exists xE\land F)\iff \operatorname {let} x:E\operatorname {in} F}$

gives

${\displaystyle \operatorname {let} x=f\ x\operatorname {in} y\ f=x}$

Also, using

${\displaystyle x\not \in \operatorname {FV} (E)\land x\in \operatorname {FV} (F)\to \operatorname {let} x:G\operatorname {in} E\ F=E\ (\operatorname {let} x:G\operatorname {in} F)}$

gives

${\displaystyle y\ f=\operatorname {let} x=f\ x\operatorname {in} x}$

And then using the eta reduction rule

${\displaystyle f\ x=y\iff f=\lambda x.y}$

gives

${\displaystyle y=\lambda f.\operatorname {let} x=f\ x\operatorname {in} x}$

Derivation of the Y combinator

Curry's Y combinator may be readily obtained from the definition of y.^[5]

We begin with

${\displaystyle \lambda f.\operatorname {let} x=f\ x\operatorname {in} x}$

A lambda abstraction does not support reference to the variable name in the applied expression, so x must be passed in as a parameter to x. We can think of this as replacing x by x x, but formally this is not correct. Instead defining y by ${\displaystyle \forall z,y\ z=x}$ gives

${\displaystyle \lambda f.\operatorname {let} y\ z=f\ (y\ z)\operatorname {in} y\ z\ .}$

The let expression may be regarded as the definition of the function y, where z is the parameter. Instantiation z as y in the call gives

${\displaystyle \lambda f.\operatorname {let} y\ z=f\ (y\ z)\operatorname {in} y\ y\ .}$

And, because the parameter z always passes the function y,

${\displaystyle \lambda f.\operatorname {let} y\ z=f\ (z\ z)\operatorname {in} y\ y\ .}$

Using the eta reduction rule,

${\displaystyle f\ x=y\equiv f=\lambda x.y\ ,}$

gives

${\displaystyle \lambda f.\operatorname {let} y=\lambda z.f\ (z\ z)\operatorname {in} y\ y\ .}$

A let expression may be expressed as a lambda abstraction; using

${\displaystyle n\not \in FV(E)\to (\operatorname {let} n=E\operatorname {in} L\equiv (\lambda n.L)\ E)}$

gives

${\displaystyle \lambda f.(\lambda y.y\ y)\ (\lambda z.f\ (z\ z))\ .}$

This is possibly the simplest implementation of a fixed-point combinator in lambda calculus. However, one beta reduction gives the more symmetrical form of Curry's Y combinator:

${\displaystyle \lambda f.(\lambda z.f\ (z\ z))\ (\lambda z.f\ (z\ z))\ .}$

See also Translating between let and lambda expressions.

Other fixed-point combinators

In untyped lambda calculus fixed-point combinators are not especially rare. In fact there are infinitely many of them.^[6] In 2005 Mayer Goldberg showed that the set of fixed-point combinators of untyped lambda calculus is recursively enumerable.^[7]

The Y combinator can be expressed in the SKI-calculus as

${\displaystyle Y=S(K(SII))(S(S(KS)K)(K(SII)))}$

Additional combinators (B, C, K, W system) allow for a much shorter definition. With U = SII the self-application combinator, since S(Kx)yz = x(yz) = Bxyz and Sx(Ky)z = xzy = Cxyz, the above becomes

${\displaystyle Y=S(KU)(SB(KU))=BU(CBU)}$

The simplest fixed-point combinator in the SK-calculus, found by John Tromp, is

${\displaystyle Y'=SSK(S(K(SS(S(SSK))))K)}$

although note that it is not in normal form, which is longer. This combinator corresponds to the lambda expression

${\displaystyle Y'=(\lambda xy.xyx)(\lambda yx.y(xyx))}$

The following fixed-point combinator is simpler than the Y combinator, and β-reduces into the Y combinator; it is sometimes cited as the Y combinator itself:

${\displaystyle X=\lambda f.(\lambda x.xx)(\lambda x.f(xx))}$

Another common fixed-point combinator is the Turing fixed-point combinator (named after its discoverer, Alan Turing):^{[8][2]: 132}

${\displaystyle \Theta =(\lambda xy.y(xxy))\ (\lambda xy.y(xxy))}$

Its advantage over ${\displaystyle {\textsf {Y}}}$ is that ${\displaystyle \Theta \ f}$ beta-reduces to ${\displaystyle f\ (\Theta f)}$,^{[note 3]} whereas ${\displaystyle {\textsf {Y}}\ f}$ and ${\displaystyle f\ ({\textsf {Y}}f)}$ only beta-reduce to a common term.^{[note 2]}

${\displaystyle \Theta }$ also has a simple call-by-value form:

${\displaystyle \Theta _{v}=(\lambda xy.y(\lambda z.xxyz))\ (\lambda xy.y(\lambda z.xxyz))}$

The analog for mutual recursion is a polyvariadic fix-point combinator,^[9][10][11] which may be denoted Y*.

Strict fixed-point combinator

In a strict programming language the Y combinator will expand until stack overflow, or never halt in case of tail call optimization.^[12] The Z combinator will work in strict languages (also called eager languages, where applicative evaluation order is applied). The Z combinator has the next argument defined explicitly, preventing the expansion of Z g in the right-hand side of the definition:^[13]

${\displaystyle Zgv=g(Zg)v\ .}$

and in lambda calculus it is an eta-expansion of the Y combinator:

${\displaystyle Z=\lambda f.(\lambda x.f(\lambda v.xxv))\ (\lambda x.f(\lambda v.xxv))\ .}$

Non-standard fixed-point combinators

In untyped lambda calculus there are terms that have the same Böhm tree as a fixed-point combinator, that is they have the same infinite extension λx.x (x (x ... )). These are called non-standard fixed-point combinators. Any fixed-point combinator is also a non-standard one, but not all non-standard fixed-point combinators are fixed-point combinators because some of them fail to satisfy the equation that defines the "standard" ones. These strange combinators are called strictly non-standard fixed-point combinators; an example is the following combinator:

${\displaystyle N=BM(B(BM)B)}$

where

${\displaystyle B=\lambda xyz.x(yz)}$

${\displaystyle M=\lambda x.xx\ .}$

The set of non-standard fixed-point combinators is not recursively enumerable.^[7]

Lazy functional implementation

In a language that supports lazy evaluation, like in Haskell, it is possible to define a fixed-point combinator using the defining equation of the fixed-point combinator which is conventionally named fix. Since Haskell has lazy datatypes, this combinator can also be used to define fixed points of data constructors (and not only to implement recursive functions). The definition is given here, followed by some usage examples. In Hackage, the original sample is: ^[14]

fix, fix' :: (a -> a) -> a
fix f = let x = f x in x         -- Lambda dropped. Sharing.
                                 -- Original definition in Data.Function.
-- alternative:
fix' f = f (fix' f)              -- Lambda lifted. Non-sharing.

fix (\x -> 9)                    -- this evaluates to 9

fix (\x -> 3:x)                  -- evaluates to the lazy infinite list [3,3,3,...]

fact = fix fac                   -- evaluates to the factorial function
  where fac f 0 = 1
        fac f x = x * f (x-1)

fact 5                           -- evaluates to 120

Strict functional implementation

In a strict functional language, as illustrated below with OCaml, the argument to f is expanded beforehand, yielding an infinite call sequence,

${\displaystyle f\ (f...(f\ ({\mathsf {fix}}\ f))...)\ x}$.

This may be resolved by defining fix with an extra parameter.

let rec fix f x = f (fix f) x (* note the extra x; here fix f = \x-> f (fix f) x *)

let factabs fact = function   (* factabs has extra level of lambda abstraction *)
   0 -> 1
 | x -> x * fact (x-1)

let _ = (fix factabs) 5       (* evaluates to "120" *)

In a multi-paradigm functional language (one decorated with imperative features), such as Lisp, Landin (1963) suggests the use of a variable assignment to create a fixed-point combinator, as in the below example using Scheme:

(define Y!
  (lambda (f)
    ((lambda (i)                       
       (set! i (f (lambda (x) (i x)))) ;; (set! i expr) assigns i the value of expr
       i)                              ;; replacing it in the present lexical scope
     #f)))

Using a lambda calculus with axioms for assignment statements, it can be shown that Y! satisfies the same fixed-point law as the call-by-value Y combinator:^[15][16]

${\displaystyle ({\textsf {Y}}_{!}\ \lambda x.e)e'=(\lambda x.e)\ ({\textsf {Y}}_{!}\ \lambda x.e)e'}$

In more idiomatic modern Lisp usage, this would typically be handled via a lexically scoped label (a let expression), as lexical scope was not introduced to Lisp until the 1970s:

(define Y*
  (lambda (f)
    ((lambda (i)
       (let ((i (f (lambda (x) (i x))))) ;; (let ((i expr)) i) locally defines i as expr
	     i))                             ;; non-recursively: thus i in expr is not expr
     #f)))

Or without the internal label:

(define Y
  (lambda (f)
    ((lambda (i) (i i))
     (lambda (i)
       (f (lambda (x)
	        (apply (i i) x)))))))

Imperative language implementation

This example is a slightly interpretive implementation of a fixed-point combinator. A class is used to contain the fix function, called fixer. The function to be fixed is contained in a class that inherits from fixer. The fix function accesses the function to be fixed as a virtual function. As for the strict functional definition, fix is explicitly given an extra parameter x, which means that lazy evaluation is not needed.

template <typename R, typename D>
class fixer
{
public:
    R fix(D x)
    {
        return f(x);
    }
private:
    virtual R f(D) = 0;
};

class fact : public fixer<long, long>
{
    virtual long f(long x)
    {
        if (x == 0)
        {
            return 1;
        }
        return x * fix(x-1);
    }
};

long result = fact().fix(5);

Type for the Y combinator

In programming languages that support recursive data types, it is possible to type the Y combinator by appropriately accounting for the recursion at the type level. The need to self-apply the variable x can be managed using a type (Rec a), which is defined so as to be isomorphic to (Rec a -> a).

For example, in the following Haskell code, we have In and out being the names of the two directions of the isomorphism, with types:^[18][19]

In :: (Rec a -> a) -> Rec a
out :: Rec a -> (Rec a -> a)

which lets us write:

newtype Rec a = In { out :: Rec a -> a }

y :: (a -> a) -> a
y = \f -> (\x -> f (out x x)) (In (\x -> f (out x x)))

Or equivalently in OCaml:

type 'a recc = In of ('a recc -> 'a)
let out (In x) = x

let y f = (fun x a -> f (out x x) a) (In (fun x a -> f (out x x) a))

Alternatively:

let y f = (fun x -> f (fun z -> out x x z)) (In (fun x -> f (fun z -> out x x z)))