last fixes to Stlc and StlcProp before sending out for comment

index.md

@@ -3,7 +3,11 @@ title  : Table of Contents
 layout : page
 ---
  
+<!--
   - [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }})
+-->
+
   - [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
   - [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
   - [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})
+

out/Basics.md

@@ -50,16 +50,16 @@ proofs and sound informal reasoning about program behavior.
 
 The other sense in which functional programming is "functional" is
 that it emphasizes the use of functions (or methods) as
-*first-class* values -- i.e., values that can be passed as
+_first-class_ values -- i.e., values that can be passed as
 arguments to other functions, returned as results, included in
 data structures, etc.  The recognition that functions can be
 treated as data in this way enables a host of useful and powerful
 idioms.
 
-Other common features of functional languages include *algebraic
+Other common features of functional languages include _algebraic
-data types* and *pattern matching*, which make it easy to
+data types_ and _pattern matching_, which make it easy to
 construct and manipulate rich data structures, and sophisticated
-*polymorphic type systems* supporting abstraction and code reuse.
+_polymorphic type systems_ supporting abstraction and code reuse.
 Agda shares all of these features.
 
 This chapter introduces the most essential elements of Agda.
@@ -67,7 +67,7 @@ This chapter introduces the most essential elements of Agda.
 ## Enumerated Types
 
 One unusual aspect of Agda is that its set of built-in
-features is *extremely* small. For example, instead of providing
+features is _extremely_ small. For example, instead of providing
 the usual palette of atomic data types (booleans, integers,
 strings, etc.), Agda offers a powerful mechanism for defining new
 data types from scratch, from which all these familiar types arise
@@ -87,7 +87,7 @@ very simple example.
 ### Days of the Week
 
 The following declaration tells Agda that we are defining
-a new set of data values -- a *type*.
+a new set of data values -- a _type_.
 
 <pre class="Agda">
 
@@ -358,7 +358,7 @@ One thing to note is that the argument and return types of
 this function are explicitly declared.  Like most functional
 programming languages, Agda can often figure out these types for
 itself when they are not given explicitly -- i.e., it performs
-*type inference* -- but we'll include them to make reading
+_type inference_ -- but we'll include them to make reading
 easier.
 
 Having defined a function, we should check that it works on
@@ -372,13 +372,13 @@ would be an excellent moment to fire up Agda and try this for yourself.
 Load this file, `Basics.lagda`, load it using `C-c C-l`, submit the
 above example to Agda, and observe the result.
 
-Second, we can record what we *expect* the result to be in the
+Second, we can record what we _expect_ the result to be in the
 form of an Agda type:
 
 <pre class="Agda">
 
-<a name="4097" href="Basics.html#4097" class="Function Operator"
+<a name="4097" href="Basics.html#4097" class="Function"
-      >test_nextWeekday</a
+      >test-nextWeekday</a
       ><a name="4113"
       > </a
       ><a name="4114" class="Symbol"
@@ -420,8 +420,8 @@ a term of the above type:
 
 <pre class="Agda">
 
-<a name="4472" href="Basics.html#4097" class="Function Operator"
+<a name="4472" href="Basics.html#4097" class="Function"
-      >test_nextWeekday</a
+      >test-nextWeekday</a
       ><a name="4488"
       > </a
       ><a name="4489" class="Symbol"
@@ -435,13 +435,13 @@ a term of the above type:
 </pre>
 
 There is no essential difference between the definition for
-`test_nextWeekday` here and the definition for `nextWeekday` above,
+`test-nextWeekday` here and the definition for `nextWeekday` above,
 except for the new symbol for equality `≡` and the constructor `refl`.
 The details of these are not important for now (we'll come back to them in
 a bit), but essentially `refl` can be read as "The assertion we've made
 can be proved by observing that both sides of the equality evaluate to the
 same thing, after some simplification."
 
-Third, we can ask Agda to *compile* some program involving our definition,
+Third, we can ask Agda to _compile_ some program involving our definition,
 This facility is very interesting, since it gives us a way to construct
-*fully certified* programs. We'll come back to this topic in later chapters.
+_fully certified_ programs. We'll come back to this topic in later chapters.

src/Basics.lagda

@@ -20,16 +20,16 @@ proofs and sound informal reasoning about program behavior.
 
 The other sense in which functional programming is "functional" is
 that it emphasizes the use of functions (or methods) as
-*first-class* values -- i.e., values that can be passed as
+_first-class_ values -- i.e., values that can be passed as
 arguments to other functions, returned as results, included in
 data structures, etc.  The recognition that functions can be
 treated as data in this way enables a host of useful and powerful
 idioms.
 
-Other common features of functional languages include *algebraic
+Other common features of functional languages include _algebraic
-data types* and *pattern matching*, which make it easy to
+data types_ and _pattern matching_, which make it easy to
 construct and manipulate rich data structures, and sophisticated
-*polymorphic type systems* supporting abstraction and code reuse.
+_polymorphic type systems_ supporting abstraction and code reuse.
 Agda shares all of these features.
 
 This chapter introduces the most essential elements of Agda.
@@ -37,7 +37,7 @@ This chapter introduces the most essential elements of Agda.
 ## Enumerated Types
 
 One unusual aspect of Agda is that its set of built-in
-features is *extremely* small. For example, instead of providing
+features is _extremely_ small. For example, instead of providing
 the usual palette of atomic data types (booleans, integers,
 strings, etc.), Agda offers a powerful mechanism for defining new
 data types from scratch, from which all these familiar types arise
@@ -57,7 +57,7 @@ very simple example.
 ### Days of the Week
 
 The following declaration tells Agda that we are defining
-a new set of data values -- a *type*.
+a new set of data values -- a _type_.
 
 \begin{code}
 data Day : Set where
@@ -92,7 +92,7 @@ One thing to note is that the argument and return types of
 this function are explicitly declared.  Like most functional
 programming languages, Agda can often figure out these types for
 itself when they are not given explicitly -- i.e., it performs
-*type inference* -- but we'll include them to make reading
+_type inference_ -- but we'll include them to make reading
 easier.
 
 Having defined a function, we should check that it works on
@@ -106,11 +106,11 @@ would be an excellent moment to fire up Agda and try this for yourself.
 Load this file, `Basics.lagda`, load it using `C-c C-l`, submit the
 above example to Agda, and observe the result.
 
-Second, we can record what we *expect* the result to be in the
+Second, we can record what we _expect_ the result to be in the
 form of an Agda type:
 
 \begin{code}
-test_nextWeekday : nextWeekday (nextWeekday saturday) ≡ tuesday
+test-nextWeekday : nextWeekday (nextWeekday saturday) ≡ tuesday
 \end{code}
 
 This declaration does two things: it makes an assertion (that the second
@@ -121,17 +121,17 @@ Having made the assertion, we must also verify it. We do this by giving
 a term of the above type:
 
 \begin{code}
-test_nextWeekday = refl
+test-nextWeekday = refl
 \end{code}
 
 There is no essential difference between the definition for
-`test_nextWeekday` here and the definition for `nextWeekday` above,
+`test-nextWeekday` here and the definition for `nextWeekday` above,
 except for the new symbol for equality `≡` and the constructor `refl`.
 The details of these are not important for now (we'll come back to them in
 a bit), but essentially `refl` can be read as "The assertion we've made
 can be proved by observing that both sides of the equality evaluate to the
 same thing, after some simplification."
 
-Third, we can ask Agda to *compile* some program involving our definition,
+Third, we can ask Agda to _compile_ some program involving our definition,
 This facility is very interesting, since it gives us a way to construct
-*fully certified* programs. We'll come back to this topic in later chapters.
+_fully certified_ programs. We'll come back to this topic in later chapters.

src/Stlc.lagda

@@ -20,6 +20,7 @@ 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.
@@ -28,6 +29,7 @@ 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
@@ -818,19 +820,30 @@ The entire process can be automated using Agsy, invoked with C-c C-a.
 
 #### Non-examples
 
-We can also show that terms are _not_ typeable.
+We can also show that terms are _not_ typeable.  For example, here is
-For example, here is a formal proof that it is not possible
+a formal proof that it is not possible to type the term `` true ·
-to type the term `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ``.
+false ``.  In other words, no type `A` is the type of this term.  It
-In other words, no type `A` is the type of this term.
+cannot be typed, because doing so requires that the first term in the
+application is both a boolean and a function.
+
+\begin{code}
+notyping₂ : ∀ {A} → ¬ (∅ ⊢ true · false ∶ A)
+notyping₂ (⇒-E () _)
+\end{code}
+
+As a second example, here is a formal proof that it is not possible to
+type `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y `` It cannot be typed, because
+doing so requires `x` to be both boolean and a function.
 
 \begin{code}
 contradiction : ∀ {A B} → ¬ (𝔹 ≡ A ⇒ B)
 contradiction ()
 
-notyping : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
+notyping₁ : ∀ {A} → ¬ (∅ ⊢ λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y ∶ A)
-notyping (⇒-I (⇒-I (⇒-E (Ax Γx) (Ax Γy)))) =  contradiction (just-injective Γx)
+notyping₁ (⇒-I (⇒-I (⇒-E (Ax Γx) _))) =  contradiction (just-injective Γx)
 \end{code}
 
+
 #### Quiz
 
 For each of the following, given a type `A` for which it is derivable,

src/StlcProp.lagda

@@ -28,8 +28,11 @@ import Data.Nat using (ℕ)
 
 ## Canonical Forms
 
+<!--
 As we saw for the simple calculus in Chapter [Types]({{ "Types" | relative_url }}),
-the first step in establishing basic properties of reduction and typing
+-->
+
+The first step in establishing basic properties of reduction and typing
 is to identify the possible _canonical forms_ (i.e., well-typed closed values)
 belonging to each type.  For function types the canonical forms are lambda-abstractions,
 while for boolean types they are values `true` and `false`.  
@@ -63,11 +66,12 @@ data Progress : Term → Set where
 progress : ∀ {M A} → ∅ ⊢ M ∶ A → Progress M
 \end{code}
 
-The proof is a relatively
+<!--
-straightforward extension of the progress proof we saw in
+The proof is a relatively straightforward extension of the progress proof we saw in
 [Types]({{ "Types" | relative_url }}).
-We give the proof in English
+-->
-first, then the formal version.
+
+We give the proof in English first, then the formal version.
 
 _Proof_: By induction on the derivation of `∅ ⊢ M ∶ A`.
 
@@ -157,9 +161,12 @@ substitution.  Working from top to bottom (from the high-level
 property we are actually interested in to the lowest-level
 technical lemmas), the story goes like this:
 
-  - The _preservation theorem_ is proved by induction on a typing
+  <!--
-    derivation, pretty much as we did in the [Types]({{ "Types" | relative_url }})
+  - The _preservation theorem_ is proved by induction on a typing derivation.
-    chapter.  The one case that is significantly different is the one for the
+    derivation, pretty much as we did in chapter [Types]({{ "Types" | relative_url }})
+  -->
+
+  - The one case that is significantly different is the one for the
     `βλ·` rule, whose definition uses the substitution operation.  To see that
     this step preserves typing, we need to know that the substitution itself
     does.  So we prove a ... 
@@ -589,11 +596,21 @@ preservation (𝔹-E ⊢L ⊢M ⊢N) (ξif L⟹L′) with preservation ⊢L L⟹
 
 #### Exercise: 2 stars, recommended (subject_expansion_stlc)
 
+<!--
 An exercise in the [Types]({{ "Types" | relative_url }}) chapter asked about the
 subject expansion property for the simple language of arithmetic and boolean
 expressions.  Does this property hold for STLC?  That is, is it always the case
 that, if `M ==> N` and `∅ ⊢ N ∶ A`, then `∅ ⊢ M ∶ A`?  It is easy to find a
 counter-example with conditionals, find one not involving conditionals.
+-->
+
+We say that `M` _reduces_ to `N` if `M ⟹ N`,
+and that `M` _expands_ to `N` if `N ⟹ M`.
+The preservation property is sometimes called _subject reduction_.
+Its opposite is _subject expansion_, which holds if
+`M ==> N` and `∅ ⊢ N ∶ A`, then `∅ ⊢ M ∶ A`.
+Find two counter-examples to subject expansion, one
+with conditionals and one not involving conditionals.
 
 ## Type Soundness