From 4c538c96ddd38c086c5d7c661a7131019a9494e0 Mon Sep 17 00:00:00 2001 From: wadler Date: Sat, 30 Dec 2017 12:54:51 -0200 Subject: [PATCH] inductive definition of addition --- assets/main.scss | 7 +++ src/Naturals.lagda | 133 +++++++++++++++++++++++++++++++++++---------- 2 files changed, 111 insertions(+), 29 deletions(-) diff --git a/assets/main.scss b/assets/main.scss index ffeb15b2..4796f231 100644 --- a/assets/main.scss +++ b/assets/main.scss @@ -8,3 +8,10 @@ div.equation { text-align: center; } + +h1 { font-size: 50px } +h2 { font-size: 40px } +h3 { font-size: 30px } +h4 { font-size: 25px } +h5 { font-size: 20px } +h6 { font-size: 15px } diff --git a/src/Naturals.lagda b/src/Naturals.lagda index 4ae88192..3a4131d0 100644 --- a/src/Naturals.lagda +++ b/src/Naturals.lagda @@ -76,6 +76,8 @@ after zero; and `2` is shorthand for `suc (suc zero)`, which is the same as `suc 1`, the successor of one; and `3` is shorthand for the successor of two; and so on. +**Exercise 1** Write out `7` in longhand. + ### Unpacking the inference rules @@ -123,17 +125,19 @@ Let's look again at the definition of natural numbers: 1. The term `zero` is a natural number. 2. If `n` is a natural number, then the term `suc n` is also a natural number. -Wait a minute! The second line appears to be defining natural numbers +Wait a minute! The second line defines natural numbers in terms of natural numbers. How can that posssibly be allowed? +Isn't this as useless as claiming `Brexit means Brexit`? -In fact, it is possible to assign this a non-circular meaning. -Furthermore, we can do so while only working with *finite* sets and never -referring to the entire *infinite* set of natural numbers. +In fact, it is possible to assign our definition a meaning without +resorting to any unpermitted circularities. Furthermore, we can do so +while only working with *finite* sets and never referring to the +entire *infinite* set of natural numbers. We will think of it as a creation story. To start with, we know about no natural numbers at all. - -- in the beginning there are no natural numbers + -- 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 @@ -247,54 +251,125 @@ multiplication. Here is the definition of addition in Agda: \begin{code} _+_ : ℕ → ℕ → ℕ -zero + n = n -(suc m) + n = suc (m + n) +zero + n = n -- (i) +(suc m) + n = suc (m + n) -- (ii) \end{code} -This definition is *recursive*, in that the last line defines addition -(of `suc m` and `n`) in terms of addition (of `m` and `n`). -As with the inductive definition of the naturals, the apparent -circularity is not a problem. It works because addition of larger -numbers is defined in terms of addition of smaller numbers. For -example, let's add two and three. +Let's unpack this definition. Addition is an infix operator. It is +written with underbars where the arguement go, hence its name is +`_+_`. It's type, `ℕ → ℕ → ℕ`, indicates that it accepts two naturals +and returns a natural. There are two ways to construct a natural, +with `zero` or with `suc`, so there are two lines defining addition, +labeled with comments as `(i)` and `(ii)`. Line `(i)` says that +adding zero to a number (`zero + n`) returns that number (`n`). Line +`(ii)` says that adding the successor of a number to another number +(`(suc m) + n`) returns the successor of adding the two numbers +(`suc (m+n)`). + +This definition is *recursive*, in that the last line defines addition +in terms of addition. As with the inductive definition of the +naturals, the apparent circularity is not a problem. It works because +addition of larger numbers is defined in terms of addition of smaller +numbers. For example, let's add two and three. 2 + 3 = { expand shorthand } (suc (suc zero)) + (suc (suc (suc zero))) - = { by the second equation, with m = suc zero and n = suc (suc (suc zero)) } + = { by (ii) } suc ((suc zero) + (suc (suc (suc zero)))) - = { by the second equation, with m = zero and n = suc (suc (suc zero)) } + = { by (ii) } suc (suc (zero + (suc (suc (suc zero))))) - = { by the first equation, with n = suc (suc (suc zero)) } + = { by (i) } suc (suc (suc (suc (suc zero)))) - = { compress shorthand } + = { compress longhand } 5 -Or, more succintly, +We can write this more compactly by only expanding shorthand as needed. 2 + 3 - = + = { by (ii) } suc (1 + 3) - = + = { by (ii) } suc (suc (0 + 3)) - = + = { by (i) } suc (suc 3) - = + = 5 +The first use of `(ii)` matches by taking `m = 1` and `n = 3`, +The second use of `(ii)` matches by taking `m = 0` and `n = 3`, +and the use of `(i)` matches by taking `n = 3`. + +**Exercise** Compute `3 + 4` by the same technique. -Indeed, the reasoning that justifies inductive and +### The story of creation, revisited + +As with the definition of the naturals by induction, in the definition +of addition by recursion we have defined addition in terms of addition. + +Again, it is possible to assign our definition a meaning without +resorting to unpermitted circularities. We do so by reducing our +definition to equivalent inference rules for judgements about equality. + + n : ℕ + ------------ + zero + n = n + + m + n = p + ------------------- + (suc m) + n = suc p + +Here we assume we have already defined the infinite set of natural +numbers, specifying the meaning of the judgment `n : ℕ`. The first +inference rule asserts that if `n` is a natural number then adding +zero to it gives `n`, and the second rule asserts that if adding `m` +and `n` gives `p`, then adding `suc m` and `n` gives `suc p`. + +Now we can resort to a similar creation story, where now we are +concerned with judgements about addition. + + -- in the beginning, we know nothing about addition + +Now, we apply the rules to all the judgment we know about. +One rule tells us that `zero + n = n` for every natural `n`, +so we add all those equations. The other rule tells us that if +`m + n = p` (on the day before today) then `suc m + n = suc p` +(today). We didn't know any equations about addition before today, +so that rule doesn't give us any equations. + + -- on the first day, we know about addition of 0 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... + +Then we repeat the process, so on the next day we know about all the +equations from the day before, plus any equations added by the rules. One +rule tells us that `zero + n = n` for every natural `n`, but we already knew +that. But now the other rule tells us that for every equation `m + n = p` +that we knew yesterday, we know `suc m + n = suc p` today. + + -- on the second day, we know about addition of 0 and 1 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... + 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 ... + +And we repeat the process again. You've probably got the hang of it by now. + + -- on the third day, we know about addition of 0, 1, and 2 + 0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 ... + 1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 ... + 2 + 0 = 2 2 + 1 = 3 2 + 2 = 4 ... + +The process continues. On the *m*th day we will know all the equations +where the first number is less than *m*. + +As before, there is both a base case (line `(i)` of the definition) +and an inductive case (line `(ii)` of the definition). + +As we can see, the reasoning that justifies inductive and recursive definitions is quite similar, and they might be considered as two sides of the same coin. - - - - - -## Equality on naturals is also an inductive datatype +## Equality is also an inductive datatype ## Proofs over naturals are also recursive functions