PrivateboundB⟨?x⟩
PrivateclustersVariable to its group; a group may be pinned to the term or the shape all of its members equal.
PrivatemembersThe groups namedMembers was asked about, with the revision of clusters they were read at.
Filled in group by group rather than in one walk, most of the callers wanting a single group. It goes
stale the way readings does, and for the same reason: the members of a group are a function of
clusters alone, and no two states of any two sets share a stamp.
PrivateorderThe variables in the order they were first mentioned, used to keep a pass idempotent.
PrivatereadingsThe last readingsPerGroup taken, with the revision of clusters it was taken at.
Nothing invalidates it: the decomposition is a function of clusters alone, and a stamp is unique to
one state of one set, so a write - or adopt putting a different set here altogether - leaves
the stamp it was taken at unreachable. See readingsPerGroup for why that is the whole of it.
PrivatestrengthStrength per root variable, and only meaningful for variables in a group. The accessor conjuncts about
?o are exactly as strong as what is known about ?o itself, reading a position of an unbound variable
being an error.
PrivateunboundU⟨?x⟩
How many variables the conjunction says something about.
PrivateadoptTakes over the state of a clone that an attempted assertion succeeded on.
The clone to adopt
Conjoins one assertion about one access, in whichever of the states it is - the inverse of conjuncts.
false on a contradiction
PrivateassertResolves an access to a group, asserting a shape for every position it reads through on the way - which is the point rather than a side effect, reading a position of something being what says that something is a triple term.
The access to resolve
the group the access names, or false when one of those shapes contradicts what a group holds
Conjoins B⟨?x⟩: bound(?x).
The variable to assert bound
false on a contradiction
PrivateassertedThe kind of term Θ itself says the group holds: a condition asserted it outright, or Θ holds a shape for the group, which is a triple term by being one.
The group to look up
the term type, or undefined where Θ says nothing about it
Conjoins A⟨a ≡ c⟩ or W⟨a ≡ c⟩ for an arbitrary access, which pins the group that access names and shapes the groups on the way to it.
The access to pin
The term it equals
Whether it holds outright, rather than only where its root is bound
false on a contradiction
PrivateassertConjoins what the source has to satisfy for reading it to yield a value at all, which is what B⟨?x⟩ on a transferred target comes to.
What carries the target's value below
false on a contradiction
PrivateassertRestates on the source what Θ holds about the access being transferred away.
The access being transferred away
What carries its value below
false on a contradiction
PrivateassertConjoins a form that implies bound(?x) of the root it is about, which rules U out, absorbs B and makes
the member strong before apply runs.
The variable the form is about
The narrowing to make once the root is known bound
false on a contradiction
Conjoins A⟨?x ≡ c⟩ or W⟨?x ≡ c⟩, pinning the group of ?x to c - which fixes every member of a clique
at once, and is how an assertion met above a unification travels onto all the variables it unified.
The variable to pin
The term it equals
Whether it holds outright, rather than only where ?x is bound
false when the assertion contradicts what is already known
Conjoins T⟨a : τ⟩ - isIRI(a), isBLANK(a), isLITERAL(a), isTRIPLE(a) - or its weak form,
narrowing the group a names to the one kind of term it may hold.
The access to narrow
The kind of term it holds
Whether it holds outright, rather than only where its root is bound
false on a contradiction
Conjoins U⟨?x⟩: !bound(?x).
The variable to assert unbound
false on a contradiction
PrivateassertConjoins the weak form ¬bnd(?x) ∨ φ of something about the root ?x.
The variable the form is about
The narrowing φ makes
false only where U⟨?x⟩ itself contradicts, a φ the group cannot hold coming to U⟨?x⟩
rather than to an empty conjunction
PrivateassertChecks the invariant a weak member rests on: it is the only variable naming its group.
get reports any other member of a group as a strong edge to its representative without reading strength, which is right only where no weak member has another member to point at. The single way into a group of several is assertUnify, which makes both of its sides strong, so a weak member is alone in its group - and a violation would state a weak edge as a strong one, adding solutions.
The variable just made weak
The variables Θ entails bound(?x) of - every member of a clique, and every variable a shape
reaches, a triple term and each of its positions being bound (S5).
those variable names, which is what lets a structural assertion decide the rules the strong form decides even where the edge itself cannot travel
A copy that shares no state with this one, so that either may be asserted into on its own.
the copy
The independent conjuncts Θ decomposes into: one per reading of every group it can reach from a named variable, plus the two term-less forms.
the conjuncts, every one of them pointing at the representative of its group so that a re-run of the pass absorbs what it finds instead of stacking it
PrivateenforcedWhether matching the pattern the substitution builds already states what the conjunct states.
The conjunct to check
The value per group, from patternValues
whether the pattern enforces it, so that it need not be restated over it
Every group Θ names more than one way, as the ways of naming its value: a variable that is a member of it, or a position of a shape, read from the representative of the group holding that shape.
Several readings is the statement that they are equal - a clique for a group of variables, one edge for
sameTerm(SUBJECT(?o), ?s), and the two are one thing here. A rule deciding per reading would split
such a group into pieces that no longer say it, so it splits the edges instead (splitClique in the pushdown).
A group pinned to a term is not one of them: every reading of it is that term, which already states it.
the readings per group, each list representative first
What Θ decides about the expressions it is substituted into, which is strictly less than what it knows: the term an access is fixed to, which kind of term an access is, and which variables are bound.
the view; a shape may not be substituted into an expression at all (S3), so what travels is only what folds to a term, plus the variable that reads a group most directly
What the conjunction says about one variable, read as a bare access.
What a shape says about the positions is not about this variable at all - it is about the groups those positions name - so it is conjuncts rather than this that reports it.
The variable to look up
the assertion, or undefined when the conjunction says nothing about it
PrivategroupThe conjuncts one group of Θ contributes, given how the whole of it can be read, remembered on the walk that asked for them.
Without the memo the walk is exponential in the depth of the shape: writing a group out asks whether its
positions speak up (shapeIsWitnessed), which writes each of them out and asks the same of
their own positions, so every group below is written once per ancestor and once again per ancestor's
question. FILTER(sameTerm(OBJECT(OBJECT(...(?z))), ?w)) nests as deep as it is written, which made a
fourteen-deep chain a million calls.
The group to write out
The decomposition being written, whose memo this fills in
its conjuncts, shared with whoever asks again on the same walk and so not to be written to
What a pattern takes of Θ, and what it leaves behind: two halves of one decision, decided together off the one set of values written for the groups.
The substitution is rebuildingSubstitution with the shapes written out further: a member of a shaped group maps to the triple term that shape is, its positions filled in with the terms they are pinned to, the variables that name them, and a variable coined for each position nothing names (D4). That last part is why this may only go into a pattern (S3): the pattern is what binds the coined variables, where a condition reading them would error away every row.
The residual is what that pattern does not state, read off the value the pattern holds at each side of
a conjunct rather than off the form of the conjunct. asWritten is what it has to be read against once
the pattern holds those values: Θ keeps saying OBJECT(?o) where the plan says ?o_o, so
isIRI(OBJECT(?o)) is written as isIRI(?o_o), a condition over a variable the pattern binds.
Coins the variable for a position, once per position and query (utils!derivedVarNamer)
the substitution to write into the pattern, the residual to state over it, and the view that residual has to be written through
PrivateisWhether what is said about an access holds outright, rather than only where its root is bound.
The access to check
whether its root is strong
PrivatenamedThe variables in a group, memoised per state of clusters.
Sorting is what makes a group's representative the same one every time, and so what keeps the pass idempotent - but hardly anything asks about a group once. get takes a representative per variable it is asked about, rebuildingSubstitution one per group it rebuilds, and walkReadingsPerGroup two per group, so a pushdown over a filter of a few hundred conditions sorts some thousands of times over, under an eighth of which reads a group this has not already got.
The group to read
them lexicographically, the first being the group's representative; handed out read-only, the memo being shared
PrivatenamesThe variables the conjunction says something about, in the order it first met them.
those variable names
PrivatenarrowingConjoins something that narrows the group an access names: the shapes on the way to the access are
opened, and then narrow says what the group it names may be.
The access to narrow
Whether the narrowing holds outright, or only where the root is bound
What to do to the group, given the clusters of the conjunction it is applied to - which is a copy of this one wherever the weak form has to try the narrowing before committing to it
false on a contradiction
Reads Θ in terms of what an operation binds, converting between the forms at every step of the pushdown.
Where ?x is certainly bound, !bound(?x) is unsatisfiable, so W is A, B is true and U is empty;
where ?x can never be bound, A and B empty the operation by (FBndII) while W and U are true. The
ranges decide the same two things one level finer - a variable whose range is empty never binds, exactly
as one out of scope does, and a variable pinned to something outside a non-empty range cannot be bound
to it, which makes the strong form unsatisfiable and the weak form exactly U⟨?x⟩.
Takes the CPMeta of the operation the filter sits on: the variables it binds in every solution, and the scope it binds with the term types each variable there can take.
the normalised conjunction, or undefined when it makes that operation empty
PrivatepatternThe value the pattern holds where an access reads it: an access is answered exactly as deep as the shapes were written.
The access to read
The value per group, from patternValues
the value, or undefined where the pattern holds none - a weak member among them, the pattern
never writing one
PrivatepatternThe value a pattern holds for every group a variable of Θ names: the term it is pinned to, the triple term its shape is written out as, or the variable that reads it.
Coins the variable for a position nothing names
the value per group; two readings of one group become the same term or the same variable in the same pattern, and matching that pattern is what states the equality Θ carried as a condition
PrivaterangePrivatereadingsEvery group Θ can reach from a variable it names, with the readings of it, representative first.
FILTER(sameTerm(?x, ?y)) - one group, readings [?x, ?y], giving the edge ?y = ?x.FILTER(sameTerm(SUBJECT(?o), ?s)) - ?o's group holds [?o]; its subject position holds
[?s, SUBJECT(?o)], giving the edge SUBJECT(?o) = ?s. The other two positions are anonymous.FILTER(sameTerm(SUBJECT(?o), :a)) - the subject position has one reading, so no edge; it writes
SUBJECT(?o) = :a from that single reading.
Memoised per state of clusters, which is the only thing the walk reads: an operation asks for the
decomposition several times over (conjuncts, equatedReadings, patternValues), and
the walk is a BFS over every group plus a sort per group. Handed out read-only, the memo being shared.the readings per group; a group nothing reaches is left out, being what is left of a shape a variable was taken out of, which nothing may be written about
The substitution the strong assertions stand for: a pinned member maps to its term, a clique member to its representative, and a member of a shaped group to the triple term that shape is - written out of the variables that already read its positions, and undecided where a position is read by nothing at all.
the substitution, everything in which is already written elsewhere, so it stays usable outside a pattern where S3 rules the materialised shape out (intoPattern)
PrivaterememberPrivateremoveTakes a variable out of its group, dropping the group when nothing is left to be equal to.
The variable to remove
PrivaterepresentativeThe representative of a group: its lexicographically first member, so that the pass stays idempotent.
The group to read
the representative, or undefined for a group no variable names
PrivateresolveThe group an access names, without asserting anything.
The access to resolve
the group, or undefined when Θ does not name it yet
PrivateshapeWhether a position of the shape says something of its own, in which case T⟨representative : Quad⟩ need not be stated - reading a position already entails that what it is read through is a triple term.
The shaped group to ask about
The decomposition being written
whether some position speaks up
PrivateshapeWhether writing the shape of a group into a pattern states anything the pattern did not already state, which is exactly whether some position of it, however deep, holds a term or is named.
The group to ask about
whether writing it is worth the variables it coins
Splits Θ in two: a conjunct all of whose variables match predicate goes inside, the rest outside.
Which variables belong inside
the two halves, which together hold every conjunct and so are equivalent to the whole
PrivatestrongThe substitution replacing every strong member by what valueOf makes of its group, which is the one
thing rebuildingSubstitution and intoPattern differ in.
The value to substitute for a group, undefined to leave its members alone
the substitution, never mapping a variable to itself - the representative of its own group is
already written where it is, and re-binding it would be the BIND(?x AS ?x) the algebra raises on
PrivatesubstitutionWhat an expression may be given in place of an access: the term it reads where Θ decides one, and otherwise the variable that reads its group most directly.
The access to substitute
the term or variable, or undefined where Θ decides neither
PrivatetermThe term a group is fixed to, which for a shape is the triple term its decided positions make.
One walk for both callers, so that the two cannot come to disagree about what a shape is. A caller that always has a value for an undecided group always gets a term back, which the second signature states: every way out of the walk is a pin's term, a quad built from three of those, or that value.
The group to resolve
the term, or undefined where a position is decided by nothing at all
The term a group is fixed to, which for a shape is the triple term its decided positions make.
One walk for both callers, so that the two cannot come to disagree about what a shape is. A caller that always has a value for an undecided group always gets a term back, which the second signature states: every way out of the walk is a pin's term, a quad built from three of those, or that value.
The group to resolve
What to put where the pins decide nothing; a substitution into an expression has nothing to offer (S3), a substitution into a pattern has the variable reading the group
the term, or undefined where a position is decided by nothing at all
The term a group is fixed to, which for a shape is the triple term its decided positions make.
One walk for both callers, so that the two cannot come to disagree about what a shape is. A caller that always has a value for an undecided group always gets a term back, which the second signature states: every way out of the walk is a pin's term, a quad built from three of those, or that value.
The group to resolve
What to put where the pins decide nothing; a substitution into an expression has nothing to offer (S3), a substitution into a pattern has the variable reading the group
the term, or undefined where a position is decided by nothing at all
PrivatetermThe kind of term the group has to be told to be: only what is not already entailed by the rest of what the group writes out, since restating it would stop the pass being idempotent.
The group to look at
The decomposition being written
the term type, or undefined when nothing has to be told
The single condition the (non-empty) conjunction stands for, each conjunct in the form it carries.
The transformation context
the condition
Θ with name taken out of it and whatever it said about it restated against replacement - what
carries its value where the result is going, which the caller is responsible for establishing.
For a BIND that is its expression: below BIND(?z AS ?t) it is ?z that holds what ?t holds above.
An access takes over everything the group holds, a term is what the group has to be, and a construction
is the shape itself, so what the group said about a position is restated about the variable holding it.
The variable to take out
What carries its value below
the transferred conjunction, or undefined when the transfer contradicts what is known
The conjuncts of Θ about one access alone: what it is fixed to, which kind of term it is, whether it is bound.
conjuncts without the edges, which are the only conjuncts mentioning two accesses and so the only ones a rule cannot decide by looking at a single one
PrivatewalkThe walk readingsPerGroup memoises, run once per state of clusters.
the readings per group, each list representative first
PrivatewriteThe walk groupConjuncts memoises, run once per group and decomposition.
A shape holds no cycles (datastructures/TermClusterSet!TermClusterSet), so a group is never asked for while it is being written, and the memo is filled in with a finished list.
The group to write out
The decomposition being written
its conjuncts
PrivatewritesWhether the group, or anything the shape of it reaches, writes a conjunct of its own.
The group to ask about
The decomposition being written
whether the subtree writes anything - the whole subtree, since a position that says nothing itself may hold one that does
StaticofThe conjunction of the assertions of conjuncts, which never contradict when every one of them is
entailed by one satisfiable Θ - a subset of its conjuncts, or
the weakened and entailed forms the pushdown derives from them, which are implied by what they came
from and so satisfiable with it.
The conjuncts to conjoin
the conjunction they make
A set of assertions Θ, in the states an assertion about an access can be in:
sameTerm(?x, c)!bound(?x) ∨ sameTerm(?x, c)sameTerm(?x, ?rep)isIRI(?x),isBLANK(?x),isLITERAL(?x),isTRIPLE(?x)!bound(?x) ∨ is<τ>(?x)!bound(?x)/bound(?x), no termEvery row is written back in the form the recogniser reads straight back into the same state, which is what toExpression and collectAssertions being inverses of each other means. What was derived rather than asserted - that a subject holds no literal, that a shaped group holds a triple term - is left unsaid (AssertionClusterSet).
Two invariants shape everything below:
sameTerm(?o, <<( ... )>>)(S2), only as onesameTerm(SUBJECT(?o), ...)per position that says something: the positions nobody named would be unbound wherever the filter sits, so the condition would error and drop every row.The
assert...methods report a contradiction by returningfalserather than raising: one variable asserted to be two terms at once is an ordinary outcome, which the pass turns into the empty operation. A conjunction they returnedfalsefor holds no meaningful state and has to be discarded.