Ex 9.9 in Paul Hudak's book

[Tom Bevan]

Thanks Olaf, I'll follow up your references.

Tom

On Wed, 3 Apr 2002 21:40, Olaf Chitil wrote:
> 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 betw=
een
> > 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 define=
d
> 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 _|_. _|_ =3D
> 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 =3D \f -> \n -> if n=3D=3D0 then 1 else n * f (n-1)
>
> Note that factGen _|_ =3D \n -> if n =3D=3D 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