diff --git a/out/Stlc.md b/out/Stlc.md index ecc03cca..5d615dea 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -4,762 +4,834 @@ layout : page permalink : /Stlc --- -This chapter defines the simply-typed lambda calculus. +The _lambda-calculus_, first published by the logician Alonzo Church in +1932, is a core calculus with only three syntactic constructs: +variables, abstraction, and application. It embodies the concept of +_functional abstraction_, which shows up in almsot every programming +language in some form (as functions, procedures, or methods). +The _simply-typed lambda calculus_ (or STLC) is a variant of the +lambda calculus published by Church in 1940. It has just the three +constructs above for function types, plus whatever else is required +for base types. Church had a minimal base type with no operations; +we will be slightly more pragmatic and choose booleans as our base type. + +This chapter formalises the STLC (syntax, small-step semantics, and typing rules), +and the next chapter reviews its main properties (progress and preservation). +The new technical challenges arise from the mechanisms of +_variable binding_ and _substitution_. + +We've already seen how to formalize a language with +variables ([Imp]({{ "Imp" | relative_url }})). +There, however, the variables were all global. +In the STLC, we need to handle the variables that name the +parameters to functions, and these are _bound_ variables. +Moreover, instead of just looking up variables in a global store, +we'll need to reduce function applications by _substituting_ +arguments for parameters in function bodies. + +We choose booleans as our base type for simplicity. At the end of the +chapter we'll see how to add numbers as a base type, and in later +chapters we'll enrich STLC with useful constructs like pairs, sums, +lists, records, subtyping, and mutable state. ## Imports 
 
-open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
 open PartialMap using (∅) renaming (_,_↦_ to _,_∶_)
 open import Data.Nat using (ℕ)
 open import Data.Maybe using (Maybe; just; nothing)
 open import Relation.Nullary using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
- ## Syntax -Syntax of types and terms. +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 +numbers as a base type. + +Here is the syntax of types in BNF. + + 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. 
+
+With the exception of variables, each construct either constructs
+a value of a given type (abstractions yield functions, true and
+false yield booleans) or deconstructs it (applications use functions,
+conditionals use booleans). We will see this again when we come
+to the rules for assigning types to terms, where constructors
+correspond to introduction rules and deconstructors to eliminators.
+
+Here is the syntax of terms in BNF.
+
+
+
+
+
+
+infixl 20 _·_
 infix  15 λ[_∶_]_
 infix  15 if_then_else_
 
 data Term : Set where
   ` : Id → Term
   λ[_∶_]_ : Id → Type → Term → Term
   _·_ : Term → Term → Term
   true : Term
   false : 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
+
+
+
 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)
 
@@ -769,130 +841,130 @@ Example terms.
 
 
 
-data Value : Term → Set where
   value-λ     : ∀ {x A N} → Value (λ[ x ∶ A ] N)
   value-true  : Value true
   value-false : Value false
 
@@ -902,645 +974,645 @@ Example terms.
 
 
 
-_[_:=_] : Term → Id → Term → Term
 (` x′) [ x := V ] with x ≟ x′
 ... | yes _ = V
 ... | no  _ = ` x′
 (λ[ x′ ∶ A′ ] N′) [ x := V ] with x ≟ x′
 ... | yes _ = λ[ x′ ∶ A′ ] N′
 ... | no  _ = λ[ x′ ∶ A′ ] (N′ [ x := V ])
 (L′ · M′) [ x := V ] =  (L′ [ x := V ]) · (M′ [ x := V ])
 (true) [ x := V ] = true
 (false) [ x := V ] = false
 (if L′ then M′ else N′) [ x := V ] = if (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
 
@@ -1550,569 +1622,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 : ∀ {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
 
@@ -2123,665 +2195,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 · 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
   ∎
 
@@ -2795,683 +2867,683 @@ 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 M A B} →
     Γ ⊢ L ∶ A ⇒ B →
     Γ ⊢ M ∶ A →
     Γ ⊢ L · M ∶ B
   𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ true ∶ 𝔹
   𝔹-I₂ : ∀ {Γ} →
     Γ ⊢ false ∶ 𝔹
   𝔹-E : ∀ {Γ L M N A} →
     Γ ⊢ L ∶ 𝔹 →
     Γ ⊢ M ∶ A →
     Γ ⊢ N ∶ A →
     Γ ⊢ if L then M else N ∶ A
 
@@ -3481,205 +3553,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 10ea0dcf..9abc392d 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -30,7 +30,7 @@ we'll need to reduce function applications by _substituting_
 arguments for parameters in function bodies.
 
 We choose booleans as our base type for simplicity.  At the end of the
-chapter we'll see how to add naturals as a base type, and in later
+chapter we'll see how to add numbers as a base type, and in later
 chapters we'll enrich STLC with useful constructs like pairs, sums,
 lists, records, subtyping, and mutable state.
 
@@ -47,7 +47,19 @@ open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 
 ## Syntax
 
-We have just two types, function types and booleans.
+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
+numbers as a base type.
+
+Here is the syntax of types in BNF.
+
+    A, B, C ::= A ⇒ B | 𝔹
+
+And here it is formalised in Agda.
 
 \begin{code}
 infixr 20 _⇒_
@@ -57,11 +69,28 @@ data Type : Set where
   𝔹 : Type
 \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.
+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. 
+
+With the exception of variables, each construct either constructs
+a value of a given type (abstractions yield functions, true and
+false yield booleans) or deconstructs it (applications use functions,
+conditionals use booleans). We will see this again when we come
+to the rules for assigning types to terms, where constructors
+correspond to introduction rules and deconstructors to eliminators.
+
+Here is the syntax of terms in BNF.
+
+
 
-CONTINUE FROM HERE
 
 \begin{code}
 infixl 20 _·_
@@ -77,6 +106,14 @@ 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
+
+
+
 Example terms.
 \begin{code}
 f x : Id