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

t₁ bintree   t₂ bintree
―――――――――――――――――――――――   n integer
    n(t₁,t₂) bintree

If the judgement(s) above the line are derivable, and the condition(s) 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 children’s 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 (first try): By induction on the height of the derivation of t bintree.

Base case (height=1): The only derivations of height 1 are derivations of trees n where n is an integer:
```
―――――――――
n bintree
```
This tree has one leaf and zero internal nodes.
Inductive step (height=h>1): Assume that any tree with a derivation of height less than h has one more leaf than it does internal nodes. A tree with a derivation of height h>1 must have the form
```
     ⋮             ⋮
――――――――――   ――――――――――
t₁ bintree   t₂ bintree
―――――――――――――――――――――――
   n(t₁,t₂) bintree
```
where t₁ and t₂ have derivations of height at most h-1. So by the induction hypothesis, t₁ has one more leaf than it does internal nodes, and t₂ likewise has one more leaf than it does internal nodes. 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.

Let’s try the proof again using structural induction, which instead of using a counter (h), uses the structure of the derivation itself.

Proof (second try): By induction on the structure of the derivation of t bintree.

Case: The derivation is of the form
```
―――――――――
n bintree
```

The tree n has one leaf and zero internal nodes.

Case: The derivation is of the form

     ⋮             ⋮
――――――――――   ――――――――――
t₁ bintree   t₂ bintree
―――――――――――――――――――――――
   n(t₁,t₂) bintree

By the induction hypothesis, t₁ has one more leaf than it does internal nodes, and similarly for t₂. 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.