Concerning RIF Erratum 16.2

Hi Christian.

I have occasionally been checking on the erratum for RIF-PRD.  I still  
have some concerns about erratum 16.2.  If these concerns are  
unfounded, please let me know where my misunderstanding lies.  If I  
have overlooked available answers to my questions, please direct me  
toward them.

The proposed solution to http://www.w3.org/2005/rules/wiki/Errata#Erratum_16.2 
  is to add the following condition in the definition of State of the  
Fact Base (SFB): "for every equality term t1=t2 in \Phi, if t1 and t2  
are, both, constants in the symbol spaces that are data types, then  
they have the same value;".  This seems like a partial solution, since  
it applies only to cases in which t1 and t2 are constants in symbol  
spaces that are data types.  What if the equality statement has a term  
that is not a constant (like a list), or a constant that is not in the  
symbol space of a data type?  Should such facts be allowed in a SFB?   
If so, shouldn't there be more conditions on SFB to ensure symmetry  
and transitivity of equality?

For example, the new condition basically says that explicit facts in a  
SFB pertaining to equality of "datatyped" constants must agree with  
how these equality statements would be evaluated independent of the  
SFB.  So one can no longer say that 1=2.  However, one could still  
form the following SFB:

1=_x
2=_x
_x=:iri_representing_1
2=:iri_representing_2
3=List()

There appear to be a few problems here.  Using the new definition of  
matching substitution from http://www.w3.org/2005/rules/wiki/Errata#Erratum_16.3 
  ,

1. Effective equality of unequal constants.  And(1=?v ?v=2) matches  
the SFB, but 1=2 does not.

2. Effective inequality of equal constants by lack of transitivity.   
And(1=?v ?v=:iri_representing_1) matches the SFB, but  
1=:iri_representing_1 does not.

3. Effective inequality of equal constants by lack of symmetry.   
2=:iri_representing_2 matches the SFB, but :iri_representing_2=2 does  
not.

4. Non-intuitive equality.  3=List() matches the SFB, but should not.

The first three conflict with the model-theoretic semantics which  
interpret equality statements as logical equality, and thus symmetry  
and transitivity should apply.  In general, all of them seem to  
conflict with basic intuition.

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