Re: Apparent inconsistency regarding equality in RIF-PRD

From: Christian De Sainte Marie <csma@fr.ibm.com>
Date: Mon, 9 Jul 2012 17:54:04 +0200
To: Jesse Weaver <weavej3@rpi.edu>

Message-ID: <OF6538E5F9.5F83353C-ONC1257A33.004114FC-C1257A36.00575C8F@fr.ibm.com>
Hi Jesse,

The semantics of equality formulas, in PRD, is not specified wrt a state
of the fact base, but wrt the value of the terms on both side of the
equality: t1 = t2 iff sigma(t1) and sigma(t2) have the same value. So, no
need for equality facts, and no problem with transitivity, symetry or
reflexivity.

The case of lists is missing, though (since uninterpreted (logically
defined) terms are not allowed in RIF-PRD, a ground term either has an
atomic value or it is a ground list): I believe this is oversight, and the
intent was that ground lists List(a1...an) = List(b1..bm) iff n=m and
Ai=bi for all i.

I will propose a correction/clarification in the 2nd edition.

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,
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 Monday, 9 July 2012 15:54:58 UTC

This archive was generated by hypermail 2.3.1 : Tuesday, 6 January 2015 21:48:00 UTC