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

[Patrick Browne]

Heinrich Apfelmus wrote:

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


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

Best Regards,
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