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.
Olaf
--
OLAF CHITIL,
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