From 6f446bcec7af7dc9ef7efc8371c0691f0842f8a9 Mon Sep 17 00:00:00 2001 From: wadler Date: Mon, 9 Jul 2018 18:41:57 -0300 Subject: [PATCH] reviewing section headings --- src/plfa/DeBruijn.lagda | 26 +++++++-------- src/plfa/Lambda.lagda | 21 ++++++------- src/plfa/More.lagda | 66 ++++++++++++++++++++++++++++----------- src/plfa/Properties.lagda | 7 ----- 4 files changed, 69 insertions(+), 51 deletions(-) diff --git a/src/plfa/DeBruijn.lagda b/src/plfa/DeBruijn.lagda index 6ac26559..8cb770e5 100644 --- a/src/plfa/DeBruijn.lagda +++ b/src/plfa/DeBruijn.lagda @@ -214,7 +214,7 @@ For each new section, we show the corresponding old section or sections. * DeBruijn: Inherently typed de Bruijn representation - + Inherently typed terms (1.1, 1.5) + + Syntax (1.1, 1.5) + Values (1.2, 2.1) + Renaming (2.3) + Substitution (1.3, 2.3) @@ -222,16 +222,14 @@ sections. + Progress (2.2) + Evaluation (2.6) -The definition of terms now combines both the syntax of terms -and their typing rules, and the definition of values now -incorporates the Canonical Forms lemma. The definition of -substitution is somewhat more involved, but incorporates the -trickiest part of the previous proof, the lemma establishing -that substitution preserves types. The definition of -reduction incorporates preservation, which no longer requires -a separate proof. +The syntax of terms now incorporates their typing rules, and the +definition of values now incorporates the Canonical Forms lemma. The +definition of substitution is somewhat more involved, but incorporates +the trickiest part of the previous proof, the lemma establishing that +substitution preserves types. The definition of reduction +incorporates preservation, which no longer requires a separate proof. -## Inherently typed terms +## Syntax We now begin our formal development. @@ -423,7 +421,7 @@ _ = ƛ ƛ (` S Z · (` S Z · ` Z)) The final inherently-typed term represents the Church numeral two. -### A convenient abbreviation +### Abbreviating de Bruijn indices We can use a natural number to select a type from a context. \begin{code} @@ -775,7 +773,7 @@ And combining definition with proof makes it harder for errors to sneak in. -## Reductions +## Reduction With substitution out of the way, it is straightforward to define values and reduction. @@ -869,7 +867,7 @@ preserves types, which we previously is built-in to our definition of substitution. -## Reflexive and transitive closure +### Reflexive and transitive closure The reflexive and transitive closure is exactly as before. We simply cut-and-paste the previous definition. @@ -899,7 +897,7 @@ begin M—↠N = M—↠N \end{code} -### Examples +## Examples We reiterate each of our previous examples. First, the Church numeral two applied to the successor function and zero yields diff --git a/src/plfa/Lambda.lagda b/src/plfa/Lambda.lagda index 64cefc22..85ae468a 100644 --- a/src/plfa/Lambda.lagda +++ b/src/plfa/Lambda.lagda @@ -10,13 +10,6 @@ permalink : /Lambda/ module plfa.Lambda where \end{code} - - 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 captures the key concept of @@ -675,6 +668,13 @@ The three constructors specify, respectively, that `—↠` includes `—→` and is reflexive and transitive. A good exercise is to show that the two definitions are equivalent (indeed, isomoprhic). +#### Exercise (`—↠≃—↠′`) + +Show that the two notions of reflexive and transitive closure +above are isomorphic. + +## Confluence + One important property a reduction relation might satisfy is to be _confluent_. If term `L` reduces to two other terms, `M` and `N`, then both of these reduce to a common term `P`. @@ -721,11 +721,6 @@ the diamond property, and that every relation that satisfies the diamond property is confluent. Hence, all the reduction systems studied in this text are trivially confluent. -#### Exercise (`—↠≃—↠′`) - -Show that the two notions of reflexive and transitive closure -above are isomorphic. - ## Examples @@ -1302,3 +1297,5 @@ This chapter uses the following unicode ⊢ U+22A2: RIGHT TACK (\vdash or \|-) ⦂ U+2982: Z NOTATION TYPE COLON (\:) +We compose reduction —→ from an em dash — and an arrow →. +Similarly for reflexive and transitive closure —↠. diff --git a/src/plfa/More.lagda b/src/plfa/More.lagda index aa6f27ca..d5858c2c 100644 --- a/src/plfa/More.lagda +++ b/src/plfa/More.lagda @@ -10,14 +10,22 @@ module plfa.More where So far, we have focussed on a relatively minimal language, based on Plotkin's PCF, which supports functions, naturals, and fixpoints. In -this chapter we extend our calculus to support `let` bindings and more -datatypes, including products, sums, unit type, empty type, and lists, -all of which are familiar from Part I of this textbook. We also give -alternative formulations of products and unit type. For `let` and the -alternative formulations we show how they translate to other constructs -in the calculus. Most of the description will be informal. We show -how to formalise a few of the constructs and leave the rest as an -exercise for the reader. +this chapter we extend our calculus to support the following: + + * _let_ bindings + * products + * an alternative formulation of products + * sums + * unit type + * and an alternative formulation of unit type + * empty type + * lists + +All of the data types should be familiar from Part I of this textbook. +For _let_ and the alternative formulations we show how they translate +to other constructs in the calculus. Most of the description will be +informal. We show how to formalise the first three constructs and leave +the rest as an exercise for the reader. Our informal descriptions will be in the style of Chapter [Lambda]({{ site.baseurl }}{% link out/plfa/Lambda.md %}), @@ -29,8 +37,8 @@ using de Bruijn indices and inherently typed terms. By now, explaining with symbols should be more concise, more precise, and easier to follow than explaining in prose. For each construct, we give syntax, typing, reductions, and an example. -We also give translations where relevant. Formally establishing the -correctness of such translations will be the subject of the next chapter. +We also give translations where relevant; formally establishing the +correctness of translations will be the subject of the next chapter. ## Let bindings @@ -484,6 +492,17 @@ Here is the map function for lists. | x ∷ xs ⇒ f · x `∷ ml · f · xs ] +## Formalisation + +We now show how to formalise + + * _let_ bindings + * products + * an alternative formulation of products + +and leave formalisation of the remaining constructs as an exercise. + + ## Imports \begin{code} @@ -521,7 +540,11 @@ infix 9 #_ infixr 6 _V-∷_ infix 8 V-suc_ +\end{code} +### Types + +\begin{code} data Type : Set where `ℕ : Type _⇒_ : Type → Type → Type @@ -530,11 +553,19 @@ data Type : Set where `⊤ : Type `⊥ : Type `List : Type → Type +\end{code} +### Contexts + +\begin{code} data Context : Set where ∅ : Context _,_ : Context → Type → Context +\end{code} +### Variables and the lookup judgement + +\begin{code} data _∋_ : Context → Type → Set where Z : ∀ {Γ A} @@ -545,7 +576,11 @@ data _∋_ : Context → Type → Set where → Γ ∋ B --------- → Γ , A ∋ B +\end{code} +### Terms and the typing judgment + +\begin{code} data _⊢_ : Context → Type → Set where -- variables @@ -695,22 +730,17 @@ lookup (Γ , A) zero = A lookup (Γ , _) (suc n) = lookup Γ n lookup ∅ _ = ⊥-elim impossible where postulate impossible : ⊥ -\end{code} -\begin{code} count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n count {Γ , _} zero = Z count {Γ , _} (suc n) = S (count n) count {∅} _ = ⊥-elim impossible where postulate impossible : ⊥ -\end{code} -\begin{code} #_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n # n = ` count n \end{code} - ## Substitution ### Renaming @@ -803,7 +833,7 @@ _[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} σ N σ (S (S x)) = ` x \end{code} -## Reductions +## Reduction ### Value @@ -869,7 +899,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where Implicit arguments need to be supplied when they are not fixed by the given arguments. -## Reduction +### Reduction step \begin{code} infix 2 _—→_ @@ -1056,7 +1086,7 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where → caseL (V `∷ W) M N —→ N [ V ][ W ] \end{code} -## Reflexive and transitive closure +### Reflexive and transitive closure \begin{code} infix 2 _—↠_ diff --git a/src/plfa/Properties.lagda b/src/plfa/Properties.lagda index 5099e7d1..48f7b931 100644 --- a/src/plfa/Properties.lagda +++ b/src/plfa/Properties.lagda @@ -8,10 +8,6 @@ permalink : /Properties/ module plfa.Properties where \end{code} -[Parts of this chapter take their text from chapter _StlcProp_ -of _Software Foundations_ (_Programming Language Foundations_). -Those parts will be revised.] - This chapter covers properties of the simply-typed lambda calculus, as introduced in the previous chapter. The most important of these properties are progress and preservation. We introduce these below, @@ -1431,9 +1427,6 @@ checker complains, because the arguments have merely switched order and neither is smaller. - - - #### Exercise: `progress-preservation` Without peeking at their statements above, write down the progress