Chapter 15 — Antecedent Constraint Languages

A small language (the book calls it TCON) for wiring numeric devices together, where local propagation carries values and their dependencies. companion index

The big idea

Up to here the companion has been about belief: clauses, labels, justifications, contradictions. Chapter 15 changes the subject to computation — but it keeps the TMS underneath. The setting is constraint networks: little algebraic devices (an adder, a multiplier) wired together so that information set anywhere flows everywhere it can.

The classic picture is the adder. It has three terminals — a, b, and the sum c — and it enforces a + b = c. The crucial property is that it does not have a fixed input/output direction. Set any two terminals and it computes the third:

• know a and b → derive c = a + b,
• know a and c → derive b = c − a,
• know b and c → derive a = c − b.

This is local propagation: each device fires whenever it has enough known terminals to compute another one, no global solver required. Wire many devices together and a single observation can ripple across the whole network.

TCON (“Tiny CONstraint language”) is the chapter’s vehicle for this idea, and its defining choice is that it runs on a TMS. Every value a device computes is installed with a justification recording exactly which other values it was computed from. So a constraint network is not just a calculator: it is a calculator that remembers why each number is what it is, and can therefore explain any value and cleanly retract it when an input changes. That is the antecedent-tracking that gives the chapter its name.

Heads-up on scope: TCON is not implemented in this ltms package — it is an explicit non-goal (see BRIEFING.md). This chapter teaches the ideas and walks the exercise designs; the worked solutions live, in our own words, in ../exercises/ch15/. The “Try it in this repo” section points at the closest machinery we do have (the JTRE) and is honest about where the analogy stops.

Concepts, step by step

Cells

A cell is the unit of storage in a constraint network. In the basic version of TCON a cell holds at most one value, plus a record of why it holds that value (an informant naming the rule or source that supplied it, and the antecedents — the other cells whose values were read to compute this one). A cell is “known” once it has a value and “unknown” otherwise.

Terminals of devices are cells; networks also have internal cells used to carry intermediate quantities (for example, a 2D-vector device internally holds the products rho·cos(theta) and rho·sin(theta)).

Constraints and constraint rules

A constraint (an adder, multiplier, comparator, …) is a bundle of small constraint rules. Each rule is an antecedent rule of exactly the kind earlier chapters built: it has a trigger condition (some subset of the constraint’s cells must be known), and when it fires it computes a value for another cell and records the cells it read as that value’s antecedents.

The adder above is three rules — one per solvable direction. The general principle is that a faithful n-quantity device needs a rule for every direction in which one unknown can be solved from the rest. Miss a direction and the network will sometimes sit quiescent when a value was actually derivable (Exercise 8 is exactly this audit on a three-input adder).

set!, informants, and contradictions

Installing a value into a cell goes through set!. It takes the value plus an informant (the rule that produced it). Two interesting cases arise:

• Agreement. If the cell is already known and the incoming value matches, the basic policy keeps what is already there (“first writer wins”). Exercise 5 argues this is sometimes the wrong choice — a fragile derived justification can squat in a cell that a later, ground value would have justified more robustly — and proposes letting ground values supersede derived ones.
• Conflict. If the incoming value disagrees with the existing one, that is a contradiction. Because TCON sits on a TMS, this is not a hard crash: the conflicting values’ joint support becomes a nogood, and retracting one of the premises behind it dissolves the conflict.

Why the antecedents must be exact

The single discipline that makes TCON correct is: a rule must list as antecedents exactly the cells it actually read — no more, no fewer.

• List too few and the dependency record is unsound: retracting a genuinely-used premise will not retract the value it produced, leaving a stale belief floating with no support.
• List too many and you get spurious retractions and bloated nogoods: a value vanishes when something it never depended on changes.

In the basic language this is enforced structurally by a “use everything you trigger on” convention, which is why each formula is expected to read all its declared inputs. Exercise 6 explores relaxing that — letting a formula report the subset it used — and the tradeoff is precisely the one above: tighter, cheaper dependencies in exchange for trusting each formula to report honestly.

Local propagation: what it can and cannot do

Propagation is monotonic and quiescent. Values get filled in; the engine runs to a fixed point and stops. There is no notion of time and no value re-causing its own change, which is why a loop of constraint-modeled relays cannot oscillate the way a real relay circuit does (Exercise 1g): you either reach a consistent fixed point or the TMS flags circular, unfounded support.

The big limitation is that local propagation is incomplete as an equation solver. It only fires a device when that one device has enough known cells. A system of simultaneous equations — say two linear relations sharing two unknowns — can be perfectly solvable while no single constraint ever has enough known cells to fire. The network just stalls. Section 15.5.2 and Exercise 12 address this by gathering the relevant equations and handing them to a symbolic algebra solver, then writing the solutions back as justified values.

Composing constraints

Bigger devices are built by wiring smaller ones, not by writing one giant formula. A 2D-vector is cleaner as a composition of multiplier, sin, cos, square, adder, sqrt, and atan2 sub-constraints than as a flat block of rules (Exercise 14). Composition is also where the dependency tracking earns its keep: each derived component carries fine-grained antecedents on exactly the sub-devices involved, so changing one input retracts only what truly depended on it.

Section 15.5.1 sketches several extensions that the exercises flesh out:

• Shared structure (Exercise 9): compile each prototype once into a template and reuse the rule code across instances, allocating only per-instance cells — the “flyweight + memoize” transformation, to cut consing in large repetitive networks.
• Removal rules (Exercise 10): rules whose action is to retract values or dismantle structure, the dual of ordinary additive rules — useful for network topology that should change with mode (a switch that disconnects part of a circuit).
• Indirect cells and wiring rules (Exercise 11): cells whose referent is resolved at run time, and rules whose action builds new constraints. Together they let a network grow itself — powerful enough to model an unbounded timeline of states on demand, and dangerous enough to grow without bound unless you add budgets, interning, and demand-driven (lazy) expansion.

Simulation vs. inference (the diagnosis angle)

Section 15.4.3 introduces a distinction that pays off in chapter 17’s diagnosis. A value computed forward, from designated inputs toward designated outputs, is a prediction — something you can later check against a measurement. A value computed backward, from an observed output to an input, is an inference about a cause, not a forecast. Exercise 13 makes the split structural: give every terminal two cells, a simulation cell and an inference cell, and define adder-sim (inputs → outputs) separately from adder-inf (outputs → inputs). A mismatch between a predicted sim-value and the observed inf-value at the same terminal is exactly the discrepancy that drives diagnosis. Keeping the two cell families from crossing is what keeps “what I predicted” and “what I observed” comparable.

The examples, explained

The chapter’s recurring worked example is the adder, and it is worth internalizing because every other device is a variation on it:

• Three-direction propagation. The adder demonstrates the headline feature: one device, three rules, no fixed direction. It is the smallest complete illustration of “set two, get the third,” and it is the example the exercises build a JTRE version of (Exercise 7).

• Building relational devices from comparisons. From an equality test (==?) and a comparator, the chapter shows how to derive sign tests (positive?, zero?, negative?) by wiring against a constant-0 cell, and then how to use a sign test to enforce a physical sanity condition — that travel time in uniform motion (distance = rate · time) must be positive (Exercise 1a–1d). The lesson is reuse: these are compositions of existing primitives, not new primitive rules.

• The relay as a value router. A relay chooses between two inputs based on a control cell (coil). It is the example that most sharply shows why exact antecedents matter: the propagated value depends on the switch position, so coil must appear among the antecedents while the unselected input must not. Flip the coil and the output retracts and re-derives correctly. The relay also composes into a signed-square-root device (Exercise 1e–1f), and motivates the “no oscillation” discussion (1g).

• The 2D vector. This is the example of composition over flat formulas. The book’s 2D-vector (Fig. 15.11) is written flat with many direct rules; Exercise 14 rebuilds it as a wiring of trig, square, adder, and sqrt sub-constraints. The example teaches that the modular version reproduces the same behavior while giving each component sharper dependencies — at the cost of needing a few new primitive constraint types and a small change to how 2D-motion references the vector (through its public terminals, not its internals).

• The diagnosis setup. The Section 15.4.3 example (an adder with a set input and a set output) is what generate-candidates runs over to separate genuine predictions from backward inferences — the seed of the simulation/inference split above.

Exercises walk-through

The full set, with paraphrased statements and conceptual answers, is in ../exercises/ch15/README.md. These are design and analysis answers — there is no runnable code, because TCON is out of this package’s scope. The notable ones:

• Ex 1 (relational devices). Build ==?, comparator, the sign tests, and a relay, then compose them (positive-time enforcement, signed square root). The throughline is that the only complete directions are the forward computation and the =/T inverse; coarse “unequal” or </> outputs carry too little information to pin an unknown back, so they have no inverse rule in a point-valued network. And (1g) constraint propagation cannot oscillate because it has no temporal dimension.

• Ex 2 (one formulae per prototype). Two formula blocks would break the single deterministic pass that assigns each generated rule a stable identity/index — names would collide or rules would be dropped, and “the rule that set this cell” records would go ambiguous. Hence the one-block convention.

• Ex 3 (don’t join networks with ==?). ==? exposes only a 1-bit equality summary; it does not propagate the underlying value or its dependencies, so bolting it between two networks reports whether they match but does not actually couple them. Real sharing needs an identity wire inside one network.

• Ex 4 (sets/intervals as cell values). The big generalization: turn single-value cells into domain cells. set! becomes domain intersection, contradiction becomes an empty domain, devices become relational filters that prune (AC-3-style arc consistency), and “solved” means “domain is a singleton.” This is TCON re-imagined as a finite-domain CSP propagator with TMS-backed justifications.

• Ex 5 (ground beats derived). Tag values as ground vs derived; on a compatible re-set!, prefer the ground justification so the value survives later assumption retraction. The constraint-language analog of “premise beats derivation” in a TMS.

• Ex 6 (return the used subset). Let a formula return (value . used-cells) so set! records the minimal antecedents. Wins: tighter dependencies, fewer spurious retractions, author freedom to short-circuit. Costs: correctness now rests on each formula being honest about what it read, plus per-call overhead and loss of static analyzability.

• Ex 7 (constraints via a PDIS). Implement an adder as three JTRE/JTMS rules (one per direction), each assert justified by the two value facts it read, plus a shared contradiction rule that fires when one cell holds two unequal values. This is the one exercise with a concrete bridge to our code — see “Try it in this repo.”

• Ex 8 (three-input adder semantics). A faithful s = a + b + c needs four directional rules (one per quantity). If the figure supplies fewer, it is incomplete for single-unknown cases; supplying all four fixes it. (It still cannot solve when two-or-more are unknown — that is the inherent limit of local propagation, not a bug.)

• Ex 9 / 10 / 11 (the extensions). Shared-structure building, removal rules, and indirect cells + wiring rules — the language-extension trio summarized above. Exercise 11’s lazy, demand-driven timeline (build state[t+1] only when queried) is the cleanest illustration of how to let a network grow safely.

• Ex 12 (beat local propagation with algebra). gather-equations walks the network from a target cell collecting the relevant equations (substituting known values, expanding the frontier of unknowns), hands the system to a computer-algebra solver, and writes solutions back as justified values. The analysis catalogs the limits: nonlinear multiple roots, underdetermined systems, blow-up, and the need to preserve provenance so the TMS can still retract a CAS-derived value. (12c/12d push further: symbolic-value propagation, and rebuilding SYN or an algebra word-problem solver on top.)

• Ex 13 (simulation/inference split). Dual cells and dual constraints (adder-sim, adder-inf) per terminal; predictions are forward sim-values, discrepancies are sim-vs-inf disagreements. The candidate-generation machinery is adapted to keep the two passes (and two work queues) separate.

• Ex 14 (modular 2D-vector). Replace the flat formula block with a wiring of primitive constraints; the only fallout is updating 2D-motion to reference the vector’s public terminals instead of its now-renamed internals.

Try it in this repo

TCON itself is not here. It is conceptual in this repository; the analysis lives in ../exercises/ch15/. What this repo does have is the machinery Exercise 7 points to — a pattern-directed inference engine on a TMS — and that is the right place to feel the core idea (multi-directional propagation with explicit antecedents) for yourself.

The closest engines are the JTRE (../src/ltms/jtre.py) and the LTRE (../src/ltms/ltre.py). The JTRE is the natural fit for Exercise 7’s adder: represent a cell value as a fact ("value", cell, number), write one rule per solvable direction, justify each derived value by the two facts it read, and add a contradiction rule for two unequal values on one cell. Sketch:

from ltms.jtre import JTre, Condition
from ltms.terms import Var

e = JTre("adder")
x, y, z = Var("x"), Var("y"), Var("z")

# if a and b are known, derive c = a + b  (justified by the two values read)
@e.rule(("value", "a", x), condition=Condition.IN)
def _ab(b1, eng):
    @eng.rule(("value", "b", y), condition=Condition.IN)
    def _inner(b2, eng2):
        a_val, b_val = b1[x], b2[y]
        eng2.justify("adder-fwd", ("value", "c", a_val + b_val),
                     [("value", "a", a_val), ("value", "b", b_val)])

# (write the symmetric a,c -> b and b,c -> a rules the same way,
#  plus a contradiction rule on two unequal values for one cell)

e.assert_(("value", "a", 3))
e.assert_(("value", "b", 4))
e.run_rules()
assert e.is_in(("value", "c", 7))     # forward propagation
print(e.why(("value", "c", 7)))        # the antecedents that produced it

This reproduces the chapter’s essence — a device that propagates and records dependencies — but note the honest gap: the JTRE adder above only fires forward unless you also write the inverse-direction rules, and JTRE facts are not the same as TCON’s single-valued, re-settable cells (in particular set!’s “first writer wins” / conflict policy is something you would have to model). The point of the exercise is precisely that a PDIS can encode constraints; building all the directions and the contradiction rule is left as the (paper) exercise.

For TMS-adjacent ideas that are implemented and runnable, the neighboring companion chapters are the place to go:

. .venv/bin/activate
python examples/run_kb.py examples/kb/belief_revision.kb   # retraction / revision
python examples/coloring_dds.py                            # dependency-directed search

• belief revision and dependency tracking — ch07, ch08
• the LTMS / LTRE and contradiction handling — ch09, ch10
• nogoods and dependency-directed backtracking — ch09

These give you the justification and retraction behavior that TCON layers under its constraints, even though the constraint language on top is not built here.

Takeaways

• A constraint network is cells wired by constraints; each constraint is a bundle of small antecedent rules, one per direction it can solve.
• Local propagation fills in values whenever a single device has enough known cells. It is monotonic, quiescent, and incomplete as an equation solver.
• TCON runs on a TMS, so every value carries a justification — making the network explainable and cleanly revisable, and turning value clashes into retractable contradictions.
• The one discipline that makes it correct: antecedents must be exactly the cells a rule read — too few is unsound, too many is wasteful.
• Beyond the basics lie domain cells (CSP), shared structure, removal rules, self-growing networks (indirect cells + wiring rules), the simulation/inference split for diagnosis, and an algebra hook to beat local propagation’s limits.
• In this repo the language is conceptual; the runnable analog is the TMS-backed PDIS (JTRE/LTRE), and the worked designs are in ../exercises/ch15/.

Back to the companion index · previous: Chapter 14 — Putting the ATMS to Work · next: Chapter 16 — Assumption-Based Constraint Languages.