******************************************************************** ELECTRONIC NEWSLETTER ON REASONING ABOUT ACTIONS AND CHANGE Issue 98079 Editor: Erik Sandewall 28.10.1998 Back issues available at http://www.ida.liu.se/ext/etai/rac/ ******************************************************************** ********* TODAY ********* Today's issue contains Graham White's answer to questions by Andreas Herzig regarding his ETAI submitted article. Concerning the reference articles for current approaches to actions and change, we have received four such articles, and two more are expected. Since these are intended for a concise presentation of current approaches, and not for the publication of new results, review comments ought to refer to their adequacy for the stated purpose: readability and understandability, consistency with previouly published articles, etc. In addition, of course, the reference articles may be used for a continuation of the discussion on comparison of approaches to actions and change, that started already at the NRAC workshop at last year's IJCAI. Hopefully, the reference articles will make it possible to discuss in more precise terms what expressivity is included or not included in various approaches, and how and to what extent one can be translated into the other. Contributions are welcome! ********* 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: The Author | TO: Andreas Herzig -------------------------------------------------------- Dear Andreas, Thank you for your comments on my paper. I'll try to respond in order. > > In my opinion all these attemps have failed in the sense that the only > thing they can handle within LL is the simplest case: deterministic actions, I can handle non-deterministic actions; all you need is the additive connectives. If you have linear logic terms $a_1$ and $a_2$, each representing an action, then the term $a_1 \& a_2$ represents the action which nondeterministically executes either $a_1$ or $a_2$. > no state constraints, I haven't talked much about state constraints because I am a little sceptical about the prominent role given to them in the current literature: I do not believe that the ramification behaviour can be given simply by the state constraints. In this respect, my position is somewhat similar to that of Deneker et al. in the article the recently submitted to ETAI (http://www.ep.liu.se/ea/cis/1998/007) However, if you do want state constraints (if, for example, you want to do other things than simply generate the ramification behaviour from them), they can be added to my approach, and I've shown how to treat a simple case in my reply to Tom Costello. However, there are important conceptual (not mathematical) issues to be resolved first: in particular, there is an obvious distinction between state constraints which are required to hold *during* the ramification process, or only *at the end* of it. > knowledge about the initial situation only. I can deal with that too. In my "Actions, Ramification, and Linear Modalities", QMW Technical Report no. 749 (1998), at ftp://ftp.dcs.qmw.ac.uk/pub/applied_logic/graham/ramMod.ps, I show that every valid inference in the logic corresponds to an evolution of the system according to the intended semantics, and vice versa; so if we carry out a proof search starting with partial data in either or both of the initial or final situations or in the action (representing the partiality be the appropriate quantifiers: $\forall$ before the entailment, $\exists$ after it) then, if that proof search terminates, the corresponding entailment will correspond to a correct evolution of the system. > They didn't succeed in going beyond that without violating the spirit of LL: > they all introduced extra concepts that were used to constrain deduction in > one way or another. I think you have to distinguish here between "extra concepts ... used to constrain deduction" and genuine extensions of the system. I have tried to show (in "Actions, Ramification, and Linear Modalities") that my extra connectives have both a good proof theory and a semantics. > In the present paper it is time which is made explicit in the encoding > of reasoning about action problems (section 3, 3rd paragraph). But I only put the explicit time in to make the example conceptually clearer. You don't need it. > But I would expect time to be implicit in a LL account of reasoning about > actions: it is the implication of LL which - if we take Girard seriously - > should be able capture the dynamics, and not formulas such as > ``time(0) & occurs(lift)(0)''. There seem to be other extra concepts, such > as grouping of those sequent rules corresponding to an action (see below). This is, of course, and important point, and I more or less agree with it. However, I want to make one caveat: you do seem to need to represent some notion of synchronisation. That is, you need to say that a particular tensor product of fluent formulae represents a particular situation, *and that these are all of the fluents in that situation*. Otherwise you can't express universally quantified assertions (for example, if you want to say ``all the blocks are on the table'' in a given situation). I've gone into this in ``Golog and Linear Logic'', QMW Department of Computer Science Technical Report (December 1997), at ftp://ftp.dcs.qmw.ac.uk/applied_logic/graham/golog.ps. > This is my main criticism. What follows are more detailed comments. > > Sections 2.2. The two-blocks Example 1 is similar to Lifschitz' two > switches example, I suppose. (Btw. on p.4, line 8 should be dropped.) > I guess circumscription doesn't give *the* solution, but several ones, > one of which you give in the table. (Btw. one b_1 should be b_2 there.) No, circumscription (with the indicated fluents) only gives one solution, and that solution is clearly not the intended one. So it's not similar to Lifschitz' two switches example in that respect. > Sections 2.3. I don't understand the difference between Example 1 and > Examples 2 and 3. Where does the `support' concept come from? I need more > comments here. Ah. Sorry about that: I forgot to give enough context for the quote from the referee. The point is that you can try to fix up the state constraints by saying that a ball is either supported directly, or hangs from a directly supported ball. > Section 2.4. The expression `` equivalent in first order logic to theory T, > but expressed in L' '' is inaccurate. I don't know whether you refer to > logical equivalence in the union of the two languages L and L' under the > translation theory of Table 3, or rather to interpretability as in the > end of the subsection. Interpretablity. Sorry about the ambiguity. > Section 3.2. You claim your rewrite rules for the two blocks theory is > `local data', in the sense that they remain valid `if we introduce new > types of cause'. But what about introducing an action such as cutting or > removing the string between the blocks? Then the rewrite rules `linking' > the blocks do not hold any longer. In that case, of course, we'd have to introduce new fluents, since we don't, in this example, have a representation for whether the string is intact or not, and we'd consequently have to change the rewrite rules somewhat. > Section 4.1. Wy don't you mention the cut rule here? (you talk about its > elimination in the proof of Proposition 1). In the statement of Proposion 1, > you don't say what ACI is. Well, I can prove cut elimination (in the tech report ``Actions, Ramification, and Linear Modalities''), so the system without cut is equivalent to the system with cut. Cut elimination is important, because, if you have it, you can show that the only proofs of the sequents that encode actions correspond to the changes that those actions produce; that is, it says that the linear logic connectives have their intuitive meaning. This is a theme in a tradition in the proof theory of intuitionism, starting with Martin-Lof; the question is, can you understand the logical connectives simply by their role in proofs? And the answer is, yes you can, *if* the system satisfies cut elimination: because then we only need finite data to decide whether we can apply a rule or not. But the cut rule breaks this, because we can apply it with *any* cut formula, which is an unbounded totality. So systems without cut can be understood, in some way, finitely, whereas systems with cut can't. > If you have cut, how can composition of rewrites be a problem? Cut is just > doing that job, viz. chaining sequents. We need composition of rewrites in order to be able to prove cut elimination. > 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. 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. > This means that there is a > new concept that is exterior to LL. (I think the problem of termination of > sequences is similar.) > > Section 4.2. I don't understand how the introduction of modal operators > solves the above problem. I say more about this in ``Actions, Ramifications, and Linear Modalities'', but I can write more about this if you still find this mystifying. > In the basic rewrite rule of Definition 1, I suppose the LL `times' operator > is rather an ACI bullet. > > I found it difficult to understand the exposition on termination. I suppose it is a bit compressed. I'm intending the paper as a non-technical guide to the more technical results (which are mostly in ``Actions, Ramification, and Linear Modalities''), but I agree with you that some parts of it might have left the technical details out a bit too enthusiastically. > I suppose termination refers to termination of a rewrite sequence > corresponding to an action. In the rule, the notation $A - A_i$ has > not explained. What is a `state' $A_i$? Here you can treat it as a term of the metatheory. We start with atomic terms representing basic fluents; state propositions will then be combinations of them using $\otimes$ (and you can, in fact, use $\oplus$ as well, which will give you a notion of disjunctive states). The rewrite operation will then take state propositions to state propositions. Provided you start with atomic terms, and only combine them in the above ways, you can then prove cut elimination. (In ``Actions, Ramifications, and Linear Modalities'' I do it rather differently, and I have a representation within the logic for state terms; but you don't need to do that.) Anyway, I hope this helps. Thanks again for your questions. Graham White ******************************************************************** 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/actions/njl/ ********************************************************************