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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
