[<<][staapl][>>][..]Mon Sep 17 18:55:07 CEST 2007
a fixed point p of the expression F satisfies F(p) = p. the Y
combinator expresses p in terms of F as p = Y F. combining the two we
F (Y F) = (Y F)
simply expanding this gives exactly what we want:
Y F = F (Y F) = F (F (Y F)) = F (F (F (...)))
where the dots represent an infinite sequence of self applications.
that's all folks. in order to implement useful recursion, simply write
the 'body' F, and Y will take care of the rest.
let's make this a bit more intuitive. suppose we want to create a
function f which is defined recursively in terms of f. look at F as a
function which produces such a function f,
F : x -> f
the recursion is a consequence of the infinite chain of applications
f = Y F
= F (F (F ...))
= F f
so what are the properties of F? first it needs to map f -> f. and
second if a finite recursion is desired, it needs to do this in a way
that it creates a 'bigger' f from a 'smaller' one, eventually starting
from the 'smallest' f which does not depend on f: this leads to a
finite reduction when normal order reduction is used.
let's solve this problem in scheme, for Y F = factorial. so we know
factorial = F (F (F (...)))
factorial = F factorial
in words, F is a function that returns a factorial function if it is
applied to a factorial function. so the factorial function is a fixed
point of F. the Y combinator finds this fixed point as
factorial = Y F.
the rest is fairly straightforward: a nested lambda expression which
uses the provided 'factorial' function to compute one factorial
(if (zero? x)
(* x (factorial (- x 1))))))
the thing which always tricked me is 'fixed point', because i was
thinking about iterated functions on the reals used in many iterative
numerical algorithms like the newton method. in the lambda calculus,
there are only functions and applications, so a fixed point IS the
infinite nested application, since that fixed point value doesn't have
another representation, while a fixed point of a function on the reals
is just a point in the reals.