[Haskell-cafe] Induction (help!)
Ryan Ingram
ryani.spam at gmail.com
Thu May 8 19:11:08 EDT 2008
On 5/8/08, Daniel Fischer <daniel.is.fischer at web.de> wrote:
> No. In the induction step, we prove that
> IF p(j) holds, THEN p(j+1) holds, too.
> p(j) is the assumption, and we prove that *given that assumption*, p(j+1)
> follows.
> Then we have proved
> (*) p(j) implies p(j+1), for all j.
To formalize this, you can work in a system of logic with the following rules:
Variable introduction:
x is not free in L,
L |- t is a type
proves
L, x :: t |- x :: t --- this is a proof of "x has type t"
Forall introduction (removing the above assumption)
L, x :: t |- p
proves
L |- forall x :: t. p
Assumption of a proposition:
L, p |- p --- no pre-requisites
Impication introduction ("Deduction"; if P then Q)
L, p |- q
proves
L |- p => q
The part to the left of the |- is an "environment"; it represents
assumptions you have made up to this point. The part to the right is
a statement which is "true" in that environment; the L just represents
"any environment".
For example, in the first rule, we say that if we know that t is a
type, and we haven't assumed anything about x yet, we can assume that
x is a member of that type. Then in the second rule, if we've proved
some proposition "p" once we've assumed that x is something of type t,
we can say that p holds for -all- x of type t; we didn't assume
anything about that x besides its type.
Induction corresponds to adding the following rule to the logic:
L |- p(0)
L |- forall x :: Nat, p(x) => p(x+1)
proves
L |- forall x :: Nat, p(x)
A "true" statement is one that holds with no environment:
|- p
Now, if you are proving something by induction, you had to prove that
second line; and the only way to do so is by making some assumptions.
A skeleton of a proof:
axiom
|- Nat is a type
variable introduction
x :: Nat |- x :: Nat
proposition introduction
x :: Nat, p(x) |- p(x)
... some proof using p(x) here ...
x :: Nat, p(x) |- p(x+1)
deduction
x :: Nat |- p(x) => p(x+1)
forall introduction
|- forall x :: Nat, p(x) => p(x+1)
... some proof of p(0) here ...
|- p(0)
induction
|- forall x :: Nat, p(x)
Every proof by induction looks basically like this; you just need to
fill in the "... some proof here..." parts.
-- ryan
More information about the Haskell-Cafe
mailing list