[Haskell-cafe] Re: lambda calculus and equational logic
Heinrich Apfelmus
apfelmus at quantentunnel.de
Thu Jul 15 05:26:03 EDT 2010
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
More information about the Haskell-Cafe
mailing list