Next: finite set family | Prev: opening credits | Up: contents

I hope you don't mind me presenting inductive definitions in natural deduction style. Sorry folks, when you've got exciting dependent datatypes, you just can't get away with

or similar. I quite like the natural deduction style anyway: it looks more like the constructors are made of wood, with holes for hypotheses and a lug for the conclusion. I want a set of wooden datatypes for Christmas. Of course, we couldn't make them out of plastic for fear of legal action...

Live, I construct the hypotheses of the elimination rule (induction) by stealing the structure of the introduction rules (counting), sliding the constructor patterns down so that each n : nat becomes Phi n.

Note that the horizontal dotted line is means the same thing as the conventional but annoying vertical line in natural deduction. The thing above the dotted line is a `hypothetical hypothesis'. Rod and I cooked up this notation one day, when he got fed up with me writing scary types on his blackboard.

Oh yeah, and here's the computational behaviour associated with natElim. It's like primitive recursion, but dependently typed and higher order.

Next: finite set family | Prev: opening credits | Up: contents

Conor's Work Page