Semantics: Behaviour catalogue

Semantics: Behaviour catalogue by Enrico

SYNTAX:

graph ::= *(triple)
triple ::= no-literal-term iri term
no-literal-term ::= iri | bnode | quoted-triple-term
term ::= no-literal-term | literal
quoted-triple-term ::= transparent-qtt | CG-qtt | asserted-qtt | ...
xxx-qtt ::= no-literal-term iri term

Terms are denoted by r, triples by t, and graphs by g.
Given a triple or quoted triple term a, we denote the subject, predicate, and object of a as a.s, a.p, and a.o, respectively.

SEMANTICS:

An RDF-star interpretation I is a structure:

• < < IR, IP, IS0, IL0, IEXT0 >, IT0,
   < IR, IP, IS1, IL1, IEXT1 >, IT1, ... >
  

such that:

• < IR, IP, ISi, ILi, IEXTi > is a RDF 1.1 simple interpretation.
• ITi is a mapping from IRxIPxIR to IR,
      such that: ∀ <x,y,z> ∈ dom(ITi). <x,z> ∈ IEXTi(y).
  

• Ai are mappings from blank nodes to IR.
  

Given I, [Ii+Aj] is a function defined over RDF-star terms and RDF-star triples as follows.

• [Ii+Aj](r) = ILi(r) if r is a literal
  
• [Ii+Ai](r) = ISi(r) if r is a IRI
  
• [Ii+Aj](r) = Aj(r) if r is a blank node
  
• [Ii+A0](r) = IT1(<[I0+A0](r.s),[I0+A0](r.p),[I0+A0](r.o)>) if r is a transparent quoted triple term
  
• [Ii+A0](r) = IT2(<[I2+A0](r.s),[I2+A0](r.p),[I2+A0](r.o)>) if r is a CG quoted triple term
  
• [I0+A0](r) = IT0(<[I0+A0](r.s),[I0+A0](r.p),[I0+A0](r.o)>) if r is an asserted quoted triple term
  
• [Ii+Aj](r) = ... if r is a xxx quoted triple term
  

• [I0+A0](t) = TRUE if and only if <[I0+A0](t.s),[I0+A0](t.o)> ∈ IEXT0(IS0(t.p))
  

• [I0+A0](g) = TRUE if and only if ∀ t ∈ g . [I0+A0](t) = TRUE
  

An interpretation I is called a model for g if there exists A0 such that [I0+A0](g) = TRUE.

Simple entailment: g ⊨ g' if and only if models(g) ⊆ models(g').

( A review of the standard semantics of RDF 1.0: semantics of RDF.pdf ).

DIFFERENT INTERPRETATION OF QUOTED TRIPLE TERMS:

Triple:

• true in the asserted world: same IEXT
• true in a different world IEXTi
  • distinct world for each occurrence
    • distinct worlds for the same quoted triple terms appearing in distinct triples
    • same world for the same quoted triple terms appearing in distinct triples
  • special worlds — e.g., syntactic, or same modality

IRI:

• transparent: same IS
• opaque: distinct ISi for each world
• hard opaque: pairwise disjoint ISi for each world

Bnodes:

• transparent: same A
• opaque: distinct Aj for each world
• hard opaque: pairwise disjoint Aj for each world

Literals:

• transparent: same IL
• opaque: distinct ILi for each world
• hard opaque: pairwise disjoint ILi for each world

CASES:

• "Transparent" quoted triple terms (the TEP case of the CG spec) have transparent IRIs, Literals, BNodes, and are true in an alternative world (IEXT1):

  :measuredOn rdf:type rdf-star:TransparencyEnablingProperty .
  << dbr:Linköping dbo:populationTotal "104232"^^xsd::nonNegativeInteger >>
      :type rdf-star:statement ;
      :measuredOn "2010-12-31"^^xsd:date .
  

• "CG" quoted triple terms (the basic case of the Community Group spec) have opaque IRIs and Literals, transparent BNodes, and are true in one an alternative world (IEXT2):

  << dbr:Linköping dbo:populationTotal "104232"^^xsd::nonNegativeInteger >>
      :type rdf-star:triple ;
      :source <https://dbpedia.org/data/Linköping.ttl> .
  

• "Asserted" quoted triple terms have transparent IRIs, BNodes, Literals and are true in the asserted world (IEXT0) - this captures the representation of n-ary relations:

  << :john :teaches :cs101 >> 
      rdf:type :teaching ; 
      dct:Location  dbr:Stanford_University .