The read-mode reify of a ground NAT: the reserved namespaces, the reifiable_function
mark, the natFormula and correspondence lookups a reader or writer in a context
resolves an application through, and the walk both reify modes share. Below provers,
so the belief projection reifies a proposition in the agent's context. See docs/nat.md.
The read-mode reify of a ground NAT: the reserved namespaces, the `reifiable_function` mark, the `natFormula` and correspondence lookups a reader or writer in a context resolves an application through, and the walk both reify modes share. Below `provers`, so the belief projection reifies a proposition in the agent's context. See docs/nat.md.
True while nat/mint-nat! stores a constant's bookkeeping: its asserts queue nothing,
and the mint queues the constant once its bookkeeping is stored.
True while `nat/mint-nat!` stores a constant's bookkeeping: its asserts queue nothing, and the mint queues the constant once its bookkeeping is stored.
{f entries}: while bound, sorted-expression sorts an application of each key f by
the symmetric and commuting marks of f its entries list (res/mark-entries' keys)
and no others, the marks one reader believes (sorted-by-at), so the reconcile stores,
and a read looks up, the constant that reader names the application by.
`{f entries}`: while bound, `sorted-expression` sorts an application of each key `f` by
the `symmetric` and commuting marks of `f` its `entries` list (`res/mark-entries`' keys)
and no others, the marks one reader believes (`sorted-by-at`), so the reconcile stores,
and a read looks up, the constant that reader names the application by.The reifiable_function functions whose ground applications stay as written while
bound: the ones a reader does not believe the mark of (withheld-at), so the reconcile
stores, and a read looks up, the spelling that reader reads (chain/reconcile-reified!).
The `reifiable_function` functions whose ground applications stay as written while bound: the ones a reader does not believe the mark of (`withheld-at`), so the reconcile stores, and a read looks up, the spelling that reader reads (`chain/reconcile-reified!`).
(any-reifiable-functions? kb)Does the KB declare a reifiable_function? One in-memory taxonomy prop read. False
means no sentence holds a reifiable NAT, and every reify pass returns its input.
Does the KB declare a `reifiable_function`? One in-memory taxonomy prop read. False means no sentence holds a reifiable NAT, and every reify pass returns its input.
(any-result-declarations? kb)Does the KB declare any result, genlResult or resultArg? Three O(1) functor
counts.
Does the KB declare any `result`, `genlResult` or `resultArg`? Three O(1) functor counts.
(computed-genlCx-edge? kb sx)Is sx a genlCx edge the structural producer computed: not a premise, and every
support under the contextArgSubrelation informant (docs/context-nat.md, Orphan
collection)? Belief is not read. The orphan sweep reads such an edge as the engine's
own wiring, and a declaration's sweep over stored facts draws nothing from it
(special/entail-existing).
Is `sx` a `genlCx` edge the structural producer computed: not a premise, and every support under the `contextArgSubrelation` informant (docs/context-nat.md, Orphan collection)? Belief is not read. The orphan sweep reads such an edge as the engine's own wiring, and a declaration's sweep over stored facts draws nothing from it (`special/entail-existing`).
Reserved namespace of a context reified constant, which a ground application in a sentex's context slot mints, whatever is declared about its head (docs/context-nat.md).
Reserved namespace of a context reified constant, which a ground application in a sentex's context slot mints, whatever is declared about its head (docs/context-nat.md).
(correspondence-value kb E context)(correspondence-value kb E context write?)The term a :monotonic corresponding fact visible from context (CxUniverse when nil)
names as the value of the ground NAT expression E, spelled under context's merges,
when the visible facts name that one value and no other, or nil. Where the
corresponding predicate is not_assertible, a mark read KB-wide as assert's refusal
reads it, the value is the prover registry's (computed-value). With write?, only
that prover value: a write names the application's own constant, which a stored value
reaches through chain/sync-values!'s merge (docs/nat.md, The corresponding predicate).
The term a `:monotonic` corresponding fact visible from `context` (CxUniverse when nil) names as the value of the ground NAT expression `E`, spelled under `context`'s merges, when the visible facts name that one value and no other, or nil. Where the corresponding predicate is `not_assertible`, a mark read KB-wide as `assert`'s refusal reads it, the value is the prover registry's (`computed-value`). With `write?`, only that prover value: a write names the application's own constant, which a stored value reaches through `chain/sync-values!`'s merge (docs/nat.md, The corresponding predicate).
(dedup-constant kb E)(dedup-constant kb E ns context)(dedup-constant kb E ns context write?)The existing reified constant for the ground NAT expression E in reify namespace ns
(default nat/) for a reader in context (CxUniverse when nil), or nil: the
natFormula rows map-rows reads. Where several constants map E in one namespace
(an import restores what the dump held, or a merge the reader sees joins two
expressions), the lexicographically smallest, the survivor group-collisions elects.
With write?, a nat/ expression answers only a reified constant, never a term a
merge's twin of the map names: a write names the application's own constant.
The existing reified constant for the ground NAT expression `E` in reify namespace `ns` (default `nat/`) for a reader in `context` (CxUniverse when nil), or nil: the `natFormula` rows `map-rows` reads. Where several constants map `E` in one namespace (an import restores what the dump held, or a merge the reader sees joins two expressions), the lexicographically smallest, the survivor `group-collisions` elects. With `write?`, a `nat/` expression answers only a reified constant, never a term a merge's twin of the map names: a write names the application's own constant.
(existing-term kb E ns context)(existing-term kb E ns context write?)The term ground NAT expression E already resolves to in reify namespace ns for a
reader in context, or nil: a rewriteOf target, the value its corresponding
predicate names where context reads it (correspondence-value), else the constant
dedup-constant finds. With write?, the term a write in context stores: the
value and the constant as correspondence-value and dedup-constant read them for a
write. A context slot (cx/) takes no correspondence value, which names an object.
The term ground NAT expression `E` already resolves to in reify namespace `ns` for a reader in `context`, or nil: a `rewriteOf` target, the value its corresponding predicate names where `context` reads it (`correspondence-value`), else the constant `dedup-constant` finds. With `write?`, the term a write in `context` stores: the value and the constant as `correspondence-value` and `dedup-constant` read them for a write. A context slot (`cx/`) takes no correspondence value, which names an object.
(fact-constants kb sentence)The constants minted for the applications the positive literal sentence names a value
of under each stored correspondence declaration of its functor, read off the map
(dedup-constant).
The constants minted for the applications the positive literal `sentence` names a value of under each stored correspondence declaration of its functor, read off the map (`dedup-constant`).
(in-namespace? ns k)Does the term k a natFormula map names belong to reify namespace ns? A context
slot's constant is a context (nm/context?), and an argument's is any other term.
Does the term `k` a `natFormula` map names belong to reify namespace `ns`? A context slot's constant is a context (`nm/context?`), and an argument's is any other term.
(maybe-reify-for-read kb sentence context)(maybe-reify-for-read kb sentence context write?)Reify every reifiable ground NAT subterm of a query sentence to its existing term for
a reader in context (CxUniverse when nil), never minting; a never-minted NAT resolves
to no-match, except a quoting application, which stays as written. With write?,
each resolves to the term a write in context stores (read-leaf), the reading a
lookup of a stored sentex takes. An application of a function context does not
believe reifiable stays as written (withheld-at), and an application of a function
whose permuting marks some reader does not believe is sorted by the ones context
believes (sorted-by-at).
Reify every reifiable ground NAT subterm of a query `sentence` to its existing term for a reader in `context` (CxUniverse when nil), never minting; a never-minted NAT resolves to `no-match`, except a quoting application, which stays as written. With `write?`, each resolves to the term a write in `context` stores (`read-leaf`), the reading a lookup of a stored sentex takes. An application of a function `context` does not believe reifiable stays as written (`withheld-at`), and an application of a function whose permuting marks some reader does not believe is sorted by the ones `context` believes (`sorted-by-at`).
Reserved namespace of an object reified constant, which a ground application of a
(reifiable_function F) in argument position mints.
Reserved namespace of an object reified constant, which a ground application of a `(reifiable_function F)` in argument position mints.
The reserved constant a read-mode reify resolves a never-minted NAT to (sx/no-match).
The reserved constant a read-mode reify resolves a never-minted NAT to (`sx/no-match`).
(note-values kb sentences uses?)Queue on :respell what the stored, removed or relabelled sentences move the
values of: [:valued-fn f] for a correspondence declaration of f, [:valued k] for
each constant a corresponding fact names a value of (fact-constants) and for each
constant minted for the expression of a compound rewriteOf, and with uses? for each
constant a sentence names whose function is declared or whose expression a compound
rewriteOf names (valued-constants). Answers whether it queued anything. The
correspondence arms are behind values-reachable?, a use's rewriteOf arm behind
rewrites-reachable?, read once and only for a use naming a reified constant; nothing
while *minting?*.
Queue on `:respell` what the stored, removed or relabelled `sentences` move the values of: `[:valued-fn f]` for a correspondence declaration of `f`, `[:valued k]` for each constant a corresponding fact names a value of (`fact-constants`) and for each constant minted for the expression of a compound `rewriteOf`, and with `uses?` for each constant a sentence names whose function is declared or whose expression a compound `rewriteOf` names (`valued-constants`). Answers whether it queued anything. The correspondence arms are behind `values-reachable?`, a use's `rewriteOf` arm behind `rewrites-reachable?`, read once and only for a use naming a reified constant; nothing while `*minting?*`.
(reifiable-entries kb f){[:prop :reifiable f] {handle context}}, the reifiable_function mark of f and its
supporters, in res/mark-entries' shape.
`{[:prop :reifiable f] {handle context}}`, the `reifiable_function` mark of `f` and its
supporters, in `res/mark-entries`' shape.(reifiable-function? kb head)True iff head reifies its ground applications in argument position: a believed
(reifiable_function head), and head not in *withheld*. The mark is read
unscoped; a reader that does not believe it binds *withheld*.
True iff `head` reifies its ground applications in argument position: a believed `(reifiable_function head)`, and `head` not in `*withheld*`. The mark is read unscoped; a reader that does not believe it binds `*withheld*`.
(reifiable-ground-nat? kb form)True iff form is a ground (F …) whose head is a reifiable function: a NAT the
argument-position reify mints to a nat/ constant.
True iff `form` is a ground `(F …)` whose head is a reifiable function: a NAT the argument-position reify mints to a `nat/` constant.
(reified-context-symbol? term)True iff term is a reified context constant, a symbol in cx/.
True iff `term` is a reified context constant, a symbol in `cx/`.
(reified-nat-symbol? term)True iff term is a reified constant: a symbol in nat/ or cx/.
True iff `term` is a reified constant: a symbol in `nat/` or `cx/`.
(reified-object-symbol? term)True iff term is a reified object constant, a symbol in nat/.
True iff `term` is a reified object constant, a symbol in `nat/`.
(reify-existing kb sentence context)(reify-existing kb sentence context write?)Reify every reifiable ground NAT subterm of sentence that has an existing term for a
reader in context (CxUniverse when nil) to that term, and leave every other one as
written. With write?, the existing term a write in context stores
(existing-term). Never mints. vaelii.core/check and a firing's conclusion read a
sentence through this with write? (docs/nat.md, Typing an application that is never
minted).
Reify every reifiable ground NAT subterm of `sentence` that has an existing term for a reader in `context` (CxUniverse when nil) to that term, and leave every other one as written. With `write?`, the existing term a write in `context` stores (`existing-term`). Never mints. `vaelii.core/check` and a firing's conclusion read a sentence through this with `write?` (docs/nat.md, Typing an application that is never minted).
(reify-in kb s nat-fn)(reify-in kb s nat-fn head-fn)Reify every reifiable ground NAT subterm of literal/sentence s, calling nat-fn (a
(fn [kb form])) at each one, and head-fn (default nat-fn) at a literal's head that
is one; each returns the NAT's term, having reified its nested NAT arguments itself. A
symbol head, a quoting-predicate argument and a modal_predicate's proposition
(res/attitude-application?) stay opaque. The modal mark is read KB-wide, once per
walk: whether an argument is a mention is a fact about the sentence
(tax/mention-marks). A vector is descended element by element (docs/nat.md, Write
path).
Reify every reifiable ground NAT subterm of literal/sentence `s`, calling `nat-fn` (a `(fn [kb form])`) at each one, and `head-fn` (default `nat-fn`) at a literal's head that is one; each returns the NAT's term, having reified its nested NAT arguments itself. A symbol head, a quoting-predicate argument and a `modal_predicate`'s proposition (`res/attitude-application?`) stay opaque. The modal mark is read KB-wide, once per walk: whether an argument is a mention is a fact about the sentence (`tax/mention-marks`). A vector is descended element by element (docs/nat.md, Write path).
(reify-nat-for-read kb form ns context)(reify-nat-for-read kb form ns context write?)Read-mode leaf: reify nested NAT arguments, then resolve the expression, in its
sorted-expression order, to its existing term in reify namespace ns for a reader in
context (existing-term, with write? as a write in context stores it), or to
no-match. Never mints. A quoting function's argument stays opaque, as
reify-or-mint-nat holds it.
Read-mode leaf: reify nested NAT arguments, then resolve the expression, in its `sorted-expression` order, to its existing term in reify namespace `ns` for a reader in `context` (`existing-term`, with `write?` as a write in `context` stores it), or to `no-match`. Never mints. A quoting function's argument stays opaque, as `reify-or-mint-nat` holds it.
(resolve-for-read kb sentence context)(resolve-for-read kb sentence context write?)The read-mode reify of sentence for a reader in context (maybe-reify-for-read,
with write? as given) when every reifiable NAT in it has a stored term, else nil.
The read-mode reify of `sentence` for a reader in `context` (`maybe-reify-for-read`, with `write?` as given) when every reifiable NAT in it has a stored term, else nil.
(result-arg-types E ns)The symbols application E holds at the positions ns its function's (resultArg F n) declarations name. A position E lacks, or a non-symbol there, names no type.
The symbols application `E` holds at the positions `ns` its function's `(resultArg F n)` declarations name. A position `E` lacks, or a non-symbol there, names no type.
(rewrite-target kb E ns context)The real term T a (rewriteOf T E) a reader in context (CxUniverse when nil)
reads (map-rows) reifies NAT expression E to, spelled under context's merges, or
nil. Nil when the declarations name more than one target (docs/nat.md, The
corresponding predicate), and when the one T lies outside reify namespace ns
(in-namespace?). Every row map-rows reads is a stored rewriteOf, so a KB storing
none answers nil off one functor count, before E is normalized and spelled.
The real term `T` a `(rewriteOf T E)` a reader in `context` (CxUniverse when nil) reads (`map-rows`) reifies NAT expression `E` to, spelled under `context`'s merges, or nil. Nil when the declarations name more than one target (docs/nat.md, The corresponding predicate), and when the one `T` lies outside reify namespace `ns` (`in-namespace?`). Every row `map-rows` reads is a stored `rewriteOf`, so a KB storing none answers nil off one functor count, before `E` is normalized and spelled.
(rewrites-reachable? kb)Can a compound rewriteOf reach a minted constant: does the KB declare a reifiable
function and store a rewriteOf and a natFormula map? One set read, then two O(1)
functor counts.
Can a compound `rewriteOf` reach a minted constant: does the KB declare a reifiable function and store a `rewriteOf` and a `natFormula` map? One set read, then two O(1) functor counts.
(sorted-by-at kb reader)The *sorted-by* binding that names an application as reader names it: each
reifiable function some reader does not believe a permuting mark of
(res/split-mark-entries), with the marks reader believes. Empty for a variable or
nil reader. The reifiable_function mark is read unscoped, a superset of the
functions reader names an application of, and a function it does not believe
reifiable is withheld (withheld-at) before its marks are read.
The `*sorted-by*` binding that names an application as `reader` names it: each reifiable function some reader does not believe a permuting mark of (`res/split-mark-entries`), with the marks `reader` believes. Empty for a variable or nil `reader`. The `reifiable_function` mark is read unscoped, a superset of the functions `reader` names an application of, and a function it does not believe reifiable is withheld (`withheld-at`) before its marks are read.
(sorted-expression kb E)Ground application E with its own arguments in the order its symmetric and
commuting marks give it (sx/permute-args, permuting-marks): the expression a reified
constant is named by and found under, so both spellings of a commuted application name
one constant. The associative, idempotent and meet arms are not applied, since they can
collapse an application to one argument.
Ground application `E` with its own arguments in the order its `symmetric` and commuting marks give it (`sx/permute-args`, `permuting-marks`): the expression a reified constant is named by and found under, so both spellings of a commuted application name one constant. The associative, idempotent and meet arms are not applied, since they can collapse an application to one argument.
(split-reifiable? kb f)Does some reader not believe f's stored reifiable_function mark
(res/uniform-marks?)?
Does some reader not believe `f`'s stored `reifiable_function` mark (`res/uniform-marks?`)?
The context every NAT bookkeeping fact is stored in.
The context every NAT bookkeeping fact is stored in.
(values-reachable? kb)Can a corresponding fact reach a minted constant: does the KB declare a reifiable
function (any-reifiable-functions?) and store a correspondence declaration and a
natFormula map? One set read, then two O(1) functor counts.
Can a corresponding fact reach a minted constant: does the KB declare a reifiable function (`any-reifiable-functions?`) and store a correspondence declaration and a `natFormula` map? One set read, then two O(1) functor counts.
(visible-result-targets kb pred head context)The distinct arg2s of the believed (<pred> head ?t) facts visible from context
(res/matches-visible), as a check and a goal read a declaration (docs/nat.md, Typing
an application that is never minted).
The distinct arg2s of the believed `(<pred> head ?t)` facts visible from `context` (`res/matches-visible`), as a check and a goal read a declaration (docs/nat.md, Typing an application that is never minted).
(visible-result-types kb head context)Types T with a (result head T) visible from context: what an application of
head is an instance of. Given an application (head a…) in place of head, adds the
argument at each position a visible (resultArg head n) declares, behind one O(1)
functor count.
Types `T` with a `(result head T)` visible from `context`: what an application of `head` is an instance of. Given an application `(head a…)` in place of `head`, adds the argument at each position a visible `(resultArg head n)` declares, behind one O(1) functor count.
(withheld-at kb reader)The reifiable functions reader does not believe the mark of while another reader
does, as a set: what *withheld* holds to spell a sentence as reader reads it.
Empty for a variable or nil reader.
The reifiable functions `reader` does not believe the mark of while another reader does, as a set: what `*withheld*` holds to spell a sentence as `reader` reads it. Empty for a variable or nil `reader`.
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 |