From 5cdd4d13229867220f50cb842082e8252f47ecf7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 27 Mar 2021 17:03:26 -0400 Subject: [PATCH] Start of splitting evaluation contexts out of LambdaCalculusAndTypeSoundness --- EvaluationContexts.v | 219 ++++++++++++++++++++++++ LambdaCalculusAndTypeSoundness.v | 283 ++++++++++--------------------- _CoqProject | 1 + frap_book.tex | 170 +++++++++++++++++++ 4 files changed, 480 insertions(+), 193 deletions(-) create mode 100644 EvaluationContexts.v diff --git a/EvaluationContexts.v b/EvaluationContexts.v new file mode 100644 index 0000000..7102ef0 --- /dev/null +++ b/EvaluationContexts.v @@ -0,0 +1,219 @@ +(** Formal Reasoning About Programs + * 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. diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v index 7465afb..237e894 100644 --- a/LambdaCalculusAndTypeSoundness.v +++ b/LambdaCalculusAndTypeSoundness.v @@ -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) diff --git a/_CoqProject b/_CoqProject index 4300b13..c070bbf 100644 --- a/_CoqProject +++ b/_CoqProject @@ -41,6 +41,7 @@ SubsetTypes_template.v SubsetTypes.v LambdaCalculusAndTypeSoundness_template.v LambdaCalculusAndTypeSoundness.v +EvaluationContexts.v DependentInductiveTypes_template.v DependentInductiveTypes.v TypesAndMutation.v diff --git a/frap_book.tex b/frap_book.tex index 3efa674..fce6fbf 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -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}