diff --git a/out/Maps.md b/out/Maps.md deleted file mode 100644 index b03eabb4..00000000 --- a/out/Maps.md +++ /dev/null @@ -1,6329 +0,0 @@ ---- -title : "Maps: Total and Partial Maps" -layout : page -permalink : /Maps ---- - -Maps (or dictionaries) are ubiquitous data structures, both in software -construction generally and in the theory of programming languages in particular; -we're going to need them in many places in the coming chapters. They also make -a nice case study using ideas we've seen in previous chapters, including -building data structures out of higher-order functions (from [Basics]({{ -"Basics" | relative_url }}) and [Poly]({{ "Poly" | relative_url }}) and the use -of reflection to streamline proofs (from [IndProp]({{ "IndProp" | relative_url -}})). - -We'll define two flavors of maps: _total_ maps, which include a -"default" element to be returned when a key being looked up -doesn't exist, and _partial_ maps, which return an `Maybe` to -indicate success or failure. The latter is defined in terms of -the former, using `nothing` as the default element. - -## The Agda Standard Library - -One small digression before we start. - -Unlike the chapters we have seen so far, this one does not -import the chapter before it (and, transitively, all the -earlier chapters). Instead, in this chapter and from now, on -we're going to import the definitions and theorems we need -directly from Agda's standard library. You should not notice -much difference, though, because we've been careful to name our -own definitions and theorems the same as their counterparts in the -standard library, wherever they overlap. - -
{% raw %}
-open import Data.Nat         using (ℕ)
-open import Data.Empty       using (⊥; ⊥-elim)
-open import Data.Maybe       using (Maybe; just; nothing)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Binary.PropositionalEquality
-                             using (_≡_; refl; _≢_; trans; sym)
-{% endraw %}
- -Documentation for the standard library can be found at -. - -## Identifiers - -First, we need a type for the keys that we use to index into our -maps. For this purpose, we again use the type `Id` from the -[Lists](sf/Lists.html) chapter. To make this chapter self contained, -we repeat its definition here. - -
{% raw %}
-data Id : Set where
-  id : ℕ → Id
-{% endraw %}
- -We recall a standard fact of logic. - -
{% raw %}
-contrapositive : ∀ {ℓ₁ ℓ₂} {P : Set ℓ₁} {Q : Set ℓ₂} → (P → Q) → (¬ Q → ¬ P)
-contrapositive p→q ¬q p = ¬q (p→q p)
-{% endraw %}
- -Using the above, we can decide equality of two identifiers -by deciding equality on the underlying strings. - -
{% raw %}
-_≟_ : (x y : Id) → Dec (x ≡ y)
-id x ≟ id y with x Data.Nat.≟ y
-id x ≟ id y | yes refl  =  yes refl
-id x ≟ id y | no  x≢y   =  no (contrapositive id-inj x≢y)
-  where
-    id-inj : ∀ {x y} → id x ≡ id y → x ≡ y
-    id-inj refl  =  refl
-{% endraw %}
- -## Total Maps - -Our main job in this chapter will be to build a definition of -partial maps that is similar in behavior to the one we saw in the -[Lists](sf/Lists.html) chapter, plus accompanying lemmas about their -behavior. - -This time around, though, we're going to use _functions_, rather -than lists of key-value pairs, to build maps. The advantage of -this representation is that it offers a more _extensional_ view of -maps, where two maps that respond to queries in the same way will -be represented as literally the same thing (the same function), -rather than just "equivalent" data structures. This, in turn, -simplifies proofs that use maps. - -We build partial maps in two steps. First, we define a type of -_total maps_ that return a default value when we look up a key -that is not present in the map. - -
{% raw %}
-TotalMap : Set → Set
-TotalMap A = Id → A
-{% endraw %}
- -Intuitively, a total map over anfi element type `A` _is_ just a -function that can be used to look up ids, yielding `A`s. - -
{% raw %}
-module TotalMap where
-{% endraw %}
- -The function `always` yields a total map given a -default element; this map always returns the default element when -applied to any id. - -
{% raw %}
-  always : ∀ {A} → A → TotalMap A
-  always v x = v
-{% endraw %}
- -More interesting is the update function, which (as before) takes -a map `ρ`, a key `x`, and a value `v` and returns a new map that -takes `x` to `v` and takes every other key to whatever `ρ` does. - -
{% raw %}
-  infixl 15 _,_↦_  
-
-  _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A
-  (ρ , x ↦ v) y with x ≟ y
-  ... | yes x≡y = v
-  ... | no  x≢y = ρ y
-{% endraw %}
- -This definition is a nice example of higher-order programming. -The update function takes a _function_ `ρ` and yields a new -function that behaves like the desired map. - -For example, we can build a map taking ids to naturals, where `x` -maps to 42, `y` maps to 69, and every other key maps to 0, as follows: - -
{% raw %}
-  module example where
-
-    x y z : Id
-    x = id 0
-    y = id 1
-    z = id 2
-
-    ρ₀ : TotalMap ℕ
-    ρ₀ = always 0 , x ↦ 42 , y ↦ 69
-
-    test₁ : ρ₀ x ≡ 42
-    test₁ = refl
-
-    test₂ : ρ₀ y ≡ 69
-    test₂ = refl
-
-    test₃ : ρ₀ z ≡ 0
-    test₃ = refl
-{% endraw %}
- -This completes the definition of total maps. Note that we don't -need to define a `find` operation because it is just function -application! - -To use maps in later chapters, we'll need several fundamental -facts about how they behave. Even if you don't work the following -exercises, make sure you understand the statements of -the lemmas! - -#### Exercise: 1 star, optional (apply-always) -The `always` map returns its default element for all keys: - -
{% raw %}
-  postulate
-    apply-always : ∀ {A} (v : A) (x : Id) → always v x ≡ v
-{% endraw %}
- - - -#### Exercise: 2 stars, optional (update-eq) -Next, if we update a map `ρ` at a key `x` with a new value `v` -and then look up `x` in the map resulting from the update, we get -back `v`: - -
{% raw %}
-  postulate
-    update-eq : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A)
-              → (ρ , x ↦ v) x ≡ v
-{% endraw %}
- - - -#### Exercise: 2 stars, optional (update-neq) -On the other hand, if we update a map `m` at a key `x` and -then look up a _different_ key `y` in the resulting map, we get -the same result that `m` would have given: - -
{% raw %}
-  update-neq : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id)
-             → x ≢ y → (ρ , x ↦ v) y ≡ ρ y
-  update-neq ρ x v y x≢y with x ≟ y
-  ... | yes x≡y = ⊥-elim (x≢y x≡y)
-  ... | no  _   = refl
-{% endraw %}
- -For the following lemmas, since maps are represented by functions, to -show two maps equal we will need to postulate extensionality. - -
{% raw %}
-  postulate
-    extensionality : ∀ {A : Set} {ρ ρ′ : TotalMap A} → (∀ x → ρ x ≡ ρ′ x) → ρ ≡ ρ′
-{% endraw %}
- -#### Exercise: 2 stars, optional (update-shadow) -If we update a map `ρ` at a key `x` with a value `v` and then -update again with the same key `x` and another value `w`, the -resulting map behaves the same (gives the same result when applied -to any key) as the simpler map obtained by performing just -the second update on `ρ`: - -
{% raw %}
-  postulate
-    update-shadow : ∀ {A} (ρ : TotalMap A) (x : Id) (v w : A) 
-                  → (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w)
-{% endraw %}
- - - -#### Exercise: 2 stars (update-same) -Prove the following theorem, which states that if we update a map `ρ` to -assign key `x` the same value as it already has in `ρ`, then the -result is equal to `ρ`: - -
{% raw %}
-  postulate
-    update-same : ∀ {A} (ρ : TotalMap A) (x : Id) → (ρ , x ↦ ρ x) ≡ ρ
-{% endraw %}
- - - -#### Exercise: 3 stars, recommended (update-permute) -Prove one final property of the `update` function: If we update a map -`m` at two distinct keys, it doesn't matter in which order we do the -updates. - -
{% raw %}
-  postulate
-    update-permute : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A)
-                   → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
-{% endraw %}
- - - -## Partial maps - -Finally, we define _partial maps_ on top of total maps. A partial -map with elements of type `A` is simply a total map with elements -of type `Maybe A` and default element `nothing`. - -
{% raw %}
-PartialMap : Set → Set
-PartialMap A = TotalMap (Maybe A)
-{% endraw %}
- -
{% raw %}
-module PartialMap where
-{% endraw %}
- -
{% raw %}
-  ∅ : ∀ {A} → PartialMap A
-  ∅ = TotalMap.always nothing
-{% endraw %}
- -
{% raw %}
-  infixl 15 _,_↦_  
-
-  _,_↦_ : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) → PartialMap A
-  ρ , x ↦ v = TotalMap._,_↦_ ρ x (just v)
-{% endraw %}
- -We now lift all of the basic lemmas about total maps to partial maps. - -
{% raw %}
-  apply-∅ : ∀ {A} → (x : Id) → (∅ {A} x) ≡ nothing
-  apply-∅ x  = TotalMap.apply-always nothing x
-{% endraw %}
- -
{% raw %}
-  update-eq : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A)
-            → (ρ , x ↦ v) x ≡ just v
-  update-eq ρ x v = TotalMap.update-eq ρ x (just v)
-{% endraw %}
- -
{% raw %}
-  update-neq : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id)
-             → x ≢ y → (ρ , x ↦ v) y ≡ ρ y
-  update-neq ρ x v y x≢y = TotalMap.update-neq ρ x (just v) y x≢y
-{% endraw %}
- -
{% raw %}
-  update-shadow : ∀ {A} (ρ : PartialMap A) (x : Id) (v w : A) 
-                → (ρ , x ↦ v , x ↦ w) ≡ (ρ , x ↦ w)
-  update-shadow ρ x v w = TotalMap.update-shadow ρ x (just v) (just w)
-{% endraw %}
- -
{% raw %}
-  update-same : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) 
-              → ρ x ≡ just v
-              → (ρ , x ↦ v) ≡ ρ
-  update-same ρ x v ρx≡v rewrite sym ρx≡v = TotalMap.update-same ρ x
-{% endraw %}
- -
{% raw %}
-  update-permute : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) (y : Id) (w : A) 
-                 → x ≢ y → (ρ , x ↦ v , y ↦ w) ≡ (ρ , y ↦ w , x ↦ v)
-  update-permute ρ x v y w x≢y = TotalMap.update-permute ρ x (just v) y (just w) x≢y
-{% endraw %}
- -We will also need the following basic facts about the `Maybe` type. - -
{% raw %}
-  just≢nothing : ∀ {X : Set} → ∀ {x : X} → ¬ (_≡_ {A = Maybe X} (just x) nothing)
-  just≢nothing ()
-
-  just-injective : ∀ {X : Set} {x y : X} → _≡_ {A = Maybe X} (just x) (just y) → x ≡ y
-  just-injective refl = refl
-{% endraw %}
diff --git a/out/Stlc.md b/out/Stlc.md deleted file mode 100644 index 462370e9..00000000 --- a/out/Stlc.md +++ /dev/null @@ -1,5684 +0,0 @@ ---- -title : "Stlc: The Simply Typed Lambda-Calculus" -layout : page -permalink : /Stlc ---- - -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 just 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 be slightly more pragmatic and choose booleans as our base type. - -This chapter formalises the STLC (syntax, small-step semantics, and typing rules), -and the next chapter reviews its main properties (progress and preservation). -The new technical challenges arise from the mechanisms of -_variable binding_ and _substitution_. - - - -We choose booleans as our base type for simplicity. At the end of the -chapter we'll see how to add numbers as a base type, and in later -chapters we'll enrich STLC with useful constructs like pairs, sums, -lists, records, subtyping, and mutable state. - -## Imports - -
{% raw %}
-open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
-open PartialMap using (∅; just-injective) renaming (_,_↦_ to _,_∶_)
-open import Data.Nat using (ℕ)
-open import Data.Maybe using (Maybe; just; nothing)
-open import Relation.Nullary using (Dec; yes; no; ¬_)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
-{% endraw %}
- -## Syntax - -We have just two types. - - * Functions, `A ⇒ B` - * Booleans, `𝔹` - -We require some form of base type, because otherwise the set of types -would be empty. Church used a trivial base type `o` with no operations. -For us, it is more convenient to use booleans. Later we will consider -numbers as a base type. - -Here is the syntax of types in BNF. - - A, B, C ::= A ⇒ B | 𝔹 - -And here it is formalised in Agda. - -
{% raw %}
-infixr 20 _⇒_
-
-data Type : Set where
-  _⇒_ : Type → Type → Type
-  𝔹 : Type
-{% endraw %}
- -Terms have six constructs. Three are for the core lambda calculus: - - * Variables, `` ` x `` - * Abstractions, `λ[ x ∶ A ] N` - * Applications, `L · M` - -and three are for the base type, booleans: - - * True, `true` - * False, `false` - * Conditions, `if L then M else N` - -Abstraction is also called lambda abstraction, and is the construct -from which the calculus takes its name. - -With the exception of variables, each term form either constructs -a value of a given type (abstractions yield functions, true and -false yield booleans) or deconstructs it (applications use functions, -conditionals use booleans). 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 ∶ A ] N | L · M | true | false | if L then M else N - -And here it is formalised in Agda. - -
{% raw %}
-infixl 20 _·_
-infix  15 λ[_∶_]_
-infix  15 if_then_else_
-
-data Term : Set where
-  ` : Id → Term
-  λ[_∶_]_ : Id → Type → Term → Term
-  _·_ : Term → Term → Term
-  true : Term
-  false : Term
-  if_then_else_ : Term → Term → Term → Term
-{% endraw %}
- -#### Special characters - -We use the following special characters - - ⇒ U+21D2: RIGHTWARDS DOUBLE ARROW (\=>) - ` U+0060: GRAVE ACCENT - λ U+03BB: GREEK SMALL LETTER LAMBDA (\Gl or \lambda) - ∶ U+2236: RATIO (\:) - · U+00B7: MIDDLE DOT (\cdot) - -Note that ∶ (U+2236 RATIO) is not the same as : (U+003A COLON). -Colon is reserved in Agda for declaring types. Everywhere that we -declare a type in the object language rather than Agda we use -ratio in place of colon. - -Using ratio for this purpose is arguably a bad idea, because one must use context -rather than appearance to distinguish it from colon. Arguably, it might be -better to use a different symbol, such as `∈` or `::`. We reserve `∈` -for use later to indicate that a variable appears free in a term, and -eschew `::` because we consider it too ugly. - - -#### 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 since it is closer to the informal notation `x`. - -Similarly, informal presentation often use the notations `A → B` for -functions, `λ x . N` for abstractions, and `L M` for applications. We -cannot use these, because they overlap with the notation used by Agda. -In `λ[ x ∶ A ] N`, recall that Agda treats square brackets `[]` as -ordinary symbols, while round parentheses `()` and curly braces `{}` -have special meaning. We would use `L @ M` for application, but -`@` has a reserved meaning in Agda. - - -#### Examples - -Here are a couple of example terms, `not` of type -`𝔹 ⇒ 𝔹`, which complements its argument, and `two` of type -`(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` which takes a function and a boolean -and applies the function to the boolean twice. - -
{% raw %}
-f x y : Id
-f  =  id 0
-x  =  id 1
-y  =  id 2
-
-not two : Term 
-not =  λ[ x ∶ 𝔹 ] (if ` x then false else true)
-two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
-{% endraw %}
- - -#### Bound and free variables - -In an abstraction `λ[ x ∶ A ] N` we call `x` the _bound_ variable -and `N` the _body_ of the abstraction. One of the most important -aspects of lambda calculus is that names of bound variables are -irrelevant. Thus the five terms - -* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` -* `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) `` -* `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) `` -* `` λ[ 😈 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 😈 · (` 😈 · ` 😄) `` -* `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) `` - -are all considered equivalent. This equivalence relation -is sometimes called _alpha renaming_. - -As we descend from a term into its subterms, variables -that are bound may become free. Consider the following terms. - - - - -* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` - Both variable `f` and `x` are bound. - -* `` λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` - has `x` as a bound variable but `f` as a free variable. - -* `` ` f · (` f · ` x) `` - has both `f` and `x` 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. A formal definition of bound and free variables will be -given in the next chapter. - -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. - -#### Special characters - - 😈 U+1F608: SMILING FACE WITH HORNS - 😄 U+1F604: SMILING FACE WITH OPEN MOUTH AND SMILING EYES - -#### 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) `` - - abbreviates `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` - - and not `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``. - -
{% raw %}
-ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
-ex₁ = refl
-
-ex₂ : two · not · true ≡ (two · not) · true
-ex₂ = refl
-
-ex₃ : λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
-      ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x))))
-ex₃ = refl
-{% endraw %}
- -#### 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. - -## Values - -We only consider reduction of _closed_ terms, -those that contain no free variables. We consider -a precise definition of free variables in -[StlcProp]({{ "StlcProp" | relative_url }}). - -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. - -
{% raw %}
-data Value : Term → Set where
-  value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
-  value-true  : Value true
-  value-false : Value false
-{% endraw %}
- -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 ∶ A ] N` as a value only if `N` is a value. -Indeed, this is how Agda normalises terms. -Formalising this approach requires a more sophisticated -definition of substitution, which permits substituting -closed terms for values. - -## Substitution - -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 `false` for `` `x `` 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 `V`, -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. - -
{% raw %}
-_[_:=_] : Term → Id → Term → Term
-(` x′) [ x := V ] with x ≟ x′
-... | yes _ = V
-... | no  _ = ` x′
-(λ[ x′ ∶ A′ ] N′) [ x := V ] with x ≟ x′
-... | yes _ = λ[ x′ ∶ A′ ] N′
-... | no  _ = λ[ x′ ∶ A′ ] (N′ [ x := V ])
-(L′ · M′) [ x := V ] =  (L′ [ x := V ]) · (M′ [ x := V ])
-(true) [ x := V ] = true
-(false) [ x := V ] = false
-(if L′ then M′ else N′) [ x := V ] =
-  if (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
-{% endraw %}
- -The two key cases are variables and abstraction. - -* For variables, we compare `x`, 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 `x`, the variable we are substituting for, -with `x′`, the variable bound in the abstraction. If they are the same, -we yield abstraction unchanged, otherwise we subsititute inside the body. - -In all other cases, we push substitution recursively into -the subterms. - -#### Special characters - - ′ U+2032: PRIME (\') - -Note that ′ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE). - - -#### Examples - -Here is confirmation that the examples above are correct. - -
{% raw %}
-ex₁₁ : ` f [ f := not ] ≡  not
-ex₁₁ = refl
-
-ex₁₂ : true [ f := not ] ≡ true
-ex₁₂ = refl
-
-ex₁₃ : (` f · true) [ f := not ] ≡ not · true
-ex₁₃ = refl
-
-ex₁₄ : (` f · (` f · true)) [ f := not ] ≡ not · (not · true)
-ex₁₄ = refl
-
-ex₁₅ : (λ[ x ∶ 𝔹 ] ` f · (` f · ` x)) [ f := not ] ≡ λ[ x ∶ 𝔹 ] not · (not · ` x)
-ex₁₅ = refl
-
-ex₁₆ : (λ[ y ∶ 𝔹 ] ` y) [ x := true ] ≡ λ[ y ∶ 𝔹 ] ` y
-ex₁₆ = refl
-
-ex₁₇ : (λ[ x ∶ 𝔹 ] ` x) [ x := true ] ≡ λ[ x ∶ 𝔹 ] ` x
-ex₁₇ = refl
-{% endraw %}
- -#### 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.a - -In an informal presentation of the formal semantics, -the rules for reduction are written as follows. - - L ⟹ L′ - --------------- ξ·₁ - L · M ⟹ L′ · M - - Value V - M ⟹ M′ - --------------- ξ·₂ - V · M ⟹ V · M′ - - Value V - --------------------------------- βλ· - (λ[ x ∶ A ] 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. - -
{% raw %}
-infix 10 _⟹_ 
-
-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 A N V} → Value V →
-    (λ[ x ∶ A ] N) · V ⟹ N [ x := V ]
-  ξif : ∀ {L L′ M N} →
-    L ⟹ L′ →    
-    if L then M else N ⟹ if L′ then M else N
-  βif-true : ∀ {M N} →
-    if true then M else N ⟹ M
-  βif-false : ∀ {M N} →
-    if false then M else N ⟹ N
-{% endraw %}
- -#### Special characters - -We use the following special characters - - ⟹ 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) - -#### Quiz - -What does the following term step to? - - (λ[ x ∶ 𝔹 ⇒ 𝔹 ] ` x) · (λ [ x ∶ 𝔹 ] ` x) ⟹ ??? - -1. `` (λ [ x ∶ 𝔹 ] ` x) `` -2. `` (λ[ x ∶ 𝔹 ⇒ 𝔹 ] ` x) `` -3. `` (λ[ x ∶ 𝔹 ⇒ 𝔹 ] ` x) · (λ [ x ∶ 𝔹 ] ` x) `` - -What does the following term step to? - - (λ[ x ∶ 𝔹 ⇒ 𝔹 ] ` x) · ((λ[ x ∶ 𝔹 ⇒ 𝔹 ] ` x) (λ [ x ∶ 𝔹 ] ` x)) ⟹ ??? - -1. `` (λ [ x ∶ 𝔹 ] ` x) `` -2. `` (λ[ x ∶ 𝔹 ⇒ 𝔹 ] ` x) `` -3. `` (λ[ 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 `` -4. `` true `` -5. `` 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. - -
{% raw %}
-infix 10 _⟹*_ 
-infixr 2 _⟹⟨_⟩_
-infix  3 _∎
-
-data _⟹*_ : Term → Term → Set where
-  _∎ : ∀ M → M ⟹* M
-  _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N
-{% endraw %}
- -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 of the two clauses in the definition of reflexive -and transitive closure have been chosen to allow us to lay -out example reductions in an appealing way. - -
{% raw %}
-reduction₁ : not · true ⟹* false
-reduction₁ =
-    not · true
-  ⟹⟨ βλ· value-true ⟩
-    if true then false else true
-  ⟹⟨ βif-true ⟩
-    false
-  ∎
-
-reduction₂ : two · not · true ⟹* true
-reduction₂ =
-    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
-  ∎
-{% endraw %}
- - - -#### Special characters - -We use the following special characters - - ∎ U+220E: END OF PROOF (\qed) - ⟨ U+27E8: MATHEMATICAL LEFT ANGLE BRACKET (\<) - ⟩ U+27E9: MATHEMATICAL RIGHT ANGLE BRACKET (\>) - -## 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 - -which asserts 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`. - -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 ∶ A ] 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. - -
{% raw %}
-Context : Set
-Context = PartialMap Type
-
-infix 10 _⊢_∶_
-
-data _⊢_∶_ : Context → Term → Type → Set where
-  Ax : ∀ {Γ x A} →
-    Γ x ≡ just A →
-    Γ ⊢ ` x ∶ A
-  ⇒-I : ∀ {Γ x N A B} →
-    Γ , x ∶ A ⊢ N ∶ B →
-    Γ ⊢ λ[ x ∶ A ] 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
-{% endraw %}
- -#### 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`: - - ------------ 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`: - - ----------------- Ax ------------ Ax - Γ₂ ⊢ ` 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 `Γ₂ = ∅ , f ∶ 𝔹 ⇒ 𝔹 , x ∶ 𝔹`. - -Here are the above derivations formalised in Agda. - -
{% raw %}
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
-typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
-
-typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
-typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
-{% endraw %}
- -#### Interaction with Agda - -Construction of a type derivation is best done interactively. -Start with the declaration: - - typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹 - typing₁ = ? - -Typing C-l causes Agda to create a hole and tell us its expected type. - - typing₁ = { }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. - - typing₁ = ⇒-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. - - typing₁ = ⇒-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. - -#### 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. - -
{% raw %}
-notyping₂ : ∀ {A} → ¬ (∅ ⊢ true · false ∶ A)
-notyping₂ (⇒-E () _)
-{% endraw %}
- -As a second example, here is a formal proof that it is not possible to -type `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y `` It cannot be typed, because -doing so requires `x` to be both boolean and a function. - -
{% raw %}
-contradiction : ∀ {A B} → ¬ (𝔹 ≡ A ⇒ B)
-contradiction ()
-
-notyping₁ : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
-notyping₁ (⇒-I (⇒-I (⇒-E (Ax Γx) _))) =  contradiction (just-injective Γx)
-{% endraw %}
- - -#### 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`, and `C` 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 `` - - - diff --git a/out/StlcProp.md b/out/StlcProp.md deleted file mode 100644 index 41f3a0b3..00000000 --- a/out/StlcProp.md +++ /dev/null @@ -1,7777 +0,0 @@ ---- -title : "StlcProp: Properties of STLC" -layout : page -permalink : /StlcProp ---- - -In this chapter, we develop the fundamental theory of the Simply -Typed Lambda Calculus---in particular, the type safety -theorem. - -## Imports - -
{% raw %}
-open import Function using (_∘_)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Maybe using (Maybe; just; nothing)
-open import Data.Product using (_×_; ∃; ∃₂; _,_; ,_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; trans; sym)
-open import Maps using (Id; _≟_; PartialMap)
-open Maps.PartialMap using (∅; apply-∅; update-permute; just≢nothing; just-injective)
-                     renaming (_,_↦_ to _,_∶_)
-open import Stlc
-import Data.Nat using (ℕ)
-{% endraw %}
- - -## 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`. - -
{% raw %}
-data canonical_for_ : Term → Type → Set where
-  canonical-λ : ∀ {x A N B} → canonical (λ[ x ∶ A ] 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) ()
-{% endraw %}
- -## 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. - -
{% raw %}
-data Progress : Term → Set where
-  steps : ∀ {M N} → M ⟹ N → Progress M
-  done  : ∀ {M} → Value M → Progress M
-
-progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
-{% endraw %}
- - - -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. - -
{% raw %}
-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
-{% endraw %}
- -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. - -
{% raw %}
-postulate
-  progress′ : ∀ M {A} → ∅ ⊢ M ∶ A → Progress M
-{% endraw %}
- -## 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 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: - - - `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: - -
{% raw %}
-data _∈_ : Id → Term → Set where
-  free-`  : ∀ {x} → x ∈ ` x
-  free-λ  : ∀ {x y A N} → y ≢ x → x ∈ N → x ∈ (λ[ y ∶ A ] N)
-  free-·₁ : ∀ {x L M} → x ∈ L → x ∈ (L · M)
-  free-·₂ : ∀ {x L M} → x ∈ M → x ∈ (L · M)
-  free-if₁ : ∀ {x L M N} → x ∈ L → x ∈ (if L then M else N)
-  free-if₂ : ∀ {x L M N} → x ∈ M → x ∈ (if L then M else N)
-  free-if₃ : ∀ {x L M N} → x ∈ N → x ∈ (if L then M else N)
-{% endraw %}
- -A term in which no variables appear free is said to be _closed_. - -
{% raw %}
-_∉_ : Id → Term → Set
-x ∉ M = ¬ (x ∈ M)
-
-closed : Term → Set
-closed M = ∀ {x} → x ∉ M
-{% endraw %}
- -Here are proofs corresponding to the first two examples above. - -
{% raw %}
-f≢x : f ≢ x
-f≢x ()
-
-example-free₁ : x ∈ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
-example-free₁ = free-λ f≢x (free-·₂ free-`)
-
-example-free₂ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x)
-example-free₂ (free-λ f≢f _) = f≢f refl
-{% endraw %}
- - -#### Exercise: 1 star (free-in) -Prove formally the remaining examples given above. - -
{% raw %}
-postulate
-  example-free₃ : x ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
-  example-free₄ : f ∈ ((λ[ f ∶ (𝔹 ⇒ 𝔹) ] ` f · ` x) · ` f)
-  example-free₅ : x ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
-  example-free₆ : f ∉ (λ[ f ∶ (𝔹 ⇒ 𝔹) ] λ[ x ∶ 𝔹 ] ` f · ` x)
-{% endraw %}
- -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`. - -
{% raw %}
-free-lemma : ∀ {x M A Γ} → x ∈ M → Γ ⊢ M ∶ A → ∃ λ B → Γ x ≡ just B
-{% endraw %}
- -_Proof_: We show, by induction on the proof that `x` appears - free in `M`, that, for all contexts `Γ`, if `M` is well - typed under `Γ`, then `Γ` assigns some type to `x`. - - - If the last rule used was `` free-` ``, then `M = `` `x ``, and from - the assumption that `M` is well typed under `Γ` we have - immediately that `Γ` assigns a type to `x`. - - - If the last rule used was `free-·₁`, then `M = L · M` and `x` - appears free in `L`. Since `L` is well typed under `Γ`, - we can see from the typing rules that `L` must also be, and - the IH then tells us that `Γ` assigns `x` a type. - - - Almost all the other cases are similar: `x` appears free in a - subterm of `M`, and since `M` is well typed under `Γ`, we - know the subterm of `M` in which `x` appears is well typed - under `Γ` as well, and the IH yields the desired conclusion. - - - The only remaining case is `free-λ`. In this case `M = - λ[ y ∶ A ] N`, and `x` appears free in `N`; we also know that - `x` is different from `y`. The difference from the previous - cases is that whereas `M` is well typed under `Γ`, its - body `N` is well typed under `(Γ , y ∶ A)`, so the IH - allows us to conclude that `x` is assigned some type by the - extended context `(Γ , y ∶ A)`. To conclude that `Γ` - assigns a type to `x`, we appeal the decidable equality for names - `_≟_`, and note that `x` and `y` are different variables. - -
{% raw %}
-free-lemma free-` (Ax Γx≡A) = (_ , Γx≡A)
-free-lemma (free-·₁ x∈L) (⇒-E ⊢L ⊢M) = free-lemma x∈L ⊢L
-free-lemma (free-·₂ x∈M) (⇒-E ⊢L ⊢M) = free-lemma x∈M ⊢M
-free-lemma (free-if₁ x∈L) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈L ⊢L
-free-lemma (free-if₂ x∈M) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈M ⊢M
-free-lemma (free-if₃ x∈N) (𝔹-E ⊢L ⊢M ⊢N) = free-lemma x∈N ⊢N
-free-lemma (free-λ {x} {y} y≢x x∈N) (⇒-I ⊢N) with free-lemma x∈N ⊢N
-... | Γx≡C with y ≟ x
-... | yes y≡x = ⊥-elim (y≢x y≡x)
-... | no  _   = Γx≡C
-{% endraw %}
- -A subtle point: if the first argument of `free-λ` was of type -`x ≢ y` rather than of type `y ≢ x`, then the type of the -term `Γx≡C` would not simplify properly; instead, one would need -to rewrite with the symmetric equivalence. - -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) - -
{% raw %}
-postulate
-  ∅⊢-closed : ∀ {M A} → ∅ ⊢ M ∶ A → closed M
-{% endraw %}
- - - -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. - -
{% raw %}
-context-lemma : ∀ {Γ Γ′ M A}
-        → (∀ {x} → x ∈ M → Γ x ≡ Γ′ x)
-        → Γ  ⊢ M ∶ A
-        → Γ′ ⊢ M ∶ A
-{% endraw %}
- -_Proof_: By induction on the derivation of `Γ ⊢ M ∶ A`. - - - If the last rule in the derivation was `Ax`, then `M = x` - and `Γ x ≡ just A`. By assumption, `Γ′ x = just A` as well, and - hence `Γ′ ⊢ M : A` by `Ax`. - - - If the last rule was `⇒-I`, then `M = λ[ y : A] N`, with - `A = A ⇒ B` and `Γ , y ∶ A ⊢ N ∶ B`. The - induction hypothesis is that, for any context `Γ″`, if - `Γ , y : A` and `Γ″` assign the same types to all the - free variables in `N`, then `N` has type `B` under - `Γ″`. Let `Γ′` be a context which agrees with - `Γ` on the free variables in `N`; we must show - `Γ′ ⊢ λ[ y ∶ A] N ∶ A ⇒ B`. - - By `⇒-I`, it suffices to show that `Γ′ , y:A ⊢ N ∶ B`. - By the IH (setting `Γ″ = Γ′ , y : A`), it suffices to show - that `Γ , y : A` and `Γ′ , y : A` agree on all the variables - that appear free in `N`. - - Any variable occurring free in `N` must be either `y` or - some other variable. Clearly, `Γ , y : A` and `Γ′ , y : A` - agree on `y`. Otherwise, any variable other - than `y` that occurs free in `N` also occurs free in - `λ[ y : A] N`, and by assumption `Γ` and - `Γ′` agree on all such variables; hence so do - `Γ , y : A` and `Γ′ , y : A`. - - - If the last rule was `⇒-E`, then `M = L · M`, with `Γ ⊢ L ∶ A ⇒ B` - and `Γ ⊢ M ∶ B`. One induction hypothesis states that for all - contexts `Γ′`, if `Γ′` agrees with `Γ` on the free variables in - `L` then `L` has type `A ⇒ B` under `Γ′`; there is a similar IH - for `M`. We must show that `L · M` also has type `B` under `Γ′`, - given the assumption that `Γ′` agrees with `Γ` on all the free - variables in `L · M`. By `⇒-E`, it suffices to show that `L` and - `M` each have the same type under `Γ′` as under `Γ`. But all free - variables in `L` are also free in `L · M`; in the proof, this is - expressed by composing `free-·₁ : ∀ {x} → x ∈ L → x ∈ L · M` with - `Γ~Γ′ : (∀ {x} → x ∈ L · M → Γ x ≡ Γ′ x)` to yield `Γ~Γ′ ∘ free-·₁ - : ∀ {x} → x ∈ L → Γ x ≡ Γ′ x`. Similarly for `M`; hence the - desired result follows from the induction hypotheses. - - - The remaining cases are similar to `⇒-E`. - -
{% raw %}
-context-lemma Γ~Γ′ (Ax Γx≡A) rewrite (Γ~Γ′ free-`) = Ax Γx≡A
-context-lemma {Γ} {Γ′} {λ[ x ∶ A ] N} Γ~Γ′ (⇒-I ⊢N) = ⇒-I (context-lemma Γx~Γ′x ⊢N)
-  where
-  Γx~Γ′x : ∀ {y} → y ∈ N → (Γ , x ∶ A) y ≡ (Γ′ , x ∶ A) y
-  Γx~Γ′x {y} y∈N with x ≟ y
-  ... | yes refl = refl
-  ... | no  x≢y  = Γ~Γ′ (free-λ x≢y y∈N)
-context-lemma Γ~Γ′ (⇒-E ⊢L ⊢M) = ⇒-E (context-lemma (Γ~Γ′ ∘ free-·₁)  ⊢L)
-                                       (context-lemma (Γ~Γ′ ∘ free-·₂) ⊢M) 
-context-lemma Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
-context-lemma Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
-context-lemma Γ~Γ′ (𝔹-E ⊢L ⊢M ⊢N) = 𝔹-E (context-lemma (Γ~Γ′ ∘ free-if₁) ⊢L)
-                                         (context-lemma (Γ~Γ′ ∘ free-if₂) ⊢M)
-                                         (context-lemma (Γ~Γ′ ∘ free-if₃) ⊢N)
-{% endraw %}
- - -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`. - -
{% raw %}
-preservation-[:=] : ∀ {Γ x A N B V}
-                 → (Γ , x ∶ A) ⊢ N ∶ B
-                 → ∅ ⊢ V ∶ A
-                 → Γ ⊢ (N [ x := V ]) ∶ B
-{% endraw %}
- -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. - - - -_Proof_: By induction on the derivation of `Γ , x ∶ A ⊢ N ∶ B`, -we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`. - - - If `N` is a variable there are two cases to consider, - depending on whether `N` is `x` or some other variable. - - - If `N = `` `x ``, then from `Γ , x ∶ A ⊢ x ∶ B` - we know that looking up `x` in `Γ , x : A` gives - `just B`, but we already know it gives `just A`; - applying injectivity for `just` we conclude that `A ≡ B`. - We must show that `x [ x := V] = V` - has type `A` under `Γ`, given the assumption that - `V` has type `A` under the empty context. This - follows from context invariance: if a closed term has type - `A` in the empty context, it has that type in any context. - - - If `N` is some variable `x′` different from `x`, then - we need only note that `x′` has the same type under `Γ , x ∶ A` - as under `Γ`. - - - If `N` is an abstraction `λ[ x′ ∶ A′ ] N′`, then the IH tells us, - for all `Γ′`́ and `B′`, that if `Γ′ , x ∶ A ⊢ N′ ∶ B′` - and `∅ ⊢ V ∶ A`, then `Γ′ ⊢ N′ [ x := V ] ∶ B′`. - - The substitution in the conclusion behaves differently - depending on whether `x` and `x′` are the same variable. - - First, suppose `x ≡ x′`. Then, by the definition of - substitution, `N [ x := V] = N`, so we just need to show `Γ ⊢ N ∶ B`. - But we know `Γ , x ∶ A ⊢ N ∶ B` and, since `x ≡ x′` - does not appear free in `λ[ x′ ∶ A′ ] N′`, the context invariance - lemma yields `Γ ⊢ N ∶ B`. - - Second, suppose `x ≢ x′`. We know `Γ , x ∶ A , x′ ∶ A′ ⊢ N′ ∶ B′` - by inversion of the typing relation, from which - `Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′` follows by update permute, - so the IH applies, giving us `Γ , x′ ∶ A′ ⊢ N′ [ x := V ] ∶ B′` - By `⇒-I`, we have `Γ ⊢ λ[ x′ ∶ A′ ] (N′ [ x := V ]) ∶ A′ ⇒ B′` - and the definition of substitution (noting `x ≢ x′`) gives - `Γ ⊢ (λ[ x′ ∶ A′ ] N′) [ x := V ] ∶ A′ ⇒ B′` as required. - - - If `N` is an application `L′ · M′`, the result follows - straightforwardly from the definition of substitution and the - induction hypotheses. - - - The remaining cases are similar to application. - -We need a couple of lemmas. A closed term can be weakened to any context, and `just` is injective. -
{% raw %}
-weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∶ A → Γ ⊢ V ∶ A
-weaken-closed {V} {A} {Γ} ⊢V = context-lemma Γ~Γ′ ⊢V
-  where
-  Γ~Γ′ : ∀ {x} → x ∈ V → ∅ x ≡ Γ x
-  Γ~Γ′ {x} x∈V = ⊥-elim (x∉V x∈V)
-    where
-    x∉V : ¬ (x ∈ V)
-    x∉V = ∅⊢-closed ⊢V {x}
-{% endraw %}
- -
{% raw %}
-preservation-[:=] {Γ} {x} {A} (Ax {Γ,x∶A} {x′} {B} [Γ,x∶A]x′≡B) ⊢V with x ≟ x′
-...| yes x≡x′ rewrite just-injective [Γ,x∶A]x′≡B  =  weaken-closed ⊢V
-...| no  x≢x′  =  Ax [Γ,x∶A]x′≡B
-preservation-[:=] {Γ} {x} {A} {λ[ x′ ∶ A′ ] N′} {.A′ ⇒ B′} {V} (⇒-I ⊢N′) ⊢V with x ≟ x′
-...| yes x≡x′ rewrite x≡x′ = context-lemma Γ′~Γ (⇒-I ⊢N′)
-  where
-  Γ′~Γ : ∀ {y} → y ∈ (λ[ x′ ∶ A′ ] N′) → (Γ , x′ ∶ A) y ≡ Γ y
-  Γ′~Γ {y} (free-λ x′≢y y∈N′) with x′ ≟ y
-  ...| yes x′≡y  = ⊥-elim (x′≢y x′≡y)
-  ...| no  _     = refl
-...| no  x≢x′ = ⇒-I ⊢N′V
-  where
-  x′x⊢N′ : Γ , x′ ∶ A′ , x ∶ A ⊢ N′ ∶ B′
-  x′x⊢N′ rewrite update-permute Γ x A x′ A′ x≢x′ = ⊢N′
-  ⊢N′V : (Γ , x′ ∶ A′) ⊢ N′ [ x := V ] ∶ B′
-  ⊢N′V = preservation-[:=] x′x⊢N′ ⊢V
-preservation-[:=] (⇒-E ⊢L ⊢M) ⊢V = ⇒-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V)
-preservation-[:=] 𝔹-I₁ ⊢V = 𝔹-I₁
-preservation-[:=] 𝔹-I₂ ⊢V = 𝔹-I₂
-preservation-[:=] (𝔹-E ⊢L ⊢M ⊢N) ⊢V =
-  𝔹-E (preservation-[:=] ⊢L ⊢V) (preservation-[:=] ⊢M ⊢V) (preservation-[:=] ⊢N ⊢V)
-{% endraw %}
- - -### 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. - -
{% raw %}
-preservation : ∀ {M N A} → ∅ ⊢ M ∶ A → M ⟹ N → ∅ ⊢ N ∶ A
-{% endraw %}
- -_Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`. - -- We can immediately rule out `Ax`, `⇒-I`, `𝔹-I₁`, and - `𝔹-I₂` as the final rules in the derivation, since in each of - these cases `M` cannot take a step. - -- If the last rule in the derivation was `⇒-E`, then `M = L · M`. - There are three cases to consider, one for each rule that - could have been used to show that `L · M` takes a step to `N`. - - - If `L · M` takes a step by `ξ·₁`, with `L` stepping to - `L′`, then by the IH `L′` has the same type as `L`, and - hence `L′ · M` has the same type as `L · M`. - - - The `ξ·₂` case is similar. - - - If `L · M` takes a step by `β⇒`, then `L = λ[ x ∶ A ] N` and `M - = V` and `L · M` steps to `N [ x := V]`; the desired result now - follows from the fact that substitution preserves types. - -- If the last rule in the derivation was `if`, then `M = if L - then M else N`, and there are again three cases depending on - how `if L then M else N` steps. - - - If it steps via `β𝔹₁` or `βB₂`, the result is immediate, since - `M` and `N` have the same type as `if L then M else N`. - - - Otherwise, `L` steps by `ξif`, and the desired conclusion - follows directly from the induction hypothesis. - -
{% raw %}
-preservation (Ax Γx≡A) ()
-preservation (⇒-I ⊢N) ()
-preservation (⇒-E (⇒-I ⊢N) ⊢V) (βλ· valueV) = preservation-[:=] ⊢N ⊢V
-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 𝔹-I₁ ()
-preservation 𝔹-I₂ ()
-preservation (𝔹-E 𝔹-I₁ ⊢M ⊢N) βif-true = ⊢M
-preservation (𝔹-E 𝔹-I₂ ⊢M ⊢N) βif-false = ⊢N
-preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹L′
-...| ⊢L′ = 𝔹-E ⊢L′ ⊢M ⊢N
-{% endraw %}
- - -#### 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. - -
{% raw %}
-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)
-{% endraw %}
- - - - -## Uniqueness of Types - -#### Exercise: 3 stars (types_unique) - -Another nice property of the STLC is that types are unique: a -given term (in a given context) has at most one type. -Formalize this statement and prove it. - - -## 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 ∶ A ] ` 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 - - -### Exercise: STLC with Arithmetic - -To see how the STLC might function as the core of a real -programming language, let's extend it with a concrete base -type of numbers and some constants and primitive -operators. - -To types, we add a base type of numbers (and remove -booleans, for brevity). - -
{% raw %}
-data Type′ : Set where
-  _⇒_ : Type′ → Type′ → Type′
-  ℕ : Type′
-{% endraw %}
- -To terms, we add natural number constants, along with -plus, minus, and testing for zero. - -
{% raw %}
-data Term′ : Set where
-  `_ : Id → Term′
-  λ[_∶_]_ : Id → Type′ → Term′ → Term′
-  _·_ : Term′ → Term′ → Term′
-  #_ : Data.Nat.ℕ → Term′
-  _+_ : Term′ → Term′ → Term′
-  _-_ : Term′ → Term′ → Term′
-  if0_then_else_ : Term′ → Term′ → Term′ → Term′
-{% endraw %}
- -(Assume that `m - n` returns `0` if `m` is less than `n`.) - -#### Exercise: 4 stars (stlc_arith) - -Finish formalizing the definition and properties of the STLC extended -with arithmetic. Specifically: - - - Copy the whole development of STLC that we went through above (from - the definition of values through the Type Soundness theorem), and - paste it into the file at this point. - - - Extend the definitions of the `subst` operation and the `step` - relation to include appropriate clauses for the arithmetic operators. - - - Extend the proofs of all the properties (up to `soundness`) of - the original STLC to deal with the new syntactic forms. Make - sure Agda accepts the whole file. - diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 91f06935..d923fe72 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -127,7 +127,7 @@ Let's look again at the definition of natural numbers: Wait a minute! The second line defines natural numbers in terms of natural numbers. How can that posssibly be allowed? -Isn't this as useless as claiming `Brexit means Brexit`? +Isn't this as useless as claiming "Brexit means Brexit"? In fact, it is possible to assign our definition a meaning without resorting to any unpermitted circularities. Furthermore, we can do so @@ -296,25 +296,25 @@ numbers. Such a definition is called *well founded*. For example, let's add two and three. 2 + 3 - = { expand shorthand } + = (is shorthand for) (suc (suc zero)) + (suc (suc (suc zero))) - = { by (ii) } + = (ii) suc ((suc zero) + (suc (suc (suc zero)))) - = { by (ii) } + = (ii) suc (suc (zero + (suc (suc (suc zero))))) - = { by (i) } + = (i) suc (suc (suc (suc (suc zero)))) - = { compress longhand } + = (is longhand for) 5 We can write this more compactly by only expanding shorthand as needed. 2 + 3 - = { by (ii) } + = (ii) suc (1 + 3) - = { by (ii) } + = (ii) suc (suc (0 + 3)) - = { by (i) } + = (i) suc (suc 3) = 5 @@ -358,11 +358,11 @@ larger numbers is defined in terms of multiplication of smaller numbers. For example, let's multiply two and three. 2 * 3 - = {by (iv)} + = (iv) 3 + (1 * 3) - = {by (iv)} + = (iv) 3 + (3 + (0 * 3)) - = {by (iii)} + = (iii) 3 + (3 + 0) = 6 @@ -418,22 +418,22 @@ small numbers. For example, let's subtract two from three. 3 ∸ 2 - = {by (ix)} + = (ix) 2 ∸ 1 - = {by (ix)} + = (ix) 1 ∸ 0 - = {by (vii)} + = (vii) 1 We did not use equation (viii) at all, but it will be required if we try to subtract a smaller number from a larger one. 2 ∸ 3 - = {by (ix)} + = (ix) 1 ∸ 2 - = {by (ix)} + = (ix) 0 ∸ 1 - = {by (viii)} + = (viii) 0 **Exercise** Compute `5 ∸ 3` and `3 ∸ 5` by the same technique. diff --git a/src/Properties.lagda b/src/Properties.lagda new file mode 100644 index 00000000..fa0454b2 --- /dev/null +++ b/src/Properties.lagda @@ -0,0 +1,154 @@ +--- +title : "Properties: Proof by Induction" +layout : page +permalink : /Properties +--- + +Now that we've defined the naturals and operations upon them, +our next step is to learn how to prove properties that they +satisfy. Unsurprisingly, properties of *inductive datatypes* +are proved by *induction*. + + +## Imports + +Each chapter will begin with a list of the imports we require from the +Agda standard library. We will, of course, require the naturals; +everything in the previous chapter is also found in the library module +`Data.Nat`, so we import the required definitions from there. We also +require propositional equality. + +\begin{code} +open import Data.Nat using (ℕ; zero; suc) +open import Relation.Binary.PropositionalEquality using (_≡_; refl) +\end{code} + +Each import consists of the keywords `open` and `import`, followed by +the module name, followed by the keyword `using`, followed by the +names of each identifier imported from the module, surrounded by +parentheses and separated by semicolons. + + +## Associativity + +One property of addition is that it is *associative*, that is that the +order of the parentheses does not matter: + + (m + n) + p ≡ m + (n + p) + +We write `=` in an Agda definition, whereas we write `≡` for an +equality we are trying to prove. Here `m`, `n`, and `p` are variables +that range over all natural numbers. + +We can test the proposition by choosing specific numbers for the three +variables. + + (3 + 4) + 5 + ≡ + 7 + 5 + ≡ + 12 + ≡ + 3 + 9 + ≡ + 3 + (4 + 5) + +Here we have displayed the computation in tabular form, one term to a +line. We will often use such a form. It is often easiest to read +such computations from the top down until one reaches the simplest +possible term (in this case, 12), and then from the bottom up until +one reaches the same term. + +We could go on testing the proposition by choosing other numbers, but---since there are an infinite number of naturals---we will never finish. + + + +To prove a property of natural numbers by induction, we need to prove two things. +First, we prove the property holds for `zero`, and secondly we prove that if +the property holds for an arbitrary natural `m` then it also holds for `suc m`. +If we write `P m` for a property of `m`, then we can write out the principle +of induction as an inference rule: + + P zero + ∀ (m : ℕ) → P m → P (suc m) + ----------------------------- + ∀ (m : ℕ) → P m + +Let's unpack this rule. The first hypothesis states +that property `P` holds for `zero`. The second hypothesis states that for all natural +numbers `m`, if `P` holds for `m` then `P` also holds for `suc m`. The conclusion +states that for all natural numbers `m` we have that `P` holds for `m`. +We call the first hypothesis the *base case*; it requires we show `P zero`. +We call the second hypothesis the *inductive case*; it requires we assume `P m`, which +we call the *induction hypothesis*, and use it to show `P (suc m)`. + +In order to prove associativity, we take `P m` to be the property + + (m + n) + p ≡ m + (n + p) + +Then the appropriate instance of the inference rule becomes: + + (zero + n) + p ≡ zero + (n + p) + ∀ (m : ℕ) → (m + n) + p ≡ m + (n + p) → (suc m + n) + p ≡ (suc m + n) + p + ----------------------------------------------------------------------------- + ∀ (m : ℕ) → (m + n) + p ≡ m + (n + p) + +In the inference rule, `n` and `p` are any arbitary natural numbers, so when we +are done with the proof we know it holds for any `n` and `p` as well as any `m`. + +Recall the definition of addition. +\begin{code} +_+_ : ℕ → ℕ → ℕ +zero + n = n -- (i) +(suc m) + n = suc (m + n) -- (ii) +\end{code} + +For the base case, we must show: + + (zero + n) + p ≡ zero + (n + p) + +By (i), both sides of the equation simplify to `n + p`, so it holds. +In tabular form, we write this as follows: + + (zero + n) + p + ≡ (i) + n + p + ≡ (i) + zero + (n + p) + +It is often easiest to read such proofs down from the top and up from +the bottom, meeting in the middle where the two terms are the same. + +For the inductive case, we assume + + (m + n) + p ≡ m + (n + p) + +and must show + + (suc m + n) + p ≡ (suc m + n) + p + +By (ii), the left-hand side simplifies to `suc ((m + n) + p)` and the +right-hand side simplifies to `suc (m + (n + p))`, and the equality of +these follow from what we assumed. In tabular form: + + (suc m + n) + p + ≡ (ii) + suc (m + n) + p + ≡ (ii) + suc ((m + n) + p) + ≡ (induction hypothesis) + suc (m + (n + p)) + ≡ (ii) + suc m + (n + p) + + + + + +## Unicode + +In this chapter we use the following unicode. + + ≡ U+2261 IDENTICAL TO (\==) + ∀ U+2200 FOR ALL (\forall) + λ U+03BB GREEK SMALL LETTER LAMBDA (\Gl, \lambda)