[Haskell-cafe] Semantic Domain, Function, and denotational model.....

[Greg Meredith]

Daryoush,

Hopefully, the other replies about proving the monad laws already answered
your previous question: yes!

As for notions of semantic domain and denotational model, these ideas go
back quite a ways; but, were given solid footing by Dana
Scott<http://en.wikipedia.org/wiki/Dana_Scott>.
In a nutshell, we have essentially three views of a computation

   - Operational <http://en.wikipedia.org/wiki/Operational_semantics> --
   computation is captured in a program and rules for executing it
   - Logical <http://en.wikipedia.org/wiki/Proof-theoretic_semantics> --
   computation is captured in a proof and rules for normalizing it
   - Denotational <http://en.wikipedia.org/wiki/Denotational_semantics> --
   computation is captured as a (completely unfolded) mathematical structure

In the latter view we think of computations/programs as denoting some
(usually infinitary) mathematical object. Our
aim<http://en.wikipedia.org/wiki/Domain_theory>is to completely define
the meaning of programs in terms of maps between
their syntactic representation and the mathematical objects their syntax is
intended to denote. (Notationally, one often writes such maps as [| - |] :
Program -> Denotation.) For example, we model terms in the lambda calculus
as elements in a D-infinity domain or Bohm trees or ... . Or, in more modern
parlance, we model terms in the lambda calculus as morphisms in some
Cartesian closed category, and the types of those terms as objects in said
category. The gold standard of quality of such a model is full
abstraction<http://en.wikipedia.org/wiki/Denotational_semantics#Full_abstraction>--
when the denotational notion of equivalence exactly coincides with an
intended operational notion of equivalence. In symbols,


   - P ~ Q <=> [| P |] = [| Q |], where ~ and = are the operational and
   denotational notions of equivalence, respectively


The techniques of denotational semantics have been very fruitful, but
greatly improved by having to rub elbows with operational characterizations.
The original proposals for denotational models of the lambda calculus were
much too arms length from the intensional structure implicit in the notion
of computation and thus failed to achieve full abstraction even for toy
models of lambda enriched with naturals and booleans (cf the so-called full
abstraction for PCF
problem<http://en.wikipedia.org/wiki/Programming_language_for_Computable_Functions>).
On the flip side, providing a better syntactic exposure of the use of
resources -- ala linear logic -- aided the denotational programme.

More generally, operational models fit neatly into two ready-made notions of
equivalence

   - contextual
equivalence<http://encyclopedia2.thefreedictionary.com/Contextual+equivalence>--
behaves the same in all contexts
   - bisimulation <http://en.wikipedia.org/wiki/Bisimulation> -- behaves the
   same under all observations

Moreover, these can be seen to coincide with ready-made notions of
equivalence under the logical view of programs. Except for syntactically
derived initial/final denotational models -- the current theory usually
finds a more "home-grown" denotational notion of equivalence. In fact, i
submit that it is this very distance from the syntactic presentation that
has weakened the more popular understanding of "denotational" models to just
this -- whenever you have some compositionally defined map from one
representation to another that respects some form of equivalence, the target
is viewed as the denotation.

Best wishes,

--greg

Date: Mon, 15 Sep 2008 10:13:53 -0700
From: "Daryoush Mehrtash" <dmehrtash at gmail.com>
Subject: Re: [Haskell-cafe] Semantic Domain, Function,  and
       denotational model.....
To: "Ryan Ingram" <ryani.spam at gmail.com>
Cc: Haskell Cafe <haskell-cafe at haskell.org>
Message-ID:
       <e5b8e9790809151013k53fdc105i88f2f47f1f9b16bd at mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1

Interestingly, I was trying to read his paper when I realized that I
needed to figure out the meaning of denotational model, semantic
domain, semantic functions.  Other Haskell books didn't talk about
design in those terms, but obviously for him this is how he is driving
his design.   I am looking for a simpler tutorial, text book like
reference on the topic.

Daryoush

On Mon, Sep 15, 2008 at 1:33 AM, Ryan Ingram <ryani.spam at gmail.com> wrote:
> I recommend reading Conal Elliott's "Efficient Functional Reactivity"
> paper for an in-depth real-world example.
>
> http://www.conal.net/papers/simply-reactive
>
>  -- ryan
>
> On Sun, Sep 14, 2008 at 11:31 AM, Daryoush Mehrtash <dmehrtash at gmail.com>
wrote:
>> I have been told that for a Haskell/Functional programmer the process
>> of design starts with defining Semantic Domain, Function, and
>> denotational model of the problem.  I have done some googling on the
>> topic but haven't found a good reference on it.    I would appreciate
>> any good references on the topic.
>>
>> thanks,
>>
>> daryoush
>>
>> ps.  I have found referneces like
>> http://en.wikibooks.org/wiki/Haskell/Denotational_semantics  which
>> talks about semantic domain for "the Haskell programs 10, 9+1, 2*5"
>> which doesn't do any good for me.    I need something with a more real
>> examples.
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>



-- 
L.G. Meredith
Managing Partner
Biosimilarity LLC
806 55th St NE
Seattle, WA 98105

+1 206.650.3740

http://biosimilarity.blogspot.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20080916/b15a6461/attachment.htm