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. In a nutshell, we have essentially three views of a computation

• Operational -- computation is captured in a program and rules for executing it
• Logical -- computation is captured in a proof and rules for normalizing it
• Denotational -- 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 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 -- 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). 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 -- behaves the same in all contexts
• 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@gmail.com>
Subject: Re: [Haskell-cafe] Semantic Domain, Function,  and
       denotational model.....
To: "Ryan Ingram" <ryani.spam@gmail.com>
Cc: Haskell Cafe <haskell-cafe@haskell.org>
Message-ID:
       <e5b8e9790809151013k53fdc105i88f2f47f1f9b16bd@mail.gmail.com

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

+1 206.650.3740

http://biosimilarity.blogspot.com