Re: Semantic Predication: 5 - model theory

> On 21. Feb 2023, at 12:30, Timothée Haudebourg <timothee.haudebourg@spruceid.com> wrote:
> 
> Thanks Enrico, you made me realize I've completely overlooked the model theoretic semantics up until now (I hope I'll be pardoned, I'm still relatively new on this topic).
> 
> Anyway. The semantics you proposed is so simple I am now convinced referential transparency should be the default (I discuss how to add opacity below), although I would omit the last semantic condition:
> 
> [I+A](s,p,o)=true iff ∃b. [I+A](<<<s,p,o>>>)=[I+A](b)
> 
> Is that really necessary? That would forbid anyone from quoting non asserted triples. I believe removing it would only affect the logical equivalence without breaking the other properties of this semantics, right? Without it, the semantics is equivalent to the alternative referentially transparent semantics discussed in the CG: https://www.w3.org/2021/12/rdf-star.html#other-alternatives-to-referential-opacity
> 
> Now how do we reintroduce referential opacity on top of that? Would it be a good idea to add new types of resources that wraps around syntactic constructs to add opacity? Let me explain with an example.
> 
> :klarkKent owl:sameAs :superman .
> :Journalist rdfs:subClassOf :Worker .
> :lois :knows <<:klarkKent rdf:type :Journalist>> .
> 
> With referential transparency the quoted triple is equivalent to the following:
> 
> _:stm unstar:subject :klarkKent .
> _:stm unstar:predicate rdf:type .
> _:stm unstar:object :Journalist .
> 
> Because :lois does not know that :klarkKent is :superman (I don't know the Superman lore, maybe she actually knows but let's assume not), we do not want referential transparency for :klarkKent in the quoted triple. However we may safely assume that :lois knows everything about what a :Journalist is, in particular that if :klarkKent is a :Journalist she also knows he is a :Worker, so we may want transparency there.

Indeed.

> A sort of selective transparency. 

Rather a sort of selective opacity on specific terms. That would certainly be enough to reason about Clark Kent/Superman and Morning Star/Evening Star.

> I express the opacity with an additional <>, but I know this is not a good syntax:
> 
> :lois :knows <<<:klarkKent> rdf:type :Journalist>> .

How about:

    <":clarkKent"^^rdf:ttl>

Your example then would become:

    :lois :knows << <":clarkKent"^^rdf:ttl> rdf:type :Journalist>> .

That requires two things:
- an RDF graph literal datatype
- a definition that enclosing such a graph literal with <…> interprets it (referentially opaque)

The graph literal can also be used to implement other use cases driving the proposed semantics, eg versioning.


Thomas



> :klarkKent is now opaque, which would be equivalent to the following:
> 
> _:stm unstar:opaqueSubject _:subject .
> _:stm unstar:predicate rdf:type .
> _:stm unstar:object :Journalist .
> _:subject rdf:type unstar:quotedIRI .
> _:subject unstar:value "https://example.org/klarkKent"^^xsd:anyURI .
> 
> I introduce the unstar:opaqueSubject property that we can substitute to the unstar:subject to specify that the subject is opaque. The domain of unstar:opaqueSubject is some unstar:opaqueNode (unstar:quotedIRI, unstar:quotedBlank, unstar:quotedLiteral) that describes the syntactic representation of the node, without referring to its interpretation. Similarly to unstar:quotedIRI, unstar:quotedLiteral can describe a literal value and its type:
> 
> _:literal rdf:type unstar:quotedLiteral .
> _:literal unstar:value "01" .
> _:literal unstar:datatype xsd:integer .
> 
> I'm not sure how we would quote blank node identifiers unless we have a way of identifying the graph we are in. In which case the blank node identifier _:0 could be quoted as
> 
> _:blank rdf:type unstar:quotedBlank .
> _:blank unstar:value "0" .
> _:blank unstar:namespace g .
> 
> where g is the hypothetical graph identifier.
> 
> I think I can come up with a model theoretic semantics for all of that if needed (except maybe for the blank node identifier part).
> To summarize:
> 
>   - Semantic predication: can be achieved by simply quoting and stating triples:
> 
> :john :teaches :cs101 .
> << :john :teaches :cs101 >> rdf:type :teaching ;
>                             dct:Location dbr:Stanford_University ;
>                             dct:PeriodOfTime :1st-term-2022 .
> 
>   - Syntactic predication: can be achieved by quoting with opaque components:
> 
> << <:john> <:teaches> <:cs101> >> :recorded "2021-07-07"^^xsd:date .
> 
>   - Modal/epistemic predication: here I'm not sure because I don't yet understand the difference with semantic predication.
> 
> Some additional notes:
> 
>   - unstar:subject and unstar:opaqueSubject are not necessarily mutually exclusive. We could have a quoted triple with transparent subject AND that also specifies the syntactic representation of the subject (or predicate or object):
> 
> _:stm unstar:subject _:klarkKent .
> _:stm unstar:opaqueSubject _:subject .
> _:subject rdf:type unstar:quotedIRI .
> _:subject unstar:value "https://example.org/klarkKent"^^xsd:anyURI .
> 
>   - We may allow quoting components alone, outside of quoted triples, like <:klarkKent>. In this case we need to decide a custom syntax in quoted triples to differentiate between opaque components and transparent quoted components.
> 
> -- 
> Timothée
> 
>

Received on Wednesday, 22 February 2023 14:25:33 UTC