michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fixes #355

Browse source
This commit is contained in:
Wen Kokke 2019-07-18 11:15:08 +01:00
parent f6b899dd4e
commit 56ca94be1b
16 changed files with 72 additions and 72 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/plfa/Bisimulation.lagda.md
View file

@ -119,14 +119,14 @@ above is a simulation from source to target. We leave
establishing it in the reverse direction as an exercise. establishing it in the reverse direction as an exercise.
Another exercise is to show the alternative formulations Another exercise is to show the alternative formulations
of products in of products in
Chapter [More][plfa.More] Chapter [More]({{ site.baseurl }}/More/)
are in bisimulation. are in bisimulation.
## Imports ## Imports
We import our source language from We import our source language from
Chapter [More][plfa.More]: Chapter [More]({{ site.baseurl }}/More/):
``` ```
open import plfa.More open import plfa.More
``` ```
@ -164,7 +164,7 @@ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
---------------------- ----------------------
→ `let M N ~ (ƛ N†) · M† → `let M N ~ (ƛ N†) · M†
``` ```
The language in Chapter [More][plfa.More] has more constructs, which we could easily add. The language in Chapter [More]({{ site.baseurl }}/More/) has more constructs, which we could easily add.
However, leaving the simulation small let's us focus on the essence. However, leaving the simulation small let's us focus on the essence.
It's a handy technical trick that we can have a large source language, It's a handy technical trick that we can have a large source language,
but only bother to include in the simulation the terms of interest. but only bother to include in the simulation the terms of interest.
@ -468,7 +468,7 @@ a bisimulation.
#### Exercise `products` #### Exercise `products`
Show that the two formulations of products in Show that the two formulations of products in
Chapter [More][plfa.More] Chapter [More]({{ site.baseurl }}/More/)
are in bisimulation. The only constructs you need to include are are in bisimulation. The only constructs you need to include are
variables, and those connected to functions and products. variables, and those connected to functions and products.
In this case, the simulation is _not_ lock-step. In this case, the simulation is _not_ lock-step.

6
src/plfa/Connectives.lagda.md
View file

@ -234,7 +234,7 @@ corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter.
#### Exercise `⇔≃×` (recommended) #### Exercise `⇔≃×` (recommended)
Show that `A ⇔ B` as defined [earlier][plfa.Isomorphism#iff] Show that `A ⇔ B` as defined [earlier]({{ site.baseurl }}/Isomorphism/#iff)
is isomorphic to `(A → B) × (B → A)`. is isomorphic to `(A → B) × (B → A)`.
``` ```
@ -770,9 +770,9 @@ The standard library constructs pairs with `_,_` whereas we use `⟨_,_⟩`.
The former makes it convenient to build triples or larger tuples from pairs, The former makes it convenient to build triples or larger tuples from pairs,
permitting `a , b , c` to stand for `(a , (b , c))`. But it conflicts with permitting `a , b , c` to stand for `(a , (b , c))`. But it conflicts with
other useful notations, such as `[_,_]` to construct a list of two elements in other useful notations, such as `[_,_]` to construct a list of two elements in
Chapter [Lists][plfa.Lists] Chapter [Lists]({{ site.baseurl }}/Lists/)
and `Γ , A` to extend environments in and `Γ , A` to extend environments in
Chapter [DeBruijn][plfa.DeBruijn]. Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
The standard library `_⇔_` is similar to ours, but the one in the The standard library `_⇔_` is similar to ours, but the one in the
standard library is less convenient, since it is parameterised with standard library is less convenient, since it is parameterised with
respect to an arbitrary notion of equivalence. respect to an arbitrary notion of equivalence.

14
src/plfa/DeBruijn.lagda.md
View file

@ -56,10 +56,10 @@ And here is its corresponding type derivation:
∋z = Z ∋z = Z
(These are both taken from Chapter (These are both taken from Chapter
[Lambda][plfa.Lambda] [Lambda]({{ site.baseurl }}/Lambda/)
and you can see the corresponding derivation tree written out and you can see the corresponding derivation tree written out
in full in full
[here][plfa.Lambda#derivation].) [here]({{ site.baseurl }}/Lambda/#derivation).)
The two definitions are in close correspondence, where: The two definitions are in close correspondence, where:
* `` `_ `` corresponds to `` ⊢` `` * `` `_ `` corresponds to `` ⊢` ``
@ -112,7 +112,7 @@ typed terms, which in context `Γ` have type `A`.
While these two choices fit well, they are independent. One While these two choices fit well, they are independent. One
can use de Bruijn indices in raw terms, or (with more can use de Bruijn indices in raw terms, or (with more
difficulty) have inherently typed terms with names. In difficulty) have inherently typed terms with names. In
Chapter [Untyped][plfa.Untyped], Chapter [Untyped]({{ site.baseurl }}/Untyped/),
we will introduce terms with de Bruijn indices that we will introduce terms with de Bruijn indices that
are inherently scoped but not typed. are inherently scoped but not typed.
@ -408,7 +408,7 @@ lookup ∅ _ = ⊥-elim impossible
We intend to apply the function only when the natural is We intend to apply the function only when the natural is
shorter than the length of the context, which we indicate by shorter than the length of the context, which we indicate by
postulating an `impossible` term, just as we did postulating an `impossible` term, just as we did
[here][plfa.Lambda#impossible]. [here]({{ site.baseurl }}/Lambda/#impossible).
Given the above, we can convert a natural to a corresponding Given the above, we can convert a natural to a corresponding
de Bruijn index, looking up its type in the context: de Bruijn index, looking up its type in the context:
@ -437,9 +437,9 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0))
### Test examples ### Test examples
We repeat the test examples from We repeat the test examples from
Chapter [Lambda][plfa.Lambda]. Chapter [Lambda]({{ site.baseurl }}/Lambda/).
You can find them You can find them
[here][plfa.Lambda#derivation] [here]({{ site.baseurl }}/Lambda/#derivation)
for comparison. for comparison.
First, computing two plus two on naturals: First, computing two plus two on naturals:
@ -772,7 +772,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
Here `zero` requires an implicit parameter to aid inference, Here `zero` requires an implicit parameter to aid inference,
much in the same way that `[]` did in much in the same way that `[]` did in
[Lists][plfa.Lists]. [Lists]({{ site.baseurl }}/Lists/).
## Reduction ## Reduction

4
src/plfa/Decidable.lagda.md
View file

@ -39,7 +39,7 @@ open import plfa.Isomorphism using (_⇔_)
## Evidence vs Computation ## Evidence vs Computation
Recall that Chapter [Relations][plfa.Relations] Recall that Chapter [Relations]({{ site.baseurl }}/Relations/)
defined comparison as an inductive datatype, defined comparison as an inductive datatype,
which provides _evidence_ that one number which provides _evidence_ that one number
is less than or equal to another: is less than or equal to another:
@ -548,7 +548,7 @@ postulate
#### Exercise `iff-erasure` (recommended) #### Exercise `iff-erasure` (recommended)
Give analogues of the `_⇔_` operation from Give analogues of the `_⇔_` operation from
Chapter [Isomorphism][plfa.Isomorphism#iff], Chapter [Isomorphism]({{ site.baseurl }}/Isomorphism/#iff),
operation on booleans and decidables, and also show the corresponding erasure: operation on booleans and decidables, and also show the corresponding erasure:
``` ```
postulate postulate

2
src/plfa/Equality.lagda.md
View file

@ -347,7 +347,7 @@ an order that will make sense to the reader.
#### Exercise `≤-Reasoning` (stretch) #### Exercise `≤-Reasoning` (stretch)
The proof of monotonicity from The proof of monotonicity from
Chapter [Relations][plfa.Relations] Chapter [Relations]({{ site.baseurl }}/Relations/)
can be written in a more readable form by using an analogue of our can be written in a more readable form by using an analogue of our
notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use
it to write out an alternative proof that addition is monotonic with it to write out an alternative proof that addition is monotonic with

10
src/plfa/Induction.lagda.md
View file

@ -366,7 +366,7 @@ proof of associativity.
The symbol `∀` appears in the statement of associativity to indicate that The symbol `∀` appears in the statement of associativity to indicate that
it holds for all numbers `m`, `n`, and `p`. We refer to `∀` as the _universal it holds for all numbers `m`, `n`, and `p`. We refer to `∀` as the _universal
quantifier_, and it is discussed further in Chapter [Quantifiers][plfa.Quantifiers]. quantifier_, and it is discussed further in Chapter [Quantifiers]({{ site.baseurl }}/Quantifiers/).
Evidence for a universal quantifier is a function. The notations Evidence for a universal quantifier is a function. The notations
@ -697,11 +697,11 @@ judgments where the first number is less than _m_.
There is also a completely finite approach to generating the same equations, There is also a completely finite approach to generating the same equations,
which is left as an exercise for the reader. which is left as an exercise for the reader.
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc} #### Exercise `finite-|-assoc` (stretch) {#finite-plus-assoc}
Write out what is known about associativity of addition on each of the Write out what is known about associativity of addition on each of the
first four days using a finite story of creation, as first four days using a finite story of creation, as
[earlier][plfa.Naturals#finite-creation]. [earlier]({{ site.baseurl }}/Naturals/#finite-creation).
``` ```
-- Your code goes here -- Your code goes here
@ -927,7 +927,7 @@ for all naturals `n`. Did your proof require induction?
``` ```
#### Exercise `∸-+-assoc` {#monus-plus-assoc} #### Exercise `∸-|-assoc` {#monus-plus-assoc}
Show that monus associates with addition, that is, Show that monus associates with addition, that is,
@ -954,7 +954,7 @@ for all `m`, `n`, and `p`.
#### Exercise `Bin-laws` (stretch) {#Bin-laws} #### Exercise `Bin-laws` (stretch) {#Bin-laws}
Recall that Recall that
Exercise [Bin][plfa.Naturals#Bin] Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin)
defines a datatype of bitstrings representing natural numbers defines a datatype of bitstrings representing natural numbers
``` ```
data Bin : Set where data Bin : Set where

36
src/plfa/Inference.lagda.md
View file

@ -12,9 +12,9 @@ module plfa.Inference where
So far in our development, type derivations for the corresponding So far in our development, type derivations for the corresponding
term have been provided by fiat. term have been provided by fiat.
In Chapter [Lambda][plfa.Lambda] In Chapter [Lambda]({{ site.baseurl }}/Lambda/)
type derivations were given separately from the term, while type derivations were given separately from the term, while
in Chapter [DeBruijn][plfa.DeBruijn] in Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/)
the type derivation was inherently part of the term. the type derivation was inherently part of the term.
In practice, one often writes down a term with a few decorations and In practice, one often writes down a term with a few decorations and
@ -27,9 +27,9 @@ inference, which will be presented in this chapter.
This chapter ties our previous developments together. We begin with This chapter ties our previous developments together. We begin with
a term with some type annotations, quite close to the raw terms of a term with some type annotations, quite close to the raw terms of
Chapter [Lambda][plfa.Lambda], Chapter [Lambda]({{ site.baseurl }}/Lambda/),
and from it we compute a term with inherent types, in the style of and from it we compute a term with inherent types, in the style of
Chapter [DeBruijn][plfa.DeBruijn]. Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
## Introduction: Inference rules as algorithms {#algorithms} ## Introduction: Inference rules as algorithms {#algorithms}
@ -382,7 +382,7 @@ required for `sucᶜ`, which inherits its type as an argument of `plusᶜ`.
## Bidirectional type checking ## Bidirectional type checking
The typing rules for variables are as in The typing rules for variables are as in
[Lambda][plfa.Lambda]: [Lambda]({{ site.baseurl }}/Lambda/):
``` ```
data _∋_⦂_ : Context → Id → Type → Set where data _∋_⦂_ : Context → Id → Type → Set where
@ -456,25 +456,25 @@ data _⊢_↓_ where
→ Γ ⊢ (M ↑) ↓ B → Γ ⊢ (M ↑) ↓ B
``` ```
We follow the same convention as We follow the same convention as
Chapter [Lambda][plfa.Lambda], Chapter [Lambda]({{ site.baseurl }}/Lambda/),
prefacing the constructor with `⊢` to derive the name of the prefacing the constructor with `⊢` to derive the name of the
corresponding type rule. corresponding type rule.
The rules are similar to those in The rules are similar to those in
Chapter [Lambda][plfa.Lambda], Chapter [Lambda]({{ site.baseurl }}/Lambda/),
modified to support synthesised and inherited types. modified to support synthesised and inherited types.
The two new rules are those for `⊢↑` and `⊢↓`. The two new rules are those for `⊢↑` and `⊢↓`.
The former both passes the type decoration as the inherited type and returns The former both passes the type decoration as the inherited type and returns
it as the synthesised type. The latter takes the synthesised type and the it as the synthesised type. The latter takes the synthesised type and the
inherited type and confirms they are identical --- it should remind you of inherited type and confirms they are identical --- it should remind you of
the equality test in the application rule in the first the equality test in the application rule in the first
[section][plfa.Inference#algorithms]. [section]({{ site.baseurl }}/Inference/#algorithms).
#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul} #### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
Rewrite your definition of multiplication from Rewrite your definition of multiplication from
Chapter [Lambda][plfa.Lambda], decorated to support inference. Chapter [Lambda]({{ site.baseurl }}/Lambda/), decorated to support inference.
``` ```
-- Your code goes here -- Your code goes here
@ -484,7 +484,7 @@ Chapter [Lambda][plfa.Lambda], decorated to support inference.
#### Exercise `bidirectional-products` (recommended) {#bidirectional-products} #### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
Extend the bidirectional type rules to include products from Extend the bidirectional type rules to include products from
Chapter [More][plfa.More]. Chapter [More]({{ site.baseurl }}/More/).
``` ```
-- Your code goes here -- Your code goes here
@ -494,7 +494,7 @@ Chapter [More][plfa.More].
#### Exercise `bidirectional-rest` (stretch) #### Exercise `bidirectional-rest` (stretch)
Extend the bidirectional type rules to include the rest of the constructs from Extend the bidirectional type rules to include the rest of the constructs from
Chapter [More][plfa.More]. Chapter [More]({{ site.baseurl }}/More/).
``` ```
-- Your code goes here -- Your code goes here
@ -1004,7 +1004,7 @@ _ = refl
From the evidence that a decorated term has the correct type it is From the evidence that a decorated term has the correct type it is
easy to extract the corresponding inherently typed term. We use the easy to extract the corresponding inherently typed term. We use the
name `DB` to refer to the code in name `DB` to refer to the code in
Chapter [DeBruijn][plfa.DeBruijn]. Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
It is easy to define an _erasure_ function that takes evidence of a It is easy to define an _erasure_ function that takes evidence of a
type judgment into the corresponding inherently typed term. type judgment into the corresponding inherently typed term.
@ -1067,17 +1067,17 @@ _ = refl
``` ```
Thus, we have confirmed that bidirectional type inference Thus, we have confirmed that bidirectional type inference
converts decorated versions of the lambda terms from converts decorated versions of the lambda terms from
Chapter [Lambda][plfa.Lambda] Chapter [Lambda]({{ site.baseurl }}/Lambda/)
to the inherently typed terms of to the inherently typed terms of
Chapter [DeBruijn][plfa.DeBruijn]. Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
#### Exercise `inference-multiplication` (recommended) #### Exercise `inference-multiplication` (recommended)
Apply inference to your decorated definition of multiplication from Apply inference to your decorated definition of multiplication from
exercise [`bidirectional-mul`][plfa.Inference#bidirectional-mul], and show that exercise [`bidirectional-mul`]({{ site.baseurl }}/Inference/#bidirectional-mul), and show that
erasure of the inferred typing yields your definition of erasure of the inferred typing yields your definition of
multiplication from Chapter [DeBruijn][plfa.DeBruijn]. multiplication from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/).
``` ```
-- Your code goes here -- Your code goes here
@ -1086,7 +1086,7 @@ multiplication from Chapter [DeBruijn][plfa.DeBruijn].
#### Exercise `inference-products` (recommended) #### Exercise `inference-products` (recommended)
Using your rules from exercise Using your rules from exercise
[`bidirectional-products`][plfa.Inference#bidirectional-products], extend [`bidirectional-products`]({{ site.baseurl }}/Inference/#bidirectional-products), extend
bidirectional inference to include products. bidirectional inference to include products.
``` ```
@ -1096,7 +1096,7 @@ bidirectional inference to include products.
#### Exercise `inference-rest` (stretch) #### Exercise `inference-rest` (stretch)
Extend the bidirectional type rules to include the rest of the constructs from Extend the bidirectional type rules to include the rest of the constructs from
Chapter [More][plfa.More]. Chapter [More]({{ site.baseurl }}/More/).
``` ```
-- Your code goes here -- Your code goes here

8
src/plfa/Isomorphism.lagda.md
View file

@ -89,7 +89,7 @@ Extensionality asserts that the only way to distinguish functions is
by applying them; if two functions applied to the same argument always by applying them; if two functions applied to the same argument always
yield the same result, then they are the same function. It is the yield the same result, then they are the same function. It is the
converse of `cong-app`, as introduced converse of `cong-app`, as introduced
[earlier][plfa.Equality#cong]. [earlier]({{ site.baseurl }}/Equality/#cong).
Agda does not presume extensionality, but we can postulate that it holds: Agda does not presume extensionality, but we can postulate that it holds:
``` ```
@ -104,7 +104,7 @@ known to be consistent with the theory that underlies Agda.
As an example, consider that we need results from two libraries, As an example, consider that we need results from two libraries,
one where addition is defined, as in one where addition is defined, as in
Chapter [Naturals][plfa.Naturals], Chapter [Naturals]({{ site.baseurl }}/Naturals/),
and one where it is defined the other way around. and one where it is defined the other way around.
``` ```
_+′_ : ℕ → ℕ → ℕ _+′_ : ℕ → ℕ → ℕ
@ -456,8 +456,8 @@ Show that equivalence is reflexive, symmetric, and transitive.
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding} #### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
Recall that Exercises Recall that Exercises
[Bin][plfa.Naturals#Bin] and [Bin]({{ site.baseurl }}/Naturals/#Bin) and
[Bin-laws][plfa.Induction#Bin-laws] [Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws)
define a datatype of bitstrings representing natural numbers: define a datatype of bitstrings representing natural numbers:
``` ```
data Bin : Set where data Bin : Set where

12
src/plfa/Lambda.lagda.md
View file

@ -25,7 +25,7 @@ recursive function definitions.
This chapter formalises the simply-typed lambda calculus, giving its This chapter formalises the simply-typed lambda calculus, giving its
syntax, small-step semantics, and typing rules. The next chapter syntax, small-step semantics, and typing rules. The next chapter
[Properties][plfa.Properties] [Properties]({{ site.baseurl }}/Properties/)
proves its main properties, including proves its main properties, including
progress and preservation. Following chapters will look at a number progress and preservation. Following chapters will look at a number
of variants of lambda calculus. of variants of lambda calculus.
@ -33,7 +33,7 @@ of variants of lambda calculus.
Be aware that the approach we take here is _not_ our recommended Be aware that the approach we take here is _not_ our recommended
approach to formalisation. Using de Bruijn indices and approach to formalisation. Using de Bruijn indices and
inherently-typed terms, as we will do in inherently-typed terms, as we will do in
Chapter [DeBruijn][plfa.DeBruijn], Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
leads to a more compact formulation. Nonetheless, we begin with named leads to a more compact formulation. Nonetheless, we begin with named
variables, partly because such terms are easier to read and partly variables, partly because such terms are easier to read and partly
because the development is more traditional. because the development is more traditional.
@ -138,7 +138,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
``` ```
The recursive definition of addition is similar to our original The recursive definition of addition is similar to our original
definition of `_+_` for naturals, as given in definition of `_+_` for naturals, as given in
Chapter [Naturals][plfa.Naturals#plus]. Chapter [Naturals]({{ site.baseurl }}/Naturals/#plus).
Here variable "m" is bound twice, once in a lambda abstraction and once in Here variable "m" is bound twice, once in a lambda abstraction and once in
the successor branch of the case; the first use of "m" refers to the successor branch of the case; the first use of "m" refers to
the former and the second to the latter. Any use of "m" in the successor branch the former and the second to the latter. Any use of "m" in the successor branch
@ -373,7 +373,7 @@ to treat variables as values, and to treat
`ƛ x ⇒ N` as a value only if `N` is a value. `ƛ x ⇒ N` as a value only if `N` is a value.
Indeed, this is how Agda normalises terms. Indeed, this is how Agda normalises terms.
We consider this approach in We consider this approach in
Chapter [Untyped][plfa.Untyped]. Chapter [Untyped]({{ site.baseurl }}/Untyped/).
## Substitution ## Substitution
@ -678,7 +678,7 @@ the reflexive and transitive closure `—↠` of the step relation `—→`.
We define reflexive and transitive closure as a sequence of zero or We define reflexive and transitive closure as a sequence of zero or
more steps of the underlying relation, along lines similar to that for more steps of the underlying relation, along lines similar to that for
reasoning about chains of equalities in reasoning about chains of equalities in
Chapter [Equality][plfa.Equality]: Chapter [Equality]({{ site.baseurl }}/Equality/):
``` ```
infix 2 _—↠_ infix 2 _—↠_
infix 1 begin_ infix 1 begin_
@ -1310,7 +1310,7 @@ We can fill in `Z` by hand. If we type C-c C-space, Agda will confirm we are don
The entire process can be automated using Agsy, invoked with C-c C-a. The entire process can be automated using Agsy, invoked with C-c C-a.
Chapter [Inference][plfa.Inference] Chapter [Inference]({{ site.baseurl }}/Inference/)
will show how to use Agda to compute type derivations directly. will show how to use Agda to compute type derivations directly.

4
src/plfa/Lists.lagda.md
View file

@ -178,7 +178,7 @@ and follows by straightforward computation combined with the
inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive
invocation of the proof, in this case `++-assoc xs ys zs`. invocation of the proof, in this case `++-assoc xs ys zs`.
Recall that Agda supports [sections][plfa.Induction#sections]. Recall that Agda supports [sections]({{ site.baseurl }}/Induction/#sections).
Applying `cong (x ∷_)` promotes the inductive hypothesis: Applying `cong (x ∷_)` promotes the inductive hypothesis:
(xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
@ -932,7 +932,7 @@ Show that the equivalence `All-++-⇔` can be extended to an isomorphism.
#### Exercise `¬Any≃All¬` (stretch) #### Exercise `¬Any≃All¬` (stretch)
First generalise composition to arbitrary levels, using First generalise composition to arbitrary levels, using
[universe polymorphism][plfa.Equality#unipoly]: [universe polymorphism]({{ site.baseurl }}/Equality/#unipoly):
``` ```
_∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃} _∘′_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C : Set ℓ₃}
→ (B → C) → (A → B) → A → C → (B → C) → (A → B) → A → C

4
src/plfa/More.lagda.md
View file

@ -31,10 +31,10 @@ informal. We show how to formalise the first four constructs and leave
the rest as an exercise for the reader. the rest as an exercise for the reader.
Our informal descriptions will be in the style of Our informal descriptions will be in the style of
Chapter [Lambda][plfa.Lambda], Chapter [Lambda]({{ site.baseurl }}/Lambda/),
using named variables and a separate type relation, using named variables and a separate type relation,
while our formalisation will be in the style of while our formalisation will be in the style of
Chapter [DeBruijn][plfa.DeBruijn], Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
using de Bruijn indices and inherently typed terms. using de Bruijn indices and inherently typed terms.
By now, explaining with symbols should be more concise, more precise, By now, explaining with symbols should be more concise, more precise,

2
src/plfa/Naturals.lagda.md
View file

@ -277,7 +277,7 @@ all the names specified in the `using` clause into the current scope.
In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We
will see how these are used below. We take these as givens for now, will see how these are used below. We take these as givens for now,
but will see how they are defined in but will see how they are defined in
Chapter [Equality][plfa.Equality]. Chapter [Equality]({{ site.baseurl }}/Equality/).
Agda uses underbars to indicate where terms appear in infix or mixfix Agda uses underbars to indicate where terms appear in infix or mixfix
operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written

4
src/plfa/Negation.lagda.md
View file

@ -189,7 +189,7 @@ again causing the equality to hold trivially.
#### Exercise `<-irreflexive` (recommended) #### Exercise `<-irreflexive` (recommended)
Using negation, show that Using negation, show that
[strict inequality][plfa.Relations#strict-inequality] [strict inequality]({{ site.baseurl }}/Relations/#strict-inequality)
is irreflexive, that is, `n < n` holds for no `n`. is irreflexive, that is, `n < n` holds for no `n`.
``` ```
@ -200,7 +200,7 @@ is irreflexive, that is, `n < n` holds for no `n`.
#### Exercise `trichotomy` #### Exercise `trichotomy`
Show that strict inequality satisfies Show that strict inequality satisfies
[trichotomy][plfa.Relations#trichotomy], [trichotomy]({{ site.baseurl }}/Relations/#trichotomy),
that is, for any naturals `m` and `n` exactly one of the following holds: that is, for any naturals `m` and `n` exactly one of the following holds:
* `m < n` * `m < n`

14
src/plfa/Quantifiers.lagda.md
View file

@ -90,7 +90,7 @@ postulate
(∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x)
``` ```
Compare this with the result (`→-distrib-×`) in Compare this with the result (`→-distrib-×`) in
Chapter [Connectives][plfa.Connectives]. Chapter [Connectives]({{ site.baseurl }}/Connectives/).
#### Exercise `⊎∀-implies-∀⊎` #### Exercise `⊎∀-implies-∀⊎`
@ -233,7 +233,7 @@ Indeed, the converse also holds, and the two together form an isomorphism:
``` ```
The result can be viewed as a generalisation of currying. Indeed, the code to The result can be viewed as a generalisation of currying. Indeed, the code to
establish the isomorphism is identical to what we wrote when discussing establish the isomorphism is identical to what we wrote when discussing
[implication][plfa.Connectives#implication]. [implication]({{ site.baseurl }}/Connectives/#implication).
#### Exercise `∃-distrib-⊎` (recommended) #### Exercise `∃-distrib-⊎` (recommended)
@ -263,7 +263,7 @@ Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`.
## An existential example ## An existential example
Recall the definitions of `even` and `odd` from Recall the definitions of `even` and `odd` from
Chapter [Relations][plfa.Relations]: Chapter [Relations]({{ site.baseurl }}/Relations/):
``` ```
data even : ℕ → Set data even : ℕ → Set
data odd : ℕ → Set data odd : ℕ → Set
@ -371,7 +371,7 @@ restated in this way.
-- Your code goes here -- Your code goes here
``` ```
#### Exercise `∃-+-≤` #### Exercise `∃-|-≤`
Show that `y ≤ z` holds if and only if there exists a `x` such that Show that `y ≤ z` holds if and only if there exists a `x` such that
`x + y ≡ z`. `x + y ≡ z`.
@ -432,9 +432,9 @@ Does the converse hold? If so, prove; if not, explain why.
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism} #### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
Recall that Exercises Recall that Exercises
[Bin][plfa.Naturals#Bin], [Bin]({{ site.baseurl }}/Naturals/#Bin),
[Bin-laws][plfa.Induction#Bin-laws], and [Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and
[Bin-predicates][plfa.Relations#Bin-predicates] [Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates)
define a datatype of bitstrings representing natural numbers: define a datatype of bitstrings representing natural numbers:
``` ```
data Bin : Set where data Bin : Set where

12
src/plfa/Relations.lagda.md
View file

@ -155,7 +155,7 @@ either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`.
Given two numbers, it is straightforward to compute whether or not the Given two numbers, it is straightforward to compute whether or not the
first is less than or equal to the second. We don't give the code for first is less than or equal to the second. We don't give the code for
doing so here, but will return to this point in doing so here, but will return to this point in
Chapter [Decidable][plfa.Decidable]. Chapter [Decidable]({{ site.baseurl }}/Decidable/).
## Inversion ## Inversion
@ -377,7 +377,7 @@ evidence of `m ≤ n` and `n ≤ m` respectively.
(For those familiar with logic, the above definition (For those familiar with logic, the above definition
could also be written as a disjunction. Disjunctions will could also be written as a disjunction. Disjunctions will
be introduced in Chapter [Connectives][plfa.Connectives].) be introduced in Chapter [Connectives]({{ site.baseurl }}/Connectives/).)
This is our first use of a datatype with _parameters_, This is our first use of a datatype with _parameters_,
in this case `m` and `n`. It is equivalent to the following in this case `m` and `n`. It is equivalent to the following
@ -572,7 +572,7 @@ It is also monotonic with regards to addition and multiplication.
Most of the above are considered in exercises below. Irreflexivity Most of the above are considered in exercises below. Irreflexivity
requires negation, as does the fact that the three cases in requires negation, as does the fact that the three cases in
trichotomy are mutually exclusive, so those points are deferred to trichotomy are mutually exclusive, so those points are deferred to
Chapter [Negation][plfa.Negation]. Chapter [Negation]({{ site.baseurl }}/Negation/).
It is straightforward to show that `suc m ≤ n` implies `m < n`, It is straightforward to show that `suc m ≤ n` implies `m < n`,
and conversely. One can then give an alternative derivation of the and conversely. One can then give an alternative derivation of the
@ -599,7 +599,7 @@ Define `m > n` to be the same as `n < m`.
You will need a suitable data declaration, You will need a suitable data declaration,
similar to that used for totality. similar to that used for totality.
(We will show that the three cases are exclusive after we introduce (We will show that the three cases are exclusive after we introduce
[negation][plfa.Negation].) [negation]({{ site.baseurl }}/Negation/).)
``` ```
-- Your code goes here -- Your code goes here
@ -742,7 +742,7 @@ Show that the sum of two odd numbers is even.
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates} #### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
Recall that Recall that
Exercise [Bin][plfa.Naturals#Bin] Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin)
defines a datatype `Bin` of bitstrings representing natural numbers. defines a datatype `Bin` of bitstrings representing natural numbers.
Representations are not unique due to leading zeros. Representations are not unique due to leading zeros.
Hence, eleven may be represented by both of the following: Hence, eleven may be represented by both of the following:
@ -801,7 +801,7 @@ import Data.Nat.Properties using (≤-refl; ≤-trans; ≤-antisym; ≤-total;
``` ```
In the standard library, `≤-total` is formalised in terms of In the standard library, `≤-total` is formalised in terms of
disjunction (which we define in disjunction (which we define in
Chapter [Connectives][plfa.Connectives]), Chapter [Connectives]({{ site.baseurl }}/Connectives/)),
and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here, and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here,
and more arguments are implicit. and more arguments are implicit.

4
src/plfa/Untyped.lagda.md
View file

@ -62,7 +62,7 @@ open import Relation.Nullary.Product using (_×-dec_)
## Untyped is Uni-typed ## Untyped is Uni-typed
Our development will be close to that in Our development will be close to that in
Chapter [DeBruijn][plfa.DeBruijn], Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/),
save that every term will have exactly the same type, written `★` save that every term will have exactly the same type, written `★`
and pronounced "any". and pronounced "any".
This matches a slogan introduced by Dana Scott This matches a slogan introduced by Dana Scott
@ -756,7 +756,7 @@ Confirm that two times two is four.
#### Exercise `encode-more` (stretch) #### Exercise `encode-more` (stretch)
Along the lines above, encode all of the constructs of Along the lines above, encode all of the constructs of
Chapter [More][plfa.More], Chapter [More]({{ site.baseurl }}/More/),
save for primitive numbers, in the untyped lambda calculus. save for primitive numbers, in the untyped lambda calculus.
``` ```