Sign arithmetic — the coarsest quantitative reasoning there is, and the one a common-sense KB can nearly always do. Nobody knows how fast the tap runs or how fast the drain empties, and everybody knows the tub fills when the tap runs faster.
A quantity's sign is one of three values, SignNegative / SignZero /
SignPositive, and the three are jointly exhaustive and pairwise disjoint over the
reals — so a set of them is a real constraint and its complement is a refutation, which
is the same licence the relation algebras of vaelii.impl.qcn reason under. A
quantity's trend is the sign of its rate of change, and it is not a second theory:
(derivativeOf Rate Q) says which quantity a rate is the rate of, and a trend is then
that rate's sign read at the other end of the edge.
Three declared relations do the arithmetic. (qualitativeSum A B Q) says Q is A + B,
(qualitativeDifference A B Q) that it is A − B, (qualitativeProduct A B Q) that it
is A × B — declarations about which quantities stand in the relation, not sentences
about numbers, since there are no numbers here at all.
Ambiguity is answered with no answer. Two positives sum to a positive and two
negatives to a negative, but a positive and a negative sum to anything whatever: the
sign of the total is the sign of the larger, and nothing here knows which that is. So
the sum takes all three values and no goal about it is answered — never a guess. What
resolves it is a stated (greaterInMagnitudeThan A B), and then the sum takes A's sign.
Written the way qcn and stp are written, and for the same reason: pure data in,
pure data out in the first half, the KB reading and the prover in the second. The
algorithm is a greatest fixpoint over sets of possible signs — a constraint narrows an
output and never widens it, intersection is commutative and associative, so the reading
is a function of the believed facts and never of the order they arrived in. A set
narrowed to nothing is a contradiction, reported to the violations ledger, and then no
sign goal in that context is answered: an unsatisfiable theory is not mined for
conclusions.
The prover is opt-in: register it with vaelii.core/add-reasoner :sign, and until
then a KB stores and retrieves these facts as ordinary facts. The vocabulary ships in
kb/upper/CxMeasure.txt either way. See docs/sign.md.
Sign arithmetic — the coarsest quantitative reasoning there is, and the one a common-sense KB can nearly always do. Nobody knows how fast the tap runs or how fast the drain empties, and everybody knows the tub fills when the tap runs faster. A quantity's **sign** is one of three values, `SignNegative` / `SignZero` / `SignPositive`, and the three are jointly exhaustive and pairwise disjoint over the reals — so a set of them is a real constraint and its complement is a refutation, which is the same licence the relation algebras of `vaelii.impl.qcn` reason under. A quantity's **trend** is the sign of its rate of change, and it is not a second theory: `(derivativeOf Rate Q)` says which quantity a rate is the rate *of*, and a trend is then that rate's sign read at the other end of the edge. Three declared relations do the arithmetic. `(qualitativeSum A B Q)` says Q is A + B, `(qualitativeDifference A B Q)` that it is A − B, `(qualitativeProduct A B Q)` that it is A × B — declarations about *which* quantities stand in the relation, not sentences about numbers, since there are no numbers here at all. **Ambiguity is answered with no answer.** Two positives sum to a positive and two negatives to a negative, but a positive and a negative sum to anything whatever: the sign of the total is the sign of the larger, and nothing here knows which that is. So the sum takes all three values and no goal about it is answered — never a guess. What resolves it is a stated `(greaterInMagnitudeThan A B)`, and then the sum takes A's sign. Written the way `qcn` and `stp` are written, and for the same reason: **pure data in, pure data out** in the first half, the KB reading and the prover in the second. The algorithm is a greatest fixpoint over sets of possible signs — a constraint narrows an output and never widens it, intersection is commutative and associative, so the reading is a function of the believed facts and never of the order they arrived in. A set narrowed to nothing is a contradiction, reported to the violations ledger, and then no sign goal in that context is answered: an unsatisfiable theory is not mined for conclusions. The prover is **opt-in**: register it with `vaelii.core/add-reasoner :sign`, and until then a KB stores and retrieves these facts as ordinary facts. The vocabulary ships in `kb/upper/CxMeasure.txt` either way. See docs/sign.md.
The three values a quantity's sign takes. Jointly exhaustive and pairwise disjoint
over the reals: exactly one holds of any quantity, which is what makes a set of them
the constraint "one of these" rather than an absence of knowledge, and what licenses
the refutation solve answers for a negated goal.
The three values a quantity's sign takes. Jointly exhaustive and pairwise disjoint over the reals: exactly one holds of any quantity, which is what makes a *set* of them the constraint "one of these" rather than an absence of knowledge, and what licenses the refutation `solve` answers for a negated goal.
The three declared relations the arithmetic runs over.
The three declared relations the arithmetic runs over.
(combined kind sa sb dominant)The signs the output of kind can take, given its two inputs' possible sets and which
input (if either) is the larger in magnitude. kind is the arithmetic predicate the
relation was stated with.
The signs the output of `kind` can take, given its two inputs' possible sets and which input (if either) is the larger in magnitude. `kind` is the arithmetic predicate the relation was stated with.
What resolves the one ambiguous entry in the addition table.
What resolves the one ambiguous entry in the addition table.
The edge joining a rate to the quantity it is the rate of, and so a sign to a trend.
The edge joining a rate to the quantity it is the rate of, and so a sign to a trend.
(inconsistent-state? state)Has some quantity been narrowed to no sign at all? A quantity has one of three values and a set of them is the claim "one of these", so an empty set is a set of facts no assignment satisfies.
Has some quantity been narrowed to no sign at all? A quantity has one of three values and a set of them is the claim "one of these", so an empty set is a set of facts no assignment satisfies.
Each sign under negation — what qualitativeDifference turns its subtrahend into, so
that A − B is read as A + (−B) and one addition table serves both.
Each sign under negation — what `qualitativeDifference` turns its subtrahend into, so that A − B is read as A + (−B) and one addition table serves both.
(possible-signs kb context attribute quantity)The signs attribute (:sign or :trend) may take for quantity in context, and
what says so: [#{sign} #{handle}].
[#{} #{}] when the reading is inconsistent — an unsatisfiable theory entails nothing —
and the whole of all-signs with no support for a quantity nothing constrains, which is
a real answer ("nothing is known") rather than an absent one.
The signs `attribute` (`:sign` or `:trend`) may take for `quantity` in `context`, and
what says so: `[#{sign} #{handle}]`.
`[#{} #{}]` when the reading is inconsistent — an unsatisfiable theory entails nothing —
and the whole of `all-signs` with no support for a quantity nothing constrains, which is
a real answer ("nothing is known") rather than an absent one.(reading kb context)The resolved sign state visible from context: {[attribute quantity] → [#{sign} #{handle}]}, or :inconsistent when the facts contradict each other.
Resident on the KB's :qcn atom under a key of this namespace's own, stamped with
observe/change-clock exactly as a qualitative network is (qcn-kb/read-network), so a
rule joining a sign antecedent over many bindings reads the KB once rather than once per
binding — and so does a settle re-checking one firing after another.
The inconsistency is reported on the way past, once per KB, context and state
(observe/newly-seen?): the alternative is a query that silently answers nothing about
a KB that has said two contradictory things. A change of belief is a different state
and reports again.
The resolved sign state visible from `context`: `{[attribute quantity] → [#{sign}
#{handle}]}`, or `:inconsistent` when the facts contradict each other.
**Resident** on the KB's `:qcn` atom under a key of this namespace's own, stamped with
`observe/change-clock` exactly as a qualitative network is (`qcn-kb/read-network`), so a
rule joining a sign antecedent over many bindings reads the KB once rather than once per
binding — and so does a settle re-checking one firing after another.
The inconsistency is **reported** on the way past, once per KB, context and state
(`observe/newly-seen?`): the alternative is a query that silently answers nothing about
a KB that has said two contradictory things. A change of belief is a different state
and reports again.(resolve-state state cs)Narrow every constraint's output to a fixpoint, and answer the state reached.
It terminates because every step shrinks a set in a three-element lattice and there
are finitely many keys, and it reaches the same state whatever order the constraints are
taken in: intersection is commutative and associative, so the fixpoint is the greatest
one below the stated facts and is unique. The order the constraints are taken in
decides only which handles a narrowing names, and constraint-order fixes that on
content.
Narrow every constraint's output to a fixpoint, and answer the state reached. It terminates because every step **shrinks** a set in a three-element lattice and there are finitely many keys, and it reaches the same state whatever order the constraints are taken in: intersection is commutative and associative, so the fixpoint is the greatest one below the stated facts and is unique. The order the constraints are taken in decides only which handles a narrowing names, and `constraint-order` fixes that on content.
The three sign individuals, and the value each denotes. Symbols in the KB, keywords in the arithmetic — the KB's own three terms are the interface and the keywords are what the tables are written over.
The three sign individuals, and the value each denotes. Symbols in the KB, keywords in the arithmetic — the KB's own three terms are the interface and the keywords are what the tables are written over.
The two predicates a sign is stated with, and the two the prover answers. trendOf
is answered as well as read: a trend is a value in its own right, whether stated
outright or read off the rate that produces it.
The two predicates a sign is *stated* with, and the two the prover answers. `trendOf` is answered as well as read: a trend is a value in its own right, whether stated outright or read off the rate that produces it.
(sign-prover)The sign-arithmetic prover, to register with vaelii.core/add-prover.
The sign-arithmetic prover, to register with `vaelii.core/add-prover`.
Every predicate the reading reads, which is what a conclusion drawn from a sign rests
on besides the facts a rule's other antecedents matched (provers/SupportingProver).
Every predicate the reading reads, which is what a conclusion drawn from a sign rests on besides the facts a rule's other antecedents matched (`provers/SupportingProver`).
sign-of-value read backwards: how a computed value is rendered as the term a KB
states.
`sign-of-value` read backwards: how a computed value is rendered as the term a KB states.
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 |