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

added emoji example to alpha renaming

Browse source
This commit is contained in:
wadler 2017-07-24 11:54:46 +01:00
parent 456696acbd
commit a96c961727
5 changed files with 3574 additions and 3728 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
out/Basics.md
View file

@ -4,8 +4,7 @@ layout : page
permalink : /Basics
---
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="113" class="Keyword"
>open</a
><a name="117"
@ -35,8 +34,7 @@ permalink : /Basics
><a name="179" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
The functional programming style brings programming closer to
simple, everyday mathematics: If a procedure or method has no side
@ -89,8 +87,7 @@ very simple example.
The following declaration tells Agda that we are defining
a new set of data values -- a _type_.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="2469" class="Keyword"
>data</a
><a name="2473"
@ -201,8 +198,7 @@ a new set of data values -- a _type_.
><a name="2612" href="Basics.html#2474" class="Datatype"
>Day</a
>
</pre>
{% endraw %}</pre>
The type is called `day`, and its members are `monday`,
`tuesday`, etc. The second and following lines of the definition
@ -211,8 +207,7 @@ can be read "`monday` is a `day`, `tuesday` is a `day`, etc."
Having defined `day`, we can write functions that operate on
days.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="2894" href="Basics.html#2894" class="Function"
>nextWeekday</a
><a name="2905"
@ -351,8 +346,7 @@ days.
><a name="3135" href="Basics.html#2492" class="InductiveConstructor"
>monday</a
>
</pre>
{% endraw %}</pre>
One thing to note is that the argument and return types of
this function are explicitly declared. Like most functional
@ -375,8 +369,7 @@ above example to Agda, and observe the result.
Second, we can record what we _expect_ the result to be in the
form of an Agda type:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="4097" href="Basics.html#4097" class="Function"
>test-nextWeekday</a
><a name="4113"
@ -408,8 +401,7 @@ form of an Agda type:
><a name="4153" href="Basics.html#2510" class="InductiveConstructor"
>tuesday</a
>
</pre>
{% endraw %}</pre>
This declaration does two things: it makes an assertion (that the second
weekday after `saturday` is `tuesday`), and it gives the assertion a name
@ -418,8 +410,7 @@ that can be used to refer to it later.
Having made the assertion, we must also verify it. We do this by giving
a term of the above type:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="4472" href="Basics.html#4097" class="Function"
>test-nextWeekday</a
><a name="4488"
@ -431,8 +422,7 @@ a term of the above type:
><a name="4491" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>
There is no essential difference between the definition for
`test-nextWeekday` here and the definition for `nextWeekday` above,

198
out/Maps.md
View file

@ -32,8 +32,7 @@ much difference, though, because we've been careful to name our
own definitions and theorems the same as their counterparts in the
standard library, wherever they overlap.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="1490" class="Keyword"
>open</a
><a name="1494"
@ -218,8 +217,7 @@ standard library, wherever they overlap.
><a name="1800" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
Documentation for the standard library can be found at
<https://agda.github.io/agda-stdlib/>.
@ -231,8 +229,7 @@ maps. For this purpose, we again use the type `Id` from the
[Lists](sf/Lists.html) chapter. To make this chapter self contained,
we repeat its definition here.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="2166" class="Keyword"
>data</a
><a name="2170"
@ -273,13 +270,11 @@ we repeat its definition here.
><a name="2197" href="Maps.html#2171" class="Datatype"
>Id</a
>
</pre>
{% endraw %}</pre>
We recall a standard fact of logic.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="2262" href="Maps.html#2262" class="Function"
>contrapositive</a
><a name="2276"
@ -428,14 +423,12 @@ We recall a standard fact of logic.
><a name="2374" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
Using the above, we can decide equality of two identifiers
by deciding equality on the underlying strings.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="2509" href="Maps.html#2509" class="Function Operator"
>_&#8799;_</a
><a name="2512"
@ -713,8 +706,7 @@ by deciding equality on the underlying strings.
><a name="2737" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>
## Total Maps
@ -735,8 +727,7 @@ We build partial maps in two steps. First, we define a type of
_total maps_ that return a default value when we look up a key
that is not present in the map.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="3573" href="Maps.html#3573" class="Function"
>TotalMap</a
><a name="3581"
@ -781,14 +772,12 @@ that is not present in the map.
><a name="3612" href="Maps.html#3603" class="Bound"
>A</a
>
</pre>
{% endraw %}</pre>
Intuitively, a total map over anfi element type `A` _is_ just a
function that can be used to look up ids, yielding `A`s.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="3760" class="Keyword"
>module</a
><a name="3766"
@ -800,15 +789,13 @@ function that can be used to look up ids, yielding `A`s.
><a name="3776" class="Keyword"
>where</a
>
</pre>
{% endraw %}</pre>
The function `always` yields a total map given a
default element; this map always returns the default element when
applied to any id.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="3944" href="Maps.html#3944" class="Function"
>always</a
><a name="3950"
@ -869,15 +856,13 @@ applied to any id.
><a name="3991" href="Maps.html#3985" class="Bound"
>v</a
>
</pre>
{% endraw %}</pre>
More interesting is the update function, which (as before) takes
a map `ρ`, a key `x`, and a value `v` and returns a new map that
takes `x` to `v` and takes every other key to whatever `ρ` does.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="4216" class="Keyword"
>infixl</a
><a name="4222"
@ -1050,8 +1035,7 @@ takes `x` to `v` and takes every other key to whatever `ρ` does.
><a name="4353" href="Maps.html#4300" class="Bound"
>y</a
>
</pre>
{% endraw %}</pre>
This definition is a nice example of higher-order programming.
The update function takes a _function_ `ρ` and yields a new
@ -1060,8 +1044,7 @@ function that behaves like the desired map.
For example, we can build a map taking ids to naturals, where `x`
maps to 42, `y` maps to 69, and every other key maps to 0, as follows:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="4688" class="Keyword"
>module</a
><a name="4694"
@ -1330,8 +1313,7 @@ maps to 42, `y` maps to 69, and every other key maps to 0, as follows:
><a name="4935" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>
This completes the definition of total maps. Note that we don't
need to define a `find` operation because it is just function
@ -1345,8 +1327,7 @@ the lemmas!
#### Exercise: 1 star, optional (apply-always)
The `always` map returns its default element for all keys:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="5411" class="Keyword"
>postulate</a
><a name="5420"
@ -1427,12 +1408,10 @@ The `always` map returns its default element for all keys:
><a name="5478" href="Maps.html#5447" class="Bound"
>v</a
>
</pre>
{% endraw %}</pre>
<div class="hidden">
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="5528" href="Maps.html#5528" class="Function"
>apply-always&#8242;</a
><a name="5541"
@ -1529,8 +1508,7 @@ The `always` map returns its default element for all keys:
><a name="5606" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>
</div>
#### Exercise: 2 stars, optional (update-eq)
@ -1538,8 +1516,7 @@ Next, if we update a map `ρ` at a key `x` with a new value `v`
and then look up `x` in the map resulting from the update, we get
back `v`:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="5830" class="Keyword"
>postulate</a
><a name="5839"
@ -1657,12 +1634,10 @@ back `v`:
><a name="5928" href="Maps.html#5889" class="Bound"
>v</a
>
</pre>
{% endraw %}</pre>
<div class="hidden">
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="5978" href="Maps.html#5978" class="Function"
>update-eq&#8242;</a
><a name="5988"
@ -1870,8 +1845,7 @@ back `v`:
><a name="6151" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
</div>
#### Exercise: 2 stars, optional (update-neq)
@ -1879,8 +1853,7 @@ On the other hand, if we update a map `m` at a key `x` and
then look up a _different_ key `y` in the resulting map, we get
the same result that `m` would have given:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="6400" href="Maps.html#6400" class="Function"
>update-neq</a
><a name="6410"
@ -2132,14 +2105,12 @@ the same result that `m` would have given:
><a name="6594" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>
For the following lemmas, since maps are represented by functions, to
show two maps equal we will need to postulate extensionality.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="6759" class="Keyword"
>postulate</a
><a name="6768"
@ -2250,8 +2221,7 @@ show two maps equal we will need to postulate extensionality.
><a name="6849" href="Maps.html#6805" class="Bound"
>&#961;&#8242;</a
>
</pre>
{% endraw %}</pre>
#### Exercise: 2 stars, optional (update-shadow)
If we update a map `ρ` at a key `x` with a value `v` and then
@ -2260,8 +2230,7 @@ resulting map behaves the same (gives the same result when applied
to any key) as the simpler map obtained by performing just
the second update on `ρ`:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="7205" class="Keyword"
>postulate</a
><a name="7214"
@ -2415,12 +2384,10 @@ the second update on `ρ`:
><a name="7330" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
<div class="hidden">
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="7380" href="Maps.html#7380" class="Function"
>update-shadow&#8242;</a
><a name="7394"
@ -2803,8 +2770,7 @@ the second update on `ρ`:
><a name="7702" href="Maps.html#7676" class="Bound"
>x&#8802;y</a
>
</pre>
{% endraw %}</pre>
</div>
#### Exercise: 2 stars (update-same)
@ -2812,8 +2778,7 @@ Prove the following theorem, which states that if we update a map `ρ` to
assign key `x` the same value as it already has in `ρ`, then the
result is equal to `ρ`:
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="7940" class="Keyword"
>postulate</a
><a name="7949"
@ -2914,12 +2879,10 @@ result is equal to `ρ`:
><a name="8018" href="Maps.html#7975" class="Bound"
>&#961;</a
>
</pre>
{% endraw %}</pre>
<div class="hidden">
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="8068" href="Maps.html#8068" class="Function"
>update-same&#8242;</a
><a name="8080"
@ -3185,8 +3148,7 @@ result is equal to `ρ`:
><a name="8299" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>
</div>
#### Exercise: 3 stars, recommended (update-permute)
@ -3194,8 +3156,7 @@ Prove one final property of the `update` function: If we update a map
`m` at two distinct keys, it doesn't matter in which order we do the
updates.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="8540" class="Keyword"
>postulate</a
><a name="8549"
@ -3409,12 +3370,10 @@ updates.
><a name="8697" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
<div class="hidden">
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="8747" href="Maps.html#8747" class="Function"
>update-permute&#8242;</a
><a name="8762"
@ -4085,13 +4044,11 @@ updates.
><a name="9312" class="Symbol"
>))</a
>
</pre>
{% endraw %}</pre>
And a slightly different version of the same proof.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="9399" href="Maps.html#9399" class="Function"
>update-permute&#8242;&#8242;</a
><a name="9415"
@ -4683,8 +4640,7 @@ And a slightly different version of the same proof.
><a name="9895" class="Symbol"
>))</a
>
</pre>
{% endraw %}</pre>
</div>
## Partial maps
@ -4693,8 +4649,7 @@ Finally, we define _partial maps_ on top of total maps. A partial
map with elements of type `A` is simply a total map with elements
of type `Maybe A` and default element `nothing`.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10132" href="Maps.html#10132" class="Function"
>PartialMap</a
><a name="10142"
@ -4743,11 +4698,9 @@ of type `Maybe A` and default element `nothing`.
><a name="10187" class="Symbol"
>)</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10214" class="Keyword"
>module</a
><a name="10220"
@ -4759,11 +4712,9 @@ of type `Maybe A` and default element `nothing`.
><a name="10232" class="Keyword"
>where</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10265" href="Maps.html#10265" class="Function"
>&#8709;</a
><a name="10266"
@ -4812,11 +4763,9 @@ of type `Maybe A` and default element `nothing`.
><a name="10312" href="https://agda.github.io/agda-stdlib/Data.Maybe.Base.html#403" class="InductiveConstructor"
>nothing</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10347" class="Keyword"
>infixl</a
><a name="10353"
@ -4963,13 +4912,11 @@ of type `Maybe A` and default element `nothing`.
><a name="10473" class="Symbol"
>)</a
>
</pre>
{% endraw %}</pre>
We now lift all of the basic lemmas about total maps to partial maps.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10573" href="Maps.html#10573" class="Function"
>apply-&#8709;</a
><a name="10580"
@ -5066,11 +5013,9 @@ We now lift all of the basic lemmas about total maps to partial maps.
><a name="10667" href="Maps.html#10632" class="Bound"
>x</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10696" href="Maps.html#10696" class="Function"
>update-eq</a
><a name="10705"
@ -5232,11 +5177,9 @@ We now lift all of the basic lemmas about total maps to partial maps.
><a name="10837" class="Symbol"
>)</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="10866" href="Maps.html#10866" class="Function"
>update-neq</a
><a name="10876"
@ -5446,11 +5389,9 @@ We now lift all of the basic lemmas about total maps to partial maps.
><a name="11035" href="Maps.html#10994" class="Bound"
>x&#8802;y</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="11066" href="Maps.html#11066" class="Function"
>update-shadow</a
><a name="11079"
@ -5660,11 +5601,9 @@ We now lift all of the basic lemmas about total maps to partial maps.
><a name="11248" class="Symbol"
>)</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="11277" href="Maps.html#11277" class="Function"
>update-same</a
><a name="11288"
@ -5847,11 +5786,9 @@ We now lift all of the basic lemmas about total maps to partial maps.
><a name="11462" href="Maps.html#11411" class="Bound"
>x</a
>
{% endraw %}</pre>
</pre>
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="11491" href="Maps.html#11491" class="Function"
>update-permute</a
><a name="11505"
@ -6137,13 +6074,11 @@ We now lift all of the basic lemmas about total maps to partial maps.
><a name="11718" href="Maps.html#11664" class="Bound"
>x&#8802;y</a
>
</pre>
{% endraw %}</pre>
We will also need the following basic facts about the `Maybe` type.
<pre class="Agda">
<pre class="Agda">{% raw %}
<a name="11818" href="Maps.html#11818" class="Function"
>just&#8802;nothing</a
><a name="11830"
@ -6391,5 +6326,4 @@ We will also need the following basic facts about the `Maybe` type.
><a name="12028" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
>refl</a
>
</pre>
{% endraw %}</pre>

6596
out/Stlc.md
View file

File diff suppressed because it is too large Load diff

472
out/StlcProp.md
View file

File diff suppressed because it is too large Load diff

10
src/Stlc.lagda
View file

@ -137,7 +137,6 @@ for use later to indicate that a variable appears free in a term, and
eschew `::` because we consider it too ugly.
#### Formal vs informal
In informal presentation of formal semantics, one uses choice of
@ -179,11 +178,12 @@ two = λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x)
In an abstraction `λ[ x ∶ A ] N` we call `x` the _bound_ variable
and `N` the _body_ of the abstraction. One of the most important
aspects of lambda calculus is that names of bound variables are
irrelevant. Thus the four terms
irrelevant. Thus the five terms
* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ``
* `` λ[ g ∶ 𝔹 ⇒ 𝔹 ] λ[ y ∶ 𝔹 ] ` g · (` g · ` y) ``
* `` λ[ fred ∶ 𝔹 ⇒ 𝔹 ] λ[ xander ∶ 𝔹 ] ` fred · (` fred · ` xander) ``
* `` λ[ 👿 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😄 ∶ 𝔹 ] ` 👿 · (` 👿 · ` 😄) ``
* `` λ[ x ∶ 𝔹 ⇒ 𝔹 ] λ[ f ∶ 𝔹 ] ` x · (` x · ` f) ``
are all considered equivalent. This equivalence relation
@ -236,9 +236,9 @@ Thus,
We choose the binding strength for abstractions and conditionals
to be weaker than application. For instance,
* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) `` abbreviates
`` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) `` and not
`` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``.
* `` λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] ` f · (` f · ` x) ``
- abbreviates `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) ``
- and not `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``.
\begin{code}
ex₁ : (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹 ≡ (𝔹 ⇒ 𝔹) ⇒ (𝔹 ⇒ 𝔹)