<div dir="ltr">Daryoush,<br><br>The two chapters in the Handbook of Logic in Computer Science -- especially the <a href="http://www.cs.bham.ac.uk/%7Eaxj/pub/papers/handy1.pdf">one</a> by Abramsky and Jung -- are good.&nbsp; i noticed that Lloyd Allison wrote a book on practical denotational semantics. i&#39;ve never read it, but i was intrigued by his work using minimal message length as the basis for a generic framework in Haskell for machine-learning models. He might have something useful to say.<br>
<br>It is difficult to judge what would be a good book for you, however, because i don&#39;t know if you what your aim is. Do you want context, history and mathematical foundations or a quick way to
understanding enough FP-speak to write better commercial code? As i said, a lot of people loosely speak of the <i>target</i> of some compositionally defined function (usually based on some structural recursion) that preserves some operational notion of equality as the denotation. This is almost certainly what is going on in the references you cited early. You can kind of leave it at that.<br>
<br>On the other hand, if you wish to go deeper, the study of the meaning of programs is highly rewarding and will change the way you think. One particularly fruitful place is games semantics. Guy McCusker&#39;s PhD thesis might be a way in. Abramsky and Jagadeesan&#39;s papers might be a way in. As i said before, the places where denotational and operational semantics have had to rub elbows has been useful to both approaches. One of the hands down best characterizations of the relationship of the logical and operational view of computation is Abramsky&#39;s <a href="http://www.comlab.ox.ac.uk/people/samson.abramsky/cill.ps.gz">Computational Interpretations of Linear Logic</a>. In this paper Samson repeats the same process 3 times -- <br>
<ol><li>specifies a logic by giving syntax for formulae and proof rules</li><li>derives a term language (syntax of programs) and operational semantics that is sound w.r.t a type system given by the logical formulae</li><li>
derives a virtual machine for the term language</li><li>refines the logic by an analysis of where the logic fails to capture our intuitions about resources -- looping back to step 1</li></ol>The starting point is Intuitionistic Logic which yields the core of a standard functional language. The next iteration is Intuitionistic Linear Logic, which yields a linear FPL. The next iteration is Classical Linear Logic which yields a concurrent language. Following the development of this process will clarify the relationships between the logical and operational view -- which ultimately bear on reasonable interpretations of denotational interpretations.<br>
<br>If you make the step to say that the denotation must be the completely unfolded structure -- the tree of reductions, the collection of possible plays, etc -- then there are ways to see how these views logical, operational and denotational are all calculable from one another -- and why you might want to have all of them in any complete account of computation.<br>
<br>Best wishes,<br><br>--greg <br><br><div class="gmail_quote">On Wed, Sep 17, 2008 at 11:03 AM, Daryoush Mehrtash <span dir="ltr">&lt;<a href="mailto:dmehrtash@gmail.com">dmehrtash@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
I noticed that Wikipedia has listed a few text books on the topic:<br>
<br>
<a href="http://en.wikipedia.org/wiki/Denotational_semantics#Textbooks" target="_blank">http://en.wikipedia.org/wiki/Denotational_semantics#Textbooks</a><br>
<br>
Any recommendations on which one might be a &quot;better&quot; read?<br>
<br>
Thanks,<br>
<br>
Daryoush<br>
<br>
2008/9/16 Greg Meredith &lt;<a href="mailto:lgreg.meredith@biosimilarity.com">lgreg.meredith@biosimilarity.com</a>&gt;:<br>
<div><div></div><div class="Wj3C7c">&gt; Daryoush,<br>
&gt;<br>
&gt; Hopefully, the other replies about proving the monad laws already answered<br>
&gt; your previous question: yes!<br>
&gt;<br>
&gt; As for notions of semantic domain and denotational model, these ideas go<br>
&gt; back quite a ways; but, were given solid footing by Dana Scott. In a<br>
&gt; nutshell, we have essentially three views of a computation<br>
&gt;<br>
&gt; Operational -- computation is captured in a program and rules for executing<br>
&gt; it<br>
&gt; Logical -- computation is captured in a proof and rules for normalizing it<br>
&gt; Denotational -- computation is captured as a (completely unfolded)<br>
&gt; mathematical structure<br>
&gt;<br>
&gt; In the latter view we think of computations/programs as denoting some<br>
&gt; (usually infinitary) mathematical object. Our aim is to completely define<br>
&gt; the meaning of programs in terms of maps between their syntactic<br>
&gt; representation and the mathematical objects their syntax is intended to<br>
&gt; denote. (Notationally, one often writes such maps as [| - |] : Program -&gt;<br>
&gt; Denotation.) For example, we model terms in the lambda calculus as elements<br>
&gt; in a D-infinity domain or Bohm trees or ... . Or, in more modern parlance,<br>
&gt; we model terms in the lambda calculus as morphisms in some Cartesian closed<br>
&gt; category, and the types of those terms as objects in said category. The gold<br>
&gt; standard of quality of such a model is full abstraction -- when the<br>
&gt; denotational notion of equivalence exactly coincides with an intended<br>
&gt; operational notion of equivalence. In symbols,<br>
&gt;<br>
&gt; P ~ Q &lt;=&gt; [| P |] = [| Q |], where ~ and = are the operational and<br>
&gt; denotational notions of equivalence, respectively<br>
&gt;<br>
&gt; The techniques of denotational semantics have been very fruitful, but<br>
&gt; greatly improved by having to rub elbows with operational characterizations.<br>
&gt; The original proposals for denotational models of the lambda calculus were<br>
&gt; much too arms length from the intensional structure implicit in the notion<br>
&gt; of computation and thus failed to achieve full abstraction even for toy<br>
&gt; models of lambda enriched with naturals and booleans (cf the so-called full<br>
&gt; abstraction for PCF problem). On the flip side, providing a better syntactic<br>
&gt; exposure of the use of resources -- ala linear logic -- aided the<br>
&gt; denotational programme.<br>
&gt;<br>
&gt; More generally, operational models fit neatly into two ready-made notions of<br>
&gt; equivalence<br>
&gt;<br>
&gt; contextual equivalence -- behaves the same in all contexts<br>
&gt; bisimulation -- behaves the same under all observations<br>
&gt;<br>
&gt; Moreover, these can be seen to coincide with ready-made notions of<br>
&gt; equivalence under the logical view of programs. Except for syntactically<br>
&gt; derived initial/final denotational models -- the current theory usually<br>
&gt; finds a more &quot;home-grown&quot; denotational notion of equivalence. In fact, i<br>
&gt; submit that it is this very distance from the syntactic presentation that<br>
&gt; has weakened the more popular understanding of &quot;denotational&quot; models to just<br>
&gt; this -- whenever you have some compositionally defined map from one<br>
&gt; representation to another that respects some form of equivalence, the target<br>
&gt; is viewed as the denotation.<br>
&gt;<br>
&gt; Best wishes,<br>
&gt;<br>
&gt; --greg<br>
&gt;<br>
&gt; Date: Mon, 15 Sep 2008 10:13:53 -0700<br>
&gt; From: &quot;Daryoush Mehrtash&quot; &lt;<a href="mailto:dmehrtash@gmail.com">dmehrtash@gmail.com</a>&gt;<br>
&gt; Subject: Re: [Haskell-cafe] Semantic Domain, Function, &nbsp;and<br>
&gt; &nbsp; &nbsp; &nbsp; &nbsp;denotational model.....<br>
&gt; To: &quot;Ryan Ingram&quot; &lt;<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>&gt;<br>
&gt; Cc: Haskell Cafe &lt;<a href="mailto:haskell-cafe@haskell.org">haskell-cafe@haskell.org</a>&gt;<br>
&gt; Message-ID:<br>
&gt; &nbsp; &nbsp; &nbsp; &nbsp;&lt;<a href="mailto:e5b8e9790809151013k53fdc105i88f2f47f1f9b16bd@mail.gmail.com">e5b8e9790809151013k53fdc105i88f2f47f1f9b16bd@mail.gmail.com</a><br>
&gt;&gt;<br>
&gt; Content-Type: text/plain; charset=ISO-8859-1<br>
&gt;<br>
&gt; Interestingly, I was trying to read his paper when I realized that I<br>
&gt; needed to figure out the meaning of denotational model, semantic<br>
&gt; domain, semantic functions. &nbsp;Other Haskell books didn&#39;t talk about<br>
&gt; design in those terms, but obviously for him this is how he is driving<br>
&gt; his design. &nbsp; I am looking for a simpler tutorial, text book like<br>
&gt; reference on the topic.<br>
&gt;<br>
&gt; Daryoush<br>
&gt;<br>
&gt; On Mon, Sep 15, 2008 at 1:33 AM, Ryan Ingram &lt;<a href="mailto:ryani.spam@gmail.com">ryani.spam@gmail.com</a>&gt; wrote:<br>
&gt;&gt; I recommend reading Conal Elliott&#39;s &quot;Efficient Functional Reactivity&quot;<br>
&gt;&gt; paper for an in-depth real-world example.<br>
&gt;&gt;<br>
&gt;&gt; <a href="http://www.conal.net/papers/simply-reactive" target="_blank">http://www.conal.net/papers/simply-reactive</a><br>
&gt;&gt;<br>
&gt;&gt; &nbsp;-- ryan<br>
&gt;&gt;<br>
&gt;&gt; On Sun, Sep 14, 2008 at 11:31 AM, Daryoush Mehrtash &lt;<a href="mailto:dmehrtash@gmail.com">dmehrtash@gmail.com</a>&gt;<br>
&gt;&gt; wrote:<br>
&gt;&gt;&gt; I have been told that for a Haskell/Functional programmer the process<br>
&gt;&gt;&gt; of design starts with defining Semantic Domain, Function, and<br>
&gt;&gt;&gt; denotational model of the problem. &nbsp;I have done some googling on the<br>
&gt;&gt;&gt; topic but haven&#39;t found a good reference on it. &nbsp; &nbsp;I would appreciate<br>
&gt;&gt;&gt; any good references on the topic.<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; thanks,<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; daryoush<br>
&gt;&gt;&gt;<br>
&gt;&gt;&gt; ps. &nbsp;I have found referneces like<br>
&gt;&gt;&gt; <a href="http://en.wikibooks.org/wiki/Haskell/Denotational_semantics" target="_blank">http://en.wikibooks.org/wiki/Haskell/Denotational_semantics</a> &nbsp;which<br>
&gt;&gt;&gt; talks about semantic domain for &quot;the Haskell programs 10, 9+1, 2*5&quot;<br>
&gt;&gt;&gt; which doesn&#39;t do any good for me. &nbsp; &nbsp;I need something with a more real<br>
&gt;&gt;&gt; examples.<br>
&gt;&gt;&gt; _______________________________________________<br>
&gt;&gt;&gt; Haskell-Cafe mailing list<br>
&gt;&gt;&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
&gt;&gt;&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;&gt;&gt;<br>
&gt;&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; --<br>
&gt; L.G. Meredith<br>
&gt; Managing Partner<br>
&gt; Biosimilarity LLC<br>
&gt; 806 55th St NE<br>
&gt; Seattle, WA 98105<br>
&gt;<br>
&gt; +1 206.650.3740<br>
&gt;<br>
&gt; <a href="http://biosimilarity.blogspot.com" target="_blank">http://biosimilarity.blogspot.com</a><br>
&gt;<br>
&gt; _______________________________________________<br>
&gt; Haskell-Cafe mailing list<br>
&gt; <a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
&gt; <a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
&gt;<br>
&gt;<br>
</div></div></blockquote></div><br><br clear="all"><br>-- <br>L.G. Meredith<br>Managing Partner<br>Biosimilarity LLC<br>806 55th St NE<br>Seattle, WA 98105<br><br>+1 206.650.3740<br><br><a href="http://biosimilarity.blogspot.com">http://biosimilarity.blogspot.com</a><br>

</div>