From aef1fa75cabc1fd23dd387f59eb9855ca49e021f Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Fri, 14 Jul 2017 11:07:38 +0100 Subject: [PATCH] finished intro to syntax --- out/Stlc.md | 4673 ++++++++++++++++++++++++------------------------ src/Stlc.lagda | 19 +- 2 files changed, 2345 insertions(+), 2347 deletions(-) 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