Proposal to RDF Data Shapes WG
SHACL (Shapes Constraint Language) provides structural constraints for RDF graphs. SHACL constraints are grouped into conjunctions called "shapes", which may also be referenced by constraints in other shapes. These constraints restrict the predicates of triples connecting nodes in the graph. SHACL can restrict the number of these triples and the permitted object datatype or object terms, require that the subject or object match some shape or lexical and datatype conditions.
The full abstract syntax of SHACL is defined at SHACL Language
In this section we map the terms of the full abstract syntax to the simplified abstract syntax that will be employed in the axiomatic definition of SHACL
| SHACL construct | Abstract Syntax | notes |
|---|---|---|
| shape | empty | A shape without any constraint |
| property constraint | arc predicate value cardinality | |
| inverse property constraint | inverseArc predicate value cardinality | |
| and constraint | And(S1,S2) | Multiple conjuncts S1...SN can be defined and(S1,and(S2,...and(SN-1,SN))) |
| or constraint | Or(S1,S2) | Multiple disjuncts S1...SN can be defined or(S1,or(S2,...or(SN-1,SN))) |
| predicate | p | |
| node type | NodeType(t) | |
| datatype(t) | Datatype(dt) | |
| allowed value(V1...VN) | AllowedValue(V1,...VN) | |
| value shape(shape) | ValueShape(shape) |
The BNF notation that represents the simplified abstract syntax is:
Shape ::= Empty // No constraint
| BasicArc Predicate Value Cardinality // Basic Arc with predicate, value and cardinality
| And Shape Shape // Matches if Shape1 and Shape2 match
| Or Shape Shape // Matches if Shape1 or Shape2 match
BasicArc can be can be a direct property or an inverse property
BasicArc ::= Arc | InvArc //
Cardinality defines the minimum and maximum cardinality.
The maximum cardinality can be unbounded which
is the default value
Cardinality ::= {Int,Int | unbounded} // Min,Max-cardinality
A predicate is just an IRI.
Predicate ::= IRI // the predicate to match
A Value defines the shape of Objects or Subjects.
Value ::= NodeType IRI // Matches if the term is of the kind specified by the IRI (ex. sh:IRI, sh:Literal,...)
| AllowedValue v1 v2 ... vN // Matches if the term belongs to the set of values v1...vN where Vi can be IRI or Literal
| DataType IRI // Matches if the term is belongs to the datatype denoted by IRI
| ValueShape Label // Matches if the value is a node that conforms with shape ShapeRef
A Schema is a mapping from Labels (IRIs) to Shapes
The abstract syntax of a Schema is:
Schema ::= (Label Shape) * // Schema associates a Label with a Shape Label ::= IRI // A Label identifies a Shape in a Schema
This document doesn't define shape dereferentiation from a Label. For simplicity, labels are defined as IRIs. It may be possible to have BNodes as Labels also.
# shapes (Turtle)
ex:IssueShape a sh:Shape ;
sh:property [
sh:predicate ex:state ;
sh:allowedValue (ex:unassigned ex:assigned) ;
sh:minCount 1 ; sh:maxCount 1
] ;
sh:property [
sh:predicate ex:reportedBy ;
sh:valueShape sh:UserShape ;
sh:minCount 1 ; sh:maxCount 1
] .
ex:UserShape a sh:Shape ;
sh:property [
sh:predicate foaf:name ;
sh:valueType xsd:string ;
sh:minCount 1 ; sh:maxCount 1
] ;
sh:property [
sh:predicate foaf:mbox ;
sh:nodeType sh:IRI ;
sh:minCount 1
] .
The example can be defined in the abstract syntax as:
ex:IssueShape
(And (Arc ex:state (ValueSet (ex:unasigned ex:asigned)) {1,1})
(Arc ex:reportedBy (ValueShape ex:UserShape) {1,1})
)
ex:UserShape
(And (Arc foaf:name (ValueType xsd:string) {1,1})
(Arc foaf:mbox (NodeType IRI) {1,unbounded})
)
The semantics of a Shape schema consist of a specification of what nodes in an RDF graph match a specific shape with respect to that schema. The semantics is described formally using axioms and inference rules. Axioms are propositions that are provable unconditionally. An inference rule consists of one or more antecedents and exactly one consequent. An antecedent is either positive or negative. If all the positive antecedents of an inference rule are provable and none of the negative antecedents are provable, then the consequent of the inference rule is provable.
The notation for inference rules separates the antecedents from the consequent by a horizontal line: the antecedents are above the line; the consequent is below the line. If an antecedent is of the form not(p), then it is a negative antecedent; otherwise, it is a positive antecedent.
We represent RDF graphs as sets of RDF triples, where an RDF triple is <subject,predicate,object> such that subject is a URI or a BNode, predicate is a URI and object is a URI, BNode or Literal.
A node is a subject or an object. For our purposes, an RDF graph has the following operations:
| {} | Empty graph (empty set of triples) |
| {t} | Singleton graph with triple t |
| g1 ∪ g2 | Union of graphs g1 and g2 |
| g1 ∩ g2 | Intersection of graphs g1 and g2 |
| addTriple(t,ts) | The set of triples that results of adding triple t to
the set of triples ts
addTriple(t,ts) = {t} ∪ ts |
| removeTriple(ts) |
A pair (t,ts') where t is a triple removed from the set of triples g and g' is the remaining triples removeTriple(ts) ∈ {(t,ts')| {t} ∪ ts' = ts ∧ t ∉ ts' } |
| g.triplesAround(node) |
Selects the triples that contain node as subject or as object in graph g
g.triplesAround(node) = { <s,p,o> ∈ g | s = node ∨ o = node } |
During the matching process, SHACL processors assign typings to nodes in an RDF graph. A typing is a map from RDF nodes (IRI's or BNodes) to sets of shapes. We assume each shape can be uniquely identified by a label (URI or BNode)
We define the following operations on those typings:
| {} | empty shape typing |
| addType(node,label,typing) | the result of associating type label to node in typing |
| combineTypings(t1, t2) | combination of typings t1 and t2 |
| contains(t,node,label) | succeeds if typing t asserts that node has shape label |
This section needs to be improved to describe in more details the typing operations
The SHACL processor acts in a context.
A context is a tuple (s, g, t) where s is a set of shapes (also called schema) which can be identified by a label (URI or bNode), g is an RDF Graph and t is a Typing.
We define the following operations on contexts:
| ctx.typing | current typing in ctx |
| ctx { node → label } | Given a context with typing t, represents the same context where typing is addType(node,label,t) |
| matchNode | ctx.schema(label) = shape ctx.graph.triplesAround(node) = ts ctx { node → label } |- matchShape(ts, shape) = (t,cs,rs) |
| ctx |- matchNode(node,label) = (t,cs,rs) |
Define the startup conditions of the matching nodes. The typing context must contain an empty typing when matching a node for the first time.
ctx |- matchShape(triples, shape) checks if a set of triples triples conforms with shape in context ctx. If it conforms, it evaluates to (t,cs,rs) where t is a typing, cs is a set of checked triples, rs is a set of remaining triples.
The empty shape matches any set of triples without any constraint.
| Empty | |
| ctx |- matchShape(ts,Empty) = (ctx.typing,{},ts) |
We distinguish the following cases for basic arcs depending on the cardinality.
When the cardinality is {0,unbounded} and there is no arc that matches, then it matches the set of triples without consuming any triple
| BasicArc_unbounded1 | ctx |- noMatchAny(ts,basicArc) |
| ctx |- matchShape(ts,basicArc {0,unbounded}) = (ctx.typing,{},ts) |
When the cardinality is {0,unbounded} and there is some arc that matches it consumes it
| BasicArc_unbounded2 | removeTriple(ts) = (t,ts') ctx |- matchBasicArc(t,basicArc) = t1 ctx |- matchShape(ts',basicArc {0,unbounded}) = (t2,cs,rs) |
| ctx |- matchShape(ts,basicArc {0,unbounded}) = (combineTypings(t1,t2),addTriple(t,cs),rs) |
When the cardinality is {m,unbounded} for m > 0 it matches if there is one triple that matches and if the rest of triples matches with a cardinality of {m - 1, unbounded}
Notice that it only matches if there is at least one triple
| BasicArc_unbounded3 | m > 0 removeTriple(ts) = (t,ts') ctx |- matchArc(t,basicArc) = t1 ctx |- matchShape(ts',basicArc {m - 1,unbounded}) = (t2,cs,rs) |
| ctx |- matchShape(ts, basicArc {m,unbounded}) = (combineTypings(t1,t2),addTriple(t,cs),rs) |
When the cardinality is {0, n} for n >= 0 it can match if there is not triple that matches or if there is one triple that matches and the rest of triples matches with a cardinality of {0, n-1}
| BasicArc_bounded1 | n >= 0 ctx |- noMatchAny(ts,basicArc)) |
| ctx |- matchShape(ts, basicArc {0, n}) = (ctx.typing,{},ts) |
| basicArc_bounded2 | n > 0 removeTriple(ts) = (t,ts') matchArc(t,basicArc) = t1 ctx |- matchShape(ts', basicArc {0, n - 1}) = (t2,cs,rs) |
| ctx |- matchShape(ts, basicArc {0, n}) = (combineTypings(t1,t2), addTriple(t,cs), rs) |
If the cardinality if {m, n} it matches if there is one triple that matches and if the rest of triples match with the cardinality {m - 1, n - 1}
| BasicArc_bounded3 | m > 0, n >= m removeTriple(ts) = (t,ts') matchBasicArc(t, basicArc) = t1 ctx |- matchShape(ts', basicArc {m-1, n-1} ) = (t2, cs, rs) |
| ctx |- matchShape(ts, basicArc {m, n}) = (combineTypings(t1,t2), addTriple(t,cs), rs) |
If the shape is a conjunction it matches if it matches the first element and then, the second with the remaining triples
| And | ctx |- matchShape(ts, e1) = (t1, cs1, rs1) ctx |- matchShape(ts, e2) = (t2, cs2, rs2) |
| ctx |- matchShape(ts, And(e1, e2) = (combineTypings(t1,t2), cs1 union cs2, rs1 intersection rs2) |
If the shape is a disjunction it matches if either the first element matches or the second one does
| Or_1 | ctx |- matchShape(ts, e1) = (t, cs, rs) |
| ctx |- matchShape(ts, Or(e1,e2) = (t, cs, rs) |
| Or_2 | ctx |- matchShape(ts, e2) = (t, cs, rs) |
| ctx |- matchShape(ts, Or(e1,e2) = (t, cs, rs) |
This section covers how to match a basic Arc: ctx|-matchBasicArc(triple,basicArc).
There are two cases: direct arcs match the value with the object of the triple while inverse arcs match the value with the subject the triple
| ObjectArc | ctx |- >matchValue(o,v) = t |
| ctx |- matchBasicArc(<s,p,o>, Arc p v) = t |
| SubjectArc | ctx |- >matchValue(s,v) = t |
| ctx |- matchBasicArc(<s,p,o>, InvArc p v) = t |
A term matches if it belongs to the set of allowed values
| AllowedValue | x ∈ set |
| ctx |- matchValue(x, AllowedValue(set)) = ctx.typing |
A node type matches if the RDF term if of the corresponding kind
hasKind(node,URI) must be better defined
or described. An example would be hasKind(rdfs:label,sh:IRI)
| nodeType | hasKind(x,t) |
| ctx |- matchValue(x, NodeType t) = ctx.typing |
A data type matches if the literal datatype matches
hasDatatype(node,URI) must be defined
or described. An example would be hasDatatype("23"^^xsd:integer,xsd:integer)
| dataType | hasDatatype(x,t) |
| ctx |- matchValue(x, Datatype t) = ctx.typing |
Add a construct to match language tagged literals
ValueShape handles references to shapes. There are two cases, the first initial case, when the context already contains the declaration that x has shape label just evaluates to the current typing.
| valueShape_1 | contains(ctx.typing, x, label) |
| ctx |- matchValue(x, ValueShape(label)) = ctx.typing |
The second case, when the context does not contain the declaration that x has the shape label is solved by trying to match x with shape label in the graph.
| valueShape_2 | not(contains(ctx.typing, x, label)) ctx |- matchNode(x,v) = (t,_,_) |
| ctx |- matchValue(x, ValueShape(label)) = t |
noMatchArcAny takes a set of triples and a basic arc and checks that there is no triple that matches the basic arc
It has two possibilities.
| noMatchAny_1 | |
| ctx |- noMatchAny({}, basicArc) |
| noMatchAny_2 | removeTriple(ts) = (t,ts') ctx |- noMatchBasicArc(t,basicArc) ctx |- noMatchAny(ts',basicArc) |
| ctx |- noMatchAny(ts, basicArc) |
noMatchBasicArc succeeds if the basic arc doesn't match.
If the predicates are different, it succeeds
| noMatchBasicArc_1 | p ≠ p' |
| ctx |- noMatchBasicArc(<s,p,o>, Arc p' v) |
If the predicates are the same it succeeds if the value doesn't match. There are two cases depending on direct/inverse arcs
| noMatchSubjectArc | ctx |- noMatchValue(o,v) |
| ctx |- noMatchBasicArc (<s,p,o>, Arc p v) |
| noMatchObjectArc | ctx |- noMatchValue(s,v) |
| ctx |- noMatchBasicArc(<s,p,o>, InvArc p v) |
It succeeds if the value doesn't match with the node.
| noAllowedValue | x ∉ set |
| ctx |- noMatchValue(x, AllowedValue(set)) |
| noNodeType | hasNoKind(x,t) |
| ctx |- noMatchValue(x, NodeType t) = ctx.typing |
It matches if the literal doesn't match the data type
| noDataType | hasNoDatatype(x,t) |
| ctx |- noMatchValue(x, Datatype t) = ctx.typing |
noValueShape handles references to shapes. There are two cases, the first initial case, when the context already contains the declaration that x has shape label just evaluates to the current typing.
Review definition of noValueShape.
In order to handle issues with recursive shapes and negation,
the previous definition can be expressed using negation as failure
or augmenting the axiomatic definition with negative typing assertions.
Typing assertions can have three values: true, false or unknown.
We would like to acknowledge the contributions of Peter F. Patel-Schneider, Eric Prud'hommeaux, Iovka Boneva and the other members of the W3c Data Shapes Working group.