3
$\begingroup$

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

Improve this question
$\endgroup$
3
  • $\begingroup$ 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. $\endgroup$ Commented Oct 19, 2017 at 21:16
  • $\begingroup$ 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.) $\endgroup$ Commented Oct 19, 2017 at 21:20
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Oct 20, 2017 at 7:23

1 Answer 1

Reset to default
8
$\begingroup$

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 logic1 (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.

1 See Chapter 12.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Maybe in the first paragraph you should clarify that, when termination is guaranteed, we do not necessarily have an inductive proof, but we do have a proof (right?). Anyway, the paper statement is so vague that it's hard to understand what they want to say in precise terms. I have the feeling that they do not exploit Curry-Howard in any way, but they do exploit type safety: they just enforce some needed invariant though types (I think). $\endgroup$ Commented Oct 20, 2017 at 8:23

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.