diff --git a/out/Stlc.md b/out/Stlc.md index cd9f6b14..9e603fc5 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -919,7 +919,7 @@ irrelevant. Thus the five terms * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` * `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) `` * `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) `` -* `` λ[ 👿 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 👿 · (` 👿 · ` 😄) `` +* `` λ[ 😈 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 😈 · (` 😈 · ` 😄) `` * `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) `` are all considered equivalent. This equivalence relation @@ -958,6 +958,10 @@ variables in a term are distinct from the free variables, which can avoid confusions that may arise if bound and free variables have the same names. +#### Special characters + + 😈 U+1F608: SMILING FACE WITH HORNS + 😄 U+1F604: SMILING FACE WITH OPEN MOUTH AND SMILING EYES #### Precedence @@ -977,369 +981,369 @@ to be weaker than application. For instance, - and not `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``. 
{% raw %}
-ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)
-ex₁ = refl
-
-ex₂ : two · not · true ≡ (two · not) · true
-ex₂ = refl
-
-ex₃ : λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[: x(𝔹 ∶⇒ 𝔹) ]⇒ `𝔹 f⇒ ·𝔹 (`≡ f · ` x)
-      ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹) ]⇒ (λ[ x ∶ 𝔹 ]⇒ (` f · (` f · ` x))))𝔹)
 ex₃ex₁ = refl
+
+ex₂ : two · not · true ≡ (two · not) · true
+ex₂ = refl
+
+ex₃ : λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
+      ≡ (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x))))
+ex₃ = refl
 {% endraw %}
@@ -1389,130 +1393,130 @@ as values. The predicate `Value M` holds if term `M` is a value. 
{% raw %}
-data Value : Term → Set where
   value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
   value-true  : Value true
   value-false : Value false
 {% endraw %}
@@ -1583,646 +1587,646 @@ name. Here is the formal definition in Agda. 
{% raw %}
-_[_:=_] : Term → Id → Term → Term
-(` x′) [ x := V ] with x ≟ x′
-... | yes _ = V
-... | no  _ = ` x′
-(λ[ x′ ∶ A′ ] N′) [ x := V ] with x ≟: x′
-...Term → |Id yes→ _ =Term λ[→ x′ ∶ A′ ] N′Term
 ...(` |x′) no[ x := V ]  _ =with λ[ x′ ∶ A′ ] (N′ [ x :=≟ V ])x′
 (L′... ·| yes _ = V
+... | no  _ M′)= ` [ x :=x′
+(λ[ Vx′ ∶ A′ ] =  (L′N′) [ x := V:= ])V ·] (M′with [ x :=≟ V ])x′
 ... (true)| [yes x_ :== Vλ[ x′ ]∶ =A′ true] N′
 (false)... [| no  _ x :== Vλ[ ] =x′ false
-(if∶ L′A′ ] (N′ [ thenx := M′V else N′])
+(L′ · M′) [ x := V ] =
-  if (L′ [ x := V ]) then=  (L′ [ x := V ]) · (M′ (M′[ x [ x := V ])
+(true) else[ (N′ [ x := V ] = Vtrue
+(false) [ x := V ] = false
+(if L′ then M′ else N′) [ x := V ] =
+  if (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
 {% endraw %}
@@ -2252,527 +2256,320 @@ Note that ′ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE). Here is confirmation that the examples above are correct. 
{% raw %}
-ex₁₁ : ` f [ f := not ] ≡  not
-ex₁₁ = refl
-
-ex₁₂ : true [ f := not ] ≡ true
-ex₁₂ = refl
-
-ex₁₃ : (` f · true) [ f := not ] ≡ not · true
-ex₁₃ =f refl
-
-ex₁₄:= not ] ≡ : (`  not
+ex₁₁ f · (`= f · true))refl
+
+ex₁₂ [: f :=true not[ f := not ] ≡ not · (not · true)
 ex₁₄ex₁₂ = refl
 
 ex₁₅ex₁₃ : (` f :· (λ[ xtrue) ∶[ 𝔹f := not ] ` f · (`≡ f ·not `· x)) [ f := not ] ≡ λ[ x ∶ 𝔹 ] not · (not · ` x)true
 ex₁₅ex₁₃ = refl
 
 ex₁₆ex₁₄ : (λ[` f · (` f · true)) [ f := not ] ≡ not · (not y· ∶ 𝔹 ] ` ytrue)
+ex₁₄ [= x :=refl
+
+ex₁₅ true ] ≡: (λ[ yx ` yf
-ex₁₆ · (` =f refl
-
-ex₁₇· :` (λ[ x)) [ f := not ∶] 𝔹≡ ]λ[ ` x) ∶ [𝔹 x] :=not true· ](not ≡· λ[` x ∶ 𝔹 ] ` x)
 ex₁₇ex₁₅ = refl
+
+ex₁₆ : (λ[ y ∶ 𝔹 ] ` y) [ x := true ] ≡ λ[ y ∶ 𝔹 ] ` y
+ex₁₆ = refl
+
+ex₁₇ : (λ[ x ∶ 𝔹 ] ` x) [ x := true ] ≡ λ[ x ∶ 𝔹 ] ` x
+ex₁₇ = refl
 {% endraw %}
@@ -2983,569 +2987,569 @@ and indeed such rules are traditionally called beta rules. Here are the above rules formalised in Agda. 
{% raw %}
-infix 10 _⟹_ 
 
 data _⟹_ : Term → Term → Set where
-  ξ·₁ : ∀ {L L′ M} →
-    L ⟹ L′ →
-    L · M ⟹ L′ · M
-  ξ·₂ : ∀ {V M M′} →
-    Value V →
-    M ⟹ M′ →
-    V ·: MTerm ⟹→ VTerm ·→ M′Set where
   βλ· : ∀ {xξ·₁ A: N∀ V}{L →L′ ValueM} → V →
     (λ[L x⟹ ∶L′ A→
+    L ]· N)M ·⟹ VL′ ⟹· N [ x :=M
+  ξ·₂ V: ]
-  ξif : ∀ {LV L′ M NM′} →
+    Value →V →
     L ⟹M L′⟹ →M′    
+      > →
     ifV L· thenM ⟹ V · M else NM′
+  βλ· ⟹: if L′ then M else N
-  βif-true : ∀ {Mx A N V} → Value V →
+    (λ[ x ∶ A ] N} →)
-    if true· V ⟹ N [ x then:= V M] else N ⟹ M
   βif-falseξif : ∀ {L L′ M N} →
     ifL false then M else N ⟹ L′ →    
+    if L then M else N ⟹ if L′ then M else N
+  βif-true : ∀ {M N} →
+    if true then M else N ⟹ M
+  βif-false : ∀ {M N} →
+    if false then M else N ⟹ N
 {% endraw %}
@@ -3613,189 +3617,189 @@ are written as follows. Here it is formalised in Agda. 
{% raw %}
-infix 10 _⟹*_ 
 infixr 2 _⟹⟨_⟩_
 infix  3 _∎
 
 data _⟹*_ : Term → Term → Set where
   _∎ : ∀ M → M ⟹* M
   _⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N
 {% endraw %}
@@ -3813,477 +3817,477 @@ and transitive closure have been chosen to allow us to lay out example reductions in an appealing way. 
{% raw %}
-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 · true ⟹* true
+reduction₂ ·= true)
-  ⟹⟨ ξ·₂ value-λ (βλ· value-true) ⟩
     nottwo · not · true
+  ⟹⟨ ξ·₁ (ifβλ· value-λ) ⟩
+    (λ[ x true∶ then𝔹 ] not false· else(not · ` true)x)) · true
   ⟹⟨ ξ·₂βλ· value-λvalue-true βif-true  ⟩
     not · (not · false
-  ⟹⟨true) βλ· value-false ⟩
-    if false then false else true
   ⟹⟨ βif-falseξ·₂ 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
+  ∎
 {% endraw %}
@@ -4370,564 +4374,377 @@ functions, conditionals use booleans). Here are the above rules formalised in Agda. 
{% raw %}
-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} →_⊢_∶_
-    Γdata ,_⊢_∶_ x: ∶Context A ⊢ N ∶ B →
-    Γ Term ⊢→ λ[ xType ∶→ A ]Set N ∶ Awhere ⇒ B
   ⇒-EAx : ∀ {Γ ∀x {ΓA} L M A B} →
     Γ x ≡ just ⊢A L ∶ A ⇒ B →
     Γ ⊢ M` x ∶ A
+  ⇒-I A: →∀
-     {Γ ⊢x LN ·A B} M ∶ B
-  𝔹-I₁ : ∀ {Γ} →
     Γ ⊢, truex ∶ 𝔹A ⊢ N ∶ B →
-  𝔹-I₂Γ ⊢ λ[ x ∶ A ] N :∶ ∀A {Γ}⇒ B →
-    Γ ⊢ false ∶ 𝔹
   𝔹-E⇒-E : ∀ {Γ L M A B} →
+    Γ {Γ⊢ L M∶ N A} ⇒ B 
     Γ ⊢ LM ∶ 𝔹A 
     Γ ⊢ ML ∶· AM →
-    Γ ⊢ N ∶ AB
+  𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ if Ltrue then∶ M𝔹 else N
+  𝔹-I₂ ∶: ∀ {Γ} →
+    Γ ⊢ false ∶ 𝔹
+  𝔹-E : ∀ {Γ L M N A} →
+    Γ ⊢ L ∶ 𝔹 →
+    Γ ⊢ M ∶ A →
+    Γ ⊢ N ∶ A →
+    Γ ⊢ if L then M else N ∶ A
 {% endraw %}
@@ -5086,205 +5090,205 @@ where `Γ₁ = ∅ , f ∶ 𝔹 ⇒ 𝔹` and `Γ₂ = ∅ , f ∶ 𝔹 ⇒ 𝔹 Here are the above derivations formalised in Agda. 
{% raw %}
-typing₁ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
 typing₁ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₂ 𝔹-I₁)
 
 typing₂ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
 typing₂ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
 {% endraw %}
@@ -5335,82 +5339,82 @@ cannot be typed, because doing so requires that the first term in the application is both a boolean and a function. 
{% raw %}
-notyping₂ : ∀ {A} → ¬ (∅ ⊢ true · false ∶ A)
 notyping₂ (⇒-E () _)
 {% endraw %}
@@ -5420,237 +5424,237 @@ type `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y `` It cannot be typed, beca doing so requires `x` to be both boolean and a function. 
{% raw %}
-contradiction : ∀ {A B} → ¬ (𝔹 ≡ A ⇒ B)
-contradiction ()
-
-notyping₁ : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
-notyping₁ (⇒-I (⇒-I (⇒-E (Ax Γx)→ ¬ _)))(𝔹 ≡ =A   ⇒ B)
+contradiction (just-injective()
+
+notyping₁ Γx: ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
+notyping₁ (⇒-I (⇒-I (⇒-E (Ax Γx) _))) =  contradiction (just-injective Γx)
 {% endraw %}
diff --git a/src/Stlc.lagda b/src/Stlc.lagda index 38fff2ba..fae038d7 100644 --- a/src/Stlc.lagda +++ b/src/Stlc.lagda @@ -183,7 +183,7 @@ irrelevant. Thus the five terms * `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` * `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) `` * `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) `` -* `` λ[ 👿 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 👿 · (` 👿 · ` 😄) `` +* `` λ[ 😈 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 😈 · (` 😈 · ` 😄) `` * `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) `` are all considered equivalent. This equivalence relation @@ -222,6 +222,10 @@ variables in a term are distinct from the free variables, which can avoid confusions that may arise if bound and free variables have the same names. +#### Special characters + + 😈 U+1F608: SMILING FACE WITH HORNS + 😄 U+1F604: SMILING FACE WITH OPEN MOUTH AND SMILING EYES #### Precedence