Chapter 8 – Putting the JTMS to Work (JTRE)

How the bare JTMS truth-maintenance core becomes a usable, pattern-directed reasoning engine, and how a problem solver like JSAINT rides on top of it. Back to the companion index.

The big idea

A truth-maintenance system on its own is a bookkeeping device. It knows about nodes, justifications, and which nodes are believed (IN) or not believed (OUT), but it has no idea what those nodes mean and no way to grow the network by itself. You hand it justifications one at a time and it keeps the labels consistent. That is useful, but it is not yet a reasoner.

Chapter 8 closes that gap by wrapping the JTMS in a forward, pattern-directed rule engine called JTRE (the “JTMS Reasoning Engine”). JTRE adds three things the raw JTMS lacks:

  1. A fact database of ground propositions, indexed so you can look facts up quickly and unify patterns against them.
  2. Rules: little programs that wait for a fact matching a pattern to exist or to become believed, then run a body that asserts more facts or installs more rules.
  3. A control loop that drains a queue of triggered rule activations until nothing is left to do.

The payoff is that you write knowledge as rules (“if ?x is human then ?x is mortal”) and the engine instantiates them against concrete facts, while the JTMS underneath keeps track of why every derived fact is believed. Retract a premise and the JTMS automatically withdraws everything that depended on it, with no extra work from your rules. That marriage of pattern-directed inference with dependency tracking is what makes JTRE more than a plain production system.

The second half of the chapter builds JSAINT, a symbolic-integration solver modeled on Slagle’s classic SAINT program, on top of JTRE. JSAINT shows the rule engine being driven not by blind forward chaining but by an agenda of goals under best-first control, where each integration technique is an operator that proposes subgoals. JSAINT is not part of this repository’s ltms package (which ships the truth-maintenance and rule-engine substrate, not the integration operators), so the JSAINT exercises are answered in prose, while the rule-engine mechanics are demonstrated with runnable code.

This chapter is the JTMS twin of the later LTRE material (Chapter 12). If you read them side by side you will see the same architecture: a datum-to-node bridge, car-indexed buckets, parked rules woken by the TMS, and a queue that runs to quiescence. JTRE is the gentler version because its TMS is two-valued and purely forward; LTRE swaps in the clause-based LTMS with bidirectional propagation.

Concepts, step by step

Everything below is grounded in ../src/ltms/jtre.py, which is a compact but faithful Python port of the engine. Read it alongside this section; it is under 250 lines and every piece described here is visible there.

The datum-to-node bridge

The JTMS thinks in Node objects; the rule engine thinks in facts (ground s-expressions like ("prime-number", 7)). JTRE glues the two together with a Datum:

  • Every ground fact gets exactly one Datum.
  • Every Datum owns exactly one JTMS Node.
  • Belief is read straight off the node’s label: node.is_in / node.is_out.

So “is this fact believed?” becomes “find its datum, look at its node’s label.” The datum also carries a small back-pointer (assumption) recording whether the fact was assumed (and by whom) rather than derived, which is what lets you retract it later. The node keeps a reverse pointer back to its datum so the TMS can print readable explanations.

Car-indexing and dbclasses

You do not want to unify a new fact against every fact you have ever seen. JTRE borrows TRE’s trick: index everything by its leftmost constant symbol (its “car,” in Lisp terms). All facts and rules whose pattern starts with the symbol prime-number live together in one bucket, a Dbclass. When a fact arrives, only the rules in its own bucket are even considered for matching, and vice versa. This is the only indexing the system has, and it is enough because patterns in practice almost always have a constant in head position.

get_dbclass walks down to that leftmost symbol (recursing through compounds and chasing bound variables through the environment). A variable in head position with no binding is an error, because there would be nothing to index on.

Interning a fact: referent

referent(fact, create=...) is the single entry point for turning a fact into a datum. It looks in the fact’s bucket for an existing datum with an equal form (facts are deduplicated by structural equality). If none exists and create is true, it mints a fresh datum, creates a JTMS node, links them, files the datum in the bucket, and, crucially, lets every pre-existing rule in that bucket try to match the new datum. That last step is what makes rule-versus-fact arrival order irrelevant.

Assertions, assumptions, justifications

JTRE exposes four ways to put belief into the system, each a thin wrapper over a JTMS operation:

  • assert_(fact) installs the fact as a premise: a justification with no antecedents. It is believed unconditionally and can only stop being believed if you tear down the justification.
  • assume(fact, informant) installs the fact as a retractable assumption. It converts the node to an assumption and enables it. Assumptions are the hooks that dependency-directed search and hypothetical reasoning grab onto.
  • justify(informant, consequent, antecedents) records that a set of already-known facts jointly support a new fact. This is the workhorse rule bodies call: it is how a rule says “because these things are believed, conclude that.” The JTMS then decides whether the consequent is actually IN (it is, precisely when all antecedents are IN).
  • retract(fact, informant) withdraws an assumption you previously made (and only if the same informant made it). The JTMS handles the fallout: anything that was believed only through this assumption goes OUT.

contradiction(fact) marks a node as a contradiction, so that if it ever becomes believed the JTMS signals trouble. The JTMS only signals; resolving the contradiction (dependency-directed backtracking) is the engine’s or the search layer’s job.

Queries

  • is_in(fact) / is_out(fact) read belief. Note the asymmetry: a fact that was never interned counts as OUT (not believed), which matches the JTMS meaning of OUT as “not currently derivable,” not “known false.” The JTMS can never conclude a negation; that two-valued limitation is the whole reason the LTMS exists later.
  • fetch(pattern) returns every stored fact that unifies with a pattern, with the pattern’s variables substituted. It only scans the pattern’s bucket, so the leftmost symbol must be a constant.
  • why(fact) asks the JTMS for a human-readable account of the fact’s current support, e.g. ('suggest-key', 7) is IN via key <= ('prime', 7).

Rules: triggers, conditions, parking

A rule is a trigger pattern plus a body callable plus a firing condition. The three conditions are the heart of the chapter’s design:

  • INTERN: fire as soon as a matching fact exists, regardless of whether it is believed. Use this when you want to react to the mere appearance of a fact.
  • IN: fire when a matching node is believed. This is the default and the common case.
  • OUT: fire when a matching node is not believed. This lets you reason about absence, carefully.

The subtle part is what happens when a rule matches a fact whose node does not yet have the required label. An IN rule that matches an OUT node cannot fire yet, so JTRE parks the activation on the node (node.in_rules). Later, when the JTMS flips that node to IN, it calls an injected enqueue procedure that pushes the parked activation onto the engine’s rule queue. This is the TMS-to-engine bridge: the rule engine hands the JTMS a callback at construction time, and the JTMS uses it to wake sleeping rules exactly when their belief precondition is met. Parked rules are one-shot: once woken they are cleared, so a rule does not re-fire just because a node’s label was reassigned to the same value.

add_rule files the rule in the trigger’s bucket and immediately tests it against every fact already in that bucket, so, just as with facts, a rule sees the data that arrived before it. rule(...) is a decorator-flavored sugar over add_rule for when you want to write the body inline.

The matcher and the queue

_try_rule_on is the single place matching happens. It unifies the fact against the rule’s trigger, seeded with the rule’s captured environment. On success it builds an activation (body, bindings) and routes it: INTERN goes straight to the queue, IN/OUT go to the queue if the label already matches, otherwise they park on the node.

run_rules then drains the queue. It pops activations LIFO (the book notes that order does not affect correctness) and calls each body with its bindings and the engine. Bodies may assert facts, justify conclusions, or install more rules, all of which can enqueue further activations, so the loop runs until the system reaches quiescence. The rules_run counter records how much work happened.

Conjunction by nesting

There is no multi-trigger rule syntax. A rule that should fire only when several conditions hold simultaneously is built by nesting: the rule on the first trigger, when it fires, installs a rule on the second trigger that has captured the first’s bindings; that inner rule installs a rule on the third; and the innermost body is the real work. Because every level fires only under its own IN condition, the body runs only when all the triggers are simultaneously believed. And because the body justifies its conclusion through all the antecedents, the JTMS withdraws the conclusion the moment any antecedent goes OUT. This is exactly how a multi-clause rule macro would compile, and it is the mechanism behind Exercise 3.

The examples, explained

The chapter’s worked material falls into two arcs: small JTRE programs that show the mechanics, and the JSAINT integration solver that shows the engine driving a real search.

The “suggest a code key” rule (the cautionary tale)

The book’s running cautionary example is a rule that, on seeing a prime number, suggests it as a key, but only if some side condition holds. The natural-looking way to write the side condition is a :TEST clause that calls fetch against the live database to see whether (using trap-door-code) is currently believed. The example exists to show why that is a trap, and it drives all of Exercise 1.

The lesson: a :TEST is arbitrary code run by the matcher, during the most performance-critical phase of the engine. If it consults current belief, the rule’s firing becomes a function of assertion order rather than of its trigger bindings, and, worse, the conclusion gets no dependency link to the consulted fact. So the conclusion can survive after the fact it secretly depended on is retracted. That defeats the entire purpose of having a TMS. The fix is to put belief conditions into the trigger conjunction (where the JTMS records dependencies) and reserve :TEST for pure, terminating arithmetic and structural guards over the bindings.

JSAINT solves symbolic integrals the way SAINT did: by treating “integrate this expression” as a goal and applying operators, each a known integration technique, that either solve the goal directly or reduce it to subgoals. A few ideas worth carrying away even though the code is not in this repo:

  • Operators are pattern-triggered. An operator applies only when the goal’s expression syntactically matches its trigger. This is why one mathematical law often needs two operators: the special-cased surface form (x^2) and the general form (x^n) are different patterns, and purely syntactic matching has no “this constant or any exponent” construct. That is Exercise 6.

  • Control terms are first-class propositions. A goal like (integrate expr result) lives in the same database and TMS as domain facts. That means goals get dependencies, can be retracted, and compose into explanations uniformly, the “standard predicate” reading that Exercise 7 demonstrates: assert the goal, it justifies a result; retract the goal, the TMS withdraws the result.

  • An agenda gives best-first control. Rather than blind forward chaining, JSAINT keeps an agenda of pending subgoals ordered by an estimated difficulty, and works the most promising one next. Exercise 10 is all about improving that estimate and making the solver behave coherently instead of thrashing between half-finished approaches.

  • Some operators are speculative. Integration by parts and u-substitution may or may not make progress, and you only find out after solving the subgoals. That post-hoc applicability (Exercise 8) is the seed of generate-and-test operators with a validation step.

Exercises walk-through

The full paraphrased problem statements and answers live in ../exercises/ch08/README.md; the runnable demonstrations are in ../exercises/ch08/solutions.py. Six rule-engine exercises are demonstrated with code; the JSAINT/simplifier design exercises (6, 8 through 16) are answered in prose there because JSAINT, its operator language, and the simplifier are not part of the package. Here are the notable ones.

Exercise 1 – the dangers of :TEST

The pivotal exercise. _ex1a_unsafe_test builds the same two facts, (using trap-door-code) and (prime-number 7), in two different orders against two engines. In order A (condition asserted first) the suggestion is believed; in order B (condition asserted last) it is not. Same facts, opposite conclusions: order_dependent_bug = True. That single result makes the abstract warning concrete. The remaining parts (1b through 1d) design a safe sublanguage for tests (pure, terminating, side-effect-free predicates over the bindings only), show how to enforce it syntactically at rule-definition time, and then honestly note which useful tests that restriction forbids, concluding that the real fix is moving database conditions into the trigger, not enriching the test language.

Exercise 3 – conjunctive triggers

_ex3_conjunctive_trigger is the cleanest illustration of the nesting pattern. The outer rule on (foo ?x), when it fires, installs an inner rule on (bar ?x) that has captured ?x. After asserting only (foo a), (mumble a) is not believed (mumble_after_foo_only = False); after also asserting (bar a) it is (mumble_after_both = True). The conclusion is justified through both antecedents, so it is properly dependency-tracked.

Exercise 4 – one-shot rules on ground triggers

A rule whose trigger is fully ground, like (bar A), can match at most one fact, so once it has fired it is dead weight and an optimizer could splice it out of its bucket. The exercise is demonstrated in two halves. _ex4_one_shot_rule uses a “done” guard so the body fires exactly once even after the matching datum is re-justified (body_invocations = 1). _ex4_match_count confirms the premise in a plain Tre: a ground trigger (bar a) has exactly one successful match (successful_matches_for_ground_trigger = 1) even after an unrelated (bar b) is asserted, so the rule really is spent afterward.

Exercise 5 – generalizing TRY-IN-CONTEXT

A design exercise that maps neatly onto code already in the package. The j-queens version of TRY-IN-CONTEXT misbehaves when the solver caches partial solutions and nogoods, because it can blame the current choice for a contradiction that actually involves a cached choice. The fix is to skip choices already forced true/false and to compute the responsible assumptions from the violated clause, recording the nogood over the real culprits. That corrected discipline is exactly what ../src/ltms/dds.py already implements, so the generalized TRY-IN-CONTEXT is structurally the per-choice body of dd_search.

Exercise 7 – the logical status of a control term

_ex7_control_term_is_proposition demonstrates the predicate reading of a control term. An (integrate x^2) goal is assumed, a rule fires and justifies (integral-result x^2), and the query confirms the result is believed while the goal is in (result_while_goal_in = True). Then the goal is retracted and the TMS withdraws the result (result_after_goal_retracted = False). A control term behaves like a first-class, dependency-tracked proposition, which is the practical argument for treating goals as ordinary facts rather than reaching for modal machinery the JTMS does not have.

Exercise 11a – a tiny symbolic differentiator

u-substitution needs derivatives, so _ex11a_symbolic_diff builds a small forward-chaining differentiator out of Tre rules: constant rule, variable rule, power rule, and a sum rule that requests its two sub-derivatives and then a nested rule combines them once both arrive (the same nesting idiom as Exercise 3). Running it on x^3 + 5 yields ("+", ("*", ("const", 3), ("^", ("var",), 2)), ("const", 0)), that is, 3x^2 + 0. Product, quotient, and chain rules would extend the same pattern. The later parts (11b, 11c) discuss what knowledge makes good substitution suggestions and sketch a defsubst facility, both in prose.

The prose exercises (6, 8 through 16)

These probe JSAINT and the simplifier directly and are answered as design discussions in the exercises README: why one integral law needs two operators and how to fuse them (6); operators whose applicability is only known after subgoals solve (8); adding wall-clock and storage governors to the agenda loop (9); sharper difficulty estimation and more coherent goal selection (10); integration by parts and its non-determinism (12); a faster like-terms combiner that indexes base terms instead of enumerating segment splits (13); a higher-order pattern language with predicate-bearing subset patterns over associative-commutative operators (14); and the two capstones, extending JSAINT to SAINT’s full range (15) and reconstructing the LEX learning system on top of it (16). The summary table at the end of the exercises README tracks which are demonstrated and which are prose.

Try it in this repo

All commands are run from the repository root with the virtualenv active.

Activate the environment once:

. .venv/bin/activate

Run every demonstrated Chapter 8 exercise and see the labeled results:

python exercises/ch08/solutions.py

You should see output confirming the key findings, including order_dependent_bug: True (Exercise 1a), mumble_after_foo_only: False with mumble_after_both: True (Exercise 3), body_invocations: 1 (Exercise 4), result_after_goal_retracted: False (Exercise 7), and the differentiated 3x^2 + 0 expression (Exercise 11a).

Drive JTRE directly to watch the datum-to-node bridge, a rule firing, and an explanation in one go:

python -c "
from ltms import JTre, Var
N = Var('n')
e = JTre()
e.add_rule(('prime', N),
           lambda b, t: t.justify('key', ('suggest-key', b[N]), [('prime', b[N])]))
e.assert_(('prime', 7))
e.run_rules()
print('believed?', e.is_in(('suggest-key', 7)))
print(e.why(('suggest-key', 7)))
"

This prints believed? True and ('suggest-key', 7) is IN via key <= ('prime', 7), showing the rule firing and the JTMS recording the justification.

To see retraction withdraw a conclusion (the Exercise 7 effect), assume a fact, derive from it, then retract it:

python -c "
from ltms import JTre, Var
X = Var('x')
e = JTre()
e.add_rule(('integrate', X),
           lambda b, t: t.justify('m', ('result', b[X]), [('integrate', b[X])]))
e.assume(('integrate', 'x^2'), 'goal'); e.run_rules()
print('while goal in:', e.is_in(('result', 'x^2')))
e.retract(('integrate', 'x^2'), 'goal')
print('after retract:', e.is_in(('result', 'x^2')))
"

Note on the .kb files: the directives under ../examples/kb/ (run with python examples/run_kb.py examples/kb/<file>.kb) load against the LTRE engine, not JTRE, so they belong with the later chapters. There is no kb/ directory for Chapter 8; the JTRE demonstrations all live in the solutions.py above. The engine source to read is ../src/ltms/jtre.py, and its truth-maintenance core is ../src/ltms/jtms.py.

Takeaways

  • JTRE = JTMS + a fact database + pattern-directed rules + a run-to-quiescence loop. The TMS supplies belief and dependencies; the engine supplies matching and instantiation. Neither is useful for problem solving alone.
  • One datum per ground fact, one node per datum. Belief is read off the node’s label, and the fact database is car-indexed into dbclasses so matching only ever touches a small bucket.
  • Three trigger conditions (INTERN, IN, OUT) plus parking are the whole rule model. A belief-conditioned rule that matches too early sleeps on its node and is woken by the TMS-to-engine enqueue bridge when the label arrives.
  • Conjunction is nesting. Multi-condition rules are built by having each fired trigger install the next, capturing bindings as it goes, with the JTMS keeping the final conclusion honest.
  • Never let a :TEST consult the database. Doing so makes belief depend on assertion order and breaks dependency tracking. Put belief conditions in the trigger; keep tests pure.
  • Control terms are just propositions. Treating goals like (integrate ...) as ordinary dependency-tracked facts is what lets a solver like JSAINT retract goals, explain its reasoning, and reuse the TMS for free.
  • JTRE is the JTMS-flavored sibling of LTRE. Same architecture, simpler TMS. When you move to ../exercises/ch09/ and the LTMS chapters, you will recognize every piece, now with three-valued labels and clause-based propagation.
This site uses Just the Docs, a documentation theme for Jekyll.