From a515aaf2894c8f40cf6a93e5d11e85033e848d8c Mon Sep 17 00:00:00 2001 From: wadler Date: Sun, 20 May 2018 19:39:58 -0300 Subject: [PATCH] added Lambda and LambdaProp --- src/Lambda.lagda | 1026 ++++++++++++++++++++++++++++++++++++++++++ src/LambdaProp.lagda | 662 +++++++++++++++++++++++++++ 2 files changed, 1688 insertions(+) create mode 100644 src/Lambda.lagda create mode 100644 src/LambdaProp.lagda diff --git a/src/Lambda.lagda b/src/Lambda.lagda new file mode 100644 index 00000000..f5a28121 --- /dev/null +++ b/src/Lambda.lagda @@ -0,0 +1,1026 @@ +--- +title : "Lambda: Introduction to Lambda Calculus" +layout : page +permalink : /Lambda +--- + +The _lambda-calculus_, first published by the logician Alonzo Church in +1932, is a core calculus with only three syntactic constructs: +variables, abstraction, and application. It embodies the concept of +_functional abstraction_, which shows up in almost every programming +language in some form (as functions, procedures, or methods). +The _simply-typed lambda calculus_ (or STLC) is a variant of the +lambda calculus published by Church in 1940. It has the three +constructs above for function types, plus whatever else is required +for base types. Church had a minimal base type with no operations. +We will instead echo the power of Plotkin's Programmable Computable +Functions (PCF), and add operations on natural numbers and +recursive function definitions. + +This chapter formalises the simply-typed lambda calculus, giving its +syntax, small-step semantics, and typing rules. The next chapter +[LambdaProp](LambdaProp) reviews its main properties, including +progress and preservation. Following chapters will look at a number +of variants of lambda calculus. + +Readers should be warned up front: the approach we take here is +_not_ our recommended approach to formalisation. It turns out that +using De Bruijn indices and inherently-typed terms, as we will do in +Chapter [DeBruijn](DeBruijn), leads to a more compact formulation. +Nonetheless, we begin with named variables, partly because such terms +are easier to read and partly because the development is more traditional. + + +## Imports + +\begin{code} +module Lambda where + +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) +open import Data.String using (String; _≟_) +open import Data.Nat using (ℕ; zero; suc) +open import Data.Empty using (⊥; ⊥-elim) +open import Relation.Nullary using (Dec; yes; no; ¬_) +\end{code} + +## Syntax of terms + +Terms have seven constructs. Three are for the core lambda calculus: + + * Variables, `# x` + * Abstractions, `ƛ x ⇒ N` + * Applications, `L · M` + +Three are for the naturals: + + * Zero, `` `zero `` + * Successor, `` `suc `` + * Case, `` `case L [zero⇒ M |suc x⇒ N ] + +And one is for recursion: + + * Fixpoint, `μ x ⇒ M` + +Abstraction is also called lambda abstraction, and is the construct +from which the calculus takes its name. + +With the exception of variables and fixpoints, each term +form either constructs a value of a given type (abstractions yield functions, +zero and successor yield booleans) or deconstructs it (applications use functions, +case terms use naturals). We will see this again when we come +to the rules for assigning types to terms, where constructors +correspond to introduction rules and deconstructors to eliminators. + +Here is the syntax of terms in BNF. + + L, M, N ::= + # x + ƛ x ⇒ N + L · M + `zero + `suc M + `case L [zero⇒ M |suc x ⇒ N] + μ x ⇒ M + +And here it is formalised in Agda. +\begin{code} +Id : Set +Id = String + +infix 5 ƛ_⇒_ +infix 5 μ_⇒_ +infix 6 `suc_ +infixl 8 _·_ +infix 9 #_ + +data Term : Set where + #_ : Id → Term + ƛ_⇒_ : Id → Term → Term + _·_ : Term → Term → Term + `zero : Term + `suc_ : Term → Term + `case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term + μ_⇒_ : Id → Term → Term +\end{code} +We represent identifiers by strings. We choose precedence so that +lambda abstraction and fixpoint bind least tightly, then successor, then application, +and tightest of all is the constructor for variables. Case +expressions are self-bracketing. + +### Example terms + +Here are some example terms: the naturals two and four, the recursive +definition of a function to naturals, and a term that computes +two plus two. +\begin{code} +tm2 tm4 tm+ tm2+2 : Term +tm2 = `suc `suc `zero +tm4 = `suc `suc `suc `suc `zero +tm+ = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ + `case # "m" + [zero⇒ # "n" + |suc "m" ⇒ `suc (# "+" · # "m" · # "n") ] +tm2+2 = tm+ · tm2 · tm2 +\end{code} +The recursive definition of addition is similar to our original +definition of `_+_` for naturals, as given in Chapter [Natural](Naturals). + +As a second example, we use higher-order functions to represent +natural numbers. In particular, the number _n_ is represented by a +function that accepts two arguments and applies the first to the +second _n_ times. This is called the _Church representation_ of the +naturals. Similar to before, we define: the numerals two and four, a +function to add numerals, a function to convert numerals to naturals, +and a term that computes two plus two. +\begin{code} +ch2 ch4 ch+ chℕ ch2+2 : Term +ch2 = ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z") +ch4 = ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · (# "s" · (# "s" · # "z"))) +ch+ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ + # "m" · # "s" · (# "n" · # "s" · # "z") +chℕ = ƛ "n" ⇒ # "n" · (ƛ "m" ⇒ `suc (# "m")) · `zero +ch2+2 = ch+ · ch2 · ch2 +\end{code} +Two takes two arguments `s` and `z`, and applies `s` twice to `z`; +similarly for four. Addition takes two numerals `m` and `n`, a +function `s` and an argument `z`, and it uses `m` to apply `s` to the +result of using `n` to apply `s` to `z`; hence `s` is applied `m` plus +`n` times to `z`, yielding the Church numeral for the sum of `m` and +`n`. The conversion function takes a numeral `n` and instantiates its +first argument to the successor function and its second argument to +zero. + +### Formal vs informal + +In informal presentation of formal semantics, one uses choice of +variable name to disambiguate and writes `x` rather than `# x` +for a term that is a variable. Agda requires we distinguish. +Often researchers use `var x` rather than `# x`, but we chose +the latter as less noisy. + +Similarly, informal presentation often use the same notation for +function types, lambda abstraction, and function application in both +the object language (the language one is describing) and the +meta-language (the language in which the description is written), +trusting readers can use context to distinguish the two. Agda is is +not quite so forgiving, so here we use `ƛ x ⇒ N` and `L · M` for the +object language, as compared to `λ x → N` and `L M` in our +meta-language, Agda. + + +### Bound and free variables + +In an abstraction `ƛ x ⇒ N` we call `x` the _bound_ variable +and `N` the _body_ of the abstraction. One of the most important +aspects of lambda calculus is consistent renaming of bound variables +leaves the meaning of a term unchanged. Thus the five terms + +* `` ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z") `` +* `` ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") `` +* `` ƛ "fred" ⇒ ƛ "xander" ⇒ # "fred" · (# "fred" · # "xander") `` +* `` λ[ 😇 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😈 ∶ 𝔹 ] ` 😇 · (` 😇 · ` 😈 ) `` +* `` ƛ "z" ⇒ ƛ "s" ⇒ # "z" · (# "z" · # "s") `` + +are all considered equivalent. Following the convention introduced +by Haskell Curry, this equivalence relation is called _alpha renaming_. + +As we descend from a term into its subterms, variables +that are bound may become free. Consider the following terms. + +* `` ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z") `` + has both `s` and `z` as bound variables. + +* `` ƛ "z" ⇒ # "s" · (# "s" · # "z") `` + has `s` bound and `z` free. + +* `` # "s" · (# "s" · # "z") `` + has both `s` and `z` as free variables. + +We say that a term with no free variables is _closed_; otherwise it is +_open_. Of the three terms above, the first is closed and the other +two are open. + +Different occurrences of a variable may be bound and free. +In the term + + (ƛ "x" ⇒ # "x") · # "x" + +the inner occurrence of `x` is bound while the outer occurrence is free. +Note that by alpha renaming, the term above is equivalent to + + (ƛ "y" ⇒ # "y") · # "x" + +in which `y` is bound and `x` is free. A common convention, called the +Barendregt convention, is to use alpha renaming to ensure that the bound +variables in a term are distinct from the free variables, which can +avoid confusions that may arise if bound and free variables have the +same names. + +Case and recursion also introduce bound variables, which are also subject +to alpha renaming. In the term + + μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ + `case # "m" + [zero⇒ # "n" + |suc "m" ⇒ `suc (# "+" · # "m" · # "n") ] + +notice that there are two binding occurrences of `m`, one in the first +line and one in the last line. It is equivalent to the following term, + + μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒ + `case # "x" + [zero⇒ # "y" + |suc "x′" ⇒ `suc (# "plus" · # "x′" · # "y") ] + +where the two binding occurrences corresponding to `m` now have distinct +names, `x` and `x′`. + + +## Values + +We only consider reduction of _closed_ terms, +those that contain no free variables. We consider +a precise definition of free variables in Chapter +[LambdaProp](LambdaProp). + +*rewrite (((* +A term is a value if it is fully reduced. +For booleans, the situation is clear: `true` and +`false` are values, while conditionals are not. +For functions, applications are not values, because +we expect them to further reduce, and variables are +not values, because we focus on closed terms. +Following convention, we treat all abstractions +as values. +*)))* + +The predicate `Value M` holds if term `M` is a value. + +\begin{code} +data Value : Term → Set where + + value-ƛ : ∀ {x N} + --------------- + → Value (ƛ x ⇒ N) + + value-zero : + ----------- + Value `zero + + value-suc : ∀ {V} + → Value V + -------------- + → Value (`suc V) +\end{code} + +We let `V` and `W` range over values. + + +### Formal vs informal + +In informal presentations of formal semantics, using +`V` as the name of a metavariable is sufficient to +indicate that it is a value. In Agda, we must explicitly +invoke the `Value` predicate. + +### Other approaches + +An alternative is not to focus on closed terms, +to treat variables as values, and to treat +`ƛ x ⇒ N` as a value only if `N` is a value. +Indeed, this is how Agda normalises terms. +We consider this approach in a [later chapter](Untyped). + +## Substitution + +*((( rewrite examples with `not` )))* + +The heart of lambda calculus is the operation of +substituting one term for a variable in another term. +Substitution plays a key role in defining the +operational semantics of function application. +For instance, we have + + (ƛ "f" ⇒ # "f" · (# "f" · true)) · not + ⟹ + not · (not · true) + +where we substitute `not` for `` `f `` in the body +of the function abstraction. + +We write substitution as `N [ x := V ]`, meaning +"substitute term `V` for free occurrences of variable `x` in term `N`", +or, more compactly, "substitute `V` for `x` in `N`". +Substitution works if `V` is any closed term; +it need not be a value, but we use `V` since we +always substitute values. + +Here are some examples. + +* `` # "f" [ "f" := not ] `` yields `` not `` +* `` true [ "f" := not ] `` yields `` true `` +* `` (# "f" · true) [ "f" := not ] `` yields `` not · true `` +* `` (# "f" · (# "f" · true)) [ "f" := not ] `` yields `` not · (not · true) `` +* `` (ƛ "x" ⇒ # "f" · (# "f" · # "x")) [ "f" := not ] `` yields `` ƛ "x" ⇒ not · (not · # "x") `` +* `` (ƛ "y" ⇒ # "y") [ "x" := true ] `` yields `` ƛ "y" ⇒ # "y" `` +* `` (ƛ "x" ⇒ # "x") [ "x" := true ] `` yields `` ƛ "x" ⇒ # "x" `` + +The last example is important: substituting `true` for `x` in +`` ƛ "x" ⇒ # "x" `` does _not_ yield `` ƛ "x" ⇒ true ``. +The reason for this is that `x` in the body of `` ƛ "x" ⇒ # "x" `` +is _bound_ by the abstraction. An important feature of abstraction +is that the choice of bound names is irrelevant: both +`` ƛ "x" ⇒ # "x" `` and `` ƛ "y" ⇒ # "y" `` stand for the +identity function. The way to think of this is that `x` within +the body of the abstraction stands for a _different_ variable than +`x` outside the abstraction, they both just happen to have the same +name. + +Here is the formal definition in Agda. + +\begin{code} +infix 9 _[_:=_] + +_[_:=_] : Term → Id → Term → Term +(# x) [ y := V ] with x ≟ y +... | yes _ = V +... | no _ = # x +(ƛ x ⇒ N) [ y := V ] with x ≟ y +... | yes _ = ƛ x ⇒ N +... | no _ = ƛ x ⇒ N [ y := V ] +(L · M) [ y := V ] = L [ y := V ] · M [ y := V ] +(`zero) [ y := V ] = `zero +(`suc M) [ y := V ] = `suc M [ y := V ] +(`case L [zero⇒ M |suc x ⇒ N ]) [ y := V ] with x ≟ y +... | yes _ = `case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N ] +... | no _ = `case L [ y := V ] [zero⇒ M [ y := V ] |suc x ⇒ N [ y := V ] ] +(μ x ⇒ N) [ y := V ] with x ≟ y +... | yes _ = μ x ⇒ N +... | no _ = μ x ⇒ N [ y := V ] +\end{code} + +*((( add material about binding in case and μ )))* + +The two key cases are variables and abstraction. + +* For variables, we compare `w`, the variable we are substituting for, +with `x`, the variable in the term. If they are the same, +we yield `V`, otherwise we yield `x` unchanged. + +* For abstractions, we compare `w`, the variable we are substituting for, +with `x`, the variable bound in the abstraction. If they are the same, +we yield the abstraction unchanged, otherwise we subsititute inside the body. + +In all other cases, we push substitution recursively into +the subterms. + + + +#### Examples + +Here is confirmation that the examples above are correct. + +\begin{code} +_ : (# "s" · # "s" · # "z") [ "z" := `zero ] ≡ # "s" · # "s" · `zero +_ = refl + +_ : `zero [ "m" := `zero ] ≡ `zero +_ = refl + +_ : (`suc `suc # "n") [ "n" := `suc `suc `zero ] ≡ `suc `suc `suc `suc `zero +_ = refl + +_ : (ƛ "x" ⇒ # "x") [ "x" := `zero ] ≡ ƛ "x" ⇒ # "x" +_ = refl + +_ : (ƛ "x" ⇒ # "y") [ "y" := `zero ] ≡ ƛ "x" ⇒ `zero +_ = refl + +_ : (ƛ "y" ⇒ # "y") [ "x" := `zero ] ≡ ƛ "y" ⇒ # "y" +_ = refl +\end{code} + +#### Quiz + +What is the result of the following substitution? + + (ƛ "y" ⇒ # "x" · (ƛ "x" ⇒ # "x")) [ "x" := true ] + +1. `` (ƛ "y" ⇒ # "x" · (ƛ "x" ⇒ # "x")) `` +2. `` (ƛ "y" ⇒ # "x" · (ƛ "x" ⇒ true)) `` +3. `` (ƛ "y" ⇒ true · (ƛ "x" ⇒ # "x")) `` +4. `` (ƛ "y" ⇒ true · (ƛ "x" ⇒ true)) `` + + +## Reduction + +We give the reduction rules for call-by-value lambda calculus. To +reduce an application, first we reduce the left-hand side until it +becomes a value (which must be an abstraction); then we reduce the +right-hand side until it becomes a value; and finally we substitute +the argument for the variable in the abstraction. To reduce a +conditional, we first reduce the condition until it becomes a value; +if the condition is true the conditional reduces to the first +branch and if false it reduces to the second branch. + +In an informal presentation of the formal semantics, +the rules for reduction are written as follows. + + L ⟹ L′ + --------------- ξ·₁ + L · M ⟹ L′ · M + + M ⟹ M′ + --------------- ξ·₂ + V · M ⟹ V · M′ + + --------------------------------- βλ· + (ƛ x ⇒ N) · V ⟹ N [ x := V ] + + L ⟹ L′ + ----------------------------------------- ξif + if L then M else N ⟹ if L′ then M else N + + -------------------------- βif-true + if true then M else N ⟹ M + + --------------------------- βif-false + if false then M else N ⟹ N + +As we will show later, the rules are deterministic, in that +at most one rule applies to every term. As we will also show +later, for every well-typed term either a reduction applies +or it is a value. + +The rules break into two sorts. Compatibility rules +direct us to reduce some part of a term. +We give them names starting with the Greek letter xi, `ξ`. +Once a term is sufficiently +reduced, it will consist of a constructor and +a deconstructor, in our case `λ` and `·`, or +`if` and `true`, or `if` and `false`. +We give them names starting with the Greek letter beta, `β`, +and indeed such rules are traditionally called beta rules. + +Here are the above rules formalised in Agda. + +\begin{code} +infix 4 _⟹_ + +data _⟹_ : Term → Term → Set where + + ξ·₁ : ∀ {L L′ M} + → L ⟹ L′ + ----------------- + → L · M ⟹ L′ · M + + ξ·₂ : ∀ {V M M′} + → Value V + → M ⟹ M′ + ----------------- + → V · M ⟹ V · M′ + + βλ· : ∀ {x N V} + → Value V + ------------------------------ + → (ƛ x ⇒ N) · V ⟹ N [ x := V ] + + ξsuc : ∀ {M M′} + → M ⟹ M′ + ------------------ + → `suc M ⟹ `suc M′ + + ξcase : ∀ {x L L′ M N} + → L ⟹ L′ + ----------------------------------------------------------------- + → `case L [zero⇒ M |suc x ⇒ N ] ⟹ `case L′ [zero⇒ M |suc x ⇒ N ] + + βcase-zero : ∀ {x M N} + ---------------------------------------- + → `case `zero [zero⇒ M |suc x ⇒ N ] ⟹ M + + βcase-suc : ∀ {x V M N} + → Value V + --------------------------------------------------- + → `case `suc V [zero⇒ M |suc x ⇒ N ] ⟹ N [ x := V ] + + βμ : ∀ {x M} + ------------------------------ + → μ x ⇒ M ⟹ M [ x := μ x ⇒ M ] +{- +\end{code} + +*(((CONTINUE FROM HERE)))* + + +#### Quiz + +What does the following term step to? + + (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ⟹ ??? + +1. `` (ƛ "x" ⇒ # "x") `` +2. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") `` +3. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") `` + +What does the following term step to? + + (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") ⟹ ??? + +1. `` (ƛ "x" ⇒ # "x") `` +2. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") `` +3. `` (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") · (ƛ "x" ⇒ # "x") `` + +What does the following term step to? (Where `not` is as defined above.) + + not · true ⟹ ??? + +1. `` if # "x" then false else true `` +2. `` if true then false else true `` +3. `` true `` +4. `` false `` + +What does the following term step to? (Where `two` and `not` are as defined above.) + + two · not · true ⟹ ??? + +1. `` not · (not · true) `` +2. `` (ƛ "x" ⇒ not · (not · # "x")) · true `` +3. `` true `` +4. `` false `` + +## Reflexive and transitive closure + +A single step is only part of the story. In general, we wish to repeatedly +step a closed term until it reduces to a value. We do this by defining +the reflexive and transitive closure `⟹*` of the step function `⟹`. +In an informal presentation of the formal semantics, the rules +are written as follows. + + ------- done + M ⟹* M + + L ⟹ M + M ⟹* N + ------- step + L ⟹* N + +Here it is formalised in Agda, along similar lines to what +we used for reasoning about [Equality](Equality). + +\begin{code} +infix 2 _⟹*_ +infix 1 begin_ +infixr 2 _⟹⟨_⟩_ +infix 3 _∎ + +data _⟹*_ : Term → Term → Set where + _∎ : ∀ M + --------- + → M ⟹* M + + _⟹⟨_⟩_ : ∀ L {M N} + → L ⟹ M + → M ⟹* N + --------- + → L ⟹* N + +begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N) +begin M⟹*N = M⟹*N +\end{code} + +We can read this as follows. + +* From term `M`, we can take no steps, giving `M ∎` of type `M ⟹* M`. + +* From term `L` we can take a single step `L⟹M` of type `L ⟹ M` + followed by zero or more steps `M⟹*N` of type `M ⟹* N`, + giving `L ⟨ L⟹M ⟩ M⟹*N` of type `L ⟹* N`. + +The names have been chosen to allow us to lay +out example reductions in an appealing way. + +\begin{code} +_ : not · true ⟹* false +_ = + begin + not · true + ⟹⟨ βλ· value-true ⟩ + if true then false else true + ⟹⟨ βif-true ⟩ + false + ∎ + +_ : two · not · true ⟹* true +_ = + begin + two · not · true + ⟹⟨ ξ·₁ (βλ· value-λ) ⟩ + (ƛ "x" ⇒ not · (not · # "x")) · true + ⟹⟨ βλ· value-true ⟩ + not · (not · true) + ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩ + not · (if true then false else true) + ⟹⟨ ξ·₂ value-λ βif-true ⟩ + not · false + ⟹⟨ βλ· value-false ⟩ + if false then false else true + ⟹⟨ βif-false ⟩ + true + ∎ +\end{code} + +Much of the above, though not all, can be filled in using C-c C-r and C-c C-s. + + +## Syntax of types + +We have just two types. + + * Functions, `A ⇒ B` + * Natural, `` `ℕ `` + +We require some form of base type, because otherwise the set of types +would be empty. The obvious names to use in our object calculus +would be `A → B` for functions +and `ℕ` for naturals, + +We cannot use the name `ℕ` for the type of naturals in +our object calculus, because naturals already have that name in Agda, +so we use the name `` `ℕ `` instead. + +Here is the syntax of types in BNF. + + A, B, C ::= A ⇒ B | `ℕ + +And here it is formalised in Agda. + +\begin{code} +infixr 20 _⇒_ + +data Type : Set where + _⇒_ : Type → Type → Type + `ℕ : Type +\end{code} + +### Precedence + +As in Agda, functions of two or more arguments are represented via +currying. This is made more convenient by declaring `_⇒_` to +associate to the right and `_·_` to associate to the left. +Thus, + +* `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)` +* `two · not · true` abbreviates `(two · not) · true`. + +We choose the binding strength for abstractions and conditionals +to be weaker than application. For instance, + +* `` ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") `` + - denotes `` (ƛ "f" ⇒ (ƛ "x" ⇒ (# "f" · (# "f" · # "x")))) `` + - and not `` (ƛ "f" ⇒ (ƛ "x" ⇒ # "f")) · (# "f" · # "x") `` + +\begin{code} +_ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹) +_ = refl + +_ : two · not · true ≡ (two · not) · true +_ = refl + +_ : ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") + ≡ (ƛ "f" ⇒ (ƛ "x" ⇒ (# "f" · (# "f" · # "x")))) +_ = refl +\end{code} + +### Quiz + +* What is the type of the following term? + + ƛ "f" ⇒ # "f" · (# "f" · true) + + 1. `𝔹 ⇒ (𝔹 ⇒ 𝔹)` + 2. `(𝔹 ⇒ 𝔹) ⇒ 𝔹` + 3. `𝔹 ⇒ 𝔹 ⇒ 𝔹` + 4. `𝔹 ⇒ 𝔹` + 5. `𝔹` + + Give more than one answer if appropriate. + +* What is the type of the following term? + + (ƛ "f" ⇒ # "f" · (# "f" · true)) · not + + 1. `𝔹 ⇒ (𝔹 ⇒ 𝔹)` + 2. `(𝔹 ⇒ 𝔹) ⇒ 𝔹` + 3. `𝔹 ⇒ 𝔹 ⇒ 𝔹` + 4. `𝔹 ⇒ 𝔹` + 5. `𝔹` + + Give more than one answer if appropriate. + + + +## Typing + +While reduction considers only closed terms, typing must +consider terms with free variables. To type a term, +we must first type its subterms, and in particular in the +body of an abstraction its bound variable may appear free. + +In general, we use typing _judgements_ of the form + + Γ ⊢ M ⦂ A + +to assert in type environment `Γ` that term `M` has type `A`. +Environment `Γ` provides types for all the free variables in `M`. + +Here are three examples. + +* `` ∅ , "f" ⦂ 𝔹 ⇒ 𝔹 , "x" ⦂ 𝔹 ⊢ # "f" · (# "f" · # "x") ⦂ 𝔹 `` +* `` ∅ , "f" ⦂ 𝔹 ⇒ 𝔹 ⊢ (ƛ "x" ⇒ # "f" · (# "f" · # "x")) ⦂ 𝔹 ⇒ 𝔹 `` +* `` ∅ ⊢ ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x")) ⦂ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 `` + +Environments are partial maps from identifiers to types, built using `∅` +for the empty map, and `Γ , x ⦂ A` for the map that extends +environment `Γ` by mapping variable `x` to type `A`. + +*It's redundant to have two versions of the rules* + +*Need text to explain `Γ ∋ x ⦂ A`* + +In an informal presentation of the formal semantics, +the rules for typing are written as follows. + + Γ x ≡ A + ----------- Ax + Γ ⊢ ` x ⦂ A + + Γ , x ⦂ A ⊢ N ⦂ B + ------------------------ ⇒-I + Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B + + Γ ⊢ L ⦂ A ⇒ B + Γ ⊢ M ⦂ A + -------------- ⇒-E + Γ ⊢ L · M ⦂ B + + ------------- 𝔹-I₁ + Γ ⊢ true ⦂ 𝔹 + + -------------- 𝔹-I₂ + Γ ⊢ false ⦂ 𝔹 + + Γ ⊢ L : 𝔹 + Γ ⊢ M ⦂ A + Γ ⊢ N ⦂ A + -------------------------- 𝔹-E + Γ ⊢ if L then M else N ⦂ A + +As we will show later, the rules are deterministic, in that +at most one rule applies to every term. + +The proof rules come in pairs, with rules to introduce and to +eliminate each connective, labeled `-I` and `-E`, respectively. As we +read the rules from top to bottom, introduction and elimination rules +do what they say on the tin: the first _introduces_ a formula for the +connective, which appears in the conclusion but not in the premises; +while the second _eliminates_ a formula for the connective, which appears in +a premise but not in the conclusion. An introduction rule describes +how to construct a value of the type (abstractions yield functions, +true and false yield booleans), while an elimination rule describes +how to deconstruct a value of the given type (applications use +functions, conditionals use booleans). + +Here are the above rules formalised in Agda. + +\begin{code} +infix 4 _∋_⦂_ +infix 4 _⊢_⦂_ +infixl 5 _,_⦂_ + +data Context : Set where + ∅ : Context + _,_⦂_ : Context → Id → Type → Context + +data _∋_⦂_ : Context → Id → Type → Set where + + Z : ∀ {Γ x A} + ------------------ + → Γ , x ⦂ A ∋ x ⦂ A + + S : ∀ {Γ x y A B} + → x ≢ y + → Γ ∋ x ⦂ A + ------------------ + → Γ , y ⦂ B ∋ x ⦂ A + +data _⊢_⦂_ : Context → Term → Type → Set where + + Ax : ∀ {Γ x A} + → Γ ∋ x ⦂ A + ------------- + → Γ ⊢ # x ⦂ A + + ⇒-I : ∀ {Γ x N A B} + → Γ , x ⦂ A ⊢ N ⦂ B + -------------------- + → Γ ⊢ ƛ x ⇒ N ⦂ A ⇒ B + + ⇒-E : ∀ {Γ L M A B} + → Γ ⊢ L ⦂ A ⇒ B + → Γ ⊢ M ⦂ A + -------------- + → Γ ⊢ L · M ⦂ B + + 𝔹-I₁ : ∀ {Γ} + ------------- + → Γ ⊢ true ⦂ 𝔹 + + 𝔹-I₂ : ∀ {Γ} + -------------- + → Γ ⊢ false ⦂ 𝔹 + + 𝔹-E : ∀ {Γ L M N A} + → Γ ⊢ L ⦂ 𝔹 + → Γ ⊢ M ⦂ A + → Γ ⊢ N ⦂ A + --------------------------- + → Γ ⊢ if L then M else N ⦂ A +\end{code} + +### Example type derivations + +Here are a couple of typing examples. First, here is how +they would be written in an informal description of the +formal semantics. + +Derivation of `not`: + + ------------ Z + Γ₀ ∋ "x" ⦂ B + -------------- Ax -------------- 𝔹-I₂ ------------- 𝔹-I₁ + Γ₀ ⊢ # "x" ⦂ 𝔹 Γ₀ ⊢ false ⦂ 𝔹 Γ₀ ⊢ true ⦂ 𝔹 + ------------------------------------------------------ 𝔹-E + Γ₀ ⊢ if # "x" then false else true ⦂ 𝔹 + --------------------------------------------------- ⇒-I + ∅ ⊢ ƛ "x" ⇒ if # "x" then false else true ⦂ 𝔹 ⇒ 𝔹 + +where `Γ₀ = ∅ , x ⦂ 𝔹`. + +Derivation of `two`: + + ∋f ∋f ∋x + ------------------- Ax ------------------- Ax --------------- Ax + Γ₂ ⊢ # "f" ⦂ 𝔹 ⇒ 𝔹 Γ₂ ⊢ # "f" ⦂ 𝔹 ⇒ 𝔹 Γ₂ ⊢ # "x" ⦂ 𝔹 + ------------------- Ax ------------------------------------------ ⇒-E + Γ₂ ⊢ # "f" ⦂ 𝔹 ⇒ 𝔹 Γ₂ ⊢ # "f" · # "x" ⦂ 𝔹 + -------------------------------------------------- ⇒-E + Γ₂ ⊢ # "f" · (# "f" · # "x") ⦂ 𝔹 + ---------------------------------------------- ⇒-I + Γ₁ ⊢ ƛ "x" ⇒ # "f" · (# "f" · # "x") ⦂ 𝔹 ⇒ 𝔹 + ---------------------------------------------------------- ⇒-I + ∅ ⊢ ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") ⦂ 𝔹 ⇒ 𝔹 + +Where `∋f` and `∋x` abbreviate the two derivations: + + + ---------------- Z + "x" ≢ "f" Γ₁ ∋ "f" ⦂ B ⇒ B + ----------------------------- S ------------- Z + Γ₂ ∋ "f" ⦂ B ⇒ B Γ₂ ∋ "x" ⦂ 𝔹 + +where `Γ₁ = ∅ , f ⦂ 𝔹 ⇒ 𝔹` and `Γ₂ = ∅ , f ⦂ 𝔹 ⇒ 𝔹 , x ⦂ 𝔹`. + +Here are the above derivations formalised in Agda. + +\begin{code} +⊢not : ∅ ⊢ not ⦂ 𝔹 ⇒ 𝔹 +⊢not = ⇒-I (𝔹-E (Ax Z) 𝔹-I₂ 𝔹-I₁) + +⊢two : ∅ ⊢ two ⦂ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 +⊢two = ⇒-I (⇒-I (⇒-E (Ax ⊢f) (⇒-E (Ax ⊢f) (Ax ⊢x)))) + where + + f≢x : "f" ≢ "x" + f≢x () + + ⊢f = S f≢x Z + ⊢x = Z +\end{code} + +#### Interaction with Agda + +Construction of a type derivation is best done interactively. +Start with the declaration: + + ⊢not : ∅ ⊢ not ⦂ 𝔹 ⇒ 𝔹 + ⊢not = ? + +Typing C-l causes Agda to create a hole and tell us its expected type. + + ⊢not = { }0 + ?0 : ∅ ⊢ not ⦂ 𝔹 ⇒ 𝔹 + +Now we fill in the hole by typing C-c C-r. Agda observes that +the outermost term in `not` in a `λ`, which is typed using `⇒-I`. The +`⇒-I` rule in turn takes one argument, which Agda leaves as a hole. + + ⊢not = ⇒-I { }0 + ?0 : ∅ , x ⦂ 𝔹 ⊢ if ` x then false else true ⦂ 𝔹 + +Again we fill in the hole by typing C-c C-r. Agda observes that the +outermost term is now `if_then_else_`, which is typed using `𝔹-E`. The +`𝔹-E` rule in turn takes three arguments, which Agda leaves as holes. + + ⊢not = ⇒-I (𝔹-E { }0 { }1 { }2) + ?0 : ∅ , x ⦂ 𝔹 ⊢ ` x ⦂ + ?1 : ∅ , x ⦂ 𝔹 ⊢ false ⦂ 𝔹 + ?2 : ∅ , x ⦂ 𝔹 ⊢ true ⦂ 𝔹 + +Again we fill in the three holes by typing C-c C-r in each. Agda observes +that `` ` x ``, `false`, and `true` are typed using `Ax`, `𝔹-I₂`, and +`𝔹-I₁` respectively. The `Ax` rule in turn takes an argument, to show +that `(∅ , x ⦂ 𝔹) x = just 𝔹`, which can in turn be specified with a +hole. After filling in all holes, the term is as above. + +The entire process can be automated using Agsy, invoked with C-c C-a. + +### Injective + +Note that `Γ ∋ x ⦂ A` is injective. +\begin{code} +∋-injective : ∀ {Γ w A B} → Γ ∋ w ⦂ A → Γ ∋ w ⦂ B → A ≡ B +∋-injective Z Z = refl +∋-injective Z (S w≢ _) = ⊥-elim (w≢ refl) +∋-injective (S w≢ _) Z = ⊥-elim (w≢ refl) +∋-injective (S _ ∋w) (S _ ∋w′) = ∋-injective ∋w ∋w′ +\end{code} + +The relation `Γ ⊢ M ⦂ A` is not injective. For example, in any `Γ` +the term `ƛ "x" ⇒ "x"` has type `A ⇒ A` for any type `A`. + +### Non-examples + +We can also show that terms are _not_ typeable. For example, here is +a formal proof that it is not possible to type the term `` true · +false ``. In other words, no type `A` is the type of this term. It +cannot be typed, because doing so requires that the first term in the +application is both a boolean and a function. + +\begin{code} +ex₁ : ∀ {A} → ¬ (∅ ⊢ true · false ⦂ A) +ex₁ (⇒-E () _) +\end{code} + +As a second example, here is a formal proof that it is not possible to +type `` ƛ "x" ⇒ # "x" · # "x" `` It cannot be typed, because +doing so requires some types `A` and `B` such that `A ⇒ B ≡ A`. + +\begin{code} +contradiction : ∀ {A B} → ¬ (A ⇒ B ≡ A) +contradiction () + +ex₂ : ∀ {A} → ¬ (∅ ⊢ ƛ "x" ⇒ # "x" · # "x" ⦂ A) +ex₂ (⇒-I (⇒-E (Ax ∋x) (Ax ∋x′))) = contradiction (∋-injective ∋x ∋x′) +\end{code} + + +#### Quiz + +For each of the following, given a type `A` for which it is derivable, +or explain why there is no such `A`. + +1. `` ∅ , y ⦂ A ⊢ λ[ x ⦂ 𝔹 ] ` x ⦂ 𝔹 ⇒ 𝔹 `` +2. `` ∅ ⊢ λ[ y ⦂ 𝔹 ⇒ 𝔹 ] λ[ x ⦂ 𝔹 ] ` y · ` x ⦂ A `` +3. `` ∅ ⊢ λ[ y ⦂ 𝔹 ⇒ 𝔹 ] λ[ x ⦂ 𝔹 ] ` x · ` y ⦂ A `` +4. `` ∅ , x ⦂ A ⊢ λ[ y : 𝔹 ⇒ 𝔹 ] `y · `x : A `` + +For each of the following, give type `A`, `B`, `C`, and `D` for which it is derivable, +or explain why there are no such types. + +1. `` ∅ ⊢ λ[ y ⦂ 𝔹 ⇒ 𝔹 ⇒ 𝔹 ] λ[ x ⦂ 𝔹 ] ` y · ` x ⦂ A `` +2. `` ∅ , x ⦂ A ⊢ x · x ⦂ B `` +3. `` ∅ , x ⦂ A , y ⦂ B ⊢ λ[ z ⦂ C ] ` x · (` y · ` z) ⦂ D `` + + + +## Unicode + +This chapter uses the following unicode + + ⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>) + ƛ U+019B: LATIN SMALL LETTER LAMBDA WITH STROKE (\Gl-) + ⦂ U+2982: Z NOTATION TYPE COLON (\:) + · U+00B7: MIDDLE DOT (\cdot) + 😇 U+1F607: SMILING FACE WITH HALO + 😈 U+1F608: SMILING FACE WITH HORNS + ′ U+2032: PRIME (\') + ⟹ U+27F9: LONG RIGHTWARDS DOUBLE ARROW (\r6) + ξ U+03BE: GREEK SMALL LETTER XI (\Gx or \xi) + β U+03B2: GREEK SMALL LETTER BETA (\Gb or \beta) + +Note that ′ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE). + +\begin{code} +-} +\end{code} diff --git a/src/LambdaProp.lagda b/src/LambdaProp.lagda new file mode 100644 index 00000000..009f2ceb --- /dev/null +++ b/src/LambdaProp.lagda @@ -0,0 +1,662 @@ +--- +title : "LambdaProp: Properties of Simply-Typed Lambda Calculus" +layout : page +permalink : /LambdaProp +--- + +This chapter develops the fundamental theory of the Simply +Typed Lambda Calculus, particularly progress and preservation. + +## Imports + +\begin{code} +module LambdaProp where + +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) +open import Data.String using (String; _≟_) +open import Data.Empty using (⊥; ⊥-elim) +open import Data.Product + using (_×_; proj₁; proj₂; ∃; ∃-syntax) + renaming (_,_ to ⟨_,_⟩) +open import Data.Sum using (_⊎_; inj₁; inj₂) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Function using (_∘_) +open import StlcNew +\end{code} + + +## Canonical Forms + +The first step in establishing basic properties of reduction and typing +is to identify the possible _canonical forms_ (i.e., well-typed closed values) +belonging to each type. For function types the canonical forms are lambda-abstractions, +while for boolean types they are values `true` and `false`. + +\begin{code} +data canonical_for_ : Term → Type → Set where + canonical-λ : ∀ {x A N B} → canonical (ƛ x ⇒ N) for (A ⇒ B) + canonical-true : canonical true for 𝔹 + canonical-false : canonical false for 𝔹 + +canonical-forms : ∀ {L A} → ∅ ⊢ L ⦂ A → Value L → canonical L for A +canonical-forms (Ax ()) () +canonical-forms (⇒-I ⊢N) value-λ = canonical-λ +canonical-forms (⇒-E ⊢L ⊢M) () +canonical-forms 𝔹-I₁ value-true = canonical-true +canonical-forms 𝔹-I₂ value-false = canonical-false +canonical-forms (𝔹-E ⊢L ⊢M ⊢N) () +\end{code} + +## Progress + +As before, the _progress_ theorem tells us that closed, well-typed +terms are not stuck: either a well-typed term can take a reduction +step or it is a value. + +\begin{code} +data Progress (M : Term) : Set where + steps : ∀ {N} → M ⟹ N → Progress M + done : Value M → Progress M + +progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M +\end{code} + +We give the proof in English first, then the formal version. + +_Proof_: By induction on the derivation of `∅ ⊢ M ⦂ A`. + + - The last rule of the derivation cannot be `Ax`, + since a variable is never well typed in an empty context. + + - If the last rule of the derivation is `⇒-I`, `𝔹-I₁`, or `𝔹-I₂` + then, trivially, the term is a value. + + - If the last rule of the derivation is `⇒-E`, then the term has the + form `L · M` for some `L` and `M`, where we know that `L` and `M` + are also well typed in the empty context, giving us two induction + hypotheses. By the first induction hypothesis, either `L` + can take a step or is a value. + + - If `L` can take a step, then so can `L · M` by `ξ·₁`. + + - If `L` is a value then consider `M`. By the second induction + hypothesis, either `M` can take a step or is a value. + + - If `M` can take a step, then so can `L · M` by `ξ·₂`. + + - If `M` is a value, then since `L` is a value with a + function type we know from the canonical forms lemma + that it must be a lambda abstraction, + and hence `L · M` can take a step by `βλ·`. + + - If the last rule of the derivation is `𝔹-E`, then the term has + the form `if L then M else N` where `L` has type `𝔹`. + By the induction hypothesis, either `L` can take a step or is + a value. + + - If `L` can take a step, then so can `if L then M else N` by `ξif`. + + - If `L` is a value, then since it has type boolean we know from + the canonical forms lemma that it must be either `true` or + `false`. + + - If `L` is `true`, then `if L then M else N` steps by `βif-true` + + - If `L` is `false`, then `if L then M else N` steps by `βif-false` + +This completes the proof. + +\begin{code} +progress (Ax ()) +progress (⇒-I ⊢N) = done value-λ +progress (⇒-E ⊢L ⊢M) with progress ⊢L +... | steps L⟹L′ = steps (ξ·₁ L⟹L′) +... | done valueL with progress ⊢M +... | steps M⟹M′ = steps (ξ·₂ valueL M⟹M′) +... | done valueM with canonical-forms ⊢L valueL +... | canonical-λ = steps (βλ· valueM) +progress 𝔹-I₁ = done value-true +progress 𝔹-I₂ = done value-false +progress (𝔹-E ⊢L ⊢M ⊢N) with progress ⊢L +... | steps L⟹L′ = steps (ξif L⟹L′) +... | done valueL with canonical-forms ⊢L valueL +... | canonical-true = steps βif-true +... | canonical-false = steps βif-false +\end{code} + +This code reads neatly in part because we consider the +`steps` option before the `done` option. We could, of course, +do it the other way around, but then the `...` abbreviation +no longer works, and we will need to write out all the arguments +in full. In general, the rule of thumb is to consider the easy case +(here `steps`) before the hard case (here `done`). +If you have two hard cases, you will have to expand out `...` +or introduce subsidiary functions. + +#### Exercise: 3 stars, optional (progress_from_term_ind) +Show that progress can also be proved by induction on terms +instead of induction on typing derivations. + +\begin{code} +postulate + progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Progress M +\end{code} + +## Preservation + +The other half of the type soundness property is the preservation +of types during reduction. For this, we need to develop +technical machinery for reasoning about variables and +substitution. Working from top to bottom (from the high-level +property we are actually interested in to the lowest-level +technical lemmas), the story goes like this: + + - The _preservation theorem_ is proved by induction on a typing derivation. + derivation, pretty much as we did in chapter [Types]({{ "Types" | relative_url }}) + + - The one case that is significantly different is the one for the + `βλ·` rule, whose definition uses the substitution operation. To see that + this step preserves typing, we need to know that the substitution itself + does. So we prove a ... + + - _substitution lemma_, stating that substituting a (closed) term + `V` for a variable `x` in a term `N` preserves the type of `N`. + The proof goes by induction on the form of `N` and requires + looking at all the different cases in the definition of + substitition. The lemma does not require that `V` be a value, + though in practice we only substitute values. The tricky cases + are the ones for variables and for function abstractions. In both + cases, we discover that we need to take a term `V` that has been + shown to be well-typed in some context `Γ` and consider the same + term in a different context `Γ′`. For this we prove a ... + + - _context invariance_ lemma, showing that typing is preserved + under "inessential changes" to the context---a term `M` + well typed in `Γ` is also well typed in `Γ′`, so long as + all the free variables of `M` appear in both contexts. + And finally, for this, we need a careful definition of ... + + - _free variables_ of a term---i.e., those variables + mentioned in a term and not bound in an enclosing + lambda abstraction. + +To make Agda happy, we need to formalize the story in the opposite +order. + + +### Free Occurrences + +A variable `x` appears _free_ in a term `M` if `M` contains an +occurrence of `x` that is not bound in an enclosing lambda abstraction. +For example: + + - Variable `x` appears free, but `f` does not, in ``ƛ "f" ⇒ # "f" · # "x"``. + - Both `f` and `x` appear free in ``(ƛ "f" ⇒ # "f" · # "x") · # "f"``. + Indeed, `f` appears both bound and free in this term. + - No variables appear free in ``ƛ "f" ⇒ ƛ "x" ⇒ # "f" · # "x"``. + +Formally: + +\begin{code} +data _∈_ : Id → Term → Set where + free-# : ∀ {x} → x ∈ # x + free-ƛ : ∀ {w x N} → w ≢ x → w ∈ N → w ∈ (ƛ x ⇒ N) + free-·₁ : ∀ {w L M} → w ∈ L → w ∈ (L · M) + free-·₂ : ∀ {w L M} → w ∈ M → w ∈ (L · M) + free-if₁ : ∀ {w L M N} → w ∈ L → w ∈ (if L then M else N) + free-if₂ : ∀ {w L M N} → w ∈ M → w ∈ (if L then M else N) + free-if₃ : ∀ {w L M N} → w ∈ N → w ∈ (if L then M else N) +\end{code} + +A term in which no variables appear free is said to be _closed_. + +\begin{code} +_∉_ : Id → Term → Set +x ∉ M = ¬ (x ∈ M) + +closed : Term → Set +closed M = ∀ {x} → x ∉ M +\end{code} + +Here are proofs corresponding to the first two examples above. + +\begin{code} +x≢f : "x" ≢ "f" +x≢f () + +ex₃ : "x" ∈ (ƛ "f" ⇒ # "f" · # "x") +ex₃ = free-ƛ x≢f (free-·₂ free-#) + +ex₄ : "f" ∉ (ƛ "f" ⇒ # "f" · # "x") +ex₄ (free-ƛ f≢f _) = f≢f refl +\end{code} + + +#### Exercise: 1 star (free-in) +Prove formally the remaining examples given above. + +\begin{code} +postulate + ex₅ : "x" ∈ ((ƛ "f" ⇒ # "f" · # "x") · # "f") + ex₆ : "f" ∈ ((ƛ "f" ⇒ # "f" · # "x") · # "f") + ex₇ : "x" ∉ (ƛ "f" ⇒ ƛ "x" ⇒ # "f" · # "x") + ex₈ : "f" ∉ (ƛ "f" ⇒ ƛ "x" ⇒ # "f" · # "x") +\end{code} + +Although `_∈_` may appear to be a low-level technical definition, +understanding it is crucial to understanding the properties of +substitution, which are really the crux of the lambda calculus. + +### Substitution + +To prove that substitution preserves typing, we first need a technical +lemma connecting free variables and typing contexts. If variable `x` +appears free in term `M`, and if `M` is well typed in context `Γ`, +then `Γ` must assign a type to `x`. + +\begin{code} +free-lemma : ∀ {w M A Γ} → w ∈ M → Γ ⊢ M ⦂ A → ∃[ B ](Γ ∋ w ⦂ B) +free-lemma free-# (Ax {Γ} {w} {B} ∋w) = ⟨ B , ∋w ⟩ +free-lemma (free-ƛ {w} {x} w≢ ∈N) (⇒-I ⊢N) with w ≟ x +... | yes refl = ⊥-elim (w≢ refl) +... | no _ with free-lemma ∈N ⊢N +... | ⟨ B , Z ⟩ = ⊥-elim (w≢ refl) +... | ⟨ B , S _ ∋w ⟩ = ⟨ B , ∋w ⟩ +free-lemma (free-·₁ ∈L) (⇒-E ⊢L ⊢M) = free-lemma ∈L ⊢L +free-lemma (free-·₂ ∈M) (⇒-E ⊢L ⊢M) = free-lemma ∈M ⊢M +free-lemma (free-if₁ ∈L) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma ∈L ⊢L +free-lemma (free-if₂ ∈M) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma ∈M ⊢M +free-lemma (free-if₃ ∈N) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma ∈N ⊢N +\end{code} + + + +As a second technical lemma, we need that any term `M` which is well +typed in the empty context is closed (has no free variables). + +#### Exercise: 2 stars, optional (∅⊢-closed) + +\begin{code} +postulate + ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ⦂ A → closed M +\end{code} + + + +Sometimes, when we have a proof `Γ ⊢ M ⦂ A`, we will need to +replace `Γ` by a different context `Γ′`. When is it safe +to do this? Intuitively, the only variables we care about +in the context are those that appear free in `M`. So long +as the two contexts agree on those variables, one can be +exchanged for the other. + +\begin{code} +ext : ∀ {Γ Δ} + → (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B) + ----------------------------------------------------- + → (∀ {w x A B} → Γ , x ⦂ A ∋ w ⦂ B → Δ , x ⦂ A ∋ w ⦂ B) +ext σ Z = Z +ext σ (S w≢ ∋w) = S w≢ (σ ∋w) + +rename : ∀ {Γ Δ} + → (∀ {w B} → Γ ∋ w ⦂ B → Δ ∋ w ⦂ B) + ---------------------------------- + → (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) +rename σ (Ax ∋w) = Ax (σ ∋w) +rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N) +rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M) +rename σ 𝔹-I₁ = 𝔹-I₁ +rename σ 𝔹-I₂ = 𝔹-I₂ +rename σ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (rename σ ⊢L) (rename σ ⊢M) (rename σ ⊢N) +\end{code} + +We have three important corrolaries. First, +any closed term can be weakened to any context. +\begin{code} +rename-∅ : ∀ {Γ M A} + → ∅ ⊢ M ⦂ A + ---------- + → Γ ⊢ M ⦂ A +rename-∅ {Γ} ⊢M = rename σ ⊢M + where + σ : ∀ {z C} + → ∅ ∋ z ⦂ C + --------- + → Γ ∋ z ⦂ C + σ () +\end{code} + +Second, if the last two variable in a context are +equal, the term can be renamed to drop the redundant one. +\begin{code} +rename-≡ : ∀ {Γ x M A B C} + → Γ , x ⦂ A , x ⦂ B ⊢ M ⦂ C + -------------------------- + → Γ , x ⦂ B ⊢ M ⦂ C +rename-≡ {Γ} {x} {M} {A} {B} {C} ⊢M = rename σ ⊢M + where + σ : ∀ {z C} + → Γ , x ⦂ A , x ⦂ B ∋ z ⦂ C + ------------------------- + → Γ , x ⦂ B ∋ z ⦂ C + σ Z = Z + σ (S z≢x Z) = ⊥-elim (z≢x refl) + σ (S z≢x (S z≢y ∋z)) = S z≢x ∋z +\end{code} + +Third, if the last two variable in a context differ, +the term can be renamed to flip their order. +\begin{code} +rename-≢ : ∀ {Γ x y M A B C} + → x ≢ y + → Γ , y ⦂ A , x ⦂ B ⊢ M ⦂ C + -------------------------- + → Γ , x ⦂ B , y ⦂ A ⊢ M ⦂ C +rename-≢ {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename σ ⊢M + where + σ : ∀ {z C} + → Γ , y ⦂ A , x ⦂ B ∋ z ⦂ C + -------------------------- + → Γ , x ⦂ B , y ⦂ A ∋ z ⦂ C + σ Z = S (λ{refl → x≢y refl}) Z + σ (S z≢x Z) = Z + σ (S z≢x (S z≢y ∋z)) = S z≢y (S z≢x ∋z) +\end{code} + + +Now we come to the conceptual heart of the proof that reduction +preserves types---namely, the observation that _substitution_ +preserves types. + +Formally, the _Substitution Lemma_ says this: Suppose we +have a term `N` with a free variable `x`, where `N` has +type `B` under the assumption that `x` has some type `A`. +Also, suppose that we have some other term `V`, +where `V` has type `A`. Then, since `V` satisfies +the assumption we made about `x` when typing `N`, we should be +able to substitute `V` for each of the occurrences of `x` in `N` +and obtain a new term that still has type `B`. + +_Lemma_: If `Γ , x ⦂ A ⊢ N ⦂ B` and `∅ ⊢ V ⦂ A`, then +`Γ ⊢ (N [ x := V ]) ⦂ B`. + +One technical subtlety in the statement of the lemma is that we assume +`V` is closed; it has type `A` in the _empty_ context. This +assumption simplifies the `λ` case of the proof because the context +invariance lemma then tells us that `V` has type `A` in any context at +all---we don't have to worry about free variables in `V` clashing with +the variable being introduced into the context by `λ`. It is possible +to prove the theorem under the more general assumption `Γ ⊢ V ⦂ A`, +but the proof is more difficult. + + + +\begin{code} +subst : ∀ {Γ x N V A B} + → Γ , x ⦂ A ⊢ N ⦂ B + → ∅ ⊢ V ⦂ A + ----------------------- + → Γ ⊢ N [ x := V ] ⦂ B + +subst {Γ} {y} {# x} (Ax Z) ⊢V with x ≟ y +... | yes refl = rename-∅ ⊢V +... | no x≢y = ⊥-elim (x≢y refl) +subst {Γ} {y} {# x} (Ax (S x≢y ∋x)) ⊢V with x ≟ y +... | yes refl = ⊥-elim (x≢y refl) +... | no _ = Ax ∋x +subst {Γ} {y} {ƛ x ⇒ N} (⇒-I ⊢N) ⊢V with x ≟ y +... | yes refl = ⇒-I (rename-≡ ⊢N) +... | no x≢y = ⇒-I (subst (rename-≢ x≢y ⊢N) ⊢V) +subst (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) +subst 𝔹-I₁ ⊢V = 𝔹-I₁ +subst 𝔹-I₂ ⊢V = 𝔹-I₂ +subst (𝔹-E ⊢L ⊢M ⊢N) ⊢V = 𝔹-E (subst ⊢L ⊢V) (subst ⊢M ⊢V) (subst ⊢N ⊢V) +\end{code} + + +### Main Theorem + +We now have the tools we need to prove preservation: if a closed +term `M` has type `A` and takes a step to `N`, then `N` +is also a closed term with type `A`. In other words, small-step +reduction preserves types. + +\begin{code} +preservation : ∀ {M N A} → ∅ ⊢ M ⦂ A → M ⟹ N → ∅ ⊢ N ⦂ A +preservation (Ax ()) +preservation (⇒-I ⊢N) () +preservation (⇒-E ⊢L ⊢M) (ξ·₁ L⟹L′) with preservation ⊢L L⟹L′ +... | ⊢L′ = ⇒-E ⊢L′ ⊢M +preservation (⇒-E ⊢L ⊢M) (ξ·₂ valueL M⟹M′) with preservation ⊢M M⟹M′ +... | ⊢M′ = ⇒-E ⊢L ⊢M′ +preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = subst ⊢N ⊢V +preservation 𝔹-I₁ () +preservation 𝔹-I₂ () +preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′ +... | ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N +preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-true = ⊢M +preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N +\end{code} + + +#### Exercise: 2 stars, recommended (subject_expansion_stlc) + + + +We say that `M` _reduces_ to `N` if `M ⟹ N`, +and that `M` _expands_ to `N` if `N ⟹ M`. +The preservation property is sometimes called _subject reduction_. +Its opposite is _subject expansion_, which holds if +`M ==> N` and `∅ ⊢ N ⦂ A`, then `∅ ⊢ M ⦂ A`. +Find two counter-examples to subject expansion, one +with conditionals and one not involving conditionals. + +## Type Soundness + +#### Exercise: 2 stars, optional (type_soundness) + +Put progress and preservation together and show that a well-typed +term can _never_ reach a stuck state. + +\begin{code} +Normal : Term → Set +Normal M = ∀ {N} → ¬ (M ⟹ N) + +Stuck : Term → Set +Stuck M = Normal M × ¬ Value M + +postulate + Soundness : ∀ {M N A} → ∅ ⊢ M ⦂ A → M ⟹* N → ¬ (Stuck N) +\end{code} + + + + +## Additional Exercises + +#### Exercise: 1 star (progress_preservation_statement) + +Without peeking at their statements above, write down the progress +and preservation theorems for the simply typed lambda-calculus. + +#### Exercise: 2 stars (stlc_variation1) + +Suppose we add a new term `zap` with the following reduction rule + + --------- (ST_Zap) + M ⟹ zap + +and the following typing rule: + + ----------- (T_Zap) + Γ ⊢ zap : A + +Which of the following properties of the STLC remain true in +the presence of these rules? For each property, write either +"remains true" or "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + + +#### Exercise: 2 stars (stlc_variation2) + +Suppose instead that we add a new term `foo` with the following +reduction rules: + + ------------------- (ST_Foo1) + (λ x ⇒ # x) ⟹ foo + + ------------ (ST_Foo2) + foo ⟹ true + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + +#### Exercise: 2 stars (stlc_variation3) + +Suppose instead that we remove the rule `ξ·₁` from the `⟹` +relation. Which of the following properties of the STLC remain +true in the absence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + +#### Exercise: 2 stars, optional (stlc_variation4) +Suppose instead that we add the following new rule to the +reduction relation: + + ---------------------------------- (ST_FunnyIfTrue) + (if true then t_1 else t_2) ⟹ true + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + + +#### Exercise: 2 stars, optional (stlc_variation5) + +Suppose instead that we add the following new rule to the typing +relation: + + Γ ⊢ L ⦂ 𝔹 ⇒ 𝔹 ⇒ 𝔹 + Γ ⊢ M ⦂ 𝔹 + ------------------------------ (T_FunnyApp) + Γ ⊢ L · M ⦂ 𝔹 + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + + + +#### Exercise: 2 stars, optional (stlc_variation6) +Suppose instead that we add the following new rule to the typing +relation: + + Γ ⊢ L ⦂ 𝔹 + Γ ⊢ M ⦂ 𝔹 + --------------------- (T_FunnyApp') + Γ ⊢ L · M ⦂ 𝔹 + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + + + +#### Exercise: 2 stars, optional (stlc_variation7) + +Suppose we add the following new rule to the typing relation +of the STLC: + + -------------------- (T_FunnyAbs) + ∅ ⊢ λ[ x ⦂ 𝔹 ] N ⦂ 𝔹 + +Which of the following properties of the STLC remain true in +the presence of this rule? For each one, write either +"remains true" or else "becomes false." If a property becomes +false, give a counterexample. + + - Determinism of `step` + + - Progress + + - Preservation + +