Terminology

Connect to definitions in RDF 1.2 Concepts.

The following definitions from other specifications are used in this document: @@

TODO

RFC 2119 language should autmatically be inserted here.

Basic Usage

   :A :fatherOf :X .
   :B :motherOf :X .
   :C :motherOf :A .

RULE { ?x :childOf ?y } WHERE { ?y :fatherOf ?x }
RULE { ?x :childOf ?y } WHERE { ?y :motherOf ?x }

RULE { ?x :descendedFrom ?y } WHERE { ?x :childOf ?y }
RULE { ?x :descendedFrom ?y } WHERE { ?x :childOf ?z . ?z :childOf ?y }

The above rules, applied to the data, will conclude that: `:X` is the `:childOf` `:A` and `:B`, and that `:X` is `:descendedFrom` `:C`.

Recursion

RULE { ?x :ancestorOf ?y } WHERE { ?y :descendedFrom ?x }
RULE { ?a :ancestorOf ?b } WHERE { ?a :ancestorOf ?c . ?c :ancestorOf ?b }

Negation

# Default value - calculate a name
RULE { ?x :name ?FN } WHERE { 
    ?x rdf:type :Person 
    NOT { ?x :name ?someName }
    ?x :givenName ?name1 ;
       :familyName ?name2 .
    BIND(concat(?name1, " ", ?name2) AS ?FN)
}

Stratification

Stratification is the process of labelling rules based on their dependency relationships in a rule set. The set of rules with the same label are called a layer.

stratification layer

A stratification layer, usually, just "layer", is the set of rules with same stratification labelling. stratification layer, layer

rule element dependency

A [=rule body element=] `E` depends on a rule `R` if the head of rule `R` contains a [=triple template=] that may provide a triple that is matched by a triple pattern in `E`.

rule dependency

A rule `R1` depends on rule `R2` if any rule element of `R1` depends on `R2`.
@@formalize

Process

• Layer 0 = base graph
• For each rule, determine the label of all rule elements if possible yet.
• Label of a rule is the max label of its [=rule body elements=]
• repeat

Conditions

• For a rule, all its (rule elements) negation/aggregation dependencies must have a label that is less than the layer label of this rule.

Well-formedness Conditions

Well-formedness is a set of conditions on the abstract syntax of shapes rules. Together, these rules ensure that a [=variable=] in the [=head=] of a rule has a value defined in the [=body=] of the rule; that each variable in an condition expression or assignment expression has a value at the point of evaluation; and that each assignment in a rule introduces a new variable, not used earlier in the rule body.

A [=rule=] is a well-formed rule if all of the following conditions are met:

• For every [=variable=] appearing in a [=triple template=] of the [=head=] of the [=rule=], there is one or more occurrences of a [=variable=] of the same name in the [=triple patterns=] in the [=body=], or in an [=assignment=] in the body, or both.
• For every [=variable=] in an [=expression=] at position i of the [=body=], there is a corresponding [=variable=] of the same name occuring in a [=triple pattern=] at a position j, or occurring as an [=assignment variable=] at a position j, where i > j.
• Each [=assignment variable=] is used in only one [=assignment=] in the [=body=] of the [=rule=].
• An [=assignment variable=] at position i of a [=rule body=] does not occur in any [=triple pattern=] at position j where i > j.
• For every [=variable=] in an [=assignment expression=] at position i, there is a corresponding variable in a triple pattern at position j where i > j, or there is an [=assignment variable=] in an [=assignment=] at position j where i > j.

A [=rule set=] is "well-formed" if and only if all of the [=rules=] of the rule set are "well-formed".

Shape Rules Language syntax

The grammar is given below.

Mapping the AST to the abstract syntax.

RDF Rules Syntax

Vocabulary: shacl-rules.ttl.

Evaluation Definitions

solution mapping

A solution mapping, μ, is a partial function μ : V → T, where V is the set of all variables and T is the set of all RDF terms. The domain of μ is denoted by dom(μ), and it is the subset of V for which μ is defined. We use the term [=solution=] where it is clear that a [=solution mapping=] is meant. Write μ₀ for the solution mapping such that dom(μ0) is the empty set.

substitution function

A substitution function, or just substitution, is a function subst(μ, [=triple pattern=]) that returns a triple pattern where each occurrence in the triple pattern of a variable that is in the dom(μ) is replaced by the [=RDF term=] given by the [=solution mapping=] for var. If the triple pattern result has no variables, then it is an [=RDF Triple=].

base graph

The [=base graph=] is the [=RDF Graph=] given as input to the evaluation process.

evaluation graph

A [=evaluation graph=] is an [=RDF Graph=] that combines the [=base graph=] and all triples produced during the evaluation of a rule set.

graph match

A [=graph match=] finds the ways to map a triple pattern onto triples in an [=RDF Graph=].

Let G be an [=RDF graph=] and TP be a triple pattern. The function `graphMatch(G, TP)` returns a set of all possible solutions that, when applied to the triple pattern, produce a triple that is in the [=evaluation graph=]

Let G be an [=RDF graph=] and TP be a triple pattern.

graphMatch(G, TP) = { μ | subst(μ, TP) is a triple in G }

solution compatible

Two solutions S1 and S2 are [=compatible=] if they agree on the variables in common.

Let S1 and S2 be solutions.

compatible(μ1, μ2) = true
                      if forall v in dom(μ1) intersection dom(μ2)
                          μ1(v) = μ2(v)
compatible(μ1, μ2) = false otherwise
              

solution sequence

A [=solution sequence=] is a multi-set of solutions. There is no defined order to the sequence. It is equivalent to an unordered list and it can contain duplicates.

solution merge

If two solutions are compatible, the merge of two solutions is the solution that maps variables of each solution to the [=RDF term=] from one or other of the solutions.

Let μ₁, μ₂ be solution mappings, and S1 and S2 be solution sequences.

merge(μ1, μ2) = { μ |
                    μ(v) = μ1(v) if v in dom(μ1)
                    μ(v) = μ2(v) otherwise }

merge(S1, S2) = { μ |
                    μ1 in S1, μ2 in S2
                    and compatible(μ1, μ2)
                    μ(v) = merge(μ1, μ2)

Say the domain is `dom(S1) ∪︀ dom(S2)`.

Say that two solutions that have no variables in common are compatible.

Evaluation of an Expression

Sketch

Let F(arg1, arg2, ...) be an expression.
where arg1, arg2 are RDF terms.
@@

Let [x/μ] be
    if x is an RDF term, then [x/row] is x
    if x is a variable, then [x/row] is μ(x)
    ## By well-formedness, it is an error if x is not in the row.

eval(F(expr1, expr2 ...), row) = F(eval(expr1, row), eval(expr2, row), ...)
 ...
eval(FF(expr1, expr2) , row) = ... things that are not functions like `IF`

Evaluation of a Rule

let R be a well-formed rule.
let rule R = (H, B) where
             H is the sequence of triple templates in the head
             B is the sequence of triple patterns, condition expressions,
                and assignments in the body

let R : map variable to RDF term as a set of pairs (variable, RDF term)

## Solution sequence of one solution that does not map any variables.
## (This is the join identity)

let SEQ: Solution sequence = { μ0 }
let G = evaluation graph

# Start::

Replace each blank node in B with a fresh 
variable that does not occur in the rule body.

# Evaluate rule body

for each rule element rElt in B
    if rElt is a triple pattern TP:
        X = graphMatch(G, TP)
        SEQ1 = {}
        for each μ1 in X:
            for each μ2 in SEQ:
              if compatible(μ1, μ2)
                μ3 = merge(μ1, μ2)
                add μ3 to SEQ1
            endfor
        endif

    if rElt is a condition expression F:
        SEQ1 = {}
        for each solution μ in SEQ:
            ## EBV = Effective boolean value.
            ## TODO: Eval errors.
            if ( EBV(eval(μ, F)) is true )
                add μ to SEQ1
                endif
            endfor
        endif

    if rElt is an assignment(V, expr)
        SEQ1 = {}
        for each solution S in SEQ:
            let x = eval(expr, S)
            add(V, x) to S
            add S to SEQ1
            endfor
        endif

     if SEQ1 is empty 
        SEQ = {}
        exit
        endif

      SEQ = SEQ1
   
    endfor

# Evaluate rule head
let H = empty set
for each μ in SEQ:
    let S = {}
    for each triple template TT in head
        let triple = subst(μ, TT)
        Add triple to S
    H = H union S
    endfor

result eval(R, G) is H

Note that `H` may contain triples that are also in the data graph.

Evaluation of a Rule Set

Sketch

let G0 be the input RDF graph.
let RS be the rule set
Apply stratification to RS
let L be the sequence of layers after stratification

let GI = G0
for each layer in L:
    let finished = false
    while !finished:
        finished = true
        for each rule in layer:
            let X = eval(rule, GI)
            let Y = { t ∈ X | t ∉ in GI }
            if Y is not empty:
                finished = false
                endif
            let GI = Y ∪︀ GI
            endfor
        endwhile
    endfor
the result is GI