RDF star profile "functional opaque"

RDF-star profile "functional opaque" (DRAFT 2024.05.15)

ABSTRACT SYNTAX

graph            ::= ( triple | reifier rdf:annotationOf opaqueTripleTerm )*
triple           ::= subject predicate object 
subject          ::= iri | BlankNode
predicate        ::= iri_but_rdf:annotationOf 
object           ::= iri | BlankNode | literal
reifier          ::= iri | BlankNode  
opaqueTripleTerm ::= triple

Notes:

• RDF 1.1 syntax is the above without the opaqueTripleTerm category.
• A term is denoted by r, a triple by t, and a graph by g.
• Given a triple t, we denote the subject, predicate, object of t as t.s, t.p, t.o, respectively.

SEMANTICS

An RDF simple interpretation I is a structure <IR, IP, IS, IL, IEXT, SRE> consisting of:

1. A non-empty set IR of resources, called the domain or universe of I.
2. A set IP, called the set of properties of I.
3. A mapping IS from IRIs into IR ⋃ IP, called the interpretation of IRIs.
4. A partial mapping IL from literal into IR, called the interpretation of literals.
5. A mapping IEXT from IP into 2IR x IR, called the extension of properties.
6. ⏩ A (canonical) injective function SRE from opaqueTripleTerm into literal of datatype rdf:TripleTermDatatype, called the syntactic denotation of triple terms. ⏪
   

A is a mapping from BlankNode to IR.

Given I and A, the function [I+A](.) is defined over terms, triples, and graphs as follows.

• [I+A](r) = IS(r)   if r is a iri
• [I+A](r) = IL(r)   if r is a literal
• ⏩ [I+A](r) = IL(SRE(r))   if r is a opaqueTripleTerm ⏪️
• [I+A](r) = A(r)   if r is a BlankNode

• [I+A](t) = TRUE   if and only if   <[I+A](t.s), [I+A](t.o)> ∈ IEXT([I+A](t.p))

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

An interpretation I is a model of a graph g   if and only if
  ∃ A . [I+A](g) = TRUE and
  ⏩ ∀ x,y1,y2 . (x,y1) ∈ IEXT(IS(rdf:annotationOf)) ⋀ (x,y2) ∈ IEXT(IS(rdf:annotationOf)) → y1=y2 ⏪️

The set of all models of a graph g is called models(g).

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

Notes:

• RDF 1.1 semantics is the above without the parts within ⏩...⏪ marks, involving the opaqueTripleTerm category, and the functionality of rdf:annotationOf.