Inductive definitions and proofs

Reading: TAPL 3.2-3.

The book uses the syntax of NB as an opportunity to introduce several different ways of writing an inductive definition. We only ever use context-free grammars (Backus-Naur form) to define syntax, but the other ways are used for other purposes. Of these, the one that needs most explanation is probably inference rules (Definition 3.2.2). These originated in logic as a way of writing proofs; we use them to define things like how to evaluate a program, or the type system of a language.

Here’s another (non-PL) example of an inductive definition using inference rules. We define binary trees with integer labels by defining a judgement of the form t bintree (read: “t is a binary tree”), using the following inference rules:

―――――――――   n integer 
n bintree

t1 bintree   t2 bintree
―――――――――――――――――――――――   n integer
    n(t1,t2) bintree

If the judgements above the line are derivable, and the conditions on the side hold, then the judgement below the line is derivable.

For example, the derivation of tree 12(34,56) is:

――――――――――   ――――――――――
34 bintree   56 bintree
―――――――――――――――――――――――
   12(34,56) bintree

We sometimes deviate from the book’s notation for inference rules in a couple of ways.

• When there are no premises, we sometimes still draw the line. There’s absolutely no difference in meaning; drawing the line over the conclusion just emphasizes that it’s a conclusion, not a premise.

• We distinguish between premises (above the line) and side conditions (written on the side), whereas the book writes them all above the line. Premises must be judgements and, in a derivation, need to be derived. Side conditions are conditions, written in ordinary math or English, on the metavariables in the inference rule. Because a derivation doesn’t have metavariables anymore, it doesn’t have side conditions anymore, either.

Exercise: A heap is a binary tree in which every parent node’s value is greater than or equal to its childrens’ values. Write this definition using inference rules.

One reason we use this notation is that it provides a structure for writing inductive proofs.

Returning to the bintree example (not heaps), we might want to prove that a binary tree has one more leaf than it does internal nodes.

Show: If t is a binary tree, then the number of leaves in t is one greater than the number of internal nodes in t.

Proof: By induction on the structure of the derivation of t bintree.

• Case: t = n. This tree has one leaf and zero internal nodes.

• Case: t = n(t1, t2). By the induction hypothesis, t1 has one more leaf than it does internal nodes, and similarly for t2. Together, they have two more leaves than internal nodes, but n is also an internal node, so t has one more leaf than it does internal nodes.

Exercise: Prove that the root of a heap has the maximum value of all of its nodes’ values.