[Haskell-cafe] Re: lambda calculus and equational logic
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
> 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*.
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