Alan Dix
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
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:
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.
thttp://alandix.com/academic/papers/fixpts-YCS107-88/ | Alan Dix 8/1/2002 |