Notes on PL 02 - Inductive Definitions and Proofs
In this note, we will use the semantics of our simple language of arithmetic expressions,
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
To fix this problem, we can restrict our attention to well-formed configurations
- 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
The set
- 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
Structural Induction
Given an inductively defined set 𝐴, to prove that a property 𝑃 holds for all elements of 𝐴, we need to show:
- Base cases: For each axiom
- Inductive cases: For each inference rule
if
Note that if the set
Example: Progress
Let’s consider the progress property defined above, and repeated here:
Progress: For each expression
Proof. Let
by structural induction on
CASE
CASE
CASE
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
- Subcase
and : By assumption and the definition of we have
Hence, by the induction hypothesis
CASE
CASE
We have
Subcase
: By rule we have where Subcase
Int: By assumption and the definition of fvs we have
Hence, by induction hypothesis we also have
.