Skip to main content

Chapter 5: Fixed Points and Recursion

Fixed Points​

In regular mathematics, a fixed point x0x_0 of a function ff is a point that maps back to itself, i.e.

f(x0)=x0f(x_0)=x_0

In regular mathematics, not all functions have a fixed point. But in lambda calculus, everything is a function and has a fixed point.

Fixed-point Combinators​

How to solve fixed points of a function? It may surprise you that there is a kind of functions called fixed-point combinators capable to generate fixed points from arbitrary function by applying it with the function. I will introduce two of them.

Curry’s Paradoxical Combinator:Y=λf.(λx.f(xx))(λx.f(xx))Turing Combinator:Θ=(λxy.y(xxy))(λxy.y(xxy))\begin{array}{} \text{Curry's Paradoxical Combinator:}&Y&=&\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))\\ \text{Turing Combinator:}&\Theta&=&(\lambda xy.y(xxy))(\lambda xy.y(xxy)) \end{array}

For arbitrary function FF, it has two fixed points (YF)(YF) and (ΘF)(\Theta F), i. e. F(YF)=YFF(YF)=YF and F(ΘF)=ΘFF(\Theta F)=\Theta F.

Proof:

YF=(λf.(λx.f(xx))(λx.f(xx)))F=(λx.F(xx))(λx.F(xx))=F((λx.F(xx))(λx.F(xx)))=F(YF)ΘF=(λxy.y(xxy))(λxy.y(xxy))F=F((λxy.y(xxy))(λxy.y(xxy))F)=F(ΘF)\begin{array}{} YF&=&(\lambda f.(\lambda x.f(xx))(\lambda x.f(xx)))F\\ &=&(\lambda x.F(xx))(\lambda x.F(xx))\\ &=&F((\lambda x.F(xx))(\lambda x.F(xx)))\\ &=&F(YF) \end{array}\\ \begin{array}{} \Theta F&=&(\lambda xy.y(xxy))(\lambda xy.y(xxy))F\\ &=&F((\lambda xy.y(xxy))(\lambda xy.y(xxy))F)\\ &=&F(\Theta F) \end{array}

Infinity​

What if I apply fixed-point combinator with succussor function SS?

YS=S(YS)=S(S(YS))=⋯=S(S(S(⋯ )))=∞YS=S(YS)=S(S(YS))=\cdots=S(S(S(\cdots)))=\infty

Let's call it infinity. And it still meet requirement of a fixed point, since

S(∞)=∞S(\infty)=\infty

is reasonable and acceptable.

Recursion​

To implement certain algorithms, recursion is often needed. Let's take factorial\text{factorial} for example:

factorial=λn.(is-zero n)1(mul n(factorial(pred n)))\text{factorial}=\lambda n.(\text{is-zero }n)1(\text{mul }n(\text{factorial}(\text{pred }n)))

Since functions are anonymous, the name of the function is not assigned until the full definition of the function, So factorial\text{factorial} is actually used before its full definition, which is a hideous logical defect! Don't panic, let's take advantages of fixed points!

Take an inverse β\beta reduction on the right:

factorial=(λf.λn.(is-zero n)1(mul n(f(pred n))))factorial\text{factorial}=(\lambda f.\lambda n.(\text{is-zero }n)1(\text{mul }n(f(\text{pred }n))))\text{factorial}

Observe this carefully. It states that factorial\text{factorial} is a fixed point of

(λf.λn.(is-zero n)1(mul n(f(pred n))))(\lambda f.\lambda n.(\text{is-zero }n)1(\text{mul }n(f(\text{pred }n))))

Which means, the definition of factorial\text{factorial} could be rewritten as:

factorial=Θ(λf.λn.(is-zero n)1(mul n(f(pred n))))\text{factorial}=\Theta(\lambda f.\lambda n.(\text{is-zero }n)1(\text{mul }n(f(\text{pred }n))))

Perhaps you did never associate fixed points and recursion together before this fantastic journey. Mathematical consequence may be far beyond our imagination.

Division, Remainder and Logarithm​

With the help of recursion, the decrement of church numerals speeds up.

div=Θ(λf.λmn.(lt mn)0(add 1(f(sub mn)n)))rem=Θ(λf.λmn.(lt mn)m(f(sub mn)n))log=Θ(λf.λmn.(lt mn)0(add 1(f(div mn)n)))\text{div}=\Theta(\lambda f.\lambda mn.(\text{lt }mn)0(\text{add }1(f(\text{sub }mn)n)))\\ \text{rem}=\Theta(\lambda f.\lambda mn.(\text{lt }mn)m(f(\text{sub }mn)n))\\ \text{log}=\Theta(\lambda f.\lambda mn.(\text{lt }mn)0(\text{add }1(f(\text{div }mn)n)))

Recursive Algorithms and Data Structures​

Recursive algorithms work well with recursive data structures such as linked list. A typical reduction function could be defined as:

reduce=Θ(λf.λlr.(is-nil (pop-front l))(get-front l)(r(get-front l)(f(pop-front l)r)))\text{reduce}=\Theta(\lambda f.\lambda lr.(\text{is-nil }(\text{pop-front }l))(\text{get-front }l)(r(\text{get-front }l)(f(\text{pop-front }l)r)))

With l=(1,3,5)l=(1,3,5), you could get:

reduce ladd=9reduce lmul=15\text{reduce }l\text{add}=9\\ \text{reduce }l\text{mul}=15

With the powerful weapon of recursion, now it is not difficult to implement arbitrary computational task via lambda calculus.