Basic Encoding of Reified Propositions

Note

This is a draft proposal, not yet ready for wider consideration.

Abstract

This document describes a way of encoding RDF 1.2-reified propositions in RDF 1.2 Basic. (In RDF 1.2 Basic abstract syntax, like in RDF 1.1, triples are not available as terms of other triples.)

Bonus inclusions:

• An OWL model specifying the well-formedness requirement of encoded propositions.
• A semantic extension entailing the basic encoding.

Example

The following expression (using syntactic sugar):

    :alice :thinks << :bob :likes :bob ~ _:e >> .

which expands to:

    :alice :thinks _:e .

    _:e rdf:reifies <<( :bob :likes :bob )>> .

is basic-encoded as:

    :alice :thinks _:e .

    _:e rdf:reifiesEncoded _:tt .

    _:tt a rdf:EncodedProposition ;
        rdf:subject :bob ;
        rdf:predicate :likes ;
        rdf:object :bob .

Basic Design

The encoding uses a relationship from a reifier to some described encoded proposition, existentially quantified (with a blank node), and described with relations to the resources denoted by the constituents of this proposition. This encoding is a "token", and a reification the abstract proposition. It may be the triple itself; that is undefined. The necessary restriction is that these encodings correspond one-to-one with the abstract proposition.

This avoids exposing the abstract proposition as a resource in the model.

Note

Note that these encodings are specialized instances of the classic rdf:Statement "tokens", with the above one-to-one constraint. This clarifies that not all classic reifications are in themselves these one-to-one tokens, but some may be. This is also a "safety" in the encoded form, since if the token would be further described, such "stray facts" can be kept in RDF 1.2 Full.

  << :bob :likes :bob ~ _:tt >> :spurious "note" .

Warning

It does, however, expose a token thereof in the model; which in very constrained universes may be "reading too much" into the interpretation? A counter-argument could be that these tokens only exist when the universe contains abstract propositions, and that presupposes something. Only of the existing reifiers cannot have "proper parts" corresponding one-to-one with the abstract propositions would this be a problem.

Limitation by design: Does not encode all uses of triple terms, only reified or annotated triples (the "syntactic sugar" forms in Turtle).

Model

    rdf:EncodedProposition a rdfs:Class ;
      rdfs:subClassOf rdf:Statement .

    rdf:reifiesEncoded a owl:ObjectProperty ;
      rdfs:range rdf:EncodedProposition .

Well-formed Requirement

A triple is denoted by a blank node. It must have exactly one subject, predicate and object, and is uniquely identified through those as a key. Logically, it reifies exactly one proposition.

Optional relaxation

This would allow the (indirect) encoding of all possible references to propositions.

Instead of the shorthand relationship from the reifier to the encoded proposition:

    _:e rdf:reifiesEncoded _:tt .

both can be described as directly refiying the proposition, denoted by a blank node:

    _:e rdf:reifies _:pp .
    _:tt rdf:reifies _:pp .

In this form, the proposition is "exposed" as a blank node co-denoting it. (No further properties thereof need to be described. Its type does not need to be encoded, as it is entailed.)

But by exposing the proposition, it also enables misuse of the blank node to encode ill-formed propositions, such as self-referential propositions, propositions with multiple distinct predicates, or as subjects.

In OWL

The meaning of the well-formedness can be expressed in OWL as:

    rdf:EncodedProposition
      rdfs:subClassOf [ owl:onProperty rdf:reifies ; owl:cardinality 1 ] ;
      owl:hasKey (rdf:subject rdf:predicate rdf:object) .

Note that:

    _:e rdf:reifiesPropositionEncodedBy _:tt .

should be implied by:

    _:e rdf:reifies _:pp .
    _:tt rdf:reifies _:pp .
    _:tt a rdf:EncodedProposition .

Using OWL, this can be specified with:

    rdf:reifiesPropositionEncodedBy
      owl:propertyChainAxiom (rdf:reifies [ owl:inverseOf rdf:reifies ] _:selfOfTypeTriple) .

    rdf:EncodedProposition
      owl:equivalentClass [ owl:onProperty _:selfOfTypeTriple ;
                            owl:hasSelf true ] .

Entailment Extension

For every reified proposition, there exists some encoding thereof.

Formally:

    aaa rdf:reifies <<( bbb ccc ddd )>> .

entails:

    aaa rdf:reifies _:pp .
    _:tt rdf:reifies _:pp .
    _:tt rdf:type rdf:EncodedProposition .
    _:tt rdf:subject bbb .
    _:tt rdf:predicate ccc .
    _:tt rdf:object ddd .

Note that, given the OWL definitions above, that in turn entails:

    aaa rdf:reifiesPropositionEncodedBy _:tt .

This:

• Ensures that applications built on RDF 1.2 Basic assumptions can continue to work when upgraded RDF 1.2 Full (through these entailed facts).
• Enables modelling using OWL to bridge different modelling designs and granularities.

(This extension would resolve issue https://github.com/w3c/rdf-ucr/issues/27 and https://github.com/w3c/rdf-star-wg/issues/154.)