-
Notifications
You must be signed in to change notification settings - Fork 9
Expand file tree
/
Copy pathalgorithms.html
More file actions
840 lines (665 loc) · 46.4 KB
/
Copy pathalgorithms.html
File metadata and controls
840 lines (665 loc) · 46.4 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="utf-8"/>
<meta name="viewport" content="width=device-width"/>
<title>Algorithms for Static Analysis and Validation of the Shape Expressions Language</title>
<link rel="stylesheet" href="local.css"/>
<script src='https://www.w3.org/Tools/respec/respec-w3c-common'
defer class='remove'></script>
<!-- script src='../primer/respec-w3c-common.js' async class='remove'></script -->
<script src="jquery-2.1.4.min.js" type="text/javascript"></script>
<script type="text/javascript" src="scripts.js"></script>
<script class='remove'>
var respecConfig = {
localBiblio: {
"shex-spec" : {
"authors": ["Eric Prud'hommeaux", "Iovka Boneva", "Jose Emilio Labra Gayo", "Gregg Kellogg"],
"title": "Shape Expressions Language 2.next",
"href": "index.html"
},
"shex-vocab": {
"authors": ["Gregg Kellogg"],
"title": "Shape Expression Vocabulary",
"href": "http://www.w3.org/ns/shex#"
},
"shape-map": {
"authors": ["Eric Prud'hommeaux", "Thomas Baker"],
"title": "ShapeMap Structure and Language",
"href": "http://shex.io/shape-map/"
},
"shex-complexity": {
"authors": ["Iovka Boneva", "Jose Emilio Labra Gayo", "Eric Prud'hommeaux", "S\u0142awek Staworko"],
"title": "Complexity and Expressiveness of ShEx for RDF",
"href": "https://drops.dagstuhl.de/opus/volltexte/2015/4979/"
}
},
specStatus: "CG-DRAFT",
shortName: "shex-algorithms",
latestVersion: "",
thisVersion: "",
prevVersion: "",
edDraftURI: "",
previousPublishDate: "",
previousMaturity:"",
testSuiteURI: "",
issueBase: "",
githubAPI: "",
editors: [
{ name: "Iovka Boneva",
url: "http://cristal.univ-lille.fr/~boneva/",
company: "University of Lille",
companyURL: "http://www.univ-lille1.fr/" },
{ name: "Jérémie Dusart",
company: "Inria",
companyURL: "http://www.inria.fr/" },
],
wg: "Shape Expressions Community Group",
wgURI: "https://www.w3.org/community/shex/",
wgPublicList: "public-shex",
//wgPatentURI: "https://www.w3.org/2004/01/pp-impl/73865/status",
bugTracker: {
open: "https://github.com/shexSpec/shex/issues",
new: "https://github.com/shexSpec/shex/issues/new"
},
otherLinks: [{
key: "Version control",
data: [{
value: "Github Repository",
href: ""
}]
}],
postProcess: [ expandPinRefs, initPinHighlights ],
};
</script>
</head>
<body>
<section id="abstract">
<p>
The <a href="index.html">Shape Expressions (ShEx) language</a> describes <a>RDF nodes</a> and <a>graph</a> structures, organized in a shapes schema.
A shapes schema must comply to a series of <a href="index.html#schema-requirements">requirements</a>.
</p>
<p>
This document presents the algorithms that allow to test whether a syntactically correct shapes schema satisfies the requirements.
It also presents algorithms for validating an RDF graph against a ShEx schema that satisfies the requirements.
</p>
</section>
<section id="sotd">
<p>This document is being developed by the
<a href="https://www.w3.org/community/shex/">Shape Expressions Community Group</a>.
</p>
<p>
This version is an editor's draft.
</p>
</section>
<section id="introduction">
<h2>Introduction</h2>
</section>
<section id="schema-requirements">
<h2>Algorithms for Checking the Schema Requirements</h2>
<section id="shape-expr-ref">
<h3>Shape Expression Reference Requirement</h3>
<p>
The <a href="index.html#shapeExprRef-requirement">definition of this requirement</a> is in the shape expressions language specification.
</p>
<p>For a ShEx schema <span class="math">sch</span>, let <span class="math">ShapeExprIds(sch)</span> be the set of shape expression identifiers in <span class="math">sch</span>.</p>
<p>
The dependency graph traced by this requirement records the <em>same-node</em> dependencies: an edge from <span class="math">se</span> to <span class="math">se'</span> means that deciding whether a node satisfies <span class="math">se</span> immediately requires deciding whether that <em>same</em> node satisfies <span class="math">se'</span>.
The operands of <code>ShapeAnd</code>, <code>ShapeOr</code> and <code>ShapeNot</code> and the target of a shape expression reference are such dependencies.
So is each shape expression named in a Shape's <code>EXTENDS</code> clause: a node conforms to an extending Shape only if a split of the node's own neighbourhood satisfies every extended shape expression, so the dependency is not mediated by any triple constraint — it behaves like an additional conjunct.
A Shape's <em>triple expression</em>, by contrast, contributes no edges here: the value expressions inside it constrain <em>other</em> nodes (the triples' objects), and those dependencies are the subject of the <a href="#negation">negation requirement</a>.
</p>
<p>Algorithm checkShapeExpressionReferenceRequirement</p>
<pre><code>
Input: sch: a schema
Output: true sch satisfies the shape expression reference requirement, false otherwise
whenever the latter is true, produces also D: the shape expressions dependency graph induced by sch
let ShapeExprIds be the set of all shape expression ids in sch
let ShapeExprRefs be the set of all shape expression references in sch
if shapeExprRefs is not included in shapeExprIds then return false
initiate a directed edge labelled graph D which nodes are all Shape, NodeConstraint, ShapeNot, ShapeOr, ShapeAnd and shapeExprRef elements that appear in sch
foreach ShapeExpr se in the vertex set of D
if se is a ShapeOr or a ShapeAnd then
foreach ShapeExpr sub in se.shapeExprs
add to D an edge from se to sub labelled with pos
else if se is a ShapeNot then
add to D an edge from se to se.shapeExpr labelled with neg
else if se is a shapeExprRef then
add to D an edge from se to shapeExprWithId(se) labelled with pos
<mark>else if se is a Shape then
foreach ShapeExpr ext in se.extends
add to D an edge from se to ext labelled with pos</mark>
if D contains a cycle then
return false
else
return (true, D)
</code></pre>
<p>
Because <em>every</em> cycle in <span class="math">D</span> is rejected — whether or not it traverses a <span class="math">neg</span>-labelled edge — an <code>EXTENDS</code> cycle (<span class="math">S</span> extends <span class="math">T</span>, <span class="math">T</span> extends <span class="math">S</span>) is ill-formed even without negation: it defines conformance to <span class="math">S</span> in terms of itself with no triple constraint in between to ground the recursion.
When such a cycle does traverse a negation, the schema is not merely ungrounded but contradictory, as the following example shows.
</p>
<section id="extends-negation-example">
<h4>Worked Example: a Paradox through EXTENDS and NOT</h4>
<p>
The following schema is the shexTest suite's <a href="https://github.com/shexSpec/shexTest/blob/main/negativeStructure/Cycle2ExtendsNegation.shex"><code>negativeStructure/Cycle2ExtendsNegation</code></a> test.
Without the highlighted <code>EXTENDS</code> rule above, it slips through the requirement checks: the reference from <code>:T</code> back to <code>:S</code> sits directly in <code>:T</code>'s shape expression (no triple constraint mediates it), so the <a href="#negation">negation requirement</a>'s dependency graph — which only traces dependencies through triple constraints' value expressions — never sees the cycle.
</p>
<div class="example">
<div class="exsec">Schema (<code>Cycle2ExtendsNegation.shex</code>):</div>
<pre class="nohighlight">PREFIX : <http://example.org/>
:S EXTENDS @:T {}
:T NOT @:S</pre>
</div>
<p>
The dependency graph <span class="math">D</span> has the cycle:
</p>
<pre class="nohighlight">Shape(:S) --pos (EXTENDS)--> @:T --pos--> ShapeNot(:T) --neg--> @:S --pos--> Shape(:S)</pre>
<p>
so <span class="math">checkShapeExpressionReferenceRequirement</span> returns <span class="math">false</span> and the schema is rejected.
</p>
<p>
To see why it must be, suppose the schema were admitted and validate any node at all — say <span class="math">n</span> in the one-triple graph:
</p>
<div class="example">
<div class="exsec">Data:</div>
<pre class="nohighlight">PREFIX : <http://example.org/>
:n :p 1 .</pre>
</div>
<p>
Write <span class="math">S(n)</span> for “<span class="math">n</span> satisfies <code>:S</code>” and <span class="math">T(n)</span> likewise.
Unfolding the definitions:
</p>
<ul>
<li>
<span class="math">S(n)</span> holds iff some split of <span class="math">n</span>'s neighbourhood lets the extended <code>@:T</code> accept its share and the local triple expression <code>{}</code> accept the rest.
<code>{}</code> is not <code>CLOSED</code> and constrains nothing, and <code>:T</code>'s shape expression contains no triple constraints either, so the split is immaterial: <span class="math">S(n) ⇔ T(n)</span>.
</li>
<li>
<span class="math">T(n)</span> holds iff <span class="math">n</span> does <em>not</em> satisfy <code>:S</code>: <span class="math">T(n) ⇔ ¬S(n)</span>.
</li>
</ul>
<p>
Chaining the two: <span class="math">S(n) ⇔ ¬S(n)</span> — the liar's paradox.
No assignment of conformance is consistent, for <em>any</em> node in <em>any</em> graph:
</p>
<ul>
<li>
A validator that tests <code>:n</code> against <code>:S</code> and, on encountering the recursion, <em>assumes the pending</em> <span class="math">S(n)</span> <em>fails</em>, concludes <span class="math">T(n)</span> holds — and therefore that <span class="math">S(n)</span> <em>succeeds</em>, contradicting its assumption.
</li>
<li>
Assuming instead that the pending <span class="math">S(n)</span> succeeds makes <span class="math">T(n)</span> fail — and therefore <span class="math">S(n)</span> fail, again contradicting the assumption.
</li>
</ul>
<p>
So the verdict depends entirely on the order of evaluation and the guess made at the recursion, and each guess refutes itself: <code>:n</code> is “both valid and invalid”.
The same contradiction defeats <a href="#refine-validation">refine validation</a> before it starts: the schema admits no stratification, since <code>:S</code> and <code>:T</code> would occupy the same stratum across a negated dependency.
Rejecting the schema statically — here, by the cycle test on <span class="math">D</span> — is what keeps <span class="math">satisfies</span> well-defined.
</p>
</section>
</section>
<section id="triple-expr-ref">
<h3>Triple Expression Reference Requirement</h3>
<p>
The <a href="index.html#tripleExprRef-requirement">definition of this requirement</a> is in the shape expressions language specification.
</p>
</section>
<section id="negation">
<h3>Negation Requirement</h3>
<p>
The <a href="index.html#negation-requirement">definition of this requirement</a> is in the shape expressions language specification.
</p>
<p>Algorithm for computing the dependency graph of a schema.</p>
<p>
Since <span class="math">DSE</span> (computed by <span class="math">checkShapeExpressionReferenceRequirement</span>) contains an edge from each Shape to every shape expression in its <code>EXTENDS</code> clause, the paths followed below traverse extension hierarchies without further provision: <span class="math">atomicShapes(tc.valueExpr)</span> includes the extension bases of every Shape it reaches, with the count of <span class="math">neg</span>-labelled edges carried along the path.
For example, if <span class="math">tc.valueExpr</span> is <code>NOT @:S</code> and <code>:S</code> extends <code>:T</code>, the algorithm records <span class="math">neg</span>-labelled edges to both <code>:S</code> and <code>:T</code>.
</p>
<pre><code>
Input: schema a ShexSchema
Output: D the shape expressions dependency graph
let DSE be the dependency graph as computed by checkShapeExpressionReferenceRequirement
let DTE be the dependency graph as computed by checkTripleExpressionReferenceRequirement
let atomicTripleConstraints be the map that with every TripleExpression s.expression that appears in schema (for some Shape s) associates the set of TripleConstrants tc s.t. there is a path in DTE between s.expression and tc;
let atomicShapes be the map that with every ShapeExpression tc.valueExpr that appears in schema (for some TripleConstraint tc) associates the set of Shapes s s.t. there is path in DSE from tc.valueExpr to s
initiate a directed edge-labelled graph D with vertex set that contains all the Shapes in schema
foreach Shape s vertex of D s.t. s.expression is in the key set of atomicTripleConstraints
foreach TripleConstraint tc in atomicTripleConstraints(s.expression)
if tc.valueExpr is present then
foreach Shape s2 that belongs to atomicShapes(tc.valueExpr)
if there is at least one path in DSE from tc.valueExpr to s2 that traverses an odd number of neg-labelled edges then
add to D a neg-labelled edge from s to s2
else
add to D a pos-labeled edge from s to s2
return D
</code></pre>
<p>Algorithm for computing the stratification of a schema.</p>
<pre><code>
Input: schema a ShexSchema
Output: a map stratum from the set of Shapes in schema to natural numbers, or ERROR if the schema cannot be stratified
let D be the dependency graph of schema
if D contains a strongly connected component stc that contains a neg-labelled edge then
raise an error
let S be a directed graph which set of vertices is the set of strongly connected components of D
let L be a topological sorting of the vertices of S
foreach s node of D
let stratum(s) be the index in L of the unique strongly connected component stc s.t. s belongs to stc
return stratum
</code></pre>
</section>
</section>
<section id="validation">
<h2>Algorithms for Validation</h2>
<section id="matching-search">
<h3>Validation as a Search over Matchings</h3>
<p>
The algorithms in this section orchestrate calls to <span class="math">satisfies(n, s, G, sm)</span>: refine validation evaluates it for every (node, shape) pair, stratum by stratum; recursive validation evaluates it on demand.
When <span class="math">s</span> is a Shape with triple expression <span class="math">E</span>, deciding <span class="math">satisfies</span> is itself a search problem: does <em>some</em> assignment ("matching") of the relevant neighbourhood triples of <span class="math">n</span> to the triple constraints of <span class="math">E</span> satisfy <span class="math">E</span>'s cardinalities and grouping (EachOf, OneOf)?
With <code>EXTENDS</code>, the neighbourhood must additionally <em>split</em> among the shapes of the extension hierarchy so that every supertype's own triple expression accepts its share.
</p>
<p>
The direct reading of that decision problem is: <em>for each triple constraint, which triples could possibly satisfy it?</em> — a map from triple constraints to candidate triples.
But a matching is a <em>choice</em>, not a relation: every triple must end up assigned to exactly one triple constraint (or shown to be excused by <code>EXTRA</code> or absent altogether).
Turning the constraint-indexed relation into a triple-indexed <em>function</em> — one candidate constraint chosen per triple — is what makes "matching" a well-formed combinatorial object that can be enumerated, pruned and verified.
Three related structures recur below.
Given the neighbourhood triples <span class="math">T</span> of the node and the triple constraints <span class="math">TC</span> of a (possibly <code>EXTENDS</code>-composed) triple expression:
</p>
<dl>
<dt><dfn>pre-matching</dfn></dt>
<dd>
a map <span class="math">T → 2^{TC}</span>: with every triple, the set of triple constraints it <em>could</em> be assigned to — same predicate, and (recursively) the triple's value satisfies the constraint's value expression.
For a fixed triple constraint <span class="math">tc</span>, its candidate triples are recovered as <span class="math">{ t ∈ T : tc ∈ preMatching(t) }</span> — the "triple constraint → set of triples" view the reader may start from.
</dd>
<dt><dfn>matching</dfn></dt>
<dd>
a map <span class="math">T → TC</span> choosing, for every triple, exactly one of its pre-matching candidates.
A pre-matching is a compact representation of the set of matchings obtainable by choosing one candidate per triple — the Cartesian product <span class="math">∏_t preMatching(t)</span>.
The search is organized in this triple-indexed form because there, "assign every triple exactly once" is a syntactic guarantee rather than a side condition to check.
</dd>
<dt><dfn>split</dfn></dt>
<dd>
the inverse of a chosen matching: a map <span class="math">TC → 2^T</span> (or, grouped one level further, <span class="math">shapeLabel → 2^T</span> for an <code>EXTENDS</code> hierarchy) recovering, for a <em>specific</em> matching, which triples ended up on which constraint.
This is the view a cardinality check needs ("how many triples did <span class="math">tc</span> receive?"), and the view against which <code>EXTENDS</code> constraints and semantic actions are evaluated.
</dd>
</dl>
<p>Algorithm for deciding <span class="math">satisfies(n, s, G, sm)</span> for a Shape <span class="math">s</span>, by exhaustive enumeration of matchings.</p>
<pre><code>
Input: an RDF graph G, a node n, a Shape s with triple expression E, a shape map sm
Output: true if some matching of the relevant neighbourhood of n satisfies E, false otherwise
let TCs be the set of triple constraints of E (with EXTENDS, of every triple expression of the hierarchy)
let matchables be the set of triples (n,p,o) in G s.t. p is the predicate of some tc in TCs,
plus the triples (o,p,n) s.t. ^p is the predicate of some inverse tc in TCs
foreach t = (n,p,o) in matchables
let cands(t) = { tc in TCs : tc.predicate = p and
(tc has no valueExpr, or o satisfies tc.valueExpr under sm) }
foreach t in matchables with cands(t) = {}
if t.predicate is not in s.extra then return false
remove t from matchables
foreach matching m in the Cartesian product over t in matchables of cands(t)
let bag(m) be the map tc -> number of triples t s.t. m(t) = tc
if bag(m) is accepted by E then // exact check: cardinalities, EachOf grouping, OneOf choice
return true // m also fixes the split consumed by EXTENDS
// constraints and by semantic actions
return false
</code></pre>
<p>
The enumeration line is a Cartesian product: <span class="math">k</span> triples with 2 candidates each yield <span class="math">2^k</span> candidate matchings, and whenever triple constraints share a predicate — across OneOf alternatives, across the shapes of an <code>EXTENDS</code> hierarchy, or between a shape and its <code>EXTRA</code>-tolerated context — most of those matchings are doomed for reasons visible long before each is individually verified.
<a href="#matching-pruning"></a> refines this algorithm with two pruning techniques that leave its answers — indeed its entire set of accepted matchings — unchanged.
</p>
</section>
<section id="refine-validation">
<h3>Refine Validation</h3>
<p>Algorithm for refine validation.</p>
<pre><code>
Input: an RDF graph G, a ShexSchema schema which set of shapes is S
Output: the shape map completeTyping(G,sch)
let stratum=stratification(sch)
let k be the greatest number in the range of stratum
let typing be the empty set
for i in 0 .. k do
let shapes-i be the set of Shapes s in S s.t. stratum(s) = i
let typing-i = nodes(G) x shapes-i
do
changing = false
foreach (n,s) in typing-i do
if not matches(n,s,G,Sch,typing-i union typing)
remove (n,s) from typing-i
changing = true
while (changing)
add typing-i to typing
end for
return typing
</code></pre>
</section>
<section id="recursive-validation">
<h3>Recursive Validation</h3>
<p>Algorithm isValid(G,sch,n,se) for checking a unique node s against a unique shape expression s.</p>
<pre><code>
Input: RDF graph G, ShexSchema sch with set of Shapes S, node n in G, Shape s in sch, hyp: a stack over Nodes(G)xS
Output: true if satisfies(G,sch,n,s,completeTyping(G,sch)), false otherwise
push (n,s) on hyp
let sm be an empty shape map
let atomicTripleConstranits be the set of atomic triple constraints of s.expression
let neighbourhood be the set of (predicate,n2) s.t. either (n, predicate, n2) in G and predicate appears in a triple constraint in allTC, or (n2, predicate, n) in G and ^predicate appears in a triple constraint in allTC
for (pred,n2) in neighbourhood do
foreach tc in allTC
if tc.predicate == pred then
if tc.valueExpr is present then
foreach s2 in atomicShapes(tc.valueExpr)
if isValid(G,sch,n2,s2) then
add (n2,s2) to sm
add all elements of hyp to sm
result = satisfies(n,s,G,sm)
pop from hyp
return result
</code></pre>
<p>Recursive validation algorithm.</p>
<pre><code>
Input: an RDF graph G, a ShexSchema schema which set of shapes is S, an initial shapeMap map
Output: true if satisfies(n,s,G,sch,completeTyping(G,sch)) for every (n,s) in map, false otherwise
let sm be an empty shape map
foreach (n,se) in map
foreach Shape s in atomicShapes of se
if isValid(s,n,G,sch) then
add (n,s) to sm
if not satisfies(n,se,G,sch,sm) then
return false
return true
</code></pre>
</section>
<section id="matching-pruning">
<h3>Pruning the Matching Search</h3>
<p>
The two refinements below prune the enumeration algorithm of <a href="#matching-search"></a> without changing its answers: each only ever discards candidate matchings that the exact verification would also have rejected, so the set of accepted matchings — and everything downstream of it (<code>EXTENDS</code> splits, semantic actions) — is untouched.
Some search is unavoidable: for expressions with repeated triple constraints, deciding bag membership is NP-complete [[shex-complexity]], and even where polynomial decision procedures exist, a practical validator streams concrete witness matchings — of which there can be exponentially many — because downstream checks consume the specific triples matched.
Both refinements are implemented in Apache Jena's <code>jena-shex</code> module, from which the measurements below are taken.
</p>
<section id="negative-caching">
<h4>Negative Caching: Prune Refuted Candidate Pairs</h4>
<p>
The pre-matching construction already contains the first pruning: computing <span class="math">cands(t)</span> once, upfront, for every (triple, candidate constraint) pair — one recursive value-expression check per pair — and never revisiting a pair that failed.
Informally this is a <em>negative cache</em>: rather than re-discovering, inside every candidate matching that happens to try the pair again, that the triple's value does not satisfy the constraint, the failure is recorded once against the pre-matching itself and the pair never enters the search.
A validator that instead evaluates value expressions while walking each candidate matching re-pays that cost once per matching — multiplied by however many candidate matchings the <em>rest</em> of the neighbourhood generates (measured concretely in <a href="#soso-example"></a>).
</p>
<p>
The same contract generalizes from values to structure: a candidate can also be refuted because committing even one triple to it can never lead to an accepted matching — a co-occurrence obligation elsewhere in the expression that the data cannot meet, a OneOf exclusivity already violated, or a maximum cardinality already exceeded.
Both forms have the same shape: delete a <span class="math">(t, tc)</span> pair the moment it is known to appear in <em>no</em> accepted matching, so no refutation is ever derived twice.
The structural form is the subject of the next section.
</p>
</section>
<section id="bag-search">
<h4>Bag-Directed Search with Partial-Bag Refutation</h4>
<p>
Whether a triple expression accepts a matching depends only on the matching's <em>bag</em> — the count of triples assigned to each triple constraint; which specific triple went where matters only to downstream consumers (splits, semantic actions).
And once the pre-matching is computed, two triples with the same candidate set are interchangeable in any bag.
So: group the triples into <em>classes</em> by candidate set, and search over count vectors — how many triples of the class go to each of its candidates — instead of over individual assignments.
A class of <span class="math">n</span> triples over <span class="math">k</span> candidates has <span class="math">\binom{n+k-1}{k-1}</span> count vectors, polynomial in <span class="math">n</span> for fixed <span class="math">k</span>, in place of <span class="math">k^n</span> assignments.
Concrete matchings are produced only for bags that survive, by enumerating the multiset permutations within each class.
</p>
<p>
During the search, each triple constraint <span class="math">tc</span> carries an interval <span class="math">[lo(tc), hi(tc)]</span>: <span class="math">lo</span> counts the triples already committed to it by decided classes, and <span class="math">hi = lo +</span> the total size of the undecided classes that still offer <span class="math">tc</span> as a candidate.
A test <span class="math">refute(lo, hi)</span>, computed compositionally over the expression tree, answers: is <em>no</em> exact bag between <span class="math">lo</span> and <span class="math">hi</span> (pointwise) accepted?
It is a sound necessary-condition test — <em>true</em> proves the entire region hopeless, since every bag reachable by finishing the search lies between the current <span class="math">lo</span> and <span class="math">hi</span>, while <em>false</em> proves nothing and leaves the verdict to the exact verification of complete bags.
It accounts for minimum and maximum cardinalities, EachOf co-occurrence obligations, and OneOf exclusivity — including that exclusivity does not survive repetition: each iteration of <code>(:a . | :b .)+</code> chooses its alternative independently.
(The Jena implementation calls this test <em>feasibility</em>; this document says <em>refutation</em>, since refuting is the only verdict it delivers definitively.)
</p>
<p>
The test is applied at two moments.
Upfront, as an <em>arc-consistency</em> pass: for every candidate <span class="math">(t, tc)</span> pair, if committing a single triple to <span class="math">tc</span> is already refutable under the most optimistic <span class="math">hi</span>, delete <span class="math">tc</span> from the whole class at once — the structural generalization of negative caching.
And once per search node: after committing each class's count vector, either the remaining region is refuted (backtrack) or the search descends.
If arc consistency empties a class's candidate set, the shape fails outright: a triple that value-matches some constraint can never be left unmatched — <code>EXTRA</code> only excuses triples that matched no constraint to begin with.
</p>
<p>
Both refinements <em>delete</em>: the negative cache removes refuted <span class="math">(t, tc)</span> pairs from the <a>pre-matching</a> as it is built, and arc consistency removes candidates from whole classes at once.
The invariance stated above is about <em>accepted matchings</em>, and does not extend to the pre-matching itself: what survives pruning is a search state, not a description of the neighbourhood.
When a node cannot conform for any reason, refutation cascades, and that state can end with every triple's candidate set empty however much the node contains.
An implementation that also <em>reports</em> on failures — which triples had nowhere to go, how many of a property the node had, what would make it conform — must take those readings from the neighbourhood and the initial pre-matching, before the first deletion.
Read from the pruned state, they describe the search rather than the data.
</p>
<p>
<span class="math">refute</span> deliberately ignores constraints that per-constraint intervals cannot express: count coupling inside a repeated group (<code>(:a . ; :b .)+</code> requires equal counts of <code>:a</code> and <code>:b</code>) and divisibility (<code>(:a . {2,2})*</code> accepts only even counts).
Bags that survive are therefore always verified exactly, once, before acceptance; the refinement loses no correctness, only doomed work.
</p>
<p>The enumeration algorithm of <a href="#matching-search"></a>, with the refinement's additions <mark>highlighted</mark>:</p>
<pre><code>
Input: an RDF graph G, a node n, a Shape s with triple expression E, a shape map sm
Output: as for enumeration - the same matchings are accepted; only the work spent differs
let TCs, matchables and cands be as in the enumeration algorithm
// computing cands() once, upfront, is the negative
// cache: a refuted (t,tc) pair is never revisited
foreach t in matchables with cands(t) = {}
if t.predicate is not in s.extra then return false
remove t from matchables
<mark>partition matchables into classes: class(C) = { t : cands(t) = C }</mark>
<mark>repeat until no candidate is removed: // arc consistency</mark>
<mark> foreach class C and candidate tc of C</mark>
<mark> if refute(lo = one triple on tc, hi = every triple on all of its candidates)</mark>
<mark> remove tc from C's candidates</mark>
<mark>if some class has no candidates left then return false</mark>
<mark> // a triple that value-matches some tc can never be left unmatched,</mark>
<mark> // so EXTRA does not excuse a class emptied by refutation</mark>
<mark>search depth-first over the classes, fewest candidates first:</mark>
<mark> at each class C, enumerate the count vectors over C's candidates summing to |C|,</mark>
<mark> each count capped by the candidate's declared maximum</mark>
<mark> after committing a count vector: if refute(lo, hi) then backtrack</mark>
<mark>each leaf of the search determines a bag w over TCs</mark>
if w is accepted by E then // exact check, unchanged
<mark> foreach matching m realising w // multiset permutations within each class</mark>
return true // m fixes the split consumed by EXTENDS
// constraints and by semantic actions
return false
</code></pre>
</section>
<section id="soso-example">
<h4>Worked Example: a Science-on-Schema.org Dataset Profile</h4>
<p>
The following profile — modelled on the <a href="https://science-on-schema.org/">Science-on-Schema.org</a> guidance for schema.org <code>Dataset</code> descriptions — demonstrates both `negative caching` and `partial bag refutation`.
It uses a subset of real schema.org practice: repeated <code>creator</code> and <code>identifier</code> properties whose objects are choice types (<code>Person</code> or <code>Organization</code>; a <code>PropertyValue</code> or a plain string).
schema.org's repeated properties are <em>unordered repeated triples</em> — its JSON-LD context declares no <code>@list</code> containers, and order, where wanted, is modelled explicitly (<code>ItemList</code> with <code>position</code>) — so a node's neighbourhood carries one triple per value, which is precisely what exposes the repetition to the matching search.
Shape labels use the document-relative <code><#Label></code> pattern, resolved against the schema document's base IRI.
</p>
<p>
The profile accepts two conventions on each of two independent axes.
Creators: either a short list (one or two) of persons or organizations, or a longer list that must then include at least one ORCID-identified person (so someone is unambiguously citable and contactable).
Identifiers: either the dataset is identified by one or two DOIs — expressed, per the Science-on-Schema.org guidance, as <code>PropertyValue</code>s whose <code>propertyID</code> names the DOI registry — or it carries legacy string identifiers plus exactly one DOI.
Neither convention is declared explicitly; the validator works each out from what is present.
</p>
<div class="example">
<div class="exsec">Schema:</div><br/>
<pre class="line-labels nohighlight">
<span class="lineno schema pin S1">S1</span>
<span class="lineno schema pin te1">te1</span>
<span class="lineno schema pin tc1">tc1</span>
<span class="lineno schema pin tc2">tc2</span>
<span class="lineno schema pin tc3">tc3</span>
<span class="lineno schema pin te2">te2</span>
<span class="lineno schema pin tc4">tc4</span>
<span class="lineno schema pin tc5">tc5</span>
<span class="lineno schema pin tc6">tc6</span>
<span class="lineno schema pin S2">S2</span>
<span class="lineno schema pin S3">S3</span>
<span class="lineno schema pin S4">S4</span>
<span class="lineno schema pin S5">S5</span>
<span class="lineno schema pin S6">S6</span>
</pre>
<div class="inline shexc">
<pre class="nohighlight"><span class="keyword">PREFIX</span> schema: <span class="relativeIRI"><https://schema.org/></span>
<span class="keyword">PREFIX</span> xsd: <span class="relativeIRI"><http://www.w3.org/2001/XMLSchema#></span>
<span class="pin S1"><span class="relativeIRI"><#SOSODataset></span> {
<span class="pin te1">(
<span class="pin tc1">schema:creator @<span class="relativeIRI"><#Agent></span> {1,2}</span>
|
<span class="pin tc2">schema:creator @<span class="relativeIRI"><#Agent></span> + ;</span>
<span class="pin tc3">schema:creator @<span class="relativeIRI"><#OrcidPerson></span></span>
) ;</span>
<span class="pin te2">(
<span class="pin tc4">schema:identifier @<span class="relativeIRI"><#DoiPropertyValue></span> {1,2}</span>
|
<span class="pin tc5">schema:identifier xsd:string + ;</span>
<span class="pin tc6">schema:identifier @<span class="relativeIRI"><#DoiPropertyValue></span></span>
)</span>
}</span>
<span class="pin S2"><span class="relativeIRI"><#Agent></span> @<span class="relativeIRI"><#Person></span> <span class="keyword">OR</span> @<span class="relativeIRI"><#Organization></span></span>
<span class="pin S3"><span class="relativeIRI"><#Person></span> {
<span class="keyword">a</span> <span class="valueSet">[schema:Person]</span> ;
schema:name xsd:string
}</span>
<span class="pin S4"><span class="relativeIRI"><#Organization></span> {
<span class="keyword">a</span> <span class="valueSet">[schema:Organization]</span> ;
schema:name xsd:string
}</span>
<span class="pin S5"><span class="relativeIRI"><#OrcidPerson></span> {
<span class="keyword">a</span> <span class="valueSet">[schema:Person]</span> ;
schema:name xsd:string ;
schema:identifier <span class="pattern">/^https:\/\/orcid\.org\//</span>
}</span>
<span class="pin S6"><span class="relativeIRI"><#DoiPropertyValue></span> {
<span class="keyword">a</span> <span class="valueSet">[schema:PropertyValue]</span> ;
schema:propertyID <span class="valueSet">[<span class="string">"https://registry.identifiers.org/registry/doi"</span>]</span> ;
schema:value <span class="pattern">/^10\./</span>
}</span></pre>
</div>
<div style="clear:both;"></div>
</div>
<p>
@te1@ and @te2@ are the two OneOf groups.
@tc1@ and @tc2@ are the short-list and long-list creator constraints — value-indistinguishable, since any valid agent satisfies both — while @tc3@ demands an ORCID-identified person (@S5@).
On the identifier side the roles are mirrored: @tc4@ and @tc6@ share the DOI value expression (@S6@) and are indistinguishable from each other, but value-distinguishable from the plain-string constraint @tc5@.
@S2@ is the schema.org choice type: a creator may be a @S3@ person or a @S4@ organization.
</p>
<div class="example">
<div class="exsec">Data (conformant — a long creator list and a legacy identifier alongside the DOI):</div><br/>
<pre class="line-labels nohighlight">
<span class="lineno data pin t1">t1</span>
<span class="lineno data pin t2">t2</span>
<span class="lineno data pin t3">t3</span>
<span class="lineno data pin t4">t4</span>
<span class="lineno data pin t5">t5</span>
<span class="lineno data pin t6">t6</span>
<!-- <span class="lineno data">t7</span> -->
<!-- <span class="lineno data">t8</span> -->
<!-- <span class="lineno data">t9</span> -->
<!-- <span class="lineno data">t10</span> -->
<!-- <span class="lineno data">t11</span> -->
<!-- <span class="lineno data">t12</span> -->
<!-- <span class="lineno data">t13</span> -->
<!-- <span class="lineno data">t14</span> -->
<!-- <span class="lineno data">t15</span> -->
<!-- <span class="lineno data">t16</span> --></pre>
<div class="inline json">
<pre class="nohighlight"><span class="keyword">PREFIX</span> schema: <span class="relativeIRI"><https://schema.org/></span>
<span class="keyword">PREFIX</span> ex: <span class="relativeIRI"><http://example.org/datasets#></span>
<span class="pin t1">ex:dset1 <span class="keyword">a</span> schema:Dataset ;</span>
<span class="pin t2">schema:creator ex:alice ;</span>
<span class="pin t3">schema:creator ex:bob ;</span>
<span class="pin t4">schema:creator ex:noaa ;</span>
<span class="pin t5">schema:identifier <span class="string">"gov.noaa.ncdc:C00861"</span> ;</span>
<span class="pin t6">schema:identifier ex:doi1 .</span>
ex:alice <span class="keyword">a</span> schema:Person ;
schema:name <span class="string">"Alice Walker"</span> ;
schema:identifier <span class="string">"https://orcid.org/0000-0002-1825-0097"</span> .
ex:bob <span class="keyword">a</span> schema:Person ;
schema:name <span class="string">"Bob Ferris"</span> .
ex:noaa <span class="keyword">a</span> schema:Organization ;
schema:name <span class="string">"NOAA National Centers for Environmental Information"</span> .
ex:doi1 <span class="keyword">a</span> schema:PropertyValue ;
schema:propertyID <span class="string">"https://registry.identifiers.org/registry/doi"</span> ;
schema:value <span class="string">"10.7289/V5D21VHZ"</span> .</pre>
</div>
<div style="clear:both;"></div>
</div>
<p>
The focus node's neighbourhood is @t1@–@t6@: three creators and two identifiers, plus the <code>rdf:type</code> triple @t1@, whose predicate matches no constraint — since @S1@ is not <code>CLOSED</code>, it is simply ignored.
</p>
<p>
By predicate alone, the pre-matching of <code>ex:dset1</code> is @t2@–@t4@ → {@tc1@, @tc2@, @tc3@}; @t5@,@t6@ → {@tc4@, @tc5@, @tc6@} — a Cartesian product of 3³·3² = 243 matchings.
</p>
<p>
Negative caching checks each pair once, recursively.
<code>ex:bob</code> (@t3@) has no <code>schema:identifier</code> at all, so @S5@'s mandatory ORCID constraint is refuted without assembling any sub-matching: @tc3@ deleted.
<code>ex:noaa</code> (@t4@) is typed <code>schema:Organization</code>, failing @S5@'s <code>[schema:Person]</code> value set: @tc3@ deleted.
The legacy identifier (@t5@) is a literal with no outgoing arcs, so @S6@'s mandatory constraints can never be matched: @tc4@ and @tc6@ deleted.
And <code>ex:doi1</code> (@t6@) is an IRI node, not a literal: @tc5@ deleted.
The pre-matching becomes @t2@ → {@tc1@, @tc2@, @tc3@}; @t3@,@t4@ → {@tc1@, @tc2@}; @t5@ → {@tc5@}; @t6@ → {@tc4@, @tc6@}: 3·2·2·1·2 = 24 matchings — and no value expression is ever evaluated again.
</p>
<p>
The classes are {@t2@} over three candidates; {@t3@,@t4@} over {@tc1@, @tc2@}; {@t5@} over {@tc5@}; and {@t6@} over {@tc4@, @tc6@}.
Committing the forced singleton @t5@ → @tc5@ occupies @tc5@, so @te2@'s first alternative — which requires the second alternative's constraints to stay empty — is refuted for any vector using @tc4@: @t6@ goes to @tc6@.
On the creator side, the all-@tc1@ vector dies on @tc1@'s {1,2} cap (there are three creators), every mixed vector dies on OneOf exclusivity, so the long alternative must hold — and @t2@ (<code>ex:alice</code>) is the only possible occupant of the mandatory @tc3@.
Exactly one bag survives, and its expansion is a single matching, whose split is:
</p>
<table class="simple">
<thead>
<tr><th>triple constraint</th><th>matched triples</th></tr>
</thead>
<tbody>
<tr><td>@tc1@ (creators, short list)</td><td>—</td></tr>
<tr><td>@tc2@ (creators, long list)</td><td>@t3@ @t4@</td></tr>
<tr><td>@tc3@ (ORCID-identified person)</td><td>@t2@</td></tr>
<tr><td>@tc4@ (DOI, DOI-only convention)</td><td>—</td></tr>
<tr><td>@tc5@ (legacy string identifier)</td><td>@t5@</td></tr>
<tr><td>@tc6@ (DOI alongside legacy identifiers)</td><td>@t6@</td></tr>
</tbody>
</table>
<p>
That matching satisfies @te1@ {t3} and @te2@ (each via its second alternative) and hence @S1@: <code>ex:dset1</code> conforms.
Counting everything — the focus-node search plus every recursive check of a creator or identifier node against a candidate shape — the whole validation verifies 10 (sub-)matchings, measured, against the 24 focus-node matchings alone that post-caching enumeration walks, or the 243 that a validator evaluating value expressions inside the walk would explore.
</p>
<p>
Now scale the same schema with a realistic failure mode — the harvested record: <span class="math">n_a</span> creators, none carrying an ORCID, and <span class="math">n_i</span> DOI <code>PropertyValue</code>s (one per release, say) with no legacy string identifier.
No instance with <span class="math">n_a ≥ 3</span> or <span class="math">n_i ≥ 3</span> conforms, so nothing short-circuits — the worst case for any search.
With no ORCID-bearing creator, <span class="math">hi(tc3) = 0</span>, and arc consistency deletes @tc2@ from every creator: committing even one triple to it requires @tc3@ to be occupiable.
Symmetrically, with no string identifier, <span class="math">hi(tc5) = 0</span> and @tc6@ is deleted from every DOI.
Both sides collapse onto their {1,2}-capped candidate; for counts of 3 or more no count vector fits, and the search assembles <em>zero</em> focus-node matchings.
Every verified matching is a one-time caching check: 2 per creator (the @tc1@ and @tc2@ checks each verify the person's own little sub-matching once; the @tc3@ check is refuted for free) and 2 per DOI (@tc4@ and @tc6@ — the same @S6@ check made once per candidate constraint; @tc5@ refuted for free).
</p>
<table class="simple">
<thead>
<tr><th><span class="math">n_a</span></th><th><span class="math">n_i</span></th><th>Cartesian matchings (<span class="math">2^{n_a+n_i}</span>)</th><th>verified matchings, incl. recursive checks (measured)</th></tr>
</thead>
<tbody>
<tr><td>4</td><td>4</td><td>256</td><td>16</td></tr>
<tr><td>8</td><td>8</td><td>65,536</td><td>32</td></tr>
<tr><td>12</td><td>12</td><td>16,777,216</td><td>48</td></tr>
<tr><td>16</td><td>16</td><td>4,294,967,296</td><td>64</td></tr>
<tr><td>24</td><td>24</td><td>281,474,976,710,656</td><td>96</td></tr>
</tbody>
</table>
<p>Isolating the two axes shows the costs compose additively:</p>
<table class="simple">
<thead>
<tr><th>isolated axis</th><th><span class="math">n_a</span></th><th><span class="math">n_i</span></th><th>verified matchings (measured)</th></tr>
</thead>
<tbody>
<tr><td>creators only</td><td>16</td><td>0</td><td>32</td></tr>
<tr><td>identifiers only</td><td>0</td><td>16</td><td>32</td></tr>
</tbody>
</table>
<p>
The verified count is <span class="math">2(n_a + n_i)</span> exactly: 64 at <span class="math">n_a = n_i = 16</span> is precisely the 32 measured for each axis alone, added — each axis's one-time caching cost is linear in its own count and entirely independent of the other's combinatorics.
The Cartesian column, by contrast, multiplies the two sides together.
As a positive control, <span class="math">n_a = 2, n_i = 1</span> conforms (both short conventions): the search verifies 7 (sub-)matchings and accepts — real work still happens for satisfiable instances; the pruning only ever discards states that could never be accepted.
</p>
</section>
<section id="pruning-summary">
<h4>Summary</h4>
<ul>
<li>
Organize the search triple-indexed (a candidate-constraint set per triple, one choice per triple), and recover the constraint-indexed <a>split</a> from each chosen matching for the checks that need it.
</li>
<li>
Refute once, never re-derive: by value (the negative cache) when the <a>pre-matching</a> is built, and by structure (partial-bag refutation) at class granularity upfront and at every search node thereafter.
</li>
<li>
Search count vectors over classes of interchangeable triples; verify surviving bags with the exact check, and expand a bag into concrete matchings only then.
</li>
<li>
Both prunings are necessary-condition filters: the set of accepted matchings is invariant; only the amount of work spent discovering it changes.
</li>
<li>
Both prunings also delete from the <a>pre-matching</a>, so what remains of it is a search state: a validator that reports on failures reads the neighbourhood as it was before pruning began.
</li>
</ul>
</section>
</section>
</section>
</body>
</html>