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