From 3b62e81c06eedf41884b7dd4bbefb3dfe04a7981 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Mon, 17 Jul 2017 16:06:36 +0100 Subject: [PATCH] minor fixes to Stlc --- out/Stlc.md | 4829 ++++++++++++++++++++++++------------------------ src/Stlc.lagda | 29 +- 2 files changed, 2426 insertions(+), 2432 deletions(-) diff --git a/out/Stlc.md b/out/Stlc.md index a3a71733..069d4a8e 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -613,11 +613,11 @@ And here it is formalised in Agda. 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) + ⇒ 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 @@ -658,246 +658,246 @@ and applies the function to the boolean twice. 
 
-f x y : Id
-f  =  id : Id
+f  =  id 0
 x  =  id 1
 y  =  id 2
 
 not two : Term 
-not =  λ[ x ∶Term 
+not 𝔹=  λ[ ] (ifx `∶ x𝔹 ] (if ` x then false else true)
-two =  λ[true) f ∶
+two 𝔹= ⇒ 𝔹  λ[ ]f λ[ x ∶ 𝔹 ⇒ 𝔹 ] `λ[ fx ·∶ (`𝔹 ] ` f · ` x(` f · ` x)
 
@@ -969,384 +969,381 @@ currying. This is made more convenient by declaring `_⇒_` to
 associate to the right and `_·_` to associate to the left.
 Thus,
 
-> `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)`,
-
-and similarly,
-
-> `two · not · true` abbreviates `(two · not) · true`.
+* `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` 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) ``.
+* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` abbreviates
+  `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` and not
+  `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``.
 
 
 
-ex₁ : (𝔹 ⇒ 𝔹) (𝔹 ⇒ 𝔹 ⇒ 𝔹) ⇒≡ (𝔹 ⇒ 𝔹 ≡) (𝔹 ⇒ (𝔹 𝔹) ⇒ 𝔹) (𝔹 ⇒ 𝔹)
 ex₁ = refl
 
 ex₂ : two · :not two· · not · true ≡ (two · not) · true
 ex₂ = refl
 
 ex₃ : λ[ f ∶ 𝔹 ⇒ f𝔹 ∶] 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] x` ∶f 𝔹· ] ` f · (` f · ` x)
       ≡ (λ[ f ∶ (λ[𝔹 ⇒ f𝔹 ∶] 𝔹 ⇒(λ[ 𝔹x ]∶ (λ[𝔹 ] x ∶ 𝔹 ] (` f · (` f · ` x))))
 ex₃ = refl
 
@@ -1398,130 +1395,130 @@ The predicate `Value M` holds if term `M` is a value.
 
 
 
-data Value : Value : Term → Set where
   value-λ     : ∀ {x A N} {x→ A N}Value →(λ[ Valuex ∶ (λ[A ] x ∶ A ] N)
   value-true  : Value true
   value-false : Value : Value false
 
@@ -1594,646 +1591,646 @@ Here is the formal definition in Agda.
 
 
 
-_[_:=_] : Term → Id → Term → Term
+(` Term
-(`x′) [ x x′) [ x := V ] with x ≟ x′
 ... | yes _ |= yes _V
+... =| V
-...no  _ |= no  _ = ` x′
 (λ[ x′ ∶ A′ x′] ∶N′) A′[ ]x N′) [ x := V ] with x ≟ x′
 ... | yes _ |= yesλ[ _x′ =∶ λ[A′ x′ ∶ A′ ] N′
 ... | no  _ |= noλ[  _ x′ =∶ λ[A′ x′] ∶(N′ A′[ ]x (N′ [ x := V ])
 (L′ · M′) [ ·x M′) [ x := V ] =  (L′ [ x := V ]) :=· V(M′ ])[ ·x (M′:= [V x]) := V ])
 (true) [ x := V ] = true
+(false)
-(false) [ x := V ] = false
 (if L′ then L′M′ thenelse M′N′) else[ x N′) [ x := V ] =
   if (L′ [ x (L′:= [V x]) := Vthen ])(M′ then[ x (M′:= [V x]) := Velse ])(N′ else[ x (N′ [ x := V ])
 
@@ -2265,666 +2262,666 @@ Here is confirmation that the examples above are correct.
 
 
 
-ex₁₁ : ` f [ :f ` f [ f := not ] ≡  not
 ex₁₁ = refl
 
 ex₁₂ : true [ f := not ] ≡ not ] ≡ true
 ex₁₂ = refl
 
 ex₁₃ : (` f · true) ·[ true) [ f := not ] ≡ not ]· ≡ not · true
 ex₁₃ = refl
 
 ex₁₄ : (` f · (` f · true)) [ f := not ] ≡ not ]· ≡ not · (not · true)
 ex₁₄ = refl
 
 ex₁₅ : (λ[ x :∶ (λ[𝔹 ] x` ∶f 𝔹· ] ` f · (` f · ` x)) ·[ `f x)) [ f := not ] ≡ not ] ≡ λ[ x ∶ 𝔹 ] x ∶not 𝔹· ] not · (not · ` x)
+ex₁₅ x)
-ex₁₅ = refl
 
 ex₁₆ : (λ[ y :∶ (λ[𝔹 ] y` ∶ 𝔹 ] ` y) [ x := true := true ] ≡ λ[ y ∶ 𝔹 ] y` ∶ 𝔹 ] ` y
 ex₁₆ = refl
 
 ex₁₇ : (λ[ x :∶ (λ[𝔹 ] x` ∶ 𝔹 ] ` x) [ x := true := true ] ≡ λ[ x ∶ 𝔹 ] x` ∶ 𝔹 ] ` x
 ex₁₇ = refl
 
@@ -2996,200 +2993,216 @@ and indeed such rules are traditionally called beta rules.
 
 
 
-infix 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
   ξ·₁ : ∀ {L L′ ∀ {L L′ M} →
+    L →⟹ L′ →
     L ⟹ L′ →·
-    L · M ⟹ L′ · M
   ξ·₂ : ∀ {V M M′} →
     Value V →
+    M →⟹ M′ →
     M ⟹ M′V →·
-     M ⟹ V · M ⟹ V · M′
   βλ· : ∀ {x A N V} → Value →V Value V →
     (λ[ x ∶ A ] x ∶ A ] N) · V ⟹ N ·[ Vx ⟹ N [ x := V ]
+  ξif ]
-  ξif : ∀ {L L′ ∀M {LN} L′ M N}→
+    L →
-    L ⟹ L′ →    
     if L then M else N ⟹ if L′ ⟹ ifthen L′ then M else N
   βif-true : ∀ {M N} ∀ {M N} →
     if true then M else N ⟹ M
   βif-false : ∀ {M N} ∀ {M N} →
     if false then M else N ⟹ N
 
@@ -3568,9 +3565,9 @@ and indeed such rules are traditionally called beta rules.
 
 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)
+    ⟹  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
 
@@ -3628,189 +3625,189 @@ Here it is formalised in Agda.
 
 
 
-infix 10 _⟹*_ 
 infixr 2 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : : Term → → Term → → Set where
   _∎ : :∀ ∀M M→ →M M ⟹* M
   _⟹⟨_⟩_ : :∀ ∀L L {M N} → →L L⟹ ⟹M M→ →M M ⟹* N N→ →L L ⟹* N
 
@@ -3830,477 +3827,477 @@ out example reductions in an appealing way.
 
 
 
-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 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
   ∎
 
@@ -4347,683 +4344,683 @@ environment `Γ` by mapping variable `x` to type `A`.
 
 
 
-Context : : Set
 Context = = PartialMap Type
 
 infix 10 _⊢_∶_
 
 data _⊢_∶_ : : Context → → Term → → Type → → Set where
   Ax : :∀ ∀ {Γ x x A} →
     Γ x x≡ ≡ just A A →
     Γ ⊢ ⊢` `x x∶ ∶ A
   ⇒-I : :∀ ∀ {Γ x xN NA A B} →
     Γ , ,x x∶ ∶A A⊢ ⊢N N∶ ∶B B →
     Γ ⊢ ⊢ λ[ x x∶ ∶A A] ]N N∶ ∶A A⇒ ⇒ B
   ⇒-E : :∀ ∀ {Γ L LM MA A B} →
     Γ ⊢ ⊢L L∶ ∶A A⇒ ⇒B B →
     Γ ⊢ ⊢M M∶ ∶A A →
     Γ ⊢ ⊢L L· ·M M∶ ∶ B
   𝔹-I₁ : :∀ ∀ {Γ} →
     Γ ⊢ ⊢ true ∶ ∶ 𝔹
   𝔹-I₂ : :∀ ∀ {Γ} →
     Γ ⊢ ⊢ false ∶ ∶ 𝔹
   𝔹-E : :∀ ∀ {Γ L LM MN N A} →
     Γ ⊢ ⊢L L∶ ∶𝔹 𝔹 →
     Γ ⊢ ⊢M M∶ ∶A A →
     Γ ⊢ ⊢N N∶ ∶A A →
     Γ ⊢ ⊢ if L L then M M else N N∶ ∶ A
 
@@ -5033,205 +5030,205 @@ environment `Γ` by mapping variable `x` to type `A`.
 
 
 
-typing₁ : :∅ ∅⊢ ⊢ not ∶ ∶𝔹 𝔹⇒ ⇒ 𝔹
 typing₁ = = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : :∅ ∅⊢ ⊢ two ∶ ∶ (𝔹 ⇒ ⇒ 𝔹) ⇒ ⇒𝔹 𝔹⇒ ⇒ 𝔹
 typing₂ = = ⇒-I (⇒-I (⇒-E (Ax refl) ) (⇒-E (Ax refl) (Ax refl))))
 
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 71fe2d21..c3791aef 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -117,11 +117,11 @@ data Term : Set where
 
 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)
+    ⇒  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
@@ -237,18 +237,15 @@ currying. This is made more convenient by declaring `_⇒_` to
 associate to the right and `_·_` to associate to the left.
 Thus,
 
-> `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` abbreviates `(𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)`,
-
-and similarly,
-
-> `two · not · true` abbreviates `(two · not) · true`.
+* `(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` 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) ``.
+* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` abbreviates
+  `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` and not
+  `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``.
 
 \begin{code}
 ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
@@ -530,9 +527,9 @@ data _⟹_ : Term → Term → Set where
 
 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)
+    ⟹  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