vaelii.impl.sentex — com.vaelii/vaelii 0.29.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. The root starts at 1M, above the shipped ontology plus the whole of OpenCyc (~188k constants), and size-symbol-pool raises it when a store with a larger token dictionary opens. Past the limit the generations rotate: 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, which an open does not move.

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

arg-projections clj

Each binary projection of arg, with the position it projects: (argN P T) states what (arg P N T) states. The declaration checks and the integrity census read it.

arity-binding clj

(arity-binding s)

[P kind value] for the sentence s of a stored fact that binds a relation's length, else nil: (arity P n) and an exact-arity class membership bind :exact n, a variable_arity membership :var nil, and (arityMin P m) :min m. The index posts each under its binding family (vaelii.impl.kv), which arity/relation-length reads.

arity-binding-functors clj

The functors of the facts arity-binding answers a length binding for.

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, the conjunctions inside it ordered as a rule's unknown antecedent's are (sort-query-conjunctions, naf-numberings), so the sort reads structure rather than the author's binder names; then once more across the sorted conjuncts, so two conjuncts' binders stay distinct names. A deferred literal inside a conjunct keeps its written place among the deferred literals of its conjunction, after the generators: the forward join runs a deferred literal whose inputs are not yet bound in that order, and an aggregate binds what a later test reads.

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 rule antecedents antes (with consequent conseq and exception exc) use their NAF and deferred literals soundly:

• every free variable of an unknown, aggregate or other deferred literal is bound by a generator antecedent or by a deferred literal written before it (:naf-not-closed);
• a thereExists binder or an aggregate's reduction variable appears nowhere outside its own literal (:quantifier-not-local);
• a quantified variable a computed conjunct of an unknown query reads is produced by a generator conjunct of the same query (unproducible-inputs, :naf-not-closed), and an aggregate's local census variables are ones census-bound-vars reaches;
• an unknown query is not an empty conjunction, a reduction slot holds a variable, and so does every thereExists, forall and head exists binder (:not-well-formed).

docs/naf.md, "Fully bound to evaluate", and docs/aggregate.md, "Grouping", give the reasons.

closed? clj

(closed? sx)

True when the sentence has no free variable: every variable occurrence is bound by an enclosing quantifier or sits inside a (Quote …), the quoted form being syntax the sentence mentions. A ground? sentence answers at once. This is the test for "is this sentence closed"; ground? is the test for "does it hold any variable".

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. An (and) yields none (docs/naf.md, "S may be a conjunction").

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 generates the inner rule (docs/generators.md). The nesting is not capped there: a generated rule may generate 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 top-level or, or a not over one — nothing expands an or outside a rule antecedent (docs/canonicalization.md), so either would store as one opaque literal;
• a not over unknown, thereExists or forall in an antecedent or an exception, at any depth — no prover answers a negated query, so the condition never holds (docs/naf.md);
• 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 reason: it consumes the bindings its argument's free-vars need and produces none. thereExists is absent, because a standalone one is desugared to its body (desugar-there-exists, docs/naf.md).

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 — placing 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).

matchesPattern and the value kinds (integer, string, number, boolean, keyword, character) 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") or (string ?s) to the registry once the literal binding ?s has run. A value kind of a constant or a compound is read from the store instead (provers/term-value-kind-goal?).

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:

(unknown (thereExists ?y (and Body… (unknown Head))))

A conjunctive Body contributes its conjuncts; Head is left whole. Throws :not-well-formed when the second argument is not an (implies …) (docs/naf.md, "forall is sugar for a nested unknown").

desugar-forall-rule clj

(desugar-forall-rule rule-form)

rule-form with every (forall …) antecedent replaced by desugar-forall-literal's nested NAF. A form with none, and a form that is not a rule, is returned unchanged. Called by the sentex constructor and rules/inner-rule (docs/naf.md).

desugar-there-exists clj

(desugar-there-exists antes)

Rule antecedents antes with each standalone positive (thereExists ?x S) replaced by the conjuncts of S, spliced in (docs/naf.md, "Standalone positive thereExists desugars").

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.

exact-arity-classes clj

What each exact-arity class membership says the arity is. The arity sentexes and these memberships derive each other through the core.txt rules, so a declared relation normally has both — but a {:chain? false} assert or a KB loaded without the rules has only what was written, so both spellings are read.

Fifteen spellings, because core.txt ships fifteen classes. unary / binary / ternary / quaternary / quinary are the relation-wide ones and the other ten specialize them by kind, so a KB may write the arity of a function as (binary_function F) exactly as it writes a predicate's as (binary_predicate P). The arity readers read a stored membership by its own functor (arity-binding), and what a KB stored is whichever of the fifteen its author wrote.

The three arities never disagree across the spellings one term holds: a class and its specializations map to one number, and one separating declaration under fixed_arity separates the relation-wide five, which the ten inherit through their genl edges.

Here, below the index, arity/relation-length and kb/relation?, because all of them read it; a table copied twice is a table that drifts.

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, or a (set/monotonic …) / (set/inert …) elsewhere on the wrapper chain or inside the sentence, 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-peel clj

(form-peel form)

[sentence opts problem] for one whole form: (set/monotonic S) is S with {:strength :monotonic}, (set/inert S) is S with {:inert true}, and anything else is itself with nil. problem is the :shape refusal of a wrapper around no sentence or two, or around the other wrapper, since an inert sentex has no strength.

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 stopping at 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 those a quantifier inside it binds. unknown is transparent, thereExists and forall subtract their binder, and an aggregate subtracts its ?v and its ?n (docs/naf.md, "Fully bound to evaluate").

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). A plain tree search: a variable inside a (Quote …) or under a quantifier counts. closed? is the test for a sentence with no free variable.

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.

inert-wrapper clj

(set/inert S) — S stored through assert-inert: indexed and durable, never a premise. Read by the text KB format alone, around a whole form; assert, check and assert-inert refuse it on the wrapper chain and inside the sentence (:shape), since it names another entry point rather than an option of theirs.

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 S) antecedent's query is evaluated as: conjuncts of S. The unknown spelling of exception-query-conjuncts.

names-no-match? clj

(names-no-match? goal)

Is no-match a direct argument of literal goal?

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.

no-match clj

The reserved constant a read-mode reify resolves a never-minted NAT to, and a goal's application with no correspondence is replaced by. No stored sentex names it, and it denotes no term, so only the stored-fact prover reads a literal holding it (provers/applicable-provers).

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.

peel-strength clj

(peel-strength sentence opts)

[sentence opts]: a whole-form (set/monotonic S) read as S asserted {:strength :monotonic}, as the text KB format reads it, and anything else as it came. Throws :shape for a malformed wrapper and for one beside an opts :strength other than :monotonic.

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 variable or a sequence of them. A written vector becomes a list under canon, so this keys on sequential?, not vector?. Non-variables are dropped; check-naf-closed refuses a rule whose binder holds one.

quasiquote-functor clj

The template-constructing quoting function: (Quasiquote T) mentions T with its (Unquote v) holes spliced. quasiquote/quasiquote-function is this symbol.

quote-form? clj

(quote-form? form)

Is form a (Quote X) mention? unquoted-free-vars, res/unify, res/substitute and the literal cache's renaming all read a form this answers true for as a constant.

quote-functor clj

The quoting function whose argument is a form taken as syntax: (Quote X) mentions X. quasiquote/quote-function is this symbol.

quoting-functor? clj

(quoting-functor? head)

Is head one of the quoting-functors?

quoting-functors clj

The quoting functions — Quote and Quasiquote, fixed by the engine. A quoting function's arguments are a mention, a term named as syntax rather than used: they are held opaque to identity congruence (res/representative-term rewrites them by a rewriteOf spelling rename only, never by a sameAs / equals merge), not reified on their own when the application is (nat/reify-or-mint-nat), and not typed by what they denote (checks). The set is not declared in the KB and no assertion changes it, so whether an argument is a mention is a fact about the sentence alone.

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.

root-context clj

The context the upper ontology is stored in, every genlCx edge with it, and the one every context the shipped topology wires in sees (docs/contexts.md).

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?

size-symbol-pool clj

(size-symbol-pool tokens)

Raise the root of *symbol-pool-limit* to twice tokens, the entry count of a token dictionary a store is opening, and never lower it. A caller calls it before the dictionary interns its tokens, so one generation holds them all. A thread binding is left alone. See docs/storage.md, "Symbol interning".

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-peel clj

(strength-peel sentence opts)

[sentence opts problem]: sentence with a whole-form (set/monotonic S) read as S and :strength :monotonic in opts, or both as they came with the :shape problem that refuses them, or nil. A (set/inert S) comes back as it came, for the wrapper chain to refuse.

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.

Read in two positions. Around a whole sentence it is {:strength :monotonic}, read by the text KB format and by assert, check and try-assert alike (peel-strength). Around an exceptWhen's query 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). Anywhere else, on the wrapper chain or inside the sentence, it is refused (:shape).

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 branch 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)

Is antecedent form a standalone positive thereExists? On an antecedent list a thereExists under unknown is never an element.

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?

unquoted-free-vars clj

(unquoted-free-vars form)

The variables of form free in it: every variable occurrence that no enclosing forall, thereExists or head exists binds and no (Quote …) holds. A Quasiquote is not opaque, since its variables are meant to be bound from outside.

variable-arity-classes clj

The memberships that release a relation from one exact length.

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.