A NAT is a function-application term (F arg…) that denotes an entity —
(FruitFn AppleTree), (CapitalOf France), (QuantityFn 5 Meter). A stored sentence has
no first-class function terms; every stored token is atomic. NATs
are supported by reification, and functions split by declaration into two kinds.
(reifiable_function F) — object-denoting. A ground (F a…) is a reified NAT: it
reifies to an opaque nat/-namespaced constant K before it reaches the index,
so the reified NAT autoindexes exactly like a hand-minted symbol.(unreifiable_function F) — evaluated / interpreted. The application stays a
structural NAT — (QuantityFn 5 Meter) keeps its magnitude and
unit readable for a downstream prover; it is never minted.A reifiable NAT is replaced by an atomic constant on the write path, so:
(color K Red) keys [color K Red], K one token;sentex/index-terms is unchanged — K is an ordinary symbol subterm;Indexing nested compounds structurally is the alternative (defenses.md).
Nothing here is a KV side table. Every mapping is a normal sentex in
CxUniverse, so it rides put-sentex, the functor / argument roots, and the
inverted term index like any other fact.
| Fact | Meaning |
|---|---|
(reifiable_function F) / (unreifiable_function F) | F's kind — a predicate-metadata mark (vaelii.impl.taxonomy :reifiable / :unreifiable prop), belief-following like transitive/symmetric |
(natFormula K E) | the constant↔expression map: constant K denotes NAT expression E. The reverse (K → E) index; E → K is the inverted term index |
(rewriteOf T E) (compound E) | NAT E reifies to the existing real term T instead of a fresh constant |
(result F T) / (genlResult F T) | F's output types — materialized on mint as (T K) / (genl K T) |
(resultArg F n) | F's output is an instance of the type the application's argument n names — derived over each natFormula fact as (a_n K) (argtypes.md) |
(functionCorrespondingPredicate F P N) | F and P state one relationship: (F a…) = V exactly when P holds of a… with V at argument N |
natFormula and rewriteOf are quoting predicates (nat/nat-quoting-predicates = #{natFormula rewriteOf}): their expression argument is a verbatim NAT payload that
must not itself be reified or type-checked as a term.
(rewriteOf T E) overloads the equality/deprecation rewriteOf, discriminated by
shape: a symbol second argument is term equality (the equality partition — see
equality.md); a compound second argument is a NAT reify-to-term
declaration. The equality integrate arm and wff/equality-problems both skip the
compound shape, so it is stored as an inert quoting fact, never entering the closure.
reifiable_function and unreifiable_function describe two mechanisms — minted into a
constant, or left structural for a prover to compute. The criterion between them is
boundedness of the application space.
Reifying stores one opaque constant per distinct application and keeps it, so it is safe
exactly when the applications are bounded: (FatherFn Muffet) is one constant per animal,
and an AdultFn-shaped function one per individual. A function whose arguments range over
a continuous or open-ended domain is not, and takes unreifiable_function instead —
(QuantityFn 5 Meter), (QuantityFn 5.001 Meter) and every magnitude between them run
over the reals, so a constant apiece is a store nothing bounds. That is why QuantityFn
and QuantityIntervalFn are unreifiable, and why a measure function is never reifiable
however atomic its value reads: reifying (QuantityFn 5 Meter) would also hide the
magnitude and the unit a prover reads.
Both marks classify: (reifiable_function F) and (unreifiable_function F) each say F is a
function, which is what (disjoint function predicate) — derived from the partition
of relation — reaches, and (partition function reifiable_function unreifiable_function)
makes the two marks exclusive: a function is one or the other. The choice changes where a
declared result type is stored, not whether it holds — a reifiable application carries
result materialized on its constant, an unreifiable one is typed from the declaration at
check time, and the two say the same thing about the same function.
A function's kind is metadata cached in the taxonomy, so the per-sentence presence check —
"does the KB declare any function that reifies?" — is a free in-memory set read
(nat-read/any-reifiable-functions? ⇒ seq of the :reifiable props),
belief-following and needing no mtime cache. A KB that declares none pays one set read per assert / query for
the argument reify. The maintenance a minted constant owes (the orphan sweep, the
collision merge, the structural genlCx producer) reads nat/any-reified-constants?,
which adds one O(1) natFormula functor count when the set is empty, since a context
slot mints a cx/ constant with no declaration (context-nat.md).
assert runs maybe-reify-nats before expand-consequent, WFF and the constraint
checks:
(F a…) is replaced by its constant K
(an existing one via dedup, else a fresh mint) — inner args reified first, then the
outer NAT;modal_predicate's
proposition opaque. A stored (believes Ann (likes Tom (FruitFn Apple))) keeps the
application, and the read entry points leave it as written in a goal, so the belief
projection reifies it in the agent's context
(belief.md);exceptWhen's conjuncts, a
thereExists's binders — so it has no head predicate to hold opaque and no element
to skip. That is what puts an exception's query in the same spelling as the fact it
is about, and the cost of stopping at one is not a missing answer: an exception that
cannot be answered does not hold (exceptions.md), so the rule fires
unguarded and nothing says so;Reify-before-WFF is required. The raw compound (FruitFn AppleTree) in an
argument slot is not indexed, and disjoint-problem skips it — the term index never
posts the raw NAT's constituents, which would pollute it (sentex/index-terms descends
into ground compounds). The minted constant K carries the materialized result
types, so it is an atomic term every check reads like any symbol.
The argument checks do not skip it. args-problem and genls-problem read a
compound through its function's declared result — see Typing an application that is
never minted below, which is what makes
one declaration bind both classes of function.
mint-nat! allocates the opaque K, asserts (natFormula K E), materializes the
result types ((T K) per result, (genl K T) per genlResult), and returns
K, all at :monotonic strength — a reified NAT's identity and result types are structural,
not defeasible. The map is asserted with chaining off unless a resultArg of F is
declared (defenses.md). assert
stores synchronously, so a second occurrence of E in the same sentence dedups against
the first; a (rewriteOf T E) declaration short-circuits the mint to the real term T.
K is named by the content of E: constant-for hashes E with SHA-256, takes the
first 96 bits, and encodes them base62 behind a one-letter scheme tag — nat/a<17 base62> for an object NAT, cx/a… for a context one (nat-scheme-tag). So the same
expression reifies to the same constant in any process and after any rebuild, as the
skolem digest (skolem.md) names its witnesses. Two dumps that minted the same
NAT hold the same (natFormula K E) fact and merge by deduplication, and a re-mint after
an orphan sweep resolves to the constant it had before. The base62 digits keep K within
the argument naming convention (naming/argument-problem). The leading letter keeps the
name a readable token, since a digit-leading name is not one, and it versions the scheme:
a later hash or encoding change is nat/b…, and old constants keep their names
(defenses.md).
The forward chainer stores a rule's conclusion itself rather than through assert, and it
reifies the same way. chain/place-conclusion replaces every ground reifiable NAT in a
fired conclusion with its constant before it stores anything (reify-conclusion). A stored
rule holds no open application of a reifiable function (A rule or a goal that names an
open application), so a ground
application reaches a conclusion through a generator's generated rule, whose application
the generator's firing binds. The generated rule goes through this pass, so a ground
application in its antecedent is spelled with the constant the facts it matches are stored
under.
rewriteOf target, the
value its corresponding predicate names, or the minted constant — through
nat-read/reify-existing, which mints nothing.checks/*entry-mints?*, which reads the application as
the constant a mint would give it, the reading check uses (below). A conclusion those
checks drop is dropped with nothing minted, so no constant is left behind whose one use
was never stored. An admitted conclusion is minted by mint-nat!, and the placement
then runs its checks again over the reified sentence; that second pass draws the
argument-type entailments on the constant.assert's mint writes: the natFormula map, the materialized
result types and the correspondence projection, as premises in CxUniverse at
:monotonic. The constant's name is the expression's content, and its bookkeeping is
the same whichever path named the application first.core/violations as :mint-refused, with
the refusal's own type under :refusal. A firing has no batch to roll back, so the
bookkeeping the mint wrote before the refusal stays stored, and no removal names that
constant for the region sweep to collect. A correspondence projection whose argument
fails its predicate's arg declaration is not a refusal: the mint stores it and holds
it inert (argtypes.md),
and the conclusion stands. The mint
runs under *defer-settle?*, as a skolem witness's mint does (skolem.md):
the fixpoint settles once when it finishes.The derived conclusion is a use of the constant, and the bookkeeping does not rest on
the firing. The conclusion is justified like every other firing; the map and the result
types are premises. The map is one map: it says what the constant denotes, independent of
which firing named it, so it is stored in CxUniverse and belongs to no one derivation.
Which constant an expression resolves to depends on the merges the reader sees (Read path,
below). When the derived use goes — its antecedent retracted, or the settle's sweep
deleting what it solely supported — the removal reaches the orphan sweep through
integrate/*removed-sink* like any other removal (Rename and remove, below), and the
constant is collected once nothing but its own bookkeeping names it. An asserted use keeps
it, and a derived use keeps it after the asserted one goes. A re-derivation after a
collection mints the same name, so derive-then-assert, assert-then-derive and a derivation
retracted and restated all store the same sentences.
A backward proof mints nothing. prove and query store no conclusion. A backward
rule reads an application through its function's corresponding predicate, as a forward
rule does: (implies (bears ?t ?o) (grownIn (FruitFn ?t) ?o)) answers (grownIn K ?o)
from the (fruitOf AppleTree K) the mint of K stored, and answers nothing for an
application no constant and no value names.
A reified application arrives at the definitional checks as its constant, typed by the
(T K) / (genl K T) the mint materialized. An unreifiable function has no mint,
so its application stays a compound all the way to the checks — and a compound holds no
type membership and can hold none, a membership being asserted of a name.
So the argument checks read the function's declaration instead. (arg P n T) reads
(result F T') — what an application of F is — and (genlArg P n T) reads
(genlResult F T') — what it is a kind of. The two are never crossed.
(resultArg F n) adds to what an application is the type its own argument n names,
so nat/result-types takes the application rather than its function: (resultArg PickFn 1) types (PickFn dog) a dog and (PickFn cat) a cat. A minted constant takes the
same type as a derived (dog K), which the argument entailment draws over its
natFormula fact in every arrival order
(argtypes.md).
A term a prover hands back is minted no more than one somebody typed, and is no
orphan. (startOf (YearFn 2000) ?i) binds ?i to (InstantFn 2000 1 1 0 0 0), an
unreifiable NAT the calendar clock computed from the year's fields
(time.md) — and computing it writes nothing: no natFormula row, no
materialized result type, no handle, so there is no orphan question to ask about it and no
retraction that could take it back. It is a value in a binding map and lives exactly as
long as the answer does. Asserting a sentence that contains one is an ordinary assert,
and (result InstantFn time_point) in time.txt is what types it there — the same one
declaration binding the computed term and the typed one.
(v/assert kb '(unreifiable_function QuantityFn) 'CxUniverse)
(v/assert kb '(result QuantityFn measure) 'CxUniverse)
(v/assert kb '(arg needs_dog 1 dog) 'CxUniverse)
(v/assert kb '(needs_dog (QuantityFn 5 Meter)) 'CxUniverse)
;; refused: (QuantityFn 5 Meter) must be a dog — QuantityFn results in a measure
Four things fix what that reading is and is not.
(result QuantityFn measure) says every (QuantityFn m u) denotes a measure. Nothing computes
a type for one application, because there is nothing to compute: the term has no
membership and can acquire none.thing is
evidence the lattice cannot judge. Only a declared result that visibly reaches thing
and visibly fails to reach the demanded type convicts.CxUniverse, where every reader sees the result, and what a term
denotes is not a thing a reader may vary. nat/result-types and
genl-result-types carry both arities for exactly that split.(result F measure)
refuses the same sentence whether F is reifiable or unreifiable — through the constant
in the first case and through this reading in the second. On the assert path a
reifiable function's application never reaches this arm, since it is minted first.check reads a reifiable application as the constant assert would mint. check
writes nothing, so it mints nothing. An application that already has a term
(nat-read/reify-existing) is checked as that term. One that has none is read under
checks/*entry-mints?*, with its function's result types standing where the minted
constant's memberships would. Under assertive argument types (argtypes.md)
the demand then refuses only a result type the taxonomy separates from the demanded type,
with :disjoint, which is what the entailment assert draws over the constant refuses; any
other result type is admitted, as assert admits it and mints the demanded type. The
checks do not read what a rule would conclude of the new constant.
What an application is given is a separate reading from what it denotes: each input is checked against the function's own argument declarations, for a reifiable function before the mint replaces the application with its constant (argtypes.md).
A quoting predicate's argument is left alone: (natFormula K (FruitFn AppleTree))
and a compound-argument (rewriteOf T E) carry the expression as a verbatim payload
rather than as a term used in that position, so typing it by what the function yields
would type a quotation by its referent. That is also where the reading would otherwise
cost a mint something — mint-nat! writes one natFormula per constant.
A quoting function's argument is a mention as well. Quote and Quasiquote are the
quoting functions, fixed by the engine (sx/quoting-functors) rather than declared, so
no KB can add one or take one away. The reify pass does not reify a NAT nested in their
argument: (Quote (FruitFn Apple)) mints against the literal (FruitFn Apple), not
against that NAT's own constant, and a read resolves against the same literal. A
quotation names its syntax, and reifying the nested NAT would collapse two quotations
whose payloads' referents merge onto one mention. The argument is held opaque to an
identity merge in the congruence walk too (equality.md).
disjoint-problem is the check that still skips a compound. Its :opposing-handle is
the conflicting membership's handle — what settle weighs the pair by — and a result
declaration is not a membership of this application: pairing them in a nogood would let
one application's assertion defeat a claim about the whole function.
Before matching, a query goal's ground reifiable NATs are reified to their
existing constant (dedup, never mint). An unknown (never-minted) NAT resolves to
the reserved nat-read/no-match sentinel, which can never be a real constant — so an
unknown-NAT query returns empty without minting. no-match names no term: a literal
holding it as an argument is read by the stored-fact prover alone
(provers/applicable-provers), so (different (FooFn Xa Xb) Zed), (equals ?x (FooFn Xa Xb)) and (genl (FooFn Xa Xb) ?y) answer nothing. A positive equation goal
(res/equation?) reads a never-minted application as written
(nat-read/reify-existing), and the equality closure answers it by identity and congruence: (equals (FooFn Xa Xb) (FooFn Xa Xb)) holds, and (equals (FooFn Xa Xb) (FooFn Xc Xd)) holds only in a context that sees
(equals Xa Xc) and (equals Xb Xd).
It is wired at every read entry, and the enumeration is the whole of the guarantee:
sentexes-matching, ask, prove, query, the anytime ask-within /
prove-within, and levels 6 and 7 of the lookup stack (levels.md), which
are the two that claim to be the engine's own dispatch. One shared step
(quasiquote/prepare-goal-for-read) does it for all of them, because the failure mode when
an entry omits it is not a wrong answer but an empty one — the compound is matched
against a store that holds a symbol, and nothing comes back, which is
indistinguishable from a KB that was never told.
Two paths resolve a NAT the same way — dedup, never mint — without being query reads,
through nat-read/resolve-for-read, which answers nil when a NAT was never minted rather
than a sentence carrying the no-match sentinel. handle-of reads the constant ist
stored, so a lookup of the compound finds the stored sentex. assert-inert stores the resolved
sentence, so an inert record keys on the constant every read reifies to instead of a
compound no read finds, and refuses a NAT this KB never minted (:unminted-nat) — it
never mints, since a natFormula is a belief-carrying write this entry point does not do.
canonical-sentex resolves before it canonicalizes, so its content identity agrees with
handle-of; a NAT with no minted constant has no canonical stored form yet, and the
compound stands.
A read resolves an expression for the context it reads from, and a write for the context
it stores in (CxUniverse for a caller that names none). nat-read/map-rows reads the
map from every context, so a reader that does not see CxUniverse still finds the constant a mint
stored there. The merges applied to the expression are the ones the reader sees. A
natFormula row answers when its expression, normalized under the reader's merges, is the
expression's normal form there, and either the row is stated (a premise, superseded or
not) or the reader sees the row's context. A migration twin is not stated, so it answers
only where its merge is visible. The stated rows are probed once per spelling the reader's
equality classes give each symbol argument (class-spellings), one spelling when no
argument has merged. A compound (rewriteOf T E) target is read the same way
(rewrite-target). With (sameAs Apple Pomme) in CxUniverse, a reader that does not see
CxUniverse leaves (FruitFn Pomme) unresolved; with the merge in the reader's own
context, (FruitFn Pomme) resolves to the constant minted for (FruitFn Apple).
An ontology that reifies MotherFn usually also has motherOf, and the two are one
claim written twice. (functionCorrespondingPredicate F P N) says so: F maps
a₁ … a_M to V exactly when (P a₁ … a_{N-1} V a_N … a_M) holds. N is 1-based
over P's arguments; omit it and the value takes the last position, which is what
(functionCorrespondingPredicate MotherFn motherOf) means and the shape nearly every
correspondence has. A value in any other position needs the explicit form —
(functionCorrespondingPredicate StreetCornerFn streetCornerOf 1), so
(StreetCornerFn Xing North) is the Lot of (streetCornerOf Lot Xing North).
The example is the shipped one: resources/kb/upper/life.txt states motherOf and
fatherOf with MotherFn and FatherFn beside them, so a KB that loads the starter can
name somebody by their role before it knows their name.
It is read in both directions, and that is the point: a KB told only one of the two spellings can otherwise reason with only that one.
(motherOf Muffet Mary) reifies (MotherFn Muffet) to
Mary for a write or a read in a context that sees the fact. The expression names the
object the KB already has a name for rather than minting a second one beside it, so the
correspondence is a computed rewriteOf target — the same protocol, looked up through
the predicate instead of declared per expression. It is consulted before the dedup
probe, because a real term outranks a placeholder.(motherOf Muffet K), asserted with the rest of
K's bookkeeping and after the result types, since the projected literal is
arg-checked and K's types are what it is checked against. So the placeholder
answers motherOf's questions instead of being a term nothing says anything about.
The alternative — minting the constant and leaving the predicate unstated — makes the
placeholder invisible to every question the predicate answers.The two meet at the merge, and that is what makes the order stop mattering. Three things can arrive in any order — the application, the fact naming its value, the declaration — and each of the three landing last has an arm:
| Last to arrive | What happens |
|---|---|
| the application | reifies to the believed value; nothing is minted |
| the fact | (rewriteOf V K), stated in the fact's context, retires the placeholder there, and the equality migration folds every use of K — its natFormula map included — onto V |
| the declaration | each constant already minted for F is equated with its value in each context holding one, and projected when CxUniverse reads none |
A value applies where it is visible. The mint reads the values the corresponding facts
visible from the writing context name, each spelled under that context's merges
(nat-read/correspondence-value), and a read does the same from the reading context. A
fact stated in CxStory reifies (MotherFn Muffet) written there or below, while a write in
CxUniverse mints a placeholder. The placeholder is then retired in each context holding
a corresponding fact, once that context reads exactly one value beside it
(nat/retire-onto-values! after the mint), so CxStory reads the placeholder as Mary
and CxUniverse does not, in every arrival order. A merge's restatement of a
corresponding fact is no second value for a context that reads the original and the
restatement as one term.
The merge is a rewriteOf, so V represents the class
(defenses.md). A minted
constant is :opaque to wff's same-role check — the naming invariants are conventions
over names a person chose, and what a reified NAT denotes is settled by its materialized
result types — so merging one into an individual is the intended move, not the import bug
that check catches.
Several believed declarations for one function decide nothing at the mint. Two
correspondences are two different claims about what (F a…) denotes, and choosing
between them would have to key on a handle, which belief may never do — so neither is
read and the application mints as if none were declared. A rule and a goal read through
every one, which picks nothing (below). The same for a value: correspondence-value
answers only when the context reads exactly one, and a context reading two values beside
a placeholder retires it onto neither. The same for a rewriteOf target:
rewrite-target answers nil when the believed (rewriteOf T E) declarations name two
targets, and two declarations of one target are one answer.
The declaration is read through the index, not a taxonomy cache. It is consulted
once per NAT, where the reify is already probing for a rewriteOf target and a dedup,
and a KB declaring none pays one O(1) functor count per assert
(res/any-corresponding-predicates?). Nothing to integrate means nothing for recover
to rebuild — a correspondence works across a restart because the declaration is a
stored fact and always has been; recover holds the rules below again
(checks/force-stored!). It bites only for a reifiable_function: an undeclared
function's application is a raw compound the reify pass never visits.
The engine does not pattern-match a function application. res/kb-sentex, the
constructor every store and lookup builds a sentex through, respells a rule whose
antecedents or consequent hold an open application (F a…) of a reifiable_function
(res/respell-applications). The application becomes a variable ?v, and the literal
the correspondence makes equivalent to it, (P a… ?v) with ?v at the declared position,
joins the antecedents. Inner applications are respelled first, and one application
written twice is one variable:
(implies (tagged (FruitFn ?t)) (ripe ?t))
;; is stored as
(implies (and (fruitOf ?t ?fruit) (tagged ?fruit)) (ripe ?t))
(implies (bears ?t ?o) (grownIn (FruitFn ?t) ?o))
;; is stored as
(implies (and (bears ?t ?o) (fruitOf ?t ?fruit)) (grownIn ?fruit ?o))
An equals literal one of whose sides is an open application is the corresponding
literal itself, with the other side at the value position: (equals ?food (FruitFn ?t))
is (fruitOf ?t ?food), in a rule and in a goal, and searches no equality.
The variable is named for the function, its Fn suffix dropped and its first letter
lowercased, with a hash of the application appended where the rule uses the name already.
Canonicalization renames it with the rule's other variables, so the two spellings store
one handle, and why and the browser show the predicate form. The DFS prover, the node
engine and rete read the stored rule, so none of them reads an application. A forward rule
concluding about an application fires on the value its predicate names, a stated fact or
the projection a mint writes, and mints nothing.
A function with several believed correspondences gives the rule one spelling per
correspondence, and a rule applying several such functions one per combination
(res/rule-respellings). The row keeps the spelling that reads each function's
content-least correspondence, so both written spellings still store one handle. Each
other spelling is stored beside it, justified respell by the rule and the declarations
it reads (chain/sync-rule-respellings!), so the rule answers through the union of its
correspondences and a declaration leaving takes its spelling with it. A read picks no
correspondence, so the union is order independent.
A rule applying a function with no believed correspondence is stored as written and held
in the :out forced set (nat/held-application?, read by checks/forced-out?): it
fires nothing, and its application is never matched as written. A rule holding a
variable-functor application, (tagged (?fn ?t)), is held the same way
(What reification does not cover), except where the
compound sits in a sentence position (res/formula-position?). An application inside an unknown,
thereExists, forall, exists, ist or aggregate condition is not respelled, so a rule
holding one is held too. A quoting function's argument and a quoting predicate's payload
are mentions, neither respelled nor held. A generator's consequent rule is not read: the
rule it generates is respelled or held when it is stored. kb-integrity reports each
function a held rule applies with no correspondence
(integrity.md).
The rule follows the correspondence in both directions:
| The correspondence | The rule |
|---|---|
| arrives, the first believed | is respelled in place, leaves the :out set, and the settle joins it |
| arrives beside another | adds its spelling, which the settle joins; the row moves to the content-least spelling |
| leaves, another still believed | takes its spelling away, and the firings it made with it |
| leaves, the last believed | returns the row to its written spelling, held again |
assert records a respelled rule's written spelling on its row (integrate/spellings-key,
the record a permuting mark keeps), and the move back restores it. A row holding premise
assertions in two spellings splits, each assertion returning to its own spelling. The rows
are found as a reifiable mark's are (chain/reconcile-reified!), and through the antecedent
index of each predicate a declaration of the function names (nat/corresponded-rules).
A declaration arriving runs the move from nat-maintenance/reconcile-assert, and one
leaving runs it from collect-orphans!, so both arrival orders store the same rule.
A move that changes a rule's antecedents or its hold drops the firings the rule made in
the spelling it left, and a rule left believed fires again
(order_independence_test/a-late-reifiable-declaration-re-spells-a-stored-rule-and-withdraws-an-application-firing).
A rule that concluded (SkillFn ?x) before SkillFn was reifiable therefore keeps no
conclusion, and no constant, that the declaration arriving first would not have made.
The sentence positions a variable-functor rule's hold reads move the rule the same way. An
arg, argN or quotedArg declaration typed formula or under it, and a genl edge
putting a declared type under formula, stored or torn down, re-decide the rules with an
antecedent or a consequent on the declaration's predicate that hold a variable-functor
application (nat/formula-declared-predicates, nat/formula-position-rules). The move is
the row move above with the hold re-read (chain/reconcile-formula-positions!): a rule
left held keeps no firing, a rule left believed fires again, and a rule that also applies
a fixed function moves between its written and respelled spellings. (implies (holdsIn ?c (?p Rex)) (heardOf ?c ?p)) is held beside no declaration and believed beside (arg holdsIn 2 sentence), whichever arrives first
(nat_test/a-formula-declaration-releases-a-held-variable-functor-rule-in-every-order).
A goal is respelled before it is answered (res/goal-alternatives). A function with one
believed correspondence reads its predicate: prove (grownIn (FruitFn ?t) ?o) asks
[(fruitOf ?t ?fruit) (grownIn ?fruit ?o)], and its answers bind ?fruit too. A function
with several reads the declaration and a predicate variable, so the goal answers through
each correspondence and merges the answers:
(favoriteFood Pace (FruitFn ?tree))
;; with fruitOf and producesFruit both declared, asks
[(functionCorrespondingPredicate FruitFn ?fruitPredicate)
(?fruitPredicate ?tree ?fruit) (favoriteFood Pace ?fruit)]
A variable-functor application reads every function's declarations the same way:
(favoriteFood Pace (?fn AppleTree)) asks (functionCorrespondingPredicate ?fn ?fnPredicate), (?fnPredicate AppleTree ?fnValue) and (favoriteFood Pace ?fnValue),
and binds ?fn to the function. Declarations putting the value at different positions
are different literal shapes, so the goal runs one conjunction per distinct position and
merges their answers, each projected onto the variables every conjunction binds:
(owns Bob (?fn Xing North)) answers ?fn StreetCornerFn from
(functionCorrespondingPredicate StreetCornerFn streetCornerOf 1),
(streetCornerOf Lot Xing North) and (owns Bob Lot). A variable-functor compound in a
position an arg, argN or quotedArg declaration types as a formula
(res/formula-position?), or in a construct's argument, is a sentence pattern and is not
expanded: (believes Pace (?p Rex)) matches (believes Pace (dog Rex)). An and goal is
read as its conjuncts.
prove, provable?, query and their bounded forms merge the conjunctions. The readers
that report on one search, query-status, abduce, search-tree, compare-tacticians
and prove-within, refuse a goal that needs more than one with a :shape refusal
(quasiquote/prepare-conjunction-for-read). A goal applying a function with no
correspondence answers nothing: the application is replaced by nat-read/no-match. A
ground application in a goal keeps the
read path's reify, which resolves it to the constant, value or rewriteOf
target the KB holds for it; with a correspondence the respell reaches the same term
through the projection or the value's fact. ask reads one sentence and expands no rule,
and a stored fact holds a constant rather than an application, so an open application in
an ask goal finds nothing.
nat/expand-expression reverses the map, recursively rebuilding a reified constant
back to its functional expression — (color (FruitFn AppleTree) Red), never a raw
nat/ symbol. Non-reified NAT content is returned unchanged (same identity); only
reified NAT-bearing forms are rebuilt.
A constant is never what a reader sees. It is an implementation of term identity
— a nat/-namespaced hash is not a name anybody wrote — so a display layer resolves
it, and vaelii.core carries the pair that lets one: reified-term?, a pure test on the
reserved namespace that adds no work on a KB that has minted none, and
term-expression, one hop of the map. One hop rather than the whole expansion,
because a caller rendering each term individually — linking it, colouring it — recurses
and keeps every level addressable; expand-expression is the flat answer for a caller
that wants the form and not the parts. The browser does the former, showing the
expression with bold parens and the opening one linking to the constant's own page
(web.md, "A reified term is never shown as its constant").
Rename is an equality assert. (rewriteOf MalusTree AppleTree) retires
AppleTree; the equality migration (equality.md) restates every
sentex naming it, including (natFormula K (FruitFn AppleTree)), whose rewritten twin
is (natFormula K (FruitFn MalusTree)). K stays stable — it is not the term
renamed — so nested NATs referencing K need no cascade. A rename can collapse two
NATs onto one expression; merge-colliding-nats! (behind the reified-constant presence
check) restores the 1:1 invariant by merging each colliding group's constants into its
lexicographically-smallest survivor via a further equality, which migrates their uses.
A collision holds where a context sees both rows, so the repair runs per context:
merge-collisions! visits the contexts holding the rows most general first and states
each equality in the context that reads the collision, skipping a pair a visible equality
already merges. A merge stated in CxQ joins (FruitFn AppleTree) and
(FruitFn MalusTree) in CxQ alone, and CxUniverse keeps the two constants apart.
Three writes can join a collision, and each reads only the rows it can have joined: an
equality reads the rows naming its terms' classes, a mint's natFormula the rows naming
its expression's merged arguments, and a genlCx edge the rows its migration restated
below its lower context. A collision an import stored stays until a caller asks
colliding-constant-groups
(defenses.md).
The retired spelling stays a usable question: a goal naming the old term
goal-rewrites to the new expression and still resolves to K.
The invariant holds per reify namespace. An expression written in a context slot maps
to a cx/ constant beside the nat/ one its argument-position use maps to, and every
E → K read and the collision grouping take the namespace they want
(context-nat.md).
A collision can also run the other way — one constant mapped to two expressions — and
until the repair reaches it, every reader of the map takes the same one: the
content-least (nat/authoritative-expression, the choice dedup-constant makes on the
other side of the map). That is what keeps the orphan sweep coherent: orphan? decides
orphanhood against the expression bookkeeping-handles then computes the retraction set
from, so no verdict about one expression retracts records belonging to another.
Remove is retraction. When the last stored use of a reified NAT goes, its natFormula map
and materialized types would dangle a raw nat/ symbol — so remove-orphaned-nats!
(run after retract! and edit! behind the reified-constant presence check, suppressed
while already removing orphans)
collects every constant whose only remaining stored sentexes are its own bookkeeping.
Stored, not believed: a use sitting OUT revives when the defeat above it lifts, and an
inert use (a labeling's choice head) has no TMS node at all — either would dangle if a
sweep counted only belief, and re-reifying the expression would mint a second constant
beside the first. A
correspondence projection is bookkeeping for this: like a result type it states what
the constant is, and counting it as a use would make every placeholder immortal.
Bookkeeping is decided by authorship, not by shape. K's own sentexes are its
natFormula map plus exactly what mint-nat! wrote about it, and nat/minted-for
re-derives that set the way the mint derived it: (T K) for each believed (result F T), (genl K T) for each (genlResult F T), F being the function of the expression
K maps to, and the correspondence projection. A record the argument-type entailment
derives off K's own sentexes alone is K's own as well (nat/entailed-from?), and
leaves with them. Two such records are a membership an argument declaration on
natFormula or a resultArg of F derives off the map, and the (predicate K) the
declaration on genl derives off a materialized (genl K T). The test follows the
source of each justification, so a record entailed off such a record is K's own too;
a record with one justification resting on a use, or a rule's conclusion, is a use.
Everything else naming K is somebody's
assertion whatever its arity — (prime K) is a claim about K exactly as (noted Author K) is, and a sweep reading arity alone would retract the claim along with the constant.
The set is computed behind a delay, and the natFormula clause is tested first: a
constant a teardown collects has its map and nothing else left, so the common answer is
reached without reading the declarations at all. The one constant this keeps
alive that a shape test would have collected is one whose result declaration was
retracted after the mint: the materialized (T K) is then a believed sentence no rule
supports and nobody has withdrawn, and holding K for it is the direction to err in.
The answer is realized before the caller acts on it. bookkeeping-handles decides
membership by re-reading K's natFormula, and its caller retracts that map. A lazy
answer read after the map's retraction calls every later sentex "not bookkeeping" and
leaves it stored, naming a collected constant, in the term-index orders that yield the
map first. Both the per-constant set and the sweep's per-round orphan list are realized
before the round's first retraction.
The sweep asks about the region the teardown removed, not about the KB. A constant
becomes an orphan only when something that referenced it goes, so the candidates are the
constants the departing sentexes named (orphans-named-by), and each is settled by one
inverted-term-index read — orphan?, since a constant's uses, its map and its
materialized types are all sentexes naming it (indexing.md). What a
retraction costs is the size of what it removed, and a KB that has minted a hundred
thousand NATs the retraction is not about adds nothing to it.
A cx/ context constant is collected by the same sweep, with its extent as one more
source of liveness: orphans-named-by reads a removed sentex's context beside its
sentence, and orphan? reads the extent, one O(1) count-in-context, before the term
index (context-nat.md).
The removals reach the sweep through integrate/*removed-sink*, the record the removal
choke point fills while a teardown runs, because they arrive from three places: the
dependency-directed sweep; the settle that follows it, where an exception that starts
holding blocks a justification and what it solely supported is deleted
(exceptions.md); and the orphan sweep's own retractions. The third is
how the region grows with the fixpoint — removing an orphan removes the natFormula
sentex holding its expression, so a reified NAT nested in that expression is a candidate
on the next round. A cascade is therefore found by the rule that found the first orphan,
and the loop ends on the round that removes nothing.
preview's rollback is the one caller that asks the whole KB instead
(orphaned-constants): the batch it undoes runs with the settle sweep off
(preview.md) and reaches the orphan sweep at no point, so the claim it owes
— the KB is as it was found — is about all of it rather than about one teardown's region.
The write path spells a sentence by the marks believed when it is written, so a
(reifiable_function F) mark that starts or stops holding after sentences naming F are
stored changes how those sentences would be written. The settle that follows the move
re-spells them (chain/reconcile-reified!), so the store holds what a KB told the same
sentences with the mark already in place holds:
| The mark | What the settle re-spells |
|---|---|
| arrives: asserted, derived, or revived from OUT | each stored ground application of F becomes its term, minted as assert mints it |
| leaves: retracted, or OUT | each use of a constant minted for F names the application again |
| is defeated or excepted at or above a use's context, so no reader of the use believes it | the use is spelled as written, and its constant is collected |
| is defeated or excepted below a use's context, so the use's readers disagree | the use stays as written, and the reified use is stored beside it, justified respell by the use and the mark |
The move is noted where the mark changes in the taxonomy (special/note-permuting-moves!,
beside the permuting marks), on the :respell queue the settle drains. The region is read
off the inverted term index (nat/respell-region): every stored sentex holding an
application of F, and every use of a constant whose expression holds one, at any
nesting. A constant's own bookkeeping is not a use and does not move. A quoting
predicate's payload is a mention and does not move either. Each row is re-spelled by
expanding its constants and reifying again (nat/respelled), which is the write path's
own walk. A rule's antecedent and consequent move the same way, and a rule holding an open
application of F is respelled through F's correspondence or held
(A rule or a goal that names an open application).
integrate/move-row!, the move a late symmetric
mark makes). Otherwise it folds into that row. A re-asserted use therefore dedups to
the moved row instead of storing a second one.integrate/take-out!.A map that leaves while uses still name its constant re-spells those uses. The region
walk reaches a constant only through its stored natFormula map, so a map retracted
before the mark would leave its uses spelled with a constant nothing expands. The teardown
that removes the map reads the expression off its removal record and re-spells each
remaining use, and each use of a constant whose expression names the departed one, with
the departed constant written as that expression (chain/reconcile-stranded!, run from
nat-maintenance/collect-orphans! before the orphan sweep). Under a believed mark the
use keeps its spelling and the constant is minted again, map included, under a new
handle. With the mark gone the use names the application. The mark and its maps
therefore leave the same store in any retraction order.
A reader that does not believe the mark reads no row naming a constant minted for F,
the mint and its result types included, and a reader that believes it reads no row holding
an application of F unreified (res/without-unbelieved-spellings). A goal is reified
with the marks its reader believes (nat-read/maybe-reify-for-read given the reader). The
readers are found as for a permuting mark
(canonicalization.md), and a write
naming such an application queues the function for the settle (nat/queue-split-uses!).
The settle reaches stored rows, believed or not, so a use sitting OUT is spelled as the KB
spells it when its defeat lifts. A declaration written before any application finds only
its own declarations about F, and a KB declaring no reifiable function queues nothing.
A store recovered from rows written before this re-spelling existed keeps them: recover
re-spells nothing, and retracting the declaration and asserting it again runs the sweep.
A (result F T) or (genlResult F T) asserted after constants were minted for F
materializes (T K) or (genl K T) on each of them, as the mint does when the declaration
comes first (nat/reconcile-nats!).
vaelii.impl.nat-read — below provers, so BeliefProjectionProver calls it: the
detectors (reified-nat-symbol?, reifiable-function?, reifiable-ground-nat?), the
E → K lookups (dedup-constant, rewrite-target, correspondence-value /
corresponding-literal), the shared reify walk (reify-in) and the read mode
(maybe-reify-for-read, reify-existing, resolve-for-read). Reads through
resolution and reads.vaelii.impl.nat — held-application?, the lookups nat-expression, result-types /
genl-result-types and corresponded-rules, expand-expression, the write mode
(maybe-reify-nats, mint-nat!), and the rename / remove / correspondence maintenance — the orphan questions among it
(orphan? per constant, orphans-named-by over a region, orphaned-constants over
the KB, reified-nats-in for the candidates) and reconcile-nats!, the collision
merge and the correspondence in the order the assert path runs them. Reads the store,
taxonomy and belief directly, and reaches assertion through wiring/assert-sentence.vaelii.impl.resolution — the correspondence reads (correspondence-of,
believed-correspondences) and the respell of a rule's and a goal's open applications
(respell-applications, which kb-sentex runs, and respell-goal-applications).vaelii.impl.nat-maintenance — the sequencing the write paths run around that:
reconcile-assert once a sentence is stored (reconcile-nats!, the rules a
correspondence declaration respells, then the structural genlCx edges the fact entails
and the merges those edges license) and collect-orphans! on the retract! and edit!
sweeps, which respells the rules a removed declaration respelled and loops
remove-orphaned-nats! to a fixpoint. The teardown entry point is an argument, so the
engine requires nothing above it.vaelii.core — the reify call sites: the write-path reify at the head of assert,
the read-path reify at the query entries, and one call into
vaelii.impl.nat-maintenance per maintenance site.vaelii.impl.chain — reify-conclusion, the derivation-path reify place-conclusion
runs on a fired conclusion, with the checks asked before the mint. It runs only when
nat/names-reifiable-nat? holds, a walk that rebuilds nothing. Also reconcile-reified!, the
settle's re-spelling when a reifiable mark or a correspondence moves.vaelii.impl.integrate — *removed-sink*, the removal choke point's record of what a
teardown took away, which is the region the orphan sweep runs over.vaelii.impl.special — the two function-kind prop marks, the correspondence's
wff-only entry, and the equality-arm skip for a compound-arg rewriteOf.vaelii.impl.checks — convicting-result-type, the arm args-problem and
genls-problem read a compound argument through (argtypes.md), and the
forced-out? arm that holds a rule nat/held-application? accepts.vaelii.impl.quasiquote — prepare-conjunction-for-read, the goal respell.vaelii.impl.wff — function-decl-problems, correspondence-problems, the
:opaque role a minted constant carries through the same-role check, and the
equality-problems waiver for a compound-arg rewriteOf.resources/kb/upper/core.txt — the seven NAT predicates, declared and documented.functionCorrespondingPredicate, a rule applying the function is held inert and a goal
applying it answers nothing
(A rule or a goal that names an open application).
An application inside an unknown, thereExists, forall, exists, ist or
aggregate condition is held with one too.except, moves no rule,
and the respell reads the reifiable mark unscoped, so a reader that does not believe the
mark reads the rule respelled.(?fn a…) outside a
sentence position is held inert and fires nothing; only a goal expands one.genl edge is stored
or torn down. A declaration a rule derives re-decides no rule as it arrives, and one
hidden from a reader by an except re-decides none.(likes ?x (?f Bob)) reads only
the declared correspondences, so a structural application of an undeclared function
stored as a compound term does not answer it.unreifiable_function's application is computed, not reified. A rule matches it
as written, and the respell does not read it.CxUniverse reads no collision repair. Its reads
resolve an expression to the content-least constant it reads (A NAT resolves under the
reader's merges), and the uses of the other constant do not answer there.class-spellings varies the symbol arguments at the top level, so a reader that does
not see CxUniverse does not resolve (Quote (foo Muffet)) through a rename of
Muffet stated in a context it sees.(motherOf Muffet Mary) in CxA and (motherOf Muffet Maria) in CxB, a context
seeing both reads the placeholder as Mary and as Maria, so it reads the two as one
term.rewriteOf target, a correspondence value and a placeholder an equality
retired stand where a KB that never declared the function holds the application.The measure-evaluating quantity prover — measure comparison over a dimensionOf /
conversionFactor table — reads the structural measures an unreified application keeps. It lives
in quantity.md.
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |