Terminology

Connect to definitions in RDF 1.2 Concepts.

TODO

RFC 2119 language should autmatically be inserted here.

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

RDF Rules Syntax

@@ link to SHACL constraints

Compact Rules Syntax

The grammar is given below.

Mapping the AST to the abstract syntax.

Evaluation Definitions

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=].

Evaluation Graph

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

triple pattern match

A [=triple pattern 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 `match(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.

match(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 comptible, 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. (It is the union of solutions if defined as sets of pairs.)

Let S1 and S2 be solution sequences.

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

Evaluation of an Expression

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

Let [x/μ] be
    if x is an RDF term, the [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 = (head, body) 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
    let S1 = { }

    if rElt is a triple pattern TP:
        X = match(G, TP)
        SEQ1 = { μ0 }
        for each μ1 in X:
            for each μ2 in T:
              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, μ)
            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 T:
    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 grapoh.

Evaluation of a Rule Set

Let G be the input RDF graph.
Let I be the set of triples generated by evaluation
Let RS be a rule set
Let finished = false
while !finished:
    finished = true
    foreach rule in RS
        let GI = G union I
        let X = eval(rule, GI)
        let Y = those triples in X that are not in GI
        if Y is not empty:
            finished = false
            endif
        let I = Y union I
        endfor
    endwhile

result is GI