pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Start of splitting evaluation contexts out of LambdaCalculusAndTypeSoundness

Browse source
This commit is contained in:
Adam Chlipala 2021-03-27 17:03:26 -04:00
parent 26c272f53f
commit 5cdd4d1322
4 changed files with 480 additions and 193 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

219
EvaluationContexts.v Normal file
View file

@ -0,0 +1,219 @@
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
* Chapter 12: More on Evaluation Contexts
* Author: Adam Chlipala
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
Require Import Frap.
Module Stlc.
Inductive exp : Set :=
| Var (x : var)
| Const (n : nat)
| Plus (e1 e2 : exp)
| Abs (x : var) (e1 : exp)
| App (e1 e2 : exp).
Inductive value : exp -> Prop :=
| VConst : forall n, value (Const n)
| VAbs : forall x e1, value (Abs x e1).
Fixpoint subst (e1 : exp) (x : string) (e2 : exp) : exp :=
match e2 with
| Var y => if y ==v x then e1 else Var y
| Const n => Const n
| Plus e2' e2'' => Plus (subst e1 x e2') (subst e1 x e2'')
| Abs y e2' => Abs y (if y ==v x then e2' else subst e1 x e2')
| App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'')
end.
Inductive context : Set :=
| Hole : context
| Plus1 : context -> exp -> context
| Plus2 : exp -> context -> context
| App1 : context -> exp -> context
| App2 : exp -> context -> context.
Inductive plug : context -> exp -> exp -> Prop :=
| PlugHole : forall e, plug Hole e e
| PlugPlus1 : forall e e' C e2,
plug C e e'
-> plug (Plus1 C e2) e (Plus e' e2)
| PlugPlus2 : forall e e' v1 C,
value v1
-> plug C e e'
-> plug (Plus2 v1 C) e (Plus v1 e')
| PlugApp1 : forall e e' C e2,
plug C e e'
-> plug (App1 C e2) e (App e' e2)
| PlugApp2 : forall e e' v1 C,
value v1
-> plug C e e'
-> plug (App2 v1 C) e (App v1 e').
(* Small-step, call-by-value evaluation, using our evaluation contexts *)
(* First: the primitive reductions *)
Inductive step0 : exp -> exp -> Prop :=
| Beta : forall x e v,
value v
-> step0 (App (Abs x e) v) (subst v x e)
| Add : forall n1 n2,
step0 (Plus (Const n1) (Const n2)) (Const (n1 + n2)).
(* Then: running them in context *)
Inductive step : exp -> exp -> Prop :=
| StepRule : forall C e1 e2 e1' e2',
plug C e1 e1'
-> plug C e2 e2'
-> step0 e1 e2
-> step e1' e2'.
(* It's easy to wrap everything as a transition system. *)
Definition trsys_of (e : exp) := {|
Initial := {e};
Step := step
|}.
(* Typing details are the same as last chapter. *)
Inductive type :=
| Nat (* Numbers *)
| Fun (dom ran : type) (* Functions *).
Inductive hasty : fmap var type -> exp -> type -> Prop :=
| HtVar : forall G x t,
G $? x = Some t
-> hasty G (Var x) t
| HtConst : forall G n,
hasty G (Const n) Nat
| HtPlus : forall G e1 e2,
hasty G e1 Nat
-> hasty G e2 Nat
-> hasty G (Plus e1 e2) Nat
| HtAbs : forall G x e1 t1 t2,
hasty (G $+ (x, t1)) e1 t2
-> hasty G (Abs x e1) (Fun t1 t2)
| HtApp : forall G e1 e2 t1 t2,
hasty G e1 (Fun t1 t2)
-> hasty G e2 t1
-> hasty G (App e1 e2) t2.
Local Hint Constructors value plug step0 step hasty : core.
Infix "-->" := Fun (at level 60, right associativity).
Coercion Const : nat >-> exp.
Infix "^+^" := Plus (at level 50).
Coercion Var : var >-> exp.
Notation "\ x , e" := (Abs x e) (at level 51).
Infix "@" := App (at level 49, left associativity).
(** * Now we adapt the automated proof of type soundness. *)
Ltac t0 := match goal with
| [ H : ex _ |- _ ] => invert H
| [ H : _ /\ _ |- _ ] => invert H
| [ |- context[?x ==v ?y] ] => cases (x ==v y)
| [ H : Some _ = Some _ |- _ ] => invert H
| [ H : step _ _ |- _ ] => invert H
| [ H : step0 _ _ |- _ ] => invert1 H
| [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
| [ H : hasty _ _ _ |- _ ] => invert1 H
| [ H : plug _ _ _ |- _ ] => invert1 H
end; subst.
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
Lemma progress : forall e t,
hasty $0 e t
-> value e
\/ (exists e' : exp, step e e').
Proof.
induct 1; t.
Qed.
Lemma weakening_override : forall (G G' : fmap var type) x t,
(forall x' t', G $? x' = Some t' -> G' $? x' = Some t')
-> (forall x' t', G $+ (x, t) $? x' = Some t'
-> G' $+ (x, t) $? x' = Some t').
Proof.
simplify.
cases (x ==v x'); simplify; eauto.
Qed.
Local Hint Resolve weakening_override : core.
Lemma weakening : forall G e t,
hasty G e t
-> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t)
-> hasty G' e t.
Proof.
induct 1; t.
Qed.
Local Hint Resolve weakening : core.
(* Replacing a typing context with an equal one has no effect (useful to guide
* proof search as a hint). *)
Lemma hasty_change : forall G e t,
hasty G e t
-> forall G', G' = G
-> hasty G' e t.
Proof.
t.
Qed.
Local Hint Resolve hasty_change : core.
Lemma substitution : forall G x t' e t e',
hasty (G $+ (x, t')) e t
-> hasty $0 e' t'
-> hasty G (subst e' x e) t.
Proof.
induct 1; t.
Qed.
Local Hint Resolve substitution : core.
Lemma preservation0 : forall e1 e2,
step0 e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
invert 1; t.
Qed.
Local Hint Resolve preservation0 : core.
Lemma generalize_plug : forall e1 C e1',
plug C e1 e1'
-> forall e2 e2', plug C e2 e2'
-> (forall t, hasty $0 e1 t -> hasty $0 e2 t)
-> (forall t, hasty $0 e1' t -> hasty $0 e2' t).
Proof.
induct 1; t.
Qed.
Local Hint Resolve generalize_plug : core.
Lemma preservation : forall e1 e2,
step e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
invert 1; t.
Qed.
Local Hint Resolve progress preservation : core.
Theorem safety : forall e t, hasty $0 e t
-> invariantFor (trsys_of e)
(fun e' => value e'
\/ exists e'', step e' e'').
Proof.
simplify.
apply invariant_weaken with (invariant1 := fun e' => hasty $0 e' t); eauto.
apply invariant_induction; simplify; eauto; equality.
Qed.
End Stlc.

283
LambdaCalculusAndTypeSoundness.v
View file

@ -54,7 +54,7 @@ Module Ulc.
| Value : forall x e, value (Abs x e).
(* We're cheating a bit here, *assuming* that the term is also closed. *)
Hint Constructors eval value.
Local Hint Constructors eval value : core.
(* Every value executes to itself. *)
Theorem value_eval : forall v,
@ -64,7 +64,7 @@ Module Ulc.
invert 1; eauto.
Qed.
Hint Resolve value_eval.
Local Hint Resolve value_eval : core.
(* Conversely, let's prove that [eval] only produces values. *)
Theorem eval_value : forall e v,
@ -74,7 +74,7 @@ Module Ulc.
induct 1; eauto.
Qed.
Hint Resolve eval_value.
Local Hint Resolve eval_value : core.
(* Some notations, to let us write more normal-looking lambda terms *)
Coercion Var : var >-> exp.
@ -343,7 +343,7 @@ Module Ulc.
-> plug c (subst v x e) e2
-> step e1 e2.
Hint Constructors plug step.
Local Hint Constructors plug step : core.
(* Here we now go through a proof of equivalence between big- and small-step
* semantics, though we won't spend any further commentary on it. *)
@ -360,7 +360,7 @@ Module Ulc.
invert H0; eauto.
Qed.
Hint Resolve step_eval''.
Local Hint Resolve step_eval'' : core.
Lemma step_eval' : forall e1 e2,
step e1 e2
@ -370,7 +370,7 @@ Module Ulc.
invert 1; simplify; eauto.
Qed.
Hint Resolve step_eval'.
Local Hint Resolve step_eval' : core.
Theorem step_eval : forall e v,
step^* e v
@ -413,7 +413,7 @@ Module Ulc.
induct 2; simplify; eauto.
Qed.
Hint Resolve compose_ok.
Local Hint Resolve compose_ok : core.
Lemma step_plug : forall e1 e2,
step e1 e2
@ -448,7 +448,7 @@ Module Ulc.
assumption.
Qed.
Hint Resolve stepStar_plug eval_value.
Local Hint Resolve stepStar_plug eval_value : core.
Theorem eval_step : forall e v,
eval e v
@ -494,49 +494,33 @@ Module Stlc.
| App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'')
end.
(* Evaluation contexts; note that we added cases for [Plus]. *)
Inductive context : Set :=
| Hole : context
| Plus1 : context -> exp -> context
| Plus2 : exp -> context -> context
| App1 : context -> exp -> context
| App2 : exp -> context -> context.
(* Small-step, call-by-value evaluation *)
(* Plugging an expression into a context *)
Inductive plug : context -> exp -> exp -> Prop :=
| PlugHole : forall e, plug Hole e e
| PlugPlus1 : forall e e' C e2,
plug C e e'
-> plug (Plus1 C e2) e (Plus e' e2)
| PlugPlus2 : forall e e' v1 C,
value v1
-> plug C e e'
-> plug (Plus2 v1 C) e (Plus v1 e')
| PlugApp1 : forall e e' C e2,
plug C e e'
-> plug (App1 C e2) e (App e' e2)
| PlugApp2 : forall e e' v1 C,
value v1
-> plug C e e'
-> plug (App2 v1 C) e (App v1 e').
(* Small-step, call-by-value evaluation, using our evaluation contexts *)
(* First: the primitive reductions *)
Inductive step0 : exp -> exp -> Prop :=
| Beta : forall x e v,
value v
-> step0 (App (Abs x e) v) (subst v x e)
| Add : forall n1 n2,
step0 (Plus (Const n1) (Const n2)) (Const (n1 + n2)).
(* Then: running them in context *)
Inductive step : exp -> exp -> Prop :=
| StepRule : forall C e1 e2 e1' e2',
plug C e1 e1'
-> plug C e2 e2'
-> step0 e1 e2
-> step e1' e2'.
(* These rules show the real action of the semantics. *)
| Beta : forall x e v,
value v
-> step (App (Abs x e) v) (subst v x e)
| Add : forall n1 n2,
step (Plus (Const n1) (Const n2)) (Const (n1 + n2))
(* Then we have a bunch of bureaucratic, repetitive rules encoding evaluation
* order. See next lecture for how to streamline this part, but for now note
* that the [value] premises below are crucial to enforce a single order of
* evaluation. *)
| App1 : forall e1 e1' e2,
step e1 e1'
-> step (App e1 e2) (App e1' e2)
| App2 : forall v e2 e2',
value v
-> step e2 e2'
-> step (App v e2) (App v e2')
| Plus1 : forall e1 e1' e2,
step e1 e1'
-> step (Plus e1 e2) (Plus e1' e2)
| Plus2 : forall v e2 e2',
value v
-> step e2 e2'
-> step (Plus v e2) (Plus v e2').
(* It's easy to wrap everything as a transition system. *)
Definition trsys_of (e : exp) := {|
@ -573,7 +557,7 @@ Module Stlc.
-> hasty G e2 t1
-> hasty G (App e1 e2) t2.
Hint Constructors value plug step0 step hasty.
Local Hint Constructors value step hasty : core.
(* Some notation to make it more pleasant to write programs *)
Infix "-->" := Fun (at level 60, right associativity).
@ -640,40 +624,31 @@ Module Stlc.
| [ H1 : value e2, H2 : hasty $0 e2 _ |- _ ] => invert H1; invert H2
end.
exists (Const (n + n0)).
eapply StepRule with (C := Hole).
eauto.
eauto.
constructor.
match goal with
| [ H : exists x, _ |- _ ] => invert H
end.
match goal with
| [ H : step _ _ |- _ ] => invert H
end.
right.
eauto.
exists (x ^+^ e2).
constructor.
assumption.
match goal with
| [ H : exists x, _ |- _ ] => invert H
end.
match goal with
| [ H : step _ _ |- _ ] => invert H
end.
right.
eauto.
exists (e1 ^+^ x).
apply Plus2.
assumption.
assumption.
match goal with
| [ H : exists x, step e1 _ |- _ ] => invert H
end.
match goal with
| [ H : step _ _ |- _ ] => invert H
| [ H : exists x, _ |- _ ] => invert H
end.
right.
exists (Plus x e2).
eapply StepRule with (C := Plus1 C e2).
eauto.
eauto.
exists (x ^+^ e2).
constructor.
assumption.
left.
@ -686,41 +661,33 @@ Module Stlc.
| [ H1 : value e1, H2 : hasty $0 e1 _ |- _ ] => invert H1; invert H2
end.
exists (subst e2 x e0).
eapply StepRule with (C := Hole).
eauto.
eauto.
constructor.
assumption.
match goal with
| [ H : exists x, _ |- _ ] => invert H
end.
match goal with
| [ H : step _ _ |- _ ] => invert H
end.
right.
eauto.
exists (x @ e2).
constructor.
assumption.
match goal with
| [ H : exists x, _ |- _ ] => invert H
end.
match goal with
| [ H : step _ _ |- _ ] => invert H
end.
right.
eauto.
exists (e1 @ x).
constructor.
assumption.
assumption.
match goal with
| [ H : exists x, step e1 _ |- _ ] => invert H
end.
match goal with
| [ H : step _ _ |- _ ] => invert H
end.
right.
exists (App x e2).
eapply StepRule with (C := App1 C e2).
eauto.
eauto.
constructor.
assumption.
Qed.
@ -819,92 +786,45 @@ Module Stlc.
eapply IHhasty2; equality.
Qed.
(* We're almost ready for the other main property. Let's prove it first
* for the more basic [step0] relation: steps preserve typing. *)
Lemma preservation0 : forall e1 e2,
step0 e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
invert 1; simplify.
invert H.
invert H4.
eapply substitution.
eassumption.
assumption.
invert H.
constructor.
Qed.
(* We also need this key property, essentially saying that, if [e1] and [e2] are
* "type-equivalent," then they remain "type-equivalent" after wrapping the same
* context around both. *)
Lemma generalize_plug : forall e1 C e1',
plug C e1 e1'
-> forall e2 e2', plug C e2 e2'
-> (forall t, hasty $0 e1 t -> hasty $0 e2 t)
-> (forall t, hasty $0 e1' t -> hasty $0 e2' t).
Proof.
induct 1; simplify.
invert H.
apply H0.
assumption.
invert H0.
invert H2.
constructor.
eapply IHplug.
eassumption.
assumption.
assumption.
assumption.
invert H1.
invert H3.
constructor.
assumption.
eapply IHplug.
eassumption.
assumption.
assumption.
invert H0.
invert H2.
econstructor.
eapply IHplug.
eassumption.
assumption.
eassumption.
assumption.
invert H1.
invert H3.
econstructor.
eassumption.
eapply IHplug.
eassumption.
assumption.
eassumption.
Qed.
(* OK, now we're almost done. Full steps really do preserve typing! *)
Lemma preservation : forall e1 e2,
step e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
invert 1; simplify.
induct 1; simplify.
eapply generalize_plug with (e1' := e1).
eassumption.
eassumption.
simplify.
eapply preservation0.
invert H0.
invert H4.
eapply substitution.
eassumption.
assumption.
invert H.
constructor.
invert H0.
econstructor.
apply IHstep.
eassumption.
assumption.
invert H1.
econstructor.
eassumption.
apply IHstep.
assumption.
invert H0.
constructor.
apply IHstep.
assumption.
assumption.
invert H1.
constructor.
assumption.
apply IHstep.
assumption.
Qed.
@ -946,11 +866,9 @@ Module Stlc.
| [ |- context[?x ==v ?y] ] => cases (x ==v y)
| [ H : Some _ = Some _ |- _ ] => invert H
| [ H : step _ _ |- _ ] => invert H
| [ H : step0 _ _ |- _ ] => invert1 H
| [ H : step _ _ |- _ ] => invert1 H
| [ H : hasty _ ?e _, H' : value ?e |- _ ] => invert H'; invert H
| [ H : hasty _ _ _ |- _ ] => invert1 H
| [ H : plug _ _ _ |- _ ] => invert1 H
end; subst.
Ltac t := simplify; propositional; repeat (t0; simplify); try equality; eauto 6.
@ -963,7 +881,7 @@ Module Stlc.
induct 1; t.
Qed.
Hint Resolve weakening_override.
Local Hint Resolve weakening_override : core.
Lemma weakening_snazzy : forall G e t,
hasty G e t
@ -973,7 +891,7 @@ Module Stlc.
induct 1; t.
Qed.
Hint Resolve weakening_snazzy.
Local Hint Resolve weakening_snazzy : core.
(* Replacing a typing context with an equal one has no effect (useful to guide
* proof search as a hint). *)
@ -985,7 +903,7 @@ Module Stlc.
t.
Qed.
Hint Resolve hasty_change.
Local Hint Resolve hasty_change : core.
Lemma substitution_snazzy : forall G x t' e t e',
hasty (G $+ (x, t')) e t
@ -995,38 +913,17 @@ Module Stlc.
induct 1; t.
Qed.
Hint Resolve substitution_snazzy.
Lemma preservation0_snazzy : forall e1 e2,
step0 e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
invert 1; t.
Qed.
Hint Resolve preservation0_snazzy.
Lemma generalize_plug_snazzy : forall e1 C e1',
plug C e1 e1'
-> forall e2 e2', plug C e2 e2'
-> (forall t, hasty $0 e1 t -> hasty $0 e2 t)
-> (forall t, hasty $0 e1' t -> hasty $0 e2' t).
Proof.
induct 1; t.
Qed.
Hint Resolve generalize_plug_snazzy.
Local Hint Resolve substitution_snazzy : core.
Lemma preservation_snazzy : forall e1 e2,
step e1 e2
-> forall t, hasty $0 e1 t
-> hasty $0 e2 t.
Proof.
invert 1; t.
induct 1; t.
Qed.
Hint Resolve progress_snazzy preservation_snazzy.
Local Hint Resolve progress_snazzy preservation_snazzy : core.
Theorem safety_snazzy : forall e t, hasty $0 e t
-> invariantFor (trsys_of e)

1
_CoqProject
View file

@ -41,6 +41,7 @@ SubsetTypes_template.v
SubsetTypes.v
LambdaCalculusAndTypeSoundness_template.v
LambdaCalculusAndTypeSoundness.v
EvaluationContexts.v
DependentInductiveTypes_template.v
DependentInductiveTypes.v
TypesAndMutation.v

170
frap_book.tex
View file

@ -3281,6 +3281,176 @@ Since the basic proof structure matches our standard one, the main insight is th
In this case, invariant $I(e) = \; \hasty{}{e}{\tau}$ is that crucial insight, including the original design of the set of types and the typing relation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{More on Evaluation Contexts}\label{ectx}
\section{Small-Step Semantics}
$\lambda$-calculus is also straightforward to formalize with a small-step semantics\index{small-step operational semantics} and evaluation contexts\index{evaluation contexts}, following the method of Section \ref{eval_contexts}.
One might argue that the technique is even simpler for $\lambda$-calculus, since we must deal only with expressions, not also imperative variable valuations.
$$\begin{array}{rrcl}
\textrm{Evaluation contexts} & C &::=& \Box \mid C \; e \mid v \; C
\end{array}$$
Note the one subtlety: the last form of evaluation context requires the term in a function position to be a \emph{value}.
This innocuous-looking restriction enforces \emph{call-by-value evaluation order}\index{call-by-value}, where, upon encountering a function application, we must first evaluate the function, then evaluate the argument, and only then call the function.
Tweaks to the definition of $C$ produce other evaluation orders, like \emph{call-by-name}\index{call-by-name}, but we will say no more about those alternatives.
We assume a standard definition of what it means to plug an expression into the hole in a context, and now we can give the sole small-step evaluation rule for basic $\lambda$-calculus, conventionally called the \emph{$\beta$-reduction} rule\index{$\beta$-reduction}.
\encoding
$$\infer{\smallstep{\plug{C}{(\lambda x. \; e) \; v}}{\plug{C}{\subst{e}{x}{v}}}}{}$$
That is, we find a suitable position within the expression where a $\lambda$-expression is applied to a value, and we replace that position with the appropriate substitution result.
Following a very similar outline to what we used in Chapter \ref{operational_semantics}, we establish equivalence between the two semantics for $\lambda$-calculus.
\begin{theorem}
If $\smallsteps{e}{v}$, then $\bigstep{e}{v}$.
\end{theorem}
\begin{theorem}
If $\bigstep{e}{v}$, then $\smallsteps{e}{v}$.
\end{theorem}
There are a few proof subtleties beyond what we encountered before, and the Coq formalization may be worth reading, to see those details.
Again as before, we have a natural way to build a transition system from any $\lambda$-term $e$, where $\mathcal L$ is the set of $\lambda$-terms.
We define $\mathbb T(e) = \angled{\mathcal L, \{e\}, \to}$.
The next section gives probably the most celebrated $\lambda$-calculus result based on the transition-system perspective.
\section{Simple Types and Their Soundness}
Let's spruce up the language with some more constructs.
$$\begin{array}{rrcl}
\textrm{Variables} & x &\in& \mathsf{Strings} \\
\textrm{Numbers} & n &\in& \mathbb N \\
\textrm{Expressions} & e &::=& n \mid e + e \mid x \mid \lambda x. \; e \mid e \; e \\
\textrm{Values} & v &::=& n \mid \lambda x. \; e
\end{array}$$
We've added natural numbers as a primitive feature, supported via constants and addition.
Numbers may be intermixed with functions, and we may, for instance, write first-class functions that take numbers as input or return numbers.
Our language of evaluation contexts expands a bit.
$$\begin{array}{rrcl}
\textrm{Evaluation contexts} & C &::=& \Box \mid C \; e \mid v \; C \mid C + e \mid v + C
\end{array}$$
Now we want to define two kinds of basic small steps, so it is worth defining a separate relation for them.
Here we face a classic nuisance in writing rules that combine explicit syntax with standard mathematical operators, and we write $+$ for the syntactic construct and $\textbf{+}$ for the mathematical addition operator.
$$\infer{\smallstepo{(\lambda x. \; e) \; v}{\subst{e}{x}{v}}}{}
\quad \infer{\smallstepo{n + m}{n \textbf{+} m}}{}$$
Here is the overall step rule.
$$\infer{\smallstep{\plug{C}{e}}{\plug{C}{e'}}}{
\smallstepo{e}{e'}
}$$
What would be a useful property to prove about our new expressions?
For one thing, we don't want them to ``crash,'' as in the expression $(\lambda x. \; x) + 7$ that tries to add a function and a number.
No rule of the semantics knows what to do with that case, but it also isn't a value, so we shouldn't consider it as finished with evaluation.
Define an expression as \emph{stuck}\index{stuck term} when it is not a value and it cannot take a small step.
For ``reasonable'' expressions $e$, we should be able to prove that it is an invariant of $\mathbb T(e)$ that no expression is ever stuck.
To define ``reasonable,'' we formalize the popular idea of a static type system.
Every expression will be assigned a type, capturing which sorts of contexts it may legally be dropped into.
Our language of types is simple.
\abstraction
$$\begin{array}{rrcl}
\textrm{Types} & \tau &::=& \mathbb N \mid \tau \to \tau
\end{array}$$
We have trees of function-space constructors, where all the leaves are instances of the natural-number type $\mathbb N$.
Note that, with type assignment, we have yet another case of \emph{abstraction}, approximating a potentially complex expression with a type that only records enough information to rule out crashes.
To assign types to closed terms, we must recursively define what it means for an open term to have a type.
To that end, we use \emph{typing contexts}\index{typing context} $\Gamma$, finite maps from variables to types.
To mimic standard notation, we write $\Gamma, x : \tau$ as shorthand for $\mupd{\Gamma}{x}{\tau}$, overriding of key $x$ with value $\tau$ in $\Gamma$.
Now we define typing as a three-place relation, written $\hasty{\Gamma}{e}{\tau}$, to indicate that, assuming $\Gamma$ as an assignment of types to $e$'s free variables, we conclude that $e$ has type $\tau$.
We define the relation inductively, with one case per syntactic construct.
\modularity
$$\infer{\hasty{\Gamma}{x}{\tau}}{
\msel{\Gamma}{x} = \tau
}
\quad \infer{\hasty{\Gamma}{n}{\mathbb N}}{}
\quad \infer{\hasty{\Gamma}{e_1 + e_2}{\mathbb N}}{
\hasty{\Gamma}{e_1}{\mathbb N}
& \hasty{\Gamma}{e_2}{\mathbb N}
}$$
$$\infer{\hasty{\Gamma}{\lambda x. \; e}{\tau_1 \to \tau_2}}{
\hasty{\Gamma, x : \tau_1}{e}{\tau_2}
}
\quad \infer{\hasty{\Gamma}{e_1 \; e_2}{\tau_2}}{
\hasty{\Gamma}{e_1}{\tau_1 \to \tau_2}
& \hasty{\Gamma}{e_2}{\tau_1}
}$$
We write $\hasty{}{e}{\tau}$ as shorthand for $\hasty{\mempty}{e}{\tau}$, meaning that closed term $e$ has type $\tau$, with no typing context required.
Note that this style of typing rules provides another instance of \emph{modularity}, since we can separately type-check different subexpressions of a large expression, using just their types to coordinate expectations among subexpressions.
It should be an invariant of $\mathbb T(e)$ that every reachable expression has the same type as the original, so long as the original was well-typed.
This observation is the key to proving that it is also an invariant that no reachable expression is stuck, using a proof technique called \emph{the syntactic approach to type soundness}\index{syntactic approach to type soundness}, which turns out to be just another instance of our general toolbox for invariant proofs.
We work our way through a suite of standard lemmas to support that invariant proof.
\begin{lemma}[Progress]\label{progress}
If $\hasty{}{e}{\tau}$, then $e$ isn't stuck.
\end{lemma}
\begin{proof}
By induction on the derivation of $\hasty{}{e}{\tau}$.
\end{proof}
\begin{lemma}[Weakening]\label{weakening}
If $\hasty{\Gamma}{e}{\tau}$ and every mapping in $\Gamma$ is also included in $\Gamma'$, then $\hasty{\Gamma'}{e}{\tau}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\hasty{\Gamma}{e}{\tau}$.
\end{proof}
\begin{lemma}[Substitution]\label{substitution}
If $\hasty{\Gamma, x : \tau'}{e}{\tau}$ and $\hasty{}{e'}{\tau'}$, then $\hasty{\Gamma}{\subst{e}{x}{e'}}{\tau}$.
\end{lemma}
\begin{proof}
By induction on the derivation of $\hasty{\Gamma, x: \tau'}{e}{\tau}$, with appeal to Lemma \ref{weakening}.
\end{proof}
\begin{lemma}\label{preservation0}
If $\smallstepo{e}{e'}$ and $\hasty{}{e}{\tau}$, then $\hasty{}{e'}{\tau}$.
\end{lemma}
\begin{proof}
By inversion on the derivation of $\smallstepo{e}{e'}$, with appeal to Lemma \ref{substitution}.
\end{proof}
\begin{lemma}\label{generalize_plug}
If any type of $e_1$ is also a type of $e_2$, then any type of $\plug{C}{e_1}$ is also a type of $\plug{C}{e_2}$.
\end{lemma}
\begin{proof}
By induction on the structure of $C$.
\end{proof}
\begin{lemma}[Preservation]\label{preservation}
If $\smallstep{e_1}{e_2}$ and $\hasty{}{e_1}{\tau}$, then $\hasty{}{e_2}{\tau}$.
\end{lemma}
\begin{proof}
By inversion on the derivation of $\smallstep{e_1}{e_2}$, with appeal to Lemmas \ref{preservation0} and \ref{generalize_plug}.
\end{proof}
\invariants
\begin{theorem}[Type Soundness]
If $\hasty{}{e}{\tau}$, then $\neg \textrm{stuck}$ is an invariant of $\mathbb T(e)$.
\end{theorem}
\begin{proof}
First, we strengthen the invariant to $I(e) = \; \hasty{}{e}{\tau}$, justifying the implication by Lemma \ref{progress}, Progress.
Then we apply invariant induction, where the base case is trivial.
The induction step is a direct match for Lemma \ref{preservation}, Preservation.
\end{proof}
The syntactic approach to type soundness is often presented as a proof technique in isolation, but what we see here is that it follows very directly from our general invariant proof technique.
Usually syntactic type soundness is presented as fundamentally about proving Progress and Preservation conditions.
The Progress condition maps to invariant strengthening, and the Preservation condition maps to invariant induction, which we have used in almost every invariant proof so far.
Since the basic proof structure matches our standard one, the main insight is the usual one: a good choice of a strengthened invariant.
In this case, invariant $I(e) = \; \hasty{}{e}{\tau}$ is that crucial insight, including the original design of the set of types and the typing relation.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\chapter{Types and Mutation}