- From: Christian De Sainte Marie <csma@fr.ibm.com>
- Date: Fri, 6 Jul 2012 11:14:10 +0200
- To: Jesse Weaver <weavej3@rpi.edu>
- 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
- Message-ID: <OF847F15FF.3E34ED4A-ONC1257A33.0031E4E2-C1257A33.0032BFC0@fr.ibm.com>
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
Received on Friday, 6 July 2012 09:15:00 UTC