# Does a Haskell program count as an inductive proof?

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

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)
-- Equational Proof
---> (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

• I did not check the paper, but I am leaning towards "yes". That sentence seems to be a vague oversimplification of the usual Curry-Howard correspondence (which does not work in Haskell unless termination is required, as they do.) I am not too happy about their next sentence "makes testing much more powerful". They are speaking of complex aspects without providing too much detail, and being quite vague. (This is perhaps to be expected by a paper which is 1) a "towards..." and 2) a applied ontology paper) Still, I think they do have at least some ground to stand on. – chi Oct 19 '17 at 21:16
• Anyway, the full explanation would be too broad. You might want to check inductive types, Curry-Howard, type theory, types & programming languages theory, etc. There are very broad topics to present here. Anyway, induction goes far beyond natural numbers. In programming languages / type theory, usually we use much more general induction principles (see e.g. those from domain theory, involving least fixed points, etc.) – chi Oct 19 '17 at 21:20
• In a paper on medical records, take any statement about the theory of programming languages and logic with a grain of salt. Make it a nice large crystal of salt, actually. – Andrej Bauer Oct 20 '17 at 7:23

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.