An Approach for Introducing Recursion in SHACL
Assigning people from SHACL Core + Nicholas (I guess that's most relevant for this question).
CC: @robert-david, @afs, @simonstey, @liviorobaldo (perhaps also of interest to you)
I am creating a new issue. It was first a reply on the issue (plus a few more clarifications): #565 (apologies for cross-posting but I am not sure the original comment reached the destinations).
I believe it's worth having another look at recursion. The understanding of the matter is quite mature by now, and I don't think we should wait for SHACL 1.3. It would be a pity not to include some form of it. In the reply, I also drafted a version that could be something to insert into the spec.
Perhaps individual implementors may decide to cover one of the proposed recursive approaches.
What I propose concretely
In short, and each point is explained in the rest of the document:
-
Adopt positive SHACL Core as the recursive fragment. It is the largest fragment where recursion can be supported without asking implementors to build a new engine, and the exclusions (sh:not, sh:qualifiedMaxCount, sh:qualifiedValueShapesDisjoint, sh:xone) are few and easy to state.
-
Support both LFP (cautious) and GFP (brave), selected explicitly. Both come from the same one-line change to the validator, differing only in the default returned on a repeated pair. Neither is right for every use case, so the schema — not the implementation — should say which one is meant.
-
Leave negation out of scope for now. Stratified negation is tractable and well understood, but needs an outer loop over strata; unrestricted negation needs a solver or a dedicated well-founded construction. These are worth revisiting, but they are a different size of change and should not block the positive fragment.
Implementations that do not wish to support recursion at all are unaffected: a non-recursive schema behaves exactly as it does today under either default.
A few practical offers to go with this:
- If you agree with the proposal, I have already prepared the concrete changes that would need to be made in the main specification document.
- I would be happy to give a presentation of 15 to 20 minutes, or longer if that is more useful, at one of the group meetings.
- I can also provide test cases and a prototype implementation for the fragment covered here
Overview
Introducing recursion into SHACL is not easy. Whichever way one goes, a compromise has to be made somewhere: on expressiveness, on efficiency, or on how simple the result is to explain and to implement.
In this document, I will try to make the smallest possible incision into the already existing implementations but still allow for some kind of sound support for recursion.
Here's the idea:
- I'll start from the most basic possible SHACL validation algorithm, call it Algorithm 1 (implemented below as
simple_validate): evaluate the targets, then validate shape by shape for each target node, following shape references where needed, and validating neighbouring nodes against other shapes.
- Then I'll show how, for the fragment of positive SHACL Core, Algorithm 1 can be "easily" extended to allow recursive shape definitions, in two modes: brave and cautious.
- Then, for the case of non-positive SHACL (i.e. with negation), which in general needs a new algorithm (the easiest route being to implement it via logic programming), I'll present the possible options: fragments like stratified negation that stay tractable, and the general case, which may not have a tractable algorithm at all.
Background
All the observations here about recursion distill roughly eight years of work by the community that has been trying to pin down a semantics for recursive shapes, across SHACL, ShEx, and property-graph schemas (PG-Schema). I've had the good fortune to be a co-author on some of it, alongside colleagues named throughout the list below.
The papers are summarized at the end, in the References section.
Here, I'm not presenting any technical results from the papers; instead, I'm trying to distill and find safe fragments of SHACL where recursion can behave well, based on our findings. If one would really like to read something minimally, I would suggest our most recent paper (KR 2026), which summarizes all results on recursion so far, and also does an experimental comparison across all SHACL and ShEx implementations in the presence of recursion.
What I'm looking for
Given that body of work, I want to filter it down with a specific practical criterion in mind. I'm interested in approaches that:
- build on top of the validator every implementation already has. Call this Algorithm 1: evaluate the targets, then validate shape-to-shape by following shape references (when a shape requires checking a neighbouring node against another shape, unfold that check sequentially), and keep a table of (node, shape) pairs already validated, so the same pair is never re-checked.
- are sound with respect to some well-defined recursive fragment. Not every semantics can be captured this way; where an extension isn't possible, the goal is to at least delimit the SHACL fragment for which it is.
(This advice — fit the recursion semantics to the algorithms implementations already have, rather than inventing a new algorithm — is what Moshe Vardi gave us after our presentation at KR, when I asked him what semantics for recursion one should propose. :))
Assignments: what a validator is actually computing
Given a graph G and a schema, an assignment is a set of pairs (s, a) (shape name s, node a), read as "node a satisfies shape s". Equivalently, we can keep track of this in a table T[s, a] → true/false.
Every SHACL validator, regardless of implementation, is computing one of these assignments: either implicitly, on a call stack or in memory, or explicitly, as a data structure. What the current standard actually asks for is just printing the entries of T that are false, as violations. It's worth noting that the standard doesn't also expose the successful validations; I believe that in principle there's no technical reason it couldn't.
The fragment: SHACL Core and its positive subset
Focusing on SHACL Core
We restrict attention to SHACL Core because it's already enough to expose the recursion problem.
Positive SHACL
Positive SHACL is a "reasonable" fragment of SHACL Core where one can easily extend existing algorithms to support recursion.
Intuitively, recursion behaves "well" for positive SHACL since it is somewhat monotonic. Once we validate a node, adding more successful validations will not change that (whereas if we have negation it might).
More concretely, positive SHACL drops the constructs that negate a shape reference, directly or through a bound on how many neighbours satisfy one:
sh:not: direct negation of a shape.
sh:qualifiedMaxCount: bounds, from above, how many neighbours may satisfy a given shape, and that count depends on T; growing T can push the count past the bound and flip the result from true to false.
sh:qualifiedValueShapesDisjoint: requires the value sets of sibling qualified shapes to be disjoint, so growing T can create an overlap that wasn't there before and flip the result from true to false.
sh:xone: "exactly one shape holds" needs "not more than one," which needs negation over shape references.
Everything else in SHACL Core stays in, including plain sh:maxCount and sh:closed. Plain sh:maxCount (with no sh:qualifiedValueShape attached) just counts matching triples for a property path, with no shape reference, so it never consults T. sh:closed only checks which predicates appear as outgoing edges at a node against a fixed allow-list taken from the shape's own declarations, with no shape reference involved either.
Worth flagging separately: sh:node combined with sh:path ([ sh:path p ; sh:node S2 ]) says "every value reachable via p must conform to S2" — a universal.
Universals are not always monotone. If the range of the quantifier could itself depend on T, the constraint could flip from true to false as T grows, and unfolding it would reveal a hidden negation — exactly what this section is about avoiding.
Here it does not happen: the set being quantified over, values(t, p), comes straight from the graph and never depends on T. So it behaves like a conjunction of monotone checks — the same family as sh:qualifiedMinCount, not sh:qualifiedMaxCount — and stays in the fragment.
Algorithm 1: simple_validate
The following algorithm is probably the simplest possible approach to a (non-recursive) validation procedure for SHACL. It abstracts away from details like checking local properties, and focuses only on the one step that matters for recursion: when a shape references another shape.
This is deliberately left as a sketch, so it's worth being explicit about where S2, t2, and r come from. Every SHACL constraint that references another shape does so via some property path, or, for a bare sh:node, via no path at all:
sh:property [ sh:path p ; sh:node S2 ] or sh:qualifiedValueShape S2: S2 is the referenced shape, and t2 ranges over values(t, p), the values reachable from t via p.
- A bare
sh:node S2 with no path: t2 is just t itself, i.e. the same node must also conform to S2.
- In every case,
r is nothing more than the boolean returned by the recursive call for that particular (S2, t2) pair.
How the r's are then combined into result depends on the constraint: AND for sh:node/sh:and, OR for sh:or, a threshold comparison for sh:qualifiedMinCount/sh:qualifiedMaxCount, and so on. Spelling out every constraint's exact combination rule would triple the length of the pseudocode without changing anything about how recursion is handled, which is the actual point of Algorithm 1.
T : table of finished results, (S,t) -> true/false (the assignment)
simple_validate(S, t):
if (S,t) in T: return T[(S,t)]
for each constraint needing S2 at neighbour t2:
r := simple_validate(S2, t2)
result := combine the r's (AtLeast_k, etc.) and other local constraints
T[(S,t)] := result
return result
for each target node t of shape S: simple_validate(S, t)
print T
Where Algorithm 1 breaks for recursion, and how to fix it
Algorithm 1 implicitly computes an assignment: a labelling of the graph's nodes with shape names. Can we reuse this algorithm for recursion? In the presence of recursive shape definitions, though, we lose any guarantee of termination. How can we fix that?
A very simple idea: watch this unfolding of shape dependencies as if it were building a tree, whose nodes are pairs (s,t). The simplest termination condition is then: if we encounter a pair (s,t) that's already on the current branch, either accept or reject that branch right there, instead of recursing further.
The good news is that with this one small change, we get exactly two well-known fixed points.
- Accepting on repetition (
DEFAULT = true) computes the greatest fixed point (GFP): the most permissive assignment consistent with the shapes, the so-called brave assignment.
- Rejecting on repetition (
DEFAULT = false) computes the least fixed point (LFP): the most conservative, cautious assignment, since a fact only holds if it has a finite justification grounded in facts, which is precisely how the least fixed point is characterized.
It's also worth naming the classical logic-programming procedures that compute these two, because it means we're standing on fifty years of established theory rather than inventing something ad hoc. Rejecting on repetition (LFP) is exactly SLD resolution: Prolog's ordinary resolution procedure, extended with a loop check on the current branch (an ancestor check). Accepting on repetition (GFP) is exactly co-SLD resolution: the coinductive extension of Prolog's resolution procedure, and the standard way to compute a greatest fixed point via top-down proof search.
Example
Let's briefly illustrate LFP and GFP on an example of positive SHACL.
Consider four people, where Tim and Eve are mutual friends and Eve additionally owns a yacht, while Tom and Ann are mutual friends with no yacht in sight:
ex:Tom ex:hasFriend ex:Ann .
ex:Ann ex:hasFriend ex:Tom .
ex:Tim ex:hasFriend ex:Eve .
ex:Eve ex:hasFriend ex:Tim ;
ex:hasYacht ex:Wind .
and the shape:
ex:EliteShape
a sh:NodeShape ;
sh:targetNode ex:Tom, ex:Ann, ex:Tim, ex:Eve ;
sh:or (
[ sh:path ex:hasYacht ; sh:minCount 1 ]
[ sh:path ex:hasFriend ;
sh:qualifiedValueShape ex:EliteShape ;
sh:qualifiedMinCount 1 ]
) .
Validating Elite(Eve) is fine: Eve owns a yacht, done. Validating Elite(Tim) is fine too: Tim's friend Eve is (now cached as) Elite, done. But validating Elite(Tom) sends the algorithm looking for a hasFriend-neighbour that is Elite; it finds Ann, and to check Ann it needs to check whether Tom is Elite, the very question it started with. The table has no entry yet for either, so the naive algorithm doesn't know whether to say yes or no; a literal implementation just recurses forever.
We have two options:
- Cautious validation (formally: the least fixed point, LFP). Believe a node is
Elite only if that can be justified without ever assuming the very fact being proven. Under this reading, Tom and Ann are not Elite (their only route to it is circular), while Eve and Tim are, since their justification reaches a solid starting point (Eve's yacht, then Tim via Eve).
- Brave validation (formally: the greatest fixed point, GFP). Accept any assignment that is self-consistent, even if the only reason it holds together is the cycle itself. Under this reading, Tom and Ann are Elite too. Assigning them the shape doesn't contradict anything; it just rests on the premise that we want to maximize successful validations, which often suits semantic data, where graphs are incomplete and evolving. One can easily think of other scenarios where such self-justification is exactly what you want: e.g., identifying all professors teaching an academic course, where something counts as an academic course if it's taught by an academic professor, and so on.
Extending Algorithm 1 to capture LFP and GFP computations
Now we change our algorithm minimally to capture LFP and GFP computations, by simply introducing one boolean switch and an array called chain.
DEFAULT : true // for GFP (brave); set to false for LFP (cautious)
validate(S, t, chain):
if (S,t) in chain: return DEFAULT # closed (GFP: true, LFP: false)
for each constraint needing S2 at neighbour t2:
r := validate(S2, t2, chain + {(S,t)})
result := combine the r's (AtLeast_k, etc.) and check other local constraints
return result
for each target (S,t): report validate(S, t, {})
Note there's no shared table T here. chain itself costs nothing beyond what the recursion already carries — it is just the sequence of calls currently open — and leaving T out is what keeps the algorithm sound: a value computed while some pair is still open on the current branch is used only on that branch, and never picked up by another one. A naive T added on top would not preserve this.
Dropping the cache does cost efficiency, since the same pair can then be recomputed. This is a solved problem rather than an open one: standard Prolog engines already do exactly this kind of caching safely, and that technique can be adapted here directly. So the extension above fixes the semantics, and the efficiency can be recovered with a known method — happy to work that part out separately.
Worth being precise about where this actually applies, and this holds for LFP just as much as for GFP. Since we start from the targets, we only ever compute the part of the fixed point relevant to their validation. A pair that isn't a target and isn't reached via some chain of shape references from a target is never passed to validate at all; it isn't assumed true (or false) under either reading, it's simply never computed, because nothing we're actually validating ever needs its value.
Another thing worth noting: this kind of computation is very much in the spirit of so-called top-down computation. One could easily do the same computation via a classical bottom-up approach instead, using some logic-programming (answer-set programming) tool, and just check the targets at the end. However, that approach would require a new algorithm.
When defining a new algorithm from scratch becomes unavoidable
Negation is where the simple change to the algorithm stops being enough, except for a few special cases covered below.
In the worst case, in the presence of negation, one has to guess an assignment and then check whether that guess is consistent. That approach is intractable. There are, however, special fragments where this can be partly avoided.
Worth flagging up front: all of these approaches can be encoded fairly directly into logic programming, in particular answer-set programming (ASP); see e.g. WWW 2020.
Stratified negation
If negative shape references never participate in a cycle (the classical Datalog-style stratification condition), the schema can be processed stratum by stratum, each one built on the fully-settled result of the strata below it. This stays tractable, and it composes cleanly with the LFP/GFP idea above within each stratum (Andresel et al., WWW 2020).
This means that, in principle, we could still use the extended variant of our Algorithm 1 to do the computation within each stratum. However, we'd need another algorithm on top of it, to orchestrate the computation stratum by stratum. So this is not a case where Algorithm 1 alone suffices.
One caveat on which notion of model is meant here.
Take the same four people as before, and add a second shape that uses negation:
Elite(x) ← hasFriend(x, y), Elite(y)
Elite(x) ← hasYacht(x, _)
Ordinary(x) ← ¬Elite(x)
This is stratified: the negation points at Elite, which is settled by its own cycle first, and no negation occurs inside that cycle.
Two assignments are internally consistent here — two supported models:
|
Elite |
Ordinary |
| A |
Eve, Tim |
Tom, Ann |
| B |
Eve, Tim, Tom, Ann |
— |
Both survive checking. Eve is Elite on her yacht and Tim through Eve in either case. The difference is Tom and Ann: in B each is Elite because the other is, which is circular but not contradictory.
Only A is stable. Stable models additionally require every assignment to be founded — derivable without assuming itself — and nothing outside the cycle ever grounds Tom or Ann. This is the same distinction as cautious (LFP) versus brave (GFP) above.
The negation is what makes the difference bite. Without Ordinary, choosing B merely adds two Elite nodes. With it, choosing B also takes Ordinary away from Tom and Ann, so an unfounded guess in one shape silently changes the verdict for another.
The distinction matters for tractability. With stable models, plain Datalog-style stratification is enough to stay tractable. With supported models it is not, and one needs the stronger strict stratification condition to recover PTIME (see the ISWC 2018 P&D entry in the references).
Personally, for this case, I think it would be easier to do a separate bottom-up computation and define a separate algorithm that does that in some efficient way.
Unrestricted negation
If the goal is to find some 2-valued satisfying assignment that validates the targets, in the presence of unrestricted negation, the problem gets harder.
In this case, it would be better to have an implementation built entirely around some variant of an ASP or SAT solver, since in the worst case it has to guess at least some part of the shape assignment.
We took exactly this approach in Corman, Florenzano, Reutter, Savković, ISWC 2019: a hybrid strategy that evaluates a small number of SPARQL queries over the endpoint, then uses the answers to build a set of propositional formulas that are passed to a SAT solver.
Unrestricted negation, 3-valued logic
For unrestricted negation there is also a tractable variant, at a small price in complication: we need to allow a third outcome of validation: "undefined," alongside true and false. It's based on a semantics for logic programs called the well-founded semantics, where something is only considered true when it can be inferred without resorting to case-by-case guessing.
Unlike the LFP/GFP extension above, this isn't a one-line addition to Algorithm 1, it needs its own construction (Okulmus & Šimkus, KR 2024, or the ASP-based translation in WWW 2020).
To illustrate the difference between 2- and 3-valued readings, keep Tom and Ann, still friends with each other, and move the negation inside the cycle:
Elite(x) ← hasFriend(x, y), ¬Elite(y)
You are Elite if you have a friend who is not. For Tom and Ann this unfolds to
Elite(Tom) ← ¬Elite(Ann)
Elite(Ann) ← ¬Elite(Tom)
which is the classic pair p ← ¬q, q ← ¬p. Note this schema is not stratified: the negation now sits in the cycle, so nothing in the previous section applies to it.
There are two solutions (stable models): Tom is Elite and Ann is not, or Ann is Elite and Tom is not. Each is internally consistent, and nothing in the schema prefers one over the other.
- Under stable model semantics (the standard 2-valued semantics used in ASP), both are legitimate, and validation becomes a question of which model you mean: brave (conforms in at least one model — Tom and Ann both count) or cautious (conforms in every model — here neither qualifies, since each model excludes the other).
- Under well-founded semantics, there is a single canonical 3-valued model, computed once in polynomial time, with no enumeration of alternatives. On this example it leaves both Tom and Ann undefined: nothing in the schema actually justifies picking one over the other, so the well-founded model refuses to guess.
Summary
| Fragment |
Semantics |
Values |
Tractable? |
Extends Algorithm 1 directly? |
| Non-recursive |
n/a |
2 |
Yes |
Yes (this is just Algorithm 1) |
| Positive recursion |
Cautious (LFP) |
2 |
Yes, with tabling † |
Yes (add a per-branch chain of in-progress pairs) |
| Positive recursion |
Brave (GFP) |
2 |
Yes, with tabling † |
Yes (same addition, opposite default) |
| Stratified negation |
Stable models |
2 |
Yes |
Partly — Algorithm 1 within each stratum, plus an outer loop over strata |
| Stratified negation |
Supported models |
2 |
Only under strict stratification |
Only with the stronger condition |
| Unrestricted negation |
Stable models, brave |
2 |
No (NP-complete) |
No |
| Unrestricted negation |
Stable models, skeptical |
2 |
No (coNP-complete) |
No |
| Unrestricted negation |
Well-founded |
3 |
Yes |
No (needs a dedicated construction) |
† Tractable with the standard caching technique from Prolog engines; see the note under the algorithm.
References
I list papers chronologically and summarize their contributions.
| Paper |
Venue |
What it introduces |
| Corman, Reutter, Savković: Semantics and Validation of Recursive SHACL |
ISWC 2018 |
First formal semantics for recursive SHACL, based on the idea of "looking for a possible (2-valued) assignment" (supported models), plus a 3-valued relaxation to stay fault-tolerant when no consistent assignment exists. |
| Corman, Reutter, Savković: A Tractable Notion of Stratification for SHACL |
ISWC 2018 (P&D) |
Identifies that plain (Datalog-style) stratification is not enough to keep the above semantics tractable, and introduces the stronger strict stratification condition that recovers PTIME. |
| Corman, Florenzano, Reutter, Savković: Validating SHACL Constraints over a SPARQL Endpoint |
ISWC 2019 |
Algorithms for validating recursive SHACL when the graph is only reachable through a SPARQL endpoint, combining targeted queries with SAT solving. |
| Andresel, Corman, Ortiz, Reutter, Savković, Šimkus: Stable Model Semantics for Recursive SHACL |
WWW 2020 |
Replaces supported models with stable models (borrowed from Answer Set Programming), which additionally require every shape assignment to be founded (i.e., justified by a non-circular derivation). Gives an explicit translation of SHACL into logic-program (ASP) rules, and a 3-valued stable-model variant. |
| Ahmetaj, Löhnert, Ortiz, Šimkus: Magic Shapes for SHACL Validation |
VLDB 2022 |
A magic-sets-style rewriting that lets a goal-directed (target-driven) validator handle full recursion correctly, without materializing the whole graph. |
| Angles, Bonifati, Dumbrava, Fletcher, Green, Hidders, Li, Libkin, Marsault, Martens, Murlak, Plantikow, Savković, Schmidt, Sequeda, Staworko, Tomaszuk, Voigt, Vrgoč, Wu, Živković: PG-Schema: Schemas for Property Graphs |
PACMMOD / SIGMOD 2023 |
Not specifically about recursion, but the schema formalism (PG-Types, PG-Keys) that the shape-language-unification papers below build on for the property-graph side. |
| Okulmus, Šimkus: SHACL Validation under the Well-founded Semantics |
KR 2024 |
A dedicated treatment of the well-founded (3-valued, skeptical) semantics for recursive SHACL, with a target-modular translation into logic programs. |
| Ahmetaj, Boneva, Hidders, Jakubowski, Labra Gayo, Martens, Mogavero, Murlak, Okulmus, Savković, Šimkus, Tomaszuk: Common Foundations for SHACL, ShEx, and PG-Schema |
WWW 2025 |
Places SHACL, ShEx, and PG-Schema constraints in one common formal framework. |
| Same group: Common Foundations for Recursive Shape Languages |
KR 2026 |
Extends the common framework specifically to the recursive case across all three languages. |
An Approach for Introducing Recursion in SHACL
Assigning people from SHACL Core + Nicholas (I guess that's most relevant for this question).
CC: @robert-david, @afs, @simonstey, @liviorobaldo (perhaps also of interest to you)
I am creating a new issue. It was first a reply on the issue (plus a few more clarifications): #565 (apologies for cross-posting but I am not sure the original comment reached the destinations).
I believe it's worth having another look at recursion. The understanding of the matter is quite mature by now, and I don't think we should wait for SHACL 1.3. It would be a pity not to include some form of it. In the reply, I also drafted a version that could be something to insert into the spec.
Perhaps individual implementors may decide to cover one of the proposed recursive approaches.
What I propose concretely
In short, and each point is explained in the rest of the document:
Adopt positive SHACL Core as the recursive fragment. It is the largest fragment where recursion can be supported without asking implementors to build a new engine, and the exclusions (
sh:not,sh:qualifiedMaxCount,sh:qualifiedValueShapesDisjoint,sh:xone) are few and easy to state.Support both LFP (cautious) and GFP (brave), selected explicitly. Both come from the same one-line change to the validator, differing only in the default returned on a repeated pair. Neither is right for every use case, so the schema — not the implementation — should say which one is meant.
Leave negation out of scope for now. Stratified negation is tractable and well understood, but needs an outer loop over strata; unrestricted negation needs a solver or a dedicated well-founded construction. These are worth revisiting, but they are a different size of change and should not block the positive fragment.
Implementations that do not wish to support recursion at all are unaffected: a non-recursive schema behaves exactly as it does today under either default.
A few practical offers to go with this:
Overview
Introducing recursion into SHACL is not easy. Whichever way one goes, a compromise has to be made somewhere: on expressiveness, on efficiency, or on how simple the result is to explain and to implement.
In this document, I will try to make the smallest possible incision into the already existing implementations but still allow for some kind of sound support for recursion.
Here's the idea:
simple_validate): evaluate the targets, then validate shape by shape for each target node, following shape references where needed, and validating neighbouring nodes against other shapes.Background
All the observations here about recursion distill roughly eight years of work by the community that has been trying to pin down a semantics for recursive shapes, across SHACL, ShEx, and property-graph schemas (PG-Schema). I've had the good fortune to be a co-author on some of it, alongside colleagues named throughout the list below.
The papers are summarized at the end, in the References section.
Here, I'm not presenting any technical results from the papers; instead, I'm trying to distill and find safe fragments of SHACL where recursion can behave well, based on our findings. If one would really like to read something minimally, I would suggest our most recent paper (KR 2026), which summarizes all results on recursion so far, and also does an experimental comparison across all SHACL and ShEx implementations in the presence of recursion.
What I'm looking for
Given that body of work, I want to filter it down with a specific practical criterion in mind. I'm interested in approaches that:
(This advice — fit the recursion semantics to the algorithms implementations already have, rather than inventing a new algorithm — is what Moshe Vardi gave us after our presentation at KR, when I asked him what semantics for recursion one should propose. :))
Assignments: what a validator is actually computing
Given a graph G and a schema, an assignment is a set of pairs
(s, a)(shape names, nodea), read as "nodeasatisfies shapes". Equivalently, we can keep track of this in a tableT[s, a] → true/false.Every SHACL validator, regardless of implementation, is computing one of these assignments: either implicitly, on a call stack or in memory, or explicitly, as a data structure. What the current standard actually asks for is just printing the entries of
Tthat are false, as violations. It's worth noting that the standard doesn't also expose the successful validations; I believe that in principle there's no technical reason it couldn't.The fragment: SHACL Core and its positive subset
Focusing on SHACL Core
We restrict attention to SHACL Core because it's already enough to expose the recursion problem.
Positive SHACL
Positive SHACL is a "reasonable" fragment of SHACL Core where one can easily extend existing algorithms to support recursion.
Intuitively, recursion behaves "well" for positive SHACL since it is somewhat monotonic. Once we validate a node, adding more successful validations will not change that (whereas if we have negation it might).
More concretely, positive SHACL drops the constructs that negate a shape reference, directly or through a bound on how many neighbours satisfy one:
sh:not: direct negation of a shape.sh:qualifiedMaxCount: bounds, from above, how many neighbours may satisfy a given shape, and that count depends onT; growingTcan push the count past the bound and flip the result from true to false.sh:qualifiedValueShapesDisjoint: requires the value sets of sibling qualified shapes to be disjoint, so growingTcan create an overlap that wasn't there before and flip the result from true to false.sh:xone: "exactly one shape holds" needs "not more than one," which needs negation over shape references.Everything else in SHACL Core stays in, including plain
sh:maxCountandsh:closed. Plainsh:maxCount(with nosh:qualifiedValueShapeattached) just counts matching triples for a property path, with no shape reference, so it never consultsT.sh:closedonly checks which predicates appear as outgoing edges at a node against a fixed allow-list taken from the shape's own declarations, with no shape reference involved either.Worth flagging separately:
sh:nodecombined withsh:path([ sh:path p ; sh:node S2 ]) says "every value reachable viapmust conform toS2" — a universal.Universals are not always monotone. If the range of the quantifier could itself depend on
T, the constraint could flip from true to false asTgrows, and unfolding it would reveal a hidden negation — exactly what this section is about avoiding.Here it does not happen: the set being quantified over,
values(t, p), comes straight from the graph and never depends onT. So it behaves like a conjunction of monotone checks — the same family assh:qualifiedMinCount, notsh:qualifiedMaxCount— and stays in the fragment.Algorithm 1:
simple_validateThe following algorithm is probably the simplest possible approach to a (non-recursive) validation procedure for SHACL. It abstracts away from details like checking local properties, and focuses only on the one step that matters for recursion: when a shape references another shape.
This is deliberately left as a sketch, so it's worth being explicit about where
S2,t2, andrcome from. Every SHACL constraint that references another shape does so via some property path, or, for a baresh:node, via no path at all:sh:property [ sh:path p ; sh:node S2 ]orsh:qualifiedValueShape S2:S2is the referenced shape, andt2ranges overvalues(t, p), the values reachable fromtviap.sh:node S2with no path:t2is justtitself, i.e. the same node must also conform toS2.ris nothing more than the boolean returned by the recursive call for that particular(S2, t2)pair.How the
r's are then combined intoresultdepends on the constraint:ANDforsh:node/sh:and,ORforsh:or, a threshold comparison forsh:qualifiedMinCount/sh:qualifiedMaxCount, and so on. Spelling out every constraint's exact combination rule would triple the length of the pseudocode without changing anything about how recursion is handled, which is the actual point of Algorithm 1.Where Algorithm 1 breaks for recursion, and how to fix it
Algorithm 1 implicitly computes an assignment: a labelling of the graph's nodes with shape names. Can we reuse this algorithm for recursion? In the presence of recursive shape definitions, though, we lose any guarantee of termination. How can we fix that?
A very simple idea: watch this unfolding of shape dependencies as if it were building a tree, whose nodes are pairs
(s,t). The simplest termination condition is then: if we encounter a pair(s,t)that's already on the current branch, either accept or reject that branch right there, instead of recursing further.The good news is that with this one small change, we get exactly two well-known fixed points.
DEFAULT = true) computes the greatest fixed point (GFP): the most permissive assignment consistent with the shapes, the so-called brave assignment.DEFAULT = false) computes the least fixed point (LFP): the most conservative, cautious assignment, since a fact only holds if it has a finite justification grounded in facts, which is precisely how the least fixed point is characterized.It's also worth naming the classical logic-programming procedures that compute these two, because it means we're standing on fifty years of established theory rather than inventing something ad hoc. Rejecting on repetition (LFP) is exactly SLD resolution: Prolog's ordinary resolution procedure, extended with a loop check on the current branch (an ancestor check). Accepting on repetition (GFP) is exactly co-SLD resolution: the coinductive extension of Prolog's resolution procedure, and the standard way to compute a greatest fixed point via top-down proof search.
Example
Let's briefly illustrate LFP and GFP on an example of positive SHACL.
Consider four people, where Tim and Eve are mutual friends and Eve additionally owns a yacht, while Tom and Ann are mutual friends with no yacht in sight:
ex:Tom ex:hasFriend ex:Ann . ex:Ann ex:hasFriend ex:Tom . ex:Tim ex:hasFriend ex:Eve . ex:Eve ex:hasFriend ex:Tim ; ex:hasYacht ex:Wind .and the shape:
ex:EliteShape a sh:NodeShape ; sh:targetNode ex:Tom, ex:Ann, ex:Tim, ex:Eve ; sh:or ( [ sh:path ex:hasYacht ; sh:minCount 1 ] [ sh:path ex:hasFriend ; sh:qualifiedValueShape ex:EliteShape ; sh:qualifiedMinCount 1 ] ) .Validating
Elite(Eve)is fine: Eve owns a yacht, done. ValidatingElite(Tim)is fine too: Tim's friend Eve is (now cached as) Elite, done. But validatingElite(Tom)sends the algorithm looking for ahasFriend-neighbour that isElite; it finds Ann, and to check Ann it needs to check whether Tom isElite, the very question it started with. The table has no entry yet for either, so the naive algorithm doesn't know whether to say yes or no; a literal implementation just recurses forever.We have two options:
Eliteonly if that can be justified without ever assuming the very fact being proven. Under this reading, Tom and Ann are not Elite (their only route to it is circular), while Eve and Tim are, since their justification reaches a solid starting point (Eve's yacht, then Tim via Eve).Extending Algorithm 1 to capture LFP and GFP computations
Now we change our algorithm minimally to capture LFP and GFP computations, by simply introducing one boolean switch and an array called
chain.Note there's no shared table
There.chainitself costs nothing beyond what the recursion already carries — it is just the sequence of calls currently open — and leavingTout is what keeps the algorithm sound: a value computed while some pair is still open on the current branch is used only on that branch, and never picked up by another one. A naiveTadded on top would not preserve this.Dropping the cache does cost efficiency, since the same pair can then be recomputed. This is a solved problem rather than an open one: standard Prolog engines already do exactly this kind of caching safely, and that technique can be adapted here directly. So the extension above fixes the semantics, and the efficiency can be recovered with a known method — happy to work that part out separately.
Worth being precise about where this actually applies, and this holds for LFP just as much as for GFP. Since we start from the targets, we only ever compute the part of the fixed point relevant to their validation. A pair that isn't a target and isn't reached via some chain of shape references from a target is never passed to
validateat all; it isn't assumed true (or false) under either reading, it's simply never computed, because nothing we're actually validating ever needs its value.Another thing worth noting: this kind of computation is very much in the spirit of so-called top-down computation. One could easily do the same computation via a classical bottom-up approach instead, using some logic-programming (answer-set programming) tool, and just check the targets at the end. However, that approach would require a new algorithm.
When defining a new algorithm from scratch becomes unavoidable
Negation is where the simple change to the algorithm stops being enough, except for a few special cases covered below.
In the worst case, in the presence of negation, one has to guess an assignment and then check whether that guess is consistent. That approach is intractable. There are, however, special fragments where this can be partly avoided.
Worth flagging up front: all of these approaches can be encoded fairly directly into logic programming, in particular answer-set programming (ASP); see e.g. WWW 2020.
Stratified negation
If negative shape references never participate in a cycle (the classical Datalog-style stratification condition), the schema can be processed stratum by stratum, each one built on the fully-settled result of the strata below it. This stays tractable, and it composes cleanly with the LFP/GFP idea above within each stratum (Andresel et al., WWW 2020).
This means that, in principle, we could still use the extended variant of our Algorithm 1 to do the computation within each stratum. However, we'd need another algorithm on top of it, to orchestrate the computation stratum by stratum. So this is not a case where Algorithm 1 alone suffices.
One caveat on which notion of model is meant here.
Take the same four people as before, and add a second shape that uses negation:
This is stratified: the negation points at
Elite, which is settled by its own cycle first, and no negation occurs inside that cycle.Two assignments are internally consistent here — two supported models:
Both survive checking. Eve is Elite on her yacht and Tim through Eve in either case. The difference is Tom and Ann: in B each is Elite because the other is, which is circular but not contradictory.
Only A is stable. Stable models additionally require every assignment to be founded — derivable without assuming itself — and nothing outside the cycle ever grounds Tom or Ann. This is the same distinction as cautious (LFP) versus brave (GFP) above.
The negation is what makes the difference bite. Without
Ordinary, choosing B merely adds two Elite nodes. With it, choosing B also takesOrdinaryaway from Tom and Ann, so an unfounded guess in one shape silently changes the verdict for another.The distinction matters for tractability. With stable models, plain Datalog-style stratification is enough to stay tractable. With supported models it is not, and one needs the stronger strict stratification condition to recover PTIME (see the ISWC 2018 P&D entry in the references).
Personally, for this case, I think it would be easier to do a separate bottom-up computation and define a separate algorithm that does that in some efficient way.
Unrestricted negation
If the goal is to find some 2-valued satisfying assignment that validates the targets, in the presence of unrestricted negation, the problem gets harder.
In this case, it would be better to have an implementation built entirely around some variant of an ASP or SAT solver, since in the worst case it has to guess at least some part of the shape assignment.
We took exactly this approach in Corman, Florenzano, Reutter, Savković, ISWC 2019: a hybrid strategy that evaluates a small number of SPARQL queries over the endpoint, then uses the answers to build a set of propositional formulas that are passed to a SAT solver.
Unrestricted negation, 3-valued logic
For unrestricted negation there is also a tractable variant, at a small price in complication: we need to allow a third outcome of validation: "undefined," alongside true and false. It's based on a semantics for logic programs called the well-founded semantics, where something is only considered true when it can be inferred without resorting to case-by-case guessing.
Unlike the LFP/GFP extension above, this isn't a one-line addition to Algorithm 1, it needs its own construction (Okulmus & Šimkus, KR 2024, or the ASP-based translation in WWW 2020).
To illustrate the difference between 2- and 3-valued readings, keep Tom and Ann, still friends with each other, and move the negation inside the cycle:
You are Elite if you have a friend who is not. For Tom and Ann this unfolds to
which is the classic pair
p ← ¬q,q ← ¬p. Note this schema is not stratified: the negation now sits in the cycle, so nothing in the previous section applies to it.There are two solutions (stable models): Tom is Elite and Ann is not, or Ann is Elite and Tom is not. Each is internally consistent, and nothing in the schema prefers one over the other.
Summary
† Tractable with the standard caching technique from Prolog engines; see the note under the algorithm.
References
I list papers chronologically and summarize their contributions.