[Haskell-cafe] lambda calculus and equational logic

[Patrick Browne]

> In Haskell what roles are played by 1)lambda calculus and 2) equational
> logic? Are these roles related?


Hi,
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.

Thanks,
Pat


This message has been scanned for content and viruses by the DIT Information Services E-Mail Scanning Service, and is believed to be clean. http://www.dit.ie