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.
76 lines
3 KiB
Python
76 lines
3 KiB
Python
"""B2 — the transitive-chain lowering, in isolation.
|
|
|
|
``lower_transitive_chain`` proposes the propositional theory for a same-predicate
|
|
strict-order chain; the caller routes it through the UNCHANGED ``evaluate_entailment``
|
|
ROBDD. These pin the EXACT theory it emits (so a wrong lowering is caught) and its
|
|
soundness-by-construction refusals — a path that is empty, mislabeled, wrong-arity,
|
|
non-contiguous, or does not reach the target lowers to ``None`` (refuse), so a corrupted
|
|
path can never be confirmed as a wrong assertion.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from dataclasses import dataclass
|
|
|
|
from generate.composition.lower_transitive import lower_transitive_chain
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class _Fact:
|
|
"""Minimal duck-typed relational fact (the lowering reads only these two)."""
|
|
|
|
relation_predicate: str
|
|
relation_arguments: tuple[str, ...]
|
|
|
|
|
|
def test_two_hop_chain_lowers_to_transitivity_theory() -> None:
|
|
# less_than(a,b) ∘ less_than(b,c) → less_than(a,c) by p∘p→p.
|
|
path = (_Fact("less_than", ("a", "b")), _Fact("less_than", ("b", "c")))
|
|
lowered = lower_transitive_chain("less_than", "a", "c", path)
|
|
assert lowered is not None
|
|
premises, query = lowered
|
|
# p(a,b)=x0, p(b,c)=x1, rule (p∘p→p): (x0 & x1) -> p(a,c)=x2.
|
|
assert premises == ("x0", "x1", "(x0 & x1) -> x2")
|
|
assert query == "x2"
|
|
|
|
|
|
def test_three_hop_chain_lowers_linearly() -> None:
|
|
path = (
|
|
_Fact("before_event", ("a", "b")),
|
|
_Fact("before_event", ("b", "c")),
|
|
_Fact("before_event", ("c", "d")),
|
|
)
|
|
lowered = lower_transitive_chain("before_event", "a", "d", path)
|
|
assert lowered is not None
|
|
premises, query = lowered
|
|
# x0=p(a,b), x1=p(b,c), (x0&x1)->x2=p(a,c), x3=p(c,d), (x2&x3)->x4=p(a,d).
|
|
assert premises == ("x0", "x1", "(x0 & x1) -> x2", "x3", "(x2 & x3) -> x4")
|
|
assert query == "x4"
|
|
|
|
|
|
def test_empty_path_refuses() -> None:
|
|
assert lower_transitive_chain("less_than", "a", "c", ()) is None
|
|
|
|
|
|
def test_mislabeled_edge_refuses() -> None:
|
|
# an edge whose predicate is not the queried predicate must not be lowered (a
|
|
# cross-predicate edge cannot be laundered into a same-predicate transitive chain).
|
|
path = (_Fact("less_than", ("a", "b")), _Fact("greater_than", ("b", "c")))
|
|
assert lower_transitive_chain("less_than", "a", "c", path) is None
|
|
|
|
|
|
def test_wrong_arity_refuses() -> None:
|
|
path = (_Fact("less_than", ("a", "b", "extra")),) # arity 3
|
|
assert lower_transitive_chain("less_than", "a", "c", path) is None
|
|
|
|
|
|
def test_non_contiguous_path_refuses() -> None:
|
|
# the second edge does not continue from the first edge's endpoint (b != c).
|
|
path = (_Fact("less_than", ("a", "b")), _Fact("less_than", ("c", "d")))
|
|
assert lower_transitive_chain("less_than", "a", "d", path) is None
|
|
|
|
|
|
def test_path_not_reaching_target_refuses() -> None:
|
|
# a contiguous chain a→b but the target is c — the chain does not reach it.
|
|
path = (_Fact("less_than", ("a", "b")),)
|
|
assert lower_transitive_chain("less_than", "a", "c", path) is None
|