Re: builtins operating on rif:iri

Sandro Hawke wrote:
>> 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?

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)

yes

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

Did you mean List(1 2)?

> 
> 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)

Yes

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

No. eg:foo is mapped to the same object in every interpretation. Let's
call this object a. And let's say eg:foo is mapped to b. Then
list(eg:foo eg:bar) represents the sequence (a,b). And certainly the
object a appears in the first position of this sequence.

So, this should be a positive entailment test.

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

Correct.


Best, Jos

> 
> Is that right??
> 
>      -- Sandro
> 

-- 
+43 1 58801 18470        debruijn@inf.unibz.it

Jos de Bruijn,        http://www.debruijn.net/
----------------------------------------------
Many would be cowards if they had courage
enough.
  - Thomas Fuller