Re: Apparent incompleteness of semantics for firing rules in RIF-PRD

Hi Jesse,

Jesse Weaver <weavej3@rpi.edu> wrote on 05/07/2012 22:05:51:
> 
> It appears that the operational semantics of RIF-PRD are 
> incompleteness wrt firing rules.  Consider a set of facts \Phi = { 
> a#c , b#c } which represents a state of the fact base.  Consider the
> following rule:
> 
> Forall ?x ?y (
> If And( ?x#c ?y#c )
> Then Do( (?v ?x[p->?v]) ?y[p->?v] ) )
> 
> The substitution \sigma = { <?x, a> , <?y, b> } matches condition 
> formula And( ?x#c ?y#c ) to \Phi.  Therefore, by definition of 
> matching rule instance (section 4.2.3), the following is a matching 
> rule instance of the previous rule:
> 
> If And( a#c b#c )
> Then Do( (?v a[p->?v]) b[p->?v] ) )
> 
> Suppose that the conflict resolution strategy selects only this rule
> instance for firing.  Then by definition of RIF-PRD production rule 
> system (section 4.2.4), the ground atomic actions derived from the 
> rule instance's action block are executed in sequence to transit to 
> the next state.  From definition of action instance (section 4.2.3),
> the action instance is derived by extending \sigma to another ground
> substitution \sigma* = { <?x, a> , <?y, b> , <?v, d> } where d is a 
> constant such that a[p->d] \in \Phi.  However, there exists no 
> constant d such that a[p->d] \in \Phi.  Therefore, it is impossible 
> to derive an action instance for the given rule instance, and it 
> appears that such a case has an undefined operational semantics.
> 
> What I wish to know is: have I correctly determined an 
> incompleteness in the semantics, and if so, what should the 
> operational semantics be in this case?

I think this is on purpose: the rule is valid but does not have a 
semantics according to RIF-PRD if used in a context where the action 
variables cannot be bound.

I started a discussion on the WG mailing list, though.

> (Also, note that the definition of action instance requires that d 
> be a constant, which seems overly restrictive.  What if a[p->List()]
> \in \Phi, which is allowed by definition of frame atomic formula 
> (section 2.1.2) and definition of term (section 2.1.1).)

Yes, you are right, this is a mistake. The second bullet in the definition 
of action instance should read:
if vi is assigned the value of a frame's slot by the action variable 
declaration: (vi o[s->vi]), then σ(vi) is a ground term such that the 
subtitution σ matches the frame formula o[s->vi] to w. 

I will propose a correction in the revised edition.

Thanx again for your comments.

Cheers,

Christian

IBM
9 rue de Verdun
94253 - Gentilly cedex - FRANCE
Tel./Fax: +33 1 49 08 29 81

Sauf indication contraire ci-dessus:/ Unless stated otherwise above:
Compagnie IBM France
Si?ge Social : 17 avenue de l'Europe, 92275 Bois-Colombes Cedex
RCS Nanterre 552 118 465
Forme Sociale : S.A.S.
Capital Social : 645.605.931,30 €
SIREN/SIRET : 552 118 465 03644 - Code NAF 6202A