cd1a9cbe80
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).
145 lines
5.5 KiB
Python
145 lines
5.5 KiB
Python
"""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"
|