The KB half every calculus over vaelii.impl.qcn shares: a calculus value
(calculus), the believed facts of one reader context read into a resident network,
the passes over it, entailment and refutation as prover solutions, the support an
entailment rests on, and the delta a forward re-join runs over. See docs/qcn.md.
The KB half every calculus over `vaelii.impl.qcn` shares: a calculus value (`calculus`), the believed facts of one reader context read into a resident network, the passes over it, entailment and refutation as prover solutions, the support an entailment rests on, and the delta a forward re-join runs over. See docs/qcn.md.
(calculi-triggered-by kb pred)Every registered calculus one of whose :trigger-predicates is pred or a
super-predicate of it by the global genls closure, or nil. Every one, not the first:
one predicate can move two networks. A caller holding (genl sub super) asks it of
super.
Every registered calculus one of whose `:trigger-predicates` is `pred` or a super-predicate of it by the global `genls` closure, or nil. Every one, not the first: one predicate can move two networks. A caller holding `(genl sub super)` asks it of `super`.
(calculus nm algebra denotation)(calculus nm algebra denotation narrowing)(calculus nm algebra denotation narrowing typed)Bundle an algebra and its vocabulary into the value every function here takes.
denotation maps each stored predicate to the set of base relations it denotes, so its
keys are the predicates the prover claims.
narrowing is the optional second reader — nil for a calculus that has none:
{:fn (fn [kb context] → {:net … :support …} | nil)
:over-nodes (fn [nodes] → {:net … :support …} | nil)
:node? which terms are nodes, when not every node is a symbol
:bindings the dynamic vars :fn reads, whose values key the resident network
:sources every predicate whose arrival or departure moves what it answers
:contexts the subset that puts a NODE in the network, so names a reader context}
:over-nodes reads only the node set, so with-goal-nodes runs it over a goal's nodes
too. Either key may be absent. :sources and :contexts are folded into
:trigger-predicates and :context-predicates here, once.
typed is the predicates whose arg declarations are narrower than the network's
nodes, answered only over arguments those types admit (solve-goal).
The value carries its two pass caches and is registered in built-calculi.
Bundle an algebra and its vocabulary into the value every function here takes.
`denotation` maps each stored predicate to the set of base relations it denotes, so its
keys are the predicates the prover claims.
`narrowing` is the optional second reader — nil for a calculus that has none:
{:fn (fn [kb context] → {:net … :support …} | nil)
:over-nodes (fn [nodes] → {:net … :support …} | nil)
:node? which terms are nodes, when not every node is a symbol
:bindings the dynamic vars `:fn` reads, whose values key the resident network
:sources every predicate whose arrival or departure moves what it answers
:contexts the subset that puts a NODE in the network, so names a reader context}
`:over-nodes` reads only the node set, so `with-goal-nodes` runs it over a goal's nodes
too. Either key may be absent. `:sources` and `:contexts` are folded into
`:trigger-predicates` and `:context-predicates` here, once.
`typed` is the predicates whose `arg` declarations are narrower than the network's
nodes, answered only over arguments those types admit (`solve-goal`).
The value carries its two pass caches and is registered in `built-calculi`.(calculus-for kb pred)The registered calculus whose :predicates holds pred, or nil; a predicate belongs
to one calculus. A predicate that only moves a network is calculi-triggered-by's.
The registered calculus whose `:predicates` holds `pred`, or nil; a predicate belongs to one calculus. A predicate that only moves a network is `calculi-triggered-by`'s.
(closure-with-support calc kb context)The support-carrying pass over the network of calc visible from context, every pair
at once: {:network … :support …}, or {:inconsistent [i j] :culprits #{handle}}. A
caller reading many pairs reads them here; support walks every pair per call.
The support-carrying pass over the network of `calc` visible from `context`, every pair
at once: `{:network … :support …}`, or `{:inconsistent [i j] :culprits #{handle}}`. A
caller reading many pairs reads them here; `support` walks every pair per call.(constraint calc net i j)The constraint set on [i j] in net: the identity on the diagonal, the recorded
set, else the universe (unknown).
The constraint set on `[i j]` in `net`: the identity on the diagonal, the recorded set, else the universe (unknown).
(definite calc kb context a b)The single base relation between a and b when path consistency determines it;
:inconsistent when the network contradicts itself, :unknown when two or more
remain possible.
The single base relation between `a` and `b` when path consistency determines it; `:inconsistent` when the network contradicts itself, `:unknown` when two or more remain possible.
(inconsistency-culprits calc kb context){:pair [i j] :support #{handle}} for an unsatisfiable network, the pair whose
constraint emptied and the sentexes behind it, or nil when the network is satisfiable.
Which pair is blamed depends on the driver's order (docs/qcn.md, "Support").
`{:pair [i j] :support #{handle}}` for an unsatisfiable network, the pair whose
constraint emptied and the sentexes behind it, or nil when the network is satisfiable.
Which pair is blamed depends on the driver's order (docs/qcn.md, "Support").(inconsistent? calc kb context)Is the network of calc visible from context unsatisfiable?
Is the network of `calc` visible from `context` unsatisfiable?
(join-baseline kb calc context){:handles … :net …}: the handles the network of calc in context was read out of,
and the network they close to.
`{:handles … :net …}`: the handles the network of `calc` in `context` was read out of,
and the network they close to.(join-delta kb calc context){:moved … :baseline …} for calc in context: the pairs that may license a firing
the last re-join did not, and the baseline to hand note-joined after this re-join.
:moved is :all with no baseline recorded, either side unsatisfiable, or a handle gone
from the network's input; else the pairs, both directions, whose closed constraint
differs, #{} without a pair read when both baseline values are identical? to now's.
`{:moved … :baseline …}` for `calc` in `context`: the pairs that may license a firing
the last re-join did not, and the baseline to hand `note-joined` after this re-join.
`:moved` is `:all` with no baseline recorded, either side unsatisfiable, or a handle gone
from the network's input; else the pairs, both directions, whose closed constraint
differs, `#{}` without a pair read when both baseline values are `identical?` to now's.(network kb calc context)The constraint network {[a b] → #{base relations}} of every believed relation of
calc visible from context, both directions stored: each (P a b) intersects the
pair with P's denotation, each (not (P a b)) with its complement. An unrecorded pair
is the universe. A variable context reads every context's facts into one diagnostic
network that answers no goal.
The constraint network `{[a b] → #{base relations}}` of every believed relation of
`calc` visible from `context`, both directions stored: each `(P a b)` intersects the
pair with P's denotation, each `(not (P a b))` with its complement. An unrecorded pair
is the universe. A variable `context` reads every context's facts into one diagnostic
network that answers no goal.(network-support kb calc context)The asserted support of network: {[a b] → #{handle}}, the sentexes intersected into
each pair.
The asserted support of `network`: `{[a b] → #{handle}}`, the sentexes intersected into
each pair.(nodes net)Every term named by a constraint in net.
Every term named by a constraint in `net`.
(note-joined kb calc context baseline)Record baseline as the network every rule mentioning calc has now been joined over
in context, in the KB's :qcn-joined map. Only a caller that re-joins all of those
rules may call this; a single rule's own full join does not.
Record `baseline` as the network every rule mentioning `calc` has now been joined over in `context`, in the KB's `:qcn-joined` map. Only a caller that re-joins all of those rules may call this; a single rule's own full join does not.
(possible calc kb context a b)The base relations still possible between a and b given everything believed in
context — #{} when the network is inconsistent.
The base relations still possible between `a` and `b` given everything believed in
`context` — `#{}` when the network is inconsistent.(prover calc)The entailment prover for calc, to register with vaelii.core/add-prover.
The entailment prover for `calc`, to register with `vaelii.core/add-prover`.
(prover-for? nm pr)Is pr the prover of the calculus named nm?
Is `pr` the prover of the calculus named `nm`?
(reader-contexts kb calc)The reader contexts of calc: held-contexts over its :context-predicates, the
facts that put a node into a network.
The reader contexts of `calc`: `held-contexts` over its `:context-predicates`, the facts that put a node into a network.
(registered-calculi kb)The calculi whose prover is registered on kb, memoized against the registry's
identity (registry-calculi).
The calculi whose prover is registered on `kb`, memoized against the registry's identity (`registry-calculi`).
(reported-sources kb calc context)unsatisfiable-sources as a report names them: no :stand-in, and :support as a
sorted vector of handles. nil when no source is unsatisfiable.
`unsatisfiable-sources` as a report names them: no `:stand-in`, and `:support` as a sorted vector of handles. nil when no source is unsatisfiable.
(solve-with-support calc kb goal context)(solve-with-support calc kb goal context pairs)Entailed solutions for the positive literal goal in context, each paired with the
handles it rests on: a seq of [bindings #{handle}]. A solution with empty support,
the diagonal of a reflexive denotation, is dropped. pairs narrows the enumeration as
in solve-goal.
Entailed solutions for the positive literal `goal` in `context`, each paired with the
handles it rests on: a seq of `[bindings #{handle}]`. A solution with empty support,
the diagonal of a reflexive denotation, is dropped. `pairs` narrows the enumeration as
in `solve-goal`.(support calc kb context a b)The handles of the stored sentexes the relation between a and b rests on: the
facts intersected into that pair, plus the facts behind every composition that narrowed
it, for one derivation. #{} when the pair is unconstrained or the network is
inconsistent.
The handles of the stored sentexes the relation between `a` and `b` rests on: the
facts intersected into that pair, plus the facts behind every composition that narrowed
it, for one derivation. `#{}` when the pair is unconstrained or the network is
inconsistent.(tighten kb calc context net extra)pass over net, reporting an unsatisfiable one through report-inconsistency!.
net is a network as network reads it, never one with-goal-nodes extended:
newly-seen? holds one value per KB, calculus and context. A goal is tightened through
tighten-for-goal.
`pass` over `net`, reporting an unsatisfiable one through `report-inconsistency!`. `net` is a network as `network` reads it, never one `with-goal-nodes` extended: `newly-seen?` holds one value per KB, calculus and context. A goal is tightened through `tighten-for-goal`.
(typed-admits? calc kb pred x y context)Do the types context sees declared of pred's two positions admit x and y
(admits-fn)? True for a pred that calc does not name :typed. The admission
solve-goal asks of a positive goal, for a caller re-deciding one answer.
Do the types `context` sees declared of `pred`'s two positions admit `x` and `y` (`admits-fn`)? True for a `pred` that `calc` does not name `:typed`. The admission `solve-goal` asks of a positive goal, for a caller re-deciding one answer.
(unsatisfiable-as-written kb calc context)qcn/unsatisfiable-pairs of the network of calc in context, less the stand-in pairs
of its unsatisfiable sources: the pairs whose stored facts no model satisfies.
`qcn/unsatisfiable-pairs` of the network of `calc` in `context`, less the stand-in pairs of its unsatisfiable sources: the pairs whose stored facts no model satisfies.
(unsatisfiable-somewhere? calc kb)Is the network of calc unsatisfiable for some context? Asked of the
governing-contexts alone: a context sees the facts one of them at or above it sees,
less what a defeat or an except withdraws below it, and a network over fewer facts
is never tighter — so no context is unsatisfiable where all of them are satisfiable
(docs/exceptions.md, "Two withdrawals a firing carries").
Is the network of `calc` unsatisfiable for some context? Asked of the `governing-contexts` alone: a context sees the facts one of them at or above it sees, less what a defeat or an `except` withdraws below it, and a network over fewer facts is never tighter — so no context is unsatisfiable where all of them are satisfiable (docs/exceptions.md, "Two withdrawals a firing carries").
(unsatisfiable-sources kb calc context)The unsatisfiable sources a narrowing of calc read in context, each
{:source kw :pairs [[p q] …] :support #{handle} :stand-in #{[a b]}}, a :metric source
adding :cycle [instant …], or naming :dimensions [dimension …] in place of both when
its problem is refused. :stand-in is the pair of this network the narrowing
emptied for the source and no stored fact emptied. nil when no source is unsatisfiable.
The unsatisfiable sources a narrowing of `calc` read in `context`, each
`{:source kw :pairs [[p q] …] :support #{handle} :stand-in #{[a b]}}`, a `:metric` source
adding `:cycle [instant …]`, or naming `:dimensions [dimension …]` in place of both when
its problem is refused. `:stand-in` is the pair of this network the narrowing
emptied for the source and no stored fact emptied. nil when no source is unsatisfiable.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 |