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

merge

Browse source
This commit is contained in:
wadler 2020-08-07 09:05:24 +01:00
commit 91a2dd4bf8
24 changed files with 265 additions and 206 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
.travis.yml
View file

@ -28,26 +28,29 @@ addons:
env:
- SH=bash
before_install:
install:
# Install Stack:
- mkdir -p ~/.local/bin
- export PATH=$HOME/.local/bin:$PATH
- travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'
# Install Pandoc:
- travis_retry curl -L https://github.com/jgm/pandoc/releases/download/2.9.2.1/pandoc-2.9.2.1-1-amd64.deb -o $HOME/pandoc.deb && sudo dpkg -i $HOME/pandoc.deb
# Install agda, agda-stdlib, and agda2html:
- make travis-setup
# Install agda, agda-stdlib, and acknowledgements:
- travis_wait 60 make travis-install-agda
- make travis-install-agda-stdlib
- make travis-install-acknowledgements
- ruby -S bundle install
script:
- agda --version
- acknowledgements --version
- pandoc --version
- acknowledgements -i _config.yml >> _config.yml
- make build # build website
- make build # build website
- make build-history # build previous releases
- make test-offline # test website
- make epub # build EPUB
- make epubcheck # test EPUB
- make test-offline # test website
- make epub # build EPUB
- make epubcheck # test EPUB
before_deploy:
- make clean

3
Gemfile
View file

@ -8,6 +8,9 @@ group :development do
gem 'guard'
gem 'guard-shell'
gem 'html-proofer'
# ffi-1.13.1 is broken on macos
# https://github.com/ffi/ffi/issues/791
gem 'ffi', '~> 1.12.2'
end
group :epub do

19
Makefile
View file

@ -165,7 +165,7 @@ out/epub/plfa.epub: $(AGDA_FILES) $(LUA_FILES) epub/main.css out/epub/acknowledg
out/epub/acknowledgements.md: src/plfa/acknowledgements.md _config.yml
@mkdir -p out/epub/
$(BUNDLE) exec ruby epub/render-liquid-template.rb _config.yml $< $@
$(BUNDLE) exec ruby epub/render-liquid-template.rb _config.yml $< $@
.phony: epub epubcheck
@ -187,14 +187,11 @@ clobber: clean
.phony: clean clobber
# Setup Travis
travis-setup:\
$(HOME)/.local/bin/agda\
$(HOME)/.local/bin/acknowledgements\
$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src\
$(HOME)/.agda/defaults\
$(HOME)/.agda/libraries
travis-install-agda\
travis-install-agda-stdlib\
travis-install-acknowledgements
.phony: travis-setup
@ -215,11 +212,11 @@ $(HOME)/.agda/libraries:
echo "$(PLFA_DIR)/plfa.agda-lib" >> $(HOME)/.agda/libraries
$(HOME)/.local/bin/agda:
travis_retry curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip\
curl -L https://github.com/agda/agda/archive/v$(AGDA_VERSION).zip\
-o $(HOME)/agda-$(AGDA_VERSION).zip
unzip -qq $(HOME)/agda-$(AGDA_VERSION).zip -d $(HOME)
cd $(HOME)/agda-$(AGDA_VERSION);\
stack install --stack-yaml=stack-8.0.2.yaml
stack install --stack-yaml=stack-$(GHC_VERSION).yaml
travis-uninstall-agda:
rm -rf $(HOME)/agda-$(AGDA_VERSION)/
@ -236,7 +233,7 @@ travis-reinstall-agda: travis-uninstall-agda travis-install-agda
travis-install-agda-stdlib: $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src
$(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION)/src:
travis_retry curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip\
curl -L https://github.com/agda/agda-stdlib/archive/v$(AGDA_STDLIB_VERSION).zip\
-o $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip
unzip -qq $(HOME)/agda-stdlib-$(AGDA_STDLIB_VERSION).zip -d $(HOME)
mkdir -p $(HOME)/.agda
@ -256,7 +253,7 @@ travis-reinstall-agda-stdlib: travis-uninstall-agda-stdlib travis-install-agda-s
travis-install-acknowledgements: $(HOME)/.local/bin/acknowledgements
$(HOME)/.local/bin/acknowledgements:
travis_retry curl -L https://github.com/plfa/acknowledgements/archive/master.zip\
curl -L https://github.com/plfa/acknowledgements/archive/master.zip\
-o $(HOME)/acknowledgements-master.zip
unzip -qq $(HOME)/acknowledgements-master.zip -d $(HOME)
cd $(HOME)/acknowledgements-master;\

26
README.md
View file

@ -6,6 +6,7 @@ permalink: /GettingStarted/
<!-- Links -->
[epub]: https://plfa.github.io/out/epub/plfa.epub
[plfa]: http://plfa.inf.ed.ac.uk
[plfa-dev]: https://github.com/plfa/plfa.github.io/archive/dev.zip
[plfa-status]: https://travis-ci.org/plfa/plfa.github.io.svg?branch=dev
@ -14,14 +15,14 @@ permalink: /GettingStarted/
[plfa-latest]: https://github.com/plfa/plfa.github.io/releases/latest
[plfa-master]: https://github.com/plfa/plfa.github.io/archive/master.zip
[agda]: https://github.com/agda/agda/releases/tag/v2.6.0.1
[agda-version]: https://img.shields.io/badge/agda-v2.6.0.1-blue.svg
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html#notation-for-key-combinations
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.0.1/tools/package-system.html#example-using-the-standard-library
[agda]: https://github.com/agda/agda/releases/tag/v2.6.1
[agda-version]: https://img.shields.io/badge/agda-v2.6.1-blue.svg
[agda-docs-emacs-mode]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html
[agda-docs-emacs-notation]: https://agda.readthedocs.io/en/v2.6.1/tools/emacs-mode.html#notation-for-key-combinations
[agda-docs-package-system]: https://agda.readthedocs.io/en/v2.6.1/tools/package-system.html#example-using-the-standard-library
[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.1-blue.svg
[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.1
[agda-stdlib-version]: https://img.shields.io/badge/agda--stdlib-v1.3-blue.svg
[agda-stdlib]: https://github.com/agda/agda-stdlib/releases/tag/v1.3
[haskell-stack]: https://docs.haskellstack.org/en/stable/README/
[haskell-ghc]: https://www.haskell.org/ghc/
@ -44,9 +45,6 @@ permalink: /GettingStarted/
[![Agda][agda-version]][agda]
[![agda-stdlib][agda-stdlib-version]][agda-stdlib]
# Getting Started with PLFA
## Dependencies for users
You can read PLFA [online][plfa] without installing anything.
@ -64,11 +62,11 @@ The easiest way to install any specific version of Agda is using [Stack][haskell
```bash
git clone https://github.com/agda/agda.git
cd agda
git checkout v2.6.0.1
git checkout v2.6.1
```
To install Agda, run Stack from the Agda source directory:
```bash
stack install --stack-yaml stack-8.6.5.yaml
stack install --stack-yaml stack-8.8.3.yaml
```
If you want Stack to use you system installation of GHC, you can pass the `--system-ghc` flag and select the appropriate `stack-*.yaml` file. For instance, if you have GHC 8.2.2 installed, run:
```bash
@ -81,7 +79,7 @@ You can get the required version of the Agda standard library from GitHub, eithe
```bash
git clone https://github.com/agda/agda-stdlib.git
cd agda-stdlib
git checkout v1.1
git checkout v1.3
```
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
```bash
@ -227,7 +225,7 @@ bundle exec jekyll serve
### Building the EPUB
The EPUB version of the book is built using Pandoc. Here's how to build the EPUB:
The [EPUB version][epub] of the book is built using Pandoc. Here's how to build the EPUB:
1. Install a recent version of Pandoc, [available here][pandoc].
We recommend their official installer (on the linked page),

6
courses/tspl/2019/Assignment1.lagda.md
View file

@ -47,7 +47,7 @@ yourself, or your group in the case of group practicals).
```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
@ -142,7 +142,7 @@ Give an example of an operator that has an identity and is
associative but is not commutative.
#### 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
@ -196,7 +196,7 @@ Show
for all naturals `n`. Did your proof require induction?
#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
#### Exercise `∸-|-assoc` (practice) {#monus-plus-assoc}
Show that monus associates with addition, that is,

3
courses/tspl/2019/Assignment2.lagda.md
View file

@ -45,7 +45,7 @@ yourself, or your group in the case of group practicals).
```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; z≤n; s≤s)
open import Data.Nat.Properties using (+-assoc; +-identityʳ; +-suc; +-comm;
≤-refl; ≤-trans; ≤-antisym; ≤-total; +-monoʳ-≤; +-monoˡ-≤; +-mono-≤)
@ -481,4 +481,3 @@ postulate
```
-- Your code goes here
```

3
courses/tspl/2019/Assignment3.lagda.md
View file

@ -42,7 +42,7 @@ yourself, or your group in the case of group practicals).
```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Bool.Base using (Bool; true; false; T; _∧_; _∨_; not)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
open import Data.Nat.Properties using
@ -538,4 +538,3 @@ Provide proofs of the three postulates, `unstuck`, `preserves`, and `wttdgs` abo
```
-- Your code goes here
```

6
courses/tspl/2019/Assignment4.lagda.md
View file

@ -632,8 +632,10 @@ not fixed by the given arguments.
## Evaluation
```
data Gas : Set where
gas : ℕ → Gas
record Gas : Set where
constructor gas
field
amount : ℕ
data Finished {Γ A} (N : Γ ⊢ A) : Set where

6
courses/tspl/2019/Exam.lagda.md
View file

@ -351,8 +351,10 @@ module Problem2 where
### Evaluation
```
data Gas : Set where
gas : ℕ → Gas
record Gas : Set where
constructor gas
field
amount : ℕ
data Finished {Γ A} (N : Γ ⊢ A) : Set where

6
src/plfa/part1/Decidable.lagda.md
View file

@ -573,7 +573,7 @@ from `m` only if `n ≤ m`:
```
minus : (m n : ℕ) (n≤m : n ≤ m) → ℕ
minus m zero _ = m
minus (suc m) (suc n) (s≤s m≤n) = minus m n m≤n
minus (suc m) (suc n) (s≤s n≤m) = minus m n n≤m
```
Unfortunately, it is painful to use, since we have to explicitly provide
@ -595,8 +595,8 @@ fill in an implicit of an *empty* record type, since there aren't any fields
after all. This is why `⊤` is defined as an empty record.
The trick is to have an implicit argument of the type `T ⌊ n ≤? m ⌋`. Let's go
through what this means step-by-step. First, we run the decision procedure, `n
≤? m`. This provides us with evidence whether `n ≤ m` holds or not. We erase the
through what this means step-by-step. First, we run the decision procedure,
`n ≤? m`. This provides us with evidence whether `n ≤ m` holds or not. We erase the
evidence to a boolean. Finally, we apply `T`. Recall that `T` maps booleans into
the world of evidence: `true` becomes the unit type `⊤`, and `false` becomes the
empty type `⊥`. Operationally, an implicit argument of this type works as a

14
src/plfa/part1/Equality.lagda.md
View file

@ -696,23 +696,27 @@ _∘_ : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} {A : Set ℓ₁} {B : Set ℓ₂} {C
(g ∘ f) x = g (f x)
```
Further information on levels can be found in the [Agda Wiki][wiki].
Further information on levels can be found in the [Agda docs][docs].
[wiki]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism
[docs]: https://agda.readthedocs.io/en/v2.6.1/language/universe-levels.html
## Standard library
Definitions similar to those in this chapter can be found in the
standard library:
Definitions similar to those in this chapter can be found in the standard
library. The Agda standard library defines `_≡⟨_⟩_` as `step-≡`, [which reverses
the order of the arguments][step-≡]. The standard library also defines a syntax
macro, which is automatically imported whenever you import `step-≡`, which
recovers the original argument order:
```
-- import Relation.Binary.PropositionalEquality as Eq
-- open Eq using (_≡_; refl; trans; sym; cong; cong-app; subst)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
-- open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
```
Here the imports are shown as comments rather than code to avoid
collisions, as mentioned in the introduction.
[step-≡]: https://github.com/agda/agda-stdlib/blob/master/CHANGELOG/v1.3.md#changes-to-how-equational-reasoning-is-implemented
## Unicode

4
src/plfa/part1/Induction.lagda.md
View file

@ -28,7 +28,7 @@ and some operations upon them. We also import a couple of new operations,
```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_)
```
@ -656,7 +656,7 @@ time we are concerned with judgments asserting associativity:
Now, we apply the rules to all the judgments we know about. The base
case tells us that `(zero + n) + p ≡ zero + (n + p)` for every natural
`n` and `p`. The inductive case tells us that if
`n` and `p`. The inductive case tells us that if
`(m + n) + p ≡ m + (n + p)` (on the day before today) then
`(suc m + n) + p ≡ suc m + (n + p)` (today).
We didn't know any judgments about associativity before today, so that

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

@ -1106,8 +1106,8 @@ with their corresponding proofs.
Definitions similar to those in this chapter can be found in the standard library:
```
import Data.List using (List; _++_; length; reverse; map; foldr; downFrom)
import Data.List.All using (All; []; _∷_)
import Data.List.Any using (Any; here; there)
import Data.List.Relation.Unary.All using (All; []; _∷_)
import Data.List.Relation.Unary.Any using (Any; here; there)
import Data.List.Membership.Propositional using (_∈_)
import Data.List.Properties
using (reverse-++-commute; map-compose; map-++-commute; foldr-++)

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

@ -941,7 +941,7 @@ Such a pragma can only be invoked once, as invoking it twice would
raise confusion as to whether `2` is a value of type `ℕ` or type
`Data.Nat.ℕ`. Similar confusions arise if other pragmas are invoked
twice. For this reason, we will usually avoid pragmas in future chapters.
Information on pragmas can be found in the Agda documentation.
Information on pragmas can be found in the (Agda documentation)[https://agda.readthedocs.io/en/v2.6.1/language/pragmas.html].
## Unicode

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

@ -34,8 +34,8 @@ as implication of false:
¬_ : Set → Set
¬ A = A → ⊥
```
This is a form of _proof by contradiction_: if assuming `A` leads
to the conclusion `⊥` (a contradiction), then we must have `¬ A`.
This is a form of _reductio ad absurdum_: if assuming `A` leads
to the conclusion `⊥` (an absurdity), then we must have `¬ A`.
Evidence that `¬ A` holds is of the form

192
src/plfa/part2/Confluence.lagda.md
View file

@ -401,14 +401,92 @@ sub-par : ∀{Γ A B} {N N′ : Γ , A ⊢ B} {M M′ : Γ ⊢ A}
sub-par pn pm = subst-par (par-subst-zero pm) pn
```
## Parallel reduction satisfies the diamond property
The heart of the confluence proof is made of stone, or rather, of
diamond! We show that parallel reduction satisfies the diamond
property: that if `M ⇛ N` and `M ⇛ N′`, then `N ⇛ L` and `N′ ⇛ L` for
some `L`. The proof is relatively easy; it is parallel reduction's
_raison d'etre_.
some `L`. The typical proof is an induction on `M ⇛ N` and `M ⇛ N′`
so that every possible pair gives rise to a witeness `L` given by
performing enough beta reductions in parallel.
However, a simpler approach is to perform as many beta reductions in
parallel as possible on `M`, say `M ⁺`, and then show that `N` also
parallel reduces to `M ⁺`. This is the idea of Takahashi's _complete
development_. The desired property may be illustrated as
M
/|
/ |
/ |
N 2
\ |
\ |
\|
M⁺
where downward lines are instances of `⇛`, so we call it the _triangle
property_.
```
_⁺ : ∀ {Γ A}
→ Γ ⊢ A → Γ ⊢ A
(` x) ⁺ = ` x
(ƛ M) ⁺ = ƛ (M ⁺)
((ƛ N) · M) ⁺ = N ⁺ [ M ⁺ ]
(L · M) ⁺ = L ⁺ · (M ⁺)
par-triangle : ∀ {Γ A} {M N : Γ ⊢ A}
→ M ⇛ N
-------
→ N ⇛ M ⁺
par-triangle pvar = pvar
par-triangle (pabs p) = pabs (par-triangle p)
par-triangle (pbeta p1 p2) = sub-par (par-triangle p1) (par-triangle p2)
par-triangle (papp {L = ƛ _ } (pabs p1) p2) =
pbeta (par-triangle p1) (par-triangle p2)
par-triangle (papp {L = ` _} p1 p2) = papp (par-triangle p1) (par-triangle p2)
par-triangle (papp {L = _ · _} p1 p2) = papp (par-triangle p1) (par-triangle p2)
```
The proof of the triangle property is an induction on `M ⇛ N`.
* Suppose `x ⇛ x`. Clearly `x ⁺ = x`, so `x ⇛ x`.
* Suppose `ƛ M ⇛ ƛ N`. By the induction hypothesis we have `N ⇛ M ⁺`
and by definition `(λ M) ⁺ = λ (M ⁺)`, so we conclude that `λ N ⇛ λ
(M ⁺)`.
* Suppose `(λ N) · M ⇛ N′ [ M′ ]`. By the induction hypothesis, we have
`N′ ⇛ N ⁺` and `M′ ⇛ M ⁺`. Since substitution respects parallel reduction,
it follows that `N′ [ M′ ] ⇛ N ⁺ [ M ⁺ ]`, but the right hand side
is exactly `((λ N) · M) ⁺`, hence `N′ [ M′ ] ⇛ ((λ N) · M) ⁺`.
* Suppose `(λ L) · M ⇛ (λ L′) · M′`. By the induction hypothesis
we have `L′ ⇛ L ⁺` and `M′ ⇛ M ⁺`; by definition `((λ L) · M) ⁺ = L ⁺ [ M ⁺ ]`.
It follows `(λ L′) · M′ ⇛ L ⁺ [ M ⁺ ]`.
* Suppose `x · M ⇛ x · M′`. By the induction hypothesis we have `M′ ⇛ M ⁺`
and `x ⇛ x ⁺` so that `x · M′ ⇛ x · M ⁺`.
The remaining case is proved in the same way, so we ignore it. (As
there is currently no way in Agda to expand the catch-all pattern in
the definition of `_⁺` for us before checking the right-hand side,
we have to write down the remaining case explicitly.)
The diamond property then follows by halving the diamond into two triangles.
M
/|\
/ | \
/ | \
N 2 N′
\ | /
\ | /
\|/
M⁺
That is, the diamond property is proved by applying the
triangle property on each side with the same confluent term `M ⁺`.
```
par-diamond : ∀{Γ A} {M N N′ : Γ ⊢ A}
@ -416,90 +494,24 @@ par-diamond : ∀{Γ A} {M N N′ : Γ ⊢ A}
→ M ⇛ N′
---------------------------------
→ Σ[ L ∈ Γ ⊢ A ] (N ⇛ L) × (N′ ⇛ L)
par-diamond (pvar{x = x}) pvar = ⟨ ` x , ⟨ pvar , pvar ⟩ ⟩
par-diamond (pabs p1) (pabs p2)
with par-diamond p1 p2
... | ⟨ L′ , ⟨ p3 , p4 ⟩ ⟩ =
⟨ ƛ L′ , ⟨ pabs p3 , pabs p4 ⟩ ⟩
par-diamond{Γ}{A}{L · M}{N}{N′} (papp{Γ}{L}{L₁}{M}{M₁} p1 p3)
(papp{Γ}{L}{L₂}{M}{M₂} p2 p4)
with par-diamond p1 p2
... | ⟨ L₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ (L₃ · M₃) , ⟨ (papp p5 p7) , (papp p6 p8) ⟩ ⟩
par-diamond (papp (pabs p1) p3) (pbeta p2 p4)
with par-diamond p1 p2
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ N₃ [ M₃ ] , ⟨ pbeta p5 p7 , sub-par p6 p8 ⟩ ⟩
par-diamond (pbeta p1 p3) (papp (pabs p2) p4)
with par-diamond p1 p2
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ (N₃ [ M₃ ]) , ⟨ sub-par p5 p7 , pbeta p6 p8 ⟩ ⟩
par-diamond {Γ}{A} (pbeta p1 p3) (pbeta p2 p4)
with par-diamond p1 p2
... | ⟨ N₃ , ⟨ p5 , p6 ⟩ ⟩
with par-diamond p3 p4
... | ⟨ M₃ , ⟨ p7 , p8 ⟩ ⟩ =
⟨ N₃ [ M₃ ] , ⟨ sub-par p5 p7 , sub-par p6 p8 ⟩ ⟩
par-diamond {M = M} p1 p2 = ⟨ M ⁺ , ⟨ par-triangle p1 , par-triangle p2 ⟩ ⟩
```
The proof is by induction on both premises.
* Suppose `x ⇛ x` and `x ⇛ x`.
We choose `L = x` and immediately have `x ⇛ x` and `x ⇛ x`.
* Suppose `ƛ N ⇛ ƛ N₁` and `ƛ N ⇛ ƛ N₂`.
By the induction hypothesis, there exists `L′` such that
`N₁ ⇛ L′` and `N₂ ⇛ L′`. We choose `L = ƛ L′` and
by `pabs` conclude that `ƛ N₁ ⇛ ƛ L′` and `ƛ N₂ ⇛ ƛ L′.
* Suppose that `L · M ⇛ L₁ · M₁` and `L · M ⇛ L₂ · M₂`.
By the induction hypothesis we have
`L₁ ⇛ L₃` and `L₂ ⇛ L₃` for some `L₃`.
Likewise, we have
`M₁ ⇛ M₃` and `M₂ ⇛ M₃` for some `M₃`.
We choose `L = L₃ · M₃` and conclude with two uses of `papp`.
* Suppose that `(ƛ N) · M ⇛ (ƛ N₁) · M₁` and `(ƛ N) · M ⇛ N₂ [ M₂ ]`
By the induction hypothesis we have
`N₁ ⇛ N₃` and `N₂ ⇛ N₃` for some `N₃`.
Likewise, we have
`M₁ ⇛ M₃` and `M₂ ⇛ M₃` for some `M₃`.
We choose `L = N₃ [ M₃ ]`.
We have `(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]` by rule `pbeta`
and conclude that `N₂ [ M₂ ] ⇛ N₃ [ M₃ ]` because
substitution respects parallel reduction.
* Suppose that `(ƛ N) · M ⇛ N₁ [ M₁ ]` and `(ƛ N) · M ⇛ (ƛ N₂) · M₂`.
The proof of this case is the mirror image of the last one.
* Suppose that `(ƛ N) · M ⇛ N₁ [ M₁ ]` and `(ƛ N) · M ⇛ N₂ [ M₂ ]`.
By the induction hypothesis we have
`N₁ ⇛ N₃` and `N₂ ⇛ N₃` for some `N₃`.
Likewise, we have
`M₁ ⇛ M₃` and `M₂ ⇛ M₃` for some `M₃`.
We choose `L = N₃ [ M₃ ]`.
We have both `(ƛ N₁) · M₁ ⇛ N₃ [ M₃ ]`
and `(ƛ N₂) · M₂ ⇛ N₃ [ M₃ ]`
by rule `pbeta`
This step is optional, though, in the presence of triangle property.
#### Exercise (practice)
Draw pictures that represent the proofs of each of the six cases in
the above proof of `par-diamond`. The pictures should consist of nodes
and directed edges, where each node is labeled with a term and each
edge represents parallel reduction.
* Prove the diamond property `par-diamond` directly by induction on `M ⇛ N` and `M ⇛ N′`.
* Draw pictures that represent the proofs of each of the six cases in
the direct proof of `par-diamond`. The pictures should consist of nodes
and directed edges, where each node is labeled with a term and each
edge represents parallel reduction.
## Proof of confluence for parallel reduction
As promised at the beginning, the proof that parallel reduction is
confluent is easy now that we know it satisfies the diamond property.
confluent is easy now that we know it satisfies the triangle property.
We just need to prove the strip lemma, which states that
if `M ⇛ N` and `M ⇛* N′`, then
`N ⇛* L` and `N′ ⇛ L` for some `L`.
@ -519,7 +531,7 @@ where downward lines are instances of `⇛` or `⇛*`, depending on how
they are marked.
The proof of the strip lemma is a straightforward induction on `M ⇛* N′`,
using the diamond property in the induction step.
using the triangle property in the induction step.
```
strip : ∀{Γ A} {M N N′ : Γ ⊢ A}
@ -529,11 +541,8 @@ strip : ∀{Γ A} {M N N′ : Γ ⊢ A}
→ Σ[ L ∈ Γ ⊢ A ] (N ⇛* L) × (N′ ⇛ L)
strip{Γ}{A}{M}{N}{N′} mn (M ∎) = ⟨ N , ⟨ N ∎ , mn ⟩ ⟩
strip{Γ}{A}{M}{N}{N′} mn (M ⇛⟨ mm' ⟩ m'n')
with par-diamond mn mm'
... | ⟨ L , ⟨ nl , m'l ⟩ ⟩
with strip m'l m'n'
... | ⟨ L′ , ⟨ ll' , n'l' ⟩ ⟩ =
⟨ L′ , ⟨ (N ⇛⟨ nl ⟩ ll') , n'l' ⟩ ⟩
with strip (par-triangle mm') m'n'
... | ⟨ L , ⟨ ll' , n'l' ⟩ ⟩ = ⟨ L , ⟨ N ⇛⟨ par-triangle mn ⟩ ll' , n'l' ⟩ ⟩
```
The proof of confluence for parallel reduction is now proved by
@ -605,19 +614,16 @@ Broadly speaking, this proof of confluence, based on parallel
reduction, is due to W. Tait and P. Martin-Lof (see Barendredgt 1984,
Section 3.2). Details of the mechanization come from several sources.
The `subst-par` lemma is the "strong substitutivity" lemma of Shafer,
Tebbi, and Smolka (ITP 2015). The proofs of `par-diamond`, `strip`,
and `par-confluence` are based on Pfenning's 1992 technical report
about the Church-Rosser theorem. In addition, we consulted Nipkow and
Tebbi, and Smolka (ITP 2015). The proofs of `par-triangle`, `strip`,
and `par-confluence` are based on the notion of complete development
by Takahashi (1995) and Pfenning's 1992 technical report about the
Church-Rosser theorem. In addition, we consulted Nipkow and
Berghofer's mechanization in Isabelle, which is based on an earlier
article by Nipkow (JAR 1996). We opted not to use the "complete
developments" approach of Takahashi (1995) because we felt that the
proof was simple enough based solely on parallel reduction. There are
many more mechanizations of the Church-Rosser theorem that we have not
yet had the time to read, including Shankar's (J. ACM 1988) and
Homeier's (TPHOLs 2001).
article by Nipkow (JAR 1996).
## Unicode
This chapter uses the following unicode:
⇛ U+3015 RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)
⇛ U+21DB RIGHTWARDS TRIPLE ARROW (\r== or \Rrightarrow)
⁺ U+207A SUPERSCRIPT PLUS SIGN (\^+)

7
src/plfa/part2/DeBruijn.lagda.md
View file

@ -1043,8 +1043,10 @@ refer to preservation, since it is built-in to the definition of reduction.
As previously, gas is specified by a natural number:
```
data Gas : Set where
gas : ℕ → Gas
record Gas : Set where
constructor gas
field
amount : ℕ
```
When our evaluator returns a term `N`, it will either give evidence that
`N` is a value or indicate that it ran out of gas:
@ -1375,4 +1377,3 @@ This chapter uses the following unicode:
₆ U+2086 SUBSCRIPT SIX (\_6)
₇ U+2087 SUBSCRIPT SEVEN (\_7)
≠ U+2260 NOT EQUAL TO (\=n)

6
src/plfa/part2/More.lagda.md
View file

@ -1089,8 +1089,10 @@ progress (case× L M) with progress L
## Evaluation
```
data Gas : Set where
gas : ℕ → Gas
record Gas : Set where
constructor gas
field
amount : ℕ
data Finished {Γ A} (N : Γ ⊢ A) : Set where

19
src/plfa/part2/Properties.lagda.md
View file

@ -382,7 +382,7 @@ which is well typed in the empty context is also well typed in an arbitrary
context. The _drop_ lemma asserts that a term which is well typed in a context
where the same variable appears twice remains well typed if we drop the shadowed
occurrence. The _swap_ lemma asserts that a term which is well typed in a
context remains well typed if we swap two variables.
context remains well typed if we swap two variables.
(Renaming is similar to the _context invariance_ lemma in _Software
Foundations_, but it does not require the definition of
@ -775,7 +775,7 @@ Where the construct introduces a bound variable we need to compare it
with the substituted variable, applying the drop lemma if they are
equal and the swap lemma if they are distinct.
For Agda it makes a difference whether we write `x ≟ y` or
For Agda it makes a difference whether we write `x ≟ y` or
`y ≟ x`. In an interactive proof, Agda will show which residual `with`
clauses in the definition of `_[_:=_]` need to be simplified, and the
`with` clauses in `subst` need to match these exactly. The guideline is
@ -918,8 +918,10 @@ per unit of gas.
By analogy, we will use the name _gas_ for the parameter which puts a
bound on the number of reduction steps. `Gas` is specified by a natural number:
```
data Gas : Set where
gas : ℕ → Gas
record Gas : Set where
constructor gas
field
amount : ℕ
```
When our evaluator returns a term `N`, it will either give evidence that
`N` is a value or indicate that it ran out of gas:
@ -950,17 +952,16 @@ data Steps (L : Term) : Set where
The evaluator takes gas and evidence that a term is well typed,
and returns the corresponding steps:
```
{-# TERMINATING #-}
eval : ∀ {L A}
→ Gas
→ ∅ ⊢ L ⦂ A
---------
→ Steps L
eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas
eval {L} (gas zero) ⊢L = steps (L ∎) out-of-gas
eval {L} (gas (suc m)) ⊢L with progress ⊢L
... | done VL = steps (L ∎) (done VL)
... | step L—→M with eval (gas m) (preserve ⊢L L—→M)
... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
... | done VL = steps (L ∎) (done VL)
... | step {M} L—→M with eval (gas m) (preserve ⊢L L—→M)
... | steps M—↠N fin = steps (L —→⟨ L—→M ⟩ M—↠N) fin
```
Let `L` be the name of the term we are reducing, and `⊢L` be the
evidence that `L` is well typed. We consider the amount of gas

2
src/plfa/part2/Substitution.lagda.md
View file

@ -48,7 +48,7 @@ system that _decides_ whether any two substitutions are equal.
```
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; cong; cong₂; cong-app)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Function using (_∘_)
open import plfa.part2.Untyped
using (Type; Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;

61
src/plfa/part2/Subtyping.lagda.md
View file

@ -1,5 +1,5 @@
---
title : "Subtyping: records"
title : "Subtyping: Records"
layout : page
prev : /More/
permalink : /Subtyping/
@ -30,7 +30,7 @@ can also have type `B` if `A` is a subtype of `B`.
⊢<: : ∀{Γ M A B}
→ Γ ⊢ M ⦂ A
→ A <: B
→ A <: B
-----------
→ Γ ⊢ M ⦂ B
@ -58,7 +58,7 @@ written `M # l`, and whose dynamic semantics is defined by the
following reduction rule, which says that accessing the field `lⱼ`
returns the value stored at that field.
{l₁=v₁, ..., lⱼ=vⱼ, ..., lᵢ=vᵢ} # lⱼ —→ vⱼ
{l₁=v₁, ..., lⱼ=vⱼ, ..., lᵢ=vᵢ} # lⱼ —→ vⱼ
In this chapter we add records and record types to the simply typed
lambda calculus (STLC) and prove type safety. It is instructive to see
@ -138,14 +138,14 @@ Name = String
A record is traditionally written as follows
{ l₁ = M₁, ..., lᵢ = Mᵢ }
so a natural representation is a list of label-term pairs.
However, we find it more convenient to represent records as a pair of
vectors (Agda's `Vec` type), one vector of fields and one vector of terms:
l₁, ..., lᵢ
M₁, ..., Mᵢ
This representation has the advantage that the traditional subscript
notation `lᵢ` corresponds to indexing into a vector.
@ -244,9 +244,9 @@ If one vector `ns` is a subset of another `ms`, then for any element
lookup-⊆ : ∀{n m : ℕ}{ns : Vec Name n}{ms : Vec Name m}{i : Fin n}
→ ns ⊆ ms
→ Σ[ k ∈ Fin m ] lookup ns i ≡ lookup ms k
lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {zero} ns⊆ms
lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {zero} ns⊆ms
with lookup-∈ (ns⊆ms x (here refl))
... | ⟨ k , ms[k]=x ⟩ =
... | ⟨ k , ms[k]=x ⟩ =
⟨ k , (sym ms[k]=x) ⟩
lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms =
lookup-⊆ {n} {m} {ns} {ms} {i} (λ x z → x∷ns⊆ms x (there z))
@ -258,7 +258,7 @@ lookup-⊆ {suc n} {m} {x ∷ ns} {ms} {suc i} x∷ns⊆ms =
data Type : Set where
_⇒_ : Type → Type → Type
`ℕ : Type
｛_⦂_｝ : {n : ℕ} (ls : Vec Name n) (As : Vec Type n) → .{d : distinct ls} → Type
｛_⦂_｝ : {n : ℕ} (ls : Vec Name n) (As : Vec Type n) → .{d : distinct ls} → Type
```
In addition to function types `A ⇒ B` and natural numbers `ℕ`, we
@ -366,7 +366,7 @@ Here is the proof of reflexivity, by induction on the size of the type.
with ty-size-pos {A}
... | pos rewrite n≤0⇒n≡0 m
with pos
... | ()
... | ()
<:-refl-aux {suc n}{`ℕ}{m} = <:-nat
<:-refl-aux {suc n}{A ⇒ B}{m} =
let A<:A = <:-refl-aux {n}{A}{m+n≤o⇒m≤o _ (≤-pred m) } in
@ -376,7 +376,7 @@ Here is the proof of reflexivity, by induction on the size of the type.
where
G : ls ⦂ As <: ls ⦂ As
G {i}{j} lij rewrite distinct-lookup-inj (distinct-relevant d) lij =
let As[i]≤n = ≤-trans (lookup-vec-ty-size {As = As}{i}) (≤-pred m) in
let As[i]≤n = ≤-trans (lookup-vec-ty-size {As = As}{i}) (≤-pred m) in
<:-refl-aux {n}{lookup As i}{As[i]≤n}
```
The theorem statement uses `n` as an upper bound on the size of the type `A`
@ -394,7 +394,7 @@ and proceeds by induction on `n`.
Regarding the latter, we need to show that for any `i` and `j`,
`lookup ls j ≡ lookup ls i` implies `lookup As j <: lookup As i`.
Because `lookup` is injective on distinct vectors, we have `i ≡ j`.
We then use the induction hypothesis to show that
We then use the induction hypothesis to show that
`lookup As i <: lookup As i`, noting that the size of
`lookup As i` is less-than-or-equal to the size of `As`, which
is one smaller than the size of `｛ ls ⦂ As ｝`.
@ -421,7 +421,7 @@ The following corollary packages up reflexivity for ease of use.
where
As<:Cs : ls ⦂ As <: ns ⦂ Cs
As<:Cs {i}{j} ls[j]=ns[i]
with lookup-⊆ {i = i} ns⊆ms
with lookup-⊆ {i = i} ns⊆ms
... | ⟨ k , ns[i]=ms[k] ⟩ =
let As[j]<:Bs[k] = As<:Bs {k}{j} (trans ls[j]=ns[i] ns[i]=ms[k]) in
let Bs[k]<:Cs[i] = Bs<:Cs {i}{k} (sym ns[i]=ms[k]) in
@ -450,7 +450,7 @@ The proof is by induction on the derivations of `A <: B` and `B <: C`.
if we can prove that `lookup ls j ≡ lookup ms k`.
We already have `lookup ls j ≡ lookup ns i` and we
obtain `lookup ns i ≡ lookup ms k` by use of the lemma `lookup-⊆`,
noting that `ns ⊆ ms`.
noting that `ns ⊆ ms`.
We can obtain the later, that `lookup Bs k <: lookup Cs i`,
from `｛ ms ⦂ Bs ｝ <: ｛ ns ⦂ Cs ｝`.
It suffices to show that `lookup ms k ≡ lookup ns i`,
@ -527,7 +527,7 @@ The typing judgment takes the form `Γ ⊢ M ⦂ A` and relies on an
auxiliary judgment `Γ ⊢* Ms ⦂ As` for typing a vector of terms.
```
data _⊢*_⦂_ : Context → ∀ {n} → Vec Term n → Vec Type n → Set
data _⊢*_⦂_ : Context → ∀ {n} → Vec Term n → Vec Type n → Set
data _⊢_⦂_ : Context → Term → Type → Set where
@ -607,7 +607,7 @@ chapter. Here we discuss the three new rules.
* Rule `⊢<:`: (Subsumption) If a term `M` has type `A`, and `A <: B`,
then term `M` also has type `B`.
## Renaming and Substitution
@ -712,7 +712,7 @@ data Value : Term → Set where
→ Value (`suc V)
V-rcd : ∀{n}{ls : Vec Name n}{Ms : Vec Term n}
→ Value ｛ ls := Ms ｝
→ Value ｛ ls := Ms ｝
```
## Reduction
@ -827,10 +827,10 @@ canonical ⊢zero V-zero = C-zero
canonical (⊢suc ⊢V) (V-suc VV) = C-suc (canonical ⊢V VV)
canonical (⊢case ⊢L ⊢M ⊢N) ()
canonical (⊢μ ⊢M) ()
canonical (⊢rcd ⊢Ms d) VV = C-rcd {dls = d} ⊢Ms d <:-refl
canonical (⊢rcd ⊢Ms d) VV = C-rcd {dls = d} ⊢Ms d <:-refl
canonical (⊢<: ⊢V <:-nat) VV = canonical ⊢V VV
canonical (⊢<: ⊢V (<:-fun {A}{B}{C}{D} C<:A B<:D)) VV
with canonical ⊢V VV
canonical (⊢<: ⊢V (<:-fun {A}{B}{C}{D} C<:A B<:D)) VV
with canonical ⊢V VV
... | C-ƛ {N}{A′}{B′}{A}{B} ⊢N AB′<:AB = C-ƛ ⊢N (<:-trans AB′<:AB (<:-fun C<:A B<:D))
canonical (⊢<: ⊢V (<:-rcd {ks = ks}{ls = ls}{d2 = dls} ls⊆ks ls⦂Ss<:ks⦂Ts)) VV
with canonical ⊢V VV
@ -915,8 +915,8 @@ progress (⊢· ⊢L ⊢M)
... | done VL
with progress ⊢M
... | step M—→M′ = step (ξ-·₂ VL M—→M′)
... | done VM
with canonical ⊢L VL
... | done VM
with canonical ⊢L VL
... | C-ƛ ⊢N _ = step (β-ƛ VM)
progress ⊢zero = done V-zero
progress (⊢suc ⊢M) with progress ⊢M
@ -950,7 +950,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
* Case `⊢rcd`: we immediately characterize the record as a value.
* Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
## Preservation <a name="subtyping-preservation"></a>
@ -1047,9 +1047,9 @@ subst-pres : ∀ {Γ Δ σ N A}
-----------------
→ Δ ⊢ subst σ N ⦂ A
subst-pres σ⦂ (⊢` eq) = σ⦂ eq
subst-pres {σ = σ} σ⦂ (⊢ƛ ⊢N) = ⊢ƛ (subst-pres{σ = exts σ}(exts-pres {σ = σ} σ⦂) ⊢N)
subst-pres {σ = σ} σ⦂ (⊢· ⊢L ⊢M) = ⊢· (subst-pres{σ = σ} σ⦂ ⊢L) (subst-pres{σ = σ} σ⦂ ⊢M)
subst-pres {σ = σ} σ⦂ (⊢μ ⊢M) = ⊢μ (subst-pres{σ = exts σ} (exts-pres{σ = σ} σ⦂) ⊢M)
subst-pres {σ = σ} σ⦂ (⊢ƛ ⊢N) = ⊢ƛ (subst-pres{σ = exts σ}(exts-pres {σ = σ} σ⦂) ⊢N)
subst-pres {σ = σ} σ⦂ (⊢· ⊢L ⊢M) = ⊢· (subst-pres{σ = σ} σ⦂ ⊢L) (subst-pres{σ = σ} σ⦂ ⊢M)
subst-pres {σ = σ} σ⦂ (⊢μ ⊢M) = ⊢μ (subst-pres{σ = exts σ} (exts-pres{σ = σ} σ⦂) ⊢M)
subst-pres σ⦂ (⊢rcd ⊢Ms dls) = ⊢rcd (subst-vec-pres σ⦂ ⊢Ms ) dls
subst-pres {σ = σ} σ⦂ (⊢# {d = d} ⊢M lif liA) =
⊢# {d = d} (subst-pres {σ = σ} σ⦂ ⊢M) lif liA
@ -1097,7 +1097,7 @@ The proof is by induction on the typing derivation.
* Case `⊢-*-∷`: So we have `∅ ⊢ M ⦂ B` and `∅ ⊢* Ms ⦂ As`. We proceed by cases on `i`.
* If it is `0`, then lookup yields term `M` and `A ≡ B`, so we conclude that `∅ ⊢ M ⦂ A`.
* If it is `suc i`, then we conclude by the induction hypothesis.
@ -1144,7 +1144,7 @@ with cases on `M —→ N`.
* Case `⊢#` and `ξ-#`: So `∅ ⊢ M ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`, `lookup As i ≡ A`,
and `M —→ M′`. We apply the induction hypothesis to obtain `∅ ⊢ M′ ⦂ ｛ ls ⦂ As ｝`
and then conclude by rule `⊢#`.
* Case `⊢#` and `β-#`. We have `∅ ⊢ ｛ ks := Ms ｝ ⦂ ｛ ls ⦂ As ｝`, `lookup ls i ≡ l`,
`lookup As i ≡ A`, `lookup ks j ≡ l`, and `｛ ks := Ms ｝ # l —→ lookup Ms j`.
By the canonical forms lemma, we have `∅ ⊢* Ms ⦂ Bs`, `ls ⊆ ks` and `ks ⦂ Bs <: ls ⦂ As`.
@ -1230,7 +1230,7 @@ The non-algorithmic subtyping rules for variants are
∀i∈1..u, ∃j∈1..u, kⱼ = lᵢ and Aⱼ = Bᵢ
----------------------------------------------
〈k₁=A₁, ..., kᵤ=Aᵤ〉 <: 〈l₁=B₁, ..., lᵤ=Bᵤ〉
Come up with an algorithmic subtyping rule for variant types.
#### Exercise `<:-alternative` (stretch)
@ -1260,7 +1260,7 @@ of the form:
If S <: { lᵢ : Tᵢ | i ∈ 1..n }, then S ≡ { kⱼ : Sⱼ | j ∈ 1..m }
and { lᵢ | i ∈ 1..n } ⊆ { kⱼ | j ∈ 1..m }
and Sⱼ <: Tᵢ for every i and j such that lᵢ = kⱼ.
and Sⱼ <: Tᵢ for every i and j such that lᵢ = kⱼ.
## References
@ -1274,6 +1274,5 @@ of the form:
* Barbara H. Liskov and Jeannette M. Wing. A Behavioral Notion of
Subtyping. In ACM Trans. Program. Lang. Syst. Volume 16, 1994.
* Types and Programming Languages. Benjamin C. Pierce. The MIT Press. 2002.
* Types and Programming Languages. Benjamin C. Pierce. The MIT Press. 2002.

8
src/plfa/part2/Untyped.lagda.md
View file

@ -467,7 +467,7 @@ _ =
∎
```
After just two steps the top-level term is an abstraction,
and `ζ` rules drive the rest of the normalisation.
and `ζ` rules drive the rest of the normalisation.
## Progress
@ -547,8 +547,10 @@ As previously, progress immediately yields an evaluator.
Gas is specified by a natural number:
```
data Gas : Set where
gas : ℕ → Gas
record Gas : Set where
constructor gas
field
amount : ℕ
```
When our evaluator returns a term `N`, it will either give evidence that
`N` is normal or indicate that it ran out of gas:

9
src/plfa/part3/Denotational.lagda.md
View file

@ -54,9 +54,6 @@ down a denotational semantics of the lambda calculus.
## Imports
<!-- JGS: for equational reasoning
open import Relation.Binary using (Setoid)
-->
```
open import Agda.Primitive using (lzero; lsuc)
open import Data.Empty using (⊥-elim)
@ -589,7 +586,7 @@ denotation-setoid Γ = record
-->
<!--
The following went inside the module ≃-Reasoning:
open import Relation.Binary.Reasoning.Setoid (denotation-setoid Γ)
renaming (begin_ to start_; _≈⟨_⟩_ to _≃⟨_⟩_; _∎ to _☐) public
-->
@ -854,7 +851,7 @@ Dᶜ n (a[n] ∷ ls) = (D^suc n (a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦
a successor function whose denotation is given by `D^suc`,
and the start of the path (last of the vector).
It returns the `n + 1` vertex in the path.
(D^suc (suc n) (a[n+1] ∷ a[n] ∷ ls)) ↦ (vec-last (a[n] ∷ ls)) ↦ a[n+1]
The exercise is to prove that for any path `ls`, the meaning of the
@ -870,7 +867,7 @@ apply-n zero = # 0
apply-n (suc n) = # 1 · apply-n n
church : (n : ℕ) → ∅ ⊢ ★
church n = ƛ ƛ apply-n n
church n = ƛ ƛ apply-n n
```
Prove the following theorem.

44
travis-build-cache.sh Executable file
View file

@ -0,0 +1,44 @@
#!/bin/bash
# Dependencies:
# - curl <https://curl.haxx.se/>
# - yq <https://github.com/mikefarah/yq>
# Modify .travis.yml:
# - Remove 'script' and 'deploy' phases;
# - Add 'merge_mode';
# - Create JSON request.
#
body=$(cat .travis.yml \
| yq w - script "echo 'Done'"\
| yq d - before_deploy \
| yq d - deploy \
| yq p - config \
| yq w - message "Build cache" \
| yq w - branch dev \
| yq w - merge_mode replace \
| yq p - request -j)
# Send request to Travis.
#
resp=$(curl -s -X POST \
-H "Content-Type: application/json" \
-H "Accept: application/json" \
-H "Travis-API-Version: 3" \
-H "Authorization: token $TRAVIS_TOKEN" \
-d "$body" \
https://api.travis-ci.org/repo/plfa%2Fplfa.github.io/requests)
# Output response.
#
echo "$resp" \
| yq d - request.configs \
| yq d - request.config \
| yq r - --prettyPrint
# Output configuration.
#
echo "$resp" \
| yq r - request.config \
| yq p - config \
| yq r - --prettyPrint