Next: the tree syntax | Prev: thickening a finite set | Up: contents

By the way, the code for thick:

• thick (fz n) (fz n) = none
thick (fz n) (fs j) = some j
thick (fs i) (fz sn) = some (fz n)
thick (fs i) (fs j) = !fs (thick i j)
• !fs none = none
!fs (some j) = some (fs j)

!fs is just the obvious lifting of fs. It would have been `green fs' if it had made it onto the slide.

thick w is a partial inverse for thin w. It's good to think of (thin w j) as a `pattern' which matches the non-w elements of fin sn. Thickening codes up the corresponding case analysis.

I manifest the relationship between thick and thin by proving the thickElim elimination rule (by an easy structural induction). Later, we'll see just how useful this rule is for reasoning about programs involving thick. We can split thick applications into two cases:

• we thickened w and got none
• we thickened a (thin w j) and got (some j)

I got used to working with elimination rules when implementing pattern matching. They're very good for coding up the leverage a piece of information exerts on an arbitrary goal. We often think of specifications as inward-looking, telling us what program to write, but they should also be outward-looking, telling us how to reason about the program as a component of a larger one. Elimination rules do the latter job very well. I've been living in type theory so long, I'll never be content with a first-order specification logic again.

Next: the tree syntax | Prev: thickening a finite set | Up: contents

Conor's Work Page