[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,
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
More information about the Haskell-Cafe
mailing list