vaelii.impl.sentex — com.vaelii/vaelii 0.24.0

The sentex — Vaelii's unit of knowledge: a sentence paired with the context it holds in (sentence + context = sentex).

A sentence is a logical form written as a Clojure s-expression, e.g. (parentOf Tom Bob). Ground (all constants) or a pattern with variables like ?x. A context names the situation / assumption frame it is asserted within.

The structural connectives not, implies, and and are canonicalized into the record rather than left as data: a negation is at most one (not S) at the head of the sentence (double negation eliminated), read back by negative?, and a rule carries a decomposed antecedent (vector of patterns) and consequent. So the connectives never reach the inverted term index (their heads are stripped, even nested inside a rule — see content-forms), and the positional trie key drops the implies / and rule frame; a negative literal keeps its not there, so a rule concluding (flies ?x) and one concluding (not (flies ?x)) get distinct keys.

Beyond the connectives, a sentence is put into a canonical form so that logically identical knowledge is stored once:

• canonical variables — a rule's variables are renamed ?var0, ?var1, … by first occurrence in canonical order, and :varmap maps them back to what the author wrote ({?var0 ?x}), so display can restore the original names.
• canonical literal order — a rule's antecedents are sorted by a structural order (polarity, arity, ground arity, variable degree, shape), falling back to a lexical comparison of constants only as the last resort. Variables compare by their canonical index, never by name.
• symmetric arguments sorted — (siblingOf Bob Ann) and (siblingOf Ann Bob) canonicalize to one sentex when siblingOf is declared symmetric.
• comparison siblings folded — greaterThan is stored as lessThan with its arguments reversed, so only the < direction is ever stored.
• comparison chains collapsed — lessThan is variable-arity, and chained comparisons in a rule merge: (lessThan ?a ?b) + (lessThan ?b ?c) becomes the single literal (lessThan ?a ?b ?c). different gets neither fold: it is not transitive, so a merged chain would claim more than was asserted.

An exceptWhen exception does not touch the rule record: it is stored separately as a meta-sentex naming the rule by handle (see the RuleSentex field notes below).

A literal's :sentence holds its canonical, readable form for display and matching. A rule holds no sentence: its antecedent and consequent are the one representation it keeps, and sentence-of builds the implies form from them.

A sentex is one of two records — LiteralSentex (a literal: a signed predicate application — a fact or its negation, a metadata declaration, a query pattern) or RuleSentex (an implication) — so a literal sentex does not carry the rule-only slots (there are 100M+ of them), and each still round-trips through nippy with its type intact.

*min-indexed-depth* clj

How deep inside a content literal a ground compound must sit to earn its own inverted-index key — 0 being the literal itself, 1 a subterm of it, and so on.

The default 1 drops each literal's own whole-compound key. That key is what makes the token dictionary fact-scaled instead of vocabulary-scaled: a fact's body is a subterm of itself, so it mints one key holding exactly one handle, per record. Over a 12,070-record corpus of 511 names, 12,054 of the 12,565 distinct tokens are those keys; in the shipped starter, 1,724 of 2,077 — against 4 compounds that are genuinely nested. At the floor and deeper the nesting is what a probe is for: (sentexHandle H) inside an exceptWhen meta, the sentence inside an (ist Ctx S).

2 and up also drop that wrapped sentence — the corpus where the nesting is itself per-record — at the cost of the read ist exists to serve, so the corpus decides. 0 keys every compound, the literal included.

It is read at write time, so moving it over a populated store changes what the next sentex is indexed under and leaves the keys already written where they are: a posting outside the new bound is stale rather than wrong (every read fetches the record, and a dead handle drops out there), and reindex is what applies a new setting wholesale. The token ids themselves are content-keyed and durable — a store keeps the ones it no longer mints, which is not a migration.

*symbol-pool-limit* clj

The most entries the pool holds across its two generations; each generation holds at most half. Sized well above the shipped ontology plus the whole of OpenCyc (~188k constants), so a KB of that vocabulary never rotates a generation and keeps every name shared. A store whose vocabulary is larger, or a minter running per fact, rotates the generations: a name mentioned since the previous rotation stays pooled, and a name not mentioned for two rotations leaves. Dynamic so a test exercises the rotation by binding a small limit.

aggregate-body clj

(aggregate-body form)

The query an aggregate reduces the solutions of.

aggregate-functors clj

The five aggregation operators, mapped to the reduction each names. All five take the shape (<op> ?n ?v <body>).

aggregate-value-var clj

(aggregate-value-var form)

The variable an aggregate reduces over — the one projected out. Nil when the slot holds something that is not a variable, which wff refuses separately.

aggregate? clj

(aggregate? form)

Is form an (<aggregate-op> ?n ?v <body>) literal?

and-functor clj

arrangements-over clj

(arrangements-over form comps)

commuting-arrangements against components already in hand — the form a caller takes when it knows the components from somewhere other than the literal's own functor.

Forward chaining is that caller: a datum arrives and the rule antecedent it is matched against may name a super-predicate of the datum's functor, while what licences the permutation is the datum's own declaration (chain/symmetric-mirror states the same rule for the binary case). So the components come off the fact and the arrangements are built over the antecedent.

assumption-rule-wrapper clj

(set/assumptionRule (implies …)) — the rule's head is a choice offered to a solve, not a truth to derive. Canonicalizes into :effect :choose; the rule never forward-chains into belief and is consulted only when grounding a solve (docs/solving.md).

authored-sentence clj

(authored-sentence sx)

A stored sentex's sentence with the author's variable names restored through its own :varmap; a fact carries no varmap and its sentence comes back unchanged. The one spelling of the display form: vaelii.core/readable-sentence delegates here, and chain's refusal report, inference's proof tree, io.text's writer, quality's rule lines and violations' dropped-rule entry call it.

body clj

(body {:keys [sentence antecedent]})

The positive atomic form a sentex asserts (a fact's sentence without its not); nil for a rule.

canon clj

(canon x)

Canonicalize a sentence to a single sequential representation (PersistentList, recursively), interning every symbol through symbol-pool-generations on the way. Substitution and reads produce lazy seqs / vectors that are = but freeze to different nippy bytes; canonicalizing before anything reaches a key or value keeps trie keys and dedup stable, and the interning collapses the repeated vocabulary to shared objects — the trie key reuses them for free, since it passes constant symbols through unchanged.

canonical-conjunction clj

(canonical-conjunction literals)

(canonical-conjunction literals start)

[canonical varmap] for a conjunction: every variable across all of literals renumbered ?var0 ?var1 … by first occurrence under one shared numbering, and the map from each canonical name back to the name it replaced.

One numbering across the whole conjunction, not one per literal — a variable shared between two literals is what joins them, and numbering them apart would break the join into two questions.

The point of canonicalizing a conjunction (rather than a rule, which canonicalize-rule already does at storage) is identity: two conjunctions that differ only in what their variables are called become the same value, so a search that reaches one twice can recognize it. varmap is how a solution found in canonical space is carried back to the names the caller used — applied with rename-vars, which is one pass because this map can be a permutation.

start numbers from ?var<start> instead of ?var0, which is how a form is renamed clear of another one whose variables are already numbered ?var0 … ?var<start-1>: the two namespaces become disjoint by construction rather than by inventing decorated names. A stored rule is spelled ?var0 ?var1 …, so unifying one against a conjunction spelled the same way needs exactly this before it can mean anything.

canonical-engines clj

(canonical-engines engines)

The shared instance of the engine set engines.

canonical-exception clj

(canonical-exception conjuncts rule-vars)

An exceptWhen exception's conjuncts, already in the rule's canonical variables rule-vars, in their stored form: sorted (sort-conjuncts), with every variable a quantifier inside them binds numbered past the rule's own. Two exceptions that differ only in a binder's name are then one meta-sentex, as two rules that differ only in a variable's name are one rule.

Each conjunct is numbered alone first, so the sort reads structure rather than the author's binder names, and then once more across the sorted conjuncts, so two conjuncts' binders stay distinct names.

census-bound-vars clj

(census-bound-vars body)

The variables an aggregate's census body binds for itself: what its generator conjuncts match, plus what its computed conjuncts write. An inner thereExists binder is not among them. Read by check-naf-closed's census check and by provers/AggregateProver's applicability (docs/aggregate.md, "Grouping").

chained-comparisons clj

Variable-arity, transitive comparisons whose chains collapse into one literal: (lessThan ?a ?b) + (lessThan ?b ?c) ⇒ (lessThan ?a ?b ?c).

check-exception-closed clj

(check-exception-closed antecedents exception)

Throw unless the exceptWhen exception is closed over antecedents: every free variable it reads is bound before it runs, so the rule's bindings never wait on the exception. The mirror of rules/check-range-restricted, pointed at the exception instead of the consequent.

Free as free-vars counts it, so a thereExists the exception carries binds its own witness — "birds fly unless they have a sick child" is (thereExists ?c (and (childOf ?b ?c) (sick ?c))). That binder must be local (:quantifier-not-local): one the antecedents also name would be substituted with the rule's binding before the query runs, leaving a quantifier over a constant.

check-naf-closed clj

(check-naf-closed antes conseq exc)

Throw unless a rule's negation-as-failure antecedents are usable — the mirror of check-exception-closed, pointed at unknown / thereExists:

• unknown is closed. Every free variable of an (unknown S) antecedent (the ones a nested thereExists does not bind) is bound by a generator antecedent — a positive literal that produces bindings, which a standalone thereExists becomes once desugared, but which unknown and the evaluables never are. unknown produces no bindings and consumes them, so reaching one before its inputs exist tests an open formula and silently yields nothing; forbidding it makes the mistake a legible error instead.
• Every quantifier is local. A thereExists bound variable appears nowhere in the rule outside its own thereExists literal, so it cannot leak into the consequent (a range-restriction hole) or capture another literal's variable (a silent misjoin). Both read as working code, so both are refused here. Locality is what makes a quantified conjunction readable: the binder is shared by the conjuncts of one query and by nothing else, which is exactly the scope the join needs (unproducible-inputs holds the other half — a quantified variable some generator conjunct of the same query has to produce).
• An aggregate is closed and its reduction variable is local, by the same two rules. A body variable the rule names nowhere else is the census's own join, and must be one census-bound-vars reaches (:naf-not-closed).
• The reduction slot holds a variable (:not-well-formed), and so does every thereExists, forall and head exists binder.
• Every deferred literal's inputs are bound by a generator antecedent or by a deferred literal written before it (an aggregate's ?n, an evaluate's output), since the chainer throws on an unbound input mid-fixpoint.

docs/aggregate.md, "Grouping" and "Comparing the count", gives the reasons.

commuting-arrangements clj

(commuting-arrangements form groups-of)

Every rearrangement of form a lookup has to probe for, given the components groups-of licences at this literal's arity. form itself is first; a literal that commutes nothing yields just the one.

Pruned to the arrangements a stored fact can actually have. Storage sorts a ground literal within each component (sort-commuting-args), so a stored fact never holds its ground arguments out of order inside a component — and an arrangement that does can be skipped without losing an answer. The argument: unification is positional, so an arrangement's ground argument at a slot must equal the stored fact's, and a sorted sequence read at any subset of its slots is itself sorted; an arrangement that unifies therefore already holds its ground arguments in order, and is one of these.

That rests on the stored fact being canonical under the declaration the fan is reading, which integrate/commute-existing is what maintains — the same precondition sort-symmetric-args has made since the mirror probe existed, and the reason a late declaration migrates what is stored rather than leaving lookup to find both spellings. That is what keeps the fan off the factorial: with v variables among a component of g positions the probes are g!/(g-v)! rather than g!, so a pattern whose tail is ground probes once however long the tail is, and one holding a single variable probes g times. Where the fan really is factorial the answer set is too — a pattern of g distinct variables matches one stored fact g! ways, each a different binding, exactly as (sibOf ?a ?b) matches a stored pair twice (res/raw-match).

Distinct by form: two arrangements that write the same literal are one probe, which is what collapses a repeated variable ((P ?a ?a)) back to a single probe.

commuting-components clj

(commuting-components groups arity)

The components groups licences at runtime arity arity: sorted position vectors, themselves in sorted order, each holding at least two positions.

Overlapping groups are merged rather than applied one after another. Two groups that share a position do not describe two independent permutations — (commutativeInArgs P 1 2) beside (commutativeInArgs P 2 3) says 1 and 2 interchange and 2 and 3 do, so 1 and 3 interchange through 2 — and sorting the two separately is not even well defined: the result would depend on which was applied first, which is an order dependence in the storage key. Merging into connected components makes the canonical form a function of the declaration set.

A component of one position licences nothing and is dropped, so a mark whose positions fall outside the literal's arity leaves the literal alone: (commutativeInArgAndRest P 3) on a binary (P a b) names position 3 only, and the empty result is what makes a one-argument predicate marked commutative identity-only rather than a special case.

comparison-siblings clj

Comparison predicates that fold onto a canonical sibling by reversing their arguments, so (greaterThan A B) is stored as (lessThan B A). Add a pair here and both directions canonicalize to one literal.

conjunction? clj

(conjunction? form)

Is form an (and …) conjunction?

conjuncts clj

(conjuncts form)

form's conjunct literals — an (and …) flattened all the way down, anything else as a one-element vector.

Flattened because a nested and is not a goal any prover claims: left as one conjunct it would be handed to the registry, come back unanswerable, and read as not derivable. Conjunction is associative, so flattening is the reading rather than a normalization of it. An (and) yields no conjuncts, which is the shape check-naf-closed refuses rather than a shape anything evaluates.

connective-problem clj

(connective-problem sentence)

connective-problems as one :not-well-formed problem map, or nil. assert and check read it right after the sentence shape, and an import reads it over each frame, so a malformed connective frame is refused before it can store as an opaque fact or a rule that answers wrongly.

connective-problems clj

(connective-problems sentence)

Structural problems with sentence's connective frames, as strings (empty if OK) — read by check and thrown by assert under :not-well-formed before anything is stored:

• a structural connective at an arity it does not have — (not A B) would store as a positive fact whose record and index disagree about what it says, an implies at arity 2 would throw a bare exception, and one at arity 4 would silently drop its tail;
• a rule or exception literal that is not itself a sentence — a bare symbol in antecedent or consequent position matches nothing and checks as nothing, and one as the operand of a rule wrapper or a not is no rule and no fact. A bare variable is a term, so it is refused in every rule role and as a wrapper's operand; a derived sentence whose predicate a firing binds is written (?pred . ?args);
• a head existential outside consequent position — exists marks a consequent variable for skolemization and is not a predicate;
• an (ist Ctx S) in any rule position — as a read the literal matches nothing, and as a consequent it places a conclusion where the rule and its facts need not be visible (ist-rule-problem);
• a nested implies anywhere but a rule's consequent — a rule is a sentence, not a literal, and consequent position is the one place it means something else: a generator, whose firing stamps the inner rule out (docs/generators.md). The nesting is not capped there: a stamped rule may stamp one in turn, and each level is checked in the ordinary rule roles;
• a negated rule — not over an implies, bare or wrapped: negation lives on facts, and what a rule's negation would mean is said as an exception or a retraction instead (the record has no shape for it — a rule under not would store a sentence its own key cannot be computed from);
• a top-level and — a conjunction is an antecedent or a query, never one assertable sentence; assert its conjuncts;
• a combination of set/* wrappers the record cannot hold — two directions, two head wrappers, or a choice or constraint head under a direction or set/defaultRule (wrapper-stack-problems).

constraint-rule-wrappers clj

(set/hardConstraint (implies …)) / (set/softConstraint (implies …)) — the rule's head is a contradiction marker and its body a conjunctive nogood over background facts and choice-head patterns. Canonicalizes into :effect (:forbid / :penalize); like an assumptionRule the rule never forward-chains, and a solve grounds its body (docs/solving.md). A hard constraint renders as an ASPIF integrity constraint (models violating it are excluded); a soft one as a minimized violation.

content-forms clj

(content-forms sentex)

The connective-free literals a sentex is indexed and searchable by: a rule's antecedents and consequent, or a fact's positive body — each with its structural connective heads stripped, so not / implies / and never reach the term index.

An exceptWhen exception is a separate meta-sentex, findable by the rule handle it names (its (sentexHandle H) is a ground compound the term index keeps); a rule's own content never mentions it. The exception re-check index ([:exception-index <predicate>]) is what answers "which rules watch this predicate".

default-rule-wrapper clj

defeat-functor clj

(defeat <handle>) — a meta-sentex the engine derives that removes the sentex the handle names from belief at the context it is stored in and every context that sees it, read at read time. assert refuses it in every literal (checks/check-no-defeat).

deferred-input-vars clj

(deferred-input-vars g)

The variables a deferred literal must have bound before it can run: free-vars for unknown and the aggregates, and every argument it does not write for the rest.

deferred-literal? clj

(deferred-literal? l)

Is this literal one of the deferred (evaluable) ones? Public because the storage canonicalization here and the query planner (vaelii.impl.plan) must hold back exactly the same set — if the two ever disagreed, a planner could hoist an evaluate above the literal binding its arguments, which yields no solutions rather than an error.

deferred-output-vars clj

(deferred-output-vars g)

The variables a deferred literal binds — evaluate's first argument, an aggregate's ?n, and nothing at all for a pure test like lessThan or different.

deferred-predicates clj

Predicates that consume bindings rather than produce them — evaluable tests and computations. Antecedent order is operational for these: (evaluate ?z (+ ?x ?y)) can only run once ?x/?y are bound, so they must stay after the literals that bind them. Canonical ordering therefore keeps them last, in the author's relative order (one computation may feed the next).

different is here for the same reason and no other. It is a ground-only test over the equality closure (vaelii.impl.provers), so a different antecedent sorted ahead of the literal that binds its variables is not merely slow — it is inapplicable, and the rule silently stops firing.

Being deferred is all different shares with the comparisons: it is deliberately absent from comparison-siblings and chained-comparisons below. The obvious analogy is wrong. lessThan merges chains because it is transitive — a<b and b<c give a<b<c for free — whereas different is not: A≠B and B≠C say nothing whatever about A and C, so merging (different A B) with (different B C) into (different A B C) would manufacture a pairwise claim nobody asserted. The only sound merge would be a clique (every pair present), which is more machinery than the feature is worth. And since different is never stored, there is nothing to canonicalize for: canonical form exists so that logically identical knowledge stores once, and this stores never. See docs/equality.md.

unknown is here for the same operational reason: (unknown S) is negation as failure — it holds exactly while S is not derivable — so it consumes the bindings its argument's free variables need and produces none. Reaching it before those bindings exist would test an open formula, which is meaningless, so like different it is pinned after the generators that bind it (docs/naf.md). Its argument's quantified variables (a nested thereExists) are not among the ones that must be bound — that is the whole point of the quantifier — so the pinning and closure logic reads free-vars, not every variable. thereExists is deliberately absent: a standalone positive (thereExists ?x S) antecedent is desugared to S with ?x a local generator variable (see the constructor), so it never reaches the chainers as its own literal; only unknown does.

The quantity comparisons (sameQuantity / quantityLessThan / quantityGreaterThan / quantityLessThanOrEqual / quantityGreaterThanOrEqual) are deferred for the evaluate reason: QuantityProver (vaelii.impl.provers) computes them from two ground measure terms, so a comparison sorted ahead of the literal that binds its measure variable is inapplicable and the rule silently stops firing — pinning it after its binders is what a rule antecedent like (quantityGreaterThan ?q (QuantityFn 100 Kilogram)), whose ?q a (mass ?o ?q) produces, needs. Like different, being deferred is all they share with the arithmetic comparisons: they are absent from comparison-siblings and chained-comparisons above. sameQuantity is symmetric, not directional, so it folds onto no < sibling; and while quantityLessThan is transitive, a measure chain crosses units, so collapsing (quantityLessThan a b) + (quantityLessThan b c) into one variable-arity literal would smuggle in a normalization the prover has not run — the same over-eager analogy the different note warns against.

The aggregates are deferred because a group variable such as ?x in (agg/count ?n ?v (ancestorOf ?v ?x)) must be bound first, or the census counts the whole relation (docs/aggregate.md).

integer and matchesPattern are here for the lessThan reason: EvaluableProver computes them from ground arguments and nothing stores them, so a rule's join sends (matchesPattern ?s "a+b") to the registry once the literal binding ?s has run.

defn-companion-rules clj

(defn-companion-rules [pred coll cond])

The forward rule sentence(s) a defn* sentence expands into, each relating (Coll ?x) to the condition on the member ?x:

(defnNecessary Coll C) -> [(implies (Coll ?x) C)] ; member => condition (defnSufficient Coll C) -> [(implies C (Coll ?x))] ; condition => member (defnIff Coll C) -> both

Built from the sentence as written, where the member is still ?x; each rule is canonicalized when stored, and a necessary condition that is a conjunction splits into one rule per conjunct like any conjunctive consequent. A sufficient condition in which no generator conjunct names ?x — (and (integer ?x) (greaterThan ?x 0)), every conjunct computed — expands to no rule: nothing binds the member for a join, so check-naf-closed would refuse it, and DefnSufficientProver answers membership.

defn-condition-problems clj

(defn-condition-problems [pred _coll cond :as s])

Why the defn* sentence s is not well-formed, as problem strings (empty if OK). The condition must mention the member variable ?x: a condition that does not name the member says nothing about membership, and would expand to a rule that concludes it vacuously (necessary) or is not range-restricted (sufficient).

defn-member-var clj

The distinguished variable a defn* sentence names the member by. (defnNecessary Coll <cond>) reads <cond> as a condition on ?x and expands to a rule relating (Coll ?x) to it. One fixed spelling, so the member stays identifiable after canonicalization renames every other variable in the condition.

defn-predicates clj

The three definitional collection relations, each expanded into forward rules at assert (docs/defns.md). A syntactic set, read where a defn* sentence must be recognized: exempted from the ground check (its condition carries ?x), given a well-formedness arm, and materialized into companion rules.

defn-sentence? clj

(defn-sentence? sentence)

Is sentence one of the definitional collection relations — defnNecessary, defnSufficient or defnIff? Read off the functor, so it recognizes the fact a defn* assertion stores rather than any rule it expands into.

desugar-forall-literal clj

(desugar-forall-literal form)

The nested NAF an antecedent (forall ?y (implies Body Head)) is:

(forall ?y (implies Body Head))
=> (unknown (thereExists ?y (and Body… (unknown Head))))

∀?y (Body ⇒ Head) is ¬∃?y (Body ∧ ¬Head), and in a closed world ¬ is unknown — so the universal is two negations around the existential the engine already answers. Nothing new evaluates it: the outer unknown is a NAF query, its conjunction is joined (provers/conjunction-solutions), and the inner unknown is a conjunct like any other, reached once the generators of the same query have bound ?y.

A conjunctive Body contributes that many conjuncts, so the join sees the generators the author wrote. Head is left whole — an (and …) head is one nested unknown over a conjunction, which is again a query the join answers.

The binder is local, as every quantifier's is: ?y may not appear outside the forall (check-naf-closed's :quantifier-not-local), and every other variable in the body must be bound by an antecedent outside it (:naf-not-closed). The desugared form is what the checks read and what canonical-sentex shows — the sugar exists at the entry point and nowhere past it.

A forall whose second argument is not an (implies …) is refused: there is nothing to negate the consequent of, and a universal over a bare literal is a claim about every term in the domain rather than a guard.

desugar-forall-rule clj

(desugar-forall-rule rule-form)

rule-form with every (forall …) antecedent replaced by the nested NAF it is (desugar-forall-literal), or the form unchanged when it carries none.

Applied at both entry points a rule reaches — the sentex constructor and rules/inner-rule, which every pre-storage check reads through — so range restriction, closure, the quantifier locality rule and the stratification graph all see the NAF form rather than the sugar. A stored rule never holds a forall, so the gate is a some that allocates nothing and this is the identity on it.

desugar-there-exists clj

(desugar-there-exists antes)

Rewrite a rule's antecedent list, replacing every standalone positive (thereExists ?x S) with its body S. A standalone existential antecedent is exactly S with ?x a fresh local variable that the match binds and that (by locality) reaches nothing else — so S alone is the faithful, native reading, and it needs no special matcher: it joins the store like any generator, one witness per solution. A thereExists under unknown is a NAF query, evaluated by the prover, and is not touched here.

A conjunctive body is spliced in as that many antecedents, which is the same reading one step further: the binder's variable is shared across the conjuncts, and antecedents sharing a variable are exactly the join that gives them one witness. So (thereExists ?y (and (parentOf ?x ?y) (sick ?y))) becomes the two-generator body a reader would have written by hand.

direction-engines clj

The engines each set/*Rule direction runs a rule in, as the :direction opt and the wrappers spell them. :forward and :both are one set: a forward rule answers backward goals too.

disjunction? clj

(disjunction? form)

Is form a disjunction (or <alternative> ...)? Arity is not checked here — an empty (or) is a disjunction that no alternative satisfies, and naming it as one is what lets rules/disjunction-problems refuse it by that name.

disjuncts clj

(disjuncts form)

The alternatives a disjunction offers.

do-form? clj

(do-form? form)

Is form a do/ imperative?

Used both to dispatch one at the top level of assert and to refuse one anywhere it would run inside a fixpoint — a rule antecedent, a rule consequent, an exceptWhen query, or anything derived. Forward chaining's defining property is that the same knowledge in any order yields the same beliefs; an imperative firing during it would run a number of times that depends on firing order, and would mutate the KB the fixpoint is still computing over. That breaks order independence and locality at once (docs/nmtms.md), so do/ is legal only where a caller put it: at the top level of an assert, once, after settling.

do-namespace clj

The namespace marking an imperative — a form given to assert that instructs the engine to do something rather than stating that something is true. (do/labeling Ctx) is the first (docs/labeling.md).

It parallels set/, which sets a field on the rule it wraps, and ist, which is likewise given to assert and likewise never stored. Nothing in the do/ namespace is ever a sentex: there is no fact to store, only an action to take.

dot-marker clj

effect-constraint clj

(effect-constraint effect)

The constraint class of an :effect — :hard for :forbid, :soft for :penalize, nil otherwise.

engines-direction clj

(engines-direction engines)

The direction whose set/*Rule wrapper spells the base engines of engines (:solve aside) — :backward, :forward, :forward-only or :inert.

except-functor clj

(except <handle>) — a meta-sentex removing visibility of the sentex the handle names from the context it is asserted in and that context's descendants (everything that sees it). A ground fact — the handle is ground — belief-following like any other, so retracting or defeating the except restores the hidden sentex.

except-wrapper clj

(exceptWhen <query> <rule>) — the rule does not conclude for a binding its exception holds of. Unlike the other wrappers this one takes two arguments and captures one: the query. The wrapper is split off at the assert layer and stored as a (exceptWhen <query> (sentexHandle <rule-id>)) meta-sentex naming the rule, rather than folded into the rule record (see exceptWhen-meta).

exception-conjuncts clj

(exception-conjuncts form)

Normalize an exceptWhen query to its one internal shape — a vector of literals, all of which must hold. A conjunction is written as a vector, the way core/prove spells one; a single literal may be written bare.

A forall conjunct is the nested NAF it is (desugar-forall-literal), as a forall antecedent is, so the re-check index and the stratification graph read the predicates under it. A malformed one is left for check-exception-closed to refuse: this runs inside peel-rule-wrapper, which reports rather than throws.

exception-query-conjuncts clj

(exception-query-conjuncts sentence)

The conjunct literals of an exceptWhen meta-sentence's query — the inner (and …) unwrapped, or a bare single literal as a one-element vector. The inverse of exceptWhen-meta.

exception-strength-problem clj

(exception-strength-problem form)

The :shape problem a malformed strength wrapper on an exceptWhen query is refused with, or nil. A value for check, and the ex-info peel-exception-strength throws — so the two entry points refuse the same input in the same words, differing only in the delivery.

exceptWhen-meta clj

(exceptWhen-meta conjuncts rule-id)

The exceptWhen meta-sentence for conjuncts (a seq of literals, all of which must hold) qualifying the rule at rule-id. A single literal is stored bare, several as an (and …) — canon-stable either way (a vector would flatten to a list and lose the shape).

exceptWhen-meta? clj

(exceptWhen-meta? sentence)

Is sentence a (exceptWhen <query> (sentexHandle <id>)) meta-sentex — the stored form, whose second argument is a handle (as opposed to the (exceptWhen <query> <rule>) wrapper, whose second argument is a rule form)?

exceptWhen-rule-handle clj

(exceptWhen-rule-handle sentence)

The rule handle an exceptWhen meta-sentence names.

exists-functor clj

fielded-rule-slots clj

(fielded-rule-slots direction assumption constraint)

The [engines effect] of a rule frame that spells its wrappers as the three fields direction / assumption / constraint — the disk codec's rule tags 1, 3, 5, 7, 8 and 9, a record thawed whole under those keys, and a dump frame keyed by them. Such a frame always carries a direction.

forall-functor clj

forall? clj

(forall? form)

Is form a (forall <var-or-vars> (implies Body Head)) universal?

form-variables clj

(form-variables form)

Every variable anywhere in form, as a set — #{} rather than symbols-where's nil, since every caller folds the answer into something or calls it as a fn. The one set walk: resolution, plan, quality, provers and asp.solve-context call it.

form-vars clj

(form-vars form)

Every variable anywhere in form, in order of occurrence and with duplicates, so a variable used twice counts twice (locality reads occurrence counts). Lazy. The one walk for a variable sequence: rules, skolem, rewrite, asp.solve-context and the exception closure check call it; form-variables is the set form.

forms-where clj

(forms-where pred form)

Every sub-form satisfying pred, depth-first pre-order, as a vector. The collecting form of some-form — a vector rather than nil, because its callers report each form they find rather than gating on the first.

free-vars clj

(free-vars form)

The variables of form that must be bound before it can be evaluated — every variable it mentions, minus any bound by a quantifier within it. unknown is transparent (it binds nothing), a thereExists and a forall each subtract their binder, and every other form contributes all of its variables. This is what the closure check and the planner read for a NAF literal instead of the raw variable set: the point of (unknown (thereExists ?x (parentOf ?x Tom))) is that ?x is not one of the variables an antecedent has to supply.

ground-term? clj

(ground-term? t)

True when t contains no pattern variable anywhere.

ground? clj

(ground? sx)

True when the sentence contains no pattern variables (anywhere, nested).

handle-id clj

(handle-id form)

The sentex id a handle names, or nil when form is not a handle.

head-exists-body clj

(head-exists-body form)

The consequent C inside a head (exists <vars> C).

head-exists-vars clj

(head-exists-vars form)

The existential variables a head (exists <vars> C) introduces, as a set — a single variable or a sequence of them (quantified-vars reads either shape).

head-exists? clj

(head-exists? form)

Is form a head existential (exists <var-or-vars> C)?

implies? clj

(implies? form)

Is form a rule form (implies <ante> <conseq>)? Arity checked: an implies at any other arity is never read as a rule — rule-consequent is an nth, so an arity-4 form read as a rule would silently drop its tail. connective-problems refuses the malformed form at both entry points before this question is asked.

index-terms clj

(index-terms sentex)

The distinct terms that make a sentex findable: the atoms of its connective-free content at every depth, plus each ground compound between *min-indexed-depth* and max-indexed-compound. The sentex's context is added separately by the index.

indexable-term? clj

(indexable-term? t)

A subterm worth an inverted-index entry: a non-variable symbol (predicate, individual, type, context) or a fully-ground compound. Numbers, strings, and variables are dropped — useless lookup keys that only bloat the index.

intern-deep clj

(intern-deep x)

x with every symbol replaced by its pooled instance, preserving shape — a list stays a list and a vector a vector. canon is the other half of the same pair and flattens both to a list, which is right for a sentence and wrong for anything already canonical that is being rebuilt from bytes: a rule's :antecedent is a vector and a [::subterm k] marker must stay one.

So this is what every path back into memory uses — the record frames (vaelii.impl.disk.codec) and the index snapshot's token dictionary (vaelii.impl.disk.index-snapshot). Without it a thawed structure holds a private copy of every name it mentions, which on a store whose whole point is that the vocabulary is written once is the one cost that must not be paid per record.

intern-sym clj

(intern-sym s)

The pooled instance of symbol s (or s unchanged when it is not a symbol). Interning changes identity, never equality, so a pooled ?var0 still matches a fresh one as a binding key.

A hit in current pays one .get. A miss reads previous, rotates when current is full, and puts the symbol into current, as previous's instance when previous held one. A thread racing a rotation can put into the map that has just become previous; the entry stays findable there, so the race costs at most a missed sharing and never a wrong symbol.

ist-functor clj

key-stream clj

(key-stream body)

The structural token stream for a fact body: the functor at the top level (no leading marker, so the [pred …] prefix and the predicate extent's node [pred] stay the trie's first level), then each argument linearized. Deterministic and compound-blind, so it composes with α-rename and dedup unchanged — an atom body degenerates to [body].

max-indexed-compound clj

Largest ground compound subterm (node count) the inverted term index gives its own key — the ceiling *min-indexed-depth* is the floor of. Indexing a huge one stores a key holding the entire subtree (O(size) bytes, a full WAL frame on disk), so a deep ground term would cost O(depth²) index bytes and a wide one a key per level. Above the bound the whole-compound key is dropped and every symbol it contains is still indexed individually (atoms are never capped), so the term stays findable — find-sentexes pays a read for it instead. Scoped to [:term-index]: indexable-term? (which also drives the [:argument-root] argument roots) is untouched.

mentions? clj

(mentions? sentex term)

Does sentex's connective-free content hold term as a subterm? The question the term index answers wherever it has a key, asked of the record instead — the verify half of a compound probe, which turns probe-atoms' superset into the exact answer.

mirror-literal clj

(mirror-literal form)

The argument-swapped twin of a binary literal, for symmetric lookup.

naf-query-conjuncts clj

(naf-query-conjuncts unk)

The conjunct literals an (unknown …) antecedent's query is evaluated as — the inner (and …) unwrapped, a single literal as a one-element vector. The unknown spelling of exception-query-conjuncts, and the same reading: unknown is exceptWhen inlined per literal, so its query is a closed conjunction evaluated block-if-all-hold, and one evaluator (provers/exception-holds?) answers both.

The conjunction is joined, left to right in a planned order, so a conjunct may read what an earlier one bound: that is what makes (unknown (thereExists ?c (and (childOf Tom ?c) (sick ?c)))) mean what it says, one witness satisfying both conjuncts (docs/naf.md). Closure is still enforced — every variable is either bound before the query runs or bound by a quantifier inside it (check-naf-closed).

negation? clj

(negation? form)

Is form a negation (not <body>)? Arity checked, so a not at any other arity is not one.

negative? clj

(negative? sx)

Is sx a negative literal — a sentex whose sentence is (not S)? The record keeps no separate sign: construction leaves at most one not, at the head (peel-not), so the head is the whole answer. False for a rule, which holds no sentence.

not-functor clj

or-functor clj

originalize clj

(originalize form varmap)

Restore the author's variable names in form using a sentex's :varmap ({?var0 ?x}), for display. rename-vars under the name the display path calls it.

path clj

(path sentex)

The full trie path for a sentex: its (connective-free, α-renamed, structurally linearized) key tokens with the context appended as the final level.

peel-exception-strength clj

(peel-exception-strength sentence)

[sentence monotonic?] — sentence with the strength wrapper taken off its exceptWhen query, and the class that wrapper stated for the exception alone.

assert passes one opts to both halves of an (exceptWhen Q R): the rule is stored at that strength and so is the meta-sentex carrying Q. That says everything for three of the four rule×exception pairings and cannot say the fourth — a known-true exception on a default rule — which is what this reads instead. Nothing below the assert entry point sees the wrapper: the split, the naming checks and the store all read the sentence they always did.

Untouched when there is none, rather than rebuilt identically, so a sentence with no wrapper is the object it arrived as.

peel-rule-wrapper clj

(peel-rule-wrapper form)

Strip the virtual rule wrappers, returning [direction defeasible exception assumption constraint inner]. Wrappers may nest in any order — a defeasible forward rule with an exception, an assumption rule, a hard constraint — and two exceptWhens conjoin. exception is nil or a vector of literals; assumption is true or nil; constraint is :hard / :soft or nil. A set/solveRule is stripped too, and solve-wrapped? reports it.

plain-symbol? clj

(plain-symbol? x)

A symbol that is not a variable.

polarity clj

(polarity sx)

:negative for a negative literal, :positive for any other sentex — the keyword a reader compares or hashes where it wants one value for the sign.

positive-body clj

(positive-body sentence)

The double-negation-eliminated positive body of a sentence, or nil when the sentence is genuinely negative. Constraint checks use this rather than the full canonical form: they must see the predicate and argument order the author wrote, not a folded sibling (greaterThan ⇒ lessThan) or sorted symmetric arguments, or an arg would be enforced against the wrong position.

probe-atoms clj

(probe-atoms term)

The keys a compound probe narrows by: the indexable atoms it contains. Every sentex holding the compound holds all of them — atoms are keyed at every depth under every bound — so their intersection is a superset of the answer, whatever key the compound itself does or does not earn. A compound holding no indexable atom — no symbol anywhere in it — has nothing to narrow by and probes by its own key: at the default floor it can only occur nested, which is where it has one.

quantified-vars clj

(quantified-vars form)

The variables a thereExists or forall binder introduces, as a set — its second element is a single variable or a sequence of them. A written vector [?x ?y] is accepted, but so is the list (?x ?y) it becomes once canon / variable numbering / goal rewriting have normalized every sequential to a PersistentList — so this must not key on vector?, or a binder would silently stop binding the moment the form was canonicalized. Non-variables are dropped, so free-vars reads a binder holding a constant without throwing; check-naf-closed refuses a rule that holds one.

rename-vars clj

(rename-vars form m)

form with every variable m names replaced by the name it maps to — one pass, each position rewritten at most once. Unmapped terms are left alone, and a vector stays a vector so a conjunction keeps its shape.

One pass is the whole point, and it is what separates a renaming from a substitution. res/substitute chases: it looks a variable up, then looks its value up, until it reaches something unbound — right for a unifier, whose bindings form an acyclic chain to a term (the occurs check is what guarantees that). A renaming is a permutation, and permutations have cycles: applying {?var0 ?var1, ?var1 ?var0} to (P ?var0 ?var1) must give (P ?var1 ?var0), where chasing would follow ?var0 → ?var1 → ?var0 and never stop. So the two maps look alike and cannot share a function.

This is the operation that carries a form between two canonical namings — the map canonical-conjunction hands back, a rule's :varmap, a cache's rename-back.

rule-antecedents clj

(rule-antecedents form)

The antecedent patterns of a rule form (unwrapping a leading and; a single antecedent needs no and).

rule-consequent clj

(rule-consequent form)

The consequent pattern of a rule form.

rule-direction-wrappers clj

rule-functor clj

rule-sentence clj

(rule-sentence antes conseq)

Build the rule form from antecedent patterns + a consequent pattern — a single antecedent needs no and. This is the spelling the constructor stores (it rebuilds the sentence from the canonical antecedents below), so it is the one builder: rules/rule-sentence delegates here, so a rule reaches the constructor in exactly one surface spelling rather than two that only canonicalization converges.

rule-slots clj

(rule-slots dir assumption constraint generator?)

(rule-slots dir assumption constraint solve? generator?)

The record's [engines effect] for a rule written with direction dir (nil when no direction wrapper was written) under the head wrappers assumption / constraint, and under set/solveRule when solve?. An unwrapped rule runs backward, and an unwrapped generator forward, since no backward goal asks for a rule; solve? adds :solve. A choice or constraint rule runs in a solve whatever dir says.

sentence-of clj

(sentence-of sx)

A sentex's canonical sentence: a literal's :sentence, or for a rule the (implies <antecedent> <consequent>) form rule-sentence builds from its two fields. A rule record holds only the fields, so this is the one place its whole form comes from — the form path keys on and core/readable-sentence renames for display. Keyword reads only, so a sentex map off the wire answers the same as the record.

sentex clj

(sentex sentence)

(sentex sentence context)

(sentex sentence
        context
        {:keys [symmetric? groups-of]
         :or {symmetric? (constantly false) groups-of (constantly nil)}
         :as _opts})

Construct a sentex — a LiteralSentex or a RuleSentex — canonicalizing the structural connectives into the record and the sentence into canonical form (see the namespace docstring). Context defaults to 'default; id defaults to nil until the record store assigns a handle.

opts may carry the two canonicalization reads: :symmetric?, a predicate telling whether a functor is declared symmetric, so its two arguments can be sorted, and :groups-of, (fn [functor arity] -> groups) giving the commutativity groups the functor declares, so the arguments inside each component can be. Without them no predicate commutes anything (a pure, KB-free construction).

sentex-handle clj

(sentex-handle n)

The handle term naming the sentex stored at id n.

sentex-handle-functor clj

sentex-handle? clj

(sentex-handle? form)

Is form a (sentexHandle <id>) term?

solve-engines clj

The engines of a choice or constraint rule: a solve alone reads it.

solve-rule-wrapper clj

(set/solveRule (implies …)) — the rule also runs in a solve, as a normal rule (h :- b): a solve derives its head in every answer set whose atoms satisfy its body, and a constraint may name it. Adds :solve to the record's :engines; a direction wrapper beside it says how the rule runs in base (backward when there is none), and set/inertRule makes it a rule that runs in a solve alone (docs/solving.md).

solve-wrapped? clj

(solve-wrapped? form)

Is form a rule written under set/solveRule, at any depth of its wrapper stack?

some-form clj

(some-form pred form)

The first sub-form of form satisfying pred — form itself included, depth-first pre-order, the order (first (filter pred (tree-seq …))) yields — or nil. Descends compounds and asks pred of every node, so pred decides what a node has to be.

Nil is the whole of "no match", so a pred that holds of nil or false reads as one; every caller's holds of compounds, which are neither.

some-symbol? clj

(some-symbol? pred form)

Does any symbol anywhere in form satisfy pred? Short-circuits on the first.

A direct walk rather than some over tree-seq, for the reason chain's free-consequent-vars is one: this runs per stored sentex on paths that ask it of every match in an answer set, the form is usually (pred a b), and the lazy seq tree-seq builds costs several times the three cond arms it describes. Nothing is allocated on the overwhelmingly common false answer.

sort-conjuncts clj

(sort-conjuncts literals)

Put a conjunction of literals into canonical order and drop duplicates, using the same structural comparator the rule canonicalizer uses. An exceptWhen exception's conjuncts are independent ground checks, so their written order (and a repeat) is not their identity — sorting makes two spellings of one exception the same meta-sentex.

strength-wrapper clj

(set/monotonic S) — S asserted known-true. In the set/ namespace with the rule wrappers above and for their reason: it states how the sentence is asserted rather than anything the sentence says, and never reaches the store as a functor.

Two entry points read it, in two positions. The text KB format (vaelii.impl.io.text) reads it around a whole form and hands assert a {:strength :monotonic}. assert itself reads it around an exceptWhen's query, where it states the exception's own class — the one thing an opts cannot say, since one opts reaches both halves of an exceptWhen (peel-exception-strength).

subterm-arity clj

The element count an arity marker carries.

subterm-mark clj

An arity marker for a k-element subterm.

subterm-mark? clj

Is x an arity marker?

subterms clj

(subterms sentence)

Every subterm of a sentence — each atom and each compound subterm, recursively, the whole sentence included.

symbols-where clj

(symbols-where pred form)

The set of symbols anywhere in form satisfying pred, or nil when none does. The collecting form of some-symbol?, and nil rather than #{} so a caller can gate on it without allocating for the common empty answer.

symmetric-literal? clj

(symmetric-literal? form symmetric?)

A binary literal whose predicate is declared symmetric (and not a dotted form).

there-exists-antecedent? clj

(there-exists-antecedent? form)

A standalone positive thereExists antecedent — one not wrapped in unknown. These desugar to their body (the quantifier's variable becoming a local matched variable); a thereExists inside an unknown is left intact for the NAF prover.

there-exists-functor clj

there-exists? clj

(there-exists? form)

Is form a (thereExists <var-or-vars> S) existential?

underlying-body clj

(underlying-body sentence)

The body a sentence's not wrappers enclose, whatever its polarity — S for both S and (not S).

Its neighbour above answers the constraint question, where a genuinely negative sentence has no body to constrain and nil is the right answer. This answers the content question: (not (penguin X)) is content about penguin, so a trigger keyed on a predicate has to see it arrive and leave, and a re-check that only ever saw the positive polarity would miss every withdrawal a negation causes.

unknown-functor clj

unknown? clj

(unknown? form)

Is form an (unknown S) NAF literal?

variable? clj

A pattern variable: a symbol whose name starts with ?, or _ (vaelii.impl.types.sentex/variable?, which the columnar trie calls).

wrapper-effect clj

(wrapper-effect assumption constraint)

The :effect a rule's head wrappers give it: :choose under set/assumptionRule, :forbid / :penalize under a hard / soft constraint, :derive under neither.

wrapper-stack-problems clj

(wrapper-stack-problems form)

What is wrong with the combination of set/* wrappers around one rule, as strings. The wrappers state two things: how a rule runs (a direction wrapper, set/defaultRule) and what its head is (set/assumptionRule a choice, set/hardConstraint / set/softConstraint a contradiction marker). Four combinations state nothing the record can hold, and each would otherwise be dropped in silence:

• two different direction wrappers — the record holds one direction, and the innermost would win;
• two different head wrappers — a head is one of a choice, a hard constraint and a soft one;
• a head wrapper with a direction wrapper, set/defaultRule or set/solveRule — a choice or constraint head is decided by a solve and never chained or believed, so how it would chain, and what strength its conclusions would carry, say nothing, and it runs in a solve already (docs/solving.md);
• set/solveRule with set/defaultRule — one answer set has no defeat to apply, so a defeasible rule has no reading inside a solve.