- isValid: For a graph G, a schema Sch and a fixed ShapeMap ism, isValid(G, Sch, ism) indicates that for every RDFnode/shapeLabel pair (n, sl) in ism, the node n satisfies the shape expression identified by sl.
- The latter is captured by the expression satisfies(n, s, G, Sch, completeTyping(G, Sch)).
+ isValid: For a graph G, a schema Sch and a fixed ShapeMap ism, isValid(G, Sch, ism) indicates that for every RDF node/shapeLabel pair (n, sl) in ism, the node n satisfies the shape expression identified by sl.
+ The latterThis is captured by the expression satisfies(n, s, G, Sch, completeTyping(G, Sch))where s is the shape expression identified by sl.
The function satisfies is defined for every kind of shape expression.
The validation of an RDF graph G against a ShEx schema Sch is based on the existence of completeTyping(G, Sch).
- For an RDF graph G and a shapes schema Sch, a typing is a set of pairs of the form (n, s) where n is a node in G and s is a Shape that appears in some shape expression in the shapes mapping of Sch.
- A correct typing is a typing such that for every RDFnode/shape pair (n,s) in typing, matchesShape(n, s, G, Sch, typing) holds.
+ For an RDF graph G and a shapes schema Sch, a typing is a set of pairs of the form (n, s) where n is a node in G and s is a Shape that appears in some shape expression in Sch.shapes.
+ A correct typing is a typing such that for every RDF node/shape pair (n,s) in typing, matchesShape(n, s, G, Sch, typing) holds.
completeTyping(G, Sch) is a unique correct typing that exists for every graph and every ShEx schema that satisfies the schema requirements.
@@ -506,14 +517,14 @@
Validation Definition
- completeTypingOn(1, G, Sch) is the union of all correct typings that contain only RDFnode/shape pairs (n,s) with stratum(s) = 1;
+ completeTypingOn(1, G, Sch) is the union of all correct typings that contain only RDF node/shape pairs (n,s) with stratum(s) = 1;
for every i between 2 and k, completeTypingOn(i, G, Sch) is the union of all correct typings that:
-
contain only RDFnode/shape pairs (n,s) with stratum(s) ≤ i
+
contain only RDF node/shape pairs (n,s) with stratum(s) ≤ i
-
are equal to completeTypingOn(i-1, G, Sch) when restricted to their RDFnode/shape pairs (n1,s1) for which stratum(s1) < i.
+
are equal to completeTypingOn(i-1, G, Sch) when restricted to their RDF node/shape pairs (n1,s1) for which stratum(s1) < i.
This property is reminiscent of the use of stratified negation in Datalog.
- In order to decide isValid(Sch, G, m), it is sufficient to compute only a portion of completeTyping using an appropriate algorithm.
+ In order to decide isValid(Sch, G, m), it is sufficient to compute only a portion of the complete typing using an appropriate algorithm.
- A shape expression is composed of four kinds of objects combined with the algebraic operators And, Or and Not:
+ A shape expression is composed of four kinds of objects combined with the algebraic operators `And`, `Or` and `Not`:
- a node constraint (NodeConstraint) that defines the set of allowed values of a node.
+ A node constraint (NodeConstraint) defines the set of allowed values of a node.
These include specification of RDF node kind, literal datatype, XML String and numeric facets and enumeration of value sets.
- a shape constraint (Shape) that defines a constraint on the allowed neighbourhood of a node, that is, the allowed triples that contain this node as subject or object.
+ A shape constraint (Shape) defines a constraint on the allowed neighbourhood of a node, that is, the allowed triples that contain this node as subject or object.
- an external shape (ShapeExternal) which is an extension mechanism to externally define e.g. functional shapes or prohibitively large value sets.
+ An external shape (ShapeExternal) is an extension mechanism to externally define e.g. functional shapes or prohibitively large value sets.
In this ShapeOr's shapeExprs, "http://schema.example/#IssueShape" is a reference to the shape expression with the id "http://schema.example/#IssueShape".
-
+
+
+
Preliminary defintions
+
+
+ Consider a fixed schema `Sch`.
+
+
+
+ A schema MUST NOT contain any shapeExprLabel that has a negated reference to itself, either directly or transitively.
+ This is formalized by the requirement that the dependency graph of a schema MUST NOT have a cycle that traverses some negated reference.
+ Is this (partially) redundant against the stratification?
+
+
+
+ We construct a graph which nodes are the shapeExprLabels that appear in `Sch`.
+ We say that a label `L` has a reference to a label `L'` if there exists a TripleConstraint `tc` in `tcs(def(L))` such that a shapeExprRef `L'` appears in tc.valueExpr either directly or by traversing any ShapeAnd, ShapeOr, ShapeNot, tripleExprRef, in te TripleContraint's valueExpr, but without traversing shapeExprRefs.
+ A reference is a negated reference if:
+
+
+
+
an odd number of ShapeNot is traversed before reaching `tc`, or
+
an odd number of ShapeNot after tc.valueExpr, or
+
[TODO : something about extra]
+
+
+
+ The dependency graph ... as before, using negated reference.
+
+
-
Semantics
+
Semantics
+
+
+ For a shape expression `se` we define its set of shapes `shapes(se)` recursively on the structure of `se`:
+
+
+
if `se` is a NodeConstraint, then `shapes(se) = emptyset`
+
if `se` is a Shape, then `shapes(se) = {se}`
+
if `se` is a ShapeNot, then `shapes(se) = shapes(se.shapeExpr)`
+
if `se` is ShapeAnd or ShapeOr, then `shapes(se)` is the union of the sets `shapes(se')` for all `se'` in `se.shapeExprs`
+
if `se` is a shapeExprRef with label `L`, then `shapes(se) = shapes(def(L))`
+
+
+
+
For a tripleExpr `te` we define its set of TripleConstraints `tcs(te)` recursively on the structure of `te`:
+
+
if `te` is a TripleConstr, then `tcs(te)` is the singleton set `{te}`,
+
if `te` is OneOf or EachOf, then `tcs(te)` is the union of the sets `tcs(te')` for all the `se'` in `te.trileExprs`
+
if `te` is a tripleExpreRef with label `L`, then `tcs(te) = tcs(def(L))`
+
+
+ For a Shape `s`, we define `tcs(s) = tcs(s.expression)`.
+
+
+ For a shapeExpr `se`, we define `tcs(se)` as the union of the sets `tcs(s)` for all Shape `s` in `shapes(se)`.
+
+
+Finally, for a triple expression or a shape expression `e` we define `predicates(e)` as the set that contains exactly the `tc.predicate` for all the TripleConstraints `tc` in `tcs(e)`.
+
+
+
Definition of extension hierarchy graph
+
+
+ A shape expression label is called abstract if its definition is marked with `ABSTRACT`.
+ For shape expression labels `L_1`, `L_2`, we say that `L_2` directly extends `L_1` if `shapes(def(L_2))` contains a Shape `s` s.t. `s.extends` contains `L_2`.
+The extension hierarchy graph of a shapes schema is a directed graph which nodes are the shape expression labels of the schema and that has an edge from `L_2` to `L_1` whenever `L_2` directly extends `L_1`.
+
+
+
+
+ Schema requirement: the extension hierarchy graph must be acyclic.
+
+
+ For a shape label `L`, we define
+
+
+
the set `supertypes(L)` is the set of labels `L'` such that there is a possibly empty path from `L` to `L'` in the extension hierarchy graph,
+
the set `baseSubtypes(L)` is the set of labels `L'` which definition is not abstract, and s.t. there is a possibly empty path from `L'` to `L` in the extension hierarchy graph.
+
+
+ Note that because an empty path is allowed in the above definitions, every label belongs to its set of supertypes and every non abstract label belongs to its set of base subtypes.
+
+
+
+
Definition of *extendable shape expression*
+
+A shapeExpr is called *extendable* if:
+
+
+
it is named, say with label `L`,
+
it is of the form either `s` or `s AND se`, where `s` is a Shape and `se` is a shapeExpr. In this case we denote `s` as `mainShape(L)` and `se` as `constraint(L)`:
+
`se` does not contain an EXTENDS, that is, `s'.extends` is empty for every `s'` in `shapes(se)`,
+
`def(L')` is an extendable shape expression for every `L'` in `s.extends` (note that this condition is trivially met when `s.extends` is empty),
+
the set `predicates(se)` is included the union of the sets `predicates(mainShape(L'))` for all shape expression names `L'` that belong to `supertypes(L)`.
+
+
+Note that a named Shape is always an extendable shape expression.
+
+
+For an extendable shape expression with label `L` we define:
+
+
+
`superTcs(L)` as the union of the sets `tcs(mainShape(L'))` for all shape expression names `L'` that belong to `supertypes(L)`,
+
`superPredicates(L)` as the union of the sets `predicates(mainShape(L'))` for all shape expression names `L'` that belong to `supertypes(L)`.
+
+
+ Schema requirement EXTENDS appears only in extendable shape expressions. That is, for every Shape `s` that appears in the schema, if `s.extends` is non empty and for every shapeExpr `se` in the schema, if `s` belongs to `shapes(se)`, then `se` is an extendable shape expression.
+
+
+
+
Stratified schema
+
+ [TODO precise definition + how negation and stratification are to be adapted]
+
+
+Briefly: stratification is defined on shape expression labels (and not on Shapes as it used to be).
+
+
+# Semantics
+@@Indicates this should be moved?
+
+
+
+
Definitions
+
+Consider a ShEx schema `Sch` and a graph `G`, and let `U` be the set of shape expression labels of `Sch` and `N` be the set of nodes of `G`.(TODO : which labels to consider ? Only the top level ones, or any label ?)
+Then a *typing* over `G` and `Sch` is a subset of `N x U`.
+
+
+The satisfaction of the schema is defined w.r.t. a so called maximal typing, which is guaranteed to exist.
+The maximal typing is such that whenever `(n,L)` belongs to it, it holds that the neighborhood of the node `n` *satisfies* `def(L)` w.r.t. the maximal typing. Formally, `satisfies(G, Sch, maximalTyping, n, def(L), _)` holds, where `satisfies` is the function defined below and the underscore indicates that no value is given for the corresponding optional parameter.
+
+
+
+
The satisfies function
+
+It takes six parameters: the graph `G`, the schema `Sch`, a typing `typing` over `G` and `Sch`, a node `n` in `G`, a shapeExpr `se` from `Sch`, and an optional neighborhood set of triples `npart` : `satisfies(n, se, typing, npart, G, Sch)`. The value of the function is a Boolean. The function is defined recursively on the structure of the shape expression:
+
+
+[TODO : fix the order of the parameters in the satisfies function as it is not always the same]
+
+
+
`se` is node constraint and `satisfies2(n, se)` ... as before
+
`se` is ShapeOr and `satisfies(n, se', typing, npart, G, Sch)` holds for some `se'` in `se.shapeExprs`
+
`se` is a ShapeNot and `satisfies(n, npart, se, typing, G, Sch)` does not hold
+
`se` is a ShapeExternal and implementation-specific mechanisms not defined in this specification indicate success
+
`se` is a shapeExprRef with label `L` and `satisfies(n, npart, def(L), typing, G, Sch)` **[Note : here we unfold the definition of L and do not look for base subtypes. Base subtypes are considered only for the whole neighborhood, that is in TripleConstr]**
+
`se` is an extendible shape expression, let `L` be the label of `se`. Let `neigh = npart` if `npart` is given, or `neigh` be the neighbourhood of the node `n` is `npart = _`. Then
+
there exist sets of triples `matchables`, `unmatchables` and `remainder` s.t.
+
`matchables`, `unmatchables` and `remainder` are pairwise dijoint and their union is equal to `neigh`,
+
`remainder` is the set of triples from the neighborhood of `n` whose predicates do not appear neither in `superPredicates(L)` nor in `mainShape(L).extra`
+
if `mainShape(s).closed`, then `remainder` is empty
+
`matchables` contains all the triples `t` s.t. `matches(n, {t}, tc, typing, G, Sch)` holds for some `tc` in `superTcs(L)`,
+
(therefore, `unmatchables` contains all the triples `t` whose predicate is in `superPredicates(L)` or in `mainShape(L).extra`, and such that `matches(n, {t}, tc, typing)` does not hold for no `tc` in `superTcs(L)`),
+
all predicates in `unmatchables` appear in `mainShape(L).extra`,
+
there exists a partition of `matchables` that with every `L'` in `supertypes(L)` associates a set of triples denoted `npart(L')` s.t.
+
+
`matchables` is the union of the sets `npart(L')` for all the `L'`s in `supertypes(L)` and these sets are mutually disjoint,
+
`matches(n, npart(L'), mainShape(L').tripleExpr, typing, G, Sch)` holds for every `L'` in `supertypes(L)`,
+
`satisfies(n, supernpart(L'), constraint(L'), typing, G, Sch)` holds for every `L'` in `supertypes(L)` whenever `constraint(L')` exists, where `supernparts(L')` is the union of the `npart(L'')` for all the shape expression labels `L''` in `supertypes(L')`
+
`se` is a ShapeAnd without EXTENDS and `satisfies(n, se', typing, npart, G, Sch)` holds for every `se'` in `se`.shapeExprs
+
satisfies: The expression satisfies(n, se, G, Sch, t) indicates that a node n and a graphG satisfy a shape expressionse with typingt for schema Sch. notSatisfies: Conversely, notSatisfies(n, se, G, Sch, t) indicates that n and G do not satisfy se with the given typingt.
@@ -683,7 +854,7 @@
+ It takes six parameters: the graph `G`, the schema `Sch`, a typing `t` over `G` and `Sch`, a node `n` in `G`, a tripleExpr `te` from `Sch`, and a (non optional) neighborhood set of triples `npart` : `matches(n, te, typing, npart, G, Sch)`.
+ The value of the function is a Boolean. The function is defined recursively on the structure of the triple expression:
+
+
+
`te` is a TripleConstraint and `npart` is a singleton set with unique triple `t` and the predicate of `t` is the same as the predicate of `te` and ... TODO define inverse or not as before ... and:
+
+
`te` does not have a `valueExpr`, or
+
`te` has a valueExpr that is a shapeExprRef with label `L` and **there exists a label `L'` in `baseSubtypes(L)` such that `(n', L')` belongs to `typing` (note: this is the unique place in the recursive definition of the semantics where substitutability is considered.
+ Substitution is also considered when validating a shape map)**, or
+
`te` has a valueExpr that is not a shapeExprRef, then `satisfies(n', te.valueExpr, typing, _, G, Sch)` holds, where `n'` is the object ( ... TODO ... or the subject if inverse ) of `t`
+
+
+
+
`te` is tripleExprRef with label `L`, and `matches(n, def(L), typing, npart, G, Sch)` holds
+
`te` has a cardinality `[min, max]` and `npart` can be partitioned into `k` pairwise disjoint sets `npart_1` ... `npart_k` for some `min <= k <= max` and `matches(n, te, typing, npart_i, G, Sch)` for every `i` in `1..k`
+
`te` is a OneOf and `matches(n, te', typing, npart, G, Sch)` for some `te'` in `te`.tripleExprs
+
`te` is EachOf and `matches(n, te', typing, npart, G, Sch)` for every `te'` in `te`.tripleExprs
+
+
+
+
Validating a shape map
+
+ A shape map is ... TODO precise definition ... a kind of a typing, i.e. a set of pairs `(n, L)` where `n` is a node and `L` is a shape expression label.
+ A shape map is satisfied if for every `(n, L)` in the map, there exists a label `L'` in `baseSubtypes(L)` s.t. `(n', L')` belongs to the maximal typing
+
+
+
+
Definition of the maximal typing
+
+ *Similar to before, through stratification, but now the elements of the typing are pairs (node, label) where label is a **shapeExprLabel**. Before we had pairs (node, Shape) in the typing. With this new definition of typing the stratification is easier to define. What we lose is that some schemas that would have been considered stratified with the old definition won't be considered stratified with the new one. This breaks backwards compatibility, provided that there exists somewhere a schema with negations that has non trivial stratification structure, ... which would surprise me a lot*.
+
matches: asserts that a triple expression is matched by a set of triples that come from the neighbourhood of a node in an RDF graph.
The expression matches(T, expr, m) indicates that a set of triples T can satisfy these rules:
@@ -2258,7 +2463,7 @@
Negation Requirement
- The dependency graph of the schema Sch is the graph which vertices are all the Shapes that appear in some shape expression in the shapes of Sch, and that has two kinds of edges: negative and positive.
+ The dependency graph of the schema Sch is the graph whose vertices are all the Shapes that appear in some shape expression in the shapes of Sch, and that has two kinds of edges: negative and positive.
There is a negative edge from s1 to s2 if s1 has a negated reference to s2.
There is a positive edge from s1 to s2 if s1 has a reference but not a negated reference to s2.
+ As with Turtle and SPARQL, ShExC offers URL resolution relative to a base per [[RFC3986]] and prefixes map to provide shorthand ways to write IRI identifiers.
+
When used in a prefixDecl production, the prefix is a potentially empty unicode string matching the first argument of the rule and serves as a key into the prefixes map.
When used in a prefixDecl production, the prefix is a potentially empty unicode string matching the first argument of the rule and serves as a key into the prefixes map.
+