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

**Alan Dix**

alan@hcibook.com

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.

http://www.hcibook.com/alan/papers/fixpts-BCTCS91/ |
Alan
Dix 8/1/2002 |