From ec261d542c0b97fa81ee785456efdbfdccb1b906 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 Mar 2016 15:17:09 -0400 Subject: [PATCH] Comment LambdaCalculusAndTypeSoundness --- LambdaCalculusAndTypeSoundness.v | 142 +++++++++++++++++++++++-------- 1 file changed, 105 insertions(+), 37 deletions(-) diff --git a/LambdaCalculusAndTypeSoundness.v b/LambdaCalculusAndTypeSoundness.v index eb1541b..300ddba 100644 --- a/LambdaCalculusAndTypeSoundness.v +++ b/LambdaCalculusAndTypeSoundness.v @@ -5,13 +5,27 @@ Require Import Frap. -Module Ulc. - Inductive exp : Set := - | Var : var -> exp - | Abs : var -> exp -> exp - | App : exp -> exp -> exp. +(* The last few chapters have focused on small programming languages that are + * representative of the essence of the imperative languages. We now turn to + * lambda-calculus, the usual representative of functional languages. *) - Fixpoint subst (rep : exp) (x : string) (e : exp) : exp := +Module Ulc. + (* Programs are expressions, which we evaluate algebraically, rather than + * executing for side effects. *) + Inductive exp : Set := + | Var (x : var) + | Abs (x : var) (body : exp) + (* A function that binds its argument to the given variable, evaluating the + * body expression *) + | App (e1 e2 : exp). + (* Applying a function to an argument *) + + (* Key operation: within [e], changing every occurrence of variable [x] into + * [rep]. IMPORTANT: we will only apply this operation in contexts where + * [rep] is *closed*, meaning every [Var] refers to some enclosing [Abs], so + * as to avoid *variable capture*. See the book proper for a little more + * discussion. *) + Fixpoint subst (rep : exp) (x : var) (e : exp) : exp := match e with | Var y => if string_dec y x then rep else Var y | Abs y e1 => Abs y (if y ==v x then e1 else subst rep x e1) @@ -21,8 +35,8 @@ Module Ulc. (** * Big-step semantics *) - (** This is the most straightforward way to give semantics to lambda terms: - * We evaluate any closed term into a value (that is, an [Abs]). *) + (* This is the most straightforward way to give semantics to lambda terms: + * We evaluate any closed term into a value (that is, an [Abs]). *) Inductive eval : exp -> exp -> Prop := | BigAbs : forall x e, eval (Abs x e) (Abs x e) @@ -32,7 +46,8 @@ Module Ulc. -> eval (subst v2 x e1') v -> eval (App e1 e2) v. - (** Note that we omit a [Var] case, since variable terms can't be *closed*. *) + (* Note that we omit a [Var] case, since variable terms can't be *closed*, + * and therefore they aren't meaningful as top-level programs. *) (** Which terms are values, that is, final results of execution? *) Inductive value : exp -> Prop := @@ -41,6 +56,7 @@ Module Ulc. Hint Constructors eval value. + (* Every value executes to itself. *) Theorem value_eval : forall v, value v -> eval v v. @@ -50,7 +66,7 @@ Module Ulc. Hint Resolve value_eval. - (** Actually, let's prove that [eval] only produces values. *) + (** Conversely, let's prove that [eval] only produces values. *) Theorem eval_value : forall e v, eval e v -> value v. @@ -60,24 +76,39 @@ Module Ulc. Hint Resolve eval_value. + (* Some notations, to let us write more normal-looking lambda terms *) Coercion Var : var >-> exp. Notation "\ x , e" := (Abs x e) (at level 50). Infix "@" := App (at level 49, left associativity). + + (** * Church Numerals, everyone's favorite example of lambda terms in + * action *) + + (* Here are two curious definitions. *) Definition zero := \"f", \"x", "x". Definition plus1 := \"n", \"f", \"x", "f" @ ("n" @ "f" @ "x"). + (* We can build up any natural number [n] as [plus1^n @ zero]. Let's prove + * that, in fact, these definitions constitute a workable embedding of the + * natural numbers in lambda-calculus. *) + + (* A term [plus^n @ zero] evaluates to something very close to what this + * function returns. *) Fixpoint canonical' (n : nat) : exp := match n with | O => "x" | S n' => "f" @ ((\"f", \"x", canonical' n') @ "f" @ "x") end. + (* This missing piece is this wrapper. *) Definition canonical n := \"f", \"x", canonical' n. + (* Let's formalize our definition of what it means to represent a number. *) Definition represents (e : exp) (n : nat) := eval e (canonical n). + (* Zero passes the test. *) Theorem zero_ok : represents zero 0. Proof. unfold zero, represents, canonical. @@ -85,6 +116,7 @@ Module Ulc. econstructor. Qed. + (* So does our successor operation. *) Theorem plus1_ok : forall e n, represents e n -> represents (plus1 @ e) (S n). Proof. @@ -96,8 +128,15 @@ Module Ulc. econstructor. Qed. + (* What's basically going on here? The representation of number [n] is [N] + * such that, for any function [f]: + * N(f) = f^n + * That is, we represent a number as its repeated-composition operator. + * So, given a number, we can use it to repeat any operation. In particular, + * to implement addition, we can just repeat [plus1]! *) Definition add := \"n", \"m", "n" @ plus1 @ "m". + (* Our addition works properly on this test case. *) Example add_1_2 : exists v, eval (add @ (plus1 @ zero) @ (plus1 @ (plus1 @ zero))) v /\ eval (plus1 @ (plus1 @ (plus1 @ zero))) v. @@ -107,12 +146,16 @@ Module Ulc. repeat econstructor. Qed. + (* By the way: since [canonical'] doesn't mention variable "m", substituting + * for "m" has no effect. This fact will come in handy shortly. *) Lemma subst_m_canonical' : forall m n, subst m "m" (canonical' n) = canonical' n. Proof. induct n; simplify; equality. Qed. + (* This inductive proof is the workhorse for the next result, so let's skip + * ahead there. *) Lemma add_ok' : forall m n, eval (subst (\ "f", (\ "x", canonical' m)) "x" @@ -139,6 +182,7 @@ Module Ulc. econstructor. Qed. + (* [add] properly encodes the usual addition. *) Theorem add_ok : forall n ne m me, represents ne n -> represents me m @@ -165,6 +209,8 @@ Module Ulc. apply add_ok'. Qed. + (* Let's repeat the same exercise for multiplication. *) + Definition mult := \"n", \"m", "n" @ (add @ "m") @ zero. Example mult_1_2 : exists v, @@ -210,7 +256,7 @@ Module Ulc. econstructor. econstructor. rewrite subst_m_canonical'. - apply add_ok'. + apply add_ok'. (* Note the recursive appeal to correctness of [add]. *) Qed. Theorem mult_ok : forall n ne m me, @@ -247,6 +293,9 @@ Module Ulc. (** * Small-step semantics with evaluation contexts *) + (* We can also port to this setting our small-step semantics style based on + * evaluation contexts. *) + Inductive context : Set := | Hole : context | App1 : context -> exp -> context @@ -269,6 +318,9 @@ Module Ulc. * *call-by-value* instead of other evaluation strategies. Details are * largely beyond our scope here. *) + (* Compared to the small-step contextual semantics from two chapters back, we + * skip a [step0] relation, since function application (called "beta + * reduction") is the only option here. *) Inductive step : exp -> exp -> Prop := | ContextBeta : forall c x e v e1 e2, value v @@ -278,7 +330,8 @@ Module Ulc. Hint Constructors plug step. - (** We can move directly to establishing inclusion from basic small steps to contextual small steps. *) + (* 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. *) Lemma step_eval'' : forall v c x e e1 e2 v0, value v @@ -396,8 +449,12 @@ Module Ulc. Qed. End Ulc. + +(** * Now we turn to a variant of lambda calculus with static type-checking. + * This variant is called *simply typed* lambda calculus, and *simple* has a + * technical meaning, which we will explore relaxing in a problem set. *) Module Stlc. - (* Expression syntax *) + (* We add expression forms for numeric constants and addition. *) Inductive exp : Set := | Var (x : var) | Const (n : nat) @@ -421,7 +478,7 @@ Module Stlc. | App e2' e2'' => App (subst e1 x e2') (subst e1 x e2'') end. - (* Evaluation contexts *) + (* Evaluation contexts; note that we added cases for [Plus]. *) Inductive context : Set := | Hole : context | Plus1 : context -> exp -> context @@ -472,13 +529,16 @@ Module Stlc. |}. - (* Syntax of types *) + (* That language is suitable to describe with a static *type system*. Here's + * our modest, but countably infinite, set of types. *) Inductive type : Set := - | Nat - | Fun (dom ran : type). + | Nat (* Numbers *) + | Fun (dom ran : type) (* Functions *). - (* Our typing judgment uses *typing contexts* (not to be confused with - * evaluation contexts) to map free variables to their types. *) + (* Our typing relation (also often called a "judgment") uses *typing contexts* + * (not to be confused with evaluation contexts) to map free variables to + * their types. Free variables are those that don't refer to enclosing [Abs] + * binders. *) Inductive hasty : fmap var type -> exp -> type -> Prop := | HtVar : forall G x t, G $? x = Some t @@ -499,6 +559,7 @@ Module Stlc. Hint Constructors value plug step0 step hasty. + (* Some notation to make it more pleasant to write programs *) Infix "-->" := Fun (at level 60, right associativity). Coercion Const : nat >-> exp. Infix "^+^" := Plus (at level 50). @@ -506,6 +567,8 @@ Module Stlc. Notation "\ x , e" := (Abs x e) (at level 51). Infix "@" := App (at level 49, left associativity). + (* Some examples of typed programs *) + Example one_plus_one : hasty $0 (1 ^+^ 1) Nat. Proof. repeat (econstructor; simplify). @@ -527,19 +590,24 @@ Module Stlc. Qed. - (** * Some examples of typed programs *) - - (** * Let's prove type soundness first without much automation. *) - (* Now we're ready for the first of the two key properties, to show that "has - * type t in the empty typing context" is an invariant. *) + (* What useful invariants could we prove about programs in this language? How + * about that, at every point, either they're finished executing or they can + * take further steps? For instance, a program that tried to add a function + * to a number would not satisfy that condition, and we call it *stuck*. We + * want to prove that typed programs can never become stuck. Here's a good + * invariant to strive for. *) + Definition unstuck e := value e + \/ (exists e' : exp, step e e'). + + (* Now we're ready for the first of the two key properties to establish that + * invariant: well-typed programs are never stuck. *) Lemma progress : forall e t, hasty $0 e t - -> value e - \/ (exists e' : exp, step e e'). + -> unstuck e. Proof. - induct 1; simplify; try equality. + unfold unstuck; induct 1; simplify; try equality. left. constructor. @@ -635,7 +703,8 @@ Module Stlc. cases (x ==v x'); simplify; eauto. Qed. - (** Raising a typing derivation to a larger typing context *) + (* This lemma lets us transplant a typing derivation into a new context that + * includes the old one. *) Lemma weakening : forall G e t, hasty G e t -> forall G', (forall x t, G $? x = Some t -> G' $? x = Some t) @@ -722,8 +791,8 @@ Module Stlc. assumption. Qed. - (* We're almost ready for the main preservation property. Let's prove it first - * for the more basic [step0] relation. *) + (* 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 @@ -793,7 +862,7 @@ Module Stlc. eassumption. Qed. - (* OK, now we're almost done. *) + (* 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 @@ -811,14 +880,12 @@ Module Stlc. assumption. Qed. - (* Now watch this! Though the syntactic approach to type soundness is usually + (* Now watch this! Though this syntactic approach to type soundness is usually * presented from scratch as a proof technique, it turns out that the two key * properties, progress and preservation, are just instances of the same methods * we've been applying all along with invariants of transition systems! *) Theorem safety : forall e t, hasty $0 e t - -> invariantFor (trsys_of e) - (fun e' => value e' - \/ exists e'', step e' e''). + -> invariantFor (trsys_of e) unstuck. Proof. simplify. @@ -842,7 +909,8 @@ Module Stlc. Qed. - (** * Let's do that again with more automation. *) + (** * Let's do that again with more automation, whose details are beyond the + * scope of the book. *) Ltac t0 := match goal with | [ H : ex _ |- _ ] => destruct H @@ -880,7 +948,7 @@ Module Stlc. Hint Resolve weakening_snazzy. (* Replacing a typing context with an equal one has no effect (useful to guide - * proof search). *) + * proof search as a hint). *) Lemma hasty_change : forall G e t, hasty G e t -> forall G', G' = G