Re: Semantics of explicit triple terms

Hi Enrico,

following our discussion today with the Semantics TF: you mentioned that 
the inclusion of triple terms involved a functional relationship, which 
in turns leads to negation.

Could you give an example where this kind of negation occurs -- which 
should therefore lead to a contradiction?

   pa

On 22/12/2023 15:13, Franconi Enrico wrote:
> I would like to discuss the semantic implications of having explicit 
> triple terms in the syntax, e.g.:
>
>     :id rdfx:occurrenceOf <<(:s :p :o )>> .
>
> and having triple occurrences as a shortcut:
>
>     < <<| id | :s :p :o>> :p1 :o1 >  . *—>*
>     :id rdfx:occurrenceOf <<(:s :p :o )>> .  < :id :p1 :o1 > .
>
>
> According to the classical semantics of RDF, we expect that:
>
>   * any term, and so a triple term, denotes a resource;
>
>   * in each model, a triple term denotes a /unique/ resource, and that
>     resource should be the denotation of /only that/ triple term;
>
>   * this is different from the denotation of /occurrences/ of triple
>     terms, which can be more than one for a triple term, and which can
>     be the occurrence of more than one triple term — namely,
>     rdfx:occurrenceOf is an arbitrary property;
>
>   * the denotation of a triple term depends on the denotation of its
>     components, and not on its syntactic representation;
>
>   * therefore, the relation between the denotation of a triple term
>     and the denotation of its components should be a bijection.
>
> Due to the choice of transparency of triple components, the following 
> reasoning patterns should hold:
>
>     Given the RDF graph:
>     :wed-1 rdfx:occurrenceOf <<(:liz :spouse :richard )>> .
>     :wed-1 :start 1964; :end 1974 .
>     :wed-2 rdfx:occurrenceOf <<(:liz :spouse :richard-burton )>> .
>     :wed-2 :start 1975; :end 1976 .
>     :richard owl:same-as :richard-burton
>
>     entails:
>     :wed-1 rdfx:occurrenceOf <<(:liz :spouse _:b)>> .
>     :wed-1 rdfx:occurrenceOf <<(:liz :spouse :richard-burton)>> .
>     :wed-1 rdfx:occurrenceOf _:x .
>     :wed-2 rdfx:occurrenceOf _:x . / (note the same blank node _:x)/
>
>     SPARQL query:
>     ASK WHERE { :wed-1 rdfx:occurrenceOf ?x . :wed-2 rdfx:occurrenceOf
>     ?x } *=> TRUE*
>
>
> My fear is that the latter inferences (involving the bnode/variable x) 
> are very complex to be implemented. I am not aware of any correct 
> algorithm to do that kind of inferences, and how this could interact 
> with the standard reasoning algorithms (for RDFS, OWL, SHACL, etc).
> Unless we understand this, the choice to have explicit triple terms 
> may have a severe impact on the whole SW stack.
>
> I have proposed a restriction to the syntax proposed by Andy without 
> explicit triple terms, and proposed a semantics for it:
> https://github.com/w3c/rdf-star-wg/wiki/Semantics:-Andy's-proposal
>
> cheers
> —e.
>
>
>> On 21 Dec 2023, at 17:01, Franconi Enrico <franconi@inf.unibz.it> wrote:
>>
>>> On 20 Dec 2023, at 10:26, Olaf Hartig <olaf.hartig@liu.se> wrote:
>>>
>>> That's my reading as well. However, maybe someone with a more intimate
>>> understanding of the subtleties* of the notions of a token and an
>>> occurrence should look at this question.
>>>
>>> *https://plato.stanford.edu/entries/types-tokens/#Occ

>>>
>>>> Are these fundamental in the abstract syntax? Or is the token
>>>> considered syntactic sugar for something like [] rdfx:occurrenceOf
>>>> <<( :s :p :o )>>?
>>>
>>> When I read Andy's email, I was assuming the latter, and that's also
>>> what my immediate reaction would be, now that you ask this question
>>> explicitly.
>>
>> I’m trying to write the formal model theoretic semantics of Andy’s 
>> proposal.
>> I have a problem about having triple terms as the basis for everything.
>> Consider the example:
>>
>> :wed-1 rdfx:occurrenceOf <<(:liz :spouse :richard )>> .
>> :wed-1 :start 1964; :end 1974 .
>> :richard owl:same-as :richard-burton
>> ⊨
>> :wed-1 rdfx:occurrenceOf <<(:liz :spouse :richard-burton)>> .
>> _:b1 rdfx:occurrenceOf <<(:liz :spouse _:b2)>> .
>> _:b1 :start 1964 .
>>
>> This requires triple terms to have a strong semantic: namely, the 
>> identity of triple terms depends on their components.
>>
>> For this reason, I tried to formalise a semantics based on triple 
>> occurrences.
>> You can see it at:
>> https://github.com/w3c/rdf-star-wg/wiki/Semantics:-Andy's-proposal 
>> <https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fw3c%2Frdf-star-wg%2Fwiki%2FSemantics%3A-Andy%27s-proposal&data=05%7C02%7Cfranconi%40inf.unibz.it%7C5d2fcdd4e8214a37d7cf08dc023e254a%7C9251326703e3401a80d4c58ed6674e3b%7C0%7C0%7C638387713136482504%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=M%2FuUvlX9ke2MI%2F9EL%2F5uD8ThpvambYVklLcaPhwPq5I%3D&reserved=0>
>>
>> cheers
>> —e.
>