6
$\begingroup$

Chapter 7 of The Haskell Road to Logic Math and Programming discusses induction and recursion.

Haskell is strongly typed and we can define the natural numbers

data Natural = Z | S Natural
deriving (Eq, Show)

and we can try to construct addition

plus m Z = m
plus m (S n) = S (plus m n)

Can we write a program that proves that addition is associative $(a+b)+c = a+(b+c)$?
Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$?


Is it possible to write a program (e.g. in Haskell) that proves the equivalence of two other programs?

Model-checking a general purpose language is neigh impossible since models must be domain specific to be practical. Due to Gödel's Incompleteness Theorem, there simply is no method for automatically finding proofs in a sufficiently expressive logic.

This means that you have to write proofs yourself, which raises the question of whether the effort is worth the time spent. Of course, the effort creates something very valuable, namely the assurance that your program is correct. The question is not whether this is a must-have, but whether the time spent is too great a cost. The thing about proofs is that while you may have an "intuitive" understanding that your program is correct, it is often very difficult to formalize this understanding as a proof.


This blog says associativity and other simple statements can be proven in Haskell using the Curry-Howard correspondence. Not entirely sure what that is.

https://jeltsch.wordpress.com/2012/04/30/dependently-typed-programming-and-theorem-proving-in-haskell/

assoc :: Nat nat1                                          ->
         Nat nat2                                          ->
         Nat nat3                                          ->
         (nat1 :+ nat2) :+ nat3 :== nat1 :+ (nat2 :+ nat3)
assoc Zero        nat2 nat3 = Refl
assoc (Succ nat1) nat2 nat3 = case assoc nat1 nat2 nat3 of
                                  Refl -> Refl

The program compiles and therefore the proof works.


Apologia

I am an experience mathematicians, but I am new to how programmers and CS people think about proofs and theorem-proving. So please excuse me if I confuse one branch of math for the other.

$\endgroup$
  • 3
    $\begingroup$ Please ask only one question per question. This site doesn't work well when you mix multiple questions in your post. Proving associativity of addition is almost completely unrelated to proving equivalence of two programs. $\endgroup$ – D.W. Aug 30 '15 at 4:11
  • $\begingroup$ Note that many dialects of Lisp can treat code as data, so you can take a function like "x -> x*x+2x-1" and analyze and manipulate it, and turn the result back in code. The standard example is to create the derived "x' -> 2x+2" function. I would expect that you could extend this to derive the sum shown. $\endgroup$ – Thorbjørn Ravn Andersen Aug 30 '15 at 9:51
  • $\begingroup$ @ThorbjørnRavnAndersen can you write induction proofs in Lisp? $\endgroup$ – john mangual Aug 30 '15 at 11:00
  • $\begingroup$ I am not experienced enough with Lisp to be able to answer that. Perhaps this could be a new question? $\endgroup$ – Thorbjørn Ravn Andersen Aug 30 '15 at 11:10
  • $\begingroup$ I'm confused about what you are asking. Is your question Is it possible to write a program (e.g. in Haskell) that proves the equivalence of two other programs?. If so, you give the answer in the next paragraph. $\endgroup$ – cody Aug 30 '15 at 19:04
8
$\begingroup$

In order with the explicit questions:

  1. Yes
  2. Yes
  3. No

To answer the question I think you're attempting to ask, we can prove many things using type checking, but not everything. What does this have to do with programs? That's what the Curry-Howard correspondence tells us. The Curry-Howard correspondence is a relationship between logic and computational models. The informal version is "proofs and programs and programs are proofs". While the specifics are far too much to detail here, the rough idea is that a function (read program) that takes an input of type $A$ and produces an output of type $B$ is a proof that $A \rightarrow B$ (and yes the funtion type arrow maps to the logical implication arrow).

Why can't we do everything? The good old halting problem. Some things we just can't check. Even worse, in practice, we're often limited to things we already know we can check, i.e. programs that are of a subclass that we know always halt.

Just to give a more complicated example, I've written a proof/program for $1+\ldots n = \frac{n\cdot(n+1)}{2}$ in Coq. Coq is a bit different to Haskell, but the idea should be fairly apparent. In this case, Coq has the advantage that it's explicitly built for theorem proving, so we can get a "proof-like" version and a "program-like" version. The proof can only complete if all the types match correctly - i.e. if we can specify a way to get from the input type to the output type, in the normal type checking sense. To avoid using division, I've rephrased the lemma.

The proof-like version:

Fixpoint sum (n : nat) : nat :=
match n with
| 0 => 0
| S n' => n + sum n'
end.

Lemma sum_closed_form (n : nat) : 2 * sum n = n * (n + 1). 
Proof.
  induction n.
  reflexivity.
  assert (Step: sum (S n) = S n + sum n).
    reflexivity.
  rewrite Step.
  rewrite mult_plus_distr_l.
  rewrite IHn.
  assert (Id : S n = n + 1).
    omega.
  rewrite Id.
  repeat rewrite mult_plus_distr_l.
  repeat rewrite mult_plus_distr_r.
  omega.
Qed.

So apart from the individual steps being black boxes, it's fairly clear that this looks a lot like a normal proof - it is in fact an induction, and all the mystery black boxes are in fact just other proofs that allow us to take some input type to another. One of the key steps in understanding how this works is to look closely at statement of the lemma: Lemma sum_closed_form (n : nat) : 2 * sum n = n * (n + 1).

Notice that it looks a bit like a function declaration, it takes a parameter of type nat, and produces an output of type 2 * sum n = n * (n + 1). That is in fact what it is, so in this form we can see the proof bit, and get an idea of the function bit - i.e. the proof is in fact a program. More explicitly, it is this program:

sum_closed_form = 
fun n : nat =>
nat_ind (fun n0 : nat => 2 * sum n0 = n0 * (n0 + 1)) eq_refl
(fun (n0 : nat) (IHn : 2 * sum n0 = n0 * (n0 + 1)) =>
(fun Step : sum (S n0) = S n0 + sum n0 =>
eq_ind_r (fun n1 : nat => 2 * n1 = S n0 * (S n0 + 1))
(eq_ind_r (fun n1 : nat => n1 = S n0 * (S n0 + 1))
(eq_ind_r (fun n1 : nat => 2 * S n0 + n1 = S n0 * (S n0 + 1))
((fun Id : S n0 = n0 + 1 => eq_ind_r
(fun n1 : nat => 2 * n1 + n0 * (n0 + 1) = n1 * (n1 + 1))
(eq_ind_r (fun n1 : nat =>
n1 + n0 * (n0 + 1) = (n0 + 1) * (n0 + 1 + 1))
(eq_ind_r (fun n1 : nat =>
2 * n0 + 2 * 1 + n1 = (n0 + 1) * (n0 + 1 + 1))
(eq_ind_r (fun n1 : nat =>
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n1)
(eq_ind_r (fun n1 : nat =>
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n1 + (n0 + 1) * 1)
(eq_ind_r (fun n1 : nat =>
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n1 + (n0 + 1) * 1 + (n0 + 1) * 1)
(eq_ind_r (fun n1 : nat =>
2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n0 * n0 + 1 * n0 + n1 + n1)
(Decidable.dec_not_not
(2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) = n0 * n0 + 1 * n0 + (n0 * 1 + 1 * 1) +
(n0 * 1 + 1 * 1))
(dec_eq_nat (2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1))
(n0 * n0 + 1 * n0 + (n0 * 1 + 1 * 1) + (n0 * 1 + 1 * 1)))
(fun H : 2 * n0 + 2 * 1 + (n0 * n0 + n0 * 1) <> n0 * n0 + 1 * n0 +
(n0 * 1 + 1 * 1) + (n0 * 1 + 1 * 1) =>
(fun (P : Z -> Prop) (H0 : P (Z.of_nat 2 * Z.of_nat (sum n0))%Z) =>
eq_ind_r P H0 (Nat2Z.inj_mul 2 (sum n0)))
(fun x : Z => x = Z.of_nat (n0 * (n0 + 1)) -> False)
((fun (P : Z -> Prop)
(H0 : P (Z.of_nat n0 * Z.of_nat (n0 + 1))%Z) =>
eq_ind_r P H0 (Nat2Z.inj_mul n0 (n0 + 1)))
(fun x : Z => (2 * Z.of_nat (sum n0))%Z = x -> False)
((fun (P : Z -> Prop) (H0 : P (Z.of_nat n0 + Z.of_nat 1)%Z) =>
eq_ind_r P H0 (Nat2Z.inj_add n0 1))
(fun x : Z => (2 * Z.of_nat (sum n0))%Z =
(Z.of_nat n0 * x)%Z -> False)
(fun _ :  (2 * Z.of_nat (..))%Z =
(Z.of_nat n0 * (.. + 1))%Z =>
(fun  (P : Z -> Prop) (H0 : P (..)%Z) =>
eq_ind_r P H0 (Nat2Z.inj_add (..) (..)))
(fun x : Z => Z.of_nat (..) = x -> False)
((fun (P : ..) (H0 : ..) => eq_ind_r P H0 (..))
(fun x : Z => .. = ..%Z -> False)
(fun _ : .. => (..) (..) (..) (..)))
(inj_eq  (sum (S n0)) (S n0 + sum n0) Step))))
(inj_eq (2 * sum n0) 
(n0 * (n0 + 1)) IHn)))
(mult_plus_distr_r n0 1 1))
(mult_plus_distr_r n0 1 n0))
(mult_plus_distr_l (n0 + 1) n0 1))
(mult_plus_distr_l (n0 + 1) (n0 + 1) 1))
(mult_plus_distr_l n0 n0 1)) 
(mult_plus_distr_l 2 n0 1)) Id)
(Decidable.dec_not_not (S n0 = n0 + 1)
(dec_eq_nat (S n0) (n0 + 1))
(fun H : S n0 <> n0 + 1 =>
(fun (P : Z -> Prop)
(H0 : P (Z.of_nat 2 * Z.of_nat (sum n0))%Z) =>
eq_ind_r P H0 (Nat2Z.inj_mul 2 (sum n0)))
(fun x : Z => x = Z.of_nat (n0 * (n0 + 1)) -> False)
((fun (P : Z -> Prop)
(H0 : P (Z.of_nat n0 * Z.of_nat (n0 + 1))%Z) =>
eq_ind_r P H0 (Nat2Z.inj_mul n0 (n0 + 1)))
(fun x : Z => (2 * Z.of_nat (sum n0))%Z = x -> False)
((fun (P : Z -> Prop)
(H0 : P (Z.of_nat n0 + Z.of_nat 1)%Z) =>
eq_ind_r P H0 (Nat2Z.inj_add n0 1))
(fun x : Z => (2 * Z.of_nat (sum n0))%Z = (Z.of_nat n0 * x)%Z -> False)
(fun _ : (2 * Z.of_nat (sum n0))%Z =
(Z.of_nat n0 * (Z.of_nat n0 + 1))%Z =>
(fun (P : Z -> Prop) (H0 : P (Z.of_nat (S n0) + Z.of_nat (sum n0))%Z) =>
eq_ind_r P H0 (Nat2Z.inj_add (S n0) (sum n0)))
(fun x : Z => Z.of_nat (sum (S n0)) = x -> False)
((fun (P : Z -> Prop) (H0 : P (Z.succ (Z.of_nat n0))) =>
eq_ind_r P H0 (Nat2Z.inj_succ n0))
(fun x : Z => Z.of_nat (sum (S n0)) = (x + Z.of_nat (sum n0))%Z -> False)
(fun _ : Z.of_nat (sum (S n0)) =
(Z.succ (Z.of_nat n0) + Z.of_nat (sum n0))%Z =>
(fun (P : Z -> Prop) (H0 : P (Z.succ (Z.of_nat n0))) =>
eq_ind_r P H0 (Nat2Z.inj_succ n0))
(fun x : Z => Zne x (Z.of_nat (n0 + 1)) -> False)
((fun (P : Z -> Prop) (H0 : P (Z.of_nat n0 + Z.of_nat 1)%Z) =>
eq_ind_r P H0 (Nat2Z.inj_add n0 1))
(fun x : Z => Zne (Z.succ (Z.of_nat n0)) x -> False)
(fun H0 : Zne (Z.succ (Z.of_nat n0))
(Z.of_nat n0 + 1) => ex_ind (fun (Zvar29 : Z)
(Omega75 : Z.of_nat n0 = Zvar29 /\ (0 <= Zvar29 * 1 + 0)%Z) =>
and_ind (fun (Omega66 : Z.of_nat n0 = Zvar29)
(_ : (0 <= Zvar29 * 1 + 0)%Z) =>
ex_ind (fun (Zvar30 : Z) (Omega74 : .. /\ ..%Z) =>
and_ind (.. => ..) Omega74) (intro_Z (sum (..)))) Omega75)
(intro_Z n0))) (inj_neq (S n0) (n0 + 1) H)))
(inj_eq (sum (S n0)) (S n0 + sum n0) Step))))
(inj_eq (2 * sum n0) (n0 * (n0 + 1)) IHn)))) IHn)
(mult_plus_distr_l 2 (S n0) (sum n0))) Step) eq_refl) n
: forall n : nat, 2 * sum n = n * (n + 1)

To give a shorter example, the associativity of addition can be proved like so:

Lemma add_assoc (n m p : nat) : n + (m + p) = (n + m) + p.
Proof.
  induction n.
  reflexivity.
  simpl. rewrite IHn.
  reflexivity.
Qed.

The associated function is:

add_assoc = 
fun n m p : nat =>
nat_ind (fun n0 : nat => n0 + (m + p) = n0 + m + p) eq_refl
  (fun (n0 : nat) (IHn : n0 + (m + p) = n0 + m + p) =>
   eq_ind_r (fun n1 : nat => S n1 = S (n0 + m + p)) eq_refl IHn) n
     : forall n m p : nat, n + (m + p) = n + m + p  
$\endgroup$
  • $\begingroup$ I'm curious: is it actually possible to write a Haskell program that serves as a proof of $\sum_{i=1}^n i = n(n+1)/2$? From what little I know, it seems like you couldn't, since the statement contains a $\forall$, and I thought you had to step up to a dependent type system like Coq's to express that in your types? $\endgroup$ – Eli Rose Oct 27 '15 at 0:19
  • $\begingroup$ @EliRose, I believe so, but my experience with Haskell is too limited for that to be a confident statement. At least some work can be done towards dependent typing in Haskell. The $\forall$ shouldn't be to hard, as it just maps to the function type (as in the Coq example), and the tricky bit is the type on the right hand side of the function. Pushing things further, dependent typing isn't the only way to do this sort of thing, there might be a logic that's better, but I definitely couldn't say anything more there. $\endgroup$ – Luke Mathieson Oct 27 '15 at 0:31
  • $\begingroup$ DO NOT use haskell as a proof checker because you can always insert undefined and prove any propositions. $\endgroup$ – 盛安安 Oct 2 '16 at 19:15
  • $\begingroup$ @盛安安, this isn't a good reason not to use Haskell for theorem proving (there might be other reasons not to, I don't know). In Coq there's an "admit" function which "proves" any theorem. You can also just deliberately add logical contradictions as axioms, and prove anything. I imagine these things are true for any theorem proving tool. The solution is not to do it. The same solution as not using contradictions in proofs in pen and paper mathematics. $\endgroup$ – Luke Mathieson Oct 3 '16 at 12:25
2
$\begingroup$

The sort of question you are asking falls under at least two possible topics. One is theorem proving and the other symbolic computation. Regarding the second topic, I highly recommend the book "A = B" by Petkovšek, Wilf and Zeilberger, which treats algorithms for symbolic computation. In there you can read about Gosper's summation algorithm which computes closed forms of hypergeometric sums.

The point is that, once the algorithms is implemented and the implementation is proved correct, then we know that the algorithm produces correct answers so running it amounts to producing a proof.

Also, in the case of finding closed forms of sums it is often easy to check that an answer is correct: to verify that $\sum_i a_i = S_i$ verify that $S_{i+1} - S_i = a_i$, often simple algebraic manipulations suffice.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.