Re: builtins operating on rif:iri

> Sandro Hawke wrote:
> >>> Oh, hmmm.  Now I realize I'm confused and worried about using rif:iri
> >>> (or rif:local) with builtins.
> >>>
> >>> Does:
> >>>          ex:foo = 1
> >>> ential:
> >>>          external(numeric-equal(ex:foo, 1))
> >>> ?
> >> Yes. ex:foo is indistinguishable from 1 after you equated them.
> > 
> > Okay, that's what I would have expected.
> > 
> > But that means that before I equate them, the truth value of that
> > external predicate formula is 'unspecified'....  (It can't be 'false' or
> 
> Yes (in those interpretations in which ex:foo does not denote a number).
> 
> > the logic would be non-monotonic.)  Similarly,
> > external(pred:isInteger(eg:bar)) is 'unspecified' until/unless eg:bar
> > ends up equated with some data value, or we otherwise learn a lot more
> > about it.
> 
> No. in every interpretation, the truth value of pred:isInteger(eg:bar)
> is known, because it is known in that particular interpretation whether
> eg:bar denotes an integer. However, since eg:bar does not denote an
> integer in every interpretation, pred:isInteger(eg:bar) if not entailed.

Hmmmm.  Okay.   (I think I understand.)

> > So that means list-contains/member will be 'unspecified' a lot of the
> > time as well; in practice, it will never be false when there are
> > 'objects' in the list.  For example:
> > 
> >     member(eg:foo, list(eg:foo eg:bar))
> > 
> > is be true, but:
> > 
> >     member(eg:baz, list(eg:foo eg:bar))
> > 
> > is 'unspecified' unless eg:foo, eg:bar, and eg:baz are all equated to
> > data values --- and in practice, if you're using them as frame/objects,
> > you would never equate them to data values.  (You could also get a false
> > via a combination to OWL, from which you could learn they were pairwise
> > distinct.)
> 
> Same as above.  The truth value is specified in every particular
> interpretation.

... and since it's not the same in every interpretation, it's not
entailed.   I think I'm getting that.  So...

positive-entailment
PREMISE:    (empty)
CONCLUSION: member(eg:foo, list(eg:foo eg:bar))

negative-entailment
PREMISE:    (empty)
CONCLUSION: member(eg:baz, list(eg:foo eg:bar))

positive-entailment
PREMISE:    eg:baz = eg:bar
CONCLUSION: member(eg:baz, list(eg:foo eg:bar))

Agreed?

> > All the list operations that compare items have a form of this behavior.
> > For instance:
> > 
> >     index-of(list(eg:foo eg:bar), eg:foo)
> > 
> > is 'unspecified', unless we can determine, somehow, whether
> > eg:foo=eg:bar.
> >
> > I guess this unfortunate behavior is inescapable given our no-CWA,
> > no-UNA style of Core.
> > 
> > The effect is that it basically doesn't work to think of 'objects' as
> > items in lists in Core or BLD.  (Does this problem go away in PRD?)  
> > 
> > The two options I can think  of:
> > 
> >    1. Forbid 'objects' in lists; make lists just be lists of data
> >       values.  Given this, we could even define a mapping to a lexical
> >       space for lists, making them be another datatype.  (Hey, we could
> >       generalize that, and make it another Rec-track document like
> >       rdf:text.  Hey, why are you hitting me?  :-)
> > 
> >    2. Just understand that they don't really work for 'objects', even
> >       though the machinery is there.
> > 
> > I suspect option (2) is better, because it allows lists to grow more
> > useful in other dialects -- possibly PRD, and certainly a
> > logic-programming dialect with CWA/UNA.
> 
> As I said, the truth value is going to be specified in every
> interpretation, so I believe we do not have a problem.

Okay, so then I think we have these two tests:

positive-entailment
PREMISE:    eg:bar = 1
            eg:foo = 2
CONCLUSION: index-of(list(eg:foo eg:bar), eg:foo) = list(1)

positive-entailment
PREMISE:    eg:bar = eg:foo
CONCLUSION: index-of(list(eg:foo eg:bar), eg:foo) = list(1 1)

But what if the premise is empty?  I'm thinking that none of these
entailments would hold...  (so these would be valid tests)....

negative-entailment
PREMISE:    
CONCLUSION: index-of(list(eg:foo eg:bar), eg:foo) = list(1 1)

negative-entailment
PREMISE:    
CONCLUSION: index-of(list(eg:foo eg:bar), eg:foo) = list(1)

negative-entailment
PREMISE:    
CONCLUSION: index-of(list(eg:foo eg:bar), eg:foo) = list()

Is that right??

     -- Sandro

Received on Thursday, 23 April 2009 16:36:53 UTC