added more to Naturals
This commit is contained in:
wadler
parent
5d4997bc0c
commit
1bd1f19f52
5 changed files with 1812 additions and 594 deletions
2
index.md
2
index.md
|
|
@ -21,7 +21,7 @@ http://homepages.inf.ed.ac.uk/wadler/
|
|||
- [Basics: Functional Programming in Agda]({{ "/Basics" | relative_url }})
|
||||
-->
|
||||
|
||||
- [Naturals: Natural numbers]({{ "/Naturals" | relative_rul }})
|
||||
- [Naturals: Natural numbers]({{ "/Naturals" | relative_url }})
|
||||
- [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
|
||||
- [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
|
||||
- [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})
|
||||
|
|
|
|||
1972
out/Basics.md
1972
out/Basics.md
File diff suppressed because it is too large
Load diff
90
out/Stlc.md
90
out/Stlc.md
|
|
@ -38,8 +38,7 @@ lists, records, subtyping, and mutable state.
|
|||
|
||||
## Imports
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="1756" class="Keyword"
|
||||
>open</a
|
||||
><a name="1760"
|
||||
|
|
@ -280,8 +279,7 @@ lists, records, subtyping, and mutable state.
|
|||
><a name="2100" class="Symbol"
|
||||
>)</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
## Syntax
|
||||
|
||||
|
|
@ -301,8 +299,7 @@ Here is the syntax of types in BNF.
|
|||
|
||||
And here it is formalised in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="2544" class="Keyword"
|
||||
>infixr</a
|
||||
><a name="2550"
|
||||
|
|
@ -378,8 +375,7 @@ And here it is formalised in Agda.
|
|||
><a name="2614" href="Stlc.html#2564" class="Datatype"
|
||||
>Type</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
Terms have six constructs. Three are for the core lambda calculus:
|
||||
|
||||
|
|
@ -409,8 +405,7 @@ Here is the syntax of terms in BNF.
|
|||
|
||||
And here it is formalised in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="3575" class="Keyword"
|
||||
>infixl</a
|
||||
><a name="3581"
|
||||
|
|
@ -620,8 +615,7 @@ And here it is formalised in Agda.
|
|||
><a name="3801" href="Stlc.html#3637" class="Datatype"
|
||||
>Term</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
#### Special characters
|
||||
|
||||
|
|
@ -669,8 +663,7 @@ Here are a couple of example terms, `not` of type
|
|||
`(𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹` which takes a function and a boolean
|
||||
and applies the function to the boolean twice.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="5677" href="Stlc.html#5677" class="Function"
|
||||
>f</a
|
||||
><a name="5678"
|
||||
|
|
@ -913,8 +906,7 @@ and applies the function to the boolean twice.
|
|||
><a name="5835" class="Symbol"
|
||||
>)</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
|
||||
#### Bound and free variables
|
||||
|
|
@ -991,8 +983,7 @@ to be weaker than application. For instance,
|
|||
- abbreviates `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] (` f · (` f · ` x)))) ``
|
||||
- and not `` (λ[ f ∶ 𝔹 ⇒ 𝔹 ] (λ[ x ∶ 𝔹 ] ` f)) · (` f · ` x) ``.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="8432" href="Stlc.html#8432" class="Function"
|
||||
>ex₁</a
|
||||
><a name="8435"
|
||||
|
|
@ -1358,8 +1349,7 @@ to be weaker than application. For instance,
|
|||
><a name="8656" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
|
||||
>refl</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
#### Quiz
|
||||
|
||||
|
|
@ -1405,8 +1395,7 @@ as values.
|
|||
|
||||
The predicate `Value M` holds if term `M` is a value.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="9717" class="Keyword"
|
||||
>data</a
|
||||
><a name="9721"
|
||||
|
|
@ -1533,8 +1522,7 @@ The predicate `Value M` holds if term `M` is a value.
|
|||
><a name="9845" href="Stlc.html#3749" class="InductiveConstructor"
|
||||
>false</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
We let `V` and `W` range over values.
|
||||
|
||||
|
|
@ -1601,8 +1589,7 @@ name.
|
|||
|
||||
Here is the formal definition in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="12266" href="Stlc.html#12266" class="Function Operator"
|
||||
>_[_:=_]</a
|
||||
><a name="12273"
|
||||
|
|
@ -2245,8 +2232,7 @@ Here is the formal definition in Agda.
|
|||
><a name="12687" class="Symbol"
|
||||
>)</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
The two key cases are variables and abstraction.
|
||||
|
||||
|
|
@ -2272,8 +2258,7 @@ Note that ′ (U+2032: PRIME) is not the same as ' (U+0027: APOSTROPHE).
|
|||
|
||||
Here is confirmation that the examples above are correct.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="13437" href="Stlc.html#13437" class="Function"
|
||||
>ex₁₁</a
|
||||
><a name="13441"
|
||||
|
|
@ -2936,8 +2921,7 @@ Here is confirmation that the examples above are correct.
|
|||
><a name="13885" href="https://agda.github.io/agda-stdlib/Agda.Builtin.Equality.html#140" class="InductiveConstructor"
|
||||
>refl</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
#### Quiz
|
||||
|
||||
|
|
@ -3005,8 +2989,7 @@ and indeed such rules are traditionally called beta rules.
|
|||
|
||||
Here are the above rules formalised in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="15999" class="Keyword"
|
||||
>infix</a
|
||||
><a name="16004"
|
||||
|
|
@ -3572,8 +3555,7 @@ Here are the above rules formalised in Agda.
|
|||
><a name="16430" href="Stlc.html#16396" class="Bound"
|
||||
>N</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
#### Special characters
|
||||
|
||||
|
|
@ -3637,8 +3619,7 @@ are written as follows.
|
|||
|
||||
Here it is formalised in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="18004" class="Keyword"
|
||||
>infix</a
|
||||
><a name="18009"
|
||||
|
|
@ -3824,8 +3805,7 @@ Here it is formalised in Agda.
|
|||
><a name="18149" href="Stlc.html#18122" class="Bound"
|
||||
>N</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
We can read this as follows.
|
||||
|
||||
|
|
@ -3839,8 +3819,7 @@ The names of the two clauses in the definition of reflexive
|
|||
and transitive closure have been chosen to allow us to lay
|
||||
out example reductions in an appealing way.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="18610" href="Stlc.html#18610" class="Function"
|
||||
>reduction₁</a
|
||||
><a name="18620"
|
||||
|
|
@ -4314,8 +4293,7 @@ out example reductions in an appealing way.
|
|||
><a name="19148" href="Stlc.html#18086" class="InductiveConstructor Operator"
|
||||
>∎</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
<!--
|
||||
Much of the above, though not all, can be filled in using C-c C-r and C-c C-s.
|
||||
|
|
@ -4398,8 +4376,7 @@ functions, conditionals use booleans).
|
|||
|
||||
Here are the above rules formalised in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="21694" href="Stlc.html#21694" class="Function"
|
||||
>Context</a
|
||||
><a name="21701"
|
||||
|
|
@ -5079,8 +5056,7 @@ Here are the above rules formalised in Agda.
|
|||
><a name="22177" href="Stlc.html#22095" class="Bound"
|
||||
>A</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
#### Example type derivations
|
||||
|
||||
|
|
@ -5116,8 +5092,7 @@ where `Γ₁ = ∅ , f ∶ 𝔹 ⇒ 𝔹` and `Γ₂ = ∅ , f ∶ 𝔹 ⇒ 𝔹
|
|||
|
||||
Here are the above derivations formalised in Agda.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="23460" href="Stlc.html#23460" class="Function"
|
||||
>typing₁</a
|
||||
><a name="23467"
|
||||
|
|
@ -5319,8 +5294,7 @@ Here are the above derivations formalised in Agda.
|
|||
><a name="23620" class="Symbol"
|
||||
>))))</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
#### Interaction with Agda
|
||||
|
||||
|
|
@ -5367,8 +5341,7 @@ false ``. In other words, no type `A` is the type of this term. It
|
|||
cannot be typed, because doing so requires that the first term in the
|
||||
application is both a boolean and a function.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="25301" href="Stlc.html#25301" class="Function"
|
||||
>notyping₂</a
|
||||
><a name="25310"
|
||||
|
|
@ -5447,15 +5420,13 @@ application is both a boolean and a function.
|
|||
><a name="25364" class="Symbol"
|
||||
>_)</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
As a second example, here is a formal proof that it is not possible to
|
||||
type `` λ[ x ∶ 𝔹 ] λ[ y ∶ 𝔹 ] ` x · ` y `` It cannot be typed, because
|
||||
doing so requires `x` to be both boolean and a function.
|
||||
|
||||
<pre class="Agda">
|
||||
|
||||
<pre class="Agda">{% raw %}
|
||||
<a name="25592" href="Stlc.html#25592" class="Function"
|
||||
>contradiction</a
|
||||
><a name="25605"
|
||||
|
|
@ -5689,8 +5660,7 @@ doing so requires `x` to be both boolean and a function.
|
|||
><a name="25787" class="Symbol"
|
||||
>)</a
|
||||
>
|
||||
|
||||
</pre>
|
||||
{% endraw %}</pre>
|
||||
|
||||
|
||||
#### Quiz
|
||||
|
|
|
|||
268
out/StlcProp.md
268
out/StlcProp.md
File diff suppressed because it is too large
Load diff
|
|
@ -4,8 +4,6 @@ layout : page
|
|||
permalink : /Naturals
|
||||
---
|
||||
|
||||
... introduction ...
|
||||
|
||||
## The naturals are an inductive datatype
|
||||
|
||||
Our first example of an inductive datatype is ℕ, the natural numbers.
|
||||
|
|
@ -15,9 +13,11 @@ data ℕ : Set where
|
|||
suc : ℕ → ℕ
|
||||
\end{code}
|
||||
Here `ℕ` is the name of the *datatype* we are creating,
|
||||
and `zero` and `suc` (short for successor) are the
|
||||
and `zero` and `suc` (short for *successor*) are the
|
||||
*constructors* of the datatype.
|
||||
|
||||
### Inductive datatypes in detail
|
||||
|
||||
Let's unpack this definition. The keyword `data` tells us this is an
|
||||
inductive definition, that is, that we are defining a new datatype
|
||||
with constructors. The phrase
|
||||
|
|
@ -42,6 +42,74 @@ on your keyboard. At the end of each chapter is a list of all the
|
|||
special symbols, including instructions on how to type them in the
|
||||
Emacs text editor.
|
||||
|
||||
### How inductive datatypes work
|
||||
|
||||
The values of type `ℕ` are called natural numbers.
|
||||
The two lines defining constructors tell us the following:
|
||||
|
||||
1. The term `zero` is a natural number.
|
||||
2. If `n` is a natural number, then `suc n` is also a natural number.
|
||||
|
||||
Hence, the possible natural numbers are
|
||||
|
||||
zero
|
||||
suc zero
|
||||
suc (suc zero)
|
||||
suc (suc (suc zero))
|
||||
|
||||
and so on.
|
||||
|
||||
This definition is *recursive* in that it defines the concept of
|
||||
"natural number" in terms of the concept of "natural number". How can
|
||||
this possibly be a sensible thing to do? One way to think of this is
|
||||
as a creation story. To start with, we know about no natural numbers
|
||||
at all.
|
||||
|
||||
-- in the beginning there are no natural numbers
|
||||
|
||||
Now, we apply the rules to all the natural numbers we know about. One
|
||||
rule tells us that `zero` is a natural number, so we add it to the set
|
||||
of known natural numbers. The other rule tells us that if `n` is a
|
||||
natural number (on the day before today) then `suc n` is also a
|
||||
natural number (today). We didn't know about any natural numbers
|
||||
before today, so we don't add any natural numbers of the form `suc n`.
|
||||
|
||||
-- on the first day, there is one natural number
|
||||
zero
|
||||
|
||||
Then we repeat the process, so on the next day we know about all the
|
||||
numbers from the day before, plus any numbers added by the rules. One
|
||||
rule tells us that `zero` is a natural number, but we already knew
|
||||
that. But now the other rule tells us that since `zero` was a natural
|
||||
number yesterday, `suc zero` is a natural number today.
|
||||
|
||||
-- on the second day, there are two natural numbers
|
||||
zero
|
||||
suc zero
|
||||
|
||||
And we repeat the process again. Once more, one rule tells us what
|
||||
we already knew, that `zero` is a natural number. And now the other rule
|
||||
tells us that since `zero` and `suc zero` are both natural numbers, then
|
||||
`suc zero` and `suc (suc zero)` are natural numbers. We already knew about
|
||||
the first of these, but the second is new.
|
||||
|
||||
-- on the third day, there are three natural numbers
|
||||
zero
|
||||
suc zero
|
||||
suc (suc zero)
|
||||
|
||||
The process continues. On the *n*th day there will be *n* distinct
|
||||
natural numbers. Note that in this way, we only talk about finite sets
|
||||
of numbers. Every number will appear on some given finite day. In
|
||||
particular, the number *n* first appears on day *n+1*. And we never
|
||||
actually define the set of numbers in terms of itself. Instead, we define
|
||||
the set of numbers on day *n+1* in terms of the set of numbers on day *n*.
|
||||
|
||||
A process like this one is called *inductive*. We start with nothing, and
|
||||
build up a potentially infinite set by applying rules that convert one
|
||||
finite set into another finite set.
|
||||
|
||||
|
||||
### Pragmas
|
||||
|
||||
\begin{code}
|
||||
|
|
|
|||
Loading…
Reference in a new issue