Alan Dix > 1988

Download full technical report (PDF, 730K)

see blog about this report "Sandwich proofs and odd orders"

Full reference:

A. J. Dix (1988).
Finding fixed points in non-trivial domains: proofs of pending analysis and related algorithms.
YCS 107, Dept. of Computer Science, University of York.
http://alandix.com/academic/papers/fixpts-YCS107-88/

Keywords functional programming, strictness analysis, fixed point operator, monotonic functions, Y combinator, finite domains, recursive functions, pending analysis

abstract

Young and Hudak (1987) developed an algorithm called Pending Analysis for deriving the fixed points of first order functions over binary domains. They prove a result in their paper which justifies the approach, but does not really prove its correctness. Further they suggest that the analysis may be extended to deeper domains. The structure of pending analysis means that many of the intermediate functions generated are not monotonic, which means that arguments of correctness based on partial orderings tend to fail without great care.

This paper attempts to fill some of the gaps in this work, it will:

1. Give proofs of correctness for the binary case when the defining functional is fully monotonic (i.e. monotonic even for non-monotonic function arguments). This is usually for non-self applicatory functions.
2. Develop a slight variant of the algorithm which makes better use of the monotonicity of the function, and which is correct for all functions.
3. Show how the binary analysis can be used to solve more complex domains if the primatives are sufficiently well behaved.
4. Parallel steps 1 and 2 for general domains using an iterative version of the algorithm. In particular proving several incremental fixed point theorems. We will also discus representation and algorithms for the partial functions used in this algorithm.
5. Show that pending analysis (and probably other algorithms too) can be extended to higher order functions by considering the term algebra.
6. Show that the concept of a fixed point can be extended to configurations (partial functions), and that this can be used to generate easy proofs of safeness for pending analysis and similar algorithms.
7. Use these ideas to generate a non-deterministic algorithm which is always correct, and which can be instantiated with different heuristics to yield optimised algorithms. This algorithm includes as special cases pending analysis (with and without memoing) and standard bottom up fixed point calculation.

The proof techniques, especially the exploitation of the pseudo-monotonicity of most computational functionals may be of interest to those generally interested in proving properties over lattices.

An addendum completes the picture by proving pending analysis and the extended non-deterministic algorithm correct in the general case and for all finite domains. This uses 'sandwich proofs', a proof technique that involves finding montonic upper and lower bounds for non-monotonic functions.

• J. Young and P. Hudak (1986). Finding fixpoints on function spaces. YALEU/DCS/RR-505, Yale University, Department of Computer Science. http://www.cs.yale.edu/publications/techreports/tr505.pdf