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

[Heinrich Apfelmus]

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