Note: this is moved from my old blog.

Currently, I am learning Lambda Calculus, and the Y combinator. And I am going to talk about why people need such kind of combinators, but how it is derived will not be covered since there are a lot of great articles explaining it. Great thanks to the explanation given by my senior, Zhiqiang (Alex) Ren!

Great to Read First

These materials are really great and very important. Be sure you read them first if you really want to know fixpoint combinator.

Why We Need Fixpoint Combinator

In pure untyped lambda calculus, we cannot define a recursive term like we do in programming languages like C. For example, we give the factorial function (lambda abstraction) the name fact, then it could be expressed as,

\( \lambda n. \verb!if !n < 1 \verb! then !1 \verb! else fact! (n - 1)\)

However, the fact in this lambda term is a free variable, and there is actually no way to do the same thing as we say "we give the factorial function a name" and use that name in the body recursively in lambda calculus. If you really want to do "give something a name", you may try to introduce bindings by using lambda abstraction, which seems like this,

\( (\lambda \verb!fact!. \lambda n. \ldots \verb! else fact! (n-1)) (\lambda n. \ldots \verb! else fact!(n-1))\)

Yes, you see that we pass the recursive function itself to itself, so that we can call the function recursively. (This idea could be furture expanded in those "Great to Read" materials. Check them out, strongly recommended!) But there are two problems. First, the fact in the second part, is still undefined, it's a free variable. Second, since the second fact is not bound, this definition can only "recurs" once. If you really want to define a factorial function that can compute for all valid N, the definition could result in a infinite loop.

Thus, we need fixpoint in lambda calculus so that we can define terms to compute recursive problems.

Usage of Fixpoint Combinator

It doesn't mean that any languages that support recursive definitions are implemented using fixpoint combinators. For example, C language simply uses "call" to call itself. And it is recursive with the help of function call stack and the hardware. It just works that way, and has nothing to do with lambda calculus and fixpoint. But, if someone implements a language that based on lambda calculus, it should provide fixpoint combinator internally, to support recursive definition on the grammar level. (That means, by parsing the recursive source code, it will generate non-recursive lambda terms, and combine it with fixpoint combinator to compute data recursively.)

Types of Fixpoint Combinator

Because different interpreters have different evaluation strategies, like call-by-value (applicative-order), call-by-name (normal-order), call-by-need (an optimized implementation of call-by-name) and call-by-reference, you need to supply different combinators to avoid evaluation problems. Call-by-name combinators may be result in an infinite substitution in a call-by-value interpreter. These are explained in those materials.

One way to avoid an infinite substitution is to wrap a lambda expression into a lambda abstraction. Because lambda expression is going to be evaluated immediately, but a lambda abstraction will only be evaluated when it is applied. This is a great idea I found in those materials.