display | more...

A combinator Y that, for any term f in the lambda calculus, we have f (Y f) = Y f. Or in other words, it is a combinator that, when given any lambda term f as input, returns a fixed point x for f, i.e. f x = x. The first such combinator was found by Haskell B. Curry and is known as the Y combinator or Y operator.

This combinator is defined as follows:

Y = λf.(λ.x.f(x x))(λ.x.f(x x))

It is a simple exercise to show that it acts as a fixed point combinator as described above, however, it is only valid for lambda-equality and produces certain difficulties when reduction is performed (Try to perform reduction on f (Y f)... at some point a backwards beta reduction needs to be performed). Another fixed point combinator T was found by Alan Turing that doesn't have this undesirable property:

T = (λx.λy.y (x x y)(λx.λy.y (x x y))

Yet another fixed point combinator, which is very useful because it is the shortest known one when converted to the S and K basic combinators, is:

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

In terms of the S and K combinators this is:

Y' = SSK(S(K(SS(S(SSK))))K)

12 terms, as opposed to 18 terms for Curry's fixed point combinator and 20 terms for Turing's.

These combinators are useful because they allow one to define recursive functions without the need for names. For example, the factorial function:

fact(n) = if (iszero? n) then 1 else n*fact(pre n)

(iszero? is a function returning true for n=0, and pre is a function that returns one less than its argument). We can transform this into:

fact = λn.if (iszero? n) then 1 else n*fact(pre n)

which we can also write this way:

fact = (λf.λn.if (iszero? n) then 1 else n*f(pre n)) fact

Now fact has been expressed as a fixed point of this function:

F = λf.λn.if (iszero? n) then 1 else n*f(pre n))

So we can define the factorial as:

fact = Y λf.λn.if (iszero? n) then 1 else n*f(pre n))

Note that this only works if the functional language implementing this uses call by need semantics (lazy evaluation), or call by name semantics (normal order evaluation), such as Miranda or Haskell. In a functional language that uses call by value semantics (eager evaluation or strict evaluation), fixed point combinators won't produce recursive effects because their arguments are evaluated before the body, resulting in an infinite loop. For instance, doing strict evaluation on: Y f produces f Y f, which when evaluated will evaluate Y f before attempting to evaluate f, which will then produce f f Y f, and so on and on forever, or until recursion is terminated by memory exhaustion. Special steps need to be taken in order to provide for fixed point combinators in such languages.

Log in or register to write something here or to contact authors.