From 56ca94be1be273313a3f45492006bde11c03a8f7 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Thu, 18 Jul 2019 11:15:08 +0100 Subject: [PATCH] Fixes #355 --- src/plfa/Bisimulation.lagda.md | 8 ++++---- src/plfa/Connectives.lagda.md | 6 +++--- src/plfa/DeBruijn.lagda.md | 14 ++++++------- src/plfa/Decidable.lagda.md | 4 ++-- src/plfa/Equality.lagda.md | 2 +- src/plfa/Induction.lagda.md | 10 +++++----- src/plfa/Inference.lagda.md | 36 +++++++++++++++++----------------- src/plfa/Isomorphism.lagda.md | 8 ++++---- src/plfa/Lambda.lagda.md | 12 ++++++------ src/plfa/Lists.lagda.md | 4 ++-- src/plfa/More.lagda.md | 4 ++-- src/plfa/Naturals.lagda.md | 2 +- src/plfa/Negation.lagda.md | 4 ++-- src/plfa/Quantifiers.lagda.md | 14 ++++++------- src/plfa/Relations.lagda.md | 12 ++++++------ src/plfa/Untyped.lagda.md | 4 ++-- 16 files changed, 72 insertions(+), 72 deletions(-) diff --git a/src/plfa/Bisimulation.lagda.md b/src/plfa/Bisimulation.lagda.md index b1cbb273..11ab3ba4 100644 --- a/src/plfa/Bisimulation.lagda.md +++ b/src/plfa/Bisimulation.lagda.md @@ -119,14 +119,14 @@ above is a simulation from source to target. We leave establishing it in the reverse direction as an exercise. Another exercise is to show the alternative formulations of products in -Chapter [More][plfa.More] +Chapter [More]({{ site.baseurl }}/More/) are in bisimulation. ## Imports We import our source language from -Chapter [More][plfa.More]: +Chapter [More]({{ site.baseurl }}/More/): ``` open import plfa.More ``` @@ -164,7 +164,7 @@ data _~_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where ---------------------- → `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. 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. @@ -468,7 +468,7 @@ a bisimulation. #### Exercise `products` 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 variables, and those connected to functions and products. In this case, the simulation is _not_ lock-step. diff --git a/src/plfa/Connectives.lagda.md b/src/plfa/Connectives.lagda.md index 7331baec..64010ff7 100644 --- a/src/plfa/Connectives.lagda.md +++ b/src/plfa/Connectives.lagda.md @@ -234,7 +234,7 @@ corresponds to `⟨ 1 , ⟨ true , aa ⟩ ⟩`, which is a member of the latter. #### 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)`. ``` @@ -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, 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 -Chapter [Lists][plfa.Lists] +Chapter [Lists]({{ site.baseurl }}/Lists/) 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 standard library is less convenient, since it is parameterised with respect to an arbitrary notion of equivalence. diff --git a/src/plfa/DeBruijn.lagda.md b/src/plfa/DeBruijn.lagda.md index ae237ed2..3e947abe 100644 --- a/src/plfa/DeBruijn.lagda.md +++ b/src/plfa/DeBruijn.lagda.md @@ -56,10 +56,10 @@ And here is its corresponding type derivation: ∋z = Z (These are both taken from Chapter -[Lambda][plfa.Lambda] +[Lambda]({{ site.baseurl }}/Lambda/) and you can see the corresponding derivation tree written out in full -[here][plfa.Lambda#derivation].) +[here]({{ site.baseurl }}/Lambda/#derivation).) The two definitions are in close correspondence, where: * `` `_ `` corresponds to `` ⊢` `` @@ -112,7 +112,7 @@ typed terms, which in context `Γ` have type `A`. While these two choices fit well, they are independent. One can use de Bruijn indices in raw terms, or (with more 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 are inherently scoped but not typed. @@ -408,7 +408,7 @@ lookup ∅ _ = ⊥-elim impossible We intend to apply the function only when the natural is shorter than the length of the context, which we indicate by 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 de Bruijn index, looking up its type in the context: @@ -437,9 +437,9 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0)) ### Test examples We repeat the test examples from -Chapter [Lambda][plfa.Lambda]. +Chapter [Lambda]({{ site.baseurl }}/Lambda/). You can find them -[here][plfa.Lambda#derivation] +[here]({{ site.baseurl }}/Lambda/#derivation) for comparison. 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, much in the same way that `[]` did in -[Lists][plfa.Lists]. +[Lists]({{ site.baseurl }}/Lists/). ## Reduction diff --git a/src/plfa/Decidable.lagda.md b/src/plfa/Decidable.lagda.md index c8849be9..185c9a6b 100644 --- a/src/plfa/Decidable.lagda.md +++ b/src/plfa/Decidable.lagda.md @@ -39,7 +39,7 @@ open import plfa.Isomorphism using (_⇔_) ## Evidence vs Computation -Recall that Chapter [Relations][plfa.Relations] +Recall that Chapter [Relations]({{ site.baseurl }}/Relations/) defined comparison as an inductive datatype, which provides _evidence_ that one number is less than or equal to another: @@ -548,7 +548,7 @@ postulate #### Exercise `iff-erasure` (recommended) 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: ``` postulate diff --git a/src/plfa/Equality.lagda.md b/src/plfa/Equality.lagda.md index 5a372529..4d6db1dc 100644 --- a/src/plfa/Equality.lagda.md +++ b/src/plfa/Equality.lagda.md @@ -347,7 +347,7 @@ an order that will make sense to the reader. #### Exercise `≤-Reasoning` (stretch) 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 notation for `≡-Reasoning`. Define `≤-Reasoning` analogously, and use it to write out an alternative proof that addition is monotonic with diff --git a/src/plfa/Induction.lagda.md b/src/plfa/Induction.lagda.md index 6815f776..07f11f3d 100644 --- a/src/plfa/Induction.lagda.md +++ b/src/plfa/Induction.lagda.md @@ -366,7 +366,7 @@ proof of associativity. 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 -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 @@ -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, 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 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 @@ -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, @@ -954,7 +954,7 @@ for all `m`, `n`, and `p`. #### Exercise `Bin-laws` (stretch) {#Bin-laws} Recall that -Exercise [Bin][plfa.Naturals#Bin] +Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin) defines a datatype of bitstrings representing natural numbers ``` data Bin : Set where diff --git a/src/plfa/Inference.lagda.md b/src/plfa/Inference.lagda.md index a9036d90..7e65eb04 100644 --- a/src/plfa/Inference.lagda.md +++ b/src/plfa/Inference.lagda.md @@ -12,9 +12,9 @@ module plfa.Inference where So far in our development, type derivations for the corresponding 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 -in Chapter [DeBruijn][plfa.DeBruijn] +in Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/) the type derivation was inherently part of the term. 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 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 -Chapter [DeBruijn][plfa.DeBruijn]. +Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). ## 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 The typing rules for variables are as in -[Lambda][plfa.Lambda]: +[Lambda]({{ site.baseurl }}/Lambda/): ``` data _∋_⦂_ : Context → Id → Type → Set where @@ -456,25 +456,25 @@ data _⊢_↓_ where → Γ ⊢ (M ↑) ↓ B ``` 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 corresponding type rule. The rules are similar to those in -Chapter [Lambda][plfa.Lambda], +Chapter [Lambda]({{ site.baseurl }}/Lambda/), modified to support synthesised and inherited types. The two new rules are those for `⊢↑` and `⊢↓`. 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 inherited type and confirms they are identical --- it should remind you of 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} 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 @@ -484,7 +484,7 @@ Chapter [Lambda][plfa.Lambda], decorated to support inference. #### Exercise `bidirectional-products` (recommended) {#bidirectional-products} Extend the bidirectional type rules to include products from -Chapter [More][plfa.More]. +Chapter [More]({{ site.baseurl }}/More/). ``` -- Your code goes here @@ -494,7 +494,7 @@ Chapter [More][plfa.More]. #### Exercise `bidirectional-rest` (stretch) 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 @@ -1004,7 +1004,7 @@ _ = refl From the evidence that a decorated term has the correct type it is easy to extract the corresponding inherently typed term. We use the 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 type judgment into the corresponding inherently typed term. @@ -1067,17 +1067,17 @@ _ = refl ``` Thus, we have confirmed that bidirectional type inference converts decorated versions of the lambda terms from -Chapter [Lambda][plfa.Lambda] +Chapter [Lambda]({{ site.baseurl }}/Lambda/) to the inherently typed terms of -Chapter [DeBruijn][plfa.DeBruijn]. +Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). #### Exercise `inference-multiplication` (recommended) 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 -multiplication from Chapter [DeBruijn][plfa.DeBruijn]. +multiplication from Chapter [DeBruijn]({{ site.baseurl }}/DeBruijn/). ``` -- Your code goes here @@ -1086,7 +1086,7 @@ multiplication from Chapter [DeBruijn][plfa.DeBruijn]. #### Exercise `inference-products` (recommended) 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. ``` @@ -1096,7 +1096,7 @@ bidirectional inference to include products. #### Exercise `inference-rest` (stretch) 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 diff --git a/src/plfa/Isomorphism.lagda.md b/src/plfa/Isomorphism.lagda.md index 3c45b53a..dd22ef9c 100644 --- a/src/plfa/Isomorphism.lagda.md +++ b/src/plfa/Isomorphism.lagda.md @@ -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 yield the same result, then they are the same function. It is the 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: ``` @@ -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, 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. ``` _+′_ : ℕ → ℕ → ℕ @@ -456,8 +456,8 @@ Show that equivalence is reflexive, symmetric, and transitive. #### Exercise `Bin-embedding` (stretch) {#Bin-embedding} Recall that Exercises -[Bin][plfa.Naturals#Bin] and -[Bin-laws][plfa.Induction#Bin-laws] +[Bin]({{ site.baseurl }}/Naturals/#Bin) and +[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws) define a datatype of bitstrings representing natural numbers: ``` data Bin : Set where diff --git a/src/plfa/Lambda.lagda.md b/src/plfa/Lambda.lagda.md index 4433216f..76ca8ff6 100644 --- a/src/plfa/Lambda.lagda.md +++ b/src/plfa/Lambda.lagda.md @@ -25,7 +25,7 @@ recursive function definitions. This chapter formalises the simply-typed lambda calculus, giving its syntax, small-step semantics, and typing rules. The next chapter -[Properties][plfa.Properties] +[Properties]({{ site.baseurl }}/Properties/) proves its main properties, including progress and preservation. Following chapters will look at a number 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 approach to formalisation. Using de Bruijn indices and 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 variables, partly because such terms are easier to read and partly because the development is more traditional. @@ -138,7 +138,7 @@ plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒ ``` The recursive definition of addition is similar to our original 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 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 @@ -373,7 +373,7 @@ to treat variables as values, and to treat `ƛ x ⇒ N` as a value only if `N` is a value. Indeed, this is how Agda normalises terms. We consider this approach in -Chapter [Untyped][plfa.Untyped]. +Chapter [Untyped]({{ site.baseurl }}/Untyped/). ## 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 more steps of the underlying relation, along lines similar to that for reasoning about chains of equalities in -Chapter [Equality][plfa.Equality]: +Chapter [Equality]({{ site.baseurl }}/Equality/): ``` infix 2 _—↠_ 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. -Chapter [Inference][plfa.Inference] +Chapter [Inference]({{ site.baseurl }}/Inference/) will show how to use Agda to compute type derivations directly. diff --git a/src/plfa/Lists.lagda.md b/src/plfa/Lists.lagda.md index f45c3186..77c763a5 100644 --- a/src/plfa/Lists.lagda.md +++ b/src/plfa/Lists.lagda.md @@ -178,7 +178,7 @@ and follows by straightforward computation combined with the inductive hypothesis. As usual, the inductive hypothesis is indicated by a recursive 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: (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) 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 ℓ₃} → (B → C) → (A → B) → A → C diff --git a/src/plfa/More.lagda.md b/src/plfa/More.lagda.md index 1877337c..b0254a9b 100644 --- a/src/plfa/More.lagda.md +++ b/src/plfa/More.lagda.md @@ -31,10 +31,10 @@ informal. We show how to formalise the first four constructs and leave the rest as an exercise for the reader. 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, 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. By now, explaining with symbols should be more concise, more precise, diff --git a/src/plfa/Naturals.lagda.md b/src/plfa/Naturals.lagda.md index 22e23e61..9f6b64dd 100644 --- a/src/plfa/Naturals.lagda.md +++ b/src/plfa/Naturals.lagda.md @@ -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 will see how these are used below. We take these as givens for now, 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 operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written diff --git a/src/plfa/Negation.lagda.md b/src/plfa/Negation.lagda.md index f2e1b63c..1d989cba 100644 --- a/src/plfa/Negation.lagda.md +++ b/src/plfa/Negation.lagda.md @@ -189,7 +189,7 @@ again causing the equality to hold trivially. #### Exercise `<-irreflexive` (recommended) 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`. ``` @@ -200,7 +200,7 @@ is irreflexive, that is, `n < n` holds for no `n`. #### Exercise `trichotomy` 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: * `m < n` diff --git a/src/plfa/Quantifiers.lagda.md b/src/plfa/Quantifiers.lagda.md index bdfcc233..78a8bd1c 100644 --- a/src/plfa/Quantifiers.lagda.md +++ b/src/plfa/Quantifiers.lagda.md @@ -90,7 +90,7 @@ postulate (∀ (x : A) → B x × C x) ≃ (∀ (x : A) → B x) × (∀ (x : A) → C x) ``` Compare this with the result (`→-distrib-×`) in -Chapter [Connectives][plfa.Connectives]. +Chapter [Connectives]({{ site.baseurl }}/Connectives/). #### 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 establish the isomorphism is identical to what we wrote when discussing -[implication][plfa.Connectives#implication]. +[implication]({{ site.baseurl }}/Connectives/#implication). #### Exercise `∃-distrib-⊎` (recommended) @@ -263,7 +263,7 @@ Show that `∃[ x ] B x` is isomorphic to `B aa ⊎ B bb ⊎ B cc`. ## An existential example Recall the definitions of `even` and `odd` from -Chapter [Relations][plfa.Relations]: +Chapter [Relations]({{ site.baseurl }}/Relations/): ``` data even : ℕ → Set data odd : ℕ → Set @@ -371,7 +371,7 @@ restated in this way. -- Your code goes here ``` -#### Exercise `∃-+-≤` +#### Exercise `∃-|-≤` Show that `y ≤ z` holds if and only if there exists a `x` such that `x + y ≡ z`. @@ -432,9 +432,9 @@ Does the converse hold? If so, prove; if not, explain why. #### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism} Recall that Exercises -[Bin][plfa.Naturals#Bin], -[Bin-laws][plfa.Induction#Bin-laws], and -[Bin-predicates][plfa.Relations#Bin-predicates] +[Bin]({{ site.baseurl }}/Naturals/#Bin), +[Bin-laws]({{ site.baseurl }}/Induction/#Bin-laws), and +[Bin-predicates]({{ site.baseurl }}/Relations/#Bin-predicates) define a datatype of bitstrings representing natural numbers: ``` data Bin : Set where diff --git a/src/plfa/Relations.lagda.md b/src/plfa/Relations.lagda.md index e9f98a45..ea158e1c 100644 --- a/src/plfa/Relations.lagda.md +++ b/src/plfa/Relations.lagda.md @@ -155,7 +155,7 @@ either `(1 ≤ 2) ≤ 3` or `1 ≤ (2 ≤ 3)`. 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 doing so here, but will return to this point in -Chapter [Decidable][plfa.Decidable]. +Chapter [Decidable]({{ site.baseurl }}/Decidable/). ## Inversion @@ -377,7 +377,7 @@ evidence of `m ≤ n` and `n ≤ m` respectively. (For those familiar with logic, the above definition 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_, 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 requires negation, as does the fact that the three cases in 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`, 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, similar to that used for totality. (We will show that the three cases are exclusive after we introduce -[negation][plfa.Negation].) +[negation]({{ site.baseurl }}/Negation/).) ``` -- Your code goes here @@ -742,7 +742,7 @@ Show that the sum of two odd numbers is even. #### Exercise `Bin-predicates` (stretch) {#Bin-predicates} Recall that -Exercise [Bin][plfa.Naturals#Bin] +Exercise [Bin]({{ site.baseurl }}/Naturals/#Bin) defines a datatype `Bin` of bitstrings representing natural numbers. Representations are not unique due to leading zeros. 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 disjunction (which we define in -Chapter [Connectives][plfa.Connectives]), +Chapter [Connectives]({{ site.baseurl }}/Connectives/)), and `+-monoʳ-≤`, `+-monoˡ-≤`, `+-mono-≤` are proved differently than here, and more arguments are implicit. diff --git a/src/plfa/Untyped.lagda.md b/src/plfa/Untyped.lagda.md index 31a85785..947f1ad9 100644 --- a/src/plfa/Untyped.lagda.md +++ b/src/plfa/Untyped.lagda.md @@ -62,7 +62,7 @@ open import Relation.Nullary.Product using (_×-dec_) ## Untyped is Uni-typed 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 `★` and pronounced "any". This matches a slogan introduced by Dana Scott @@ -756,7 +756,7 @@ Confirm that two times two is four. #### Exercise `encode-more` (stretch) 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. ```