Brave/cautious classification of a settled tie, and materializing one labeling as a specialization context.
in?The TMS answers what do I believe. After settle arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. in? cannot tell them apart; both read as "believed".
Brave/cautious classification separates them by asking the solver for all optimal answer sets rather than one:
| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
:true | yes | yes | forced — no consistent labeling gives it up |
:supportable | no | yes | arbitrary — the current belief is one of several |
:false | no | no | excluded — no consistent labeling holds it |
:supportable is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are :supportable: whichever the TMS committed to, the
other was equally available.
Two rules keep these from drifting apart from belief.
Classification reads the recorded program, never a recomputed one. Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. core/last-program holds what the solver was
actually asked (see the KB record).
Labeling reads the TMS, not a fresh solve. label-context materializes the
labeling the engine committed to, taken from jtms/in?, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.
So the invariants hold by construction, and asp_label_test pins them:
:true ⊆ believed (cautious holds in the committed model)
:false ∩ believed = ∅ (excluded holds in no model, including that one)
:supportable — either way, by definition
Classification needs a real ASP backend; local-solver produces one labeling and
cannot enumerate optima. With no backend reachable, classify reports every
contested assumption as :supportable — honest (each is one of several options)
and never overclaims :true.
Brave/cautious classification of a settled tie, and materializing one labeling as
a specialization context.
## What this adds over `in?`
The TMS answers *what do I believe*. After `settle` arbitrates a default/default
tie, one side is IN and the other OUT — but that answer flattens two very different
situations. A belief can be IN because every consistent way of resolving the
contradictions keeps it, or because the solver had two equally good options and
picked one. `in?` cannot tell them apart; both read as "believed".
Brave/cautious classification separates them by asking the solver for *all* optimal
answer sets rather than one:
| class | in every optimum | in some optimum | meaning |
|---|---|---|---|
| `:true` | yes | yes | forced — no consistent labeling gives it up |
| `:supportable` | no | yes | arbitrary — the current belief is one of several |
| `:false` | no | no | excluded — no consistent labeling holds it |
`:supportable` is the interesting one, and it is invisible from the TMS alone. In a
Nixon diamond both sides are `:supportable`: whichever the TMS committed to, the
other was equally available.
## Concert with the TMS
Two rules keep these from drifting apart from belief.
**Classification reads the recorded program, never a recomputed one.** Resolving a
tie erases its own evidence — the defeated side stops matching, so the nogood is no
longer derivable from the KB. `core/last-program` holds what the solver was
actually asked (see the KB record).
**Labeling reads the TMS, not a fresh solve.** `label-context` materializes the
labeling the engine *committed to*, taken from `jtms/in?`, rather than re-solving
and hoping for the same answer set back. A re-solve would usually agree, and
"usually" is not a property worth building on.
So the invariants hold by construction, and `asp_label_test` pins them:
:true ⊆ believed (cautious holds in the committed model)
:false ∩ believed = ∅ (excluded holds in no model, including that one)
:supportable — either way, by definition
## Requirements
Classification needs a real ASP backend; `local-solver` produces one labeling and
cannot enumerate optima. With no backend reachable, `classify` reports every
contested assumption as `:supportable` — honest (each *is* one of several options)
and never overclaims `:true`.(classify kb)Classify the tie kb last settled — which of its beliefs were forced, which were
an arbitrary pick, and which were excluded.
Returns {:true #{handle} :supportable #{handle} :false #{handle}}, all empty when
no tie has been arbitrated (nothing contested means nothing to be uncertain about).
Classify the tie `kb` last settled — which of its beliefs were forced, which were
an arbitrary pick, and which were excluded.
Returns `{:true #{handle} :supportable #{handle} :false #{handle}}`, all empty when
no tie has been arbitrated (nothing contested means nothing to be uncertain about).(dilemma-program kb)One Program covering every dilemma kb currently reports, or nil if it
reports none.
All of them together rather than one at a time, because dilemmas can share a datum: a handle contested in two nogoods must be given up (or kept) once, consistently, and only a solver holding both constraints at once can do that. Solving them separately would let the same datum be believed by one answer and not the other, which is not a labeling of anything.
One `Program` covering **every** dilemma `kb` currently reports, or nil if it reports none. All of them together rather than one at a time, because dilemmas can share a datum: a handle contested in two nogoods must be given up (or kept) once, consistently, and only a solver holding both constraints at once can do that. Solving them separately would let the same datum be believed by one answer and not the other, which is not a labeling of anything.
(label-context kb ctx base)Mint ctx as a specialization of base holding the labeling the engine committed
to, and return ctx.
The labeling is read from the TMS — the contested assumptions it currently believes — not from a fresh solve, so the context is guaranteed to say what the engine actually decided rather than what a second solve might have chosen.
ctx sees base through genlContext, so it inherits the whole KB; what it adds
is an explicit, queryable record of one arbitration. Two labelings of the same tie
can therefore be built as sibling contexts and compared.
This entrenches the labeling, so classify before you label. What it writes are
ordinary assertions, and an assertion is evidence: the recorded side now sits in a
second nogood against its rival, which makes defeating the rival strictly cheaper
than defeating the record. A tie that classified as :supportable on both sides
will classify as :true/:false afterwards. Belief does not move — the losing
side was already OUT — but it stops looking arbitrary, because it no longer is:
something now asserts the choice. Retracting the returned handles restores the
open tie.
Additive, so no !: this creates a context and asserts into it, and retracting the
handles it returns undoes it.
Mint `ctx` as a specialization of `base` holding the labeling the engine committed to, and return `ctx`. The labeling is read from the TMS — the contested assumptions it currently believes — not from a fresh solve, so the context is guaranteed to say what the engine actually decided rather than what a second solve might have chosen. `ctx` sees `base` through `genlContext`, so it inherits the whole KB; what it adds is an explicit, queryable record of one arbitration. Two labelings of the same tie can therefore be built as sibling contexts and compared. **This entrenches the labeling, so classify before you label.** What it writes are ordinary assertions, and an assertion is evidence: the recorded side now sits in a second nogood against its rival, which makes defeating the rival strictly cheaper than defeating the record. A tie that classified as `:supportable` on both sides will classify as `:true`/`:false` afterwards. Belief does not move — the losing side was already OUT — but it stops *looking* arbitrary, because it no longer is: something now asserts the choice. Retracting the returned handles restores the open tie. Additive, so no `!`: this creates a context and asserts into it, and retracting the handles it returns undoes it.
(label-dilemmas kb ctx base)Classify the dilemmas kb currently holds, then materialize one optimal labeling
of them into ctx. Returns
{:context ctx :handles [h ...] :classification {...} :program p}; the handles are
empty when the KB holds no dilemma.
The four steps run in an order this fixes so a caller cannot get it wrong — in
particular classification is taken before materialization, because materializing
entrenches. What it writes are ordinary assertions, and an assertion is evidence:
the recorded side lands in a second nogood against its rival, so a tie that
classifies :supportable on both sides classifies :true/:false once labeled.
That is what recording a choice means, not a bug — but it means the classification
has to be read first, and making one call do both is how that stops being something
to remember.
The Program is recorded in kb's :program slot, so last-program and classify
answer about this labeling afterwards. settle never writes that slot for a
dilemma (it builds no Program for one), so nothing is being overwritten.
ctx sees base, and the labeling is recorded by strengthening. Each kept
assumption is re-asserted inside ctx at :monotonic, so ctx is a real world: the
uncontested background is inherited through genlContext (reachable with ask /
lookup at level 3 and above — note query is context-exact and will not show it),
and the contested atoms are decided within it. Nothing needs to be said about the
side that lost: the strengthened copy out-ranks it, and decide-nogood defeats the
strictly weaker member.
This commits, and the commitment is global. Belief in this TMS is a property of
a datum, not of a datum-in-a-context, so strengthening inside ctx defeats the
losing side everywhere — the base KB's dilemma stops being reported and the loser
goes OUT for every context, not just under ctx. Measured on the Nixon diamond:
contradictions 1 → 0. That is a deliberate choice of semantics (docs/labeling.md):
a labeling you can query as a world is worth more than one you can only read, and
the engine's refusal to arbitrate is preserved where it matters — it still refuses
on its own, and only commits when a caller writes the imperative.
So rival labelings are compared sequentially, not side by side: retract the returned handles, which revives the dilemma, then label again. Holding two at once needs belief to be relative to a context, which is what an ATMS's per-datum assumption labels give you and what the TMS does not have today.
Additive, so no !: this creates a context and asserts into it, and retracting the
returned handles undoes it — including the commitment.
Classify the dilemmas `kb` currently holds, then materialize one optimal labeling
of them into `ctx`. Returns
`{:context ctx :handles [h ...] :classification {...} :program p}`; the handles are
empty when the KB holds no dilemma.
The four steps run in an order this fixes so a caller cannot get it wrong — in
particular **classification is taken before materialization**, because materializing
entrenches. What it writes are ordinary assertions, and an assertion is evidence:
the recorded side lands in a second nogood against its rival, so a tie that
classifies `:supportable` on both sides classifies `:true`/`:false` once labeled.
That is what recording a choice means, not a bug — but it means the classification
has to be read first, and making one call do both is how that stops being something
to remember.
The Program is recorded in `kb`'s `:program` slot, so `last-program` and `classify`
answer about this labeling afterwards. `settle` never writes that slot for a
dilemma (it builds no Program for one), so nothing is being overwritten.
**`ctx` sees `base`, and the labeling is recorded by strengthening.** Each kept
assumption is re-asserted inside `ctx` at `:monotonic`, so `ctx` is a real world: the
uncontested background is inherited through `genlContext` (reachable with `ask` /
`lookup` at level 3 and above — note `query` is context-exact and will not show it),
and the contested atoms are decided within it. Nothing needs to be said about the
side that lost: the strengthened copy out-ranks it, and `decide-nogood` defeats the
strictly weaker member.
**This commits, and the commitment is global.** Belief in this TMS is a property of
a datum, not of a datum-in-a-context, so strengthening inside `ctx` defeats the
losing side *everywhere* — the base KB's dilemma stops being reported and the loser
goes OUT for every context, not just under `ctx`. Measured on the Nixon diamond:
`contradictions` 1 → 0. That is a deliberate choice of semantics (docs/labeling.md):
a labeling you can query as a world is worth more than one you can only read, and
the engine's refusal to arbitrate is preserved where it matters — it still refuses
*on its own*, and only commits when a caller writes the imperative.
So rival labelings are compared **sequentially**, not side by side: retract the
returned handles, which revives the dilemma, then label again. Holding two at once
needs belief to be relative to a context, which is what an ATMS's per-datum
assumption labels give you and what the TMS does not have today.
Additive, so no `!`: this creates a context and asserts into it, and retracting the
returned handles undoes it — including the commitment.(program-of-dilemma {:keys [nogood priority sentence sides]})The Program an application builds to rank one reported dilemma: the two contested
handles, the nogood between them, and what each side asserts.
contradictions' promise turned back into the shape the solver machinery takes.
The engine declines to arbitrate; the machinery is still right here for a caller
that wants to.
The `Program` an application builds to rank one reported dilemma: the two contested handles, the nogood between them, and what each side asserts. `contradictions`' promise turned back into the shape the solver machinery takes. The engine declines to arbitrate; the machinery is still right here for a caller that wants to.
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 |