Talk:Denotational semantics/Archive1

From Wikipedia, the free encyclopedia

Denotational semantics and functional programming reinforced each other's development. The design of functional programming languages was influenced by denotational semantics, the connection is certainly not only in one direction.

Contents

[edit] Questions about recent additions by CarlHewitt

I believe some of the remarks added to the article regarding denotation semantics and concurrency are incorrect. The article suggest atm that denotational semantics is inherently non-concurrent. However, this is not the case: Plotkin shows in his 1997 TCS paper "LCF Considered as a Programming Language" that PCF (the LCF programming language) can be extended with the parallel or and that a denotational model based on domains can be defined for this extended language. Hence, it can be argued that domains already allow for concurrency.

In fact, up until the 1990s it was an active topic of research on how to put extra restrictions onto domains such that only sequential functions are represented (see e.g. Ong's chapter Correspondence between Operational and Denotational Semantics: The Full Abstraction Problem for PCF, in Vol 4 of the Handbook of Logic in Computer Science) -- Koffieyahoo 10:05, 6 September 2005 (UTC)

The article also seems to have been retargeted with a focus on the Actor model, which seems completely unjustified given the wide spread use of denotational semantic through out computer science. -- Koffieyahoo 10:09, 6 September 2005 (UTC)

The article cites orginal sources. Can you cite any errors in the article?--Carl Hewitt 16:28, 6 September 2005 (UTC)

At least at two points:

  • "The Actor model provides an extension of denotational semantics to concurrent computation as demonstrated first by a theorem of Carl Hewitt and Henry Baker [1977]". I read here that denotational semantics up until 1977, and hence domain theory (it was invented before 1977) was basically non-concurrent. However, as Plotkin shows also 1977, domain theory is already capable of expression concurrent programs (see reference above). Moreover, it is self the Actor Model is a syntact construct and requires a such requires a denotational semantics. So, saying that the Actor model provides the extension is incorrect if you believe that syntaxt is something different from semantics.
  • "Sequential computations form an ω-complete subdomain": this assumes that we know in a denotational sense what sequential computations are. However, as explained in the chapter by Ong (cited above) a satisfactory definition is still lacking at least in the case of domain theory: the exisisting definitions work okay for first order functions, but in the higher-order case they don't (this e.g. spawned the field of game semantics).

Two other remarks regarding you additions:

  • Is the indented part in Unbounded nondeterminism section a quote? If it is, it is of such length that is highly likely violates a copyright.
  • In Sequential computations form an ω-complete subdomain section there is an informal proof: It's not only my opinion that proofs have not real place in encyclopedias. That's what the references are for.

-- Koffieyahoo 07:47, 7 September 2005 (UTC)

Thanks for your comments.

  • Ong is not an original source.
  • The indented part is a direct quote from Clinger's disseration. It is included in the Wikipedia by permission of the author.
  • The proof is short and informal. It is best thought as being an argument. The Wikipedia allows arguments.

--Carl Hewitt 17:03, 8 September 2005 (UTC)

Three remarks on this:

  • Ong gives on overview. Overviews are an integral part of science: Due to the way in which they present existing work they normally lead to new insights. Moreover, he cites the original sources.
Not to detract from Ong's work, it is not an original source.--Carl Hewitt 14:25, 9 September 2005 (UTC)
  • I've seen no proof that Clinger did so. If he did so, please provide that proof.
Clinger gave permission in a private message to me. I suggest that you contact him directly.--Carl Hewitt 14:25, 9 September 2005 (UTC)
  • Didn't respond wrt the errors I pointed out. Please do so (Learn to respond to all arguments. Do proceed to practice this selective responding. It's very annoying. Moreover, learn to respond to the point.).

-- Koffieyahoo 10:34, 9 September 2005 (UTC)

Sigh, I don't see why I'm not allowed to cite an overview articles. Particular one that provides you with all the relevant references. Ong cites at least 50 relevant references which I'm not going to repeat here. Moreover, overview or not, this is completely irrevant considering the remarks. So, can you now please answer my questions and remarks. -- Koffieyahoo 14:45, 12 September 2005 (UTC)

You can cite overview articles. I was simply pointing out that they are not original sources.--Carl Hewitt 16:45, 12 September 2005 (UTC)

Regrarding Clinger's thesis: looking at the front matter of the thesis I can't even tell if he's the rightful copyright owner. That might in fact be MIT. -- Koffieyahoo 14:45, 12 September 2005 (UTC)

Clinger is the copyright owner. MIT has the right to distribute.--Carl Hewitt 16:45, 12 September 2005 (UTC)
Do you have any particular questions at this point?--Carl Hewitt 16:49, 12 September 2005 (UTC)

Wikipedia is an encyclopedia. As such, there is a policy of Wikipedia:No original research. For starters, it states: "In fact, all articles on Wikipedia should be based on information collected from primary and secondary sources." Overview articles are important references for Wikipedia. --TuukkaH 16:23:54, 2005-09-12 (UTC)

I agree.--Carl Hewitt 16:45, 12 September 2005 (UTC)
Besides evading many of Koffieyahoo's points, I would also point out that the article completely ignores the contributions of J. de Bakker and his collaborators on the denotational semantics of concurrency.--CSTAR 06:44, 10 November 2005 (UTC)
Is any of de Bakker's work on denotational semantics?--Carl Hewitt 07:33, 10 November 2005 (UTC)

[edit] Reply to Hewitt

For starters, you can look at [1]. Please note the following:

  • Krzysztof R. Apt, J. W. de Bakker: Exercises in Denotational Semantics. MFCS 1976: 1-11
  • J. W. de Bakker: Least Fixed Points Revisited. Theor. Comput. Sci. 2(2): 155-181 (1976)

Not listed there is work by P. America, J. Zucker, de Bakker and others specifically on denotational semantics of concurrency.

  • P. America, J. de Bakker, J. N. Kok and J. Rutten: Denotational semantics of a parallel object-oriented language, Information and Computation, 83(2): 152 - 205 (1989)

(This paper actually appeared many years earlier in a technical report published by Centrum voor Wiskunde en Informatica

This is one of a series of papers that consider metric space denotational models. The idea in these papers can be described as finding fixed points of contractive functors on metric categories.

--CSTAR 17:06, 10 November 2005 (UTC)
Samson Abramsky has also done some work in this area.--Carl Hewitt 13:20, 11 November 2005 (UTC)
I wasn't aware of any work that Abramsky has done in this specific area (metric space domains), but maybe he has. Anyway the article is deficient in references, in coverage of the material and in clarity. In particular, I don't think you're use of extensive direct quotes is helpful. Moreover, citing original sources in science does not mean the same thing as it does in history, (including history of science) since most work in science builds heavily on previous work. I don't see how your response to KoffieYahoo's objections, in which you assert that you cite original sources is relevant.--CSTAR 17:33, 11 November 2005 (UTC)
I studied with Abramsky for a couple of years at Imperial in the early 1990s. The article has a slanted POV. Charles Matthews 18:57, 11 November 2005 (UTC)
This article is particularly important, since it is of a foundational nature in COmputer Science. Aside from the intro gives a completely distorted view of denotational semantics. It should at least begin with denotational models for the lambda calculus and relate this to work of Dana Scott and Chris Strachey. I am willing to do this myself, although I would be very appreciative if someone else did this; I would like to avoid another confrontation with Hewitt. Thanks.--CSTAR 21:24, 11 November 2005 (UTC)
Of course you realize that the lambda calculus models are submodels of Actor models in which the arrival ordering of messages sent to Actors is not visible. Nevertheless this is a useful special case that deserves treatment.--Carl Hewitt 10:54, 21 November 2005 (UTC)
Nobody is disputing the generality of the actor model of computation and its ability to model various things such as concurrency and indeterminism. However, your approach makes about as much sense as to claim that to address (a): provide a denotational semantics for the lamba calculus it would suffice to achieve (b) provide a denotational model for Turing machines (including a definition of what this means). The exercise (b), though quite interesting, would not adequately address (a).--CSTAR 17:35, 21 November 2005 (UTC)

[edit] Denotational semantics of functions

Is this section properly titled? Semantics is a function from a set of syntactic objects into a semantic domain. In what sense are you giving semantics of a function. I'm not against using imprecise language, but I think these examples should be presented carefully. I'm not sure how to rename the section, but its current title is confusing.--CSTAR 05:42, 12 November 2005 (UTC)

I concur. What do you think of "Denotational semantics of functional programs"?--Carl Hewitt 05:52, 12 November 2005 (UTC)
That probably is better. The example you give is a functional (i.e., non imperative) program.--CSTAR 06:02, 12 November 2005 (UTC)
I made the change. Thanks for noticing this.--Carl Hewitt 14:08, 12 November 2005 (UTC)
The example is still confusing; It defines the meaning of a recursive functional program.--CSTAR 18:21, 12 November 2005 (UTC)
I don't quite understand what you find confusing. Thanks,--Carl Hewitt 13:23, 13 November 2005 (UTC)

[edit] Reply to Hewitt on Fixed point semantics

(Least) fixed point semantics is a natural (and the most common) way to associate a denotation to a recursively defined program. Least fixed points can also be used to solve reflexive domain equations. But in your example, you seem to suggest that any functional program requires a fixed point definition. This is not true. For example, a language consisting of natural numbers and polynomial operations (without recursion) does not need "fixed point semantics."

One major defect of the article is this: It never mentions the basic point of denotational semantics, which is to associate meaning to expressions in a compositional way. Semantics for languages which allow recursion rely on fixed point semantics to assign meaning to definition by recursion.

There are other defects, which I will mention in due course. --CSTAR 16:35, 13 November 2005 (UTC)

I have written a section on compositonality that treats it from a modern point of view. See what you think. You should be aware that some of the classical treatments of compositonality in the text books have severe limitations, e.g., they do not handle delayed evaluation.--Carl Hewitt 10:13, 21 November 2005 (UTC)
Your new section is not an improvement. For example, it doesn't explain how denotations of variable binding operators work. Saying this treats this from a "modern point of view" is your opinion, which I doubt is widely shared.--CSTAR 16:50, 21 November 2005 (UTC)
I have explained how variable binding works. See what you think.
That the Actor model approach to compositionality is a modern point of view is not just my opinion. See the references in Actor model. The reason that the Actor approach has become the modern point of view is that other approaches have run into trouble, e.g. with delayed evaluation.
Regards,--Carl Hewitt 18:47, 21 November 2005 (UTC)
Baloney. See for example work of Mitch Wand and coworkers, such as:
Guttman, J. D., Ramsdell, J. D., and Wand, M. VLISP: a verified implementation of Scheme. Lisp and Symbolic Computation, 8 (1995), 5--32.
--CSTAR 19:03, 21 November 2005 (UTC)
The problem with classical approaches for compositional denotatonal sementics in dealing with expressions of form "delay <Expression>" has been how to formaize the semantics of the evaluation of <E>.
The Actor model provides a perfectly reasonable account:
The delay expression responds to an <Eval> message with environment E by creating a closure Actor C that has an address (called body) for <Expression> an address (called environment) for E.
When C receives a message M with Customer0, it creates a new Actor Customer1 and sends <Expression> an Eval message with environment E and the address of Customer1.
When Customer1 receives a value V, it sends V the message M with Customer0.
What is your account for the semantics of delayed evaluation?
Regards,--Carl Hewitt 19:31, 21 November 2005 (UTC)
See exercise 9-14 (p205) of
  • Kent Dybvig, The Scheme Programming Language, Prentice Hall, 1987.
Given that a denotational semantics for Scheme exists, including continuations (as per previous reference) this completes the proof.--CSTAR 20:15, 21 November 2005 (UTC)
I don't think that you quite understand the problem here. Denotational semantics is supposed to be a mathematical model theory. You can't just go off and call some particular program (e.g. eval) in the middle of your mathematical model. This is particularly true when eval is written in the programming language for which a model is to be defined!--Carl Hewitt 20:36, 21 November 2005 (UTC)
I don't think that you quite understand the problem here. Nice figure of speech.
In fact, my proof does not use eval . If you like, see Abelson and Sussman. p 264 for an implemementation of delayed evaluation within Scheme. Scheme itself has a denotational semantics. --CSTAR 21:05, 21 November 2005 (UTC)
Ah, but we are talking about mathematical models for denotational semantics here not implementation. I have provided the Actor compositional semantics above. (It's modular, relatively complete, quite short and understandable that it is correct.) What is your denotational semantics for delayed evaluation?--Carl Hewitt 21:41, 21 November 2005 (UTC)

[edit] Delayed evaluation within scheme

Ah, but implementation as used here means simply adding two definitions (not implementation at some low level): The mathematical semantics extends trivially to the extended language. Quoting Abelson and Sussman:

 (define (force delayed-object)
   (delayed-object))

On the other hand

 (delay <exp>)

is syntactic sugar for

 (lambda () <exp>)

I am relying on the existimng denotational semantics for Scheme, which I have show (by citing references) exists.

This is also modular, quite short and understandable that it is correct.QED--CSTAR 21:53, 21 November 2005 (UTC)

Sorry but it is not correct because (delay <exp>) is not necessarily a function of 0 arguments and therefore cannot possibly be syntactic sugar for (lambda () <exp>). For example (delay (plus 3 4)) is not a function of 0 arguments. In fact it is not even a function because it is in effect the number 7.
So now can say that you really didn't mean to attempt to provide a semantics for delayed evaluation because that would be too difficult. Instead you meant to provide a "hacked" (in the nonpejorative Sussman sense) version of delayed evaluation. The idea of the hacked version is that if a program suspects that a value V might be using delayed evaluation, it needs to call force with the argument V in order to obtain the real value of delayed evaluation. Of course if the suspicion is wrong then an error can result such as "Wrong number of arguments".
Regards--Carl Hewitt 01:32, 22 November 2005 (UTC)

[edit] Reply

What I am saying (directly citing H. Abelson and G. Sussman with J. Sussman, Structure and Interpretation of Computer Programs, MIT Press (1985) p 264) is that (delay <exp>) is an expression and that the meaning of this expression is the meaning of

(lambda () <expr>)

The meaning of this expression in turn is given by the denotational semantics of Scheme without delayed evaluation (as supplied by various papers in the literature)

Are you now saying that Abelson and Sussman made a mistake? --CSTAR 22:32, 21 November 2005 (UTC)

Steele and Sussman were (and are) "hackers" (in the nonpejorative sense). They were caught between a rock and hard place since they didn't understand Actors (according to the book you cited above). So they cut out on their own and attempted to "hack" (i.e. implement) their way forward. This approach had some strengths, but also some important limitations.
One of the limitations is that they ended up in some strange places. The attempt to patch delayed evaluation into Scheme is one of them. Patching the future construct (developed by Henry Baker and myself) into Scheme was another place where things got even stranger. Since then Steele is trying to do better in his Fortress language.
I suppose that you have realized by now that there is no good way using the old text books and papers to write down the denotational semantics of true delayed evaluation (i.e. the version without the strange hack in Scheme). This is one reason that modern treatments of compostional denotational semantics use the Actor model.
Regards,--Carl Hewitt 01:22, 22 November 2005 (UTC)
Re: I suppose that you have realized by now... I'm sorry I don't believe anything of what you've said. You dismiss both Steele and Sussman as hackers, suggesting their approach was strange. Presumptuous to say the least.--CSTAR 02:42, 22 November 2005 (UTC)
It seems that you are unaware of the honorable tradition of being a "hacker" at MIT. So I would never say as you did in the log that Sussman and Steele are "just" hackers. Also do I take from your remarks that you think the semantics of delayed evaluation in Scheme are fine just as you have described them?
Regards,--Carl Hewitt 03:06, 22 November 2005 (UTC)

[edit] Rewrite proposal

I hadn't looked at this article since before CH started editing, and was provoked to do so by CSTAR's comments at Wikipedia:Articles for deletion/Scientific Community Metaphor. Although CH started with an article that was not in very good shape, the article as it now stands is so imbalanced that I think WP is worse off than it was. In its defence, it was interesting for me to read some of the comments of Will Clinger from his PhD thesis (although I think the article was cobbled together with so little regard for readers that only experts will appreciate them) and there is some good content provided in the Early history of denotational semantics section. The main problems are:

  1. While Will Clinger's work has some recognition in the area, mostly, I think, through Kohei Honda's discussion of his work, he is not remotely a current authority on the subject (disclosure: I know Will, although not well, and like his work. This comment is not a reflection on his ability, only on what he has chosen to work on);
    While it is true that Clinger has not recently worked on denotational semantics, his dissertation is still a classic work on the subject and remains state of the art in terms of published literature. It is widely know by researchers in the field. Recent work builds on it and will be published soon.--Carl Hewitt 18:59, 21 November 2005 (UTC)
    • See the topic below What should this article be about? --- Charles Stewart 22:12, 22 November 2005 (UTC)
  2. I had never heard of unbounded nondeterminism as a particular problem in the semantics of concurrency: from what I can gather from this article and that, it seems to be an issue in the expressiveness of particular languages for concurrency, but present no special difficulties for models. That a semantics can be used to show presence or absence of this property is the kind of thing worth including, but it looks to me that a presence in this article beyond that is unjustified.
    It turns out that unbounded nondeterminism is a critical issue for the semantics of concurrency. Noted pioneers in the field, e.g. Dijkstra, got it wrong and influenced others. With the advent of massive concurrency (Web Services and many-core) computer architectures, unbounded nondeterminism is becoming even more critical.--Carl Hewitt 10:33, 21 November 2005 (UTC)
    • I've been in correspondence with Will Clinger on this point, and I'm persuaded that it is worth documenting. But note what I say in the topic What should this article be about? below --- Charles Stewart 22:12, 22 November 2005 (UTC)
  3. Relatively little in what CH wrote is about the denotational semantics of concurrency as a topic in its own right. The kind of things I would expect to see arise in such a section are: powerdomains, event structures, computational adequacy theorems, full abstraction theorems, game semantics, and nondeterministic operators in the lambda calculus. This list, no doubt, shows my biases, but the tiny overlap with the contents CH provides sounds an alarm bell: only the first item from my list, as far as I can see, actually appears. The bibliography is worse still.
    The article discusses power domains for Actor model diagrams which are the most modern published treatment of computational adequacy in terms event structures, nondeterminism, and indeterminacy. It turns out that full abstraction is still a controversial topic: whose treatment are you thinking of reporting? A section on game semantics would be a useful addition. There will be additional publications on denotational semantics this summer which will require the article to be revised in any case. What additions would you like to make to the bibliography?--Carl Hewitt 10:39, 21 November 2005 (UTC)
    • Full abstraction is not controversial is the sense that it is a widely recognised property of a denotational semantics that has an uncontroversial formulation and that is widely recognised to be hard to do in several cases. There is a controversy over whether fully abstract models are the best models for providing semantics of programming languages. By a treatment of a topic, I mean that the topic should be introduced in a manner that not only experts will grasp. Even the treatment of power domains does not really say what they are; with other topics, such as event structures, the reader is left completely in the dark. --- Charles Stewart 22:12, 22 November 2005 (UTC)
I generally agree with your sentiments. However, in this case the devil may be in the details. E.g., what would you say is an uncontroversial formulation of full abstraction?
With respect to event structures the article states:
The augmented Actor event diagrams [see Actor model theory] form a partially ordered set < Diagrams, ≤ > from which to construct the power domain P[Diagrams] (see the section on Power Domains below). The augmented diagrams are partial computation histories representing "snapshots" [relative to some frame of reference] of a computation on its way to being completed. For x,y∈Diagrams, x≤y means x is a stage the computation could go through on its way to y. The completed elements of Diagrams represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of Diagrams [see William Wadge 1979]. Concretely, the completed elements are those having non pending events. Intuitively, Diagrams is not ω-complete because there exist increasing sequences of finite partial computations
x0 ≤ x1 ≤ x2 ≤ x3 ≤ ...
in which some pending event remains pending forever while the number of realized events grows without bound, contrary to the requirement of finite [arrival] delay. Such a sequence cannot have a limit, because any limit would represent a completed nonterminating computation in which an event is still pending.
How can we improve?
Regards,--Carl Hewitt 22:47, 22 November 2005 (UTC)

In defence of CH, he is not a semanticist, and is documenting what he knows about. But the defence is rather weak when seen in the context of CH's pattern of editing elsewhere: the article is being used inappropriately to push the actor model, at the expense of balanced coverage of the topic at hand.

It would not be an improvement in the article to replace modern treatments and results with old obsolete ones.--Carl Hewitt 18:59, 21 November 2005 (UTC)

It's probably best to start fresh: I propose we start a new article and userfy the current article (ie. move it into CH's user space). --- Charles Stewart 21:06, 17 November 2005 (UTC)

I've changed my mind about starting from scratch, though the article needs heavy surgery. --- Charles Stewart 22:12, 22 November 2005 (UTC)

[edit] What should this article be about?

I think that this article should be mainly about two things:

  • The development of mathematical structures that are rich enough to be used in denotational semantics. See a class outline by Alex Simpson for what kind of thing I mean here;
  • The cataloging of features of computation and programming languages that are problematic or significant for denotational semantics.

When I said above that the problem of unbounded nondeterminism present no special difficulties for models, I meant that it did not require subject-changing innovations in the kinds of mathematical structures used to give models. IMO, it's these kind of innovations that constitute the classic works of the topic. These works by no means exhaust good work in denotational semantics, but they do help you distinguish work on the core of denotational semantics, which is ultimately directed at achieving such progress, from applied work in denotational semantics that attempts to make use of these refined techniques. Furthermore they tend to get sigtnificant citations by both classes of work. Apart from the citation by Kohei Honda, I don't see any citations by anyone I recognise as a worker on the structures half of the subject. --- Charles Stewart 22:12, 22 November 2005 (UTC)

Thanks for your comments.
Robin Milner has favorably cited Clinger's work. Also I can tell you that most participants at the recent CONCUR conference have at least passing acquaintance with this material. Also the participants were generally of the opinion that programming languages that are not concurrent are rapidly becoming obsolete. Concurrency lies at the core of modern day denotational semantics.
Regards,--Carl Hewitt 22:37, 22 November 2005 (UTC)

[edit] "Example of factorial function" needs explanation

I think the first example is insufficiently explained. Is the "factorial" that appears in graph(factorial) and Fix_factorial the same quantity? What is the convention for representing partial functions as sets of pairs? (e.g. I think it would help to say that domain values for which the function is undefined are simply not included in the set, if this is the case) What is a fix point operator and why is Fix_factorial one? What does omega-complete mean? I think it's a good idea to have a simple example like this early on, but it should be fleshed out a bit (and I'm not qualified to do it). A5 21:56, 21 November 2005 (UTC)

Thanks for your comments and questions. I have rewritten the section to make it more readable. Please take a look and get back with more questions and comments. This is how we improve articles on the Wikipedia.
In answer to your first question, in mathematics the same name invariable means the same thing so that factorial is the same in graph(factorial) and Fixfactorial. Hopefully your other questions are answered in the rewritten section.
Regards,--Carl Hewitt 06:56, 22 November 2005 (UTC)

[edit] Apology to CSTAR

I would like to apologize to CSTAR for the tone of 2 of my remarks in our recent discussion above on delayed evaluation:

  1. I suppose that you have realized by now ...
  2. I don't think that you quite understand the problem here ...

These remarks were not collegial and I will strive to do better in the future.

Regards,--Carl Hewitt 06:46, 24 November 2005 (UTC)