[Haskell-cafe] Re: lambda calculus and equational logic

[wren ng thornton]

Patrick Browne wrote:
> Heinrich Apfelmus wrote:
>> 3) Not sure what you mean by proof theoretic semantics. Apparently, the
>> trace of any program execution like, say
>>
>>    product [1..5] -> 1 * product [2..5] -> .. -> 120
>>
>> is a proof that the initial and the final expression denote the same value.
>>
>> The Curry-Howards correspondence is about the type system, viewing types
>> as logical propositions and programs as their proofs.
> 
> This seems to address the first point (the role of lambda calculus.
> But what of the second point, the role equational logic.
> I assume (perhaps incorrectly) that lambda calculus is not *a logic*.
> See: http://lambda-the-ultimate.org/node/3719


That depends a lot on what you think "logic" means. Certainly we should 
be willing to call Haskell's type system a logic, with the term-level 
serving as proofs of the types/propositions (by Curry/Howard). It's a 
woefully inconsistent logic[1], sure, but a logic nevertheless.

Whether we would want to call the term-level a logic is a different 
matter. And this is where we get into terminological disputes; e.g., to 
what extent are algebraic systems different/similar to logical systems? 
(and to what extent are computational systems similar/different to 
algebraic systems?) This isn't just an issue of terminology: it throws a 
spotlight on elephants hiding in the room, elephants such as whether all 
mathematics can be reduced to logic, what the relationship is between 
logic and language, etc. Mathematicians, logicians, philosophers, 
theoretical linguists, and computer scientists all have a stake in those 
arguments--- a stake which is, at best, tangential to the actual 
question, and therefore makes it hard to get a decent answer/discussion.

Equational logic is used heavily for reasoning about programs in Haskell 
(and pure functional languages generally). It shows up in the safety 
proofs for the type system, correctness proofs for compilers, strictness 
analysis, optimizations, etc. However, as you mention in that LtU post, 
equational reasoning doesn't really show up *in* Haskell, only in 
reasoning *about* Haskell. Without dependent types or a more developed 
formal language for reasoning with RULES and proving their correctness, 
it does not seem possible to support equational reasoning within Haskell 
(except in the most trivial sense that defining functions is defining a 
system of equations). It's not clear to me whether you're asking about 
equational reasoning for theory or metatheory.

Also, because the type system is inconsistent, that raises the question 
of what it could mean to reason in such a logic. Logicians throw up 
their hands whenever a logic is inconsistent, but computer scientists 
have been reasoning with inconsistency for years. In discussing a 
constructive LEM, Oleg highlights some interesting connections between 
the idea of monads-as-computation and well-known results about how the 
boundary of computability separates the space of Classical and 
Intuitionistic theorems. Issues of inconsistency also show up in 
reasoning about language-based security systems where sometimes we may 
wish to allow inconsistent states during computation so long as there is 
a formal guarantee that consistency is restored soon. But overall, the 
question of what it means to reason formally and correctly in the face 
of an inconsistent system is still an open question.


[1] Because of bottom, as well as many other reasons:
     http://okmij.org/ftp/Haskell/types.html#fix

[2] http://okmij.org/ftp/Computation/lem.html

-- 
Live well,
~wren