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

small fixes to SCP paper

Browse source
This commit is contained in:
wadler 2019-07-19 00:16:31 +01:00
commit 6b1e3eb69b
29 changed files with 225 additions and 216 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
.travis.yml
View file

@ -36,6 +36,7 @@ before_install:
- make travis-setup - make travis-setup
script: script:
- curl -L https://raw.githubusercontent.com/MestreLion/git-tools/master/git-restore-mtime | python
- agda --version - agda --version
- acknowledgements --version - acknowledgements --version
- make test-offline # disable to only build cache - make test-offline # disable to only build cache

26
Makefile
View file

@ -14,12 +14,19 @@ endif
# Build PLFA and test hyperlinks # Build PLFA and test hyperlinks
test: build test: build
ruby -S bundle exec htmlproofer _site ruby -S bundle exec htmlproofer '_site'
# Build PLFA and test hyperlinks offline # Build PLFA and test hyperlinks offline
test-offline: build test-offline: build
ruby -S bundle exec htmlproofer _site --disable-external ruby -S bundle exec htmlproofer '_site' --disable-external
# Build PLFA and test hyperlinks for stable
test-stable-offline: $(MARKDOWN)
ruby -S bundle exec jekyll clean
ruby -S bundle exec jekyll build --destination '_site/stable' --baseurl '/stable'
ruby -S bundle exec htmlproofer '_site' --disable-external
statistics: statistics:
@ -39,11 +46,10 @@ $$(out) : out = $(subst courses/,out/,$(subst src/,out/,$(subst .lagda.md,.md,$(
$$(out) : $$(in) | out/ $$(out) : $$(in) | out/
@echo "Processing $$(subst ./,,$$(in))" @echo "Processing $$(subst ./,,$$(in))"
ifeq (,$$(findstring courses/,$$(in))) ifeq (,$$(findstring courses/,$$(in)))
./highlight.sh $$(in) --include-path=src/ ./highlight.sh $$(subst ./,,$$(in)) --include-path=src/
else else
# Fix links to the file itself (out/<filename> to out/<filepath>) # Fix links to the file itself (out/<filename> to out/<filepath>)
./highlight.sh $$(in) --include-path=src/ --include-path=$$(dir $$(in)) ./highlight.sh $$(subst ./,,$$(in)) --include-path=src/ --include-path=$$(subst ./,,$$(dir $$(in)))
@sed -i 's|out/$$(notdir $$(out))|$$(subst ./,,$$(out))|g' $$(out)
endif endif
endef endef
@ -66,26 +72,18 @@ server-stop:
# Build website using jekyll # Build website using jekyll
build: AGDA2HTML_FLAGS += --link-to-agda-stdlib=$(AGDA_STDLIB_URL)
build: $(MARKDOWN) build: $(MARKDOWN)
ruby -S bundle exec jekyll build ruby -S bundle exec jekyll build
# Build website using jekyll offline
build-offline: $(MARKDOWN)
ruby -S bundle exec jekyll build
# Build website using jekyll incrementally # Build website using jekyll incrementally
build-incremental: AGDA2HTML_FLAGS += --link-to-agda-stdlib
build-incremental: $(MARKDOWN) build-incremental: $(MARKDOWN)
ruby -S bundle exec jekyll build --incremental ruby -S bundle exec jekyll build --incremental
# Remove all auxiliary files # Remove all auxiliary files
clean: clean:
rm -f .agda-stdlib.sed rm -f .agda-stdlib.sed .links-*.sed
rm -f .links-*.sed
ifneq ($(strip $(AGDAI)),) ifneq ($(strip $(AGDAI)),)
rm $(AGDAI) rm $(AGDAI)
endif endif

14
README.md
View file

@ -58,7 +58,6 @@ The Makefile offers more than just these options:
make (see make test) make (see make test)
make build (builds lagda->markdown and the website) make build (builds lagda->markdown and the website)
make build-offline (builds lagda->markdown and the website offline)
make build-incremental (builds lagda->markdown and the website incrementally) make build-incremental (builds lagda->markdown and the website incrementally)
make test (checks all links are valid) make test (checks all links are valid)
make test-offline (checks all links are valid offline) make test-offline (checks all links are valid offline)
@ -80,19 +79,6 @@ unzip, and from within the directory run
bundle exec jekyll serve bundle exec jekyll serve
## GNU sed and macOS
The version of sed that ships with macOS is not fully compatible with the GNU sed.
Therefore, you may get errors such as:
```
sed: 1: "out/plfa/Bisimulation.md": invalid command code o
```
You can fix this error by installing a GNU compatible version of sed, e.g. using [Homebrew](https://brew.sh/):
```
brew install gnu-sed --with-default-names
```
## Unicode characters ## Unicode characters
If you're having trouble typing the Unicode characters into Emacs, the end of If you're having trouble typing the Unicode characters into Emacs, the end of

8
_includes/script.html
View file

@ -1,8 +1,14 @@
<!-- Import jQuery --> <!-- Import jQuery -->
<script type="text/javascript" src="{{ "/assets/jquery.js" | prepend: site.baseurl }}"></script> <script type="text/javascript" src="{{ "/assets/jquery.js" | prepend: site.baseurl }}"></script>
<!-- Script which allows for foldable code blocks -->
<script type="text/javascript"> <script type="text/javascript">
// Makes sandwhich menu works
$('.menu-icon').click(function(){
$('.trigger').toggle();
});
// Script which allows for foldable code blocks
$('div.foldable pre').each(function(){ $('div.foldable pre').each(function(){
var autoHeight = $(this).height(); var autoHeight = $(this).height();
var lineHeight = parseFloat($(this).css('line-height')); var lineHeight = parseFloat($(this).css('line-height'));

2
_posts/2019-07-12-changes-to-plfa.md
View file

@ -5,7 +5,7 @@ title : "Changes to PLFA – Migration to Agda 2.6"
Today, we made several major changes to the PLFA infrastructure! Today, we made several major changes to the PLFA infrastructure!
We upgraded to [Agda 2.6.0.1](https://github.com/agda/agda/releases/tag/v2.6.0.1) and [version 1.1 of the standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1). If you want to continue working with the book, you'll have to update your versions locally. Please follow the instructions in [Getting Started](/GettingStarted/) to reinstall Agda and the standard library. We upgraded to [Agda 2.6.0.1](https://github.com/agda/agda/releases/tag/v2.6.0.1) and [version 1.1 of the standard library](https://github.com/agda/agda-stdlib/releases/tag/v1.1). If you want to continue working with the book, you'll have to update your versions locally. Please follow the instructions in [Getting Started]({{ site.baseurl }}/GettingStarted/) to reinstall Agda and the standard library.
We deprecated [agda2html](https://github.com/wenkokke/agda2html). In version 2.6, Agda has added support for the `--html-highlight` flag. Using this command, Agda will highlight only the code in a file, and leave the rest untouched: We deprecated [agda2html](https://github.com/wenkokke/agda2html). In version 2.6, Agda has added support for the `--html-highlight` flag. Using this command, Agda will highlight only the code in a file, and leave the rest untouched:
```bash ```bash

8
_sass/agda.scss
View file

@ -1,8 +1,8 @@
// Define variables for code formatting // Define variables for code formatting
@font-face { @font-face {
font-family: 'Dejavu Sans Mono'; font-family: 'DejaVu Sans Mono';
src: url('fonts/DejavuSansMono.woff2') format('woff2'), src: url('fonts/DejaVuSansMono.woff2') format('woff2'),
url('fonts/DejavuSansMono.woff') format('woff'); url('fonts/DejaVuSansMono.woff') format('woff');
font-weight: normal; font-weight: normal;
font-style: normal; font-style: normal;
@ -16,7 +16,7 @@
} }
@mixin code-font { @mixin code-font {
font-family: 'Dejavu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif; font-family: 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif;
font-size: .85em; font-size: .85em;
} }
@mixin code-container { @mixin code-container {

8
assets/main.scss
View file

@ -4,3 +4,11 @@
@import "katex"; @import "katex";
@import "minima"; @import "minima";
@import "agda"; @import "agda";
$on-medium: 600px !default;
.trigger { display: none; }
@media screen and (min-width: $on-medium) {
.trigger { display: block; }
}

12
courses/padova/2019/padova2019.md
View file

@ -1,7 +1,7 @@
--- ---
title : "Padova: Course notes" title : "Padova: Course notes"
layout : page layout : page
permalink : /Padova/ permalink : /Padova/2019/
--- ---
## Staff ## Staff
@ -20,20 +20,20 @@ permalink : /Padova/
<table> <table>
<tr> <tr>
<td><b>Wed 28 May</b></td> <td><b>Wed 28 May</b></td>
<td><a href="/Naturals/">Naturals</a>, <td><a href="{{ site.baseurl }}/Naturals/">Naturals</a>,
<a href="/Induction/">Induction</a> &amp; <a href="/Relations/">Relations</a></td> <a href="{{ site.baseurl }}/Induction/">Induction</a> &amp; <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Thu 29 May</b></td> <td><b>Thu 29 May</b></td>
<td><a href="/Lambda/">Lambda</a> &amp; <td><a href="{{ site.baseurl }}/Lambda/">Lambda</a> &amp;
<a href="/Properties/">Properties</a></td> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr> </tr>
</table> </table>
## Assignments ## Assignments
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/). For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
* Wed 28 May * Wed 28 May
- Naturals (`_^_`) - Naturals (`_^_`)

48
courses/puc/2019/puc2019.md
View file

@ -21,15 +21,15 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
<table> <table>
<tr> <tr>
<td><b>Fri 29 Mar</b></td> <td><b>Fri 29 Mar</b></td>
<td><a href="/Naturals/">Naturals</a></td> <td><a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 5 Apr</b></td> <td><b>Fri 5 Apr</b></td>
<td><a href="/Induction/">Induction</a> &amp; <a href="/Relations/">Relations</a></td> <td><a href="{{ site.baseurl }}/Induction/">Induction</a> &amp; <a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Thu 11 Apr</b></td> <td><b>Thu 11 Apr</b></td>
<td><a href="/Relations/">Relations</a></td> <td><a href="{{ site.baseurl }}/Relations/">Relations</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 19 Apr</b></td> <td><b>Fri 19 Apr</b></td>
@ -37,16 +37,16 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr> </tr>
<tr> <tr>
<td><b>Fri 26 Apr</b></td> <td><b>Fri 26 Apr</b></td>
<td><a href="/Equality/">Equality</a> &amp; <td><a href="{{ site.baseurl }}/Equality/">Equality</a> &amp;
<a href="/Isomorphism/">Isomorphism</a> &amp; <a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a> &amp;
<a href="/Connectives/">Connectives</a></td> <a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 3 May</b></td> <td><b>Fri 3 May</b></td>
<td><a href="/Negation/">Negation</a> &amp; <td><a href="{{ site.baseurl }}/Negation/">Negation</a> &amp;
<a href="/Quantifiers/">Quantifiers</a> &amp; <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a> &amp;
<a href="/Decidable/">Decidable</a> &amp; <a href="{{ site.baseurl }}/Decidable/">Decidable</a> &amp;
<a href="/Lists/">Lists</a></td> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 10 May</b></td> <td><b>Fri 10 May</b></td>
@ -58,8 +58,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr> </tr>
<tr> <tr>
<td><b>Fri 24 May</b></td> <td><b>Fri 24 May</b></td>
<td><a href="/Lambda/">Lambda</a> &amp; <td><a href="{{ site.baseurl }}/Lambda/">Lambda</a> &amp;
<a href="/Properties/">Properties</a></td> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 31 May</b></td> <td><b>Fri 31 May</b></td>
@ -67,8 +67,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr> </tr>
<tr> <tr>
<td><b>Fri 7 June</b></td> <td><b>Fri 7 June</b></td>
<td><a href="/DeBruijn/">DeBruijn</a> &amp; <td><a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a> &amp;
<a href="/More/">More</a></td> <a href="{{ site.baseurl }}/More/">More</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 14 June</b></td> <td><b>Fri 14 June</b></td>
@ -76,8 +76,8 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
</tr> </tr>
<tr> <tr>
<td><b>Fri 21 June</b></td> <td><b>Fri 21 June</b></td>
<td><a href="/Inference/">Inference</a> &amp; <td><a href="{{ site.baseurl }}/Inference/">Inference</a> &amp;
<a href="/Untyped/">Untyped</a></td> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
</tr> </tr>
<tr> <tr>
<td><b>Fri 28 June</b></td> <td><b>Fri 28 June</b></td>
@ -92,15 +92,15 @@ Lectures and tutorials take place Fridays and some Thursdays in 548L.
## Assignments ## Assignments
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/). For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
* [PUC Assignment 1](/PUC/2019/Assignment1/) due Friday 26 April. * [PUC Assignment 1]({{ site.baseurl }}/PUC/2019/Assignment1/) due Friday 26 April.
* [PUC Assignment 2](/PUC/2019/Assignment2/) due Wednesday 22 May. * [PUC Assignment 2]({{ site.baseurl }}/PUC/2019/Assignment2/) due Wednesday 22 May.
* [PUC Assignment 3](/PUC/2019/Assignment3/) due Wednesday 5 June. * [PUC Assignment 3]({{ site.baseurl }}/PUC/2019/Assignment3/) due Wednesday 5 June.
* [PUC Assignment 4](/PUC/2019/Assignment4/) due Wednesday 19 June. * [PUC Assignment 4]({{ site.baseurl }}/PUC/2019/Assignment4/) due Wednesday 19 June.
* [PUC Assignment 5](/PUC/2019/Assignment5/) due Tuesday 25 June. * [PUC Assignment 5]({{ site.baseurl }}/PUC/2019/Assignment5/) due Tuesday 25 June.
* [PUC Assignment 6](/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June. * [PUC Assignment 6]({{ site.baseurl }}/courses/tspl/2018/Mock1.pdf) due Tuesday 25 June.
Use file [Exam](/PUC/2019/Exam/). Despite the rubric, do **all three questions**. Use file [Exam]({{ site.baseurl }}/PUC/2019/Exam/). Despite the rubric, do **all three questions**.
Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk). Submit assignments by email to [wadler@inf.ed.ac.uk](mailto:wadler@inf.ed.ac.uk).
Attach a single file named `Assignment1.lagda.md` or the like. Include Attach a single file named `Assignment1.lagda.md` or the like. Include

54
courses/tspl/2018/tspl2018.md
View file

@ -27,51 +27,51 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0
</tr> </tr>
<tr> <tr>
<td>1</td> <td>1</td>
<td><b>17 Sep</b> <a href="/Naturals/">Naturals</a></td> <td><b>17 Sep</b> <a href="{{ site.baseurl }}/Naturals/">Naturals</a></td>
<td><b>19 Sep</b> <a href="/Induction/">Induction</a></td> <td><b>19 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
<td><b>21 Sep</b> <a href="/Induction/">Induction</a></td> <td><b>21 Sep</b> <a href="{{ site.baseurl }}/Induction/">Induction</a></td>
</tr> </tr>
<tr> <tr>
<td>2</td> <td>2</td>
<td><b>24 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td> <td><b>24 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a> (Chad)</td>
<td><b>26 Sep</b> <a href="/Relations/">Relations</a> (Chad)</td> <td><b>26 Sep</b> <a href="{{ site.baseurl }}/Relations/">Relations</a> (Chad)</td>
<td><b>28 Sep</b> (no class)</td> <td><b>28 Sep</b> (no class)</td>
</tr> </tr>
<tr> <tr>
<td>3</td> <td>3</td>
<td><b>1 Oct</b> <a href="/Equality/">Equality</a> &amp; <a href="/Isomorphism/">Isomorphism</a></td> <td><b>1 Oct</b> <a href="{{ site.baseurl }}/Equality/">Equality</a> &amp; <a href="{{ site.baseurl }}/Isomorphism/">Isomorphism</a></td>
<td><b>3 Oct</b> <a href="/Connectives/">Connectives</a></td> <td><b>3 Oct</b> <a href="{{ site.baseurl }}/Connectives/">Connectives</a></td>
<td><b>5 Oct</b> <a href="/Negation/">Negation</a></td> <td><b>5 Oct</b> <a href="{{ site.baseurl }}/Negation/">Negation</a></td>
</tr> </tr>
<tr> <tr>
<td>4</td> <td>4</td>
<td><b>8 Oct</b> <a href="/Quantifiers/">Quantifiers</a></td> <td><b>8 Oct</b> <a href="{{ site.baseurl }}/Quantifiers/">Quantifiers</a></td>
<td><b>10 Oct</b> <a href="/Decidable/">Decidable</a></td> <td><b>10 Oct</b> <a href="{{ site.baseurl }}/Decidable/">Decidable</a></td>
<td><b>12 Oct</b> (tutorial only)</td> <td><b>12 Oct</b> (tutorial only)</td>
</tr> </tr>
<tr> <tr>
<td>5</td> <td>5</td>
<td><b>15 Oct</b> <a href="/Lists/">Lists</a></td> <td><b>15 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
<td><b>17 Oct</b> (tutorial only)</td> <td><b>17 Oct</b> (tutorial only)</td>
<td><b>19 Oct</b> <a href="/Lists/">Lists</a></td> <td><b>19 Oct</b> <a href="{{ site.baseurl }}/Lists/">Lists</a></td>
</tr> </tr>
<tr> <tr>
<td>6</td> <td>6</td>
<td><b>22 Oct</b> <a href="/Lambda/">Lambda</a></td> <td><b>22 Oct</b> <a href="{{ site.baseurl }}/Lambda/">Lambda</a></td>
<td><b>24 Oct</b> (no class)</td> <td><b>24 Oct</b> (no class)</td>
<td><b>26 Oct</b> <a href="/Properties/">Properties</a></td> <td><b>26 Oct</b> <a href="{{ site.baseurl }}/Properties/">Properties</a></td>
</tr> </tr>
<tr> <tr>
<td>7</td> <td>7</td>
<td><b>29 Oct</b> <a href="/DeBruijn/">DeBruijn</a></td> <td><b>29 Oct</b> <a href="{{ site.baseurl }}/DeBruijn/">DeBruijn</a></td>
<td><b>31 Oct</b> <a href="/More/">More</a></td> <td><b>31 Oct</b> <a href="{{ site.baseurl }}/More/">More</a></td>
<td><b>2 Nov</b> <a href="/Inference/">Inference</a></td> <td><b>2 Nov</b> <a href="{{ site.baseurl }}/Inference/">Inference</a></td>
</tr> </tr>
<tr> <tr>
<td>8</td> <td>8</td>
<td><b>5 Nov</b> (no class)</td> <td><b>5 Nov</b> (no class)</td>
<td><b>7 Nov</b> (tutorial only)</td> <td><b>7 Nov</b> (tutorial only)</td>
<td><b>9 Nov</b> <a href="/Untyped/">Untyped</a></td> <td><b>9 Nov</b> <a href="{{ site.baseurl }}/Untyped/">Untyped</a></td>
</tr> </tr>
<tr> <tr>
<td>9</td> <td>9</td>
@ -95,15 +95,15 @@ Lectures take place Monday, Wednesday, and Friday in AT 7.02. (Moved from AT 5.0
## Assignments ## Assignments
For instructions on how to set up Agda for PLFA see [Getting Started](/GettingStarted/). For instructions on how to set up Agda for PLFA see [Getting Started]({{ site.baseurl }}/GettingStarted/).
* [Assignment 1](/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3) * [Assignment 1]({{ site.baseurl }}/TSPL/2018/Assignment1/) cw1 due 4pm Thursday 4 October (Week 3)
* [Assignment 2](/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5) * [Assignment 2]({{ site.baseurl }}/TSPL/2018/Assignment2/) cw2 due 4pm Thursday 18 October (Week 5)
* [Assignment 3](/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7) * [Assignment 3]({{ site.baseurl }}/TSPL/2018/Assignment3/) cw3 due 4pm Thursday 1 November (Week 7)
* [Assignment 4](/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9) * [Assignment 4]({{ site.baseurl }}/TSPL/2018/Assignment4/) cw4 due 4pm Thursday 15 November (Week 9)
* [Assignment 5](/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10) * [Assignment 5]({{ site.baseurl }}/courses/tspl/2018/Mock1.pdf) cw5 due 4pm Thursday 22 November (Week 10)
<br /> <br />
Use file [Exam](/TSPL/2018/Exam/). Despite the rubric, do **all three questions**. Use file [Exam]({{ site.baseurl }}/TSPL/2018/Exam/). Despite the rubric, do **all three questions**.
Assignments are submitted by running Assignments are submitted by running
@ -114,5 +114,5 @@ where N is the number of the assignment.
## Mock exam ## Mock exam
Here is the text of the [second mock](/courses/tspl/2018/Mock2.pdf) Here is the text of the [second mock]({{ site.baseurl }}/courses/tspl/2018/Mock2.pdf)
and the exam [instructions](/courses/tspl/2018/Instructions.pdf). and the exam [instructions]({{ site.baseurl }}/courses/tspl/2018/Instructions.pdf).

23
highlight.sh
View file

@ -2,6 +2,10 @@
AGDA_STDLIB_SED=".agda-stdlib.sed" AGDA_STDLIB_SED=".agda-stdlib.sed"
function sedi {
sed --version >/dev/null 2>&1 && sed -i "$@" || sed -i "" "$@"
}
SRC="$1" SRC="$1"
shift shift
@ -45,11 +49,18 @@ if [[ ! -f "$HTML" ]]; then
fi fi
# Add source file to the Jekyll metadata # Add source file to the Jekyll metadata
sed -i "1 s|---|---\nsrc: $SRC|" "$HTML" #sedi "1 s|---|---\nsrc: $SRC|" "$HTML"
ed "$HTML" <<EOF >/dev/null 2>&1
2i
src : "$SRC"
.
w
q
EOF
# Add raw tags around Agda code blocks # Add raw tags around Agda code blocks
sed -i "s|<pre class=\"Agda\">|{% raw %}<pre class=\"Agda\">|" "$HTML" sedi "s|<pre class=\"Agda\">|{% raw %}<pre class=\"Agda\">|" "$HTML"
sed -i "s|</pre>|</pre>{% endraw %}|" "$HTML" sedi "s|</pre>|</pre>{% endraw %}|" "$HTML"
# Fix links to the Agda standard library # Fix links to the Agda standard library
STDLIB_AGDALIB=`grep -m 1 "standard-library" $HOME/.agda/libraries` STDLIB_AGDALIB=`grep -m 1 "standard-library" $HOME/.agda/libraries`
@ -76,26 +87,24 @@ if [ ! -f "$AGDA_STDLIB_SED" ]; then
done done
fi fi
sed -i -f "$AGDA_STDLIB_SED" "$HTML" sedi -f "$AGDA_STDLIB_SED" "$HTML"
# Create a sed script which matches and repairs all local links # Create a sed script which matches and repairs all local links
for INCLUDE_PATH in "$@"; do for INCLUDE_PATH in "$@"; do
if [[ "$INCLUDE_PATH" = --include-path=* ]]; then if [[ "$INCLUDE_PATH" = --include-path=* ]]; then
INCLUDE_PATH="${INCLUDE_PATH:15}" INCLUDE_PATH="${INCLUDE_PATH:15}"
INCLUDE_PATH="${INCLUDE_PATH%/}" INCLUDE_PATH="${INCLUDE_PATH%/}"
INCLUDE_PATH="${INCLUDE_PATH#./}"
LOCAL_LINKS_SED=`echo ".links-${INCLUDE_PATH}.sed" | sed -e "s|/|-|g;"` LOCAL_LINKS_SED=`echo ".links-${INCLUDE_PATH}.sed" | sed -e "s|/|-|g;"`
if [ ! -f "$LOCAL_LINKS_SED" ]; then if [ ! -f "$LOCAL_LINKS_SED" ]; then
find "$INCLUDE_PATH" -name "*.lagda.md" -print0 | while read -d $'\0' AGDA_MODULE_SRC; do find "$INCLUDE_PATH" -name "*.lagda.md" -print0 | while read -d $'\0' AGDA_MODULE_SRC; do
AGDA_MODULE_SRC="${AGDA_MODULE_SRC#./}"
AGDA_MODULE_OUT="$(out_path "$AGDA_MODULE_SRC")" AGDA_MODULE_OUT="$(out_path "$AGDA_MODULE_SRC")"
AGDA_MODULE_HTML="$(basename "$(html_path "$AGDA_MODULE_SRC" "$HTML_DIR")" .md).html" AGDA_MODULE_HTML="$(basename "$(html_path "$AGDA_MODULE_SRC" "$HTML_DIR")" .md).html"
echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|;" >> "$LOCAL_LINKS_SED" echo "s|$AGDA_MODULE_HTML|{% endraw %}{{ site.baseurl }}{% link $AGDA_MODULE_OUT %}{% raw %}|;" >> "$LOCAL_LINKS_SED"
done done
fi fi
sed -i -f "$LOCAL_LINKS_SED" "$HTML" sedi -f "$LOCAL_LINKS_SED" "$HTML"
fi fi
done done

48
index.md
View file

@ -13,48 +13,48 @@ Pull requests are encouraged.
## Front matter ## Front matter
- [Dedication](/Dedication/) - [Dedication]({{ site.baseurl }}/Dedication/)
- [Preface](/Preface/) - [Preface]({{ site.baseurl }}/Preface/)
## Part 1: Logical Foundations ## Part 1: Logical Foundations
- [Naturals](/Naturals/): Natural numbers - [Naturals]({{ site.baseurl }}/Naturals/): Natural numbers
- [Induction](/Induction/): Proof by induction - [Induction]({{ site.baseurl }}/Induction/): Proof by induction
- [Relations](/Relations/): Inductive definition of relations - [Relations]({{ site.baseurl }}/Relations/): Inductive definition of relations
- [Equality](/Equality/): Equality and equational reasoning - [Equality]({{ site.baseurl }}/Equality/): Equality and equational reasoning
- [Isomorphism](/Isomorphism/): Isomorphism and embedding - [Isomorphism]({{ site.baseurl }}/Isomorphism/): Isomorphism and embedding
- [Connectives](/Connectives/): Conjunction, disjunction, and implication - [Connectives]({{ site.baseurl }}/Connectives/): Conjunction, disjunction, and implication
- [Negation](/Negation/): Negation, with intuitionistic and classical logic - [Negation]({{ site.baseurl }}/Negation/): Negation, with intuitionistic and classical logic
- [Quantifiers](/Quantifiers/): Universals and existentials - [Quantifiers]({{ site.baseurl }}/Quantifiers/): Universals and existentials
- [Decidable](/Decidable/): Booleans and decision procedures - [Decidable]({{ site.baseurl }}/Decidable/): Booleans and decision procedures
- [Lists](/Lists/): Lists and higher-order functions - [Lists]({{ site.baseurl }}/Lists/): Lists and higher-order functions
## Part 2: Programming Language Foundations ## Part 2: Programming Language Foundations
- [Lambda](/Lambda/): Introduction to Lambda Calculus - [Lambda]({{ site.baseurl }}/Lambda/): Introduction to Lambda Calculus
- [Properties](/Properties/): Progress and Preservation - [Properties]({{ site.baseurl }}/Properties/): Progress and Preservation
- [DeBruijn](/DeBruijn/): Inherently typed de Bruijn representation - [DeBruijn]({{ site.baseurl }}/DeBruijn/): Inherently typed de Bruijn representation
- [More](/More/): Additional constructs of simply-typed lambda calculus - [More]({{ site.baseurl }}/More/): Additional constructs of simply-typed lambda calculus
- [Bisimulation](/Bisimulation/): Relating reductions systems - [Bisimulation]({{ site.baseurl }}/Bisimulation/): Relating reductions systems
- [Inference](/Inference/): Bidirectional type inference - [Inference]({{ site.baseurl }}/Inference/): Bidirectional type inference
- [Untyped](/Untyped/): Untyped lambda calculus with full normalisation - [Untyped]({{ site.baseurl }}/Untyped/): Untyped lambda calculus with full normalisation
## Backmatter ## Backmatter
- [Acknowledgements](/Acknowledgements/) - [Acknowledgements]({{ site.baseurl }}/Acknowledgements/)
- [Fonts](/Fonts/): Test page for fonts - [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts
- [Statistics](/Statistics/): Line counts for each chapter - [Statistics]({{ site.baseurl }}/Statistics/): Line counts for each chapter
## Related ## Related
- Courses taught from the textbook: - Courses taught from the textbook:
* Philip Wadler, University of Edinburgh, * Philip Wadler, University of Edinburgh,
[2018](/TSPL/2018/) [2018]({{ site.baseurl }}/TSPL/2018/)
* David Darais, University of Vermont, * David Darais, University of Vermont,
[2018](http://david.darais.com/courses/fa2018-cs295A/) [2018](http://david.darais.com/courses/fa2018-cs295A/)
* John Leo, Google Seattle, 2018--2019 * John Leo, Google Seattle, 2018--2019
* Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), * Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio),
[2019](/PUC/2019/) [2019]({{ site.baseurl }}/PUC/2019/)
- A paper describing the book appeared in [SBMF][sbmf] - A paper describing the book appeared in [SBMF][sbmf]
[wen]: https://github.com/wenkokke [wen]: https://github.com/wenkokke

37
papers/scp/PLFA.tex
View file

@ -214,9 +214,9 @@ or the SEL4 operating system \citep{Klein-2009,O'Connor-2016}.
PLFA is aimed at students in the last year of an undergraduate PLFA is aimed at students in the last year of an undergraduate
honours programme or the first year of a master or doctorate degree. honours programme or the first year of a master or doctorate degree.
It aims to teach the fundamentals of operational semantics of It aims to teach the fundamentals of semantics of
programming languages, with simply-typed lambda calculus as the programming languages, with simply-typed and untyped lambda calculi as the
central example. The textbook is written as a literate script in Agda. central examples. The textbook is written as a literate script in Agda.
As with SF, the hope is that using As with SF, the hope is that using
a proof assistant will make the development more concrete a proof assistant will make the development more concrete
and accessible to students, and give them rapid feedback to find and accessible to students, and give them rapid feedback to find
@ -226,7 +226,7 @@ The book is broken into three parts. The first part, Logical Foundations,
develops the needed formalisms. The second part, Programming Language develops the needed formalisms. The second part, Programming Language
Foundations, introduces basic methods of operational semantics. Foundations, introduces basic methods of operational semantics.
The third part, Denotational Semantics, introduces a simple The third part, Denotational Semantics, introduces a simple
model of semantics and its properties. model of the lambda calculus and its properties.
(SF is divided into books, the first two of which have the same names (SF is divided into books, the first two of which have the same names
as the first two parts of PLFA, and cover similar material.) as the first two parts of PLFA, and cover similar material.)
Part~I and Part~II up to Untyped were written by Philip, Part~I and Part~II up to Untyped were written by Philip,
@ -435,7 +435,7 @@ SF has a third volume, written by Andrew Appel, on Verified Functional
Algorithms. We are not sufficiently familiar with that volume to have a view on Algorithms. We are not sufficiently familiar with that volume to have a view on
whether it would be easy or hard to cover that material in Agda. And SF recently whether it would be easy or hard to cover that material in Agda. And SF recently
added a fourth volume on random testing of Coq specifications using QuickChick. added a fourth volume on random testing of Coq specifications using QuickChick.
There is currently no tool equivalent to QuickChick available for Agda. There is currently no tool equivalent to QuickChick for Agda.
There is more material that would be desirable to include in PLFA which was not There is more material that would be desirable to include in PLFA which was not
due to limits of time, including mutable references, logical relations, System F, and due to limits of time, including mutable references, logical relations, System F, and
@ -548,17 +548,17 @@ in inference rules. The proof of proposition \texttt{progress} (the different
case making it a distinct name) is layed out carefully. The neat case making it a distinct name) is layed out carefully. The neat
indented structure emphasises the case analysis, and all right-hand indented structure emphasises the case analysis, and all right-hand
sides line-up in the same column. Our hope as authors is that students sides line-up in the same column. Our hope as authors is that students
will read the formal proof first, and use it as a tabular guide read the formal proof first, and use it as a tabular guide
to the informal explanation that follows. to the informal explanation that follows.
SF puts the informal explanation first, followed by the formal proof. The text SF puts the informal explanation first, followed by the formal proof. The text
hides the formal proof script under an icon; the figure shows what appears when hides the formal proof script under an icon; the figure shows what appears when
the icon is expanded. As teachers, we were aware that students might skip the the icon is expanded. As teachers, we were aware that students might skip the
formal proof on a first reading, and we would have to hope the students would formal proof on a first reading, and we have to hope the students
return to it and step through it with an interactive tool in order to make it return to it and step through it with an interactive tool in order to make it
intelligible. We expect the students skipped over many such proofs. This intelligible. We expect the students skipped over many such proofs. This
particular proof forms the basis for a question of the mock exam and the past particular proof forms the basis for a question of the mock exam and the past
exams, so we expect most students will actually look at this one if not all the exams, so we expect most students will look at this one if not all the
others. others.
\newcommand{\ex}{\texttt{x}} \newcommand{\ex}{\texttt{x}}
@ -596,7 +596,7 @@ provides an interactive development environment of a sort familiar to
most students. Interaction in Agda is supported by an Emacs mode. most students. Interaction in Agda is supported by an Emacs mode.
In Coq, interaction consists of stepping through a proof script, at In Coq, interaction consists of stepping through a proof script, at
each point examining the current goal and the variables currently in each point examining the current goal and the variables in
scope, and executing a new command in the script. Tactics are a whole scope, and executing a new command in the script. Tactics are a whole
sublanguage, which must be learned in addition to the language for sublanguage, which must be learned in addition to the language for
expressing specifications. There are many tactics one can invoke in expressing specifications. There are many tactics one can invoke in
@ -619,8 +619,8 @@ An Agda proof consists of typed code. The interaction is \emph{not}
recorded. Students may recreate it by commenting out bits of code and recorded. Students may recreate it by commenting out bits of code and
introducing a hole in their place. PLFA contains some prose descriptions introducing a hole in their place. PLFA contains some prose descriptions
of interactively building code, but mainly contains code that students of interactively building code, but mainly contains code that students
can read. They may also introduce holes to interact with the code, but can read. They may introduce holes to interact with the code, but
we expect this will be rare. we expect that will be rare.
SF encourages students to interact with all the scripts in the text. SF encourages students to interact with all the scripts in the text.
Trying to understand a Coq proof script without running it Trying to understand a Coq proof script without running it
@ -931,7 +931,7 @@ language feature.
Because the course is taught using a proof assistant, it is important Because the course is taught using a proof assistant, it is important
that students have access to a proof assistant during the exam. that students have access to a proof assistant during the exam.
Students are told in advance that they are expected to get perfect on Students are told in advance that they are expected to get perfect on
the exam, and that they will have to study hard to achieve this level. the exam, and that they will have to study hard to achieve it.
Given that the goal of formal methods is to avoid error, we believe a Given that the goal of formal methods is to avoid error, we believe a
pedagogical purpose is served by telling the students that they are pedagogical purpose is served by telling the students that they are
expected to achieve perfection and making it possible for them to do expected to achieve perfection and making it possible for them to do
@ -1000,12 +1000,13 @@ these links, rerouting links to the standard library to the online version, and
correcting links to local modules. correcting links to local modules.
(Before the release of Agda 2.6, Agda did not support highlighting embedded (Before the release of Agda 2.6, Agda did not support highlighting embedded
literate code using HTML. To address this, we wrote \texttt{agda2html}, a tool literate code in HTML. We maintained \texttt{agda2html}, a tool which rewrites
which rewrote the output of Agda's HTML highlighter to accomplish this. This the output of Agda's HTML highlighter to highlight embedded code. The tool had
tool had much more functionality, including the fixing of links as outlined much more functionality, including the fixing of links as outlined above, the
above, the stripping of implicit arguments to achieve a Haskell-like look, and stripping of implicit arguments to achieve a Haskell-like look, and the support
the support for new Markdown constructs for linking to Agda names. However, for new Markdown constructs for linking to Agda names. However, Agda 2.6 has
Agda 2.6 has incorporated almost all of this functionality.) incorporated almost all of this functionality, and \texttt{agda2html} is now
deprecated.)
The book is built, tested, and published after each commit, using Travis CI, a The book is built, tested, and published after each commit, using Travis CI, a
web service for continuous integration. This means that the book is constantly web service for continuous integration. This means that the book is constantly

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.

22
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.
@ -255,7 +255,7 @@ _ : Context
_ = ∅ , `ℕ ⇒ `ℕ , `ℕ _ = ∅ , `ℕ ⇒ `ℕ , `ℕ
``` ```
is a context with two variables in scope, where the outer is a context with two variables in scope, where the outer
bound one has type `` `ℕ → `ℕ ``, and the inner bound one has bound one has type `` `ℕ ⇒ `ℕ ``, and the inner bound one has
type `` `ℕ ``. type `` `ℕ ``.
### Variables and the lookup judgment ### Variables and the lookup judgment
@ -320,17 +320,17 @@ with all terms and variable names dropped:
``` ```
data _⊢_ : Context → Type → Set where data _⊢_ : Context → Type → Set where
`_ : ∀ {Γ} {A} `_ : ∀ {Γ A}
→ Γ ∋ A → Γ ∋ A
------ ------
→ Γ ⊢ A → Γ ⊢ A
ƛ_ : ∀ {Γ} {A B} ƛ_ : ∀ {Γ A B}
→ Γ , A ⊢ B → Γ , A ⊢ B
---------- ----------
→ Γ ⊢ A ⇒ B → Γ ⊢ A ⇒ B
_·_ : ∀ {Γ} {A B} _·_ : ∀ {Γ A B}
→ Γ ⊢ A ⇒ B → Γ ⊢ A ⇒ B
→ Γ ⊢ A → Γ ⊢ A
---------- ----------
@ -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.
``` ```