Re: Apparent inconsistency regarding equality in RIF-PRD

Hi Jesse,

When I wrote that I would examine your comments, I meant that I would 
check wrt the spec, which I did not read since a couple months, and think 
a little bit before responding; but I expect to have a full answer today, 
or Monday at the latest...

And, anyway, I committed to produce a draft of the revised edition by 
Tuesday, so, in the worst case, you will not have to wait for a very long 
time :-)

As far as I can see from where I stand now, you are right re the 
membership assertion (although your example rule is not well-formed :-) 
and re the case of the unbindable action variable; and you are wrong re 
equality (although I have to check whether and how the value of a constant 
is defined, since matching an equality is defined with respect to it in 
PRD, see definition of matching substitution, in 2.2.1).

Re membership, I have no doubt that it is pure oversight and that the 
intent was that a class membership assertion would assert all the class 
membership according to the class hierarchy. I just have to find out how 
that was supposed to work, and repair the text accordingly.

Re the unbindable action variable, I have to check the discussions that we 
had about action variables binding before proposing a solution.

I hope this helps. More later...

Cheers,

Christian

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




From:   Jesse Weaver <weavej3@rpi.edu>
To:     Christian De Sainte Marie/France/IBM@IBMFR
Cc:     Adrian.Paschke@gmx.de, Ankesh <ankesh@cs.rpi.edu>, 
cawelty@gmail.com, public-rif-wg@w3.org, sandro@w3.org, 
team-rif-chairs@w3.org
Date:   06/07/2012 16:40
Subject:        Re: Apparent inconsistency regarding equality in RIF-PRD



Hi Christian.

Thanks for responding.  I am working on my dissertation in which I use the 
operational semantics of RIF-PRD as the underpinnings for some 
formalization.  Are there any brief answers that can be given at this time 
for the three problems?  Otherwise, I will have to resolve it in my own 
way, but I would prefer to align with whatever the revised standard will 
specify.

Jesse Weaver
Ph.D. Student, Patroon Fellow
Tetherless World Constellation
Rensselaer Polytechnic Institute
http://www.cs.rpi.edu/~weavej3/index.xhtml

On Jul 6, 2012, at 5:14 AM, Christian De Sainte Marie wrote:

Hi Jesse, 

Thanx for the feedback (which could not be more appropriately timed: 
indeed, we are preparing a revised edition to correct the errors found in 
the first edition :-) 

I will examine the three problems that you have found re equality, 
subclasses and action variables and let you know. 

Cheers, 

Christian 

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




From:        Jesse Weaver <weavej3@rpi.edu> 
To:        team-rif-chairs@w3.org 
Cc:        cawelty@gmail.com, Christian De Sainte Marie/France/IBM@IBMFR, 
sandro@w3.org, Ankesh <ankesh@cs.rpi.edu>, public-rif-wg@w3.org, 
Adrian.Paschke@gmx.de 
Date:        05/07/2012 21:22 
Subject:        Apparent inconsistency regarding equality in RIF-PRD 



RIF Chairs, 

In short, if a=b and b=c, then intuitively, it should hold that a=c, but 
the operational semantics do not seem to ensure such. 

By definition of atomic formula (section 2.1.2) and informal definition of 
fact (section 2.2.2), a set of facts may include ground, equality, atomic 
formulas.  Consider then the following set of facts where t_1, t_2, and 
t_3 are different ground terms: \Phi = {t_1=t_2, t_2=t_3}.  By 
(operational) definition of state of the fact base (section 2.2.2), \Phi 
represents a state of the fact base.  According to the interpretation of 
condition formulas (section 12.2), I_{truth}(I(x=y)) iff I(x)=I(y). 
Intuitively, then, it should hold that since t_1=t_2 \in \Phi implies 
I(t_1)=I(t_2), and since t_2=t_3 \in \Phi implies I(t_2)=I(t_3), by 
transitivity of mathematical equality, I(t_1)=I(t_3).  However, there 
exists no ground substitution that matches t_1=t_3 to \Phi, and since 
ground, equality, atomic formulas cannot be inferred by rules (they are 
not syntactically allowed as the target of an assert action; see 
definition of atomic action, section 3.1.1), then there is also no 
subsequent state in which there exists a ground substitution that matches 
t_1=t_3 to the state's associated set of facts.  This seems like an 
inconsistency. 

A similar argument can be made for the simpler (but perhaps less 
interesting and less obvious) case of when \Phi = {t_1=t_2}, where t_1 and 
t_2 are different ground terms.  Then no ground substitution exists that 
matches t_2=t_1 to \Phi or to any subsequently inferred sets of facts. 

I can think of a number of ways to resolve this apparent inconsistency, 
but I wish to know: have I correctly determined an inconsistency, and if 
so, what were the intended (consistent) semantics (or definitions)? 

Jesse Weaver 
Ph.D. Student, Patroon Fellow 
Tetherless World Constellation 
Rensselaer Polytechnic Institute 
http://www.cs.rpi.edu/~weavej3/index.xhtml 



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 



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