Monotonic reasoning about non-monotonic functions - or, when finding fixed points you can do (almost) anything

Full reference:

A. J. Dix (1991).
Monotonic reasoning about non-monotonic functions - or, when finding fixed points you can do (almost) anything. (abstract only, part of Report of The Seventh British Colloquium on Theoretical Computer Science, March 26th-28th 1991).
Bulletin of the European Association for Theoretical Computer Science, 44: 289.

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

abstract

Static analysis, especially of functional programs, often results in semantic equations over finite domains. The most complicated part of their practical solution being the solution of recursive function equations, or equivalently finding of fixed points of defining functionals.

find  f :A B   st.  f = F f,     i.e. f = fix F   (N.B. fix is often written as the Y combinator)

Algorithms (e.g. frontiers algorithm) usually ensure that all intermediate functions are monotonic, and so the proofs of correctness (but not necessarily the implementation!) are straightforward. It may however be advantageous to use algorithms (such as pending analysis) where intermediate functions are not monotonic. In this case, it will not usually be the case that (even where F is defined) that:

f g     F f F g

Without this proofs become almost impossible. Happily it turns out that the functionals F of interest satisfy a stronger property pseudo-monotonicity whereby the above holds when either of the functions f or g is monotonic, not necessarily both. Using this we can begin to reason about non-monotonic functions using "monotonic" arguments. Not only do proofs of existing algorithms become possible but one realises that one has enormous flexibility in calculating fixed points. You can do almost anything.