Graham White Simulation, Ramification, and Linear Logic.

[full text]

[msg to moderator] [debate procedure] [copyright]

Q1. Tom Costello (1.10):

Dear Graham

On page 2 of your article, "Simulation, Ramification, and Linear Logic" you suggest that effect axioms should have  Sigma₁  antecedents and frame axioms  Pi₁  antecedents, based on intuitions concerning locality. However, some local properties, such as there being no block in a certain place are expressed as  Pi₁  formulas, not as  Sigma₁  formulas, e.g.   A(b, ¬ at(b, l))  states that there is no block at location  l .

It seems to me that many effect axioms will have preconditions that say that the effect will occur in certain circumstances, unless there is something that prevents it. This is naturally written as a  Pi₁  formula. Consider the Blocksworld. One effect axiom there can be written

	Ab, l, s [ Ab' [¬ On(b', top(b), s)]  ^
	Ab' [¬ On(b', l, s)]  ^ top(b) =/ l ·->
	On(b, l, move(b, l, s))]

The left hand side side of this effect axiom is clearly equivalent to a  Pi₁  formula. It seems that many preconditions will have this form. This seems to contradict your intuitions that effect axioms have  Sigma₁  antecedents, and that sufficient conditions can be written in  Sigma₁ .

Yours,

Tom Costello

A1. Graham White (3.10):

Dear Tom,

Thanks for your question. It seems to me that I would want first of all to differentiate between your two formulations of the basic objection: i) "some local properties ... are expressed as  Pi_i  formulas", and ii) "many effect axioms will have preconditions that say that the effect will occur in certain circumstances, unless there is something that prevents it".

The first formulation has to do with local properties, which I take to be a fairly general, phenomenological notion; the second is to do with action preconditions, which is a notion internal to certain treatments of the frame problem. I'll deal with the second notion first.

My approach doesn't really use action preconditions per se. I don't have anything like a result function: given linear logic terms s and a representing a situation and an action, there may or may not be a valid inference of the form

s, a  |-  s'

where  s'  is also a situation term. So there are, in some sense, implicit action preconditions, but I don't represent them explicitly. I can deal with your example in my framework as follows. We have to introduce constraints on the space of situations, which I can do by having an extra pair of fluents, say good and bad, which say whether situations are physically realisable or not, and also having extra ramification transitions

(on(b, l) × on(b', l) × good)~>(on(b, l) × on(b', l) × bad)

for  b  and  b'  unequal.

We now apply the ramification machinery that I described: that is, we look for sequents corresponding to performing the action, followed by a terminating sequence of ramification transitions, such that we eventually end up with a situation of the form  X × good . All of this can be carried out with entirely local data, but the implicit preconditions are as you described. (I'm a bit unsure about the other part of the precondition, which says that you can't pick up a block with another block on top of it. My immediate response to that is "well, I can", but I'm not sure exactly what the impossibility is supposed to be here.)

Incidentally, I'm not at all sure about the phenomenological motivation of the concept of precondition. It seems to me that it conflates two quite distinct phenomena: the first is of actions (such as "opening the door") described by what Ryle called "success words", where it doesn't make sense to talk of performing them when they don't succeed. The other is of action descriptions such as "trying to open the door", where the possibility of failure is allowed for, and where we usually also have some intuitions about what happens in the case of failure. As Ryle (and I suppose also Wittgenstein) point out, the second case is rather more complex than the first, and probably needs a more elaborate description than simply giving preconditions. The first is the usual case in a great deal of everyday language, but, by its nature, does not need any explicit talk of preconditions (although one could, presumably, in many cases find implicit preconditions).

Your first objection is that many local concepts are in fact  Pi_i . This may be true, but what surely matters for my analysis is not local concepts per se, but the local concepts that are used in the sort of representation that I am describing. One probably also ought to distinguish between genuine universal quantification and universal quantifications which are, in some way, bounded. Most local concepts would, presumably, only be  Pi_i  in the latter sense, and it would be a sense corresponding to some natural means of verification -- I check, for example, that there is nothing on my desk by looking at the locations on my desk and verifying that they are all empty (and I can tell that they're empty just by looking at them). I certainly don't do it by finding all of the objects that there are and verifying that none of them is on my desk; and an analysis of "there is nothing on my desk" that reduces it to a $ Pi  _ 1$ of that sort is likely to be epistemologically misleading.

I hope this helps, anyway.

Graham

Q2. Andreas Herzig (3.10):

Dear Graham,

I appreciate the aims of the paper, viz. the discussion about the logical form and the proof-theoretic account of reasoning about actions as given in sections 1, 2.1.1, 2.4. I think that too little work has been done in the community on such fundamental issues.

Basically you propose Linear Logic (LL) as a proof theory to reason about actions, following Girard who claimed from the beginning that LL would be much better suited for reasoning about actions and change than any other logical system. LL people have tried to support that claim, such as Masseron et al. (LNCS 427, 1990) or Bidoit et al. (JLC, 1996). The same has been tried also by people coming from Bibel's linear connection method - see e.g. Bibel's IJCAI'97 invited lecture, as well as work of Fronhofer and Grosse et al. that Bibel cites; see also the subsequent discussion at

http://www.ida.liu.se/ext/etai/actions/deb/bibel/index.html

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, no state constraints, knowledge about the initial situation only. 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. 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 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 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₁  should be  b₂  there.)

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.

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.

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.

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.

If you have cut, how can composition of rewrites be a problem? Cut is just doing that job, viz. chaining sequents. 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. 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.

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 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 ?

A2. Graham White (28.10):

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₁  and  a₂ , each representing an action, then the term  a_1 ^ a₂  represents the action which nondeterministically executes either  a₁  or  a₂ .

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  b1  should be  b2  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-Löf; 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-Ai  has not explained. What is a `state'  Ai ?

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