Paul,
Sometimes it helps to go exhaustively through every detail to be sure
there is no magic going on. Proceed only if you want exhaustive detail...
If it seems that people are skipping some steps in their argument, it is
because they are! They already understand it so well that they forgot to
add them. Here is what I believe is an excruciatingly complete proof, to
assure you that no handwaving is going on.
The values of Nat are defined inductively on their structure, using its
initial algebra. Take the data type definition
data Nat = Zero | Succ Nat
There is actually an implied undefined as well, so this is really
Nat = undefined | Zero | Succ Nat
Just as 3 = const 3 x for any x, we can convert from pointed to
pointfree notation (i.e. go from a recursive definition to a
least-defined fixed point definition):
f = const undefined | const Zero | Succ
Nat = LFP (m -> infinity) ( f^m undefined )
[ For the notationally picky, I am using | instead of + in the functor
for clarity, which causes no ambiguity.]
Because we are overachievers, we will prove our theorem not just for the
least-defined fixed point of f, but change the limit to a union and
prove it for (f^m undefined) for every m, which includes the fixed point.
Why the extra work? Because now we have an inductive argument. The base
case is undefined, and each step is another application of f.
DEFINITION:
add Zero n = n -- Line 1
add (Succ m) n = Succ (add m n) -- Line 2
THEOREM:
forall x :: Nat, add x Zero = x
PROOF: By induction
BASE CASE: x = f^0 undefined = undefined
add undefined Zero = undefined
{ Line 1, strict pattern match failure in first arg }
STEP CASE: Assume add x Zero = x, Prove add y Zero = y where y in f x
What y are in f x?
f x = (const undefined | const Zero | Succ) x
= const undefined x | const Zero x | Succ x
= undefined | Zero | Succ x
We have to consider each of these possibilities for y.
1) add undefined Zero = undefined { Base case }
2) add Zero Zero = Zero { Def. line 1 }
3) add (Succ x) Zero
= Succ (add x Zero) { Def. line 2 }
= Succ x { Step case assumption }
This exhausts the three cases for y.
Therefore, by induction add x Zero = x for all x :: Nat
Note how structural induction maps to induction over integers. You do
not have to enumerate some flattened form of the domain and do induction
over their enumerated order. Indeed, some domains (like binary trees)
are not even countably infinite, so the induction hypothesis would not
be valid when used in this way.
Instead you rely on the fact that all algebraic data types already have
an (at most countably infinite) complete partial order based on
constructor application (or eqivalently, initial algebra composition)
[and always remembering that there is an implied union in | with
undefined], grounded at undefined, and that consequently you can do
induction over constructor application.
I hope that there are no errors in the above and that I have not left
out even the smallest detail. You should be able to see from the above
that structural induction works on any algebraic data type.
Obviously, after the first time only a masochist would be so verbose.
But the induction hypothesis does after all require a first time! :)
Dan Weston
PR Stanley wrote:
Hi
One of you chaps mentioned the Nat data type
data Nat = Zero | Succ Nat
Let's have
add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ m)n = Succ (add m n)
Prove
add m Zero = m
I'm on the verge of giving up on this. :-(
Cheers
Paul
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
