The semantics of a simple functional language
[examples inductive definitions The simplest way to precisely specify the meanings of programming language expressions is through an operational semantics. Such a definition consists of a set of what look like the inference rules of a logic, stating the conditions under which a given expression can be reduced to a value, or at least evaluated one step more. Formally, this sort of specification is an inductive definition, equipped with an induction principle for proving that a property holds for all executions. Such proofs are conceptually trivial—they involve checking that the property holds initially and that it is preserved by each execution step—but are extremely tedious to write out by hand. Fortunately, they are often trivial with the help of a little automation. Let’s prove a Church–Rosser property: that expression evaluation always leads to a unique final result.
A simple functional language
Our language is insufficient to write an airline reservation system—it isn’t even Turing-complete—but it is sufficient to illustrate some of the core themes of operational semantics.
Let’s begin with the syntax. An expression can be a Boolean (true or false), or a natural number given by zero or successor, or a conditional expression, or an equality test:
datatype exp = T | F | Zero | Succ exp | IF exp exp exp | EQ exp exp
Next we define the operational semantics itself, which takes the form
of a reduction relation (⇛). We use an Isabelle/HOL inductive definition.
The first two rules cover the true and false cases of a conditional expression,
while the third case takes care of a single reduction within the condition.
The fourth rule covers the evaluation of the argument of Succ.
So this is a small-step semantics;
in a big-step semantics, every rule would be formulated
to deliver the final result.
inductive Eval :: "exp ⇒ exp ⇒ bool" (infix "⇛" 50) where IF_T: "IF T x y ⇛ x" | IF_F: "IF F x y ⇛ y" | IF_Eval: "p ⇛ q ⟹ IF p x y ⇛ IF q x y" | Succ_Eval: "x ⇛ y ⟹ Succ x ⇛ Succ y" | EQ_same: "EQ x x ⇛ T" | EQ_S0: "EQ (Succ x) Zero ⇛ F" | EQ_0S: "EQ Zero (Succ y) ⇛ F" | EQ_SS: "EQ (Succ x) (Succ y) ⇛ EQ x y" | EQ_Eval1: "x ⇛ z ⟹ EQ x y ⇛ EQ z y" | EQ_Eval2: "y ⇛ z ⟹ EQ x y ⇛ EQ x z"
The remaining six rules concern the evaluation of equality tests. I specifically designed them to be messy.
Rule inversion
The language admits nonsensical terms such as Succ T, which cannot be reduced to anything.
How do we know that? Intuitively, it’s because there is only one rule for evaluatingSucc;
that rule evaluates the argument, and there is no rule for evaluating T.
This straightforward reasoning can fortunately be automated.
The following declarations inform Isabelle’s simplifier about the possibilities of
various reductions occurring. In particular, the first three
generate theorems stating that the quoted reductions are impossible.
In other cases, the resulting theorems state conditions under which the reduction can take place,
e.g.
(Succ ?x ⇛ ?z) = (∃y. ?z = Succ y ∧ ?x ⇛ y)
inductive_simps T_simp [simp]: "T ⇛ z" inductive_simps F_simp [simp]: "F ⇛ z" inductive_simps Zero_simp [simp]: "Zero ⇛ z" inductive_simps Succ_simp [simp]: "Succ x ⇛ z" inductive_simps IF_simp [simp]: "IF p x y ⇛ z" inductive_simps EQ_simp [simp]: "EQ x y ⇛ z"
Such declarations are useful in any inductive definition where the conclusions of the rules allow most of the cases to be excluded on syntactic grounds. If your proofs seem to require a lot of explicit case analysis, see whether this sort of declaration could help you.
Types and type preservation
Our language has Booleans and natural numbers, so let’s define the corresponding type system. (It will be simpler than Martin-Löf type theory.)
datatype tp = bool | num
The great thing about operational semantics is its flexibility. Above, we defined the evaluation of expressions, which is their dynamic behaviour; now we can define their typing relation, which is static behaviour. The same techniques work for both.
True and false have the Boolean type, while zero is a number.
Succ yields a number if its argument does.
For conditional expressions and equality, the use of types has to be consistent.
inductive TP :: "exp ⇒ tp ⇒ bool" where T: "TP T bool" | F: "TP F bool" | Zero: "TP Zero num" | IF: "⟦TP p bool; TP x t; TP y t⟧ ⟹ TP (IF p x y) t" | Succ: "TP x num ⟹ TP (Succ x) num" | EQ: "⟦TP x t; TP y t⟧ ⟹ TP (EQ x y) bool"
Rule inversion for the above lets us reason easility about the type-checking possibilities for expressions.
inductive_simps TP_IF [simp]: "TP (IF p x y) t" inductive_simps TP_Succ [simp]: "TP (Succ x) t" inductive_simps TP_EQ [simp]: "TP (EQ x y) t"
Type preservation
claims that the evaluation of an expression does not change its type.
Formally, we state that if x ⇛ y and x has some type T, then y will have the same type.
Induction on the assumption x ⇛ y produces 10 gruesome-looking subgoals:
1. ⋀x y t. TP (IF T x y) t ⟹ TP x t
2. ⋀x y t. TP (IF F x y) t ⟹ TP y t
3. ⋀p q x y t. ⟦p ⇛ q; ⋀t. TP p t ⟹ TP q t; TP (IF p x y) t⟧ ⟹ TP (IF q x y) t
4. ⋀x y t. ⟦x ⇛ y; ⋀t. TP x t ⟹ TP y t; TP (Succ x) t⟧ ⟹ TP (Succ y) t
5. ⋀x t. TP (EQ x x) t ⟹ TP T t
6. ⋀x t. TP (EQ (Succ x) Zero) t ⟹ TP F t
7. ⋀y t. TP (EQ Zero (Succ y)) t ⟹ TP F t
8. ⋀x y t. TP (EQ (Succ x) (Succ y)) t ⟹ TP (EQ x y) t
9. ⋀x z y t. ⟦x ⇛ z; ⋀t. TP x t ⟹ TP z t; TP (EQ x y) t⟧ ⟹ TP (EQ z y) t
10. ⋀y z x t. ⟦y ⇛ z; ⋀t. TP y t ⟹ TP z t; TP (EQ x y) t⟧ ⟹ TP (EQ x z) t
Some courses in operational semantics expect students to be able to carry out such proofs by hand. But even writing out the subgoals perfectly by hand is next to impossible. Fortunately they are trivial to prove, with the help of rule inversion. The Isabelle/HOL proof takes a single line, which executes instantly:
proposition type_preservation: assumes "x ⇛ y" "TP x t" shows "TP y t" using assms by (induction x y arbitrary: t rule: Eval.induct) (auto simp: TP.intros)
A couple of fine points in the proof:
- designating the variable
tas arbitrary allows for the type of subexpressions to differ from the type of the top expression - you can give two proof methods to the by command
Values and value preservation
We can interpret the operators of our simple language in terms of the natural numbers. In particular, true and false denote 1 and zero, respectively. We can also give the semantics of conditional expressions and equality tests. This is a trivial example of a denotational semantics.
fun evl :: "exp ⇒ nat" where "evl T = 1" | "evl F = 0" | "evl Zero = 0" | "evl (Succ x) = evl x + 1" | "evl (IF x y z) = (if evl x = 1 then evl y else evl z)" | "evl (EQ x y) = (if evl x = evl y then 1 else 0)"
Value preservation is the claim that the evaluation of an expression does not change its value.
proposition value_preservation: assumes "x ⇛ y" shows "evl x = evl y" using assms by (induction x y; force)
Here we relate types and values. The value of a Boolean expression is less than 2.
lemma assumes "TP x t" "t = bool" shows "evl x < 2" using assms by (induction x t; force)
Proving a Church–Rosser property
The Church–Rosser theorem concerns the λ-calculus and in effect states that multiple
evaluation routes cannot yield multiple final values. It’s necessary because
in the λ-calculus it’s possible to reduce some expressions in more than one way.
Our language has the same problem. For example, four different rules are applicable
to some expressions of the form EQ (Succ x) (Succ y).
Some care is needed when expressing a Church–Rosser property. The following does not hold:
lemma assumes "x ⇛ y" "x ⇛ z" shows "∃u. y ⇛ u ∧ z ⇛ u" nitpick
The counterexample returned by nitpick is IF F F F.
The property fails simply because F cannot reduce, which is not really what we are worried about here.
To express Church–Rosser properly, we need the transitive closure of the reduction relation.
(We could also have used the built-in transitive closure operator.)
inductive EvalStar :: "exp ⇒ exp ⇒ bool" (infix "⇛*" 50) where Id: "x ⇛* x" | Step: "x ⇛ y ⟹ y ⇛* z ⟹ x ⇛* z"
The following lemma is just a warmup. We show that the type is preserved even over a string of evaluation steps.
proposition type_preservation_Star: assumes "x ⇛* y" "TP x t" shows "TP y t" using assms by (induction x y) (auto simp: type_preservation)
On the other hand, the following four lemmas are essential. Each of them transforms a string of evaluation steps into the analogous string of steps within an argument of some function. All these proofs are trivial inductions.
lemma Succ_EvalStar: assumes "x ⇛* y" shows "Succ x ⇛* Succ y" using assms by induction (auto intro: Succ_Eval EvalStar.intros)
lemma IF_EvalStar: assumes "p ⇛* q" shows "IF p x y ⇛* IF q x y" using assms by induction (auto intro: IF_Eval EvalStar.intros)
lemma EQ_EvalStar1: assumes "x ⇛* z" shows "EQ x y ⇛* EQ z y" using assms by induction (auto intro: EQ_Eval1 EvalStar.intros)
lemma EQ_EvalStar2: assumes "y ⇛* z" shows "EQ x y ⇛* EQ x z " using assms by induction (auto intro: EQ_Eval2 EvalStar.intros)
Finally we reach our destination. The diamond property is not the full
Church–Rosser claim, but it captures the main point:
that if some x can be reduced either to y or z in a single step,
then the evaluation strings can be extended to reunite at some common u.
proposition diamond: assumes "x ⇛ y" "x ⇛ z" shows "∃u. y ⇛* u ∧ z ⇛* u" using assms proof (induction x y arbitrary: z) case (IF_Eval p q x y) then show ?case by simp; meson F_simp IF_EvalStar T_simp) next case (EQ_SS x y) then show ?case by (simp; meson Eval.intros EvalStar.intros) next case (EQ_Eval1 x u y) then show ?case by (auto; meson EQ_EvalStar1 Eval.intros EvalStar.intros)+ next case (EQ_Eval2 y u x) then show ?case by (auto; meson EQ_EvalStar2 Eval.intros EvalStar.intros)+ qed (force intro: Succ_EvalStar Eval.intros EvalStar.intros)+
Finally, a nontrivial proof! I’ve tried to make it neat, but it’s a mess. You could download the Isabelle theory file and see if you can do it better.
Postscript
There is a myth that you need dependent types to do semantics. This is ridiculous; the heyday of denotational semantics was the 1970s, before most people had even heard of dependent types. Tobias Nipkow and Gerwin Klein have written an entire book, Concrete Semantics, on how to do semantics in Isabelle/HOL. It has many advanced examples. You can either buy a copy or download it for free.
This is another example from my old MPhil course, Interactive Formal Verification.