-
Notifications
You must be signed in to change notification settings - Fork 9
Expand file tree
/
Copy pathalgorithms.html
More file actions
919 lines (762 loc) · 41 KB
/
Copy pathalgorithms.html
File metadata and controls
919 lines (762 loc) · 41 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
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
<!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 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: ""
}]
}],
};
</script>
<script type="text/javascript" src="scripts.js"></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>
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>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
if D contains a cycle then
return false
else
return (true, D)
</code></pre>
</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>
<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>
<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 two refinements address different failure modes, and a schema built entirely from
one of them shows only one at work. 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 — needs both at once. It is illustrative
rather than the official profile, but the moving parts are 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. (A representation that instead preserves order with RDF Collections, as FHIR
R5 RDF does for its repeating elements, moves the repetition into
<code>rdf:first</code>/<code>rdf:rest</code> cells whose per-node neighbourhoods are
unambiguous; this machinery has little to do there.) 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">
<span class="lineno schema">S1</span>
<span class="lineno schema">te1</span>
<span class="lineno schema">tc1</span>
<span class="lineno schema">tc2</span>
<span class="lineno schema">tc3</span>
<span class="lineno schema">te2</span>
<span class="lineno schema">tc4</span>
<span class="lineno schema">tc5</span>
<span class="lineno schema">tc6</span>
<span class="lineno schema">S2</span>
<span class="lineno schema">S3</span>
<span class="lineno schema">S4</span>
<span class="lineno schema">S5</span>
<span class="lineno schema">S6</span>
</pre>
<div class="inline shexc">
<pre class="nohighlight">PREFIX schema: <https://schema.org/>
PREFIX xsd: <http://www.w3.org/2001/XMLSchema#>
<#SOSODataset> {
(
schema:creator @<#Agent> {1,2}
|
schema:creator @<#Agent> + ;
schema:creator @<#OrcidPerson>
) ;
(
schema:identifier @<#DoiPropertyValue> {1,2}
|
schema:identifier xsd:string + ;
schema:identifier @<#DoiPropertyValue>
)
}
<#Agent> @<#Person> OR @<#Organization>
<#Person> {
a [schema:Person] ;
schema:name xsd:string
}
<#Organization> {
a [schema:Organization] ;
schema:name xsd:string
}
<#OrcidPerson> {
a [schema:Person] ;
schema:name xsd:string ;
schema:identifier /^https:\/\/orcid\.org\//
}
<#DoiPropertyValue> {
a [schema:PropertyValue] ;
schema:propertyID ["https://registry.identifiers.org/registry/doi"] ;
schema:value /^10\./
}</pre>
</div>
<div style="clear:both;"></div>
</div>
<p>
<span class="lineno schema">te1</span> and <span class="lineno schema">te2</span> are
the two OneOf groups. <span class="lineno schema">tc1</span> and
<span class="lineno schema">tc2</span> are the short-list and long-list creator
constraints — value-indistinguishable, since any valid agent satisfies both — while
<span class="lineno schema">tc3</span> demands an ORCID-identified person
(<span class="lineno schema">S5</span>). On the identifier side the roles are
mirrored: <span class="lineno schema">tc4</span> and
<span class="lineno schema">tc6</span> share the DOI value expression
(<span class="lineno schema">S6</span>) and are indistinguishable from each other,
but value-distinguishable from the plain-string constraint
<span class="lineno schema">tc5</span>. <span class="lineno schema">S2</span> is the
schema.org choice type: a creator may be a <span class="lineno schema">S3</span>
person or a <span class="lineno schema">S4</span> 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">
<span class="lineno data">t1</span>
<span class="lineno data">t2</span>
<span class="lineno data">t3</span>
<span class="lineno data">t4</span>
<span class="lineno data">t5</span>
<span class="lineno data">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">PREFIX schema: <https://schema.org/>
PREFIX ex: <http://example.org/datasets#>
ex:dset1 a schema:Dataset ;
schema:creator ex:alice ;
schema:creator ex:bob ;
schema:creator ex:noaa ;
schema:identifier "gov.noaa.ncdc:C00861" ;
schema:identifier ex:doi1 .
ex:alice a schema:Person ;
schema:name "Alice Walker" ;
schema:identifier "https://orcid.org/0000-0002-1825-0097" .
ex:bob a schema:Person ;
schema:name "Bob Ferris" .
ex:noaa a schema:Organization ;
schema:name "NOAA National Centers for Environmental Information" .
ex:doi1 a schema:PropertyValue ;
schema:propertyID "https://registry.identifiers.org/registry/doi" ;
schema:value "10.7289/V5D21VHZ" .</pre>
</div>
<div style="clear:both;"></div>
</div>
<p>
The focus node's neighbourhood is <span class="lineno data">t1</span>–<span class="lineno data">t6</span>:
three creators and two identifiers, plus the <code>rdf:type</code> triple
<span class="lineno data">t1</span>, whose predicate matches no constraint — since
<span class="lineno schema">S1</span> is not <code>CLOSED</code>, it is simply
ignored. The remaining triples
(<span class="lineno data">t7</span>–<span class="lineno data">t16</span>) belong to
the creator and identifier nodes and participate only in the recursive value checks.
</p>
<p>
By predicate alone, the pre-matching of <code>ex:dset1</code> is
<span class="lineno data">t2</span>–<span class="lineno data">t4</span> →
{<span class="lineno schema">tc1</span>, <span class="lineno schema">tc2</span>,
<span class="lineno schema">tc3</span>};
<span class="lineno data">t5</span>,<span class="lineno data">t6</span> →
{<span class="lineno schema">tc4</span>, <span class="lineno schema">tc5</span>,
<span class="lineno schema">tc6</span>} — a Cartesian product of
3³·3² = 243 matchings.
</p>
<p>
Negative caching checks each pair once, recursively. <code>ex:bob</code>
(<span class="lineno data">t3</span>) has no <code>schema:identifier</code> at all,
so <span class="lineno schema">S5</span>'s mandatory ORCID constraint is refuted
without assembling any sub-matching: <span class="lineno schema">tc3</span> deleted.
<code>ex:noaa</code> (<span class="lineno data">t4</span>) is typed
<code>schema:Organization</code>, failing <span class="lineno schema">S5</span>'s
<code>[schema:Person]</code> value set: <span class="lineno schema">tc3</span>
deleted. The legacy identifier (<span class="lineno data">t5</span>) is a literal
with no outgoing arcs, so <span class="lineno schema">S6</span>'s mandatory
constraints can never be matched: <span class="lineno schema">tc4</span> and
<span class="lineno schema">tc6</span> deleted. And <code>ex:doi1</code>
(<span class="lineno data">t6</span>) is an IRI node, not a literal:
<span class="lineno schema">tc5</span> deleted. The pre-matching becomes
<span class="lineno data">t2</span> → {<span class="lineno schema">tc1</span>,
<span class="lineno schema">tc2</span>, <span class="lineno schema">tc3</span>};
<span class="lineno data">t3</span>,<span class="lineno data">t4</span> →
{<span class="lineno schema">tc1</span>, <span class="lineno schema">tc2</span>};
<span class="lineno data">t5</span> → {<span class="lineno schema">tc5</span>};
<span class="lineno data">t6</span> → {<span class="lineno schema">tc4</span>,
<span class="lineno schema">tc6</span>}: 3·2·2·1·2 = 24
matchings — and no value expression is ever evaluated again.
</p>
<p>
The classes are {<span class="lineno data">t2</span>} over three candidates;
{<span class="lineno data">t3</span>,<span class="lineno data">t4</span>} over
{<span class="lineno schema">tc1</span>, <span class="lineno schema">tc2</span>};
{<span class="lineno data">t5</span>} over {<span class="lineno schema">tc5</span>};
and {<span class="lineno data">t6</span>} over
{<span class="lineno schema">tc4</span>, <span class="lineno schema">tc6</span>}.
Committing the forced singleton <span class="lineno data">t5</span> →
<span class="lineno schema">tc5</span> occupies
<span class="lineno schema">tc5</span>, so <span class="lineno schema">te2</span>'s
first alternative — which requires the second alternative's constraints to stay
empty — is refuted for any vector using <span class="lineno schema">tc4</span>:
<span class="lineno data">t6</span> goes to <span class="lineno schema">tc6</span>.
On the creator side, the all-<span class="lineno schema">tc1</span> vector dies on
<span class="lineno schema">tc1</span>'s {1,2} cap (there are three creators), every
mixed vector dies on OneOf exclusivity, so the long alternative must hold — and
<span class="lineno data">t2</span> (<code>ex:alice</code>) is the only possible
occupant of the mandatory <span class="lineno schema">tc3</span>. 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><span class="lineno schema">tc1</span> (creators, short list)</td><td>—</td></tr>
<tr><td><span class="lineno schema">tc2</span> (creators, long list)</td><td><span class="lineno data">t3</span> <span class="lineno data">t4</span></td></tr>
<tr><td><span class="lineno schema">tc3</span> (ORCID-identified person)</td><td><span class="lineno data">t2</span></td></tr>
<tr><td><span class="lineno schema">tc4</span> (DOI, DOI-only convention)</td><td>—</td></tr>
<tr><td><span class="lineno schema">tc5</span> (legacy string identifier)</td><td><span class="lineno data">t5</span></td></tr>
<tr><td><span class="lineno schema">tc6</span> (DOI alongside legacy identifiers)</td><td><span class="lineno data">t6</span></td></tr>
</tbody>
</table>
<p>
That matching satisfies <span class="lineno schema">te1</span> and
<span class="lineno schema">te2</span> (each via its second alternative) and hence
<span class="lineno schema">S1</span>: <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
<span class="lineno schema">tc2</span> from every creator: committing even one triple
to it requires <span class="lineno schema">tc3</span> to be occupiable.
Symmetrically, with no string identifier, <span class="math">hi(tc5) = 0</span> and
<span class="lineno schema">tc6</span> 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 <span class="lineno schema">tc1</span> and
<span class="lineno schema">tc2</span> checks each verify the person's own little
sub-matching once; the <span class="lineno schema">tc3</span> check is refuted for
free) and 2 per DOI (<span class="lineno schema">tc4</span> and
<span class="lineno schema">tc6</span> — the same
<span class="lineno schema">S6</span> check made once per candidate constraint;
<span class="lineno schema">tc5</span> 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>
</ul>
</section>
</section>
</section>
</body>
</html>