completed More

src/plfa/DeBruijn.lagda

@@ -18,6 +18,13 @@ inherently typed.  Our new presentation is more compact, using
 less than half the lines of code required previously to do
 cover the same ground.
 
+The inherently typed representation was first proposed by
+Thorsten Altenkirch and Bernhard Reus.
+The formalisation of renaming and substitution
+we use is due to Conor McBride.
+Related work has been carried out by
+James Chapman, James McKinna, and many others.
+
 ## Imports
 
 \begin{code}
@@ -185,42 +192,12 @@ shadowing: with variable names, there is no way to refer to
 the former binding in the scope of the latter, but with de
 Bruijn indices it could be referred to as `# 2`.
 
-
 ## Order of presentation
 
-The presentation in the previous two chapters was ordered as
-follows, where the first chapter introduces raw terms, and the
-second proves their properties.
-
-  * Lambda: Introduction to Lambda Calculus
-    + 1.1 Syntax
-    + 1.2 Values
-    + 1.3 Substitution
-    + 1.4 Reduction
-    + 1.5 Typing
-  * Properties: Progress and Preservation
-    + 2.1 Canonical forms lemma
-    + 2.2 Progress
-    + 2.3 Renaming lemma
-    + 2.4 Substitution preserves types
-    + 2.5 Preservation
-    + 2.6 Evaluation
-
 In the current chapter, the use of inherently-typed terms
 necessitates that we cannot introduce operations such as
 substitution or reduction without also showing that they
 preserve types.  Hence, the order of presentation must change.
-For each new section, we show the corresponding old section or
-sections.
-
-  * DeBruijn: Inherently typed de Bruijn representation
-    + Syntax (1.1, 1.5)
-    + Values (1.2, 2.1)
-    + Renaming (2.3)
-    + Substitution (1.3, 2.3)
-    + Reduction (1.3, 2.4)
-    + Progress (2.2)
-    + Evaluation (2.6)
 
 The syntax of terms now incorporates their typing rules, and the
 definition of values now incorporates the Canonical Forms lemma.  The
@@ -505,19 +482,7 @@ As before we generalise everything save `2+2ᶜ` to arbitary
 contexts.  While we are at it, we also generalise `twoᶜ` and
 `plusᶜ` to Church numerals over arbitrary types.
 
-## Substitution
+## Renaming
-
-With terms in hand, we turn to substitution.
-Whereas before we had to restrict our
-attention to substituting only one variable at a time and
-could only substitute closed terms, here we can consider
-simultaneous subsitution of open terms.  The
-definition of substitution we consider is due to Conor
-McBride.  Whereas before we defined substitution in one
-chapter and showed it preserved types in the next chapter,
-here we write code that does both at once.
-
-### Renaming
 
 Renaming is a necessary prelude to substitution, enabling us
 to "rebase" a term from one context to another.  It
@@ -620,7 +585,7 @@ typing, and hence the Agda code for inherently-typed de Bruijn
 terms is inherently reliable.
 
 
-### Simultaneous Substitution
+## Simultaneous Substitution
 
 Because de Bruijn indices free us of concerns with renaming,
 it becomes easy to provide a definition of substitution that
@@ -695,7 +660,7 @@ The remaining cases are similar, recursing on each subterm,
 and extending the map whenever the construct introduces a
 bound variable.
 
-### Single substitution
+## Single substitution
 
 From the general case of substitution for multiple free
 variables in is easy to define the special case of
@@ -773,12 +738,7 @@ And combining definition with proof makes it harder for errors
 to sneak in.
 
 
-## Reduction
+## Values
-
-With substitution out of the way, it is straightforward to
-define values and reduction.
-
-### Value
 
 The definition of value is much as before, save that the
 added types incorporate the same information found in the
@@ -804,7 +764,8 @@ Here `zero` requires an implicit parameter to aid inference,
 much in the same way that `[]` did in
 [Lists]({{ site.baseurl }}{% link out/plfa/Lists.md %})).
 
-### Reduction step
+
+## Reduction
 
 The reduction rules are the same as those given earlier, save
 that for each term we must specify its types.  As before, we
@@ -867,7 +828,7 @@ preserves types, which we previously is built-in to our
 definition of substitution.
 
 
-### Reflexive and transitive closure
+## Reflexive and transitive closure
 
 The reflexive and transitive closure is exactly as before.
 We simply cut-and-paste the previous definition.

src/plfa/More.lagda

@@ -12,6 +12,7 @@ So far, we have focussed on a relatively minimal language, based on
 Plotkin's PCF, which supports functions, naturals, and fixpoints.  In
 this chapter we extend our calculus to support the following:
 
+  * primitive numbers
   * _let_ bindings
   * products
   * an alternative formulation of products
@@ -24,7 +25,7 @@ this chapter we extend our calculus to support the following:
 All of the data types should be familiar from Part I of this textbook.
 For _let_ and the alternative formulations we show how they translate
 to other constructs in the calculus.  Most of the description will be
-informal. We show how to formalise the first three constructs and leave
+informal. We show how to formalise the first four constructs and leave
 the rest as an exercise for the reader.
 
 Our informal descriptions will be in the style of
@@ -40,6 +41,58 @@ For each construct, we give syntax, typing, reductions, and an example.
 We also give translations where relevant; formally establishing the
 correctness of translations will be the subject of the next chapter.
 
+## Primitive numbers
+
+We define a `Num` type equivalent to the built-in natural number type
+with multiplication as a primitive operation on numbers.
+
+### Syntax
+
+    L, M, N ::= ...                     Terms
+      con c                               constant
+      L `* M                              multiplication
+
+### Typing
+
+The hypothesis of the `con` rule is unusual, in that
+it refers to a typing judgement of Agda rather than a
+typing judgement of the defined calculus.
+
+    c : ℕ
+    --------------- con
+    Γ ⊢ con c : Nat
+
+    Γ ⊢ L : Nat
+    Γ ⊢ M : Nat
+    ---------------- _`*_
+    Γ ⊢ L `* M : Nat
+
+### Reduction
+
+A rule that defines a primitive directly, such as the last rule below,
+is called a δ rule.  Here the δ rule defines multiplication of
+primitive numbers in terms of multiplication of naturals as given
+by the Agda standard prelude.
+
+    L —→ L′
+    ----------------- ξ-*₁
+    L `* M —→ L′ `* M
+
+    M —→ M′
+    ----------------- ξ-*₂
+    V `* M —→ V `* M′
+
+    ----------------------------- δ-*
+    con c `* con d —→ con (c * d)
+
+### Example
+
+Here is a function to cube a primitive number.
+
+    cube : ∅ ⊢ Nat ⇒ Nat
+    cube = ƛ x ⇒ x `* x `* x
+
+
 ## Let bindings
 
 Let bindings affect only the syntax of terms; they introduce no new
@@ -68,15 +121,13 @@ types or values.
 
 ### Example
 
-Let _`*_ : ∅ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ represent multiplication of naturals.
+Here is a function to raise a primitive number to the tenth power.
-Then raising a natural to the tenth power can be defined as follows.
 
-    exp10 : ∅ ⊢ `ℕ ⇒ `ℕ
+    exp10 : ∅ ⊢ Nat ⇒ Nat
     exp10 = ƛ x ⇒ `let x2  `= x  `* x  `in
                   `let x4  `= x2 `* x2 `in
                   `let x5  `= x4 `* x  `in
-                  `let x10 `= x5 `* x5 `in
+                  x5 `* x5
-                  x10
 
 ### Translation
 
@@ -141,7 +192,7 @@ We can translate each _let_ term into an application of an abstraction.
 
 ### Example
 
-Here is the definition of a function to swap the components of a pair.
+Here is a function to swap the components of a pair.
 
     swap× : ∅ ⊢ A `× B ⇒ B `× A
     swap× = ƛ z ⇒ `⟨ proj₂ z , proj₁ z ⟩
@@ -190,7 +241,7 @@ and reduction rules.
 
 ### Example
 
-Function to swap the components of a pair rewritten in the new notation.
+Here is a function to swap the components of a pair rewritten in the new notation.
 
     swap×-case : ∅ ⊢ A `× B ⇒ B `× A
     swap×-case = ƛ z ⇒ case× z 
@@ -274,7 +325,7 @@ We can also translate back the other way.
 
 ### Example
 
-Here is the definition of a function to swap the components of a sum.
+Here is a function to swap the components of a sum.
 
     swap⊎ : ∅ ⊢ A `⊎ B ⇒ B `⊎ A
     swap⊎ = ƛ z ⇒ case⊎ z
@@ -496,6 +547,7 @@ Here is the map function for lists.
 
 We now show how to formalise
 
+  * primitive numbers
   * _let_ bindings
   * products
   * an alternative formulation of products
@@ -509,7 +561,7 @@ and leave formalisation of the remaining constructs as an exercise.
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
 open import Data.Empty using (⊥; ⊥-elim)
-open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
+open import Data.Nat using (ℕ; zero; suc; _*_)
 open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
 open import Data.Unit using (⊤; tt)
 open import Function using (_∘_)
@@ -533,6 +585,7 @@ infix  5 ƛ_
 infix  5 μ_
 infixr 6 _`∷_
 infixl 7 _·_
+infixl 8 _`*_
 infix  8 `suc_
 infix  9 `_
 infix  9 S_
@@ -548,6 +601,7 @@ infix  8 V-suc_
 data Type : Set where
   `ℕ    : Type
   _⇒_   : Type → Type → Type
+  Nat   : Type
   _`×_  : Type → Type → Type
   _`⊎_  : Type → Type → Type
   `⊤    : Type
@@ -628,6 +682,19 @@ data _⊢_ : Context → Type → Set where
       ----------
     → Γ ⊢ A
 
+  -- primitive
+
+  con : ∀ {Γ}
+    → ℕ
+      -------
+    → Γ ⊢ Nat
+
+  _`*_ : ∀ {Γ}
+    → Γ ⊢ Nat
+    → Γ ⊢ Nat
+      -------
+    → Γ ⊢ Nat
+
   -- let
 
   `let : ∀ {Γ A B}
@@ -722,7 +789,7 @@ data _⊢_ : Context → Type → Set where
     → Γ ⊢ B
 \end{code}
 
-## Abbreviating de Bruijn indices
+### Abbreviating de Bruijn indices
 
 \begin{code}
 lookup : Context → ℕ → Type
@@ -741,9 +808,7 @@ count {∅}     _        =  ⊥-elim impossible
 # n  =  ` count n
 \end{code}
 
-## Substitution
+## Renaming
-
-### Renaming
 
 \begin{code}
 ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
@@ -758,6 +823,9 @@ rename ρ (`zero)        =  `zero
 rename ρ (`suc M)       =  `suc (rename ρ M)
 rename ρ (case L M N)   =  case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
 rename ρ (μ N)          =  μ (rename (ext ρ) N)
+rename ρ (con n)        =  con n
+rename ρ (M `* N)       =  rename ρ M `* rename ρ N
+rename ρ (`let M N)     =  `let (rename ρ M) (rename (ext ρ) N)
 rename ρ `⟨ M , N ⟩     =  `⟨ rename ρ M , rename ρ N ⟩
 rename ρ (`proj₁ L)     =  `proj₁ (rename ρ L)
 rename ρ (`proj₂ L)     =  `proj₂ (rename ρ L)
@@ -771,10 +839,9 @@ rename ρ (case⊥ L)      =  case⊥ (rename ρ L)
 rename ρ `[]            =  `[]
 rename ρ (M `∷ N)       =  (rename ρ M) `∷ (rename ρ N)
 rename ρ (caseL L M N)  =  caseL (rename ρ L) (rename ρ M) (rename (ext (ext ρ)) N)
-rename ρ (`let M N)     =  `let (rename ρ M) (rename (ext ρ) N)
 \end{code}
 
-### Simultaneous Substitution
+## Simultaneous Substitution
 
 \begin{code}
 exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
@@ -789,6 +856,9 @@ subst σ (`zero)        =  `zero
 subst σ (`suc M)       =  `suc (subst σ M)
 subst σ (case L M N)   =  case (subst σ L) (subst σ M) (subst (exts σ) N)
 subst σ (μ N)          =  μ (subst (exts σ) N)
+subst σ (con n)        =  con n
+subst σ (M `* N)       =  subst σ M `* subst σ N
+subst σ (`let M N)     =  `let (subst σ M) (subst (exts σ) N)
 subst σ `⟨ M , N ⟩     =  `⟨ subst σ M , subst σ N ⟩
 subst σ (`proj₁ L)     =  `proj₁ (subst σ L)
 subst σ (`proj₂ L)     =  `proj₂ (subst σ L)
@@ -802,10 +872,9 @@ subst σ (case⊥ L)      =  case⊥ (subst σ L)
 subst σ `[]            =  `[]
 subst σ (M `∷ N)       =  (subst σ M) `∷ (subst σ N)
 subst σ (caseL L M N)  =  caseL (subst σ L) (subst σ M) (subst (exts (exts σ)) N)
-subst σ (`let M N)     =  `let (subst σ M) (subst (exts σ) N)
 \end{code}
 
-### Single and double substitution
+## Single and double substitution
 
 \begin{code}
 _[_] : ∀ {Γ A B}
@@ -833,9 +902,7 @@ _[_][_] {Γ} {A} {B} N V W =  subst {Γ , A , B} {Γ} σ N
   σ (S (S x))  =  ` x
 \end{code}
 
-## Reduction
+## Values
-
-### Value
 
 \begin{code}
 data Value : ∀ {Γ A} → Γ ⊢ A → Set where
@@ -857,6 +924,12 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
       --------------
     → Value (`suc V)
 
+  -- primitives
+
+  V-con : ∀ {Γ n}
+      ---------------------
+    → Value {Γ = Γ} (con n)
+
   -- products
 
   V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
@@ -899,7 +972,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
 Implicit arguments need to be supplied when they are
 not fixed by the given arguments.
 
-### Reduction step
+## Reduction
 
 \begin{code}
 infix 2 _—→_
@@ -951,6 +1024,23 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
       ----------------
     → μ N —→ N [ μ N ]
 
+  -- primitives
+
+  ξ-*₁ : ∀ {Γ} {L L′ M : Γ ⊢ Nat}
+    → L —→ L′
+      -----------------
+    → L `* M —→ L′ `* M
+
+  ξ-*₂ : ∀ {Γ} {V M M′ : Γ ⊢ Nat}
+    → Value V
+    → M —→ M′
+      -----------------
+    → V `* M —→ V `* M′
+
+  δ-* : ∀ {Γ c d}
+      -------------------------------------
+    → con {Γ = Γ} c `* con d —→ con (c * d)
+
   -- let
 
   ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
@@ -1086,7 +1176,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
     → caseL (V `∷ W) M N —→ N [ V ][ W ]
 \end{code}
 
-### Reflexive and transitive closure
+## Reflexive and transitive closure
 
 \begin{code}
 infix  2 _—↠_
@@ -1116,7 +1206,6 @@ begin M—↠N = M—↠N
 
 ## Values do not reduce
 
-Values do not reduce.
 \begin{code}
 V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
   → Value M
@@ -1125,6 +1214,7 @@ V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
 V¬—→ V-ƛ          ()
 V¬—→ V-zero       ()
 V¬—→ (V-suc VM)   (ξ-suc M—→M′)     =  V¬—→ VM M—→M′
+V¬—→ V-con        ()
 V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′)    =  V¬—→ VM M—→M′
 V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′)  =  V¬—→ VN N—→N′
 V¬—→ (V-inj₁ VM)  (ξ-inj₁ M—→M′)    =  V¬—→ VM M—→M′
@@ -1135,15 +1225,6 @@ V¬—→ (VM V-∷ _)   (ξ-∷₁ M—→M′)      =  V¬—→ VM M—→M
 V¬—→ (_ V-∷ VN)   (ξ-∷₂ _ N—→N′)    =  V¬—→ VN N—→N′
 \end{code}
 
-As a corollary, terms that reduce are not values.
-\begin{code}
-—→¬V : ∀ {Γ A} {M N : Γ ⊢ A}
-  → M —→ N
-    ---------
-  → ¬ Value M
-—→¬V M—→N VM  =  V¬—→ VM M—→N
-\end{code}
-
 
 ## Progress
 
@@ -1175,6 +1256,12 @@ progress (`zero)                            =  done V-zero
 progress (`suc M) with progress M
 ...    | step M—→M′                         =  step (ξ-suc M—→M′)
 ...    | done VM                            =  done (V-suc VM)
+progress (con n)                            =  done V-con
+progress (L `* M) with progress L
+...    | step L—→L′                         =  step (ξ-*₁ L—→L′)
+...    | done V-con with progress M
+...        | step M—→M′                     =  step (ξ-*₂ V-con M—→M′)
+...        | done V-con                     =  step δ-*
 progress (case L M N) with progress L
 ...    | step L—→L′                         =  step (ξ-case L—→L′)
 ...    | done V-zero                        =  step β-zero
@@ -1268,6 +1355,49 @@ eval (gas (suc m)) L with progress L
 ## Examples
 
 \begin{code}
+cube : ∅ ⊢ Nat ⇒ Nat
+cube = ƛ (# 0 `* # 0 `* # 0)
+
+_ : cube · con 2 —↠ con 8
+_ = 
+  begin
+    cube · con 2
+  —→⟨ β-ƛ V-con ⟩
+    con 2 `* con 2 `* con 2
+  —→⟨ ξ-*₁ δ-* ⟩
+    con 4 `* con 2
+  —→⟨ δ-* ⟩
+    con 8
+  ∎
+
+exp10 : ∅ ⊢ Nat ⇒ Nat
+exp10 = ƛ (`let (# 0 `* # 0)
+            (`let (# 0 `* # 0)
+              (`let (# 0 `* # 2)
+                (# 0 `* # 0))))
+
+_ : exp10 · con 2 —↠ con 1024
+_ =
+  begin
+    exp10 · con 2
+  —→⟨ β-ƛ V-con ⟩
+    `let (con 2 `* con 2) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
+  —→⟨ ξ-let δ-* ⟩
+    `let (con 4) (`let (# 0 `* # 0) (`let (# 0 `* con 2) (# 0 `* # 0)))
+  —→⟨ β-let V-con ⟩
+    `let (con 4 `* con 4) (`let (# 0 `* con 2) (# 0 `* # 0))
+  —→⟨ ξ-let δ-* ⟩
+    `let (con 16) (`let (# 0 `* con 2) (# 0 `* # 0))
+  —→⟨ β-let V-con ⟩
+    `let (con 16 `* con 2) (# 0 `* # 0)
+  —→⟨ ξ-let δ-* ⟩
+    `let (con 32) (# 0 `* # 0)
+  —→⟨ β-let V-con ⟩
+    con 32 `* con 32
+  —→⟨ δ-* ⟩
+    con 1024
+  ∎
+
 swap× : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
 swap× = ƛ `⟨ `proj₂ (# 0) , `proj₁ (# 0) ⟩
 
@@ -1283,6 +1413,22 @@ _ =
     `⟨ `zero , `tt ⟩
   ∎
 
+swap×-case : ∀ {A B} → ∅ ⊢ A `× B ⇒ B `× A
+swap×-case = ƛ case× (# 0) `⟨ # 0 , # 1 ⟩
+
+_ : swap×-case · `⟨ `tt , `zero ⟩ —↠ `⟨ `zero , `tt ⟩
+_ =
+  begin
+     swap×-case · `⟨ `tt , `zero ⟩
+   —→⟨ β-ƛ V-⟨ V-tt , V-zero ⟩ ⟩
+     case× `⟨ `tt , `zero ⟩ `⟨ # 0 , # 1 ⟩
+   —→⟨ β-case× V-tt V-zero ⟩
+     `⟨ `zero , `tt ⟩
+   ∎
+\end{code}
+
+
+\begin{code}
 swap⊎ : ∀ {A B} → ∅ ⊢ A `⊎ B ⇒ B `⊎ A
 swap⊎ = ƛ (case⊎ (# 0) (`inj₂ (# 0)) (`inj₁ (# 0)))
 
@@ -1298,3 +1444,6 @@ _ =
 \end{code}
 
 
+#### Exercise (`More`)
+
+Formalise the remaining constructs defined in this chapter.

src/plfa/Properties.lagda

@@ -352,9 +352,8 @@ postulate
 ## Prelude to preservation
 
 The other property we wish to prove, preservation of typing under
-reduction, turns out to require considerably more work.  Our proof
+reduction, turns out to require considerably more work.  The proof has
-draws on a line of work by Thorsten Altenkirch, Conor McBride,
+three key steps.
-James McKinna, and others.  The proof has three key steps.
 
 The first step is to show that types are preserved by _renaming_.