9/17/19
Now we can attempt to write a recursive function. Let us try for a length of list function. Something like
length(list) = df. If (list is empty) then 0 else succ(length(tail(list)))
we can do all this with the materials we have apart from the fact that the name 'length' appears in the body of the function and in lambda calculus there are no names.
This obstacle is overcome by what is known as a fix-point combinator (and the next little piece is something with intellectual content).
In general, if we have a free variable in an expression that we would prefer not to be there, we can displace it somewhat (out of the expression and to an argument) by abstracting it out by abstraction and application. A simple example is that the free variable y is the same as (λx.x y) ; or, again (λx.f x) is the same as (λg.λx.(g x ) f).
We can do this with our length of list function
length = df. (λf.(If (list is empty) then 0 else succ(f(tail(list)))) length)
Notice the lambda abstraction itself no longer contains the name 'length'. The general form of this is
length = (λf.(....) length)
and this is not entirely unfamiliar. In mathematics a point which satisfies a function like x = f[x] is known as a fixpoint or fixed-point. For example, the function x*x has a fixpoint of 1 because 1*1 is 1. A fixpoint of a function f is a point which remains unchanged as the result of the application of f to it, so x=f[x]=f[f[x]]=f[f[f[x]]]= ... If you square 1 you get 1, and if you square that (ie the square of the square of 1) you also get 1, and so on.
In our little equation,
length = (λf.(....) length)
the function 'length', which we are after, is a fix point of the abstraction λf.(...).
Shortly we will show that there is an abstraction Y, known as the fixpoint combinator, which when applied to any lambda expression H, has the property that
(Y H) = (H (Y H))
Now, (Y H) is a solution to the fixpoint equation. We can see this by direct substitution. The fixpoint equation is
fixpoint = (H fixpoint)
and if (Y H) is substituted in we get (Y H) = (H (Y H)) which is exactly right i.e. fixpoint=(Y H) is a solution to the equation.
So, when Y applied to any lambda expression whatsoever, say H, it delivers as a result a fixpoint of H, so in the length example (Y λf.(...)) is a or the length function (without using the name length).
In our case, Y applied to λf.(...) will deliver the length function as its result.
The fixpoint combinator is not all that hard to construct and remember (though goodness only knows how someone thought of it in the first place). Start with the self application function
λx.(x x)
slip a function application into the scope of it
λx.(h (x x))
apply what you have to itself
(λx.(h (x x)) λx.(h (x x)))
then abstract over the function h that is in there
λh.(λx.(h (x x)) λx.(h (x x))) (* Y the fixpoint combinator *)
This has to satisfy, for any H
(Y H) = (H (Y H))
consider an arbitrary H
(Y H) is (λh.(λx.(h (x x)) λx.(h (x x))) H)
this reduces to
(λx.(H (x x)) λx.(H (x x))) (*keep this in mind as Y H *)
and one more reduction gives
(H (λx.(H (x x)) λx.(H (x x))))
and this is (H (Y H)) (or, more strictly (H (Y H)) reduces to that, for the (Y H) needs to be reduced once to get the H inside).
Try it as an exercise. [We don't have upper case 'H' as a well-formed lambda expression within the software-- we'll write it as 'upH'.]
a) (λh.(λx.(h (x x)) λx.(h (x x))) upH) ⇒(upH (λx.(upH (x x)) λx.(upH (x x)))) (* (Y H) reduces to (H (Y H)) *)
(If (list is empty)
then 0
else succ(length (tail list)))
We get the fixpoint by abstracting over the 'length', and appying the fixpoint combinator ie
(Y λlength.(If (list is empty)
then 0
else succ(length (tail list))))
Then this fixpoint is the length function, and we can translate this piece by piece--to get a truly horrendous expression which might be something like... (I'll make each step of the translation mnemonically first, so you can see what is happening, then abbreviate the mnemonics to keep the whole thing short). And maybe splitting over lines will make things clearer.
The first schematic of the expression is
(Y
λlength.
(If
(list is empty)
then 0
else succ(length (tail list))))
we'll insert the combinator for IF-THEN-ELSE to get the second schematic
(Y
λlength.
(((λcondition.λthen.λelse.((condition then) else)
condition)
then)
else)
)
The 'condition' is whether the list is empty, so we will insert that
(Y
λlength.
(((λcondition.λthen.λelse.((condition then) else)
λx.T)
then)
else)
)
The 'then' is the numeral 0, so we will insert that
(Y
λlength.
(((λcondition.λthen.λelse.((condition then) else)
λx.T)
λx.T)
else)
)
The 'else' is the 'succ(length (tail list))' so let us build that up '(tail list) ' is '(list λx.λy.y)' and 'length (tail list)' is '(length (list λx.λy.y))' and the successor of that is '(λt.λa.((a 0) t) (length (list λx.λy.y)))' so inserting that gives
(Y
λlength.
(((λcondition.λthen.λelse.((condition then) else)
λx.T)
λx.T)
(λt.λa.((a 0) t) (length (list λx.λy.y))))
)
and that should be it. However, we do have the fixpoint combinator in there, and definitions for true. If we take those out we get
(λh.(λx.(h (x x)) λx.(h (x x)))
λlength.
(((λcondition.λthen.λelse.((condition then) else)
λx.λx.λy.x)
λx.λx.λy.x)
(λt.λa.((a 0) t) (length (list λx.λy.y))))
)
This is a function with the free variable 'list'. It is supposed to be applied to lists so we need to abstract over the list variable, thus
λlist.
(λh.(λx.(h (x x)) λx.(h (x x)))
λlength.
(((λcondition.λthen.λelse.((condition then) else)
λx.λx.λy.x)
λx.λx.λy.x)
(λt.λa.((a 0) t) (length (list λx.λy.y))))
)
And putting that on one line gives
λlist.(λh.(λx.(h (x x)) λx.(h (x x))) λlength.(((λcondition.λthen.λelse.((condition then) else) λx.λx.λy.x) λx.λx.λy.x) (λt.λa.((a 0) t) (length (list λx.λy.y)))))
and this function will return the length of a list (you can believe me).
So, for example, were you to apply it to λa.((a b) λa.((a c) λa.((a d) λx.T)) , which is the list {b,c,d} it will return λa.((a λx.T) λa.((a λx.T) λa.((a λx.T) λx.T))) which is the numeral 3.
Just to run over the theory of the fixpoint combinator...
The fix point combinator has the property
(Y H) =>(H (Y H))
and this is important because every recursive definition can be brought into the form of a fixed-point equation
f = H [f]
where f does not occur free in H, and (Y H) is a solution to this (as we can see by direct substitution)
The Y combinator is a universal fixed point finder and works on any lambda expression.
A qualification is that the application of Y may not work practically in that Y H may not have a terminating reduction; for example,the fix point equation
x = 3x -10
has a solution x = 5, but if we lambdify it to
x = (λy.(3y-10) x) (*here I am using extended lambda notation with * and - *)
then apply the fix point combinator (Y (λy.(3y-10) x)) which reduces to (λy.(3y-10) (Y λy.(3y-10))) which reduces to 3(Y λy.(3y-10))- 10 and so on forever.
The fixpoint combinator Y in conjunction with a lambda expression H, rewrites to (Y H) => (H (Y H)) and hence to (H..(H .. (H (Y H)))), converting recursion to iteration.
What actually has to happen when reducing is that the lambda expression itself has to ensure that the iteration stops eg with fac 5 there will be 5 iterations and then it will stop. Of course, this will not always be the case. Roughly, the lambda expression has to have in it a suitable if-then-else that stops the whole show.