Next: conclusions | Prev: bounded mgu | Up: contents

Green knockout-extension is just red (constructor) knockout-extension lifted to handle failure.

The flex-rigid case just calls the occur check, which either signals failure or manufactures the compressed term ready for knockout. It's correct provided t is not a leaf, which you can check from bmgu is always the case; applying checkElim, there are two possibilities:

• t is put (leaf i) p
any unifying f forces p to be here, which is impossible if t is not a leaf
• t is (thin i) |> t'
so the knockout certainly unifies t with leaf i.

Moreover, suppose f also unifies them: it's not hard to show that, for all variables v

f v = f |> (thin i) |> (ko t' i) |> v

(note (ko t' i) is extensionally equal to (iota[t'/i])>>)

How? koElim, of course! Cases:

• v is i
ko gives us t'; but we know (thin i) |> t' is just t;
by assumption f |> t is f i
• v is (thin i j)
ko gives us (leaf j) which is then thinned back to (leaf (thin i j)),
yielding f (thin i j) as required

The flex-flex case just uses thick to compare and compress j. Unsurprisingly, the correctness proof proceeds by thickElim, yielding trivial maximality for the identity, or the same proof as above in the case of variable coalescence.

Next: conclusions | Prev: bounded mgu | Up: contents

Conor's Work Page