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

Patrick Browne patrick.browne at dit.ie
Thu Jul 15 08:46:37 EDT 2010

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,

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

More information about the Haskell-Cafe mailing list