===============================
REDUCERON MEMO 46 (IN PROGRESS)
Checking for a fixed-point
using needed narrowing
Matthew N, 8 December 2009
===============================

In Chapter 22 of "The Implementation of Functional Programming
Languages", Peyton Jones outlines a basic strictness analyser which
uses abstract interpretation.  In abstract interpretation, every
function f in a program is lifted to an abstract version f#

  f# x1 ... xn = e

where e is an expression whose type is the two-point domain {0,1};
0 denotes "does not terminate" and 1 denotes "may terminate".
Strictness of function f in parameter xi can be determined by
evaluating f# with 0 passed in for xi and 1 passed in for all other
parameters.

A problem arises when f is a recursive function

  f x1 ... xn = ... f ...

because then f# is also recursive.  If the compiler wishes to
determine the strictness of f, it may never terminate!

The solution is to pick a non-recursive function f#i from the set

  f#0 x1 ... xn = 0
  f#1 x1 ... xn = ... f#0 ...
  f#2 x1 ... xn = ... f#1 ...
  f#3 x1 ... xn = ... f#2 ...
  ...

where

  f#i x1 ... xn = f#i+1 x1 ... xn

for any x1 ... xn.  The function f#i is called the fixed-point of f#.
It can be computed in finite time since x1 ... xn have finite domains
and can be enumerated exhaustively.

Computable yes, but the fixed-point check is exponentially expensive in
the number of function arguments, and according to Hudak this is
necessarily the case.  On the bright side, Peyton Jones reports that
rapid convergence is typical, and that heuristics can be used to
handle common cases very efficiently.  Still, the check feels very
expensive.

I suspect there is a great deal to be gained by implementing the
abstract interpeter using the needed-narrowing evaluation strategy, as
opposed to lazy evaluation or eager evaluation.  That is, to determine
if f#i is a fixed point, simply evaluatate the expression

  f#i x1 ... xn  /=  f#i+1 x1 ... xn

by needed narrowing where x1 ... xn are unbound logical variables.  If
no solution is found, f#i is a fixed-point.  Needed narrowing should
be very effective at pruning the search space because the bodies of
f#i and f#i+1 are basically large compositions of conjunctions and
disjunctions over values in the abstract domain {0,1}.  As such, they
are likely to be lazy - often yielding results without demanding all
of the arguments.

To be continued...