SHACL 1.2 Rules

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

As well as sections marked as non-normative, all authoring guidelines, diagrams, examples, and notes in this specification are non-normative. Everything else in this specification is normative.

TODO

: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.

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

# 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 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 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".

The grammar is given below.

Vocabulary: shacl-rules.ttl.

binding

A binding is a pair (variable, RDF term), consistent with the definition used in [sparql12-query].

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)

Editor's note

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

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

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`

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.

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