1ff06726a6
* feat(determine): add transitive strict-order relational inference Add sound transitive closure for declared strict-order relational predicates — less_than, greater_than, before_event, after_event, and ONLY these. A query p(a, c) determines True when a same-predicate chain p(a, b), p(b, c), ... over the predicate's OWN realized edges is found (BFS reachability) and the proof_chain ROBDD verifies the transitive entailment (search-then-verify, through the UNCHANGED evaluate_entailment via a new lower_transitive_chain). Mirrors _determine_subsumption. Scope / firewall: - TRANSITIVE_PREDICATES is closed and default-off; sibling_of, parent_of, left_of/right_of, inside_of, during_event, overlaps_event are EXCLUDED. - Same-predicate edges only — no transitive-through-inverse, no cross-predicate (triple firewall: recall filter + lowering re-reject + ROBDD re-verify). - Open-world: asserts only answer=True via the shared _relational_determined surface (rule="transitive"), so INV-30 stays at exactly 3 Determined sites and no answer=False is added. One-hop inverse/symmetric (#775) is unchanged. FrameVerdict / closed-world (ADR-0222) is untouched. wrong=0 bite (unit + lane + independent oracle): non-transitive-predicate chains, non-admitted spatial chains, mixed-predicate chains, disjoint chains, reflexive cycles, and inverse+transitive composition all REFUSE. Measurement: new evals/relational_transitive lane with an INDEPENDENT BFS transitive-closure oracle (imports no engine module; INV-25/27), cross-checked both directions (positives oracle-True, confusers oracle-False). Capability-index breadth 10 -> 11, wrong_total 0, deterministic digest re-frozen. Cross-PR reconcile: migrated the one-hop confuser rinf-ref-001 (a less_than chain, which now correctly determines transitively) to a B2 positive; repurposed its unit test to a non-transitive parent_of chain; corrected a pre-existing stale breadth==9 assertion (#775 added a 10th domain but never updated test_capability_index). Verified in the worktree: determine + transitive/one-hop lanes + capability baseline/index + ProofWriter-OWA floor + INV-30/29/21/02 + full smoke — all green. A 3-skeptic read-only adversarial review found no wrong=0 leak. * test(determine): B2 hardening — TRANSITIVE_PREDICATES pin + lower_transitive defensive + budget Add the required B2 hardening tests before merge: - test_transitive_predicates_closed_and_excludes: the table is EXACTLY {less_than, greater_than, before_event, after_event}, every member is in RELATIONAL_PREDICATES, and every deliberately-excluded predicate (sibling_of, spouse_of, parent_of, child_of, left_of, right_of, inside_of, during_event, overlaps_event) is explicitly absent. (Closes the gap where relational.py's comment claimed this test existed but it did not.) - tests/test_composition_lower_transitive.py: direct defensive tests on lower_transitive_chain — empty path, mislabeled (cross-predicate) edge, wrong arity, non-contiguous path, and path-not-reaching-target all lower to None (refuse); plus exact 2-hop and 3-hop theory pins. - test_edge_budget_exhaustion_refuses: above _TRANSITIVE_EDGE_BUDGET the transitive search declines (a safe coverage refusal), never proves.
70 lines
2.8 KiB
Python
70 lines
2.8 KiB
Python
"""Transitive-chain lowering — a strict-order chain ``p(subject → … → target)`` becomes
|
|
a propositional ``(premises, query)`` theory for the sound ROBDD gate. The sibling of
|
|
``lower_logic.py`` for relational transitivity.
|
|
|
|
The lowering proposes a theory; it NEVER evaluates entailment. The caller routes the
|
|
result through the UNCHANGED ``evaluate_entailment`` gate, which re-derives validity from
|
|
scratch — so a path-construction bug here cannot produce a wrong assertion (soundness by
|
|
construction). Mirrors ``lower_logic_chain``'s ``subset ∘ subset`` branch, parameterized
|
|
by predicate: the only structural difference is the rule (``p ∘ p → p`` for any declared
|
|
transitive ``p``, vs. the is-a rules).
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from generate.realize import RealizedRecord
|
|
|
|
|
|
def lower_transitive_chain(
|
|
predicate: str,
|
|
subject: str,
|
|
target: str,
|
|
path: tuple[RealizedRecord, ...],
|
|
) -> tuple[tuple[str, ...], str] | None:
|
|
"""Lower a transitive strict-order chain into a propositional ``(premises,
|
|
query_atom)`` theory: each edge ``p(cur, nxt)`` asserted as a true atom + the
|
|
transitivity rule ``p ∘ p → p`` instantiated at each hop, querying the closure atom
|
|
``p(subject, target)``. LINEAR in the path, so it scales.
|
|
|
|
Returns ``None`` — refuse rather than smuggle a fabricated closure through a corrupted
|
|
path, regardless of the caller's discipline — for any of:
|
|
|
|
* an empty path (no chain);
|
|
* a mislabeled / wrong-arity edge (a fact whose predicate is not ``predicate`` or
|
|
whose arity is not 2 — a cross-predicate edge cannot be laundered in);
|
|
* a NON-CONTIGUOUS chain (the edges do not form ``subject → … → target``).
|
|
"""
|
|
if not path:
|
|
return None
|
|
if any(
|
|
f.relation_predicate != predicate or len(f.relation_arguments) != 2
|
|
for f in path
|
|
):
|
|
return None
|
|
|
|
atoms: dict[tuple[str, str], str] = {}
|
|
|
|
def atom(a: str, b: str) -> str:
|
|
key = (a, b)
|
|
name = atoms.get(key)
|
|
if name is None:
|
|
name = f"x{len(atoms)}"
|
|
atoms[key] = name
|
|
return name
|
|
|
|
premises: list[str] = []
|
|
cur = subject
|
|
for hop, fact in enumerate(path):
|
|
a, b = fact.relation_arguments
|
|
if a != cur: # non-contiguous: the chain does not continue from ``cur``
|
|
return None
|
|
premises.append(atom(cur, b)) # p(cur, b) is told
|
|
if hop > 0: # extend the accumulated closure p(subject, cur) with this edge
|
|
premises.append( # p ∘ p → p
|
|
f"({atom(subject, cur)} & {atom(cur, b)}) -> {atom(subject, b)}"
|
|
)
|
|
cur = b
|
|
if cur != target: # the chain does not reach ``target``
|
|
return None
|
|
|
|
return tuple(premises), atom(subject, target)
|