Patrick Browne wrote:
In Haskell what roles are played by 1)lambda calculus and 2) equational
logic? Are these roles related?
Thanks for your clear and helpful responses.
I am aware that this question can lead to into very deep water.
I am comparing Haskell with languages based on equational logic (EL)
(e.g. Maude/CafeOBJ, lets call them ELLs). I need to identify the
fundamental distinction between the semantics of ELLs and Haskell. The
focus of my original question was just the purely functional, side
effect free, part of Haskell.
Semantics can be understood under three headings:
*Denotational Semantics; is a model theoretical approach which describes
a program in terms of precise mathematical objects (e.g. sets and
functions) which provide meaning to a program text.
*Operational semantics: provides a technique for computing a result, ELs
use term rewriting systems for their operational semantics.
*Proof theoretic semantic: syntactically derivable proofs, can use the
rules of a logic
The relationship between the denotational and the proof theoretic
semantic is important for soundness and completeness. Which was sort of
behind my original question.
Would it be fair to say
1)Lambda calculus provides the operational semantics for Haskell
2)Maybe equational logic provides the denotational semantics.
3)I am not sure of proof theoretic semantic for Haskell.
The Curry-Howard correspondence is a proof theoretic view but only at
type level.
Obviously, the last three points are represent my efforts to address
this question. Hopefully the café can comment on the accuracy of these
points.
Lambda calculus is the basis for all three types of semantics:
1) Call-by-need (usually, implementations of Haskell are free to choose
other evaluation strategies as long as the denotational semantics match)
2) The denotational semantics of a lambda calculus with general
recursion, see also
http://en.wikibooks.org/wiki/Haskell/Denotational_semantics
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.
Regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
