Does a Haskell program count as an inductive proof?

Question

Is the following statement from [1] true?

"Since recursion is the main computational technique, a terminating pure Haskell program counts as an inductive proof of a theorem."

My intuition is that inductive proofs require a base case, assume the hypothesis case for k, prove induction step fork+1. I am not clear on how these steps occur in the execution of a program (function?). Also, what logic is employed in such a proof?

Regards, Patrick Browne

[1] http://ebooks.iospress.com/volumearticle/44257

---

Thanks for your very helpful answers.

Would it be fair to say that the answer may be morally yes [1], but technically perhaps no [2].

Below are two Haskell programs together with what I consider to be equational proofs (not inductive) that they evaluate to a desired ground term. The first program is not recursive. So does the quote in my original posting include non-recursive programs?

    -- Prog 1 non-recursive
x,y,z:
x = 1
y = x + 2
z = x + y
proveZ = z == 4
-- Equational Proof
[1]: (z)
---> (x + y)
[2]: (x + y)
---> (1 + y)
[3]: (1 + y)
---> (1 + (2 + x))
[4]: (1 + (2 + x))
---> (1 + (2 + 1))
[5]: (1 + (2 + 1))
---> (1 + 3)
[6]: (1 + 3)
---> (4)

-- Prog 2 recursive
data Vector  = Empty | Add Vector Int
size Empty  = 0 
size (Add v d)  = 1 + (size v)
proveSize =  size (Add (Add Empty 1) 2) == 2
-- Equational Proof
[1]: (size (Add (Add Empty 1) 2)) 
---> (1 + (size (Add Empty 1))) 
[2]: (1 + (size (Add Empty 1))) 
---> (1 + (1 + (size Empty))) 
[3]: (1 + (1 + (size Empty))) 
---> (1 + (1 + 0)) 
[4]: (1 + (1 + 0)) 
---> (1 + 1) 
[5]: (1 + 1) 
---> (2)

The motivation for my original question is that I wish to understand the relationship between the evaluation of a Haskell program and the application of equational logic to the same Haskell program. While Haskell produces the correct answer, as would a non-functional language, is the computation a proof in equational logic? I imagine that Haskell cannot do any form of symbolic proof (e.g. id a == a). In summary is my yes/no opinion reasonable?

[1] Fast and Loose Reasoning is Morally Correct: http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf

[2] Formulating Haskell: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.1399

Answer 1

The statement is not true as stated. Even if we imagine a Haskell-like language where all functions terminate and values are non-bottom, only some programs would correspond to inductive proofs (as opposed to proofs not using induction), but it would be the ones that (directly or indirectly) use recursion. That said, what they are doing induction over may not at all be obvious. (For the OP: every inductive type gives rise to a notion of structural induction with "mathematical induction" just being structural induction over the naturals.) Many patterns of recursion in practical programs, e.g. quicksort, do not correspond to a direct structural induction over their inputs.

For real Haskell, for just about any program proving that it terminates for all inputs requires very strong restrictions on those inputs: all values must be fully defined and all passed in functions must terminate on at least the inputs exercised by the current program. The latter isn't checkable in general, but what we can do instead is reduce a value that stands for a putative proof to normal form, and if we succeed then we have a real proof. Unfortunately, Haskell doesn't evaluate things to normal form but only to weak head normal form. For some types we can force the weak head normal form of one expression to correspond to normal forms via rnf, but we can't do this for functions in general.

Even without restrictions, programs in Haskell correspond to proofs in some logic, albeit an inconsistent one. This leads to another aspect that they conveniently didn't elaborate on. They say that certain Haskell programs correspond to proofs of theorems, but they don't say what theorems you can state! Haskell (particularly with higher-rank polymorphism) is closely related to the polymorphic lambda calculus and that corresponds to intuitionistic, second-order propositional logic¹ (SOPL) (not to be confused with second-order predicate logic which is usually what "second-order logic" refers to). While SOPL is uninteresting in the classical case, it turns out to be pretty powerful in the intuitionistic case, capable of embedding intuitionistic first-order predicate logic. The embedding is non-obvious and even with it you would not be able to prove something like the Fundamental Theorem of Arithmetic. In practice, most programs correspond to completely trivial theorems or (intutionistic) propositional tautologies.

From my (admittedly very brief) skimming of the paper, it seems that they are more interested in the Prolog-like reasoning the type class system enables than leveraging the propositions-as-types correspondence. So their comments seem to be a bit of a non sequitur anyway.

¹ See Chapter 12.