diff --git a/out/Stlc.md b/out/Stlc.md index 677d57e9..209fa194 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -272,8 +272,10 @@ lists, records, subtyping, and mutable state. ## Syntax We have just two types. + * Functions, `A ⇒ B` * Booleans, `𝔹` + We require some form of base type, because otherwise the set of types would be empty. Church used a trivial base type `o` with no operations. For us, it is more convenient to use booleans. Later we will consider @@ -281,100 +283,102 @@ numbers as a base type. Here is the syntax of types in BNF. - A, B, C ::= - A ⇒ B -- functions - 𝔹 -- booleans + A, B, C ::= A ⇒ B | 𝔹 And here it is formalised in Agda. 
 
-infixr 20 _⇒_
 
 data Type : Set where
   _⇒_ : Type → Type → Type
   𝔹 : Type
Terms have six constructs. Three are for the core lambda calculus: + * Variables, `` ` x `` * Abstractions, `λ[ x ∶ A ] N` * Applications, `L · M` + and three are for the base type, booleans: + * True, `true` * False, `false` * Conditions, `if L then M else N` + Abstraction is also called lambda abstraction, and is the construct from which the calculus takes its name. @@ -387,229 +391,224 @@ correspond to introduction rules and deconstructors to eliminators. Here is the syntax of terms in BNF. - L, M, N ::= ` x | λ[ x ∶ A ] N - - + L, M, N ::= ` x | λ[ x ∶ A ] N | L · M | true | false | if L then M else N +And here it is formalised in Agda. 
 
-infixl 20 _·_
-infix  15 λ[_∶_]_
-infix  15 if_then_else_
+infix  15 λ[_∶_]_
+infix  15 if_then_else_
 
 data Term : Set where
   ` : Id → Term
-  λ[_∶_]_ : Id → Type → Term → Term
-  _·_ : Term → Term → Term
   λ[_∶_]_ : Id → Type → Term → Term
+  _·_ : Term → Term → Term
+  true : Term
   false : Term
-  if_then_else_ : Term → Term → Term →Term
+  if_then_else_ : Term → Term → Term → Term
-Each type introduces its own constructs, which come in pairs, -one to introduce (or construct) values of the type, and one to eliminate -(or deconstruct) them. - CONTINUE FROM HERE @@ -617,225 +616,225 @@ CONTINUE FROM HERE Example terms. 
 
-f x : Id
 f  =  id 0
 x  =  id 1
 
 not two : Term 
 not =  λ[ x ∶ 𝔹 ] (if ` x then false else true)
 two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
 
@@ -845,130 +844,130 @@ Example terms.
 
 
 
-data Value : Term → Set where
+  value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
+  value-true  : Value true
+  value-false : Value : Term → Set where
-  value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
-  value-true  : Value true
-  value-false : Value false
 
@@ -978,646 +977,646 @@ Example terms.
 
 
 
-_[_:=_] : Term → Id → Term → Term
+(` x′) [ x := V ] with x ≟ x′
+... | yes _ = V
+... | no  _ = ` x′
+(λ[ x′ ∶ A′ ] N′) [ x := V ] with x ≟ → Termx′
+... →| Term
-(`yes _ = x′)λ[ [x′ x∶ :=A′ V] ] withN′
+... x| ≟no  _ x′
-...= |λ[ yesx′ _∶ =A′ V]
- ...(N′ |[ no  _x =:= `V ]) x′
 (λ[L′ x′· M′) ∶[ A′x ]:= N′)V ] [= x :=  (L′ V[ ]x with:= V x]) ≟· x′
-...(M′ [ |x yes:= _V ]=)
+(true) λ[[ x′ ∶ A′x ]:= N′V
-... ] = | notrue  _ = λ[
+(false) x′ ∶ A′ ] (N′ [ x := V ] = false
+(if ])
-(L′ ·then M′ else N′) [ x := V[ ]x =  (L′:= V ] [= xif := V(L′ ])[ ·x (M′:= V [ x := V ])
- then (true)M′ [ x := [V x := V ]) =else true(N′ [ x
-(false := V ]) [ x := V ] = false
-(if L′ then M′ else N′) [ x := V ] = if (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
 
 

@@ -1626,569 +1625,569 @@ Example terms.
 
 
 
-infix 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
   βλ· : ∀ {x A N V} → Value V →
     (λ[ x ∶ A ] N) · V ⟹ N [ x := V ]
+  ξ·₁ : ∀ {L L′ M} →
+    L ⟹ L′ →
+    L · M ⟹ L′ · M
+  ξ·₂ : ∀ {V M M′} →
+    Value V →
+    M ⟹ M′ →
+    V · M ⟹ V ]· M′
   ξ·₁βif-true : ∀ {L L′ M}∀ →{M
-    L ⟹N} L′ →
     Lif ·true then M else N ⟹ L′ · M
   ξ·₂ : ∀ {V Mβif-false M′: }∀ →
-    Value V →
-    {M ⟹N} M′ →
     Vif false then M else N ·⟹ MN ⟹ V ·
+  ξif M′
-  βif-true : ∀ {M N} →
-    if true then M else N ⟹ M
-  βif-false : ∀ {M N} →
-    if false then M else N ⟹ N
-  ξif : ∀ {L L′ M N} →
     L ⟹ L′ →    
     if L then M else N ⟹ if L′ then M else N
 
@@ -2199,665 +2198,665 @@ Example terms.
 
 
 
-infix 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : Term → Term → Set where
   _∎ : ∀ M → M ⟹* M
   _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N  
 
 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 ∶ 𝔹 ] not · (not · ` x)) · true
+  ⟹⟨ βλ· value-true ⟩
+    not · (not · not · true)
   ⟹⟨ ξ·₁ξ·₂ (βλ· value-λ) (βλ· value-true) ⟩
     (λ[ x ∶ 𝔹not ]· not(if · (not · ` x)) · true
-  ⟹⟨ then false else true) βλ· value-true ⟩
-    not · (not · true)
   ⟹⟨ ξ·₂ value-λ (βλ· value-true) βif-true  ⟩
     not · false
+  ⟹⟨ βλ· value-false ⟩
+    if false then (if true then false else true)
   ⟹⟨ ξ·₂ value-λ βif-true  ⟩
-    not · false
-  ⟹⟨ βλ· value-false ⟩
-    if false then false else true
-  ⟹⟨ βif-false ⟩
     true
   ∎
 
@@ -2871,147 +2870,344 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
 
-Context : Set
 Context = PartialMap Type
 
 infix 10 _⊢_∶_
 
 data _⊢_∶_ : Context → Term → Type → Set where
   Ax : ∀ {Γ x A} →
     Γ x ≡ just A →
+    Γ ⊢ ` x ∶ A
+  ⇒-I : ∀ {Γ x N A B} →
+    Γ , x ∶ A ⊢ N ∶ B →
+    Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
+  ⇒-E : ∀ {Γ ≡L justM A B} 
     Γ ⊢ `L x∶ ∶A A⇒
-  ⇒-I : ∀ {Γ x N A B} →
     Γ ⊢ M ∶ A →
+    Γ ⊢ L ,· xM ∶ AB ⊢ N ∶ B →
-    Γ ⊢ λ[ x ∶ A ] N ∶ A ⇒ B
   ⇒-E𝔹-I₁ : ∀ {Γ} →
+    Γ ⊢ true ∶ 𝔹
+  𝔹-I₂ : ∀ : {Γ∀} {Γ L M A B} →
     Γ ⊢ Lfalse ∶ 𝔹
+  𝔹-E A: ⇒∀ B →
-    {Γ ⊢L M N A} M ∶ A →
     Γ ⊢ L ∶ ⊢𝔹 L→ · M ∶
+    Γ B⊢
-  𝔹-I₁ :M ∀∶ {Γ}A →
     Γ ⊢ trueN ∶ A →
+    Γ ∶⊢ 𝔹
-  𝔹-I₂if :L ∀then {Γ}M else →N
-    Γ ⊢ false ∶ 𝔹
-  𝔹-E : ∀ {Γ L M N A} →
-    Γ ⊢ L ∶ 𝔹 →
-    Γ ⊢ M ∶ A →
-    Γ ⊢ N ∶ A →
-    Γ ⊢ if L then M else N ∶ A
 
@@ -3557,205 +3556,205 @@ Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
 
 
 
-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 59a75943..05695f81 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -48,8 +48,10 @@ open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 ## Syntax
 
 We have just two types.
+
   * Functions, `A ⇒ B`
   * Booleans, `𝔹`
+
 We require some form of base type, because otherwise the set of types
 would be empty. Church used a trivial base type `o` with no operations.
 For us, it is more convenient to use booleans. Later we will consider
@@ -57,9 +59,7 @@ numbers as a base type.
 
 Here is the syntax of types in BNF.
 
-    A, B, C ::=
-      A ⇒ B   -- functions
-      𝔹        -- booleans
+    A, B, C  ::=  A ⇒ B | 𝔹
 
 And here it is formalised in Agda.
 
@@ -72,13 +72,17 @@ data Type : Set where
 \end{code}
 
 Terms have six constructs. Three are for the core lambda calculus:
+
   * Variables, `` ` x ``
   * Abstractions, `λ[ x ∶ A ] N`
   * Applications, `L · M`
+
 and three are for the base type, booleans:
+
   * True, `true`
   * False, `false`
   * Conditions, `if L then M else N`
+
 Abstraction is also called lambda abstraction, and is the construct
 from which the calculus takes its name. 
 
@@ -91,10 +95,9 @@ correspond to introduction rules and deconstructors to eliminators.
 
 Here is the syntax of terms in BNF.
 
-    L, M, N ::= ` x | λ[ x ∶ A ] N 
-
-
+    L, M, N  ::=  ` x | λ[ x ∶ A ] N | L · M | true | false | if L then M else N
 
+And here it is formalised in Agda.
 
 \begin{code}
 infixl 20 _·_
@@ -110,10 +113,6 @@ data Term : Set where
   if_then_else_ : Term → Term → Term → Term
 \end{code}
 
-Each type introduces its own constructs, which come in pairs,
-one to introduce (or construct) values of the type, and one to eliminate
-(or deconstruct) them.
-
 CONTINUE FROM HERE