0
$\begingroup$

Could the execution of a Haskell program be considered as a proof in equational reasoning. This follows on from my earlier question on Haskell and inductive proof. Currently I am stuck between morally yes, but technically perhaps no. Below are two Haskell programs together with what I consider to be paper based equational proofs of very simple theorems. I imagine that Haskell cannot do any form of symbolic proof (e.g. id a == a), so the proofs use ground terms or values.

-- Prog 1 non-recursive
x,y,z:
x = 1
y = x + 2
z = x + y
theoremZ = z == 4
-- Paper based equational proof of Prog 1
[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)
theoremSize =  size (Add (Add Empty 1) 2) == 2
-- Paper based equational proof of Prog 2
[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)
$\endgroup$
  • $\begingroup$ I suggest you edit your question to be more specific about what exactly your question is. Hasn't "Could the execution of a Haskell program be considered as a proof in equational logic?" already been answered on that other post? Is there some specific aspect that you have a question about? Can you formulate a more specific question about that aspect? The rest of your post is a sequence of declarative statements -- this is a question-and-answer site, so we need you to articulate a specific question. (A call for discussion, or an invitation for reactions, is not specific enough.) $\endgroup$ – D.W. Oct 20 '17 at 18:45
  • $\begingroup$ Perhaps the question has appeared before, but I could not find it, my previous post concerned induction. "your post is a sequence of declarative statements" the statements , code and links are intended to provide context. The rephrased question I am asking: "can I consider the execution of a Haskell program as an equational proof" $\endgroup$ – Patrick Browne Oct 20 '17 at 22:20
  • $\begingroup$ It looks to me like the 3rd paragraph of Derek Elkins' answer responds to this question. $\endgroup$ – D.W. Oct 21 '17 at 2:35
  • $\begingroup$ Apologies, I do not have enough knowledge to completely follow Derek Elkins' answer. Is the answer to this post in his sentence? "In practice, most programs correspond to completely trivial theorems or (intutionistic) propositional tautologies.". I will read his suggested links. $\endgroup$ – Patrick Browne Oct 21 '17 at 7:16
2
$\begingroup$

"Equational logic" has a fairly specific meaning, while you seem to be vaguely referring to the notion of "equational reasoning" which makes your question not meaningful. If we tried to take your question at face value, we immediately run into issues. Before we can talk about whether computation corresponds to proof in the logic, we'd first need to be able represent Haskell programs as terms in the logic! That can't be done, at least, not in a naive way. To handle binding forms and beta reduction, would require something like nominal/higher-order equational logic or utilizing explicit substitutions. This is just the beginning. Another question is: what do you want to constitute a Haskell program? Haskell is a Church-style language, meaning you need the type information to execute the code, i.e. a Haskell program has no meaning without type information. So does "Haskell program" mean some representation with all type information included, or do you intend to model type inference equationally somehow? Once you figure all that out, you then need some equations for your equational logic, at which point you run into another problem: Haskell has no formal semantics.

Let's step way back. For just plain arithmetic, how do we show that $2+2=1+3$? One answer is that we have an equational logic with equations like $2 = 1+1$, $3=1+(1+1)$, $(x+y)+z=x+(y+z)$, $x+y = y+x$, $0+x = x$. We might prove the equality then by using $2=1+1$ twice to get $(1+1)+(1+1) = 1+3$ then use associativity to get $1+(1+(1+1))$, and then $3 = 1+(1+1)$ to get $1+3 = 1+3$ which is then true by reflexivity. There are many other proofs besides this one that could be formulated. Just given a list of equations gives you no guidance on the proof approach, i.e. which equations to apply when and in which direction. Furthermore, if you fail to find a proof, you don't know if that's just because you weren't clever enough, or if there actually is no proof (i.e. the expressions are not equal). Both of these problems are solved by formulating a notion of "normal form" and a rewrite system that takes any term to its normal form. This is what Knuth-Bendix completion and its successors do1. In this case, each rewrite rule is derived from an equational proof, and the sequence of steps can be interpreted as stitching together these proofs with transitivity.

But this is not what people are thinking when they compute by hand, it's not what your calculator/computer is doing, and it's not even what automated theorem provers/proof assistants are typically doing2. Typically this is turned around: we have an algorithm for addition, and two expressions are considered equal when the algorithm produces the same result for both of them (where "the same" here means syntactically identical). In other words, computation comes first and "equality" is a derived concept.

For arithmetic, one might argue about which perspective is more "fundamental", but for a programming language it's clear computation is the fundamental notion. This computational approach frees us to use any representation of "terms" we want and any algorithmic approach we want as long as it's (ultimately) deterministic. Of course, this presumes that normal forms exist and are computable. For a general programming language, neither statement is true. Computing a normal form is then usually semidecidable, and the "equality" gets weakened to a partial equivalence relation. Most proof assistants avoid this issue by restricting to strongly normalizing languages. Computational Type Theory/NuPRL takes a very different approach. It exposes the operational semantics of its built-in notion of computation and gives the user some control over that computation process, e.g. "perform one beta reduction". We can then define "equality" as $x = y$ iff $x \leadsto^* x'$ and $y\leadsto^* y'$ and $x' =_\alpha y'$ where $\leadsto^*$ is the reflexive, transitive closure of the one-step reduction relation. This captures the previous notion when $x$ and $y$ have normal forms, but it allows equating expressions that lack normal forms as well, as long as they reduce to a common expression. This casts us back into the world where there's no obvious strategy, and we can't in general be sure whether two expression are unequal or we have simply failed to find a proof. That's unavoidable, since this notion of equality is not decidable.

Unsurprisingly, the steps of your "equational proofs" don't directly have to do with equality, but are, instead, sketches of proofs that e.g. $1+(2+1)\leadsto^* 4$ with respect to a hypothetical operational semantics for Haskell.

1 For just checking whether two ground terms are equal, a simpler algorithm called congruence closure can be used.

2 It (or congruence closure) is what most automated theorem provers are doing if you do literally present a series of equations and then ask if two expressions are equal, but not if numbers are built-in nor, more for proof assistants, if you define addition algorithmically. More generally, many proof assistants have built-in notion of computation, and many automated theorem provers heavily rely on decision procedures.

$\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.