If we have an ordering on arrows, we can form upper-bound properties. Maximising the conjunction of a property P with an upper bound b finds the largest P-arrow smaller than b: a relativised notion of optimisation.

Of course, if the ordering has a top element (and any composition ordering does) then absolute optimisation is just bounded optimisation relative to top.

So, moving from Max to BMax introduces the extra parameter, b. What does this buy us? Well, b is going to be our accumulator. We accumulate the solution in b whilst decomposing P: once P has become trivial, we hope b will turn out to be the right answer.

For what kinds of P does this work?

Next: downward closure | Prev: the Unifier property | Up: contents