Notes on PL 02: Inductive Definitions and Proofs

In this note, we will use the semantics of our simple language of arithmetic expressions,

to express useful program properties, and we will prove these properties by induction.

Program Properties

There are a number of interesting questions about a language one can ask: Is it deterministic? Are there non-terminating programs? What sorts of errors can arise during evaluation? Having a formal semantics allows us to express these properties precisely.

• Determinism: Evaluation is deterministic,

• Termination: Evaluation of every expression terminates,

It is tempting to want the following soundness property,

• Soundness: Evaluation of every expression yields an integer,

but unfortunately it does not hold in our language! For example, consider the totally-undefined function and the expression . The configuration is stuck—it has no possible transitions–but is not an integer. The problem is that has free variables but does not contain mappings for those variables.

To fix this problem, we can restrict our attention to well-formed configurations , where is defined on (at least) the free variables in . This makes sense as evaluation typically starts with a closed expression. We can define the set of free variables of an expression as follows:

Now we can formulate two properties that imply a variant of the soundness property above:

• Progress: For each expression and store such that the free variables of are contained in the domain of , either is an integer or there exists a possible transition for ,

• Preservation: Evaluation preserves containment of free variables in the domain of the store,

The rest of this lecture shows how can we prove such properties using induction.

Inductive Sets

Induction is an important concept in programming language theory. An inductively-defined set 𝐴 is one that is described using a finite collection of axioms and inductive (inference) rules. Axioms of the form

indicate that is in the set . Inductive rules

indicate that if are all elements of , then is also an element of .

The set is the set of all elements that can be inferred to belong to using a (finite) number of applications of these rules, starting only from axioms. In other words, for each element of , we must be able to construct a finite proof tree whose final conclusion is .

• Example 1. The set described by a grammar is an inductive set. For instance, the set of arithmetic expressions can be described with two axioms and three inference rules:

These axioms and rules describe the same set of expressions as the grammar:

• Example 2. The natural numbers (expressed here in unary notation) can be inductively defined:

• Example 3. The small-step evaluation relation is an inductively defined set.

• Example 4. The multi-step evaluation relation can be inductively defined:

• Example 5. The set of free variables of an expression 𝑒 can be inductively defined:

Inductive Proofs

We can prove facts about elements of an inductive set using an inductive reasoning that follows the structure of the set definition.

Mathematical Induction

You have probably seen proofs by induction over the natural numbers, called mathematical induction. In such proofs, we typically want to prove that some property holds for all natural numbers, that is, A proof by induction works by first proving that holds, and then proving for all , if , then . The principle of mathematical induction can be stated succinctly as

The proposition is the basis of the induction (also called the base case) while is called induction step (or the inductive case). While proving the induction step, the assumption that holds is called the induction hypothesis.

Structural Induction

Given an inductively defined set 𝐴, to prove that a property 𝑃 holds for all elements of 𝐴, we need to show:

1. Base cases: For each axiom

holds.

2. Inductive cases: For each inference rule

if and and then .

Note that if the set is the set of natural numbers from Example 2 above, then the requirements for proving that holds for all elements of is equivalent to mathematical induction. If describes a syntactic set, then we refer to induction following the requirements above as structural induction. If is an operational semantics relation (such as the small-step operational semantics relation ) then such an induction is called induction on derivations. We will see examples of structural induction and induction on derivations throughout the notes

Example: Progress

Let’s consider the progress property defined above, and repeated here:

Progress: For each expression and store such that the free variables of are contained in the domain of , either is an integer or there exists a possible transition for ,

Let’s rephrase this property in terms of an explicit predicate on expressions:

This technique is called “structural induction on .” We analyze each case in the grammar and show that holds for that case. Since the grammar productions and and are inductive, they are inductive steps in the proof; the cases for and are base cases. The proof proceeds as follows.

Proof. Let be an expression. We will prove that

by structural induction on . We analyze several cases, one for each case in the grammar for expressions:

CASE : Let be an arbitrary store, and assume that . By the definition of fvs we have . By assumption we have and so . Let . By the axiom we have , which finishes the case.

CASE : We immediately have Int, which finishes the case.

CASE : Let be an arbitrary store, and assume that . We will assume that and hold and show that holds. Let’s expand these properties. We have

and want to prove:

We analyze several subcases.

• Subcase and : By rule , we immediately have , where

• Subcase : By assumption and the definition of we have

​ Hence, by the induction hypothesis we also have for some and By rule we have

• Subcase and : By assumption and the definition of we have

​ Hence, by the induction hypothesis we also have for some and

. By rule we have , which finishes the case.

CASE : Analogous to the previous case.

CASE : Let be an arbitrary store, and assume that As above, we assume that and hold and show that holds. Let’s expand these properties

We have

and want to prove:

We analyze several subcases.

• Subcase : By rule we have where

• Subcase Int: By assumption and the definition of fvs we have

​ Hence, by induction hypothesis we also have for some and By the rule we have , which finishes the case and the inductive proof. .