introduction to De Bruijn

src/plta/DeBruijn.lagda

@@ -8,14 +8,14 @@ permalink : /DeBruijn/
 module plta.DeBruijn where
 \end{code}
 
-The previous two chapters introduced lambda calculus, with
-a formalisation based on named variables, and separate definitions
-of terms and types.  We began with that approach because it is
-traditional, not because it is best.  This chapter presents an
-alternative approach, where named variables are replaced by
-De Bruijn indices and terms are 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 previous two chapters introduced lambda calculus, with a
+formalisation based on named variables, and terms defined separately
+from types.  We began with that approach because it is traditional,
+but it is not the one we recommend.  This chapter presents an
+alternative approach, where named variables are replaced by De Bruijn
+indices and terms are inherently typed.  Our new presentation is more
+compact, using less than half the lines of code required previously to
+do cover the same ground.
 
 ## Imports
 
@@ -34,6 +34,131 @@ open import Relation.Nullary.Negation using (contraposition)
 open import Relation.Nullary.Product using (_×-dec_)
 \end{code}
 
+## Introduction
+
+There is a close correspondence between the structure of a term and
+the structure of the derivation showing that it is well-typed.  For
+example, here is the term for the Church numeral two:
+
+    twoᶜ  : Term
+    twoᶜ  = ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z")
+
+and here is its corresponding type derivation:
+
+    ⊢twoᶜ  :  ∀ {A} ⇒ ∅ ⊢ two ⦂ Ch A
+    ⊢twoᶜ  =  ⊢ƛ (⊢ƛ (Ax ∋s · (Ax ∋s · Ax ∋z)))
+               where    
+               ∋s = S ("s" ≠ "z") Z
+               ∋z = Z
+
+(These are both taken from
+Chapter [Lambda]({{ site.baseurl }}{% link out/plta/Lambda.md %})
+and you can see the corresponding derivation tree written out in full
+[here]({{ site.baseurl }}{% link out/plta/Lambda.md %}/#derivation).)
+The two definitions are in close correspondence, where
+
+  * `` `_ `` corresponds to `Ax`
+  * `ƛ_⇒_`   corresponds to `⊢ƛ`
+  * `_·_`    corresponds to `_·_`
+
+Further, if we think of `Z` as zero and `S` as successor, then the
+lookup derivation for each variable corresponds to a number which
+tells us how many enclosing binding terms to count to find the binding
+of that variable.  Here `"z"` corresponds to `Z` or zero and `"s"`
+corresponds to `S Z` or one.  And, indeed, "z" is bound by the inner
+abstraction (count outward past zero abstractions) and "s" is bound by
+the outer abstraction (count outward past one abstraction).
+
+In this chapter, we are going to exploit this correspondence, and
+introduce a new notation for terms that simultaneously resembles the
+term and its type derivation.  Now we will write the following.
+
+    twoᶜ  :  ∅ ⊢ Ch `ℕ
+    twoᶜ  =  ƛ ƛ (# 1 · (# 1 · # 0))
+
+A variable is represented by a natural number (written with `Z` and `S`, and
+abbreviated in the usual way), and tells us how many enclosing binding terms
+to count to find the binding of that variable. Thus, `# 0` is bound at the
+inner `ƛ`, and `# 1` at the outer `ƛ`.
+
+Replacing variables by numbers in this way is called _De Bruijn
+representation_, and the numbers themselves are called _De Bruijn
+indices_, after the Dutch mathematician Nicolaas Govert (Dick) De
+Bruijn (1918—2012), a pioneer in the creation of proof assistants.
+One advantage of replacing named variables with De Bruijn indices
+is that each term now has a unique representation, rather than being
+represented by the equivalence class of terms under alpha renaming.
+
+The other important feature of our chosen representation is that it is
+_inherently typed_.  In the previous two chapters, the definition of
+terms and the definition of types are completely separate.  All terms
+have type `Term`, and nothing in Agda prevents one from writing a
+nonsense term such as `` `zero · `suc `zero `` which has no type.  Such
+terms that exist independent of types are sometimes called _preterms_
+or _raw terms_.  Here we are going to replace the type `Term` of raw
+terms by the more sophisticated type `Γ ⊢ A` of inherently typed
+terms, which in context `Γ` have type `A`.
+
+While these two choices fit well, they are independent.  One can use
+De Bruijn indices in raw terms, or (with more difficulty) have
+inherently typed terms with names.  In
+Chapter [Untyped]({{ site.baseurl }}{% link out/plta/Untyped.md %},
+we will terms that are not typed with De Bruijn indices
+are inherently scoped.
+
+
+
+
+
+
+
+
+
+
+For each constructor
+of terms `M`, there is a corresponding constructor of type derivations,
+`Γ ⊢ M ⦂ A`:
+
+* `` `_ `` corresponds to `Ax`
+* `ƛ_⇒_` corresponds to `⊢ƛ`
+* `_·_` corresponds to `_·_`
+* `` `zero `` corresponds to `⊢zero`
+* `` `suc_ `` corresponds to `⊢suc`
+* `` `case_[zero⇒_|suc_⇒_] `` corresponds to `⊢case`
+* `μ_⇒_` corresponds to `⊢μ`
+
+Variable names `x` in terms correspond to derivations that
+look up a name in the environment.  There are two constructors of such
+derivations `Z` and `S`, which behave similarly to constructors `here`
+and `there` for looking up elements in a list.  But derivations also
+correspond to a natural number, take `Z` as zero and `S` as successor.
+
+
+
+    ∋s                        ∋s                        ∋z
+    ------------------- `_    ------------------- `_    --------------- `_
+    Γ₂ ⊢ ` "s" ⦂ A ⇒ A        Γ₂ ⊢ ` "s" ⦂ A ⇒ A         Γ₂ ⊢ ` "z" ⦂ A
+    ------------------- `_    ------------------------------------------ _·_
+    Γ₂ ⊢ ` "s" ⦂ A ⇒ A        Γ₂ ⊢ ` "s" · ` "z" ⦂ A
+    -------------------------------------------------- _·_
+    Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ A
+    ---------------------------------------------- ⊢ƛ
+    Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A
+    ------------------------------------------------------------- ⊢ƛ
+    ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (A ⇒ A) ⇒ A ⇒ A
+
+where `∋s` and `∋z` abbreviate the two derivations:
+
+                 ---------------- Z
+    "s" ≢ "z"    Γ₁ ∋ "s" ⦂ A ⇒ A
+    ----------------------------- S        ------------- Z
+    Γ₂ ∋ "s" ⦂ A ⇒ A                       Γ₂ ∋ "z" ⦂ A
+
+and where `Γ₁ = ∅ , s ⦂ A ⇒ A` and `Γ₂ = ∅ , s ⦂ A ⇒ A , z ⦂ A`.
+
+
+
+
 
 ## Syntax
 

src/plta/Lambda.lagda

@@ -149,6 +149,10 @@ four = plus · two · two
 The recursive definition of addition is similar to our original
 definition of `_+_` for naturals, as given in
 Chapter [Naturals]({{ site.baseurl }}{% link out/plta/Naturals.md %}#plus).
+Note that there are two different binding occurrences of the
+variable "m", one in a lambda abstraction and one in a case term;
+the occurrence of "m" in the argument of the case refers to the former
+and the occurrence of "m" in the successor branch of the case refers to the latter.
 Later we will confirm that two plus two is four, in other words that
 the term
 
@@ -1021,41 +1025,43 @@ used with care, since such postulation could allow us to provide
 evidence of _any_ proposition whatsoever, regardless of its truth.
 
 
-### Example type derivations
+### Example type derivations {#derivation}
 
 Type derivations correspond to trees. In informal notation, here
 is a type derivation for the Church numberal two:
 
-    ∋s                        ∋s                        ∋z
-    ------------------- `_    ------------------- `_    --------------- `_
-    Γ₂ ⊢ ` "s" ⦂ A ⇒ A        Γ₂ ⊢ ` "s" ⦂ A ⇒ A         Γ₂ ⊢ ` "z" ⦂ A
-    ------------------- `_    ------------------------------------------ _·_
-    Γ₂ ⊢ ` "s" ⦂ A ⇒ A        Γ₂ ⊢ ` "s" · ` "z" ⦂ A
+                               ∋s                         ∋z
+                               -------------------- `_    --------------- `_
+    ∋s                         Γ₂ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ       Γ₂ ⊢ ` "z" ⦂ `ℕ
+    -------------------- `_    ------------------------------------------ _·_
+    Γ₂ ⊢ ` "s" ⦂ `ℕ ⇒ `ℕ       Γ₂ ⊢ ` "s" · ` "z" ⦂ `ℕ
     -------------------------------------------------- _·_
-    Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ A
+    Γ₂ ⊢ ` "s" · (` "s" · ` "z") ⦂ `ℕ
     ---------------------------------------------- ⊢ƛ
-    Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A
-    ---------------------------------------------------------- ⊢ƛ
-    ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ A ⇒ A
+    Γ₁ ⊢ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ `ℕ ⇒ `ℕ
+    ----------------------------------------------------------------- ⊢ƛ
+    ∅ ⊢ ƛ "s" ⇒ ƛ "z" ⇒ ` "s" · (` "s" · ` "z") ⦂ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ
 
 where `∋s` and `∋z` abbreviate the two derivations:
 
                  ---------------- Z
-    "s" ≢ "z"    Γ₁ ∋ "s" ⦂ A ⇒ A
+    "s" ≢ "z"    Γ₁ ∋ "s" ⦂ `ℕ ⇒ `ℕ
     ----------------------------- S        ------------- Z
-    Γ₂ ∋ "s" ⦂ A ⇒ A                       Γ₂ ∋ "z" ⦂ A
+    Γ₂ ∋ "s" ⦂ `ℕ ⇒ `ℕ                       Γ₂ ∋ "z" ⦂ `ℕ
 
-and where `Γ₁ = ∅ , s ⦂ A ⇒ A` and `Γ₂ = ∅ , s ⦂ A ⇒ A , z ⦂ A`.
+and where ``Γ₁ = ∅ , s ⦂ `ℕ ⇒ `ℕ`` and ``Γ₂ = ∅ , s ⦂ `ℕ ⇒ `ℕ , z ⦂ `ℕ``.
+In fact, `plusᶜ` also has this typing derivation if we replace `∅` by an
+arbitrary context `Γ`, and `` `ℕ `` by an arbitrary type `A`, but the above
+will suffice for our purposes.
 
 Here is the above typing derivation formalised in Agda.
 \begin{code}
 Ch : Type → Type
 Ch A = (A ⇒ A) ⇒ A ⇒ A
 
-⊢twoᶜ : ∀ {A} → ∅ ⊢ twoᶜ ⦂ Ch A
+⊢twoᶜ : ∅ ⊢ twoᶜ ⦂ Ch `ℕ
 ⊢twoᶜ = ⊢ƛ (⊢ƛ (Ax ∋s · (Ax ∋s · Ax ∋z)))
   where
-
   ∋s = S ("s" ≠ "z") Z
   ∋z = Z
 \end{code}
@@ -1087,7 +1093,7 @@ branch of the case expression.
 
 And here are typings for the remainder of the Church example.
 \begin{code}
-⊢plusᶜ : ∀ {A} → ∅ ⊢ plusᶜ ⦂ Ch A ⇒ Ch A ⇒ Ch A
+⊢plusᶜ : ∅ ⊢ plusᶜ ⦂ Ch `ℕ ⇒ Ch `ℕ ⇒ Ch `ℕ
 ⊢plusᶜ = ⊢ƛ (⊢ƛ (⊢ƛ (⊢ƛ (Ax ∋m · Ax ∋s · (Ax ∋n · Ax ∋s · Ax ∋z)))))
   where
   ∋m = S ("m" ≠ "z") (S ("m" ≠ "s") (S ("m" ≠ "n") Z))
@@ -1107,7 +1113,6 @@ And here are typings for the remainder of the Church example.
 ⊢2+2ᶜ = ⊢plusᶜ · ⊢twoᶜ · ⊢twoᶜ · ⊢sucᶜ · ⊢zero
 \end{code}
 
-
 ### Interaction with Agda
 
 Construction of a type derivation may be done interactively.