vaelii.impl.asp.label — com.vaelii/vaelii 0.24.0

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. The :program atom on the KB holds what the solver was actually asked (see the KB record); vaelii.core/last-program is the public read of it.

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

Classifying a Program needs a real ASP backend; local-solver produces one labeling and cannot enumerate optima. With no backend reachable, classify-program reports every contested assumption as :supportable — correct (each is one of several options) and never overclaims :true. A represented dilemma is classified and labeled off the dependency graph instead (classify-local), on every build.

classify clj

(classify kb)

Classify the program kb last labeled (last-program) — which of its assumptions were forced, which were an arbitrary pick, and which were excluded.

Returns {:true #{handle} :supportable #{handle} :false #{handle}}, all empty when no labeling has recorded a program. A program label-dilemmas recorded carries the classification it committed against, which is read back rather than recomputed from the program alone.

classify-datum clj

(classify-datum kb h)

Handle h's class over the optimal labelings of the KB's current dilemmas — :true, :supportable or :false, as classify names them — or nil when no dilemma classifies it. Read off the solve-free JTMS bracket (classify-local) once per change clock, with or without a backend, so a backend never changes an answer the bracket gives: a Program encodes no derivation between members, and on dilemmas whose members derive from one another its optima are not the KB's. A backend refines only a :refinable member — one in a cluster the bracket did not enumerate and whose members move none of each other, where the Program over its member component is exact. The (bravely S) / (cautiously S) prover reads this.

classify-local clj

(classify-local kb)

A skeptical/credulous classification of the KB's current dilemmas, read from the JTMS dependency graph — no answer-set enumeration, no backend. Returns the classify shape {:true #{} :supportable #{} :false #{}} plus :refinable, or nil when the KB reports no dilemma. :refinable holds the members of the clusters it did not enumerate whose members move none of each other: a Program over such a cluster is exact, so a backend may classify them.

A resolution forces OUT a minimum-cardinality set of dilemma members that satisfies every nogood (leaves no nogood with all its members still believed); the resolutions are a dilemma set's optimal labelings. A believed datum is classified by which resolutions keep it, read through jtms/grounded-in-region (belief recomputed with a set forced OUT):

• :true — believed under every resolution (skeptical/cautious);
• :supportable — believed under some but not every resolution (credulous/brave);
• :false — believed under no resolution: currently believed only because base belief holds conflicting dilemma sides at once, which no single resolution does. A (weird N) drawn from (and (pac N) (not (pac N))) is that case.

(hasEthicalStance N) drawn from both the pacifist and non-pacifist side is :true — every resolution keeps one side, so one support survives. (opposesWar N) resting on the pacifist side alone is :supportable. It covers derived conclusions, not only the dilemma members a Program holds, so classify-datum reads it for a derived conclusion with a backend too: base belief believes both sides and would overclaim it cautious.

Coupled dilemmas are enumerated together, independent ones apart. Nogoods that share a member, or move a member of each other, form one cluster (cluster-indices); a cluster's resolutions come from min-resolutions. A datum is classified by the joint resolutions of the clusters that move it — the cartesian product of those clusters' optima, since a cluster that does not move the datum leaves it at base whatever it resolves to. A (f N) from (and (e1 N) (e2 N)), where e1 and e2 are each :true in a separate diamond, is :true: it survives every combination. A datum whose product of clusters exceeds VAELII_CLASSIFY_MAX_JOINT_OPTIMA, or that touches a cluster larger than VAELII_CLASSIFY_MAX_CLUSTER_MEMBERS, is left :supportable — sound, and a backend refines it only when it is :refinable. So the cost is the clusters' consequence closures: linear in the number of independent dilemmas (grounded_in_region_test), exponential only inside one interacting cluster or across the clusters one datum joins, and capped at both. See docs/labeling.md.

classify-program clj

dilemma-program clj

(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.

label-context clj

(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 genlCx, 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.

The context is minted whether or not there was a tie, and label-dilemmas is deliberately the other way round. With no recorded Program — a KB the engine never arbitrated in, or a dilemma it declined — the genlCx edge is written and :handles comes back empty: a specialization that sees its base and records nothing is what "the engine committed to nothing" materializes as, and it gives a caller that asked to see one arbitration an empty view rather than an invented one. label-dilemmas makes a choice rather than reporting one, so minting a context for a choice it did not make would assert that one happened.

Additive, so no !: this creates a context and asserts into it. The labeling is undone by retracting the returned handles; the genlCx edge is a premise of its own and is retracted as one.

label-dilemmas clj

(label-dilemmas kb ctx base)

Classify the dilemmas kb currently holds, then materialize one optimal labeling of them into ctx — both read off local-labeling, so a defeat's cascade through the dependency graph is in each. 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 with the classification on it, 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 genlCx (reachable with ask / lookup at level 3 and above — note sentexes-matching 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/verdict defeats the strictly weaker member.

This commits, and the commitment is scoped to ctx. The strengthened copy and the losing side form a nogood whose vantage is ctx, so the losing side is defeated at ctx and below and nowhere else (docs/nmtms.md, "A defeat is scoped to its vantage"). The base keeps believing both sides and reporting its dilemma. The engine's refusal to arbitrate holds: it still refuses on its own, and commits inside ctx only when a caller writes the imperative (docs/labeling.md).

So rival labelings stand side by side, as sibling contexts: each labeling decides the dilemma in its own context, and retracting the returned handles revives the dilemma inside that context.

Additive, so no !: this creates a context and asserts into it, and retracting the returned handles undoes it — including the commitment.