added confluence to Lambda

extra/stlc/MuDiscussion.lagda

@@ -0,0 +1,47 @@
+Three possible formulations of `μ`
+
+    μ N  —→  N [ μ N ]
+
+    (μ N) · V  —→  N [ μ N , V ]
+
+    (μ (ƛ N)) · V  —→  N [ μ (ƛ N) , V ]
+
+The first is odd in that we substitute for `f` a term that is not a value.
+
+One advantage of the first is that it also works perfectly well on other types.
+For instance,
+
+    case (μ x → suc x) [zero→ zero | suc x → x]
+
+returns (μ x → suc x). 
+
+The second has two values of function type, both lambda abstractions and fixpoints.
+
+What if the body of μ must first reduce to a value? Two cases.
+
+    Value is a lambda.
+
+    (μ f → N) · V
+      —→  (μ f → ƛ x → N′) · V
+      —→  (ƛ x → N′) [ f := μ f → ƛ x → N ] · V
+      —→  (ƛ x → N′ [ f := μ f → ƛ x → N ]) · V
+      —→  N′ [ f := μ f → ƛ x → N , x := V ]
+
+    Value is itself a mu.
+
+    (μ f → μ g → N) · V
+      —→ (μ f → μ g → N′) · V
+      —→ (μ f → μ g → λ x → N″) · V
+      —→ (μ g → λ x → N″) [ f := μ f → μ g → λ x → N″ ] · V
+      —→ (μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]) · V
+      —→ (λ x → N″ [ f := μ f → μ g → λ x → N″ ])
+            [ g := μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ] · V
+      —→ (λ x → N″ [ f := μ f → μ g → λ x → N″ ]
+            [ g := μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]) · V
+      —→ N″ [ f := μ f → μ g → λ x → N″ ]
+             [ g := μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]
+             [ x := V ]
+
+    This is something you would *never* want to do, because f and g are
+    bound to the same function. Better to avoid it by building functions
+    into the syntax, I expect.

src/plta/DeBruijn.lagda

@@ -538,7 +538,8 @@ from variables in one context to variables in another,
 extension yields a map from the first context extended to the
 second context similarly extended.  It looks exactly like the
 old extension lemma, but with all names and terms dropped.
-\begin{code} ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
+\begin{code}
+ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A)
     ----------------------------------
   → (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
 ext ρ Z      =  Z
@@ -784,8 +785,9 @@ define values and reduction.
 
 ### Value
 
-The definition of value is much 
+The definition of value is much as before, save that the
-
+added types incorporate the same information found in the
+Canonical Forms lemma.
 \begin{code}
 data Value : ∀ {Γ A} → Γ ⊢ A → Set where
 
@@ -803,222 +805,221 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
     → Value (`suc V)
 \end{code}
 
-Here `zero` requires an implicit parameter to aid inference (much in the same way that `[]` did in [Lists]({{ site.baseurl }}{% link out/plta/Lists.md %})).
+Here `zero` requires an implicit parameter to aid inference,
+much in the same way that `[]` did in
+[Lists]({{ site.baseurl }}{% link out/plta/Lists.md %})).
 
 ### Reduction step
 
-\begin{code}
+The reduction rules are the same as those given earlier, save
-infix 2 _↦_
+that for each term we must specify its types.  As before, we
+have compatibility rules that reduce a part of a term,
+labelled with `ξ`, and rules that simplify a constructor
+combined with a destructor, labelled with `β`.
 
-data _↦_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+\begin{code}
+infix 2 _—→_
+
+data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
   ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
-    → L ↦ L′
+    → L —→ L′
       -----------------
-    → L · M ↦ L′ · M
+    → L · M —→ L′ · M
 
   ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
     → Value V
-    → M ↦ M′
+    → M —→ M′
       --------------
-    → V · M ↦ V · M′
+    → V · M —→ V · M′
 
   β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
     → Value W
       -------------------
-    → (ƛ N) · W ↦ N [ W ]
+    → (ƛ N) · W —→ N [ W ]
 
   ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
-    → M ↦ M′
+    → M —→ M′
       ----------------
-    → `suc M ↦ `suc M′
+    → `suc M —→ `suc M′
 
   ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
-    → L ↦ L′
+    → L —→ L′
       --------------------------
-    → `case L M N ↦ `case L′ M N
+    → `case L M N —→ `case L′ M N
 
   β-zero :  ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
       -------------------
-    → `case `zero M N ↦ M
+    → `case `zero M N —→ M
 
   β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
     → Value V
-      ----------------------------
+      -----------------------------
-    → `case (`suc V) M N ↦ N [ V ]
+    → `case (`suc V) M N —→ N [ V ]
 
   β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
       ---------------
-    → μ N ↦ N [ μ N ]
+    → μ N —→ N [ μ N ]
 \end{code}
+The definition states that `M —→ N` can only hold of terms `M`
+and `N` which _both_ have type `Γ ⊢ A` for some context `Γ`
+and type `A`.  In other words, it is _built-in_ to our
+definition that reduction preserves types.  There is no
+separate Preservation theorem to prove.  The Agda type-checker
+validates that each term preserves types.  In the case of `β`
+rules, preservation depends on the fact that substitution
+preserves types, which we previously is built-in to our
+definition of substitution.
 
-Two possible formulations of `μ`
-
-    μ N  ↦  N [ μ N ]
-
-    (μ N) · V  ↦  N [ μ N , V ]
-
-    (μ (ƛ N)) · V  ↦  N [ μ (ƛ N) , V ]
-
-The first is odd in that we substitute for `f` a term that is not a value.
-
-The second has two values of function type, both lambda abstractions and fixpoints.
-
-    What if the body of μ must first reduce to a value? Two cases.
-
-    Value is a lambda.
-
-    (μ f → N) · V
-      ↦  (μ f → ƛ x → N′) · V
-      ↦  (ƛ x → N′) [ f := μ f → ƛ x → N ] · V
-      ↦  (ƛ x → N′ [ f := μ f → ƛ x → N ]) · V
-      ↦  N′ [ f := μ f → ƛ x → N , x := V ]
-
-    Value is itself a mu.
-
-    (μ f → μ g → N) · V
-      ↦ (μ f → μ g → N′) · V
-      ↦ (μ f → μ g → λ x → N″) · V
-      ↦ (μ g → λ x → N″) [ f := μ f → μ g → λ x → N″ ] · V
-      ↦ (μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]) · V
-      ↦ (λ x → N″ [ f := μ f → μ g → λ x → N″ ])
-            [ g := μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ] · V
-      ↦ (λ x → N″ [ f := μ f → μ g → λ x → N″ ]
-            [ g := μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]) · V
-      ↦ N″ [ f := μ f → μ g → λ x → N″ ]
-             [ g := μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]
-             [ x := V ]
-
-    This is something you would *never* want to do, because f and g are
-    bound to the same function. Better to avoid it by building functions
-    into the syntax, I expect.
 
 ## Reflexive and transitive closure
 
+The reflexive and transitive closure is exactly as before.
+We simply cut-and-paste the previous definition.
 \begin{code}
-infix  2 _↠_
+infix  2 _—↠_
 infix 1 begin_
-infixr 2 _↦⟨_⟩_
+infixr 2 _—→⟨_⟩_
 infix 3 _∎
 
-data _↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
+data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
 
   _∎ : ∀ {Γ A} (M : Γ ⊢ A)
       --------
-    → M ↠ M
+    → M —↠ M
 
-  _↦⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
+  _—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
-    → L ↦ M
+    → L —→ M
-    → M ↠ N
+    → M —↠ N
       ---------
-    → L ↠ N
+    → L —↠ N
 
-begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M ↠ N) → (M ↠ N)
+begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M —↠ N) → (M —↠ N)
-begin M↠N = M↠N
+begin M—↠N = M—↠N
 \end{code}
 
 
-## Example reduction sequences
+### Examples
 
+We reiterate each of our previous examples.  First, the Church
+numeral two applied to the successor function and zero yields
+the natural number two.
 \begin{code}
-id : ∀ (A : Type) → ∅ ⊢ A ⇒ A
+_ : twoᶜ · sucᶜ · `zero {∅} —↠ `suc `suc `zero
-id A = ƛ ` Z
-
-_ : ∀ {A} → id (A ⇒ A) · id A  ↠ id A
 _ =
   begin
-    (ƛ ` Z) · (ƛ ` Z)
+    twoᶜ · sucᶜ · `zero
-  ↦⟨ β-ƛ V-ƛ ⟩
+  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
-    ƛ ` Z
+    (ƛ (sucᶜ · (sucᶜ · # 0))) · `zero
+  —→⟨ β-ƛ V-zero ⟩
+    sucᶜ · (sucᶜ · `zero)
+  —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
+    sucᶜ · `suc `zero
+  —→⟨ β-ƛ (V-suc V-zero) ⟩
+   `suc (`suc `zero)
   ∎
+\end{code}
+As before, we need to supply an explicit context to `` `zero ``.
 
-_ : plus {∅} · two · two ↠ `suc `suc `suc `suc `zero
+Next, a sample reduction demonstrating that two plus two is four.
+\begin{code}
+_ : plus {∅} · two · two —↠ `suc `suc `suc `suc `zero
 _ =
     plus · two · two
-  ↦⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
+  —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
     (ƛ ƛ `case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two
-  ↦⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
+  —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
     (ƛ `case two (` Z) (`suc (plus · ` Z · ` S Z))) · two
-  ↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
+  —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
     `case two two (`suc (plus · ` Z · two))
-  ↦⟨ β-suc (V-suc V-zero) ⟩
+  —→⟨ β-suc (V-suc V-zero) ⟩
     `suc (plus · `suc `zero · two)
-  ↦⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
+  —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
     `suc ((ƛ ƛ `case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
       · `suc `zero · two)
-  ↦⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
+  —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
     `suc ((ƛ `case (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two)
-  ↦⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
+  —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
     `suc (`case (`suc `zero) (two) (`suc (plus · ` Z · two)))
-  ↦⟨ ξ-suc (β-suc V-zero) ⟩
+  —→⟨ ξ-suc (β-suc V-zero) ⟩
     `suc (`suc (plus · `zero · two))
-  ↦⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
+  —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
     `suc (`suc ((ƛ ƛ `case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
       · `zero · two))
-  ↦⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
+  —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
     `suc (`suc ((ƛ `case `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two))
-  ↦⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
+  —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
     `suc (`suc (`case `zero (two) (`suc (plus · ` Z · two))))
-  ↦⟨ ξ-suc (ξ-suc β-zero) ⟩
+  —→⟨ ξ-suc (ξ-suc β-zero) ⟩
    `suc (`suc (`suc (`suc `zero)))
   ∎
 \end{code}
 
+And finally, a similar sample reduction for Church numerals.
 \begin{code}
-_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero ↠ `suc `suc `suc `suc `zero {∅}
+_ : plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero —↠ `suc `suc `suc `suc `zero {∅}
 _ =
   begin
     plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero
-  ↦⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
+  —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
     (ƛ ƛ ƛ twoᶜ · ` S Z · (` S S Z · ` S Z · ` Z)) · twoᶜ · sucᶜ · `zero
-  ↦⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
+  —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
     (ƛ ƛ twoᶜ · ` S Z · (twoᶜ · ` S Z · ` Z)) · sucᶜ · `zero
-  ↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
+  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
     (ƛ twoᶜ · sucᶜ · (twoᶜ · sucᶜ · ` Z)) · `zero
-  ↦⟨ β-ƛ V-zero ⟩
+  —→⟨ β-ƛ V-zero ⟩
     twoᶜ · sucᶜ · (twoᶜ · sucᶜ · `zero)
-  ↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
+  —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
     (ƛ sucᶜ · (sucᶜ · ` Z)) · (twoᶜ · sucᶜ · `zero)
-  ↦⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
+  —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
     (ƛ sucᶜ · (sucᶜ · ` Z)) · ((ƛ sucᶜ · (sucᶜ · ` Z)) · `zero)
-  ↦⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
+  —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
     (ƛ sucᶜ · (sucᶜ · ` Z)) · (sucᶜ · (sucᶜ · `zero))
-  ↦⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
+  —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
     (ƛ sucᶜ · (sucᶜ · ` Z)) · (sucᶜ · `suc `zero)
-  ↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
+  —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
     (ƛ sucᶜ · (sucᶜ · ` Z)) · `suc (`suc `zero)
-  ↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
+  —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
     sucᶜ · (sucᶜ · `suc (`suc `zero))
-  ↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
+  —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
     sucᶜ · `suc (`suc (`suc `zero))
-  ↦⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
+  —→⟨ β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
     `suc (`suc (`suc (`suc `zero)))
   ∎
 \end{code}
 
 ## Values do not reduce
 
-Values do not reduce.
+We have now completed all the definitions, which of
-\begin{code}
+necessity included some important results: Canonical Forms,
-Value-lemma : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M ↦ N)
+Substitution preserves types, and Preservation.
-Value-lemma V-ƛ ()
+We now turn to proving the remaining results from the
-Value-lemma V-zero ()
+preceding section.
-Value-lemma (V-suc VM) (ξ-suc M↦N)  =  Value-lemma VM M↦N
-\end{code}
 
-As a corollary, terms that reduce are not values.
+### Exercise `V¬—→`, `—→¬V`
-\begin{code}
-↦-corollary : ∀ {Γ A} {M N : Γ ⊢ A} → (M ↦ N) → ¬ Value M
-↦-corollary M↦N VM  =  Value-lemma VM M↦N
-\end{code}
 
+Adapt the reesults of the previous section to show values do
+not reduce, and its corollary, terms that reduce are not
+values.
+
+<!--
+\begin{code}
+V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M —→ N)
+V¬—→ V-ƛ        ()
+V¬—→ V-zero     ()
+V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N
+
+—→¬V : ∀ {Γ A} {M N : Γ ⊢ A} → (M —→ N) → ¬ Value M
+—→¬V M—→N VM  =  V¬—→ VM M—→N
+\end{code}
+-->
 
 ## Progress
 
 \begin{code}
 data Progress {A} (M : ∅ ⊢ A) : Set where
   step : ∀ {N : ∅ ⊢ A}
-    → M ↦ N
+    → M —→ N
       -------------
     → Progress M
   done :
@@ -1030,16 +1031,16 @@ progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
 progress (` ())
 progress (ƛ N)                            =  done V-ƛ
 progress (L · M) with progress L
-...    | step L↦L′                      =  step (ξ-·₁ L↦L′)
+...    | step L—→L′                      =  step (ξ-·₁ L—→L′)
 ...    | done V-ƛ with progress M
-...        | step M↦M′                  =  step (ξ-·₂ V-ƛ M↦M′)
+...        | step M—→M′                  =  step (ξ-·₂ V-ƛ M—→M′)
 ...        | done VM                      =  step (β-ƛ VM)
 progress (`zero)                          =  done V-zero
 progress (`suc M) with progress M
-...    | step M↦M′                      =  step (ξ-suc M↦M′)
+...    | step M—→M′                      =  step (ξ-suc M—→M′)
 ...    | done VM                          =  done (V-suc VM)
 progress (`case L M N) with progress L
-...    | step L↦L′                       =  step (ξ-case L↦L′)
+...    | step L—→L′                       =  step (ξ-case L—→L′)
 ...    | done V-zero                         =  step (β-zero)
 ...    | done (V-suc VL)                     =  step (β-suc VL)
 progress (μ N)                             =  step (β-μ)
@@ -1075,7 +1076,7 @@ reduction finished.
 data Steps : ∀ {A} → ∅ ⊢ A → Set where
 
   steps : ∀ {A} {L N : ∅ ⊢ A}
-    → L ↠ N
+    → L —↠ N
     → Finished N
       ----------
     → Steps L
@@ -1091,8 +1092,8 @@ eval : ∀ {A}
 eval (gas zero)    L                     =  steps (L ∎) out-of-gas
 eval (gas (suc m)) L with progress L
 ... | done VL                            =  steps (L ∎) (done VL)
-... | step {M} L↦M with eval (gas m) M
+... | step {M} L—→M with eval (gas m) M
-...    | steps M↠N fin                   =  steps (L ↦⟨ L↦M ⟩ M↠N) fin
+...    | steps M—↠N fin                   =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
 \end{code}
 
 ## Examples
@@ -1106,7 +1107,7 @@ _ : eval (gas 100) (plus · two · two) ≡
       `case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
    · `suc (`suc `zero)
    · `suc (`suc `zero)
-   ↦⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
+   —→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
    (ƛ
     (ƛ
      `case (` (S Z)) (` Z)
@@ -1119,7 +1120,7 @@ _ : eval (gas 100) (plus · two · two) ≡
        · ` (S Z)))))
    · `suc (`suc `zero)
    · `suc (`suc `zero)
-   ↦⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
+   —→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
    (ƛ
     `case (`suc (`suc `zero)) (` Z)
     (`suc
@@ -1130,7 +1131,7 @@ _ : eval (gas 100) (plus · two · two) ≡
       · ` Z
       · ` (S Z))))
    · `suc (`suc `zero)
-   ↦⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
+   —→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
    `case (`suc (`suc `zero)) (`suc (`suc `zero))
    (`suc
     ((μ
@@ -1139,7 +1140,7 @@ _ : eval (gas 100) (plus · two · two) ≡
         `case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
      · ` Z
      · `suc (`suc `zero)))
-   ↦⟨ β-suc (V-suc V-zero) ⟩
+   —→⟨ β-suc (V-suc V-zero) ⟩
    `suc
    ((μ
      (ƛ
@@ -1147,7 +1148,7 @@ _ : eval (gas 100) (plus · two · two) ≡
        `case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
     · `suc `zero
     · `suc (`suc `zero))
-   ↦⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
+   —→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
    `suc
    ((ƛ
      (ƛ
@@ -1161,7 +1162,7 @@ _ : eval (gas 100) (plus · two · two) ≡
         · ` (S Z)))))
     · `suc `zero
     · `suc (`suc `zero))
-   ↦⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
+   —→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
    `suc
    ((ƛ
      `case (`suc `zero) (` Z)
@@ -1173,7 +1174,7 @@ _ : eval (gas 100) (plus · two · two) ≡
        · ` Z
        · ` (S Z))))
     · `suc (`suc `zero))
-   ↦⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
+   —→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
    `suc
    `case (`suc `zero) (`suc (`suc `zero))
    (`suc
@@ -1183,7 +1184,7 @@ _ : eval (gas 100) (plus · two · two) ≡
         `case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
      · ` Z
      · `suc (`suc `zero)))
-   ↦⟨ ξ-suc (β-suc V-zero) ⟩
+   —→⟨ ξ-suc (β-suc V-zero) ⟩
    `suc
    (`suc
     ((μ
@@ -1192,7 +1193,7 @@ _ : eval (gas 100) (plus · two · two) ≡
         `case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
      · `zero
      · `suc (`suc `zero)))
-   ↦⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
+   —→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
    `suc
    (`suc
     ((ƛ
@@ -1207,7 +1208,7 @@ _ : eval (gas 100) (plus · two · two) ≡
          · ` (S Z)))))
      · `zero
      · `suc (`suc `zero)))
-   ↦⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
+   —→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
    `suc
    (`suc
     ((ƛ
@@ -1220,7 +1221,7 @@ _ : eval (gas 100) (plus · two · two) ≡
         · ` Z
         · ` (S Z))))
      · `suc (`suc `zero)))
-   ↦⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
+   —→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
    `suc
    (`suc
     `case `zero (`suc (`suc `zero))
@@ -1231,7 +1232,7 @@ _ : eval (gas 100) (plus · two · two) ≡
          `case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
       · ` Z
       · `suc (`suc `zero))))
-   ↦⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
+   —→⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
 _ = refl
 \end{code}
@@ -1246,7 +1247,7 @@ _ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
    · (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z)))
    · (ƛ `suc (` Z))
    · `zero
-   ↦⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
+   —→⟨ ξ-·₁ (ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ))) ⟩
    (ƛ
     (ƛ
      (ƛ
@@ -1255,39 +1256,39 @@ _ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
    · (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z)))
    · (ƛ `suc (` Z))
    · `zero
-   ↦⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
+   —→⟨ ξ-·₁ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ
     (ƛ
      (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · ` (S Z) ·
      ((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · ` (S Z) · ` Z)))
    · (ƛ `suc (` Z))
    · `zero
-   ↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
+   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ
     (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc (` Z)) ·
     ((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc (` Z)) · ` Z))
    · `zero
-   ↦⟨ β-ƛ V-zero ⟩
+   —→⟨ β-ƛ V-zero ⟩
    (ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc (` Z)) ·
    ((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc (` Z)) · `zero)
-   ↦⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
+   —→⟨ ξ-·₁ (β-ƛ V-ƛ) ⟩
    (ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) ·
    ((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc (` Z)) · `zero)
-   ↦⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
+   —→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-ƛ)) ⟩
    (ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) ·
    ((ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) · `zero)
-   ↦⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
+   —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
    (ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) ·
    ((ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · `zero))
-   ↦⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
+   —→⟨ ξ-·₂ V-ƛ (ξ-·₂ V-ƛ (β-ƛ V-zero)) ⟩
    (ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) ·
    ((ƛ `suc (` Z)) · `suc `zero)
-   ↦⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
+   —→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
-   (ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) · `suc (`suc `zero) ↦⟨
+   (ƛ (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · ` Z)) · `suc (`suc `zero) —→⟨
    β-ƛ (V-suc (V-suc V-zero)) ⟩
-   (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · `suc (`suc `zero)) ↦⟨
+   (ƛ `suc (` Z)) · ((ƛ `suc (` Z)) · `suc (`suc `zero)) —→⟨
    ξ-·₂ V-ƛ (β-ƛ (V-suc (V-suc V-zero))) ⟩
-   (ƛ `suc (` Z)) · `suc (`suc (`suc `zero)) ↦⟨
+   (ƛ `suc (` Z)) · `suc (`suc (`suc `zero)) —→⟨
    β-ƛ (V-suc (V-suc (V-suc V-zero))) ⟩
    `suc (`suc (`suc (`suc `zero))) ∎)
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))

src/plta/Lambda.lagda

@@ -537,14 +537,17 @@ consist of a constructor and a deconstructor, in our case `λ` and `·`,
 which reduces directly.  We give them names starting with the Greek
 letter `β` (_beta_) and such rules are traditionally called _beta rules_.
 
-The rules are deterministic, in that at most one rule applies to every
+If a term is a value, then no reduction applies; conversely,
-term.  We will show in the next chapter that for every well-typed term
+if a reduction applies to a term then it is not a value.
+We will show in the next chapter that for well-typed terms
+this exhausts the possibilities: for every well-typed term
 either a reduction applies or it is a value.
 
 For numbers, zero does not reduce and successor reduces the subterm.
 A case expression reduces its argument to a number, and then chooses
 the zero or successor branch as appropriate.  A fixpoint replaces
-the bound variable by the entire fixpoint term.
+the bound variable by the entire fixpoint term; this is the one
+case where we substitute by a term that is not a value.
 
 Here are the rules formalised in Agda.
 
@@ -695,9 +698,53 @@ data _—↠′_ : Term → Term → Set where
     → L —↠′ N
 \end{code}
 The three constructors specify, respectively, that `—↠` includes `—→`
-and is reflexive and transitive.
+and is reflexive and transitive.  A good exercise is to show that
+the two definitions are equivalent (indeed, isomoprhic).
 
-It is a straightforward exercise to show the two are equivalent.
+One important property a reduction relation might satisfy is
+to be _confluent_.  If term `L` reduces to two other terms,
+`M` and `N`, then both of these reduce to a common term `P`.
+It can be illustrated as follows.
+
+               L
+              / \
+             /   \
+            /     \
+           M       N
+            \     /
+             \   /
+              \ /
+               P
+
+Here `L`, `M`, `N` are universally quantified while `P`
+is existentially quantified.  If each line stand for zero
+or more reduction steps, this is called confluence,
+while if each line stands a single reduction step it is
+called the _diamond property_.  In symbols:
+
+    confluence : ∀ {L M N} → ∃[ P ]
+      ( ((L —↠ M) × (L —↠ N))
+        --------------------
+      → ((M —↠ P) × (M —↠ P)) )
+
+    diamond : ∀ {L M N} → ∃[ P ]
+      ( ((L —↠ M) × (L —↠ N))
+        --------------------
+      → ((M —↠ P) × (M —↠ P)) )
+
+All of the reduction systems studied in this text are determistic.
+In symbols:
+
+    deterministic : ∀ {L M N}
+      → L —→ M
+      → L —→ N
+        ------
+      → M ≡ N
+
+It is easy to show that every deterministic relation satisfies
+the diamond property, and that every relation that satisfies
+the diamond property is confluent.  Hence, all the reduction
+systems studied in this text are trivially confluent.
 
 #### Exercise (`—↠≃—↠′`)
 

src/plta/Properties.lagda

@@ -120,94 +120,6 @@ If we expand out the negations, we have
 
 which are the same function with the arguments swapped.
 
-## Reduction is deterministic
-
-Reduction is deterministic: for any term, there is at most
-one other term to which it reduces.
-
-A case term takes four arguments (three subterms and a bound
-variable), and to complete our proof we will need a variant
-of congruence to deal with functions of four arguments.  It
-is exactly analogous to `cong` and `cong₂` as defined previously.
-\begin{code}
-cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E)
-  {s w : A} {t x : B} {u y : C} {v z : D}
-  → s ≡ w → t ≡ x → u ≡ y → v ≡ z → f s t u v ≡ f w x y z
-cong₄ f refl refl refl refl = refl
-\end{code}
-
-It is now straightforward to show that reduction is deterministic.
-\begin{code}
-det : ∀ {M M′ M″}
-  → (M —→ M′)
-  → (M —→ M″)
-    --------
-  → M′ ≡ M″
-det (ξ-·₁ L—→L′)   (ξ-·₁ L—→L″)     =  cong₂ _·_ (det L—→L′ L—→L″) refl
-det (ξ-·₁ L—→L′)   (ξ-·₂ VL M—→M″)  =  ⊥-elim (V¬—→ VL L—→L′)
-det (ξ-·₁ L—→L′)   (β-ƛ _)          =  ⊥-elim (V¬—→ V-ƛ L—→L′)
-det (ξ-·₂ VL _)   (ξ-·₁ L—→L″)      =  ⊥-elim (V¬—→ VL L—→L″)
-det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″)   =  cong₂ _·_ refl (det M—→M′ M—→M″)
-det (ξ-·₂ _ M—→M′) (β-ƛ VM)         =  ⊥-elim (V¬—→ VM M—→M′)
-det (β-ƛ _)       (ξ-·₁ L—→L″)      =  ⊥-elim (V¬—→ V-ƛ L—→L″)
-det (β-ƛ VM)      (ξ-·₂ _ M—→M″)    =  ⊥-elim (V¬—→ VM M—→M″)
-det (β-ƛ _)       (β-ƛ _)           =  refl
-det (ξ-suc M—→M′)  (ξ-suc M—→M″)    =  cong `suc_ (det M—→M′ M—→M″)
-det (ξ-case L—→L′) (ξ-case L—→L″)   =  cong₄ `case_[zero⇒_|suc_⇒_]
-                                         (det L—→L′ L—→L″) refl refl refl
-det (ξ-case L—→L′) β-zero           =  ⊥-elim (V¬—→ V-zero L—→L′)
-det (ξ-case L—→L′) (β-suc VL)       =  ⊥-elim (V¬—→ (V-suc VL) L—→L′)
-det β-zero        (ξ-case M—→M″)    =  ⊥-elim (V¬—→ V-zero M—→M″)
-det β-zero        β-zero            =  refl
-det (β-suc VL)    (ξ-case L—→L″)    =  ⊥-elim (V¬—→ (V-suc VL) L—→L″)
-det (β-suc _)     (β-suc _)         =  refl
-det β-μ           β-μ               =  refl
-\end{code}
-The proof is by induction over possible reductions.  We consider
-three typical cases.
-
-* Two instances of `ξ-·₁`.
-
-      L —→ L′                 L —→ L″
-      -------------- ξ-·₁    -------------- ξ-·₁
-      L · M —→ L′ · M         L · M —→ L″ · M
-
-  By induction we have `L′ ≡ L″`, and hence by congruence
-  `L′ · M ≡ L″ · M`.
-  
-* An instance of `ξ-·₁` and an instance of `ξ-·₂`.
-
-                             Value L
-      L —→ L′                 M —→ M″
-      -------------- ξ-·₁    -------------- ξ-·₂
-      L · M —→ L′ · M         L · M —→ L · M″
-
-  The rule on the left requires `L` to reduce, but the rule on the right
-  requires `L` to be a value.  This is a contradiction since values do
-  not reduce.  If the value constraint was removed from `ξ-·₂`, or from
-  one of the other reduction rules, then determinism would no longer hold.
-
-* Two instances of `β-ƛ`.
-
-      Value V                             Value V                         
-      ---------------------------- β-ƛ    ---------------------------- β-ƛ
-      (ƛ x ⇒ N) · V —→ N [ x := V ]        (ƛ x ⇒ N) · V —→ N [ x := V ]
-
-  Since the left-hand sides are identical, the right-hand sides are
-  also identical.
-
-Almost half the lines in the above proof are redundant, e.g., the case
-when one rule is `ξ-·₁` and the other is `ξ-·₂` is considered twice,
-once with `ξ-·₁` first and `ξ-·₂` second, and the other time with the
-two swapped.  What we might like to do is delete the redundant lines
-and add
-
-    det M—→M′ M—→M″ = sym (det M—→M″ M—→M′)
-
-to the bottom of the proof. But this does not work. The termination
-checker complains, because the arguments have merely switched order
-and neither is smaller.
-
 
 ## Canonical Forms
 
@@ -668,7 +580,6 @@ we require an arbitrary context `Γ`, as in the statement of the lemma.
 Here is the formal statement and proof that substitution preserves types.
 \begin{code}
 subst : ∀ {Γ y N V A B}
-  → ∅ ⊢ V ⦂ B
   → Γ , y ⦂ B ⊢ N ⦂ A
     --------------------
   → Γ ⊢ N [ y := V ] ⦂ A
@@ -1454,6 +1365,98 @@ wttdgs′ ⊢M M—↠N  =  unstuck′ (preserves′ ⊢M M—↠N)
 \end{code}
 
 
+## Reduction is deterministic
+
+When we introduced reduction, we claimed it was deterministic:
+for any term, there is at most one other term to which it reduces.
+
+A case term takes four arguments (three subterms and a bound
+variable), and to complete our proof we will need a variant
+of congruence to deal with functions of four arguments.  It
+is exactly analogous to `cong` and `cong₂` as defined previously.
+\begin{code}
+cong₄ : ∀ {A B C D E : Set} (f : A → B → C → D → E)
+  {s w : A} {t x : B} {u y : C} {v z : D}
+  → s ≡ w → t ≡ x → u ≡ y → v ≡ z → f s t u v ≡ f w x y z
+cong₄ f refl refl refl refl = refl
+\end{code}
+
+It is now straightforward to show that reduction is deterministic.
+\begin{code}
+det : ∀ {M M′ M″}
+  → (M —→ M′)
+  → (M —→ M″)
+    --------
+  → M′ ≡ M″
+det (ξ-·₁ L—→L′)   (ξ-·₁ L—→L″)     =  cong₂ _·_ (det L—→L′ L—→L″) refl
+det (ξ-·₁ L—→L′)   (ξ-·₂ VL M—→M″)  =  ⊥-elim (V¬—→ VL L—→L′)
+det (ξ-·₁ L—→L′)   (β-ƛ _)          =  ⊥-elim (V¬—→ V-ƛ L—→L′)
+det (ξ-·₂ VL _)   (ξ-·₁ L—→L″)      =  ⊥-elim (V¬—→ VL L—→L″)
+det (ξ-·₂ _ M—→M′) (ξ-·₂ _ M—→M″)   =  cong₂ _·_ refl (det M—→M′ M—→M″)
+det (ξ-·₂ _ M—→M′) (β-ƛ VM)         =  ⊥-elim (V¬—→ VM M—→M′)
+det (β-ƛ _)       (ξ-·₁ L—→L″)      =  ⊥-elim (V¬—→ V-ƛ L—→L″)
+det (β-ƛ VM)      (ξ-·₂ _ M—→M″)    =  ⊥-elim (V¬—→ VM M—→M″)
+det (β-ƛ _)       (β-ƛ _)           =  refl
+det (ξ-suc M—→M′)  (ξ-suc M—→M″)    =  cong `suc_ (det M—→M′ M—→M″)
+det (ξ-case L—→L′) (ξ-case L—→L″)   =  cong₄ `case_[zero⇒_|suc_⇒_]
+                                         (det L—→L′ L—→L″) refl refl refl
+det (ξ-case L—→L′) β-zero           =  ⊥-elim (V¬—→ V-zero L—→L′)
+det (ξ-case L—→L′) (β-suc VL)       =  ⊥-elim (V¬—→ (V-suc VL) L—→L′)
+det β-zero        (ξ-case M—→M″)    =  ⊥-elim (V¬—→ V-zero M—→M″)
+det β-zero        β-zero            =  refl
+det (β-suc VL)    (ξ-case L—→L″)    =  ⊥-elim (V¬—→ (V-suc VL) L—→L″)
+det (β-suc _)     (β-suc _)         =  refl
+det β-μ           β-μ               =  refl
+\end{code}
+The proof is by induction over possible reductions.  We consider
+three typical cases.
+
+* Two instances of `ξ-·₁`.
+
+      L —→ L′                 L —→ L″
+      -------------- ξ-·₁    -------------- ξ-·₁
+      L · M —→ L′ · M         L · M —→ L″ · M
+
+  By induction we have `L′ ≡ L″`, and hence by congruence
+  `L′ · M ≡ L″ · M`.
+  
+* An instance of `ξ-·₁` and an instance of `ξ-·₂`.
+
+                             Value L
+      L —→ L′                 M —→ M″
+      -------------- ξ-·₁    -------------- ξ-·₂
+      L · M —→ L′ · M         L · M —→ L · M″
+
+  The rule on the left requires `L` to reduce, but the rule on the right
+  requires `L` to be a value.  This is a contradiction since values do
+  not reduce.  If the value constraint was removed from `ξ-·₂`, or from
+  one of the other reduction rules, then determinism would no longer hold.
+
+* Two instances of `β-ƛ`.
+
+      Value V                             Value V                         
+      ---------------------------- β-ƛ    ---------------------------- β-ƛ
+      (ƛ x ⇒ N) · V —→ N [ x := V ]        (ƛ x ⇒ N) · V —→ N [ x := V ]
+
+  Since the left-hand sides are identical, the right-hand sides are
+  also identical.
+
+Almost half the lines in the above proof are redundant, e.g., the case
+when one rule is `ξ-·₁` and the other is `ξ-·₂` is considered twice,
+once with `ξ-·₁` first and `ξ-·₂` second, and the other time with the
+two swapped.  What we might like to do is delete the redundant lines
+and add
+
+    det M—→M′ M—→M″ = sym (det M—→M″ M—→M′)
+
+to the bottom of the proof. But this does not work. The termination
+checker complains, because the arguments have merely switched order
+and neither is smaller.
+
+
+
+
+
 #### Exercise: `progress-preservation`
 
 Without peeking at their statements above, write down the progress