For people not familiar with the site, rosettacode was developed on the idea of "let's take a look at implementing the same task in various programming languages". This has a necessary corollary, which was that the task is not allowed to forbid programming languages.

A recent task though, labeled "Proof" has gathered a collection of people that seem bound and determined to circumvent this concept.

The task starts out innocently enough -- it asks that a type be defined representing natural numbers, and that a derivative type be defined which represents the even subset of those natural numbers, and then that we prove that when we add two even numbers we get an even number. Or its original form was something like that. Since this is a fairly trivial problem, I submitted a fairly trivial proof which illustrated some of the same points which were illustrated by the other implementations.

And then, after a long time, someone objected to my proof. And this resulted in a long discussion, where we danced around the real issues. Eventually, the task was changed, explicitly requiring a type based on the peano axioms and asking that associativity be proved.

So here's a problem: the peano axioms require an infinity of distinct values. And, computers can only represent a finite number of distinct values. And, they explicitly required that we implement this as a concrete type. And, finiteness means that there will be some value which the computer can implement where the next larger value cannot be represented.

So I added to the task a statement that the existence of this limit was expected.

And my change was almost immediately reverted, without comment.

So I reverted that reversion and asked that the change be justified.

And it was reverted, again, without justification. And, it's not like anyone feels that computers or computer implementations being finite is in any way controversial.

Instead, the person doing this seems to be confused about the distinction between "a symbol which represents infinity" and "a concrete type which must represent an infinite set of distinct values". But that's just a guess, since the behavior was not justified.

So... I have decided that I am not going to deal with the site until this unjustified behavior ceases.

Still, it's an interesting problem. So I am going to post my work here, where I do not have to worry about people reverting my changes.

I plan on doing this in a few stages: First, a casual discussion of the peano axioms, and a proof about the associativity of addition where addition is built on these axioms. Then I want to go back and think about re-implementing the proofs in an automated fashion, touching on some of the issues that this raises.

* * * * *

First, are the constraints which our peano axioms need to fit, for this task:

- Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}.
- Define an addition on that numbers.
- Define a countably infinite set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers.
- Prove that the addition of
*any*two even numbers is even. - Prove that the addition is
*always*associative.

(The peano axioms could also be built starting from the number 1 -- this changes some details in the proofs.)

So here's a set of peano axioms that would work here, borrowed from the current instance at the math wiki:

- There exists a number zero (0).
- For each , there exists a natural number that is the
*successor*of*n*, denoted by*n*'. - Zero is not the successor of any natural number. (For each , )
- For all natural numbers , if
*n*' =*m*', then*n*=*m*. - Given any predicate
*P*on the natural numbers, if*P*(0) is true and*P*(*k*) implies*P*(*k*') for any , then*P*(*n*)is true for all . (This is also known as the principle of mathematical induction.)

Note that there's a slight difference here -- the math wiki defines natural numbers as not including 0 where the rosettacode task defines natural numbers as including 0. So, for the purpose of the rosettacode task we define natural numbers as the set which includes the math wiki natural numbers and 0.

So... proof.

First off, this set of axioms is a classic mathematical problem. I think most mathematicians get exposed to it sooner or later. So showing that a system is equivalent to the peano axioms is enough to show that there is an operation like addition which is associative. And, multiplication is associative. And... mathematics is generally built on a concept rather like puns, where a set of principles developed for one line of thought can be applied to another line of thought if the underlying axioms can be shown to apply.

But there are limits to mathematical puns. For example, octonions contain the set of natural numbers but in the general case multiplication of octonions is not associative. Multiplication involving only octonions which are natural numbers is still associative, but this kind of issue means we need to proceed with caution.

So, back to the peano axioms -- how can we prove that addition is associative if all we have is the peano axioms?

First, we are going to have to define addition. Here's one implementation, using J (and originally I had used the name 'successor' where I am using the name 'next' but that resulted in some "line too long" problems, so I changed it):

zero=: 0

next=:3 :0

1 + y

)

equal=: -:

predecessor=:3 :0

zero predecessor y

:

if. y equal next x do.

x

else.

(next x) predecessor y

end.

)

addition=:3 :0

:

if. zero equal x do.

y

else.

(predecessor x) addition next y

end.

)

Example use:

predecessor next next next zero

2

(next
next
next zero) addition (next
next
next
next zero)

7

This is a rather tedious approach -- this implementation of addition is going to be extremely slow -- but note also that we can replace the initial three definitions with something entirely different and addition will still work.

For example:

zero=: ''

next=: , ? bind 9

equal=: 1:@,. :: 0:

predecessor next next next zero

2 1

(next
next
next zero) addition (next
next
next
next zero)

2 4 3 2 7 3 3Here, we are constructing sequences of arbitrary digits and our "peano numbers" are the lengths of these sequences. Equality is thus an equality of length rather than a literal equality. (This is generally the case with numbers and equality -- if we are counting sheep we do not mean that the sheep are identical, instead we mean that we do not care about the differences between the things we are counting, except that they somehow represent distinct individuals.)

So... proof... how do we prove that addition is associative? In other words, if A, B and C are valid peano numbers, how do we prove that these two sentences are peano equal?

A addition (B addition C)

(A addition B) addition C

First, we can consider the case where A is zero. If A is zero, then these are equal:

A addition (B addition C)

zero addition (B addition C) NB. substituting for A

(B addition C) NB. if. part of the definition of addition

B addition C NB. definition of parenthesis

Similarly, if A is zero, then these are equal:

(A addition B) addition C

(zero addition B) addition C NB. substituting for A

(B) addition C NB. if. part of the definition of addition

B addition C NB. definition of parenthesis

And we already know that B addition C is peano equal to B addition C

For our next step, we rely on the last clause of the peano axioms. We start by saying that A is a value where our two sentences are equal (

*A addition (B addition C)*and

*(A addition B) addition C*). If this allows us to prove that they are also equal when we replace

*A*by next

*A*then our proof is complete.

So we start this stage with they hypothesis that these are equal:

A addition (B addition C)

(A addition B) addition C

So:

((next A) addition B) addition C

(A addition (next B)) addition C NB. else. part of the definition of addition

(next (A addition B)) addition C NB. else. part of the definition of addition

(A addition B) addition (next C) NB. else. part of the definition of addition

(next ((A addition B) addition C)) NB. by induction **

(next (A addition (B addition C)) NB. hypothesis

(A addition (next (B addition C)) NB. else. part of the definition of addition

((next A) addition (B addition C)) NB. else. part of the definition of addition

These are all equal so the first statement in this chain must be equal to the last statement in this chain.

The transition between these two steps needs induction:

(A addition B) addition (next C) NB. else. part of the definition of addition

(next ((A addition B) addition C)) NB. by induction **

Here's a quick exposition of that induction:

If (A addition B) is zero then it breaks down like this:

(A addition B) addition (next C)

0 addition (next C) NB. by definition

(next C) NB. if part of addition

And, because (A addition B) is zero, we can replace C by (A addition B) addition C and it means the same thing, which leaves us with:

(next ((A addition B) addition C))

If we then assume that we have a case where (A addition B) addition (next C) equals (next ((A addition B) addition C)) we just need to show that it also holds for the next of (A addition B):

(next (A addition B)) addition (next C)

(A addition B) addition (next (next C)) NB. else part of definition of addition

by our induction, we get:

(next ( (A addition B) addition (next C))) NB. else part of definition of addition

Easy, right?

Though some people might prefer I deal with the parenthesis differently, or that I replace phrases with named values. That's a quibble, though, and you can do that kind of manipulation for yourself if you are interested in it.

One note here is that this is a rather tedious sequence of manipulations. But that's not the most important point.

I think the most important point here is the rule of induction. When we can find a case which is equivalent to the inductive rule in the peano axioms, we have found a case which we can characterize by counting. In other words: we can manipulate numbers to deal with those kinds of problems.

Many people I think take the wrong lesson here -- instead of seeing how useful numbers can be, they instead focus on the concept of recursion. But in most practical cases, numbers are good enough. So why make life complicated and tedious? (There are cases -- like ackerman's function -- where you need something more, but I do not think anyone has ever found a practical use for ackerman's function.)

Anyways, from a practical programmer's point of view: numbers are handy things. (And sequences of numbers are handy things -- but that's getting too far afield for this discussion.)

So... how do we convert this proof to a mechanical proof about types?

First, we need a definition for "type" in J. A type is the set of results which can be yielded by a parenthesized J expression.

We also need a way of expressing the above definitions (especially the definition of addition) in a fashion that lets us distinguish the if part and the else part in a mechanical fashion. It may also be convenient to represent a part of an addition. In other words, instead of 1 + 2, we might want to express this in parts like (1 + ]) 2

And, we need a way of tying these things together.

So... back to J... here's some thoughts on how I might construct a type checked program in J:

First, typing itself: If I can make the complete type declaration a part of the name of the implementation of a routine then I can limit access to the routine by type in the same way that I limit access by name.

We also need a mechanical way of expressing things like (A (equal (predecessor (next A)))). I do not need a fully general implementation of these kinds of mechanisms -- I only need enough for this task. (Or, I would not if people would stop changing the task.)

Also, how do we distinguish between different peano systems?

One issue, here, is that for us to be satisfied by a proof, we need to understand it. That's pretty much the point of a proof -- that we are comfortable with our understanding at each step of the way.

And a related issue is that the theories which we can derive from a set of axioms are always going to be restatements of those axioms. If there's something new being introduced, it's going to be a new axiom. An axiom is something that we assume to be true, and the point of all this theory and proof stuff is to minimize our set of axioms -- of assumptions.

And, the way proofs work is: we are introducing a new sequence of things which we might treat as axioms -- constructive statements -- but but which we can later ignore. We see that they are equal to axioms we already have accepted as true.

But that's not really a good description for how computer programs run. Computer programs are a mechanical set of logical processes -- very like a proof -- but instead of understanding their steps, the execution of a program happens outside of our minds. Thus, programs which deal with proofs are typically called "proof assistants". They can perform proof-like steps but it's still up to us to determine the relevance of these steps.

So... we can express the peano proof in a mechanical fashion. But whether that is convincing to the reader is going to depend on the reader and in their understanding of the underlying system.

A related issue is that we can trust the system "too much". The issue I began with here -- the issue having to do with treatment of infinity -- I think illustrates that hazard rather nicely.

But back to representing this problem in J...

Personally, I do not find mechanical manipulations to be a very adequate proof. So I would not be writing an implementation that satisfies myself. Instead, I suppose I would start by emulating an implementation in some other language. Let's take the Agda implementation, for example:

module Arith where -- 1. Natural numbers. -- -- ℕ-formation: ℕ is set. -- -- ℕ-introduction: o ∈ ℕ, -- a ∈ ℕ | (1 + a) ∈ ℕ. -- data ℕ : Set where o : ℕ 1+ : ℕ → ℕ -- 2. Addition. -- -- via ℕ-elimination. -- infixl 6 _+_ _+_ : ℕ → ℕ → ℕ o + n = n 1+ m + n = 1+ (m + n) -- 3. Even natural numbers. -- data 2×ℕ : ℕ → Set where o : 2×ℕ o 2+ : {n : ℕ} → 2×ℕ n → 2×ℕ (1+ (1+ n)) -- 4. Sum of any two even numbers is even. -- -- This function takes any two even numbers and returns their sum as an even number, -- this is a type, i.e. logical proposition, algorithm itself is a proof by unification -- which builds a required term of a given (inhabited) type, and the typechecker -- performs that proof (so that this is compile-time verification). -- even+even≡even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ (m + n) even+even≡even o n = n even+even≡even (2+ m) n = 2+ (even+even≡even m n) -- The identity type for natural numbers. -- infix 4 _≡_ data _≡_ (n : ℕ) : ℕ → Set where refl : n ≡ n cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n cong refl = refl -- 5.1. Direct proof of the associativity of addition. -- +-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-associative o _ _ = refl +-associative (1+ m) n p = cong (+-associative m n p) -- Proof _of_ mathematical induction on the natural numbers. -- -- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. -- ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n ind _ P₀ _ o = P₀ ind P P₀ next (1+ n) = next n (ind P P₀ next n) -- 5.2. Associativity of addition by induction. -- +-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-associative′ m n p = ind P P₀ is m where P : ℕ → Set P i = i + n + p ≡ i + (n + p) P₀ : P o P₀ = refl is : ∀ i → P i → P (1+ i) is i Pi = cong Pi

Here's the web site for Agda: http://wiki.portal.chalmers.se/agda/pmwiki.php

So... reading through this... o is similar to my zero and 1+ is similar to my next . Except

1. Agda begins by declaring their "type".

2. It's not clear to me if this Agda code has any concrete implementation for the type, nor whether it's intended to be able to have any concrete implementation. We can have different sets which are isomorphic to the natural numbers...

Also, this comment bothers me:

"Proof _of_ mathematical induction on the natural numbers"

This was originally an axiom -- something that we take as a given, not something that we should be proving. So either that comment is wrong or the code is doing something different from what I think that I would want to do.

Also... if I understand how Agda works (and I might not), it looks to me as if the treatment of associativity is implemented as a constraint on the original definition. In other words, it looks to me as if it's saying that the earlier definition contains an associative subset, which is something slightly different from saying that the peano axioms guarantee associativity.

But, wait, what about the mathematical "for all" statements in that induction section? Don't those show that the guarantees in part 5 must be valid for all natural numbers? ..... unfortunately, that is the

*problem*. By asserting validity for an infinite series, we are asserting that a finite implementation will eventually fail.

Anyways, it *should* be possible to discuss these kinds of issues rationally, using the english language. And I am upset that I cannot achieve any basic discussion on the subject of "what does it mean to implement a type in a computer program"?

My sense is that there are multiple concepts of type here -- that an Agda type is not anything like a J type. (A J type being the set of values which can result from an expression, an Agda type may never correspond to any results?) If so, this kind of description should be a crucial part of the Rosetta code task.

If it's really the case that the finite character of computer systems has no relevance to the definition of type being used here, this means that the type is not limited to the things which can result from the computer program. Instead, it's a purely symbolic thing -- a glib type -- a type which does not have examples, which cannot be implemented.

That's... disappointing.

## No comments:

## Post a Comment