updated fonts

src/plta/Fonts.lagda

@@ -10,33 +10,42 @@ module plta.Fonts where
 
 Test page for fonts. All vertical bars should line up.
 
-Agda:
-
 \begin{code}
 {-
+--------------------------|
 abcdefghijklmnopqrstuvwxyz|
 ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
 ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
 ₐ   ₑ   ᵢⱼ    ₒ  ᵣ  ᵤ  ₓ  |
-αβγδεφικλμνωπψρστυχξζ|
+--------------------------|
-ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ|
+------------------------|
+αβγδεζηθικλμνξοπρστυφχψω|
+ΑΒΓΔΕΖΗΘΙΚΛΜΝΞΟΠΡΣΤΥΦΧΨΩ|
+------------------------|
+----------|
 0123456789|
 ⁰¹²³⁴⁵⁶⁷⁸⁹|
 ₀₁₂₃₄₅₆₇₈₉|
-⟨⟨⟨⟩⟩⟩|
+----------|
-→→→⇒⇒⇒|
-←←←⇐⇐⇐|
-------|
-⌊⌋⌈⌉|
-→→→→|
-↦↦↦↦|
-↠↠↠↠|
-⊢⊢⊢⊢|
-⊣⊣⊣⊣|
-∈∈∈∈|
-∋∋∋∋|
 ----|
+⟨⟨⟩⟩|
+⌊⌊⌋⌋|
+⌈⌈⌉⌉|
+→→⇒⇒|
+←←⇐⇐|
+↦↦↠↠|
+∈∈∋∋|
+⊢⊢⊣⊣|
+ͰͰͰͰ|
+----|
+-}
+\end{code}
+
+Here are some characters that are not required to be monospaced.
+
+\begin{code}
+{-
 ------------
 ⟶⟶⟶⟶
 ⟹⟹⟹⟹
@@ -45,36 +54,3 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ|
 𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
 -}
 \end{code}
-
-Indented code:
-
-    abcdefghijklmnopqrstuvwxyz|
-    ABCDEFGHIJKLMNOPQRSTUVWXYZ|
-    ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ ʳˢᵗᵘᵛʷˣʸᶻ|
-    ᴬᴮ ᴰᴱ ᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾ ᴿ ᵀᵁⱽᵂ   |
-    ₐ   ₑ   ᵢⱼ    ₒ  ᵣ  ᵤ  ₓ  |
-    αβγδεφικλμνωπψρστυχξζ|
-    ΑΒΓΔΕΦΙΚΛΜΝΩΠΨΡΣΤΥΧΞΖ|
-    0123456789|
-    ⁰¹²³⁴⁵⁶⁷⁸⁹|
-    ₀₁₂₃₄₅₆₇₈₉|
-    ⟨⟨⟨⟩⟩⟩|
-    →→→⇒⇒⇒|
-    ←←←⇐⇐⇐|
-    ------|
-    ⌊⌋⌈⌉|
-    →→→→|
-    ↦↦↦↦|
-    ↠↠↠↠|
-    ⊢⊢⊢⊢|
-    ⊣⊣⊣⊣|
-    ∈∈∈∈|
-    ∋∋∋∋|
-    ----|
-    ------------
-    ⟶⟶⟶⟶
-    ⟹⟹⟹⟹
-    ------------
-    𝕒𝕓𝕔𝕕𝕖𝕗𝕘𝕙𝕚𝕛
-    𝑎𝑏𝑐𝑑𝑒𝑓𝑔𝑖𝑗𝑘
-

src/plta/Lambda.lagda

@@ -189,6 +189,12 @@ in other words that the term
 reduces to `` `suc `suc `suc `suc `zero ``.
 
 
+#### Exercise (`mul`)
+
+Write out the defintion of a lambda term that multiplies
+two natural numbers.
+
+
 ### Formal vs informal
 
 In informal presentation of formal semantics, one uses choice of
@@ -414,7 +420,7 @@ In all other cases, we push substitution recursively into
 the subterms.
 
 
-#### Examples
+### Examples
 
 Here is confirmation that the examples above are correct.
 
@@ -657,7 +663,7 @@ open Chain (Term) (_⟶_)
 \end{code}
 
 
-### Exercise
+#### Exercise (`closure-equivalent`)
 
 Show that the two notions of reflexive and transitive closure
 above are equivalent.
@@ -748,6 +754,12 @@ _ =
 In the next chapter, we will see how to compute such reduction sequences.
 
 
+#### Exercise (`mul-ex`)
+
+Using the term `mul` you defined earlier, write out the reduction
+sequence demonstrating that two times two is four.
+
+
 ## Syntax of types
 
 We have just two types.
@@ -1077,7 +1089,7 @@ Here are typings for the remainder of the Church example.
 \end{code}
 
 
-#### Interaction with Agda
+### Interaction with Agda
 
 Construction of a type derivation may be done interactively.
 Start with the declaration:
@@ -1178,6 +1190,12 @@ or explain why there are no such types.
 2. `` ∅ , "x" ⦂ A , "y" ⦂ B ⊢ ƛ "z" ⇒ ⌊ "x" ⌋ · (⌊ "y" ⌋ · ⌊ "z" ⌋) ⦂ C ``
 
 
+#### Exercise (`mul-type`)
+
+Using the term `mul` you defined earlier, write out the derivation
+showing that it is well-typed.
+
+
 ## Unicode
 
 This chapter uses the following unicode

src/plta/PandP.lagda

@@ -36,21 +36,8 @@ both reduce to `` `suc `suc `suc `suc `zero ``,
 which represents the natural number four.
 
 What we might expect is that every term is either a value or can take
-a reduction step.  However, this is not true in general.  The term
+a reduction step.  As we will see, this property does _not_ hold for
-
+every term, but it does hold for every closed, well-typed term.
-    `zero · `suc `zero
-
-is neither a value nor can take a reduction step. And if `` s ⦂ `ℕ ⇒ `ℕ ``
-then the term
-
-     s · `zero
-
-cannot reduce because we do not know which function is bound to the
-free variable `s`.
-
-However, the first of those terms is ill-typed, and the second has a free
-variable.  It turns out that the property we want does hold for every
-closed, well-typed term.
 
 _Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
 that `M ⟶ N`.
@@ -68,16 +55,16 @@ By progress, it is either a value, in which case we are done, or it reduces
 to some other term.  By preservation, that other term will itself be closed
 and well-typed.  Repeat.  We will either loop forever, in which case evaluation
 does not terminate, or we will eventually reach a value, which is guaranteed
-to be closed and of the same type as the original term.
+to be closed and of the same type as the original term.  We will turn this
+recipe into Agda code that can compute for us the reduction sequence of
+`plus · two · two`, and its Church numeral variant.
 
 In this chapter we will prove _Preservation_ and _Progress_, and show
-how to apply them to get Agda to evaluate a term for us, that is, to reduce
+how to apply them to get Agda to evaluate terms.
-that term until it reaches a value (or to loop forever).
 
 The development in this chapter was inspired by the corresponding
-development in Chapter _StlcProp_ of _Software Foundations_
+development in in _Software Foundations, volume _Programming Language
-(_Programming Language Foundations_).  It will turn
+Foundations_, chapter _StlcProp_.  It will turn out that one of our technical choices
-out that one of our technical choices in the previous chapter
 (to introduce an explicit judgment `Γ ∋ x ⦂ A` in place of
 treating a context as a function from identifiers to types)
 permits a simpler development. In particular, we can prove substitution preserves
@@ -98,6 +85,7 @@ open import Data.Product
 open import Data.Sum using (_⊎_; inj₁; inj₂)
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Function using (_∘_)
+open import plta.Isomorphism
 open import plta.Lambda
 open Chain (Term) (_⟶_)
 \end{code}
@@ -183,11 +171,26 @@ case of successor.
 
 ## Progress
 
-We now show that every closed, well-typed term is either a value
+We would like to show that every term is either a value or takes a
-or can take a reduction step.  First, we define a relation
+reduction step.  However, this is not true in general.  The term
-`Progress M` which holds of a term `M` if it is a value or
-if it can take a reduction step.
 
+    `zero · `suc `zero
+
+is neither a value nor can take a reduction step. And if `` s ⦂ `ℕ ⇒ `ℕ ``
+then the term
+
+     s · `zero
+
+cannot reduce because we do not know which function is bound to the
+free variable `s`.  The first of those terms is ill-typed, and the
+second has a free variable.  Every term that is well-typed and closed
+has the desired property.
+
+_Progress_: If `∅ ⊢ M ⦂ A` then either `M` is a value or there is an `N` such
+that `M ⟶ N`.
+
+To formulate this property, we first introduce a relation that
+captures what it means for a term `M` to make progess.
 \begin{code}
 data Progress (M : Term) : Set where
 
@@ -200,8 +203,12 @@ data Progress (M : Term) : Set where
       Value M
       ----------
     → Progress M
-\end{code}    
+\end{code}
+A term `M` makes progress if either it can take a step, meaning there
+exists a term `N` such that `M ⟶ N`, or if it is done, meaning that
+`M` is a value.
 
+If a term is well-typed in the empty context then it is a value.
 \begin{code}
 progress : ∀ {M A}
   → ∅ ⊢ M ⦂ A
@@ -226,8 +233,43 @@ progress (⊢case ⊢L ⊢M ⊢N) with progress ⊢L
 ...   | C-suc CL                             =  step (β-case-suc (value CL))
 progress (⊢μ ⊢M)                             =  step β-μ
 \end{code}
+Let's unpack the first three cases.  We induct on the evidence that
+`M` is well-typed.
 
-This code reads neatly in part because we consider the
+* The term cannot be a variable, since no variable is well typed
+  in the empty context.
+
+* If the term is a lambda abstraction then it is a value.
+
+* If the term is an application `L · M`, recursively apply
+  progress to the derivation that `L` is well-typed.
+
+  + If the term steps, we have evidence that `L ⟶ L′`,
+    which by `ξ-·₁` means that our original term steps
+    to `L′ · M`
+
+  + If the term is done, we have evidence that `L` is
+    a value. Recursively apply progress to the derivation
+    that `M` is well-typed.
+
+    - If the term steps, we have evidence that `M ⟶ M′`,
+      which by `ξ-·₂` means that our original term steps
+      to `L · M′`.  Step `ξ-·₂` applies only if we have
+      evidence that `L` is a value, but progress on that
+      subterm has already supplied the required evidence.
+
+    - If the term is done, we have evidence that `M` is
+      a value.  We apply the canonical forms lemma to the
+      evidence that `L` is well typed and a value, which
+      since we are in an application leads to the
+      conclusion that `L` must be a lambda
+      abstraction.  We also have evidence that `M` is
+      a value, so our original term steps by `β-ƛ·`.
+
+The remaining cases, for zero, successor, case, and fixpoint,
+are similar.
+
+Our code reads neatly in part because we consider the
 `step` option before the `done` option. We could, of course,
 do it the other way around, but then the `...` abbreviation
 no longer works, and we will need to write out all the arguments
@@ -236,10 +278,28 @@ in full. In general, the rule of thumb is to consider the easy case
 If you have two hard cases, you will have to expand out `...`
 or introduce subsidiary functions.
 
+Instead of defining a data type for `Progress M`, we could
+have formulated progress using disjunction and existentials:
 \begin{code}
 postulate
-  progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Progress M
+  progress′ : ∀ M {A} → ∅ ⊢ M ⦂ A → Value M ⊎ ∃[ N ](M ⟶ N)
 \end{code}
+This leads to a less perspicous proof.  Instead of the mnemonic `done`
+and `step` we use `inj₁` and `inj₂`, and the term `N` is no longer
+implicit and so must be written out in full.  In the case for `β-ƛ·`
+this requires that we match against the lambda expression `L` to
+determine its bound variable and body, `ƛ x ⇒ N`, so we can show that
+`L · M` reduces to `N [ x := M ]`.
+
+#### Exercise (`progress′`)
+
+Write out the proof of `progress′` in full, and compare it to the
+proof of `progress`.
+
+#### Exercise (`Progress-iso`)
+
+Show that `Progress M` is isomorphic to `Value M ⊎ ∃[ N ](M ⟶ N)`.
+
 
 ## Prelude to preservation