changed index to point to TypedDB

index.md

@@ -42,7 +42,7 @@ fixes are encouraged.
   - [Maps: Total and Partial Maps](Maps)
   - [Stlc: The Simply Typed Lambda-Calculus](Stlc)
   - [StlcProp: Properties of STLC](StlcProp)
-  - [Scoped: Scoped and Typed DeBruijn representation](Scoped)
+  - [TypedDB: Typed DeBruijn representation](TypedDB)
 
 ## Backmatter
 

src/Stlc.lagda

@@ -327,8 +327,10 @@ 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
+definition of substitution.  Here we only
-closed terms for values.
+substitute closed terms for variables, while
+the alternative requires the ability to substitute
+open terms for variables.
 
 ## Substitution
 
@@ -342,11 +344,11 @@ For instance, we have
     ⟹
       not · (not · true)
 
-where we substitute `false` for `` `x `` in the body
+where we substitute `not` for `` `f `` in the body
 of the function abstraction.
 
 We write substitution as `N [ x := V ]`, meaning
-substitute term `V` for free occurrences of variable `x` in term `V`,
+substitute term `V` for free occurrences of variable `x` in term `N`,
 or, more compactly, substitute `V` for `x` in `N`.
 Substitution works if `V` is any closed term;
 it need not be a value, but we use `V` since we
@@ -637,9 +639,7 @@ reduction₂ =
   ∎
 \end{code}
 
-<!--
 Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
--->
 
 #### Special characters
 
@@ -861,7 +861,7 @@ or explain why there is no such `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,
+For each of the following, give type `A`, `B`, `C`, and `D` for which it is derivable,
 or explain why there are no such types.
 
 1. `` ∅ ⊢ λ[ y ∶ 𝔹 ⇒ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` y · ` x ∶ A ``

src/StlcProp.lagda

@@ -496,7 +496,7 @@ we show that if `∅ ⊢ V ∶ A` then `Γ ⊢ N [ x := V ] ∶ B`.
 
   - 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.
+We need a lemmas stating that a closed term can be weakened to any context.
 \begin{code}
 weaken-closed : ∀ {V A Γ} → ∅ ⊢ V ∶ A → Γ ⊢ V ∶ A
 weaken-closed {V} {A} {Γ} ⊢V = context-lemma Γ~Γ′ ⊢V

src/TypedDB.lagda

@@ -1,7 +1,7 @@
 ---
 title     : "TypedDB: Typed DeBruijn representation"
 layout    : page
-permalink : /Scoped
+permalink : /TypedDB
 ---
 
 ## Imports
@@ -13,18 +13,16 @@ module TypedDB where
 \begin{code}
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; sym; trans; cong)
--- open Eq.≡-Reasoning
+open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat using (ℕ; zero; suc; _+_; _∸_)
-open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
+open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Data.Unit using (⊤; tt)
+open import Function using (_∘_)
+open import Function.Equivalence using (_⇔_; equivalence)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Nullary.Decidable using (map)
 open import Relation.Nullary.Negation using (contraposition)
 open import Relation.Nullary.Product using (_×-dec_)
-open import Data.Unit using (⊤; tt)
-open import Data.Empty using (⊥; ⊥-elim)
-open import Function using (_∘_)
-open import Function.Equivalence using (_⇔_; equivalence)
 \end{code}
 
 
@@ -77,43 +75,6 @@ data _⊢_ : Env → Type → Set where
     Γ ⊢ B
 \end{code}
 
-## Writing variables as naturals
-
-\begin{code}
-postulate
-  impossible : ⊥
-  _≟Tp_ : ∀ (A B : Type) → Dec (A ≡ B)
-
-conv : ∀ {Γ} {A} → ℕ → Γ ∋ A
-conv {ε} = ⊥-elim impossible
-conv {Γ , B} (suc n) = S (conv n)
-conv {Γ , A} {B} zero with A ≟Tp B
-...                   | yes refl  =  Z
-...                   | no  A≢B   =  ⊥-elim impossible
-
-⌈_⌉ : ∀ {Γ} {A} → ℕ → Γ ⊢ A
-⌈ n ⌉  =  ⌊ conv n ⌋
-\end{code}
-
-## Test examples
-
-\begin{code}
-Ch : Type
-Ch = (o ⇒ o) ⇒ o ⇒ o
-
-plus : ∀ {Γ} → Γ ⊢ Ch ⇒ Ch ⇒ Ch
-plus = ƛ ƛ ƛ ƛ (⌊ S S S Z ⌋ · ⌊ S Z ⌋ · (⌊ S S Z ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋))
-
-two : ∀ {Γ} → Γ ⊢ Ch
-two = ƛ ƛ (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋))
-
-four : ∀ {Γ} → Γ ⊢ Ch
-four = ƛ ƛ (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋))))
-
-four′ : ∀ {Γ} → Γ ⊢ Ch
-four′ = plus · two · two
-\end{code}
-
 ## Decide whether environments and types are equal
 
 \begin{code}
@@ -141,6 +102,44 @@ _≟_ : ∀ (Γ Δ : Env) → Dec (Γ ≡ Δ)
 \end{code}
 
 
+## Writing variables as naturals
+
+This turned out to be a lot harder than expected. Probably not a good idea.
+
+\begin{code}
+postulate
+  impossible : ⊥
+
+conv : ∀ {Γ} {A} → ℕ → Γ ∋ A
+conv {ε} = ⊥-elim impossible
+conv {Γ , B} (suc n) = S (conv n)
+conv {Γ , A} {B} zero with A ≟T B
+...                   | yes refl  =  Z
+...                   | no  A≢B   =  ⊥-elim impossible
+
+var : ∀ {Γ} {A} → ℕ → Γ ⊢ A
+var n  =  ⌊ conv n ⌋
+\end{code}
+
+## Test examples
+
+\begin{code}
+Ch : Type
+Ch = (o ⇒ o) ⇒ o ⇒ o
+
+plus : ∀ {Γ} → Γ ⊢ Ch ⇒ Ch ⇒ Ch
+plus = ƛ ƛ ƛ ƛ ⌊ S S S Z ⌋ · ⌊ S Z ⌋ · (⌊ S S Z ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋)
+
+two : ∀ {Γ} → Γ ⊢ Ch
+two = ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)
+
+four : ∀ {Γ} → Γ ⊢ Ch
+four = ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)))
+
+four′ : ∀ {Γ} → Γ ⊢ Ch
+four′ = plus · two · two
+\end{code}
+
 # Denotational semantics
 
 \begin{code}
@@ -206,12 +205,12 @@ data Normal : ∀ {Γ} {A} → Γ ⊢ A → Set
 data Neutral : ∀ {Γ} {A} → Γ ⊢ A → Set
 
 data Normal where
-  Fun : ∀ {Γ} {A B} {N : Γ , A ⊢ B} → Normal N → Normal (ƛ N)
+  ƛ_  : ∀ {Γ} {A B} {N : Γ , A ⊢ B} → Normal N → Normal (ƛ N)
-  Neu : ∀ {Γ} {A} {M : Γ ⊢ A} → Neutral M → Normal M
+  ⌈_⌉ : ∀ {Γ} {A} {M : Γ ⊢ A} → Neutral M → Normal M
 
 data Neutral where
-  Var : ∀ {Γ} {A} → {n : Γ ∋ A} → Neutral ⌊ n ⌋
+  ⌊_⌋   : ∀ {Γ} {A} → (n : Γ ∋ A) → Neutral ⌊ n ⌋
-  App : ∀ {Γ} {A B} → {L : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} → Neutral L → Normal M → Neutral (L · M)
+  _·_  : ∀ {Γ} {A B} → {L : Γ ⊢ A ⇒ B} {M : Γ ⊢ A} → Neutral L → Normal M → Neutral (L · M)
 \end{code}
 
 ## Reduction step
@@ -247,43 +246,28 @@ data _⟶_ : ∀ {Γ} {A} → Γ ⊢ A → Γ ⊢ A → Set where
 
 \begin{code}
 infix  2 _⟶*_
-
-data _⟶*_ : ∀ {Γ} {A} → Γ ⊢ A → Γ ⊢ A → Set where
-
-  reflexive : ∀ {Γ} {A} {M : Γ ⊢ A} →
-    --------
-    M ⟶* M
-
-  inclusion : ∀ {Γ} {A} {M N : Γ ⊢ A} →
-    M ⟶ N →
-    ---------
-    M ⟶* N
-
-  transitive : ∀ {Γ} {A} {L M N : Γ ⊢ A} →
-    L ⟶* M →
-    M ⟶* N →
-    ----------
-    L ⟶* N
-\end{code}
-
-## Displaying reduction sequences
-
-\begin{code}
 infix 1 begin_
 infixr 2 _⟶⟨_⟩_
 infix 3 _∎
 
+data _⟶*_ : ∀ {Γ} {A} → Γ ⊢ A → Γ ⊢ A → Set where
+
+  _∎ : ∀ {Γ} {A} (M : Γ ⊢ A) →
+    -------------
+    M ⟶* M
+
+  _⟶⟨_⟩_ : ∀ {Γ} {A} (L : Γ ⊢ A) {M N : Γ ⊢ A} →
+    L ⟶ M →
+    M ⟶* N →
+    ---------
+    L ⟶* N
+
 begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M ⟶* N) → (M ⟶* N)
 begin M⟶*N = M⟶*N
-
-_⟶⟨_⟩_ : ∀ {Γ} {A} (L : Γ ⊢ A) {M N : Γ ⊢ A} → (L ⟶ M) → (M ⟶* N) → (L ⟶* N)
-L ⟶⟨ L⟶M ⟩ M⟶*N = transitive (inclusion L⟶M) M⟶*N
-
-_∎ : ∀ {Γ} {A} (M : Γ ⊢ A) → M ⟶* M
-M ∎ = reflexive
 \end{code}
 
-## Example reduction sequence
+
+## Example reduction sequences
 
 \begin{code}
 id : ∀ (A : Type) → ε ⊢ A ⇒ A
@@ -292,65 +276,67 @@ id A = ƛ ⌊ Z ⌋
 _ : id (o ⇒ o) · id o  ⟶* id o
 _ =
   begin
-    id (o ⇒ o) · id o
+    (ƛ ⌊ Z ⌋) · (ƛ ⌊ Z ⌋)
-  ⟶⟨ β (Fun (Neu Var)) ⟩
+  ⟶⟨ β (ƛ ⌈ ⌊ Z ⌋ ⌉) ⟩
-    id o
+    ƛ ⌊ Z ⌋
   ∎
 
-Nmplus : Normal (plus {ε})
-Nmplus = Fun (Fun (Fun (Fun (Neu (App (App Var (Neu Var)) (Neu (App (App Var (Neu Var)) (Neu Var))))))))
-
-Nmtwo : Normal (two {ε})
-Nmtwo =  Fun (Fun (Neu (App Var (Neu (App Var (Neu Var))))))
 
 _ : four′ {ε} ⟶* four {ε}
 _ =
   begin
     plus · two · two
-  ⟶⟨ ξ₁ (β Nmtwo) ⟩
+  ⟶⟨ ξ₁ (β (ƛ (ƛ ⌈ ⌊ S Z ⌋ · ⌈ ⌊ S Z ⌋ · ⌈ ⌊ Z ⌋ ⌉ ⌉ ⌉))) ⟩
-    (ƛ ƛ ƛ (two · ⌊ S Z ⌋ · (⌊ S S Z ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋))) · two
+    (ƛ ƛ ƛ two · ⌊ S Z ⌋ · (⌊ S (S Z) ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋)) · two
-  ⟶⟨ β Nmtwo ⟩
+  ⟶⟨ ξ₁ (ζ (ζ (ζ (ξ₁ (β ⌈ ⌊ S Z ⌋ ⌉))))) ⟩
-    (ƛ ƛ (two · ⌊ S Z ⌋ · (two · ⌊ S Z ⌋ · ⌊ Z ⌋)))
+    (ƛ ƛ ƛ (ƛ ⌊ S (S Z) ⌋ · (⌊ S (S Z) ⌋ · ⌊ Z ⌋)) · (⌊ S (S Z) ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋)) · two
-  ⟶⟨ ζ (ζ (ξ₁ (β (Neu Var)))) ⟩
+  ⟶⟨ ξ₁ (ζ (ζ (ζ (β ⌈ (⌊ S (S Z) ⌋ · ⌈ ⌊ S Z ⌋ ⌉) · ⌈ ⌊ Z ⌋ ⌉ ⌉)))) ⟩
-    (ƛ ƛ ((ƛ (⌊ S S Z ⌋ · (⌊ S S Z ⌋ · ⌊ Z ⌋))) · (two · ⌊ S Z ⌋ · ⌊ Z ⌋)))
+    (ƛ ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S (S Z) ⌋ · ⌊ S Z ⌋ · ⌊ Z ⌋))) · two
-  ⟶⟨ ζ (ζ (ξ₂ (Fun (Neu (App Var (Neu (App Var (Neu Var)))))) (ξ₁ (β (Neu Var))))) ⟩
+  ⟶⟨ β (ƛ (ƛ ⌈ ⌊ S Z ⌋ · ⌈ ⌊ S Z ⌋ · ⌈ ⌊ Z ⌋ ⌉ ⌉ ⌉)) ⟩
-    (ƛ ƛ ((ƛ (⌊ S S Z ⌋ · (⌊ S S Z ⌋ · ⌊ Z ⌋))) · ((ƛ (⌊ S S Z ⌋ · (⌊ S S Z ⌋ · ⌊ Z ⌋))) · ⌊ Z ⌋)))
+    ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · ((ƛ (ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋))) · ⌊ S Z ⌋ · ⌊ Z ⌋))
-  ⟶⟨ ζ (ζ (ξ₂ (Fun (Neu (App Var (Neu (App Var (Neu Var)))))) (β (Neu Var)))) ⟩
+  ⟶⟨ ζ (ζ (ξ₂ ⌈ ⌊ S Z ⌋ ⌉ (ξ₂ ⌈ ⌊ S Z ⌋ ⌉ (ξ₁ (β ⌈ ⌊ S Z ⌋ ⌉))))) ⟩
-    (ƛ ƛ ((ƛ (⌊ S S Z ⌋ · (⌊ S S Z ⌋ · ⌊ Z ⌋))) · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋))))
+    ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · ((ƛ ⌊ S (S Z) ⌋ · (⌊ S (S Z) ⌋ · ⌊ Z ⌋)) · ⌊ Z ⌋))
-  ⟶⟨ ζ (ζ (β (Neu (App Var (Neu (App Var (Neu Var))))))) ⟩
+  ⟶⟨ ζ (ζ (ξ₂ ⌈ ⌊ S Z ⌋ ⌉ (ξ₂ ⌈ ⌊ S Z ⌋ ⌉ (β ⌈ ⌊ Z ⌋ ⌉)))) ⟩
-    (ƛ ƛ (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)))))
+    ƛ ƛ ⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · (⌊ S Z ⌋ · ⌊ Z ⌋)))
   ∎
 \end{code}
 
+
 ## Progress
 
 \begin{code}
-progress : ∀ {Γ} {A} → (M : Γ ⊢ A) → (∃[ N ] (M ⟶ N)) ⊎ Normal M
+data Progress {Γ A} (M : Γ ⊢ A) : Set where
-progress ⌊ x ⌋                                                  =  inj₂ (Neu Var)
+  step : ∀ (N : Γ ⊢ A) → M ⟶ N → Progress M
+  done : Normal M → Progress M
+
+progress : ∀ {Γ} {A} → (M : Γ ⊢ A) → Progress M
+progress ⌊ x ⌋                                                  =  done ⌈ ⌊ x ⌋ ⌉
 progress (ƛ N)       with progress N
-progress (ƛ N)          | inj₁ ⟨ N′ , r ⟩                       =  inj₁ ⟨ ƛ N′ , ζ r ⟩
+progress (ƛ N)          | step N′ r                             =  step (ƛ N′) (ζ r)
-progress (ƛ V)          | inj₂ NmV                              =  inj₂ (Fun NmV)
+progress (ƛ V)          | done NmV                              =  done (ƛ NmV)
 progress (L · M)     with progress L
-progress (L · M)        | inj₁ ⟨ L′ , r ⟩                       =  inj₁ ⟨ L′ · M , ξ₁ r ⟩
+progress (L · M)        | step L′ r                             =  step (L′ · M) (ξ₁ r)
-progress (V · M)        | inj₂ NmV     with progress M
+progress (V · M)        | done NmV     with progress M
-progress (V · M)        | inj₂ NmV        | inj₁ ⟨ M′ , r ⟩     =  inj₁ ⟨ V · M′ , ξ₂ NmV r ⟩
+progress (V · M)        | done NmV        | step M′ r           =  step (V · M′) (ξ₂ NmV r)
-progress (V · W)        | inj₂ (Neu NeV)  | inj₂ NmW            =  inj₂ (Neu (App NeV NmW))
+progress (V · W)        | done ⌈ NeV ⌉    | done NmW            =  done ⌈ NeV · NmW ⌉
-progress ((ƛ V) · W)    | inj₂ (Fun NmV)  | inj₂ NmW            =  inj₁ ⟨ substitute V W , β NmW ⟩
+progress ((ƛ V) · W)    | done (ƛ NmV)    | done NmW            =  step (substitute V W) (β NmW)
 \end{code}
 
 
+## Normalise
+
 \begin{code}
-{-
+data Normalise {Γ A} (M : Γ ⊢ A) : Set where
-ex₃ : progress (app (app plus one) one) ≡
+  out-of-gas : Normalise M
-  inj₁ ⟨ (app (abs (abs (abs (app (app Γone (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z)))))) Γone) , ξ₁ (β Fun) ⟩
+  normal : ∀ (N : Γ ⊢ A) → Normal N → M ⟶* N → Normalise M
-ex₃ = refl
 
-ex₄ : progress (app (abs (abs (abs (app (app Γone (var (S Z))) (app (app (var (S (S Z))) (var (S Z))) (var Z)))))) Γone) ≡
+normalise : ∀ {Γ} {A} → ℕ → (M : Γ ⊢ A) → Normalise M
-  inj₁ ⟨ (abs (abs (app (app Γone (var (S Z))) (app (app Γone (var (S Z))) (var Z))))) , β Fun ⟩
+normalise zero    L                                                =  out-of-gas
-ex₄ = refl
+normalise (suc n) L with progress L
-
+...                    | done NmL                                  =  normal L NmL (L ∎)
-ex₅ : progress (abs (abs (app (app Γone (var (S Z))) (app (app Γone (var (S Z))) (var Z))))) ≡ inj₂ Fun
+...                    | step M L⟶M with normalise n M
-ex₅ = refl  
+...                                      | out-of-gas              =  out-of-gas
-
+...                                      | normal N NmN M⟶*N     =  normal N NmN (L ⟶⟨ L⟶M ⟩ M⟶*N)
--}
 \end{code}
+
+