Applying the optimism strategy to unification for trees, we get exactly the effect we want in the rigid-rigid case.

The trouble is, how do we compute the bounded mgu in the flex-rigid case. In general, we have no choice but to apply the accumulated substitution and keep going. Applying a substitution blows up the terms, so we lose structural recursion.

This is where more conventional treatments in simply typed settings impose an external well-founded ordering respected by the recursion, something about decreasing the variable count. However, in our dependently typed world, we've got a better handle on the number of variables. It's built into the types. Let's exploit that...

Next: idempotent substitutions | Prev: the optimist's proof | Up: contents