From cd1a9cbe80a0be0f9d5097ce87bf7be2ddaf91b7 Mon Sep 17 00:00:00 2001 From: Shay Date: Sat, 6 Jun 2026 11:09:39 -0700 Subject: [PATCH] =?UTF-8?q?feat(determine):=20transitive=20subsumption=20?= =?UTF-8?q?=E2=80=94=20sound=20is-a=20reasoning=20over=20accrued=20knowled?= =?UTF-8?q?ge=20(Step=20C)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit DETERMINE was one-hop. C answers a member/subset query that holds by SOUND transitive subsumption when direct entailment misses: member∘subset* and subset∘subset (the Description-Logic is-a rules). 'Socrates is a man. All men are mortal. Is Socrates mortal?' -> yes, as told. wrong=0 hazard surfaced and closed: member∘member is NOT transitive (instance-of vs subclass-of) — 'Socrates is a man. Man is a species.' does NOT entail 'Socrates is a species'. That rule is NEVER an edge, so the fallacy is unreachable (bite-tested). The reader's member/subset split (X is a Y vs all Xs are Ys) is exactly the instance-of/ subclass-of distinction that makes the included rules sound. Mechanism: SEARCH-then-VERIFY. Reachability over the sound edges finds the chain, then the proof_chain ROBDD verifies that chain's propositional entailment (O(path) premises). Full O(n³) grounding into proof_chain was tried and rejected: it overruns the canonicalizer's per-conjunct recursion, and transitive closure is reachability, not general SAT. Search-then-verify scales (11-hop chain determines in ~2ms) and keeps the sound+complete decider as the wrong=0 verifier + proof artifact. subset is now a supported direct-entailment predicate (a told subset(a,b) answers it); the other categoricals (disjoint/intersects/some_not) stay excluded. Two existing tests updated accordingly (subset->ungrounded, disjoint stays unsupported_query). --- generate/determine/determine.py | 200 ++++++++++++++++++++++++++--- tests/test_determine_d0.py | 8 +- tests/test_determine_transitive.py | 145 +++++++++++++++++++++ tests/test_relational_reader.py | 23 +++- 4 files changed, 348 insertions(+), 28 deletions(-) create mode 100644 tests/test_determine_transitive.py diff --git a/generate/determine/determine.py b/generate/determine/determine.py index 82fca987..fae59082 100644 --- a/generate/determine/determine.py +++ b/generate/determine/determine.py @@ -37,11 +37,27 @@ from generate.realize import RealizedRecord, recall_realized from session.context import SessionContext from teaching.epistemic import ADMISSIBLE_AS_EVIDENCE, EpistemicStatus -#: The CLOSED set of query predicates D0 has a SOUND direct-entailment path for: -#: ``member`` plus the ground binary relational predicates. Direct entailment is -#: "a realized fact ``p(s, t)`` directly answers the asked ``p(s, t)``" — sound for -#: these ground relations, unsound for categorical/propositional predicates (excluded). -_SUPPORTED_PREDICATES = frozenset({"member"}) | RELATIONAL_PREDICATES +#: The CLOSED set of query predicates with a SOUND DIRECT-entailment path: ``member``, +#: ``subset`` (a told ``subset(a, b)`` — "all a are b" — directly answers the asked +#: ``subset(a, b)``), plus the ground binary relational predicates. Direct entailment is +#: "a realized fact ``p(s, t)`` directly answers the asked ``p(s, t)``". The OTHER +#: categorical predicates (``disjoint`` / ``intersects`` / ``some_not``) and the +#: propositional ones stay EXCLUDED — their truth is not a stored-pair lookup. +_SUPPORTED_PREDICATES = frozenset({"member", "subset"}) | RELATIONAL_PREDICATES + +#: Predicates C can answer by SOUND transitive SUBSUMPTION (is-a) chaining when direct +#: entailment misses. The only sound is-a rules are ``subset ∘ subset → subset`` and +#: ``member ∘ subset → member`` (Description-Logic subsumption). ``member ∘ member`` is +#: DELIBERATELY ABSENT: instance-of is not transitive — "Socrates is a man" + "man is a +#: species" does NOT entail "Socrates is a species". The reader's member/subset split +#: (instance-of vs subclass-of) is exactly what makes the included rules sound. +_SUBSUMPTION_PREDICATES = frozenset({"member", "subset"}) + +#: Bound on the realized subset-fact count the transitive search will consider. Above +#: it, transitive subsumption declines (a safe, deterministic COVERAGE refusal — never +#: an unsound answer); direct entailment is unaffected. Search-then-verify is cheap +#: (O(V+E) reachability), so this is a generous backstop, not a tight grounding budget. +_SUBSUMPTION_SUBSET_FACT_BUDGET = 4096 @dataclass(frozen=True, slots=True) @@ -108,26 +124,170 @@ def determine( predicate = query.predicate subject, target = query.arguments[0], query.arguments[1] - # Structural recall: the realized facts of this predicate about this subject (R1a). - # Exact, deterministic, versor-collision-irrelevant — never a metric call. - facts = recall_realized(ctx, subject=subject, predicate=predicate) - if not facts: - return Undetermined("ungrounded") # nothing realized about the subject + # 1. DIRECT entailment: a realized p(subject, target) holds as-told. Exact, + # deterministic structural recall (R1a) — never a metric call. Symmetric relations + # (sibling_of, equal_to …) read only the stored direction here. + direct = recall_realized(ctx, subject=subject, predicate=predicate) + grounding = next((f for f in direct if f.relation_arguments == (subject, target)), None) + if grounding is not None: + return Determined( + answer=True, + basis=_basis((grounding,)), + predicate=predicate, + subject=subject, + object=target, + grounds=(grounding,), + ) - # Direct entailment: a realized p(subject, target) holds as-told. Open-world: - # facts about the subject that do NOT match the asked target never refute it, so a - # miss is a refusal (``not_entailed``), never an asserted False. Symmetric relations - # (sibling_of, equal_to …) read only the stored direction here — the converse is a - # sound-but-incomplete ``not_entailed``, never a fabricated assertion. - grounding = next((f for f in facts if f.relation_arguments == (subject, target)), None) - if grounding is None: - return Undetermined("not_entailed") + # 2. TRANSITIVE subsumption (C): when direct entailment misses, a member/subset + # query may still hold by SOUND is-a chaining (member∘subset, subset∘subset) decided + # by the sound+complete proof_chain ROBDD — NEVER member∘member. + if predicate in _SUBSUMPTION_PREDICATES: + chained = _determine_subsumption(ctx, predicate, subject, target) + if chained is not None: + return chained + # 3. Open-world refusal — absence (no direct fact, no sound chain) never asserts a + # positive answer and never asserts False. + return Undetermined("ungrounded" if not direct else "not_entailed") + + +def _subset_path( + start: str, target: str, supers: dict[str, list[tuple[str, RealizedRecord]]] +) -> tuple[RealizedRecord, ...] | None: + """The realized ``subset`` facts on a path ``start → … → target`` (≥1 edge), or + ``None`` if ``target`` is not reachable from ``start`` over the subset edges. BFS, + so the path is shortest; deterministic (neighbours are visited in sorted order).""" + if start == target: + return () + frontier: list[str] = [start] + came_from: dict[str, tuple[str, RealizedRecord]] = {} + seen = {start} + while frontier: + node = frontier.pop(0) + for nxt, fact in sorted(supers.get(node, ()), key=lambda e: e[0]): + if nxt in seen: + continue + came_from[nxt] = (node, fact) + if nxt == target: + chain: list[RealizedRecord] = [] + cur = target + while cur != start: + prev, fact = came_from[cur] + chain.append(fact) + cur = prev + return tuple(reversed(chain)) + seen.add(nxt) + frontier.append(nxt) + return None + + +def _determine_subsumption( + ctx: SessionContext, predicate: str, subject: str, target: str +) -> Determined | None: + """Decide a member/subset query by SOUND transitive is-a chaining, or ``None`` when + no sound chain entails it (the caller then refuses, open-world). + + Search-then-verify. Reachability over the SOUND is-a edges finds a candidate chain — + ``subset ∘ subset`` for a subset query, ``member ∘ subset*`` for a member query — + then the proof_chain ROBDD VERIFIES that chain's propositional entailment (O(path) + premises; full O(n³) grounding overruns the canonicalizer, and transitive closure is + reachability, not general SAT). ``member ∘ member`` is NEVER an edge, so the + instance-of fallacy ("Socrates is a man" + "man is a species" ⊬ "Socrates is a + species") is unreachable. wrong=0 is structural: only sound edges are traversed AND + the sound+complete decider confirms the derivation. + """ + subsets = recall_realized(ctx, predicate="subset") + if len(subsets) > _SUBSUMPTION_SUBSET_FACT_BUDGET: + return None # bounded — a safe coverage refusal, never an unsound answer + + # subset adjacency: class → [(superclass, fact)], the subclass-of edges. + supers: dict[str, list[tuple[str, RealizedRecord]]] = {} + for f in subsets: + supers.setdefault(f.relation_arguments[0], []).append( + (f.relation_arguments[1], f) + ) + + if predicate == "subset": + path = _subset_path(subject, target, supers) + if not path: # None (unreachable) or () (start==target, not a real subset claim) + return None + return _verify_subsumption(predicate, subject, target, member_fact=None, subset_path=path) + + # member query: a direct membership ``member(subject, b)`` reaches ``target`` iff + # ``b`` subsumes to ``target`` over subset edges (member ∘ subset*). + for m in recall_realized(ctx, subject=subject, predicate="member"): + b = m.relation_arguments[1] + sub_path = _subset_path(b, target, supers) + if sub_path: # ≥1 subset edge from b to target (b == target is the direct case) + verdict = _verify_subsumption( + predicate, subject, target, member_fact=m, subset_path=sub_path + ) + if verdict is not None: + return verdict + return None + + +def _verify_subsumption( + predicate: str, + subject: str, + target: str, + *, + member_fact: RealizedRecord | None, + subset_path: tuple[RealizedRecord, ...], +) -> Determined | None: + """Verify a found is-a chain with the proof_chain ROBDD and, on ENTAILED, return the + Determined. The propositional theory is LINEAR in the path (the facts on the chain as + true atoms + the sound rule instantiated at each hop), so it scales — unlike the full + closure grounding. Returns ``None`` if the decider does not confirm entailment + (defence in depth: a path-construction bug cannot produce a wrong assertion).""" + atoms: dict[tuple[str, str, str], str] = {} + + def atom(p: str, a: str, b: str) -> str: + key = (p, a, b) + name = atoms.get(key) + if name is None: + name = f"x{len(atoms)}" + atoms[key] = name + return name + + premises: list[str] = [] + # Walk the subset path, asserting each edge and the sound rule that extends the chain. + if predicate == "member": + assert member_fact is not None + cur = member_fact.relation_arguments[1] + premises.append(atom("M", subject, cur)) # member(subject, b) is told + for fact in subset_path: + nxt = fact.relation_arguments[1] + premises.append(atom("S", cur, nxt)) # subset(cur, nxt) is told + premises.append( # member ∘ subset → member + f"({atom('M', subject, cur)} & {atom('S', cur, nxt)}) -> {atom('M', subject, nxt)}" + ) + cur = nxt + query_atom = atom("M", subject, target) + else: + cur = subject + for hop, fact in enumerate(subset_path): + nxt = fact.relation_arguments[1] + premises.append(atom("S", cur, nxt)) # subset(cur, nxt) is told + if hop > 0: # the first told edge IS the accumulator S_subject_c1; extend it + premises.append( # subset ∘ subset → subset + f"({atom('S', subject, cur)} & {atom('S', cur, nxt)}) -> {atom('S', subject, nxt)}" + ) + cur = nxt + query_atom = atom("S", subject, target) + + from generate.proof_chain.entail import Entailment, evaluate_entailment + + if evaluate_entailment(tuple(premises), query_atom).outcome is not Entailment.ENTAILED: + return None + + grounds = ((member_fact,) if member_fact is not None else ()) + subset_path return Determined( answer=True, - basis=_basis((grounding,)), + basis=_basis(grounds), predicate=predicate, subject=subject, object=target, - grounds=(grounding,), + grounds=grounds, ) diff --git a/tests/test_determine_d0.py b/tests/test_determine_d0.py index 152ddb60..f7d0e572 100644 --- a/tests/test_determine_d0.py +++ b/tests/test_determine_d0.py @@ -139,11 +139,13 @@ def test_unsupported_query_predicate_is_refused(vocab_persona) -> None: ctx = _ctx(vocab_persona) _tell("Truth is a concept.", ctx) span = MeaningSpan(source_id="input", start=0, end=5, text="dummy") - subset_q = Comprehension( + # `subset` is supported from Step C; `disjoint` (a non-subsumption categorical) + # stays out of the supported set and is the honest refusal here. + disjoint_q = Comprehension( meaning_graph=MeaningGraph(), - queries=(Query("subset", ("concept", "thought"), span),), + queries=(Query("disjoint", ("concept", "thought"), span),), ) - res = determine(subset_q, ctx) + res = determine(disjoint_q, ctx) assert isinstance(res, Undetermined) and res.reason == "unsupported_query" diff --git a/tests/test_determine_transitive.py b/tests/test_determine_transitive.py new file mode 100644 index 00000000..81965125 --- /dev/null +++ b/tests/test_determine_transitive.py @@ -0,0 +1,145 @@ +"""DETERMINE — transitive subsumption (Step C). + +When direct entailment misses, a member/subset query may still hold by SOUND is-a +chaining: ``member ∘ subset*`` and ``subset ∘ subset`` (Description-Logic subsumption), +decided by search (reachability over the sound edges) then verified by the proof_chain +ROBDD. ``member ∘ member`` is NEVER an edge. + +The load-bearing wrong=0 bite: the instance-of fallacy ("Socrates is a man" + "man is a +species" ⊬ "Socrates is a species") MUST refuse — if it ever determines, an unsound +member∘member rule was smuggled in. +""" + +from __future__ import annotations + +import pytest + +from chat.runtime import ChatRuntime +from generate.determine import Determined, Undetermined, determine +from generate.meaning_graph.reader import comprehend +from generate.realize import realize_comprehension +from session.context import SessionContext + +_HIGH = 10**9 + + +@pytest.fixture(scope="module") +def vocab_persona(): + rt = ChatRuntime(no_load_state=True) + return rt._context.vocab, rt._context.persona + + +def _ctx(vocab_persona) -> SessionContext: + vocab, persona = vocab_persona + return SessionContext(vocab=vocab, persona=persona, vault_reproject_interval=_HIGH) + + +def _tell(text: str, ctx: SessionContext): + return realize_comprehension(comprehend(text), ctx) + + +def _ask(text: str, ctx: SessionContext): + return determine(comprehend(text), ctx) + + +# --------------------------------------------------------------------------- # +# Sound subsumption: the engine reasons across told facts +# --------------------------------------------------------------------------- # + + +def test_member_subset_syllogism(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("Socrates is a man.", ctx) + _tell("All men are mortals.", ctx) + res = _ask("Is Socrates a mortal?", ctx) # member ∘ subset + assert isinstance(res, Determined) + assert res.answer is True and res.basis == "as_told" + assert res.predicate == "member" and res.subject == "socrates" and res.object == "mortal" + + +def test_multi_hop_subsumption(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("Socrates is a man.", ctx) + _tell("All men are mortals.", ctx) + _tell("All mortals are beings.", ctx) + res = _ask("Is Socrates a being?", ctx) # member ∘ subset ∘ subset + assert isinstance(res, Determined) and res.answer is True + + +def test_subset_transitivity(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("All dogs are mammals.", ctx) + _tell("All mammals are animals.", ctx) + res = _ask("Are all dogs animals?", ctx) # subset ∘ subset + assert isinstance(res, Determined) and res.answer is True and res.predicate == "subset" + + +def test_grounds_are_the_chain(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("Socrates is a man.", ctx) + _tell("All men are mortals.", ctx) + res = _ask("Is Socrates a mortal?", ctx) + preds = sorted(g.relation_predicate for g in res.grounds) + assert preds == ["member", "subset"] # the member fact + the subset edge on the path + + +def test_long_chain_scales(vocab_persona) -> None: + # search-then-verify is O(path); a deep chain still determines (no O(n³) blowup). + ctx = _ctx(vocab_persona) + syms = [f"glorp{i}" for i in range(11)] + for i in range(10): + _tell(f"All {syms[i]}s are {syms[i + 1]}s.", ctx) + _tell("Socrates is a glorp0.", ctx) + res = _ask("Is Socrates a glorp10?", ctx) + assert isinstance(res, Determined) and res.answer is True + + +# --------------------------------------------------------------------------- # +# wrong=0 BITE — the instance-of fallacy MUST refuse (no member∘member) +# --------------------------------------------------------------------------- # + + +def test_socrates_species_fallacy_refused(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("Socrates is a man.", ctx) # member(socrates, man) + _tell("Man is a species.", ctx) # member(man, species) — NOT subset + res = _ask("Is Socrates a species?", ctx) + # member ∘ member is never chained → the fallacy is unreachable. + assert isinstance(res, Undetermined) + assert res.reason in {"not_entailed", "ungrounded"} + + +def test_no_sound_chain_refuses_open_world(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("All dogs are mammals.", ctx) + _tell("All mammals are animals.", ctx) + res = _ask("Are all dogs reptiles?", ctx) # no edge to reptile + assert isinstance(res, Undetermined) and res.reason == "not_entailed" + + +def test_reverse_direction_not_entailed(vocab_persona) -> None: + # subset is directional: dogs ⊆ animals does NOT give animals ⊆ dogs. + ctx = _ctx(vocab_persona) + _tell("All dogs are mammals.", ctx) + _tell("All mammals are animals.", ctx) + res = _ask("Are all animals dogs?", ctx) + assert isinstance(res, Undetermined) + + +# --------------------------------------------------------------------------- # +# Direct entailment is unchanged; subset direct now answers +# --------------------------------------------------------------------------- # + + +def test_direct_member_still_determines(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("Truth is a concept.", ctx) + res = _ask("Is truth a concept?", ctx) + assert isinstance(res, Determined) and res.answer is True + + +def test_direct_subset_now_determines(vocab_persona) -> None: + ctx = _ctx(vocab_persona) + _tell("All dogs are mammals.", ctx) + res = _ask("Are all dogs mammals?", ctx) # direct subset fact + assert isinstance(res, Determined) and res.answer is True and res.predicate == "subset" diff --git a/tests/test_relational_reader.py b/tests/test_relational_reader.py index ac4233a7..572c3f17 100644 --- a/tests/test_relational_reader.py +++ b/tests/test_relational_reader.py @@ -258,11 +258,24 @@ def test_ungrounded_relation_refuses(vocab_persona) -> None: assert isinstance(res, Undetermined) and res.reason == "ungrounded" -def test_categorical_predicate_stays_excluded(vocab_persona) -> None: - # DETERMINE must NOT admit categorical predicates (subset/disjoint/…): their truth - # is not a stored-pair lookup, so a direct-entailment answer would be unsound. +def test_subset_supported_other_categoricals_excluded(vocab_persona) -> None: + # C admits `subset` (direct + transitive subsumption is sound); the OTHER + # categoricals (disjoint/intersects/some_not) stay EXCLUDED — their truth is not a + # stored-pair lookup and there is no sound is-a chain for them. + from generate.meaning_graph.model import Entity, MeaningGraph, MeaningSpan + from generate.meaning_graph.reader import Query + ctx = _ctx(vocab_persona) subset_q = comprehend("Are all men mortals?") assert isinstance(subset_q, Comprehension) and subset_q.queries[0].predicate == "subset" - res = determine(subset_q, ctx) - assert isinstance(res, Undetermined) and res.reason == "unsupported_query" + # subset is supported now: nothing realized → ungrounded (NOT unsupported_query) + assert determine(subset_q, ctx).reason == "ungrounded" + + # a disjoint query is still refused as out-of-supported-set + span = MeaningSpan("input", 0, 3, "x y") + graph = MeaningGraph( + entities=(Entity("a", "a", span, "class"), Entity("b", "b", span, "class")), + relations=(), + ) + disjoint_q = Comprehension(meaning_graph=graph, queries=(Query("disjoint", ("a", "b"), span),)) + assert determine(disjoint_q, ctx).reason == "unsupported_query"