******************************************************************** ELECTRONIC NEWSLETTER ON REASONING ABOUT ACTIONS AND CHANGE Issue 99009 Editor: Erik Sandewall 4.4.1999 Back issues available at http://www.ida.liu.se/ext/etai/rac/ ******************************************************************** ********* TODAY ********* The two Anonymous Referees for Graham White's article both recommded that the contribution be declined. Today the author answers to their critique. (The referees will be asked to comment on the answer). Also, Ray Reiter answers to John McCarthy's 'grumble' and to Pat Hayes's comments on nomenclature that that followed it. ********* ETAI PUBLICATIONS ********* --- DISCUSSION ABOUT RECEIVED ARTICLES --- The following debate contributions (questions, answers, or comments) have been received for articles that have been submitted to the ETAI and which are presently subject of discussion. To see the full context, for example, to see the question that a given answer refers to, or to see the article itself or its summary, please use the web-page version of this Newsletter. ======================================================== | AUTHOR: Graham White | TITLE: Simulation, Ramification, and Linear Logic | PAPER: http://www.ep.liu.se/ea/cis/1998/011/ | REVIEW: http://www.ida.liu.se/ext/etai/ra/rac/012/ ======================================================== -------------------------------------------------------- | FROM: Graham White -------------------------------------------------------- Anonymous Referee 1 wrote: >>1. Are the results of the article, as specified in the summary, of >> significant interest for researchers in our area? >> > No. The main objective of the paper is to propose a solution to the > Frame Problem which satisfies certain properties, which are > convincingly argued for. My only but serious concern is that existing > solutions seem to satisfy all of the requirements and that the author > fails to argue for merits of his approach in comparison. In particular > Reiter's theory [1] of generating successor state axioms from simple > effect axioms fits perfectly the author's desiderata. No, it doesn't. One of my criteria is that the data for the problem should be what I describe as local, or, as Sandewall puts it (in a passage which I cite in the article), Consider applications where every scenario describes a number of separate but interconnected objects, different scenarios involve different configurations, and each action has its immediate effects on one or a few of the objects, but indirect effects on objects which are connected to the first ones, in some sense of the word `connected'. ... action laws should only specify the ``immediate'' or ``primary'' effects of the action, and logical inference should be used for tracing how some changes ``cause'' other changes across the structure of the configuration at hand. However, Reiter's account starts from a statement of what he and Pednault describe as "effect axioms" (p. 360 of Reiter's article), which give, for each action and each fluent, conditions under which that fluent positively or negatively affects the fluent. These conditions, because they talk about all fluent-action pairs rather than just the fluents which are immediately affected by the action, are not concerned with the immediate or primary effects of actions but all of them. Now Reiter's paper does not explicitly consider the ramification problem, and, if we do not have ramification, it is entirely reasonable to suppose that actions can be described by effect axioms: actions then have no effects but their immediate effects. And it is certainly true that, in the absence of ramification, Reiter's solution does satisfy my desiderata (or, at least, the ones that I give in Table 1, apart, of course, for the requirement that the effect axioms should be local, which has little content in the absence of ramification). But, I am talking about a case with ramification, so that Reiter's methods do not apply; if we allow the effect axioms to talk about all effects, instead of just the immediate ones, then there is essentially no distinction between immediate and non-immediate effects. Neither can we hope to derive the unrestricted effect axioms from the local ones using merely classical logic (this, of course, is the assumption in Reiter's article; the effect axioms are supposed to yield all of the effects, local or non-local, using classical deduction). Consider the following example: I move a block to a place L (this is the immediate effect of the action; the location of the block is changed). If the block is in a wet place, it becomes wet. (This is the description of how effects propagate). Location L is wet in the initial state. We want, of course, to conclude that the block becomes wet. However, in order to do this, we have to conclude that location L is wet, not in the initial state, but in the successor state. And we cannot conclude this by classical logic alone; considerations of examples like this (electrical circuits are a fruitful source) shows that, if we have a chain of propagating effects, we must, in general, solve the frame problem for the propagating causes up to stage i before we can know whether to apply the rules for the propagation to stage i+1. > ... And yet this work, > which is among today's most cited papers in the area of Reasoning About > Actions And Change, the author does not even mention, let alone compare > it to his own method. No, that's true, I don't, but I do cite Murray Shanahan's book Solving the Frame Problem, which does contain a very clear and accurate account, not only of Reiter's work, but also of the work of Pednault and others which led up to it. -------------------------------------------------------- | FROM: Graham White -------------------------------------------------------- Anonymous Referee 2 wrote: > My recommendation as regards the acceptance of this paper for > ETAI is no. Accordingly, I have perhaps to explain that. > Roughly speaking, my answer is no, because there is a very little > difference between the submitted and revised versions of the > paper. On the other hand, the remarks, especially those made by > Andreas Herzig, were quite important, and so they should be > seriously taken into account in the final version. I am not > going to be very detailed, but one example should illustrate this. > > Andreas writes: >> I guess this relates to my main criticism: in order to >> identify actions in proofs, you must group together sequences >> of rules related to the same action. > > Answer of Graham: >> No, not necessarily; if you look at the examples in >> `Actions, Ramification and Linear Modalities', you can see >> that you don't need to group rule applications together >> like this. Yes, in retrospect I agree that that was a little short. Here's a fuller account of my strategy with this. I give (on p. 10 of my article or so) a logical system which is an extension of linear logic by a modal operator \poss; the important rule for \poss is \Gamma |- A, \Delta -------------------- (*) \Gamma |- \poss A', \Delta where A' is obtained from A by a ramification transition. We must, however, add new rules to the system in order to be able to prove cut elimination: in particular, we must add the rule \Gamma, A' |- \poss B, \Delta ------------------------------ (**) \Gamma, A |- \poss B, \Delta where, again, A' is derived from A by a ramification transition. We then prove, as I have said, cut elimination for this system; as with most such proofs, the proof of cut elimination proceeds by rather elementary stages but is extremely long-winded (28 subcases or so). Now we can consider our representation of ramification and actions. We first describe our actions by their primary effects, namely by linear logic formulae of the form a' -o a'', where a' and a'' roughly correspond to Strips-like "delete lists" and "add lists", respectively. (They do not exactly correspond, because in order to be able to perform this action, the fluents in a' must be part of the initial situation, whereas the Strips delete list is only a list of the propositions which will be deleted if they are present.) Call an action, described like this, \alpha. Suppose also that we have a modality, \poss, which represents our ramification transitions. Now we can use the cut elimination theorem to show that the only valid proofs of a sequent of the form A, \alpha |- \poss B correspond to the following sequences of rule applications: i) Applications of (**) to A, yielding a state a'*A' (I represent the linear tensor product as *); ii) Applications of the rules for * and -o, yielding a sequent a''*A' |- \poss B; iii) Applications of either (*) or (**), corresponding in either case to a ramification transition from a''*A' to B. iv) The identity axiom on either a''*A' or B, depending which rules we have applied. One can also prove that, in many cases, one can apply the rules in any order one likes; one can formalise this in so-called permutability theorems, saying that the applications of certain rules can be permuted around each other. In the case of the rules applied in this proof, we are free to permute rule applications except for the obvious restriction, namely that if A does not actually contain the "delete list" a' of the action, then (**) must be applied before we apply the rule for -o. However, the proof-theoretic restrictions here correspond to our intuitive picture of what it is to perform an action in the presence of ramification: that is, the initial situation may first undergo a sequence of ramification transitions, then the action should accomplish its effects, and finally there should be a sequence of ramification transitions leading to the final situation. And in the "standard case", as it were, of the ramification scenario, we start with a situation A which is already stable under ramification transitions, so no initial applications of (**) are possible; we have no choice but to apply the rules for * and -o first. So, in order to represent action in this system, we do not have to impose any artificial grouping of rules: the proof theory gives us only the proofs that correspond to realistic sequences of action and ramification. ======================================================== | AUTHOR: Hector Levesque, Fiora Pirri, and Ray Reiter | TITLE: Foundations for the Situation Calculus | PAPER: http://www.ep.liu.se/ea/cis/1998/018/ | REVIEW: http://www.ida.liu.se/ext/etai/ra/rac/017/ ======================================================== -------------------------------------------------------- | FROM: Ray Reiter -------------------------------------------------------- John McCarthy wrote: "I have a grumble about the title of the article by Reiter, et. al. about situation calculus. It presents a particular system of the situation calculus, and therefore can't quite serve as a reference article." John's grumble about our title -- Foundations for the Situation Calculus -- is perhaps justified. A better title might have been "Foundations for a Calculus of Situations". If Erik will permit it, maybe we can make that change in the archival copy. Hector suggested that if only we were centred in Denmark, we could have used something like "Foundations for the Copenhagen Interpretation of the Situation Calculus". Too bad. -------------------------------------------------------- | FROM: Ray Reiter -------------------------------------------------------- Pat Hayes wrote: > In our community it > has happened to "situation", which is now widely taken to mean what Reiter > (et. al.) defines it to be, ie a finite sequence of actions, and its > cognates such as "situation calculus", which Reiter (et al) uses to refer > to a particular formalization developed at Toronto in the last decade. > Neither of these meanings are what these terms meant before Reiter changed > the language. ... > > Evidently what Reiter and his co-authors mean by "situation > calculus" isn't what John McCarthy invented. Regardless of the relative > merits of the calculi being referred to, a survey with that title should at > least clarify and respect the way that the terminology was used for about a > quarter of a century before Reiter re-defined it." We weren't entirely unaware of the different interpretations that can be made of the sitcalc. This from our abstract: > This article gives the logical foundations for the situations-as-histories > variant of the situation calculus, focusing on the following items: And this from the introduction: > The situation calculus (McCarthy [mccarthy63]) has long been a staple of > AI research, but only recently have there been attempts to carefully > axiomatize it. The variant described here has evolved in response to the > needs of the Cognitive Robotics Project at the University of Toronto, and its > foundations are now sufficiently developed to be gathered in one place. > That is what this paper sets out to do. The principal intuition captured by our axioms is that situations are histories -- finite sequences of primitive actions -- and we provide a binary constructor $do(a,s)$ denoting the action sequence obtained from the history $s$ by adding action $a$ to it. Other intuitions are certainly possible about the nature of situations. McCarthy and Hayes [mccarthyhayes69] saw them as "snapshots" of a world. For the purposes of representing narratives, McCarthy and Costello [costellomccarthy] wish to express that any number of actions may occur between a situation and its "successor", and therefore they do not appeal to a constructor like $do$. Pat and John's complaints raise some interesting issues about the importance of fully axiomatizing one's intuitions, something that the reasoning-about-actions community has been carefull to do. In their KR'98 paper, John and Tom Costello spelled out a different variant of the sitcalc to the "Toronto interpretation". To my knowledge, this is the only other fully specified sitcalc story, and now there is the possibility of looking at the pros and cons of the two approaches. It would be very interesting to see an axiomatization of the intuitions underlying the earlier "situations-as-snapshots" view. Probably other interpretations are possible of John's original sitcalc language, or extensions to it. Situations are not like the natural numbers; there seems to be no standard interpretation for them, and maybe this discussion will encourage others to step forward with alternative axiomatizations reflecting their intuitions. It remains to be seen whether, after the dust settles, something like "the Peano situation calculus" will emerge. -------------------------------------------------------- | FROM: John McCarthy -------------------------------------------------------- I see that I didn't make my grumble clear. I think the Reiter, et. al. system is one situation calculus formalism. I think that a reference article should be broader. ******************************************************************** This Newsletter is issued whenever there is new news, and is sent by automatic E-mail and without charge to a list of subscribers. To obtain or change a subscription, please send mail to the editor, erisa@ida.liu.se. Contributions are welcomed to the same address. Instructions for contributors and other additional information is found at: http://www.ida.liu.se/ext/etai/rac/ ********************************************************************