reviewing section headings
This commit is contained in:
wadler
parent
b0ccc95e5e
commit
6f446bcec7
4 changed files with 69 additions and 51 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -10,13 +10,6 @@ permalink : /Lambda/
|
|||
module plfa.Lambda where
|
||||
\end{code}
|
||||
|
||||
<!--
|
||||
[This chapter was originally based on Chapter _Stlc_
|
||||
of _Software Foundations_ (_Programming Language Foundations_).
|
||||
It has now been updated, but if you spot any plagiarism
|
||||
please let me know. – P]
|
||||
-->
|
||||
|
||||
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 —↠.
|
||||
|
|
|
|||
|
|
@ -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 _—↠_
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue