Ex 9.9 in Paul Hudak's book

Olaf Chitil olaf@cs.york.ac.uk
Wed, 03 Apr 2002 12:40:04 +0100

Tom Bevan wrote:
> What I would like to know is how the 'fix' function could be used
> to find the fixed point of a function like ( \n -> 2*n ).
> If it isn't possible, can someone explain the crucial difference between
> n! and (\n -> 2*n ) which allows n factorial to be found via the fix point
> method and not zero.

The 'fix' function does not yield *the* fix point of its argument. A
function can have many fix points, for example the identity function
'id' has infinitely many fix points. Other functions such as (\n -> n+1)
do not seem to have any fix point.

I say "seem not to have any", because it depends which domain you
regard. (\n -> n+1) does not have any fix point in the real numbers.
However, '+ infinity' is a fix point of it. So (\n -> n+1) has a fix
point in the real numbers plus '+ infinity'.

In functional languages every type has one element that is often not
mentioned: _|_ (bottom). For example 'Bool' has the three elements
True,False and _|_. 

_|_ represents undefinedness, in particular non-termination. The value
of 'undefined' and 'error "something"' are _|_. _|_ might look like a
slightly strange value, but it is very useful for understanding the
semantics of functional languages. Because of _|_, all functions defined
by a functional program are total functions; talking about partial
functions is often rather awkward. With _|_ the semantics of non-strict
functional languages is easy to describe. _|_ helps understanding
infinite data structures (see Chapter 9 of Bird's Introduction to
Functional Programming using Haskell). And finally _|_ assures that
every function defined by a functional program has at least one fix
point (this property is not trivial to prove).

Evaluation of 'fix (\n -> 2*n)' aborts with a stack overflow. This is
not because the stack is too small, but because the value is _|_. _|_ =
2 * _|_.

The 'fix' function yields the *least* fix point of its argument. *Least*
with respect to a certain partial order on the elements of a type. In
this order _|_ is the least element. Also for example (_|_,2) < (3,2).

> factGen = \f -> \n -> if n==0 then 1 else n * f (n-1)
Note that factGen _|_ = \n -> if n == 0 then 1 else _|_. That is, _|_ is
not a fix point of factGen. \n->n! is really the least (and only) fix
point of factGen.

To learn more about this, denotational semantics, cpos and basic domain
theory are good key words.


 Dept. of Computer Science, The University of York, York YO10 5DD, UK. 
 URL: http://www.cs.york.ac.uk/~olaf/
 Tel: +44 1904 434756; Fax: +44 1904 432767