Fixed point combinator

A fixed point combinator (or fixed-point operator) is a higher-order function that computes a fixed point of other functions. This operation is relevant in programming language theory because it allows the implementation of recursion in the form of a rewrite rule, without explicit support from the language's runtime engine.

A fixed point of a function f is a value x such that f(x) = x. For example, 0 and 1 are fixed points of the function f(x) = x2, because 02 = 0 and 12 = 1. Whereas a fixed-point of a first-order function (a function on "simple" values such as integers) is a first-order value, a fixed point of a higher-order function f is another function p such that f(p) = p. A fixed point combinator, then, is a function g which produces such a fixed point p for any function f:

p = g(f), f(p) = p

or, alternately:

f(g(f)) = g(f).

Fixed point combinators allow the definition of anonymous recursive functions (see the example below). Somewhat surprisingly, they can be defined with non-recursive lambda abstractions.

Y combinator

One well-known (and perhaps the simplest) fixed point combinator in the untyped lambda calculus is called the Y combinator. It was discovered by Haskell B. Curry, and is defined as

Y = λf·(λx·f (x x)) (λx·f (x x))

We can see that this function acts as a fixed point combinator by expanding it for an example function g:

```Y g = (λf . (λx . f (x x)) (λx . f (x x))) g
Y g = (λx . g (x x)) (λx . g (x x)) (β-reduction of λf - applied main function to g)
Y g = (λy . g (y y)) (λx . g (x x)) (α-conversion - renamed bound variable)
Y g = g ((λx . g (x x)) (λx . g (x x))) (β-reduction of λy - applied left function to right function)
Y g = g (Y g) (definition of Y)
```

Note that the Y combinator is intended for the call-by-name evaluation strategy, since (Y g) diverges (for any g) in call-by-value settings.

Existence of fixed point combinators

In certain mathematical formalizations of computation, such as the untyped lambda calculus and combinatory logic, every expression can be considered a higher-order function. In these formalizations, the existence of a fixed-point combinator means that every function has at least one fixed point; a function may have more than one distinct fixed point.

In some other systems, for example the simply typed lambda calculus, a well-typed fixed-point combinator cannot be written. In those systems any support for recursion must be explicitly added to the language. In still others, such as the simply-typed lambda calculus extended with recursive types, fixed-point operators can be written, but the type of a "useful" fixed-point operator (one whose application always returns) may be restricted.

In a language which supports lazy evaluation, the Y combinator can be written with type ∀a.(a→a)→a. For example, the following Haskell code correctly implements the Y combinator:

```fix :: (a -> a) -> a
fix f = f (fix f)

-- "fix (const 9)" evaluates to "9"

fact f 0 = 1
fact f x = x * f (x-1)

-- "(fix fact) 5" evaluates to "120"
```

Note that this definition doesn't infinitely loop because of laziness. However, the above version loops forever when applied in a strict programming language -- every application Y(f) expands to f(Y(f)). The argument to f is then expanded, as required for a call-by-value language, yielding f(f(Y(f))). This process iterates "forever" (until the system runs out of memory), without ever actually evaluating the body of f.

The strict version of the Y combinator has the type ∀a.∀b.((a→b)→(a→b))→(a→b) (in other words, it only works on a function which itself takes and returns a function). For example, the following OCaml code implements this version of the Y combinator:

```let rec fix f x = f (fix f) x

let fact f = function
0 -> 1
| x -> x * f (x-1)

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

Example

Consider the factorial function (under Church encoding). The usual recursive mathematical equation is

fact(n) = if n=0 then 1 else n * fact(n-1)

We can express a "single step" of this recursion in lambda calculus as

F = λf. λx. (ISZERO x) 1 (MULT x (f (PRED x))),

where "f" is a place-holder argument for the factorial function to be passed to itself. The function F performs a single step in the evaluation of the recursive formula. Applying the fix operator gives

fix(F)(n) = F(fix(F))(n)
fix(F)(n) = λx. (ISZERO x) 1 (MULT x (fix(F) (PRED x)))(n)
fix(F)(n) = (ISZERO n) 1 (MULT n (fix(F) (PRED n)))

We can abbreviate fix(F) as fact, and we have

fact(n) = (ISZERO n) 1 (MULT n (fact(PRED n)))

So we see that a fixed-point operator really does turn our non-recursive "factorial step" function into a recursive function satisfying the intended equation.

Other fixed point combinators

A version of the Y combinator that can be used in call-by-value (applicative-order) evaluation is given by η-expansion of part of the ordinary Y combinator:

Z = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))

Here is an example of this in Python:

```>>> Z = lambda f: (lambda x: f(lambda *args: x(x)(*args)))(lambda x: f(lambda *args: x(x)(*args)))
>>> fact = lambda f: lambda x: 1 if x == 0 else x * f(x-1)
>>> Z(fact)(5)
120
```

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

Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))

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

Y' = S S K (S (K (S S (S (S S K)))) K)

which corresponds to the lambda expression

Y' = (λx. λy. x y x) (λy. λx. y (x y x))

Another common fixed point combinator is the Turing fixed-point combinator (named after its discoverer, Alan Turing):

Θ = (λx. λy. (y (x x y))) (λx. λy. (y (x x y)))

It also has a simple call-by-value form:

Θv = (λx. λy. (y (λz. x x y z))) (λx. λy. (y (λz. x x y z)))

Fixed point combinators are not especially rare (there are infinitely many of them). Some, such as this one (constructed by Jan Willem Klop) are useful chiefly for amusement:

Yk = (L L L L L L L L L L L L L L L L L L L L L L L L L L)

where:

L = λabcdefghijklmnopqstuvwxyzr. (r (t h i s i s a f i x e d p o i n t c o m b i n a t o r))

Example of encoding via recursive types

In systems with recursive types, it's 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:

```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))
```
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0, "url": "http://taggedwiki.zubiaga.org/new_content/44e45bff552833cb7460ea1529cf9ea6", "fetch_time": 1553310896000000000, "content_mime_type": "text/html", "warc_filename": "crawl-data/CC-MAIN-2019-13/segments/1552912202711.3/warc/CC-MAIN-20190323020538-20190323042538-00281.warc.gz", "warc_record_offset": 191998502, "warc_record_length": 10619, "token_count": 1976, "char_count": 6938, "score": 3.75, "int_score": 4, "crawl": "CC-MAIN-2019-13", "snapshot_type": "latest", "language": "en", "language_score": 0.8613969087600708, "file_path": "/sailhome/yjruan/project/latent-lm/data/processed/finemath-4plus/finemath-4plus/train-00050-of-00064.parquet"}