feat(determine): transitive subsumption — sound is-a reasoning over accrued knowledge (Step C)
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).
This commit is contained in:
Shay
parent
ea4ed4abb3
commit
cd1a9cbe80
4 changed files with 348 additions and 28 deletions
|
|
@ -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,
|
||||
)
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
|
||||
|
||||
|
|
|
|||
145
tests/test_determine_transitive.py
Normal file
145
tests/test_determine_transitive.py
Normal file
|
|
@ -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"
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Reference in a new issue