Unification, pattern matching against the indexed store, and backward chaining.
Matching is type-aware: a unary type predicate is matched over the subtype
closure, so an antecedent (animal ?x) is satisfied by a stored (dog Muffet).
This is how increasing an individual's specificity never loses the reasoning
that applied to its more general types — we consult the genl closure at match
time rather than materializing supertype facts.
Unification, pattern matching against the indexed store, and backward chaining. Matching is *type-aware*: a unary type predicate is matched over the subtype closure, so an antecedent `(animal ?x)` is satisfied by a stored `(dog Muffet)`. This is how increasing an individual's specificity never loses the reasoning that applied to its more general types — we consult the genl closure at match time rather than materializing supertype facts.
How lead-candidates narrows a non-symmetric literal with 2 or more indexable ground
arguments: :two (default), :all, :above-floor or :off. Every choice is a pure
cost decision: the result is a subset of the single leading column and a superset of the
matches. See docs/inference.md, Resolution reads.
How `lead-candidates` narrows a non-symmetric literal with 2 or more indexable ground arguments: `:two` (default), `:all`, `:above-floor` or `:off`. Every choice is a pure cost decision: the result is a subset of the single leading column and a superset of the matches. See docs/inference.md, Resolution reads.
The :above-floor strategy's floor: skip the intersection when the leading (tightest)
column already returns no more than this many handles, where feeding that short
superset straight to unify costs less than allocating an intersection set.
The `:above-floor` strategy's floor: skip the intersection when the leading (tightest) column already returns no more than this many handles, where feeding that short superset straight to `unify` costs less than allocating an intersection set.
Whether match-one may retrieve candidate handles from a secondary argument root
instead of always walking the trie. candidate-handles intersects the pattern's scoped
argument roots (sentexes-with-args). The candidates are a superset of the trie's hits
and unify filters them, so the switch changes cost and never the matches. Binding it
false forces the trie, which arg_root_retrieval_test compares against. Default true.
See docs/indexing.md, Argument-root retrieval.
Whether `match-one` may retrieve candidate handles from a secondary argument root instead of always walking the trie. `candidate-handles` intersects the pattern's scoped argument roots (`sentexes-with-args`). The candidates are a superset of the trie's hits and `unify` filters them, so the switch changes cost and never the matches. Binding it false forces the trie, which `arg_root_retrieval_test` compares against. Default true. See docs/indexing.md, Argument-root retrieval.
While true, kb-sentex leaves a rule's open applications as written: the spelling
assert records as a premise's written one (integrate/spellings-key).
While true, `kb-sentex` leaves a rule's open applications as written: the spelling `assert` records as a premise's written one (`integrate/spellings-key`).
Read the store as stored rather than as believed: CxEverything, and nothing else.
A named opt-out of the belief-filtering invariant, so it is a dynamic var scoped to one
read by the entry point that resolves the symbol. It gives a syntactic query with no
JTMS read, the only one that sees a defeated default. An answer taken under it is not a
justification and must not reach why.
Read the store as stored rather than as believed: `CxEverything`, and nothing else. A named opt-out of the belief-filtering invariant, so it is a dynamic var scoped to one read by the entry point that resolves the symbol. It gives a syntactic query with no JTMS read, the only one that sees a defeated default. An answer taken under it is not a justification and must not reach `why`.
True to cut a fan of any size by the slot predicate sets (slot-cut), not only one of
slot-cut-min members or more. For a walk that asks one literal of each of many terms,
few of which any member holds, where the member reads are the walk's cost
(inherit/fact-reach). A fan holding a comparison is read whole all the same: a
comparison is stored under its sibling's functor or as a longer chain
(sx/comparison-siblings, sx/chained-comparisons), which the slot sets of the
probe's functor and positions do not name.
True to cut a fan of any size by the slot predicate sets (`slot-cut`), not only one of `slot-cut-min` members or more. For a walk that asks one literal of each of many terms, few of which any member holds, where the member reads are the walk's cost (`inherit/fact-reach`). A fan holding a comparison is read whole all the same: a comparison is stored under its sibling's functor or as a longer chain (`sx/comparison-siblings`, `sx/chained-comparisons`), which the slot sets of the probe's functor and positions do not name.
An optional observer of the DFS's dead ends, (fn [goal depth]), or nil (default). A
dead end is a subgoal, substituted under the frame's bindings, that no visible believed
fact and no rule consequent unified with. A branch cut short (loop guard, :max-depth,
term-growth ceiling) is not reported. The return value is ignored. Only prove's
loop reports. docs/abduction.md, The dead end.
An optional observer of the DFS's dead ends, `(fn [goal depth])`, or nil (default). A dead end is a subgoal, substituted under the frame's bindings, that no visible believed fact and no rule consequent unified with. A branch cut short (loop guard, `:max-depth`, term-growth ceiling) is not reported. The return value is ignored. Only `prove`'s loop reports. docs/abduction.md, The dead end.
Answer a context-scoped (p a ?x) query with the set-algebra retrieval
(matches-hierarchical) rather than the nested |context-up| × |specs| fan-out. On by
default: a pure cost decision that never changes the answer set. Bound false, it runs
the reference fan-out matches_hierarchical_test compares against. See docs/indexing.md,
Hierarchical retrieval.
Answer a context-scoped `(p a ?x)` query with the set-algebra retrieval (`matches-hierarchical`) rather than the nested `|context-up| × |specs|` fan-out. On by default: a pure cost decision that never changes the answer set. Bound false, it runs the reference fan-out `matches_hierarchical_test` compares against. See docs/indexing.md, Hierarchical retrieval.
For a non-symmetric literal with a spec closure, which side lead-candidates leads
from. :scoped: one predicate-scoped node per sub-predicate (O(|specs|) probes, the
reference matches_hierarchical_test forces). :agnostic: the slot predicate set
([:argument-slot pos term]) kept to specs, then each kept functor's node. :auto
(default): :agnostic when the term holds no more postings at this position than there
are specs, else :scoped; the choice is content-derived (count-with-arg against a
realised count). A pure cost decision. checks/membership-handles reads it too.
For a non-symmetric literal with a spec closure, which side `lead-candidates` leads from. `:scoped`: one predicate-scoped node per sub-predicate (O(|specs|) probes, the reference `matches_hierarchical_test` forces). `:agnostic`: the slot predicate set (`[:argument-slot pos term]`) kept to `specs`, then each kept functor's node. `:auto` (default): `:agnostic` when the term holds no more postings at this position than there are specs, else `:scoped`; the choice is content-derived (`count-with-arg` against a realised `count`). A pure cost decision. `checks/membership-handles` reads it too.
A volatile {[x context] memberships} the separation's denial reads a term's
memberships through while bound (checks/cover-problem binds it over one write's
covers, where nothing is stored), or nil to read type-memberships afresh.
A volatile `{[x context] memberships}` the separation's denial reads a term's
memberships through while bound (`checks/cover-problem` binds it over one write's
covers, where nothing is stored), or nil to read `type-memberships` afresh.Candidate handles per prefetch hint a retrieval path gives its record store, or false
(the default) to give none. On, a walk takes candidates a chunk at a time and tells a
store implementing protocols/Prefetching which handles the chunk will ask for. The
hint returns nothing and every record still arrives through get-sentex, so this is a
cost setting. It pays over a non-local fetch only; the signal is a large :fetches
tally (vaelii.impl.profile) against wall clock. The chunk is the unit of over-fetch.
false or a positive integer; anything else, true above all, is refused where it is
bound.
Candidate handles per prefetch hint a retrieval path gives its record store, or `false` (the default) to give none. On, a walk takes candidates a chunk at a time and tells a store implementing `protocols/Prefetching` which handles the chunk will ask for. The hint returns nothing and every record still arrives through `get-sentex`, so this is a cost setting. It pays over a non-local fetch only; the signal is a large `:fetches` tally (`vaelii.impl.profile`) against wall clock. The chunk is the unit of over-fetch. `false` or a positive integer; anything else, `true` above all, is refused where it is bound.
nil, or [pred context entries]: while bound, kb-sentex sorts a literal on pred in
context by the permuting marks entries lists (mark-entries' keys) and no others,
so chain/respell-rows! stores, and core/handle-of looks up, the spelling a reader
that believes those marks reads (spelling-planner).
nil, or `[pred context entries]`: while bound, `kb-sentex` sorts a literal on `pred` in `context` by the permuting marks `entries` lists (`mark-entries`' keys) and no others, so `chain/respell-rows!` stores, and `core/handle-of` looks up, the spelling a reader that believes those marks reads (`spelling-planner`).
Does an open negative pattern's argument-root read leave out the positive facts at the
index (negative-root-handles)? A pure cost decision, like *hierarchical-retrieval*:
match-one drops a positive candidate on polarity either way, so the answer set is the
same. Bind it false for the reference read, which fetches every candidate's record
(negative_roots_test).
Does an open negative pattern's argument-root read leave out the positive facts at the index (`negative-root-handles`)? A pure cost decision, like `*hierarchical-retrieval*`: `match-one` drops a positive candidate on polarity either way, so the answer set is the same. Bind it false for the reference read, which fetches every candidate's record (`negative_roots_test`).
Whether candidate-handles may use the structural trie to narrow a positive pattern
with a nested compound argument, (mass ?o (QuantityFn ?n Kilogram)). On (default),
p/lookup narrows on the compound's interior; off, the functor extent is the superset.
The structural key is written unconditionally, so direct p/lookup paths always walk it.
On and off return the same matches (structural_index_test). Negative and flat patterns
are untouched.
Whether `candidate-handles` may use the structural trie to narrow a positive pattern with a nested compound argument, `(mass ?o (QuantityFn ?n Kilogram))`. On (default), `p/lookup` narrows on the compound's interior; off, the functor extent is the superset. The structural key is written unconditionally, so direct `p/lookup` paths always walk it. On and off return the same matches (`structural_index_test`). Negative and flat patterns are untouched.
(any-corresponding-predicates? kb)Does the KB declare any functionCorrespondingPredicate? One O(1) functor count.
Does the KB declare any `functionCorrespondingPredicate`? One O(1) functor count.
(arg-admits-fn kb pred context)A predicate (fn [x position] …): does every type the instance-level declarations
arg-constraints-at answers for pred's position (0-based) from context admit term
x? A type admits a term unless the term holds a believed type context sees as
disjoint from it, so an untyped term is admitted, as assert admits it, and nothing is
concluded from the declaration. Each term's types are read once per returned fn, and
only at a position some declaration types: an undeclared position admits every term.
A predicate `(fn [x position] …)`: does every type the instance-level declarations `arg-constraints-at` answers for `pred`'s `position` (0-based) from `context` admit term `x`? A type admits a term unless the term holds a believed type `context` sees as disjoint from it, so an untyped term is admitted, as `assert` admits it, and nothing is concluded from the declaration. Each term's types are read once per returned fn, and only at a position some declaration types: an undeclared position admits every term.
Per declaration functor, the :kind its entries carry and its shape: :at types
position n, (K P n T); :rest types n and every later one, (K P n T); :every
types every position, (K P T), read as :rest from 1.
Per declaration functor, the `:kind` its entries carry and its shape: `:at` types position n, `(K P n T)`; `:rest` types n and every later one, `(K P n T)`; `:every` types every position, `(K P T)`, read as `:rest` from 1.
(arg-constraints kb pred context)The argument constraints binding pred's tuples as context sees them, as entries
{:from n :to m :type T :kind K :via P} in declaration order. :to is nil for a tail
running to the last argument. :kind is :instance (arg, argAndRest), :type
(genlArg, argAndRestGenl, argsGenl) or :quoted (quotedArg). :via is the
predicate the declaration is written on (constraining-predicates). arg-constraints-at
answers for one position. A malformed declaration is dropped. Held in the taxonomy's
closure memo for one stretch of the change clock (tax/clock-held).
The argument constraints binding `pred`'s tuples as `context` sees them, as entries
`{:from n :to m :type T :kind K :via P}` in declaration order. `:to` is nil for a tail
running to the last argument. `:kind` is `:instance` (`arg`, `argAndRest`), `:type`
(`genlArg`, `argAndRestGenl`, `argsGenl`) or `:quoted` (`quotedArg`). `:via` is the
predicate the declaration is written on (`constraining-predicates`). `arg-constraints-at`
answers for one position. A malformed declaration is dropped. Held in the taxonomy's
closure memo for one stretch of the change clock (`tax/clock-held`).(arg-constraints-at kb pred context n)The arg-constraints entries that type position n of pred's tuples from
context: each :at entry for n, and each tail entry starting at or before it.
The `arg-constraints` entries that type position `n` of `pred`'s tuples from `context`: each `:at` entry for `n`, and each tail entry starting at or before it.
(attitude-application? modal term)Is term (P agent proposition) for a declared modal_predicate P — the shape
BeliefProjectionProver projects? Its third argument is what the agent holds true,
and the shape test is the prover's own: arity 2, over a sentence-shaped proposition. A
(believes A Foo) naming a bare term is not one — that argument refers rather than
quotes, and stays transparent.
Is `term` `(P agent proposition)` for a declared `modal_predicate` `P` — the shape `BeliefProjectionProver` projects? Its **third** argument is what the agent holds true, and the shape test is the prover's own: arity 2, over a sentence-shaped proposition. A `(believes A Foo)` naming a bare term is not one — that argument refers rather than quotes, and stays transparent.
(belief-blind?)*belief-blind*, read once by a retrieval path rather than once per candidate: a
^:dynamic deref per candidate handle is measurable in the innermost loop. Hoisting
is sound because the entry point binds it around the whole read and blind-seq
re-establishes it per realization step.
`*belief-blind*`, read once by a retrieval path rather than once per candidate: a `^:dynamic` deref per candidate handle is measurable in the innermost loop. Hoisting is sound because the entry point binds it around the whole read and `blind-seq` re-establishes it per realization step.
(believed-at? kb handle context)Is handle believed as context reads it: IN in the network, and not hidden from
context by a placed defeat in force there, or by resting only on a handle one hides
(exc/belief-hidden-fn)? The stored excepts are not applied, since an except is
visibility and this is belief.
The reader for a caller holding a sentex and no reader is the sentex's own context. A sentex resting only on a member every reader of it hides is IN in the network and hidden from every context that can read it, and this answers false for it.
Is `handle` believed as `context` reads it: IN in the network, and not hidden from `context` by a placed `defeat` in force there, or by resting only on a handle one hides (`exc/belief-hidden-fn`)? The stored excepts are not applied, since an `except` is visibility and this is belief. The reader for a caller holding a sentex and no reader is the sentex's own context. A sentex resting only on a member every reader of it hides is IN in the network and hidden from every context that can read it, and this answers false for it.
(believed-correspondences kb context match?)The correspondence declarations context sees (visible-declarations) as [function predicate position-or-nil] triples, kept where match? holds of the triple.
The correspondence declarations `context` sees (`visible-declarations`) as `[function predicate position-or-nil]` triples, kept where `match?` holds of the triple.
(blind-seq s)s, realized under *belief-blind* one element at a time, with the binding
re-established for each. A plain binding around a read is wrong here: the read
answers with a lazy seq, the frame is popped before the first element is computed, and
the belief filter runs unbound with nothing reporting it.
`s`, realized under `*belief-blind*` one element at a time, with the binding re-established for each. A plain `binding` around a read is wrong here: the read answers with a lazy seq, the frame is popped before the first element is computed, and the belief filter runs unbound with nothing reporting it.
(concludes? kb pred context)Is concluding-rule-handles non-empty, asked in every context: the same buckets, read
until the first one holding a rule. provers/shadowing-channels asks only this, once per
goal. It reads past the reader's ancestor set because the answer only decides whether a
computed prover may answer alone: a rule the reader cannot see sends the goal down the
union path, which costs time and never an answer.
Is `concluding-rule-handles` non-empty, asked in every context: the same buckets, read until the first one holding a rule. `provers/shadowing-channels` asks only this, once per goal. It reads past the reader's ancestor set because the answer only decides whether a computed prover may answer alone: a rule the reader cannot see sends the goal down the union path, which costs time and never an answer.
(concluding-rule-handles kb pred)(concluding-rule-handles kb pred context)(concluding-rule-handles kb pred context visible)Handles of rules whose consequent predicate is pred or a spec of it, the backward dual
of fire-rules-for. Plus the variable-consequent catch-all bucket
(p/var-consequent-key). A variable pred answers every rule stated where visible
reaches (reads/as-stored-rules-in). A non-symbol pred degrades to the plain lookup.
With context the spec fan walks the genl edges visible from it; with visible, a
context set, each index read returns only rules stated in one of those contexts. The
cost is one probe per spec. See docs/inference.md, Resolution reads.
Handles of rules whose consequent predicate is `pred` or a spec of it, the backward dual of `fire-rules-for`. Plus the variable-consequent catch-all bucket (`p/var-consequent-key`). A variable `pred` answers every rule stated where `visible` reaches (`reads/as-stored-rules-in`). A non-symbol `pred` degrades to the plain lookup. With `context` the spec fan walks the genl edges visible from it; with `visible`, a context set, each index read returns only rules stated in one of those contexts. The cost is one probe per spec. See docs/inference.md, Resolution reads.
(constraining-predicates kb kind pred context & [memos])The predicates whose argument declarations of kind kind bind a pred tuple: pred
itself first, then every super-predicate of it context can see that some sentence
declares kind of, sorted. (arg parentOf 1 person) constrains every fatherOf tuple
given (genl fatherOf parentOf). Both readers of a declaration come here
(checks/declaration-reader, provers/inferred-types). Filtered against the global
:props set (tax/arg-declaration-props); [] when it is empty. memos, a volatile
map held for one still taxonomy, keeps a tax/genls-among memo per kind.
The predicates whose argument declarations of kind `kind` bind a `pred` tuple: `pred` itself first, then every super-predicate of it `context` can see that some sentence declares `kind` of, sorted. `(arg parentOf 1 person)` constrains every `fatherOf` tuple given `(genl fatherOf parentOf)`. Both readers of a declaration come here (`checks/declaration-reader`, `provers/inferred-types`). Filtered against the global `:props` set (`tax/arg-declaration-props`); `[]` when it is empty. `memos`, a volatile map held for one still taxonomy, keeps a `tax/genls-among` memo per `kind`.
(contrapositive-predicates kb f context)[straight swapped]: the predicates a negated pattern on f fans over from the vantage
context, f's genl closure through the edges the reader holds at :monotonic
(tax/contrapositive-closure under holding-class). straight members are read with
their arguments as written, swapped ones with arguments 1 and 2 exchanged. The one
definition the negated arms of match1, subsuming-unify and fanned-match read.
`[straight swapped]`: the predicates a negated pattern on `f` fans over from the vantage `context`, `f`'s `genl` closure through the edges the reader holds at `:monotonic` (`tax/contrapositive-closure` under `holding-class`). `straight` members are read with their arguments as written, `swapped` ones with arguments 1 and 2 exchanged. The one definition the negated arms of `match1`, `subsuming-unify` and `fanned-match` read.
(correspondence-declarations kb context)The correspondence declarations context sees (visible-declarations) as [function predicate position-or-nil handle] rows, in content order of the declaration.
The correspondence declarations `context` sees (`visible-declarations`) as `[function predicate position-or-nil handle]` rows, in content order of the declaration.
(correspondence-of kb f m context)The [predicate position] declared for function f applied to m arguments among
the declarations context sees (believed-correspondences), or nil. position
defaults to m + 1, the value last. Nil when context sees more than one declaration
for f (docs/nat.md, The corresponding predicate).
The `[predicate position]` declared for function `f` applied to `m` arguments among the declarations `context` sees (`believed-correspondences`), or nil. `position` defaults to `m + 1`, the value last. Nil when `context` sees more than one declaration for `f` (docs/nat.md, The corresponding predicate).
The declaration relating a NAT function to the predicate stating the same thing.
The declaration relating a NAT function to the predicate stating the same thing.
(corresponding-values kb E context){value [fact-handle …]} for the ground NAT expression E read from context
(CxUniverse when nil): the value each visible corresponding fact names, spelled under
context's merges, with the believed facts naming it. Empty when the declarations
context sees give E's function no single correspondence; a variable context
reads every declaration and every context.
`{value [fact-handle …]}` for the ground NAT expression `E` read from `context`
(CxUniverse when nil): the value each visible corresponding fact names, spelled under
`context`'s merges, with the believed facts naming it. Empty when the declarations
`context` sees give `E`'s function no single correspondence; a variable `context`
reads every declaration and every context.How many levels of compound nesting a subgoal may add over the deepest term its own
derivation path has met (term-depth) before prove-from cuts the branch: the
:max-term-growth bound, where a caller names none. It catches the recursion the
per-path seen set cannot, a rule nesting a function around a head variable. The basis
rises when a leaf match binds a deep stored term (grown-term-base) and never when a
rule expands. See docs/inference.md, max-term-growth.
How many levels of compound nesting a subgoal may add over the deepest term its own derivation path has met (`term-depth`) before `prove-from` cuts the branch: the `:max-term-growth` bound, where a caller names none. It catches the recursion the per-path `seen` set cannot, a rule nesting a function around a head variable. The basis rises when a leaf match binds a deep stored term (`grown-term-base`) and never when a rule expands. See docs/inference.md, max-term-growth.
(defeatable-goal? idx goal)Could an answer to goal be one belief has already defeated — is its functor one some
defeated datum carries? False for every goal when idx is nil.
This is the push-time presence check: a chainer that answers false here adds no check to the goal at all, so a KB with no defeat on that predicate runs the search it always ran.
Could an answer to `goal` be one belief has already defeated — is its functor one some defeated datum carries? False for every goal when `idx` is nil. This is the push-time presence check: a chainer that answers false here adds no check to the goal at all, so a KB with no defeat on that predicate runs the search it always ran.
(defeated-answer? kb idx sentence context)Is sentence, an answer a rule expansion produced, a stored member of a nogood
(defeated-index) that a defeat in force, or a placed conflict, removes at the query's
reader (exc/defeats-of): context for a concrete one, the member's own context for an
unscoped read? A guard defeat covers one firing and removes no answer. Canonicalized
against the KB (kb-sentex) before the lookup.
Is `sentence`, an answer a rule expansion produced, a stored member of a nogood (`defeated-index`) that a defeat in force, or a placed conflict, removes at the query's reader (`exc/defeats-of`): `context` for a concrete one, the member's own context for an unscoped read? A guard defeat covers one firing and removes no answer. Canonicalized against the KB (`kb-sentex`) before the lookup.
(defeated-index kb)What the backward chainers filter a rule-expanded answer against: {:standing {sentence #{handle}} :functors #{functor}} over the targets of the placed defeats
(reads/as-stored-named-global) and, while an except is stored, the members of the
placed (contradicts …). Nil when the walk reads nothing (exc/placed-reads?), the
common case. :functors keeps the cost off a KB with a defeat on another predicate.
Built once per query, since a query writes nothing. defeated-answer? asks the query's
reader whether it takes a member OUT (docs/nmtms.md, A defeat is scoped to its vantage).
What the backward chainers filter a rule-expanded answer against: `{:standing
{sentence #{handle}} :functors #{functor}}` over the targets of the placed defeats
(`reads/as-stored-named-global`) and, while an `except` is stored, the members of the
placed `(contradicts …)`. Nil when the walk reads nothing (`exc/placed-reads?`), the
common case. `:functors` keeps the cost off a KB with a defeat on another predicate.
Built once per query, since a query writes nothing. `defeated-answer?` asks the query's
reader whether it takes a member OUT (docs/nmtms.md, A defeat is scoped to its vantage).(displaced-terms-in kb visible? sentence)The {old-term representative} rewrites sentence undergoes under visible?, by the
traversal representative-term rewrites with, so a mention held opaque to a sameAs is
not reported displaced.
The `{old-term representative}` rewrites `sentence` undergoes under `visible?`, by the
traversal `representative-term` rewrites with, so a mention held opaque to a `sameAs` is
not reported displaced.(entries-at kb entries reader)The entries of entries some supporter of which reader believes
(supporter-believed?), as a set.
The entries of `entries` some supporter of which `reader` believes (`supporter-believed?`), as a set.
(equation? sentence)Is sentence a positive equation, (rewriteOf P D), (sameAs A B) or (equals A B)
at the top? Migration never restates one, so retired-for? never reports one retired
and goal-normal-form asks an equation goal as spelled (docs/equality.md, "Answering
an equation").
Is `sentence` a positive equation, `(rewriteOf P D)`, `(sameAs A B)` or `(equals A B)` at the top? Migration never restates one, so `retired-for?` never reports one retired and `goal-normal-form` asks an equation goal as spelled (docs/equality.md, "Answering an equation").
(exception-aware-placements kb handles contexts)Placement candidates for handles stated in contexts: the maximal common
descendants of contexts, or, while an except hides one of handles somewhere, the
maximal contexts among them that see every handle with no except hiding it
(supporter-visible? with no defeat read). exc/closure-excepted-anywhere? is the
coarse presence check, so the ordinary path walks no ancestor set when no except reaches
the supporters. A reading pass holds the check per handle (tax/pass-held). Assertion
contexts alone do not decide the case, since an except can hide a supporter at its own
context while a meta-exception restores it in only one descendant ancestor set.
Placement candidates for `handles` stated in `contexts`: the maximal common descendants of `contexts`, or, while an except hides one of `handles` somewhere, the maximal contexts among them that see every handle with no except hiding it (`supporter-visible?` with no `defeat` read). `exc/closure-excepted-anywhere?` is the coarse presence check, so the ordinary path walks no ancestor set when no except reaches the supporters. A reading pass holds the check per handle (`tax/pass-held`). Assertion contexts alone do not decide the case, since an except can hide a supporter at its own context while a meta-exception restores it in only one descendant ancestor set.
(fanned-match kb sentence vantage raw mapcat-fn)(fanned-match kb sentence vantage raw mapcat-fn indexed?)The fan-out shared by every matcher: decompose sentence into the functor that fans and
the rebuild that puts it back, take the functor's closure from vantage, and run raw
(the caller's as-written retrieval) over each member with mapcat-fn. A variable or
absent functor fans not at all. A negation fans its body's functor upward
(contrapositive-predicates, :monotonic edges) and rebuilds the not per member. A
singleton closure is f itself. A genlInverse member is read swapped
(tax/signed-closure, docs/inference.md). indexed? cuts a wide fan with slot-cut.
The fan-out shared by every matcher: decompose `sentence` into the functor that fans and the rebuild that puts it back, take the functor's closure from `vantage`, and run `raw` (the caller's as-written retrieval) over each member with `mapcat-fn`. A variable or absent functor fans not at all. A negation fans its body's functor upward (`contrapositive-predicates`, `:monotonic` edges) and rebuilds the `not` per member. A singleton closure is `f` itself. A `genlInverse` member is read swapped (`tax/signed-closure`, docs/inference.md). `indexed?` cuts a wide fan with `slot-cut`.
(formula-position? kb pred n)Does a believed arg, argN or quotedArg declaration type position n of pred
as a formula or a type under it, as (arg ist 2 sentence) does? Read unscoped: a
rule's stored spelling and its hold are one record every reader shares.
Does a believed `arg`, `argN` or `quotedArg` declaration type position `n` of `pred` as a `formula` or a type under it, as `(arg ist 2 sentence)` does? Read unscoped: a rule's stored spelling and its hold are one record every reader shares.
(formula-type? kb t)Is t formula or a type under it? Read unscoped, as formula-position? reads it.
Is `t` `formula` or a type under it? Read unscoped, as `formula-position?` reads it.
(freshen-rule {:keys [antecedents consequent guard] :as rule} taken)rule with every variable taken already speaks for renamed apart. Without it,
(anc ?x ?z) :- (parentOf ?x ?y) (anc ?y ?z) expanded twice on one path unifies ?x with
both the grandchild and the child and answers only at distance one. Nothing is renamed
when nothing clashes. The exceptWhen guard reads the rule's own variable names from a
completed binding map, so a renamed rule's guard is wrapped to bind those names to this
instance's variables.
`rule` with every variable `taken` already speaks for renamed apart. Without it, `(anc ?x ?z) :- (parentOf ?x ?y) (anc ?y ?z)` expanded twice on one path unifies `?x` with both the grandchild and the child and answers only at distance one. Nothing is renamed when nothing clashes. The `exceptWhen` guard reads the rule's own variable names from a completed binding map, so a renamed rule's guard is wrapped to bind those names to this instance's variables.
(goal-alternatives kb goals unmatched context)Conjunction goals read through the correspondence declarations context sees, as the
vector of conjunctions whose answers the reader merges (docs/nat.md, The corresponding
predicate). A nil or variable context reads every declaration through a predicate
variable (goal-readings). An application with one believed correspondence reads its
predicate; with several, or a variable-functor application outside a sentence position
(arg-app?), one conjunction per distinct declaration shape. An and goal is read as
its conjuncts. An application with no reading becomes unmatched, so the conjunction
answers nothing. The reifiable mark is read unscoped.
Conjunction `goals` read through the correspondence declarations `context` sees, as the vector of conjunctions whose answers the reader merges (docs/nat.md, The corresponding predicate). A nil or variable `context` reads every declaration through a predicate variable (`goal-readings`). An application with one believed correspondence reads its predicate; with several, or a variable-functor application outside a sentence position (`arg-app?`), one conjunction per distinct declaration shape. An `and` goal is read as its conjuncts. An application with no reading becomes `unmatched`, so the conjunction answers nothing. The reifiable mark is read unscoped.
(goal-held-as-spelled? goal)Is goal asked as spelled, exempt from the goal rewrite? A different goal is,
since its prover reads class membership, and so is a positive equation (equation?),
whose arguments are mentions (docs/equality.md, "What a merge does" step 3).
Is `goal` asked **as spelled**, exempt from the goal rewrite? A `different` goal is, since its prover reads class membership, and so is a positive equation (`equation?`), whose arguments are mentions (docs/equality.md, "What a merge does" step 3).
(goal-key g)A goal with all variables collapsed to ?, for loop detection: two goals that
differ only in variable names share a key.
A goal with all variables collapsed to `?`, for loop detection: two goals that differ only in variable names share a key.
(goal-normal-form kb goal context)normal-form for a goal, as context sees the merges, except for a goal
goal-held-as-spelled? exempts. kb/rewrite-goal is the read entry points' spelling;
BeliefProjectionProver calls this one to put a proposition into the normal form of
the agent whose belief it is.
`normal-form` for a **goal**, as `context` sees the merges, except for a goal `goal-held-as-spelled?` exempts. `kb/rewrite-goal` is the read entry points' spelling; `BeliefProjectionProver` calls this one to put a proposition into the normal form of the **agent** whose belief it is.
(grown-term-base base b)base raised to the nesting the extension bindings b bring in: the depth a term bound
to a variable contributes at a goal's top argument position, 1 + its own
(term-depth). A leaf match reads what is stored, so a deep value is a fact about the
KB and not about a rule growing a term.
`base` raised to the nesting the extension bindings `b` bring in: the depth a term bound to a variable contributes at a goal's top argument position, `1 +` its own (`term-depth`). A leaf match reads what is stored, so a deep value is a fact about the KB and not about a rule growing a term.
(holding-class kb)handle → class for a separation's denial (tax/monotonic-route-witness) and the
contrapositive fan (contrapositive-predicates): the live
JTMS defeat class of the handle, nil while it is OUT, and :monotonic for a believed
literal in the forced-monotonic set (decide/forced-literal?) whatever strength it
was written at. A separation is outside that set (docs/nmtms.md, "The
forced-monotonic set"), so the part edges a :default covering installs read
:default.
`handle → class` for a separation's denial (`tax/monotonic-route-witness`) and the contrapositive fan (`contrapositive-predicates`): the live JTMS defeat class of the handle, nil while it is OUT, and `:monotonic` for a believed literal in the forced-monotonic set (`decide/forced-literal?`) whatever strength it was written at. A separation is outside that set (docs/nmtms.md, "The forced-monotonic set"), so the part edges a `:default` `covering` installs read `:default`.
(holds-variable-application? kb l)Does literal l hold a variable-functor application outside a sentence position
(arg-app?): one a stored rule leaves as written?
Does literal `l` hold a variable-functor application outside a sentence position (`arg-app?`): one a stored rule leaves as written?
(initial-prove-stack kb goals context)(initial-prove-stack kb goals context est-override)The one-frame DFS stack prove starts from: the cost-ordered conjunction, no bindings,
an empty loop guard, depth 0, the answer variables and the query's term depth
(term-depth), the basis the term-growth cut starts from (grown-term-base). They
ride the stack because the stack is the continuation. prove-within seeds a bounded
run with it and hands the unfinished stack to resume. est-override costs the top
conjunction as in planned-antecedents.
The one-frame DFS stack `prove` starts from: the cost-ordered conjunction, no bindings, an empty loop guard, depth 0, the answer variables and the query's term depth (`term-depth`), the basis the term-growth cut starts from (`grown-term-base`). They ride the stack because the stack is the continuation. `prove-within` seeds a bounded run with it and hands the unfinished stack to `resume`. `est-override` costs the top conjunction as in `planned-antecedents`.
(insert-at args position v)args with v spliced in at 1-based position.
`args` with `v` spliced in at 1-based `position`.
(kb-sentex kb sentence context)Build a sentex canonicalized against this KB's taxonomy: a symmetric predicate's
arguments are sorted, so (siblingOf Bob Ann) and (siblingOf Ann Bob) become one
sentex, and the commutativity marks sort a declared set of positions at any arity
(tax/commuting-groups; store-marks, docs/canonicalization.md). Every construction
that stores or looks one up goes through this. The property read is global; while
*spelled-by* names this sentence's predicate and context, only the marks it lists
apply (spelling-planner). A rule's open applications are read through their
corresponding predicates first (respell-applications).
Build a sentex canonicalized against this KB's taxonomy: a symmetric predicate's arguments are sorted, so `(siblingOf Bob Ann)` and `(siblingOf Ann Bob)` become one sentex, and the commutativity marks sort a declared set of positions at any arity (`tax/commuting-groups`; `store-marks`, docs/canonicalization.md). Every construction that stores or looks one up goes through this. The property read is global; while `*spelled-by*` names this sentence's predicate and context, only the marks it lists apply (`spelling-planner`). A rule's open applications are read through their corresponding predicates first (`respell-applications`).
(lazy-mapcat f coll)mapcat that calls f one element at a time.
Not a stylistic preference — clojure.core/mapcat is (apply concat (map f coll)),
and map realizes a whole 32-element chunk at once when its source is chunked.
Over a handful of contexts or subtypes that means every branch is expanded (each
its own trie walk) before the first result is handed back, which is exactly the
cost the matching layers exist to avoid. Here the recursive call sits inside
lazy-seq, so a caller taking one solution expands one branch.
`mapcat` that calls `f` **one element at a time**. Not a stylistic preference — `clojure.core/mapcat` is `(apply concat (map f coll))`, and `map` realizes a whole 32-element chunk at once when its source is chunked. Over a handful of contexts or subtypes that means *every* branch is expanded (each its own trie walk) before the first result is handed back, which is exactly the cost the matching layers exist to avoid. Here the recursive call sits inside `lazy-seq`, so a caller taking one solution expands one branch.
(lead-literal? sentence)A literal matches-hierarchical answers from an argument lead — a plain positive
literal (hierarchical-literal?) with an indexable argument to read the argument
roots by. For such a literal the set-algebra path costs one slot read (or one scoped
read per spec, whichever is smaller — *lead-side*) where the nested fan-out costs a
trie walk per sub-predicate, and the two return the identical set. The forward join
asks this of a substituted antecedent (chain/join-antecedent) to route a bound type
test past the |specs| fan.
A literal `matches-hierarchical` answers from an **argument lead** — a plain positive literal (`hierarchical-literal?`) with an indexable argument to read the argument roots by. For such a literal the set-algebra path costs one slot read (or one scoped read per spec, whichever is smaller — `*lead-side*`) where the nested fan-out costs a trie walk per sub-predicate, and the two return the identical set. The forward join asks this of a substituted antecedent (`chain/join-antecedent`) to route a bound type test past the `|specs|` fan.
(mark-entries tax pred)The permuting marks the store sorts pred by, as {entry {handle context}}: the
symmetric entry [:prop :symmetric pred] and one [:commuting pred group] per
commuting group, each with its supporters. Empty for a predicate nothing permutes.
The permuting marks the store sorts `pred` by, as `{entry {handle context}}`: the
`symmetric` entry `[:prop :symmetric pred]` and one `[:commuting pred group]` per
commuting group, each with its supporters. Empty for a predicate nothing permutes.(match-pattern kb sentence)(match-pattern kb sentence context)(match-pattern kb sentence context vantage)Seq of [handle bindings] for stored sentexes matching sentence within context
(default the wildcard ?ctx). The functor fans out over its sub-predicate closure, so
(animal ?x) is met by (dog Muffet); a negation fans over contrapositive-predicates.
The fan is scoped to the genl edges visible from vantage: by default the literal
context, the global closure for a ?ctx match. The four-arity serves matches-visible*,
which stands at the view context throughout so the set-algebra twin agrees.
Seq of [handle bindings] for stored sentexes matching `sentence` within `context` (default the wildcard ?ctx). The functor fans out over its sub-predicate closure, so `(animal ?x)` is met by `(dog Muffet)`; a negation fans over `contrapositive-predicates`. The fan is scoped to the genl edges visible from `vantage`: by default the literal context, the global closure for a `?ctx` match. The four-arity serves `matches-visible*`, which stands at the view context throughout so the set-algebra twin agrees.
(match1 kb antecedent fact)(match1 kb antecedent fact context)Unify a single antecedent pattern against a ground fact sentence, honoring predicate
specificity: a fact whose functor is a spec of the antecedent's functor (via the genl
closure) satisfies it. Under a negation the fan reverses: (not (dog ?x)) is met by a
negative fact on a genl of dog, over the edges the reader holds at :monotonic
(contrapositive-predicates). With a context, the closure walks only edges that
context sees. The two-arity is unscoped, for callers that fix visibility elsewhere
(chain/fire-rules-for). See docs/inference.md, predicate specificity.
Unify a single antecedent pattern against a ground fact sentence, honoring predicate specificity: a fact whose functor is a spec of the antecedent's functor (via the genl closure) satisfies it. Under a negation the fan reverses: `(not (dog ?x))` is met by a negative fact on a genl of `dog`, over the edges the reader holds at `:monotonic` (`contrapositive-predicates`). With a `context`, the closure walks only edges that context sees. The two-arity is unscoped, for callers that fix visibility elsewhere (`chain/fire-rules-for`). See docs/inference.md, predicate specificity.
(matches-hierarchical kb sentence view-context)The set-algebra twin of matches-visible for a positive literal: the identical
[handle bindings stored] set, but reached by context-scoped index reads of the
sub-predicates' own nodes instead of the |specs| × |context-up| product of trie
walks. Falls back to matches-visible for any shape it does not handle, and for a
literal with a spec stored under another functor (folded-spec?) or read swapped
(swapped-sub-predicates).
The set-algebra twin of `matches-visible` for a positive literal: the identical `[handle bindings stored]` set, but reached by context-scoped index reads of the sub-predicates' own nodes instead of the `|specs| × |context-up|` product of trie walks. Falls back to `matches-visible` for any shape it does not handle, and for a literal with a spec stored under another functor (`folded-spec?`) or read swapped (`swapped-sub-predicates`).
(matches-visible kb sentence view-context)(matches-visible kb sentence view-context cached?)Type-aware matches of sentence visible from view-context. A variable context means
any context; a concrete one sees a fact iff the fact's context is in its genlCx
up-closure. A positive literal is answered by matches-hierarchical unless
*hierarchical-retrieval* is false. A sentex an except hides from view-context is
filtered out. Answers are cached per KB by the alpha-renamed literal and the change
clock (vaelii.impl.literal-cache), keyed also on every var that selects a path.
cached? false neither consults nor fills the cache. docs/inference.md, Resolution reads.
Type-aware matches of `sentence` visible from `view-context`. A variable context means any context; a concrete one sees a fact iff the fact's context is in its genlCx up-closure. A positive literal is answered by `matches-hierarchical` unless `*hierarchical-retrieval*` is false. A sentex an `except` hides from `view-context` is filtered out. Answers are cached per KB by the alpha-renamed literal and the change clock (`vaelii.impl.literal-cache`), keyed also on every var that selects a path. `cached?` false neither consults nor fills the cache. docs/inference.md, Resolution reads.
(matches-visible* kb sentence view-context)The reference nested fan-out: |context-up| × |specs| trie walks. matches-visible
dispatches to this or to matches-hierarchical; the latter also falls back here for
a shape it does not handle, so this must not re-dispatch (it is the fixed point that
breaks the cycle).
The reference nested fan-out: `|context-up| × |specs|` trie walks. `matches-visible` dispatches to this or to `matches-hierarchical`; the latter also falls back here for a shape it does not handle, so this must not re-dispatch (it is the fixed point that breaks the cycle).
(meet-order tax)sx/sentex's :meet-order read: for a function f some (meetFunctionOf f R)
declares, (fn [a b]) answering whether a lies below b by the registered
comparator of any such R (datetime/order-comparators), or nil when no declared
order has one. A stored (R a b) fact is never read, so the canonical form does not
move with belief.
`sx/sentex`'s `:meet-order` read: for a function `f` some `(meetFunctionOf f R)` declares, `(fn [a b])` answering whether `a` lies below `b` by the registered comparator of any such `R` (`datetime/order-comparators`), or nil when no declared order has one. A stored `(R a b)` fact is never read, so the canonical form does not move with belief.
(minted-expression kb k)The expression the believed CxUniverse natFormula rows map the reified object
constant k to, the content-least where several do, or nil.
The expression the believed CxUniverse `natFormula` rows map the reified object constant `k` to, the content-least where several do, or nil.
(names-no-match? kb l)Does literal l hold sx/no-match at a term position, at any depth: an argument, or
inside an application at one? An argument at a sentence-position? is a literal of
its own, read when its prover reads it.
Does literal `l` hold `sx/no-match` at a term position, at any depth: an argument, or inside an application at one? An argument at a `sentence-position?` is a literal of its own, read when its prover reads it.
(names-variable-application? modal form)Does form hold a variable-functor application, (?fn AppleTree), at any nesting
outside a mention (applications-in)?
Does `form` hold a variable-functor application, `(?fn AppleTree)`, at any nesting outside a mention (`applications-in`)?
Predicates whose expression argument is a verbatim NAT payload, neither reified nor type-checked as a term.
Predicates whose expression argument is a verbatim NAT payload, neither reified nor type-checked as a term.
(normal-form kb term visible?)term (a sentence or a term) in the equality normal form the KB stores and asks in:
representative-term, then argument terms reduced by the schematic equations the same
reader sees (rewrite/normalize-sentence). Migration and query both go through here.
visible? is a built supporter predicate (visible-supporter-fn), nil for the unscoped
read; kb/rewrite-term takes a context instead.
`term` (a sentence or a term) in the equality **normal form** the KB stores and asks in: `representative-term`, then argument terms reduced by the schematic equations the same reader sees (`rewrite/normalize-sentence`). Migration and query both go through here. `visible?` is a built supporter predicate (`visible-supporter-fn`), nil for the unscoped read; `kb/rewrite-term` takes a context instead.
(opaque-fn tax)sx/sentex's :opaque? read: the functors whose applications keep their arguments as
written below the literal. A NAT-quoting predicate's expression is a verbatim payload,
and a reifiable function's ground application is named by the constant its written
expression hashes to (docs/nat.md), so neither is sorted. The reifiable mark is read
unscoped: the walk decides the stored key, which every reader shares.
`sx/sentex`'s `:opaque?` read: the functors whose applications keep their arguments as written below the literal. A NAT-quoting predicate's expression is a verbatim payload, and a reifiable function's ground application is named by the constant its written expression hashes to (docs/nat.md), so neither is sorted. The reifiable mark is read unscoped: the walk decides the stored key, which every reader shares.
(open-applications modal reifiable? form)The open applications of a function reifiable? accepts in form, at any nesting,
outermost first, the propositions of the modal_predicates modal unread
(applications-in).
The open applications of a function `reifiable?` accepts in `form`, at any nesting, outermost first, the propositions of the `modal_predicate`s `modal` unread (`applications-in`).
(permuted-functor sentence)The predicate whose permuting marks decide how sentence is spelled when stored — its
functor, under a not — or nil.
The predicate whose permuting marks decide how `sentence` is spelled when stored — its functor, under a `not` — or nil.
(planned-antecedents kb antecedents consequent context bindings)(planned-antecedents kb antecedents consequent context bindings est-override)A rule's antecedents in the order they should be solved, given the bindings the head
match produced. Stored order is canonical (sentex/canonicalize-rule) and bears no
relation to cost. Reordering changes cost, never the answer set;
vaelii.impl.plan fixes the evaluables and the recursive literal in place. Antecedents
are substituted before planning so the planner costs them against real values.
est-override is passed through to plan/order (provers/est-goal).
A rule's antecedents in the order they should be solved, given the bindings the head match produced. Stored order is canonical (`sentex/canonicalize-rule`) and bears no relation to cost. Reordering changes cost, never the answer set; `vaelii.impl.plan` fixes the evaluables and the recursive literal in place. Antecedents are substituted before planning so the planner costs them against real values. `est-override` is passed through to `plan/order` (`provers/est-goal`).
(probe-spelling kb sentence)Literal sentence with every ground compound below it in the order the store holds
it (sx/sort-compounds under store-marks), the spelling a match probes the store
with. sentence itself when no argument is a compound.
Literal `sentence` with every ground compound below it in the order the store holds it (`sx/sort-compounds` under `store-marks`), the spelling a match probes the store with. `sentence` itself when no argument is a compound.
(project-answer bindings answer-vars)A finished derivation's bindings, resolved and cut down to the variables the query
asked about. nil answer-vars projects nothing. The projection is by name, so a
query that writes ?var0 gets ?var0. See docs/inference.md, Resolution reads.
A finished derivation's bindings, resolved and cut down to the variables the query asked about. `nil` `answer-vars` projects nothing. The projection is by name, so a query that writes `?var0` gets `?var0`. See docs/inference.md, Resolution reads.
(prove kb rules-fn goals context)(prove kb rules-fn goals context bounds)A depth-first backward chainer over an explicit goal stack. Returns a vector of
resolved solution binding maps proving the conjunction goals in context. A per-path
:seen set of goal-keys and the term-growth ceiling (default-max-term-growth) make
every search terminate on the data. Prefer right-recursive rules: a left-recursive rule is
pruned after its first expansion. rules-fn maps a subgoal to candidate rules. The 5-arg arity takes prove-from's bounds (the
keys of prove-seq plus :max-results), e.g. a registry leaf
{:leaf-solver provers/solve-goal :est-override (provers/registry-est-override kb ctx)};
the 4-arg keeps the stored-fact leaf.
A depth-first backward chainer over an explicit goal stack. Returns a vector of
resolved solution binding maps proving the conjunction `goals` in `context`. A per-path
`:seen` set of goal-keys and the term-growth ceiling (`default-max-term-growth`) make
every search terminate on the data. Prefer right-recursive rules: a left-recursive rule is
pruned after its first expansion. `rules-fn` maps a subgoal to candidate rules. The 5-arg arity takes `prove-from`'s `bounds` (the
keys of `prove-seq` plus `:max-results`), e.g. a registry leaf
`{:leaf-solver provers/solve-goal :est-override (provers/registry-est-override kb ctx)}`;
the 4-arg keeps the stored-fact leaf.(prove-from kb
rules-fn
context
{:keys [deadline max-results max-depth max-term-growth leaf-solver
est-override]}
stack
solutions)The resumable core of prove: run the DFS from an explicit stack (and the
solutions so far) under bounds, a map of optional caps:
:deadline System/nanoTime instant :max-results :max-depth :max-term-growth
:leaf-solver (see leaf-solutions) :est-override (see planned-antecedents)
Returns {:solutions <vector> :status <kw> :stack <frames>}; :status is :complete
(:stack empty), else :timeout or :capped with a non-empty :stack to resume from.
A leaf the deadline stops inside goes back on the stack marked :unbounded-leaf?.
With bounds nil it runs to completion.
The resumable core of `prove`: run the DFS from an explicit `stack` (and the
`solutions` so far) under `bounds`, a map of optional caps:
:deadline `System/nanoTime` instant :max-results :max-depth :max-term-growth
:leaf-solver (see `leaf-solutions`) :est-override (see `planned-antecedents`)
Returns `{:solutions <vector> :status <kw> :stack <frames>}`; `:status` is `:complete`
(`:stack` empty), else `:timeout` or `:capped` with a non-empty `:stack` to resume from.
A leaf the deadline stops inside goes back on the stack marked `:unbounded-leaf?`.
With `bounds` nil it runs to completion.(prove-seq kb rules-fn goals context)(prove-seq kb rules-fn goals context bounds)The same search as prove, lazily: a seq of solution binding maps costing one solution
per pull. Runs prove-from capped at one result and resumes from the :stack it left;
:capped is the only status that continues. bounds takes prove-from's keys except
:max-results. Each segment opens its own search scope, which is sound because a query
mutates no belief. See docs/inference.md, Resolution reads.
The same search as `prove`, lazily: a seq of solution binding maps costing one solution per pull. Runs `prove-from` capped at one result and resumes from the `:stack` it left; `:capped` is the only status that continues. `bounds` takes `prove-from`'s keys except `:max-results`. Each segment opens its own search scope, which is sound because a query mutates no belief. See docs/inference.md, Resolution reads.
(raw-match kb sentence context)Match a literal in one literal context — no genlCx inheritance, no subtype
fan-out — over every argument arrangement its predicate licences (raw-match-with),
probing the stored index with match-one. Yields [handle bindings stored-sentex].
Match a literal in one **literal** context — no genlCx inheritance, no subtype fan-out — over every argument arrangement its predicate licences (`raw-match-with`), probing the stored index with `match-one`. Yields `[handle bindings stored-sentex]`.
(raw-match-with kb probe sentence)Match a literal by probe ((probe form) → a seq of [handle bindings …], one literal
context) over every argument arrangement the predicate licences: the mirror for a
symmetric predicate, the other arrangements of the commuting component for a commutative
one. This makes lookup order-insensitive, including a fact asserted before its
symmetric declaration. Deduped by handle and bindings: (sibOf ?a ?b) over a stored
(sibOf Rex Tib) binds both ways round, two answers about one handle. Lazy through the
fan. raw-match calls it with match-one, the rete alpha matcher with its memory
probe, so the paths cannot fan differently. The symmetric mark is read unscoped.
Match a literal by `probe` (`(probe form)` → a seq of `[handle bindings …]`, one literal context) over every argument arrangement the predicate licences: the mirror for a symmetric predicate, the other arrangements of the commuting component for a commutative one. This makes lookup order-insensitive, including a fact asserted before its `symmetric` declaration. Deduped by handle and bindings: `(sibOf ?a ?b)` over a stored `(sibOf Rex Tib)` binds both ways round, two answers about one handle. Lazy through the fan. `raw-match` calls it with `match-one`, the rete alpha matcher with its memory probe, so the paths cannot fan differently. The `symmetric` mark is read unscoped.
(reader-spelled-by kb sentence reader)The *spelled-by* binding that spells sentence as reader reads it, or nil when the
store's own spelling is the reader's.
The `*spelled-by*` binding that spells `sentence` as `reader` reads it, or nil when the store's own spelling is the reader's.
(reference-positions kb pred)A fn from a position of pred to whether its argument names a stored sentex by its
content, or nil when no position does: each position a believed quotedArg or
quotedArgAndRest declaration types sentex_handle_term, and, when pred is a
target_following_predicate, each an arg or argN declaration types sentence.
except's target is one whatever the KB declares. Each declaration kind is read only
for a pred its taxonomy mark names. Read unscoped, as formula-position? reads. See
docs/canonicalization.md, "A reference to a stored sentex".
A fn from a position of `pred` to whether its argument names a stored sentex by its content, or nil when no position does: each position a believed `quotedArg` or `quotedArgAndRest` declaration types `sentex_handle_term`, and, when `pred` is a `target_following_predicate`, each an `arg` or `argN` declaration types `sentence`. `except`'s target is one whatever the KB declares. Each declaration kind is read only for a `pred` its taxonomy mark names. Read unscoped, as `formula-position?` reads. See docs/canonicalization.md, "A reference to a stored sentex".
(reference-term? a)Is a an application of a function name (nm/individual?), other than a quoting one?
Its arguments are read at the function's own reference-positions: the text writer and
assert-entry/resolve-references descend into one at any argument position.
Is `a` an application of a function name (`nm/individual?`), other than a quoting one? Its arguments are read at the function's own `reference-positions`: the text writer and `assert-entry/resolve-references` descend into one at any argument position.
(representative-in kb visible? term)term's equality-class representative as visible? sees the merges. The global
representative, one map lookup, when nothing has merged term, when visible? is nil,
or when the reader sees the whole class (tax/class-fully-visible?); tax/scoped-class
otherwise.
`term`'s equality-class representative as `visible?` sees the merges. The global representative, one map lookup, when nothing has merged `term`, when `visible?` is nil, or when the reader sees the whole class (`tax/class-fully-visible?`); `tax/scoped-class` otherwise.
(representative-term kb visible? term)term with every non-variable symbol replaced by its class representative
(representative-in) at any depth, so (QuantityFn 5 Kilogram) and (QuantityFn 5 Kg)
meet under (sameAs Kilogram Kg). A mention position (a quoting function's arguments
(sx/quoting-functors), a modal_predicate's proposition) is rewritten by rewriteOf
spelling only (docs/belief.md, Opacity). The marks are read once, unscoped
(tax/mention-marks).
`term` with every non-variable symbol replaced by its class representative (`representative-in`) at any depth, so `(QuantityFn 5 Kilogram)` and `(QuantityFn 5 Kg)` meet under `(sameAs Kilogram Kg)`. A mention position (a quoting function's arguments (`sx/quoting-functors`), a `modal_predicate`'s proposition) is rewritten by `rewriteOf` spelling only (docs/belief.md, Opacity). The marks are read once, unscoped (`tax/mention-marks`).
(resolve-bindings bindings)Fully dereference every variable in a binding map so chained variables (?g -> ?x -> Tom) collapse to their ground value.
Fully dereference every variable in a binding map so chained variables (?g -> ?x -> Tom) collapse to their ground value.
(respell-applications kb sentence context)Rule sentence as kb-sentex stores it in context: the first of
rule-respellings, or sentence unchanged when that is nil.
Rule `sentence` as `kb-sentex` stores it in `context`: the first of `rule-respellings`, or `sentence` unchanged when that is nil.
(retired-for? kb visible merged? sentence)Does sentence name a term the reader has retired, so that it is not in that reader's
normal form? visible is the caller's delay over the supporter memo and merged?
its partition snapshot (tax/merged-term-pred), so an unmerged sentence answers false on
one merged? walk and never forces visible. A positive equation is never retired
(equation?). A sentence with a mention position, an equality relation's arguments
included, is confirmed against the mention-aware walk before it is called retired.
Public for qcn-kb/refuted-pairs, whose [handle a b] rows without-retired cannot
take.
Does `sentence` name a term the reader has retired, so that it is not in that reader's normal form? `visible` is the caller's **delay** over the supporter memo and `merged?` its partition snapshot (`tax/merged-term-pred`), so an unmerged sentence answers false on one `merged?` walk and never forces `visible`. A positive equation is never retired (`equation?`). A sentence with a mention position, an equality relation's arguments included, is confirmed against the mention-aware walk before it is called retired. Public for `qcn-kb/refuted-pairs`, whose `[handle a b]` rows `without-retired` cannot take.
(rewrite-rules-in kb visible?)The believed oriented rewrite rules the reader visible? sees (nil: every one). Every
normal form reads its rules here: normal-form, provers/EqualityProver and an
exception's goal rewrite.
The believed oriented rewrite rules the reader `visible?` sees (nil: every one). Every normal form reads its rules here: `normal-form`, `provers/EqualityProver` and an exception's goal rewrite.
(rule-believed? kb handle)May the rule at handle chain: is it believed? A stored rule is not a believed one,
and the rule index posts on storage, so both chainers filter through this (a derived
rule, docs/generators.md, leaves only when its licence does). A sentex the TMS holds no
node for is available, not disbelieved; for a rule that arm is defence, since
core/assert-inert refuses a rule no entry point premised, and a wrong answer would
silently stop a rule firing. An inert rule is believed
and kept from firing by its :engines alone (rules/forward-sentex? /
backward-sentex?, docs/inference.md).
May the rule at `handle` chain: is it believed? A stored rule is not a believed one, and the rule index posts on storage, so both chainers filter through this (a derived rule, docs/generators.md, leaves only when its licence does). A sentex the TMS holds no node for is available, not disbelieved; for a rule that arm is defence, since `core/assert-inert` refuses a rule no entry point premised, and a wrong answer would silently stop a rule firing. An inert rule is believed and kept from firing by its `:engines` alone (`rules/forward-sentex?` / `backward-sentex?`, docs/inference.md).
(rule-form? l)Is l a rule, its wrappers peeled: a generator's consequent, whose applications the
rule it generates reads when it is stored?
Is `l` a rule, its wrappers peeled: a generator's consequent, whose applications the rule it generates reads when it is stored?
(rule-respellings kb sentence context)Every spelling of rule sentence its antecedents' open reifiable_function
applications read through the believed correspondences, as [[spelling handle-sets] …]
(respell-rule; the consequent stays as written). The first takes each function's
content-least correspondence and is the one kb-sentex stores;
chain/sync-rule-respellings! stores the rest. Nil when sentence is no rule or no
antecedent has a reading (docs/nat.md, The corresponding predicate).
Every spelling of rule `sentence` its antecedents' open `reifiable_function` applications read through the believed correspondences, as `[[spelling handle-sets] …]` (`respell-rule`; the consequent stays as written). The first takes each function's content-least correspondence and is the one `kb-sentex` stores; `chain/sync-rule-respellings!` stores the rest. Nil when `sentence` is no rule or no antecedent has a reading (docs/nat.md, The corresponding predicate).
(rule-visible-from? kb context rule-ctx)May a rule stored in rule-ctx answer a goal asked from context? A context reasons
with the rules its genlCx ancestor set holds and no others, so the backward chainers
agree with forward placement. An open ?ctx (or nil) is the unscoped path.
May a rule stored in `rule-ctx` answer a goal asked from `context`? A context reasons with the rules its `genlCx` ancestor set holds and no others, so the backward chainers agree with forward placement. An open `?ctx` (or nil) is the unscoped path.
(same-class-in? kb a b context)(same-class-in? kb a b context admit?)Do a and b denote one thing as context sees the merges? The scoped twin of
tax/same-class?, through representative-in; a nil or ?var context gives the global
answer. admit? also refuses a supporter it does not hold for: special/covered-merges
reads only the merges stored above a copy's context.
Do `a` and `b` denote one thing as `context` sees the merges? The scoped twin of `tax/same-class?`, through `representative-in`; a nil or `?var` context gives the global answer. `admit?` also refuses a supporter it does not hold for: `special/covered-merges` reads only the merges stored above a copy's context.
(separation-denials kb t x context)The witnesses of (not (t x)) a reader at context reads off a separation, in content
order: one per believed, visible, unexcepted membership (s x) (type-memberships) and
per route a declaration separates s from t through (tax/separation-routes) that
meets tax/monotonic-route-witness. Each witness is {:membership h :sentence (s x) :context c :route {:keys :pair :supports :edges}}. Empty when no separation reaches
t (tax/separable?). provers/DisjointnessNegationProver and checks/cover-problem
read it (docs/taxonomy.md, A separation answers a denial).
The witnesses of `(not (t x))` a reader at `context` reads off a separation, in content
order: one per believed, visible, unexcepted membership `(s x)` (`type-memberships`) and
per route a declaration separates `s` from `t` through (`tax/separation-routes`) that
meets `tax/monotonic-route-witness`. Each witness is `{:membership h :sentence (s x)
:context c :route {:keys :pair :supports :edges}}`. Empty when no separation reaches
`t` (`tax/separable?`). `provers/DisjointnessNegationProver` and `checks/cover-problem`
read it (docs/taxonomy.md, A separation answers a denial).(separation-denied? kb t x context)Does a reader at context read (not (t x)) off a separation: is
separation-denials non-empty? Reads the witnesses lazily and stops at the first,
for a caller that asks whether the denial holds and names no member
(provers/DisjointnessNegationProver).
Does a reader at `context` read `(not (t x))` off a separation: is `separation-denials` non-empty? Reads the witnesses lazily and stops at the first, for a caller that asks whether the denial holds and names no member (`provers/DisjointnessNegationProver`).
(solve-deferred kb g context)Extension binding-maps for a deferred antecedent g (already substituted, so its inputs
are ground), computed by the prover registry through wiring/solve-goal. Nothing when
the literal is inapplicable (unbound inputs, a false test): the branch is pruned, the
evaluable contract vaelii.impl.plan documents. See docs/naf.md.
Extension binding-maps for a deferred antecedent `g` (already substituted, so its inputs are ground), computed by the prover registry through `wiring/solve-goal`. Nothing when the literal is inapplicable (unbound inputs, a false test): the branch is pruned, the evaluable contract `vaelii.impl.plan` documents. See docs/naf.md.
(spelling-planner kb)(fn [sentence context]) answering {spelling entries}: each spelling the readers of
sentence, written in context, read it in, with the marks that reader believes, or
nil when every reader believes every mark that sorts it (uniform-marks?) and so reads
the store's own spelling. The fn holds for its own lifetime
one memo of each predicate's marks and whether they are uniform, and one of each
[predicate context]'s readers: a walk over a predicate's rows reads both once.
`(fn [sentence context])` answering `{spelling entries}`: each spelling the readers of
`sentence`, written in `context`, read it in, with the marks that reader believes, or
nil when every reader believes every mark that sorts it (`uniform-marks?`) and so reads
the store's own spelling. The fn holds for its own lifetime
one memo of each predicate's marks and whether they are uniform, and one of each
`[predicate context]`'s readers: a walk over a predicate's rows reads both once.(spelling-readers kb context handles)The readers whose spellings of a fact stated in context can differ, given the
supporters handles of its predicate's marks: context and the contexts where it meets
the contexts that state a hiding defeat or except (hider-contexts,
tax/meet-closure), kept where they see context. A reader below context sees one
of these sets of hiders, so it reads as one of them does.
The readers whose spellings of a fact stated in `context` can differ, given the supporters `handles` of its predicate's marks: `context` and the contexts where it meets the contexts that state a hiding `defeat` or `except` (`hider-contexts`, `tax/meet-closure`), kept where they see `context`. A reader below `context` sees one of these sets of hiders, so it reads as one of them does.
(store-marks tax)sx/sentex's canonicalization reads under every permuting mark and term mark the store
spells by. Read unscoped: the fold decides the stored key, which every reader shares.
`sx/sentex`'s canonicalization reads under every permuting mark and term mark the store spells by. Read unscoped: the fold decides the stored key, which every reader shares.
(sub-predicates kb f context)The sub-predicate (genl spec) closure the matching fan-out walks for functor f, with
the predicates an even number of genlInverse edges reach (tax/signed-closure),
from the vantage context — the global closure when the vantage is a variable or
nil. The single definition every matcher shares (match-pattern,
matches-hierarchical, the rete alpha matcher), so the fan cannot drift between
them: a genl edge invisible from the vantage does not connect a sub-predicate's
facts to the pattern, exactly as it does not appear in the closure reads.
The sub-predicate (genl spec) closure the matching fan-out walks for functor `f`, with the predicates an even number of `genlInverse` edges reach (`tax/signed-closure`), from the vantage `context` — the global closure when the vantage is a variable or nil. The **single definition every matcher shares** (`match-pattern`, `matches-hierarchical`, the rete alpha matcher), so the fan cannot drift between them: a genl edge invisible from the vantage does not connect a sub-predicate's facts to the pattern, exactly as it does not appear in the closure reads.
(substitute pattern bindings)Replace bound variables in a pattern with their values (recursively). A dotted
rest pattern (head ... . ?rest) is spliced: (?pred . ?args) with ?args=(Tom Bob)
becomes (parentOf Tom Bob). A (Quote X) form comes back whole, since unify never
binds inside it. Eager, and a PersistentList: docs/inference.md, Resolution reads.
Replace bound variables in a pattern with their values (recursively). A dotted rest pattern `(head ... . ?rest)` is spliced: `(?pred . ?args)` with `?args=(Tom Bob)` becomes `(parentOf Tom Bob)`. A `(Quote X)` form comes back whole, since `unify` never binds inside it. Eager, and a `PersistentList`: docs/inference.md, Resolution reads.
(subsuming-unify kb goal consequent)(subsuming-unify kb goal consequent bindings)(subsuming-unify kb goal consequent bindings context)Unify a query goal against a rule's consequent, honoring predicate specificity: a
consequent whose functor is a spec of the goal's functor answers the goal, binding the
goal variable to the more specific instance. The backward dual of match1; a negated
goal fans as in match1 and falls through to plain unify against a positive
consequent. With a context the genl closure is scoped to the edges it sees, as
match1 does; the arities without one are unscoped.
Unify a query `goal` against a rule's `consequent`, honoring predicate specificity: a consequent whose functor is a spec of the goal's functor answers the goal, binding the goal variable to the more specific instance. The backward dual of `match1`; a negated goal fans as in `match1` and falls through to plain `unify` against a positive consequent. With a `context` the genl closure is scoped to the edges it sees, as `match1` does; the arities without one are unscoped.
(super-predicates kb f context)The genl closure of f from the vantage context: sub-predicates mirrored,
through every visible edge whatever its strength. A negative pattern fans over the
part of it the reader holds at :monotonic, contrapositive-predicates.
The **genl** closure of `f` from the vantage `context`: `sub-predicates` mirrored, through every visible edge whatever its strength. A negative pattern fans over the part of it the reader holds at `:monotonic`, `contrapositive-predicates`.
(supporter-believed? kb handle context)(supporter-believed? kb handle context defeats?)Is stored supporter handle believed from context: IN in the network, and not hidden
there by a believed except or a placed defeat in force at context, or by resting
only on a hidden handle (exc/excepted?, the read walk)? defeats? false reads the
excepts alone (exc/excepted-in-network?). The taxonomy's visible? callback
(kb/attach-visibility!): it decides whether a closure walk may cross an edge. Its
ancestor-set reads go through tax/context-up-global, so asking it inside a scoped walk
never re-enters the filtered closure. A context that disbelieves a genl edge stops
reaching over it. See docs/taxonomy.md.
Is stored supporter `handle` believed from `context`: IN in the network, and not hidden there by a believed `except` or a placed `defeat` in force at `context`, or by resting only on a hidden handle (`exc/excepted?`, the read walk)? `defeats?` false reads the excepts alone (`exc/excepted-in-network?`). The taxonomy's `visible?` callback (`kb/attach-visibility!`): it decides whether a closure walk may cross an edge. Its ancestor-set reads go through `tax/context-up-global`, so asking it inside a scoped walk never re-enters the filtered closure. A context that disbelieves a `genl` edge stops reaching over it. See docs/taxonomy.md.
(supporter-visible? kb handle context)(supporter-visible? kb handle context defeats?)Is stored supporter handle believed, inherited, and not excepted from context?
defeats? false leaves the placed defeats unread (supporter-believed?), as a
firing's placement reads them.
Is stored supporter `handle` believed, inherited, and not excepted from `context`? `defeats?` false leaves the placed defeats unread (`supporter-believed?`), as a firing's placement reads them.
(swapped-sub-predicates kb f context)The predicates sub-predicates' fan reads with arguments 1 and 2 swapped: those
below f across an odd number of genlInverse edges (tax/signed-closure). Empty —
one map read — on a KB declaring no genlInverse.
The predicates `sub-predicates`' fan reads **with arguments 1 and 2 swapped**: those below `f` across an odd number of `genlInverse` edges (`tax/signed-closure`). Empty — one map read — on a KB declaring no `genlInverse`.
(swapped-super-predicates kb f context)swapped-sub-predicates mirrored: the predicates above f across an odd number of
genlInverse edges, which a negated pattern on f reads swapped.
`swapped-sub-predicates` mirrored: the predicates above `f` across an odd number of `genlInverse` edges, which a negated pattern on `f` reads swapped.
(term-depth form)How deeply form's arguments nest compound terms: 0 for a flat literal (p A), 1
for (p (SuccFn A)), 2 for (p (SuccFn (SuccFn A))). The second half of the loop
guard (default-max-term-growth): a goal key keeps its ground arguments, so a rule
that wraps a function around a head variable mints a fresh key per expansion and the
key alone never repeats. One pass over the arguments; a flat goal reads each once.
How deeply `form`'s arguments nest compound terms: 0 for a flat literal `(p A)`, 1 for `(p (SuccFn A))`, 2 for `(p (SuccFn (SuccFn A)))`. The second half of the loop guard (`default-max-term-growth`): a goal key keeps its ground arguments, so a rule that wraps a function around a head variable mints a fresh key per expansion and the key alone never repeats. One pass over the arguments; a flat goal reads each once.
(type-memberships kb x)(type-memberships kb x context)The membership sentexes (T x) of term x that kb/types-of reads its types off, as
records: believed, asserted in a context context sees, and not hidden from it by an
except (default: any context). The same three filters matches-visible applies. A
negative membership is excluded by the argument test: a (not (T x)) sentex has not
as its functor.
The membership sentexes `(T x)` of term `x` that `kb/types-of` reads its types off, as records: believed, asserted in a context `context` sees, and not hidden from it by an `except` (default: any context). The same three filters `matches-visible` applies. A negative membership is excluded by the argument test: a `(not (T x))` sentex has `not` as its functor.
(uniform-marks? kb entries)Does every reader believe every mark in entries (mark-entries): each has a
supporter held-everywhere?? The four permuting marks are read from every context
(docs/contexts.md, "A context outside the topology"), so only a defeat or an except
makes two readers read one fact differently.
Does every reader believe every mark in `entries` (`mark-entries`): each has a supporter `held-everywhere?`? The four permuting marks are read from every context (docs/contexts.md, "A context outside the topology"), so only a defeat or an except makes two readers read one fact differently.
(unify x y)(unify x y bindings)Unify terms x and y under bindings, returning an extended binding map or nil.
A (Quote X) form (sx/quote-form?) is a constant: it unifies with a variable or with
an equal form, and a variable inside it binds nothing. Supports dotted rest patterns:
a sublist (. ?rest) binds ?rest to the whole remaining sequence, so
(?pred . ?args) unifies with (parentOf Tom Bob) giving ?pred=parentOf,
?args=(Tom Bob).
Unify terms x and y under `bindings`, returning an extended binding map or nil. A `(Quote X)` form (`sx/quote-form?`) is a constant: it unifies with a variable or with an equal form, and a variable inside it binds nothing. Supports dotted rest patterns: a sublist `(. ?rest)` binds `?rest` to the whole remaining sequence, so `(?pred . ?args)` unifies with `(parentOf Tom Bob)` giving `?pred=parentOf`, `?args=(Tom Bob)`.
(unify-args xs ys)(unify-args xs ys bindings)Unify two argument sequences element by element, each element as a term (unify).
The entry point for a caller holding argument lists, such as (rest literal), rather
than terms: the list (Quote X) is a quoted form as a term and the symbol Quote
followed by X as an argument list.
Unify two argument sequences element by element, each element as a term (`unify`). The entry point for a caller holding argument lists, such as `(rest literal)`, rather than terms: the list `(Quote X)` is a quoted form as a term and the symbol `Quote` followed by X as an argument list.
(visible-supporter-fn kb context)handle -> boolean, memoized: is the sentex handle believed, inherited by
context, and not hidden there by a visibility exception? nil when context is nil
or a ?var, the unscoped read, which every caller reads as no filter. The predicate
a context-scoped equality read takes: the partition records its supporters as handles.
`handle -> boolean`, memoized: is the sentex `handle` believed, inherited by `context`, and not hidden there by a visibility exception? nil when `context` is nil or a `?var`, the unscoped read, which every caller reads as *no filter*. The predicate a context-scoped equality read takes: the partition records its supporters as handles.
(without-hidden-matches kb view-context sentence matches)matches of sentence less what view-context cannot read: the handles an except
hides (exc/without-excepted), the spellings an equality merge retired
(without-retired) and the spellings its marks do not license
(without-unbelieved-spellings), in that order.
`matches` of `sentence` less what `view-context` cannot read: the handles an `except` hides (`exc/without-excepted`), the spellings an equality merge retired (`without-retired`) and the spellings its marks do not license (`without-unbelieved-spellings`), in that order.
(without-retired kb view-context matches)Drop the matches whose stored spelling view-context has retired: the
reader-scoped half of supersession (docs/equality.md, "The reader is not the fact's own
context"). Filters nothing when the closure is empty, one deref, or when
view-context is nil or a variable, the unscoped read.
Drop the `matches` whose stored spelling `view-context` has **retired**: the reader-scoped half of supersession (docs/equality.md, "The reader is not the fact's own context"). Filters nothing when the closure is empty, one deref, or when `view-context` is nil or a variable, the unscoped read.
(without-unbelieved-spellings kb view-context goal matches)Drop the matches of goal whose spelling view-context does not read: a row stored as
written that the marks the reader believes sort otherwise, a row read in an argument
order those marks do not license, and a row spelled by a reifiable_function mark the
reader takes the other way (reified-reading). A match of a permuting predicate stays
when the marks the reader believes spell the fact it reads to the stored row. This runs
only when a permuting or reifiable mark is stored at all, and per predicate only when
some reader does not believe a mark (uniform-marks?); a variable or nil view-context
filters nothing.
Drop the matches of `goal` whose spelling `view-context` does not read: a row stored as written that the marks the reader believes sort otherwise, a row read in an argument order those marks do not license, and a row spelled by a `reifiable_function` mark the reader takes the other way (`reified-reading`). A match of a permuting predicate stays when the marks the reader believes spell the fact it reads to the stored row. This runs only when a permuting or reifiable mark is stored at all, and per predicate only when some reader does not believe a mark (`uniform-marks?`); a variable or nil `view-context` filters nothing.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |