diff --git a/chat/data/deduction_serve_ledger.json b/chat/data/deduction_serve_ledger.json index 6ef01f79..2d0eb3c7 100644 --- a/chat/data/deduction_serve_ledger.json +++ b/chat/data/deduction_serve_ledger.json @@ -62,9 +62,37 @@ "t2_agrees_gold": 0, "t2_verified": 0, "wrong": 0 + }, + "en_member_atomic": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_member_chain": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_member_negative": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 + }, + "en_member_single": { + "correct": 720, + "refused": 0, + "t2_agrees_gold": 0, + "t2_verified": 0, + "wrong": 0 } }, - "content_sha256": "e89aee8fe4c99e9db6e79b3d98278c3ee9e9dcacbc4ba19598fc16d4cf048881", + "content_sha256": "3fa864444de56e9e316e8509d3b84648215af73e86540b10199d51182cb7d5ca", "note": "Sealed-practice committed ledger for deduction serving (ADR-0256). Engine reads, never writes. Ceilings stay at safe defaults (theta_SERVE=0.99). A band earns SERVE by demonstrated pipeline reliability (reader+projector+engine) at volume >= 657 committed.", "provenance": "evals.deduction_serve.practice.runner.seal_ledger", "schema": "deduction_serve_ledger_v1" diff --git a/chat/deduction_surface.py b/chat/deduction_surface.py index 7694f2ae..02e8fb5d 100644 --- a/chat/deduction_surface.py +++ b/chat/deduction_surface.py @@ -22,6 +22,11 @@ Bands (docs/research/deduction-serve-arc-phase0-baseline-2026-07-23.md): ground is wet."), read by ``generate.proof_chain.english`` and decided by the same engine. Tried strictly AFTER v1/v1b (a fallback tier), so every argument those bands serve is served byte-identically; this band only widens coverage. +- Band v3-MEM (ADR-0258) — singular-membership arguments with universal + premises ("Socrates is a man. All men are mortal. Therefore Socrates is + mortal."), read by ``generate.proof_chain.member`` via per-individual + propositional lowering and decided by the same engine. Tried strictly AFTER + v2-EN (which guards these shapes out) — again a pure widening tier. Fail-closed (INV-34): once ``looks_like_deductive_argument`` fires, every path below returns a committed, honest surface — reader refusal, out-of-band shape, @@ -41,9 +46,11 @@ from generate.meaning_graph.reader import Comprehension, comprehend from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import evaluate_entailment_with_trace +from generate.proof_chain.member import MemberArgument, read_member_argument from generate.proof_chain.render import ( render_entailment, render_entailment_english, + render_entailment_member, render_syllogism, ) from generate.proof_chain.shape import CATEGORICAL, classify_deduction_shape @@ -122,6 +129,9 @@ def deduction_grounded_surface( english = _english_band_surface(text, license_lookup) if english is not None: return english + member = _member_band_surface(text, license_lookup) + if member is not None: + return member return _READER_REFUSAL_SURFACE.format(reason=comp.reason) # Band v1 — propositional argument. projected = to_deductive_logic(comp) @@ -146,6 +156,10 @@ def deduction_grounded_surface( english = _english_band_surface(text, license_lookup) if english is not None: return english + # Band v3-MEM fallback — the membership/universal shapes v2-EN guards out. + member = _member_band_surface(text, license_lookup) + if member is not None: + return member return _OUT_OF_BAND_SURFACE @@ -162,6 +176,19 @@ def _english_band_surface(text: str, license_lookup: _LicenseLookup) -> str | No return _license_gate(surface, arg.band, license_lookup) +def _member_band_surface(text: str, license_lookup: _LicenseLookup) -> str | None: + """Band v3-MEM (ADR-0258): read *text* as a singular-membership argument, + lower per-individual, and decide with the same verified ROBDD engine; + ``None`` when the member reader refuses (the caller keeps its pre-existing + honest surface — this band only ever widens what is decided).""" + arg = read_member_argument(text) + if not isinstance(arg, MemberArgument): + return None + trace = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula) + surface = render_entailment_member(trace, arg.premise_texts, arg.query_text) + return _license_gate(surface, arg.band, license_lookup) + + def _license_gate(surface: str, band: str, license_lookup: _LicenseLookup) -> str: """Serve *surface* authoritatively iff *band* holds a SERVE license; else serve the same sound answer DISCLOSED (hedged). The one place the earned- diff --git a/core/cli_test.py b/core/cli_test.py index ea507bfe..a82d7305 100644 --- a/core/cli_test.py +++ b/core/cli_test.py @@ -178,6 +178,7 @@ TEST_SUITES: dict[str, tuple[str, ...]] = { "tests/test_deduction_serve_license.py", "tests/test_categorical_decider.py", "tests/test_english_argument_reader.py", + "tests/test_member_argument_reader.py", "tests/test_deduction_serve_e2e.py", ), "full": ("tests/",), diff --git a/docs/adr/ADR-0258-member-chain-band.md b/docs/adr/ADR-0258-member-chain-band.md new file mode 100644 index 00000000..2744cfa2 --- /dev/null +++ b/docs/adr/ADR-0258-member-chain-band.md @@ -0,0 +1,148 @@ +# ADR-0258 — Member-chain band (Band v3-MEM): singular membership + universal premises + +- **Status:** Proposed +- **Date:** 2026-07-23 +- **Relates to:** ADR-0257 (Band v2-EN — this is its scope-out #1), ADR-0256 + (earned license), ADR-0201 (ROBDD keystone), ADR-0175/0199 (calibrated + learning / arena), ADR-0253 (dual-pack serve boundary — grc/he) + +## 1. Context + +ADR-0257 §6.1 reserved the classic instantiation syllogism as the next band: + +> "Socrates is a man. All men are mortal. Therefore Socrates is mortal." + +Band v2-EN refuses it (`membership_shape_out_of_band` — an `is a|an` clause +announces internal structure the opaque band must not flatten), Band v1b's +categorical decider has no notion of an *individual* (its terms are classes), +and the v1 propositional reader declines multi-word names. The eval lane pins +the gap: `ds-en-0022` is gold-`declined` purely for want of a reading band. +The engine underneath was never the limit. + +## 2. Decision + +Add a dedicated **member-argument reader + per-individual propositional +lowering** (`generate/proof_chain/member.py`), used ONLY by the deduction +serving path as a fallback tier strictly AFTER Bands v1 / v1b / v2-EN (so +every previously-served argument is byte-identical; this band only widens): + +- **Closed sentence grammar** (function-word dispatch, refusal-first): + - Singular fact — ` is [not] [a|an] ` (contractions expanded, + plus the sentential `it is not the case that ` prefix). `` + and `` are opaque token runs; `is` only (no tense in v1). + - Universal — `all|every|each are|is [a|an] ` (affirmative A-form) + and `no are|is [a|an] ` (negative E-form). + - Conclusion — final sentence, sole `therefore`-led, **singular form only**. +- **Per-individual propositional lowering:** collect the named individuals + (subjects of singular sentences, conclusion included); mint one opaque atom + per *(individual, class)* pair; each universal instantiates at EVERY named + individual — `A(C1,C2)` ⇒ `mem(i,C1) -> mem(i,C2)`, `E(C1,C2)` ⇒ + `mem(i,C1) -> ~mem(i,C2)` for each `i`; singular facts are literals. The + same verified ROBDD engine decides; deterministic templates render the + verdict over the user's own sentences + (`generate/proof_chain/render.py::render_entailment_member`). +- **Number linking (the one semantic identification this band performs):** + a universal's class word is usually plural ("all men") while the singular + fact uses the singular ("a man"). Two *attested* class tokens are identified + iff related by a **closed morphology table** — a curated irregular/invariant + table (men↔man, people↔person, children↔child, …; invariants like sheep, + species, news map only to themselves) consulted FIRST, then the three + regular suffix rules (`+s`, `+es` after sibilants, `y↔ies`). Table priority + kills the over-link hazards (specie/species, new/news); anything the closed + relation cannot relate stays distinct — under-linking costs coverage + (honest UNKNOWN), never soundness. Linking is per-token, so multi-token + classes ("guard dog"↔"guard dogs") link on the head noun. +- **Four new shape-bands** — `en_member_single` (exactly 1 universal), + `en_member_chain` (≥2 universals), `en_member_negative` (any E-form), + `en_member_atomic` (0 universals); priority negative > chain > single > + atomic — each **earning its own SERVE license** through the ADR-0199 arena + at n=720/band wrong=0, sealed into the same ratified ledger (unlicensed ⇒ + automatically hedged, per ADR-0256). + +## 3. Why the lowering is sound (the load-bearing argument) + +1. **Universal instantiation is sound.** Every first-order model of + `∀x (C1(x) → C2(x))` satisfies its instantiation at each named individual, + so any model of the premises is a model of the lowered premise set. An + ENTAILED/REFUTED/inconsistent verdict over the lowered set therefore holds + in every model of the original premises — served at full strength. Both + verdicts survive even if two distinct names co-refer: adding equality + facts only ADDS premises, and entailment is monotone. +2. **For this closed fragment the lowering is also complete.** With premises + restricted to singular literals and A/E universals (Boolean reading, no + existential import) and a singular conclusion, a propositional countermodel + lifts to a first-order countermodel whose domain is exactly the named + individuals — every universal holds because every element is a named + individual whose instantiation holds. So UNKNOWN means genuinely not + forced *within the disclosed reading* — it is never an artifact of + instantiating too little. +3. **UNKNOWN is still the one guarded verdict.** Two readings could settle + what the lowering leaves open: distinct names might co-refer, and class + words the closed relation didn't link might be the same class. The UNKNOWN + surface therefore scopes itself — *"Reading each name as one individual + and each class word at face value…"* — same discipline as v2-EN's + indivisible-clause scoping (ADR-0257 §3). +4. **Existential forms refuse out of band.** `some/most/any/…`-led sentences + assert anonymous witnesses that per-individual lowering cannot represent — + `quantifier_out_of_band`, typed. Pure categorical arguments stay with + Band v1b (tried first, unchanged). + +Structural guards (closed refusal vocabulary, all typed): `quantifier_out_of_band`, +`bare_plural_out_of_band` ("Dogs are loyal" — implicit genericity is a reading +this band refuses to guess), `definite_description_out_of_band` ("is the …" is +identity, not membership), `relative_clause_out_of_band` (`that/which/who` +inside a name or class), `universal_conclusion_out_of_band` (categorical +conclusions belong to v1b), `mixed_structure_out_of_band` (`if/or/either/and` +— conditional-membership fusion is a future band), `internal_negation_unread`, +`structural_leak`, `sentence_shape_out_of_band`, plus the v2-EN sentence +discipline (`question_sentence`, `no_conclusion`, `multiple_conclusions`, +`conclusion_not_last`, `no_premises`, `empty_side`, `empty`) and the honesty +caps (`too_many_premises` at 16, `too_many_atoms` at 24 minted pairs — refuse, +never truncate). + +## 4. What the earned licenses certify + +Same posture as ADR-0257 §4: the license certifies READER fidelity per shape +(the engine cannot be wrong; the reader can hand it the wrong problem). The +arena corpus is synthetic names × a class lexicon chosen to exercise every +row-type of the morphology table (irregular, invariant, `+s`, `+es`, `y↔ies`); +gold is authored by construction and cross-checked against the truth-table +oracle over the template's INTENDED instantiated formulas — no reader in the +loop (INV-25). The hand-authored real-English eval lane +(`evals/deduction_serve/v2_member/`, content disjoint from the synthetic +lexicon) keeps the structural-fidelity claim honest against natural prose, +including the promoted `ds-en-0022` (declined → entailed: this band's designed +acceptance case). + +## 5. Tri-language posture + +Unchanged from ADR-0257 §5 — with one addition: the number-linking table is +CORE's **first morphology table**, and it is exactly the artifact class the +tri-language doctrine says must eventually enter through pack ratification +(ADR-0253). English needs ~30 closed rows; Greek/Hebrew declension is where a +curated morphology pack stops being optional. When a `grc_*`/`he_*` member +band is built, the table moves from module constants to a ratified pack; no +premature parameterization now. + +## 6. Scope-outs (deliberate) + +1. **Conditional–membership fusion** ("If Socrates is a man then …") — + refuses `mixed_structure_out_of_band`; a future band composes the v2-EN + connective grammar with this band's sentence readings. +2. **Existential premises/conclusions** (`some …`) — needs witness semantics; + pure categorical `some` stays with Band v1b. +3. **Tense** (`was/were`) and **verb predicates** ("Socrates runs") — refuse; + verb morphology is ADR-0257 scope-out #2's territory. +4. **Identity / definite descriptions / co-reference** — refuse + (`definite_description_out_of_band`); an equality-aware band is future work. +5. **Flag posture unchanged:** rides `deduction_serving_enabled` (default + off); no new flag. + +## 7. Verification + +- `uv run core test --suite deductive -q` — reader contract, surfaces, + license, all three lane splits, e2e through `ChatRuntime`. +- Practice arena: 13 bands × 720 = 9,360 cases, wrong=0 required for every + band; ledger re-sealed (`chat/data/deduction_serve_ledger.json`). +- Eval lane: v1 28/28, v2_en 26/26 (ds-en-0022 promoted), v2_member new — + wrong=0; report re-pinned (`scripts/verify_lane_shas.py`). diff --git a/docs/research/member-chain-band-2026-07-23.md b/docs/research/member-chain-band-2026-07-23.md new file mode 100644 index 00000000..7e74b8c6 --- /dev/null +++ b/docs/research/member-chain-band-2026-07-23.md @@ -0,0 +1,84 @@ +# Band v3-MEM: the Socrates syllogism, decided (ADR-0258) + +**Date:** 2026-07-23 · **Arc:** deduction-serve, band 4 of the cascade +**ADR:** ADR-0258 (Proposed) · **Flag:** `deduction_serving_enabled` (default off, unchanged) + +## What CORE serves now (flag-on transcripts) + +Decided, from the real `core chat` spine, rendered over the user's own +sentences — none of these were decidable yesterday: + +> **Socrates is a man. All men are mortal. Therefore Socrates is mortal.** +> → Given: socrates is a man; all men are mortal. Your premises entail: socrates is mortal. + +> **Tweety is a canary. All canaries are birds. No birds are reptiles. +> Therefore Tweety is not a reptile.** +> → …Your premises entail: tweety is not a reptile. + +> **Socrates is mortal. All men are mortal. Therefore Socrates is a man.** +> → …Reading each name as one individual and each class word at face value, +> your premises don't settle whether socrates is a man — it holds in some +> cases and fails in others. + +`ds-en-0022` — the eval-lane case pinned as `declined` purely for want of a +reading band — is promoted to decided (`entailed`), exactly as ADR-0257 §6.1 +reserved. + +## Mechanism (one new module, everything else reused) + +`generate/proof_chain/member.py` — closed sentence grammar (singular +` is [not] [a|an] ` facts; `all|every|each`/`no` universals) + +**per-individual propositional lowering**: one opaque minted atom per +*(individual, class)* pair; every universal instantiates at every named +individual; the SAME verified ROBDD engine decides. Composer tier strictly +after v1 → v1b → v2-EN: monotone widening, previously-served arguments +byte-identical (v1 lane 28/28 unchanged). + +**Soundness (ADR-0258 §3):** universal instantiation is truth-preserving in +every first-order model ⇒ ENTAILED/REFUTED/inconsistent served at full +strength (they even survive co-reference of distinct names — added premises, +monotone entailment). For this fragment (singular literals + A/E universals, +singular conclusion, Boolean reading) the lowering is also **complete**: a +propositional countermodel lifts to a first-order countermodel over exactly +the named individuals, so UNKNOWN is genuinely "not forced" — and its surface +still scopes itself to the disclosed reading. + +**Number linking — the one semantic identification:** "all men" must bind "a +man". Two *attested* class forms identify iff related by a closed morphology +table (irregular + invariant rows consulted first — table membership makes it +the sole authority, killing specie/species and new/news over-links) then +three regular suffix rules. Under-linking costs coverage, never soundness. +This is CORE's first morphology table — the artifact class the tri-language +doctrine routes through pack ratification when grc/he siblings land. + +**Refusal-first:** existential quantifiers and quantifier pronouns +(`some/everyone/nobody`), bare plurals ("Dogs are loyal"), definite +descriptions ("is the philosopher"), relative clauses, tense, mixed +connectives, universal conclusions — all typed refusals, never guesses. + +## Earned, not flagged (ADR-0256 discipline) + +- Four new shape-bands — `en_member_single/chain/negative/atomic` — each + earned SERVE at the arena: **13 bands × 720 = 9,360 cases, wrong=0**, + reliability 0.99087 ≥ θ_SERVE=0.99; ledger re-sealed + (`chat/data/deduction_serve_ledger.json`, 13 bands, self-verifying sha). +- Arena gold is by-construction and cross-checked against the truth-table + oracle over each template's INTENDED instantiated formulas — no reader in + the loop (INV-25). The synthetic class lexicon deliberately exercises every + number-table row-type, so the license certifies the linking relation too. +- New hand-authored real-English lane `evals/deduction_serve/v2_member/` + (26 cases, content-disjoint): **26/26**, alongside v1 **28/28** and v2_en + **26/26** (wrong=0 everywhere); report re-pinned. + +## Verification + +- `core test --suite deductive`: **127 passed** (41-test reader contract new). +- Practice arena: `all_bands_serve_licensed=True wrong_is_zero=True` (13 bands). +- Lane splits: v1 28/28 · v2_en 26/26 · v2_member 26/26. +- Smoke suite: green (pre-push gate). + +## Scope-outs (deliberate, ADR-0258 §6) + +Conditional–membership fusion; existential premises; tense + verb predicates +("Socrates runs"); identity/definite descriptions/co-reference. Each refuses +typed today — refusal telemetry marks which band pays next. diff --git a/evals/deduction_serve/contract.md b/evals/deduction_serve/contract.md index 637593de..6b60bd10 100644 --- a/evals/deduction_serve/contract.md +++ b/evals/deduction_serve/contract.md @@ -1,17 +1,28 @@ -# Deduction-serve lane contract (v1) +# Deduction-serve lane contract ## What this lane scores The **production serving decider** — the exact pipeline `chat/deduction_surface.py::deduction_grounded_surface` runs on a `core chat` turn: `looks_like_deductive_argument` (commit gate) → -`comprehend` (reader) → `to_deductive_logic` (projector) → -`evaluate_entailment_with_trace` (the ROBDD engine, ADR-0201/ADR-0218). +`comprehend` (reader) → the band cascade — `to_deductive_logic` (Band v1) +→ `to_syllogism` + the categorical decider (Band v1b, ADR-0256) → +`read_english_argument` (Band v2-EN, ADR-0257) → `read_member_argument` +(Band v3-MEM, ADR-0258) — with `evaluate_entailment_with_trace` (the +ROBDD engine, ADR-0201/ADR-0218) deciding every band. `evals/deduction_serve/runner.py::decide` calls these functions directly (typed outcome, not rendered prose) — the same production decision the composer makes, without re-deriving the presentation step -(`generate.proof_chain.render.render_entailment`), so this lane's pinned -bytes stay stable against wording-only changes. +(`generate.proof_chain.render`), so this lane's pinned bytes stay stable +against wording-only changes. + +## Splits + +- `v1/` — the original corpus (single-token propositional + categorical). +- `v2_en/` — hand-authored REAL-English clause arguments (ADR-0257); + content disjoint from the synthetic practice lexicon. +- `v2_member/` — hand-authored membership/universal arguments (ADR-0258), + incl. real nouns across every number-link row-type. This is **distinct** from two existing lanes that sound similar: @@ -48,22 +59,25 @@ corpus, since every committed case reads as an argument by design). `correct` — the lane rewards honest recognition of the boundary, not just committed accuracy. -## Known Band v1 boundaries this corpus documents +## Band-boundary history this corpus documents -Discovered while authoring v1 (each is a genuine reader-grammar limit, -not a lane bug): +Boundaries are DISCOVERED as declines, then PROMOTED to decided gold when +a later band earns the shape (the corpus keeps the case, renamed +`…_formerly_out_of_band`): -- **Nested negation inside `if/then`** — `generate/meaning_graph/reader.py`'s - `_parse_propositional` accepts `not P` only as a top-level clause; - `"if not q then not p"` fails `_chunk`'s reserved-word guard (`not` is in - `_RESERVED`) when it appears *inside* an if/then slot. `ds-v1-0006` - documents this (`out_of_band_nested_negation`). -- **Multi-word English propositions** — `ds-v1-0025` - (`out_of_band_multiword_conditional`), matching the Phase 0 baseline's - band-boundary finding. -- **Categorical/syllogism shapes** — `ds-v1-0023/0024/0026` - (`out_of_band_categorical`); Band v1b (a production categorical decider) - is deferred. +- **Nested negation inside `if/then`** — a shared-reader grammar limit + (`not` is reserved inside if/then slots); `ds-v1-0006` declined until + Band v2-EN decided it (promoted, ADR-0257). +- **Multi-word English propositions** — `ds-v1-0025` declined until Band + v2-EN (promoted, ADR-0257). +- **Categorical/syllogism shapes** — `ds-v1-0023/0024/0026`, decided by + Band v1b since ADR-0256. +- **`is a` membership** — `ds-en-0022` declined until Band v3-MEM decided + it (promoted, ADR-0258). +- **Still-open declines** (honest, typed): verb-phrase negation + (`ds-en-0023/0024`), ambiguous `and`/`or` scope (`ds-en-0025`), nested + conditionals (`ds-en-0026`), existential quantifiers / bare plurals / + definite descriptions / relative clauses / tense (`ds-mem-0020…0026`). ## Reproduce diff --git a/evals/deduction_serve/practice/gold.py b/evals/deduction_serve/practice/gold.py index 538a3481..7afd5c33 100644 --- a/evals/deduction_serve/practice/gold.py +++ b/evals/deduction_serve/practice/gold.py @@ -35,6 +35,7 @@ from generate.meaning_graph.reader import Comprehension, comprehend from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.member import MemberArgument, read_member_argument from generate.proof_chain.shape import ( ATOMIC, CATEGORICAL, @@ -45,6 +46,10 @@ from generate.proof_chain.shape import ( EN_CONDITIONAL_CHAIN, EN_CONDITIONAL_SINGLE, EN_DISJUNCTIVE, + EN_MEMBER_ATOMIC, + EN_MEMBER_CHAIN, + EN_MEMBER_NEGATIVE, + EN_MEMBER_SINGLE, classify_deduction_shape, ) @@ -239,10 +244,155 @@ _EN_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { ), } -#: Ledger band order: the five v1 bands, then the four v2-EN bands. +# --- Band v3-MEM (ADR-0258): member-argument synthetic corpus ----------------- +# +# Names × class-noun (singular, plural) pairs × state adjectives. The class +# lexicon deliberately exercises EVERY row-type of the reader's closed number +# table — irregular (man/men, person/people, child/children, wolf/wolves, +# mouse/mice, goose/geese), invariant (sheep, fish), and each regular suffix +# rule (+s, +es, y↔ies) — so the earned license certifies the linking relation +# itself, not just the sentence grammar. Content is synthetic ON PURPOSE +# (same posture as the v2-EN corpus above); hand-authored real-English cases +# live in ``evals/deduction_serve/v2_member``. + +_MEM_NAMES: tuple[str, ...] = ( + "Rex", "Ada", "Kai", "Milo", "Nova", "Otis", "Pia", "Quinn", "Rio", "Sol", + "Tara", "Ugo", "Vera", "Wren", "Yara", "Zed", "Bo", "Cyra", "Dax", "Elio", +) +_MEM_CLASSES: tuple[tuple[str, str], ...] = ( + ("man", "men"), ("person", "people"), ("child", "children"), + ("wolf", "wolves"), ("mouse", "mice"), ("goose", "geese"), + ("sheep", "sheep"), ("fish", "fish"), + ("cat", "cats"), ("dog", "dogs"), ("fox", "foxes"), ("pony", "ponies"), +) +_MEM_STATES: tuple[str, ...] = ( + "mortal", "loyal", "wild", "tame", "swift", "calm", + "bold", "shy", "warm", "quiet", "brave", "free", +) + + +def _mem_case(index: int) -> tuple[str, str, tuple[str, str], tuple[str, str], tuple[str, str], str]: + """Deterministic (name1, name2, class1, class2, class3, state) for case + ``index`` — names and the three classes are always pairwise distinct.""" + n1 = _MEM_NAMES[(index * 3) % len(_MEM_NAMES)] + n2 = _MEM_NAMES[(index * 3 + 1) % len(_MEM_NAMES)] + base = (index * 5) % (len(_MEM_CLASSES) - 2) + c1, c2, c3 = _MEM_CLASSES[base], _MEM_CLASSES[base + 1], _MEM_CLASSES[base + 2] + state = _MEM_STATES[(index * 7) % len(_MEM_STATES)] + return n1, n2, c1, c2, c3, state + + +#: Member-band templates: (gold, text_builder, intended_premises, intended_query). +#: Builders take ``(n1, n2, c1, c2, c3, st)`` from ``_mem_case``; the INTENDED +#: formulas are the template's per-individual lowering over fixed placeholder +#: atoms (``ma`` = first (individual, class) pair, …), cross-checked against +#: the truth-table oracle with no reader in the loop (INV-25). +_MEM_TEMPLATES: dict[str, tuple[tuple[str, Any, tuple[str, ...], str], ...]] = { + EN_MEMBER_SINGLE: ( + # Instantiated modus ponens onto a state predicate. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n1} is {st}.", + ("ma", "ma implies mb"), "mb"), + # Instantiated modus ponens onto a membership conclusion ("every" spelling). + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Every {c1[0]} is a {c2[0]}. Therefore {n1} is a {c2[0]}.", + ("ma", "ma implies mb"), "mb"), + # Universal stated FIRST ("each" spelling) — order independence. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"Each {c1[0]} is {st}. {n1} is a {c1[0]}. Therefore {n1} is {st}.", + ("ma implies mb", "ma"), "mb"), + # Contradicting the instantiated consequent. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n1} is not {st}.", + ("ma", "ma implies mb"), "not mb"), + # Converse instantiation — affirming the consequent. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. All {c1[1]} are {st}. Therefore {n1} is a {c1[0]}.", + ("mb", "ma implies mb"), "ma"), + # The universal binds a DIFFERENT named individual than the conclusion's. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {st}. Therefore {n2} is {st}.", + ("ma", "ma implies mb", "mc implies md"), "md"), + ), + EN_MEMBER_CHAIN: ( + # Two-hop instantiated chain onto a state. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is {st}.", + ("ma", "ma implies mb", "mb implies mc"), "mc"), + # Two-hop chain onto a MEMBERSHIP conclusion — the conclusion's singular + # article form links to the chain's plural class. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {c3[1]}. Therefore {n1} is a {c3[0]}.", + ("ma", "ma implies mb", "mb implies mc"), "mc"), + # Chain contradiction. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is not {st}.", + ("ma", "ma implies mb", "mb implies mc"), "not mc"), + # Broken chain — the individual's class never enters it. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c2[1]} are {c3[1]}. All {c3[1]} are {st}. Therefore {n1} is {st}.", + ("ma", "mb implies mc", "mc implies md"), "md"), + # Reverse traversal — chains do not run backwards. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. All {c1[1]} are {c2[1]}. All {c2[1]} are {st}. Therefore {n1} is a {c1[0]}.", + ("mc", "ma implies mb", "mb implies mc"), "ma"), + ), + EN_MEMBER_NEGATIVE: ( + # Instantiated E-form onto a state. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is not {st}.", + ("ma", "ma implies not mb"), "not mb"), + # Instantiated E-form onto a membership conclusion. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {c2[1]}. Therefore {n1} is not a {c2[0]}.", + ("ma", "ma implies not mb"), "not mb"), + # A-chain into an E-form. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. All {c1[1]} are {c2[1]}. No {c2[1]} are {st}. Therefore {n1} is not {st}.", + ("ma", "ma implies mb", "mb implies not mc"), "not mc"), + # Contradicting the E-form's instantiation. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is {st}.", + ("ma", "ma implies not mb"), "mb"), + # Denied antecedent under an E-form — nothing follows. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is not a {c1[0]}. No {c1[1]} are {st}. Therefore {n1} is not {st}.", + ("not ma", "ma implies not mb"), "not mb"), + ), + EN_MEMBER_ATOMIC: ( + # Membership restatement (the promoted ds-en-0022 shape). + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is a {c1[0]}.", + ("ma",), "ma"), + # State restatement. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is {st}. Therefore {n1} is {st}.", + ("ma",), "ma"), + # Selection from two facts about one individual. + ("entailed", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. {n1} is {st}. Therefore {n1} is {st}.", + ("ma", "mb"), "mb"), + # Self-contradiction (membership). + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is not a {c1[0]}.", + ("ma",), "not ma"), + # Negated fact contradicted. + ("refuted", + lambda n1, n2, c1, c2, c3, st: f"{n1} is not {st}. Therefore {n1} is {st}.", + ("not ma",), "ma"), + # Unrelated conclusion. + ("unknown", + lambda n1, n2, c1, c2, c3, st: f"{n1} is a {c1[0]}. Therefore {n1} is {st}.", + ("ma",), "mb"), + ), +} + +#: Ledger band order: the five v1 bands, the four v2-EN bands, then the four +#: v3-MEM bands. _ALL_BANDS: tuple[str, ...] = ( CONDITIONAL_SINGLE, CONDITIONAL_CHAIN, DISJUNCTIVE, ATOMIC, CATEGORICAL, EN_CONDITIONAL_SINGLE, EN_CONDITIONAL_CHAIN, EN_DISJUNCTIVE, EN_ATOMIC, + EN_MEMBER_SINGLE, EN_MEMBER_CHAIN, EN_MEMBER_NEGATIVE, EN_MEMBER_ATOMIC, ) @@ -256,6 +406,25 @@ def generate_problems(band: str, n: int) -> list[Problem]: logical form for the reader-independent oracle cross-check. """ problems: list[Problem] = [] + if band in _MEM_TEMPLATES: + templates = _MEM_TEMPLATES[band] + for i in range(n): + gold, builder, intended_premises, intended_query = templates[i % len(templates)] + problems.append( + Problem( + problem_id=f"{band}-{i:04d}", + class_name=band, + payload={ + "text": builder(*_mem_case(i)), + "gold": gold, + "intended": { + "premises": list(intended_premises), + "query": intended_query, + }, + }, + ) + ) + return problems if band in _EN_TEMPLATES: templates = _EN_TEMPLATES[band] for i in range(n): @@ -348,11 +517,15 @@ class DeductionSolver: text = problem.payload["text"] comp = comprehend(text) if not isinstance(comp, Comprehension): - # Band v2-EN fallback — mirrors the composer: the shared reader - # refused, but the English-clause argument reader may read it. + # Band v2-EN / v3-MEM fallbacks — mirror the composer: the shared + # reader refused, but the English-clause or member-argument reader + # may read it. english = self._attempt_english(problem) if english is not None: return english + member = self._attempt_member(problem) + if member is not None: + return member return _DeductionAttempt( committed=False, answer=None, reason=f"reader:{getattr(comp, 'reason', '')}", case_id=problem.problem_id, shape=problem.class_name, @@ -386,6 +559,9 @@ class DeductionSolver: english = self._attempt_english(problem) if english is not None: return english + member = self._attempt_member(problem) + if member is not None: + return member return _DeductionAttempt( committed=False, answer=None, reason="unprojectable", case_id=problem.problem_id, shape=problem.class_name, @@ -406,6 +582,21 @@ class DeductionSolver: case_id=problem.problem_id, shape=arg.band, ) + def _attempt_member(self, problem: Problem) -> _DeductionAttempt | None: + """Band v3-MEM: the member-argument path, or ``None`` when the member + reader refuses (the caller then records the honest decline).""" + arg = read_member_argument(problem.payload["text"]) + if not isinstance(arg, MemberArgument): + return None + outcome = evaluate_entailment_with_trace( + arg.premise_formulas, arg.query_formula + ).outcome + return _DeductionAttempt( + committed=outcome is not Entailment.REFUSED, + answer=_OUTCOME_TO_CLASS[outcome], reason="", + case_id=problem.problem_id, shape=arg.band, + ) + @dataclass(frozen=True, slots=True) class ConstructionGoldTether: diff --git a/evals/deduction_serve/report.json b/evals/deduction_serve/report.json index 98a2d215..22114fe7 100644 --- a/evals/deduction_serve/report.json +++ b/evals/deduction_serve/report.json @@ -1,8 +1,8 @@ { "aggregate": { - "correct": 54, + "correct": 80, "declined": 0, - "n": 54, + "n": 80, "wrong": 0 }, "all_correct": true, @@ -38,14 +38,35 @@ "v2_en": { "all_cases_correct": true, "by_gold": { - "declined": 6, - "entailed": 13, + "declined": 5, + "entailed": 14, "refuted": 3, "unknown": 4 }, "correct_by_gold": { - "declined": 6, - "entailed": 13, + "declined": 5, + "entailed": 14, + "refuted": 3, + "unknown": 4 + }, + "counts": { + "correct": 26, + "declined": 0, + "wrong": 0 + }, + "n": 26 + }, + "v2_member": { + "all_cases_correct": true, + "by_gold": { + "declined": 7, + "entailed": 12, + "refuted": 3, + "unknown": 4 + }, + "correct_by_gold": { + "declined": 7, + "entailed": 12, "refuted": 3, "unknown": 4 }, diff --git a/evals/deduction_serve/runner.py b/evals/deduction_serve/runner.py index a49a3247..bb6a6127 100644 --- a/evals/deduction_serve/runner.py +++ b/evals/deduction_serve/runner.py @@ -47,6 +47,7 @@ from generate.meaning_graph.reader import Comprehension, comprehend from generate.proof_chain.categorical import CategoricalError, decide_syllogism from generate.proof_chain.english import EnglishArgument, read_english_argument from generate.proof_chain.entail import Entailment, evaluate_entailment_with_trace +from generate.proof_chain.member import MemberArgument, read_member_argument _ROOT = Path(__file__).resolve().parent @@ -56,6 +57,10 @@ _SPLITS: tuple[tuple[str, Path], ...] = ( # deliberately disjoint from the synthetic practice lexicon, so the earned # license's structural-fidelity claim is checked against natural prose). ("v2_en", _ROOT / "v2_en" / "cases.jsonl"), + # Band v3-MEM (ADR-0258) — hand-authored membership/universal arguments, + # same content-disjoint discipline (incl. the number-link table on real + # nouns: men, people, children, canaries, sheep). + ("v2_member", _ROOT / "v2_member" / "cases.jsonl"), ) _OUTCOME_TO_CLASS = { @@ -109,9 +114,19 @@ def decide(text: str) -> str: def _decide_english(text: str) -> str: - """Band v2-EN fallback (ADR-0257) — mirrors ``_english_band_surface``.""" + """Band v2-EN fallback (ADR-0257) — mirrors ``_english_band_surface``; + chains into the Band v3-MEM fallback exactly as the composer does.""" arg = read_english_argument(text) if not isinstance(arg, EnglishArgument): + return _decide_member(text) + outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome + return _OUTCOME_TO_CLASS[outcome] + + +def _decide_member(text: str) -> str: + """Band v3-MEM fallback (ADR-0258) — mirrors ``_member_band_surface``.""" + arg = read_member_argument(text) + if not isinstance(arg, MemberArgument): return "declined" outcome = evaluate_entailment_with_trace(arg.premise_formulas, arg.query_formula).outcome return _OUTCOME_TO_CLASS[outcome] diff --git a/evals/deduction_serve/v2_en/cases.jsonl b/evals/deduction_serve/v2_en/cases.jsonl index 0e1870f3..b93035f0 100644 --- a/evals/deduction_serve/v2_en/cases.jsonl +++ b/evals/deduction_serve/v2_en/cases.jsonl @@ -19,7 +19,7 @@ {"id": "ds-en-0019", "text": "The key is lost or the lock is broken. Therefore the key is lost.", "gold": "unknown", "class": "bare_disjunct"} {"id": "ds-en-0020", "text": "The sky is clear. Therefore the sea is calm.", "gold": "unknown", "class": "unrelated_conclusion"} {"id": "ds-en-0021", "text": "The door is open. The door is not open. Therefore the moon is full.", "gold": "declined", "class": "inconsistent_premises"} -{"id": "ds-en-0022", "text": "Socrates is a man. Therefore Socrates is a man.", "gold": "declined", "class": "membership_out_of_band"} +{"id": "ds-en-0022", "text": "Socrates is a man. Therefore Socrates is a man.", "gold": "entailed", "class": "membership_formerly_out_of_band"} {"id": "ds-en-0023", "text": "It never snows. Therefore it never snows.", "gold": "declined", "class": "unnormalizable_negation"} {"id": "ds-en-0024", "text": "The engine doesn't start. Therefore the engine doesn't start.", "gold": "declined", "class": "unnormalizable_negation_contraction"} {"id": "ds-en-0025", "text": "The fan spins and the light is on or the door is open. Therefore the door is open.", "gold": "declined", "class": "ambiguous_and_or"} diff --git a/evals/deduction_serve/v2_member/cases.jsonl b/evals/deduction_serve/v2_member/cases.jsonl new file mode 100644 index 00000000..9a6b4810 --- /dev/null +++ b/evals/deduction_serve/v2_member/cases.jsonl @@ -0,0 +1,26 @@ +{"id": "ds-mem-0001", "text": "Socrates is a man. All men are mortal. Therefore Socrates is mortal.", "gold": "entailed", "class": "instantiated_modus_ponens"} +{"id": "ds-mem-0002", "text": "Ada is a person. All people are mortal. Therefore Ada is mortal.", "gold": "entailed", "class": "irregular_plural_link"} +{"id": "ds-mem-0003", "text": "Rex is a dog. All dogs are mammals. All mammals are animals. Therefore Rex is an animal.", "gold": "entailed", "class": "membership_chain"} +{"id": "ds-mem-0004", "text": "Fido is a dog. No dogs are cats. Therefore Fido is not a cat.", "gold": "entailed", "class": "negative_universal"} +{"id": "ds-mem-0005", "text": "Every child is curious. Milo is a child. Therefore Milo is curious.", "gold": "entailed", "class": "universal_first"} +{"id": "ds-mem-0006", "text": "Tweety is a canary. All canaries are birds. No birds are reptiles. Therefore Tweety is not a reptile.", "gold": "entailed", "class": "chain_into_negative"} +{"id": "ds-mem-0007", "text": "Dolly is a sheep. All sheep are woolly. Therefore Dolly is woolly.", "gold": "entailed", "class": "invariant_plural"} +{"id": "ds-mem-0008", "text": "Rex isn't a cat. Therefore Rex is not a cat.", "gold": "entailed", "class": "contraction_restatement"} +{"id": "ds-mem-0009", "text": "Each planet is round. Mars is a planet. Therefore Mars is round.", "gold": "entailed", "class": "each_spelling"} +{"id": "ds-mem-0010", "text": "Rex is a guard dog. All guard dogs are loyal. Therefore Rex is loyal.", "gold": "entailed", "class": "multi_token_class"} +{"id": "ds-mem-0011", "text": "Plato is a man. Aristotle is a man. All men are mortal. Therefore Aristotle is mortal.", "gold": "entailed", "class": "two_individuals"} +{"id": "ds-mem-0012", "text": "It is not the case that Rex is a cat. Therefore Rex is not a cat.", "gold": "entailed", "class": "sentential_negation"} +{"id": "ds-mem-0013", "text": "Socrates is a man. All men are mortal. Therefore Socrates is not mortal.", "gold": "refuted", "class": "consequent_denial"} +{"id": "ds-mem-0014", "text": "Fido is a dog. No dogs are cats. Therefore Fido is a cat.", "gold": "refuted", "class": "negative_universal_denial"} +{"id": "ds-mem-0015", "text": "Rex is loyal. Therefore Rex is not loyal.", "gold": "refuted", "class": "self_contradiction"} +{"id": "ds-mem-0016", "text": "Socrates is mortal. All men are mortal. Therefore Socrates is a man.", "gold": "unknown", "class": "converse_instantiation"} +{"id": "ds-mem-0017", "text": "Plato is a man. All men are mortal. Therefore Zeus is mortal.", "gold": "unknown", "class": "wrong_individual"} +{"id": "ds-mem-0018", "text": "Rex is a dog. All cats are animals. Therefore Rex is an animal.", "gold": "unknown", "class": "broken_chain"} +{"id": "ds-mem-0019", "text": "Milo is a child. All children are curious. Therefore Milo is happy.", "gold": "unknown", "class": "unrelated_predicate"} +{"id": "ds-mem-0020", "text": "Some men are wise. Socrates is a man. Therefore Socrates is wise.", "gold": "declined", "class": "existential_out_of_band"} +{"id": "ds-mem-0021", "text": "Dogs are loyal. Rex is a dog. Therefore Rex is loyal.", "gold": "declined", "class": "bare_plural_out_of_band"} +{"id": "ds-mem-0022", "text": "Socrates is the philosopher. All philosophers are wise. Therefore Socrates is wise.", "gold": "declined", "class": "definite_description_out_of_band"} +{"id": "ds-mem-0023", "text": "Socrates is a man. All men are mortal. Therefore all men are mortal.", "gold": "declined", "class": "universal_conclusion_out_of_band"} +{"id": "ds-mem-0024", "text": "If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal.", "gold": "declined", "class": "mixed_structure_out_of_band"} +{"id": "ds-mem-0025", "text": "Rex is a dog that barks. All dogs are loyal. Therefore Rex is loyal.", "gold": "declined", "class": "relative_clause_out_of_band"} +{"id": "ds-mem-0026", "text": "Socrates was a man. All men are mortal. Therefore Socrates is mortal.", "gold": "declined", "class": "tense_out_of_band"} diff --git a/generate/proof_chain/member.py b/generate/proof_chain/member.py new file mode 100644 index 00000000..a85666d0 --- /dev/null +++ b/generate/proof_chain/member.py @@ -0,0 +1,430 @@ +"""Member-argument reader — Band v3-MEM (ADR-0258). + +Reads the classic instantiation syllogism — "Socrates is a man. All men are +mortal. Therefore Socrates is mortal." — by **per-individual propositional +lowering**: one opaque minted atom (``a0``, ``a1``, …) per *(individual, +class)* pair, with every universal premise instantiated at every named +individual (``A(C1,C2)`` ⇒ ``mem(i,C1) -> mem(i,C2)``; ``E(C1,C2)`` ⇒ +``mem(i,C1) -> ~mem(i,C2)``). The same verified ROBDD engine decides. + +Why this is sound (ADR-0258 §3): universal instantiation at named individuals +is truth-preserving in every first-order model, so ENTAILED / REFUTED / +inconsistent verdicts over the lowered premises hold in every model of the +original argument — and both survive co-reference of distinct names, since +that only ADDS premises and entailment is monotone. For this closed fragment +(singular literals + A/E universals, singular conclusion, Boolean reading) +the lowering is also COMPLETE: a propositional countermodel lifts to a +first-order countermodel whose domain is exactly the named individuals, so +UNKNOWN means genuinely not forced within the disclosed reading. The UNKNOWN +surface still scopes itself (names read as distinct individuals, class words +at face value), and every sentence shape announcing structure this band +cannot read refuses out of band, typed. + +Number linking — the ONE semantic identification this band performs: a +universal's class word is usually plural ("all men") while the singular fact +uses the singular ("a man"). Two attested class forms are identified iff +related token-wise by a CLOSED relation: the irregular/invariant table below +(consulted first — table membership makes it the sole authority for that +token, killing over-link hazards like specie/species and new/news), else the +three regular suffix rules (``+s``, ``+es`` after sibilants, ``y↔ies``). +Anything the relation cannot relate stays distinct — under-linking costs +coverage, never soundness. + +This reader is used ONLY by the deduction serving path, strictly AFTER Bands +v1 / v1b / v2-EN — pure widening; every previously-served argument is served +byte-identically. Refusal-first, closed reason vocabulary: + + ``empty``, ``question_sentence``, ``no_conclusion``, + ``multiple_conclusions``, ``conclusion_not_last``, ``no_premises``, + ``empty_side``, ``quantifier_out_of_band``, ``bare_plural_out_of_band``, + ``definite_description_out_of_band``, ``relative_clause_out_of_band``, + ``universal_conclusion_out_of_band``, ``mixed_structure_out_of_band``, + ``internal_negation_unread``, ``sentence_shape_out_of_band``, + ``structural_leak``, ``too_many_premises``, ``too_many_atoms``. +""" + +from __future__ import annotations + +from dataclasses import dataclass + +# The v2-EN sentence splitter and tokenizer are reused VERBATIM (one +# normalization discipline, no drift between the English-argument bands) — +# a deliberate private-name import inside the proof_chain package. +from generate.proof_chain.english import _SENTENCE_RE, _tokenize +from generate.proof_chain.shape import ( + EN_MEMBER_ATOMIC, + EN_MEMBER_CHAIN, + EN_MEMBER_NEGATIVE, + EN_MEMBER_SINGLE, +) + +#: Universal-affirmative sentence leads (A-form) and the E-form lead. +_A_LEADS = frozenset({"all", "every", "each"}) +_E_LEAD = "no" + +#: Quantifier tokens (determiners AND pronouns) this band cannot lower — +#: existential/plurality readings refuse rather than misread "everyone" or +#: "some men" as an individual. A/E leads are dispatched before this check. +_QUANTIFIER_TOKENS = frozenset({ + "all", "every", "each", "no", "some", "none", "any", "most", "few", + "many", "several", "both", "either", "neither", + "everyone", "everybody", "everything", "someone", "somebody", + "something", "anyone", "anybody", "anything", "nobody", "nothing", +}) + +#: Connective structure this band does not compose (a future band fuses the +#: v2-EN connective grammar with these sentence readings — ADR-0258 §6.1). +_CONNECTIVES = frozenset({"if", "then", "or", "and", "either"}) + +#: Negation-bearing tokens with no normalized reading here (only the copular +#: ``is not`` slot and the sentential prefix are normalized). +_NEGATION_BEARING = frozenset({ + "not", "never", "cannot", "nor", "neither", "nothing", "none", "no", +}) + +#: Relative-clause markers — internal structure a name/class run must not hide. +_RELATIVE_MARKERS = frozenset({"that", "which", "who", "whom", "whose"}) + +#: All copular forms recognized for DISPATCH; only ``is``/``are`` are in-band +#: (tense is a deliberate scope-out — ADR-0258 §6.3). +_COPULA_FORMS = ("is", "are", "was", "were") + +#: The "it is not the case that " sentential-negation prefix. +_SENTENTIAL_NOT = ("it", "is", "not", "the", "case", "that") + +#: Honesty caps — beyond these the argument is refused, never truncated. +#: ``MAX_ATOMS`` counts minted (individual, class) pairs, so instantiation +#: fan-out (individuals × classes) is capped exactly where it multiplies. +MAX_PREMISE_SENTENCES = 16 +MAX_ATOMS = 24 + +#: Closed irregular/invariant number table (plural → singular; an INVARIANT +#: form maps to itself). Consulted BEFORE the regular suffix rules: if either +#: token of a candidate pair appears anywhere in this table, the table is the +#: only authority for that pair — which is what keeps ``species``/``specie`` +#: and ``news``/``new`` unlinked. CORE's first morphology table; promoted to +#: a ratified pack when the tri-language siblings land (ADR-0258 §5). +_IRREGULAR_PLURALS: dict[str, str] = { + "men": "man", "women": "woman", "people": "person", + "children": "child", "mice": "mouse", "geese": "goose", + "feet": "foot", "teeth": "tooth", "oxen": "ox", + "wolves": "wolf", "knives": "knife", "lives": "life", + "leaves": "leaf", "halves": "half", "elves": "elf", + "loaves": "loaf", "thieves": "thief", "cacti": "cactus", + "fungi": "fungus", "dice": "die", + # invariants (plural == singular) + "sheep": "sheep", "fish": "fish", "deer": "deer", + "species": "species", "series": "series", "means": "means", + "offspring": "offspring", "aircraft": "aircraft", "news": "news", +} +_TABLE_TOKENS = frozenset(_IRREGULAR_PLURALS) | frozenset(_IRREGULAR_PLURALS.values()) + +_SIBILANT_ENDINGS = ("s", "x", "z", "ch", "sh") + + +@dataclass(frozen=True, slots=True) +class MemberArgument: + """A successfully-read member argument, engine-ready. + + ``premise_formulas``/``query_formula`` are propositional formula strings + over minted atom ids; ``atoms[i]`` displays the *(individual, class)* + pair behind ``a{i}``. ``premise_texts``/``query_text`` are the normalized + original sentences — the exact reading the surface restates to the user. + """ + + premise_formulas: tuple[str, ...] + query_formula: str + premise_texts: tuple[str, ...] + query_text: str + band: str + atoms: tuple[str, ...] + + +@dataclass(frozen=True, slots=True) +class MemberRefusal: + """A typed refusal — the argument is not honestly readable by this band.""" + + reason: str + detail: str = "" + + +class _Reject(Exception): + def __init__(self, reason: str, detail: str = "") -> None: + super().__init__(reason) + self.refusal = MemberRefusal(reason, detail) + + +@dataclass(frozen=True, slots=True) +class _Singular: + """`` is [not] [a|an] `` — a literal about one individual.""" + + ind: tuple[str, ...] + cls: tuple[str, ...] + negated: bool + + +@dataclass(frozen=True, slots=True) +class _Universal: + """``all|every|each|no are|is [a|an] `` — instantiated per + individual at lowering time. ``negative`` marks the E-form (``no``).""" + + subject: tuple[str, ...] + predicate: tuple[str, ...] + negative: bool + + +def _tokens_link(a: str, b: str) -> bool: + """True iff single tokens *a* and *b* are number-forms of one class word + under the closed relation (irregular/invariant table first, then the + three regular suffix rules).""" + if a == b: + return True + if a in _TABLE_TOKENS or b in _TABLE_TOKENS: + return _IRREGULAR_PLURALS.get(a) == b or _IRREGULAR_PLURALS.get(b) == a + short, long_ = (a, b) if len(a) <= len(b) else (b, a) + if long_ == short + "s" and not short.endswith(_SIBILANT_ENDINGS): + return True + if long_ == short + "es" and short.endswith(_SIBILANT_ENDINGS): + return True + if short.endswith("y") and long_ == short[:-1] + "ies": + return True + return False + + +def _forms_link(a: tuple[str, ...], b: tuple[str, ...]) -> bool: + """Multi-token class forms link token-wise (head-noun pluralization — + "guard dogs" ↔ "guard dog"); differing lengths never link.""" + return len(a) == len(b) and all(_tokens_link(x, y) for x, y in zip(a, b)) + + +def _check_run(toks: tuple[str, ...], detail: str) -> None: + """Guard an opaque name/class token run: structure it must not hide + refuses out of band, typed. Order matters — quantifier pronouns + (``nobody``) are quantifier refusals, not negation refusals.""" + if not toks: + raise _Reject("empty_side", detail) + for tok in toks: + if tok == "therefore": + raise _Reject("structural_leak", detail) + if tok in _RELATIVE_MARKERS: + raise _Reject("relative_clause_out_of_band", detail) + if tok in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", detail) + if tok in _NEGATION_BEARING or tok.endswith("n't"): + raise _Reject("internal_negation_unread", detail) + if tok in _COPULA_FORMS: + raise _Reject("sentence_shape_out_of_band", detail) + + +def _parse_universal(toks: list[str], detail: str) -> _Universal: + negative = toks[0] == _E_LEAD + rest = toks[1:] + cop_idx = next((i for i, t in enumerate(rest) if t in ("is", "are")), None) + if cop_idx is None: + raise _Reject("sentence_shape_out_of_band", detail) + subject = rest[:cop_idx] + if subject and subject[0] == "the": # "all the dogs" — determiner, dropped + subject = subject[1:] + predicate = rest[cop_idx + 1 :] + if predicate and predicate[0] == "not": + # "All men are not mortal" — genuinely scope-ambiguous English + # (¬∀ vs ∀¬); refuse rather than guess. E-form ("no …") is the + # unambiguous spelling this band reads. + raise _Reject("internal_negation_unread", detail) + if predicate and predicate[0] in ("a", "an"): + predicate = predicate[1:] + elif predicate and predicate[0] == "the": + raise _Reject("definite_description_out_of_band", detail) + _check_run(tuple(subject), detail) + _check_run(tuple(predicate), detail) + return _Universal(tuple(subject), tuple(predicate), negative) + + +def _parse_singular(toks: list[str], detail: str) -> _Singular: + if tuple(toks[: len(_SENTENTIAL_NOT)]) == _SENTENTIAL_NOT: + inner = _parse_singular(toks[len(_SENTENTIAL_NOT) :], detail) + return _Singular(inner.ind, inner.cls, negated=not inner.negated) + cop_idx = next((i for i, t in enumerate(toks) if t in _COPULA_FORMS), None) + if cop_idx is None or toks[cop_idx] in ("was", "were"): + raise _Reject("sentence_shape_out_of_band", detail) + if toks[cop_idx] == "are": + # "Dogs are loyal" — a bare-plural generic is an implicit universal + # this band refuses to guess (ADR-0258 §3). + raise _Reject("bare_plural_out_of_band", detail) + name = tuple(toks[:cop_idx]) + rhs = toks[cop_idx + 1 :] + negated = False + if rhs and rhs[0] == "not": + negated = True + rhs = rhs[1:] + if rhs and rhs[0] in ("a", "an"): + rhs = rhs[1:] + elif rhs and rhs[0] == "the": + # "Socrates is the philosopher" — identity via definite description, + # not class membership (ADR-0258 §6.4). + raise _Reject("definite_description_out_of_band", detail) + _check_run(name, detail) + _check_run(tuple(rhs), detail) + return _Singular(name, tuple(rhs), negated) + + +def _parse_sentence(toks: list[str], detail: str) -> _Singular | _Universal: + if any(t in _CONNECTIVES for t in toks): + raise _Reject("mixed_structure_out_of_band", detail) + head = toks[0] + if head in _A_LEADS or head == _E_LEAD: + return _parse_universal(toks, detail) + if head in _QUANTIFIER_TOKENS: + raise _Reject("quantifier_out_of_band", detail) + return _parse_singular(toks, detail) + + +def read_member_argument(text: str) -> MemberArgument | MemberRefusal: + """Read *text* as a member argument, or refuse (typed). + + Deterministic and pure: same text → same ``MemberArgument``. The + conclusion is the final sentence, the sole "therefore"-led one, and must + be singular; every earlier sentence is a premise. Lowering is two-pass — + sentences parse first, then universals instantiate at every named + individual (so a universal may precede the individuals it binds) — with + premise formulas emitted in sentence order and atom ids minted in + emission order. + """ + if not text or not text.strip(): + return MemberRefusal("empty") + sentences = [ + (m.group(1), m.group(2)) for m in _SENTENCE_RE.finditer(text) if m.group(1).strip() + ] + if not sentences: + return MemberRefusal("empty") + + premises: list[_Singular | _Universal] = [] + premise_texts: list[str] = [] + conclusion: _Singular | None = None + query_text: str | None = None + + try: + for idx, (body, terminator) in enumerate(sentences): + if terminator == "?": + raise _Reject("question_sentence", body) + toks = _tokenize(body) + if not toks: + continue + if toks[0] == "therefore": + if conclusion is not None: + raise _Reject("multiple_conclusions", body) + if idx != len(sentences) - 1: + raise _Reject("conclusion_not_last", body) + rest = toks[1:] + if not rest: + raise _Reject("empty_side", body) + parsed = _parse_sentence(rest, body) + if not isinstance(parsed, _Singular): + raise _Reject("universal_conclusion_out_of_band", body) + conclusion = parsed + query_text = " ".join(rest) + continue + if len(premises) >= MAX_PREMISE_SENTENCES: + raise _Reject("too_many_premises", body) + premises.append(_parse_sentence(toks, body)) + premise_texts.append(" ".join(toks)) + + if conclusion is None or query_text is None: + return MemberRefusal("no_conclusion") + if not premises: + return MemberRefusal("no_premises") + + # --- lowering (ADR-0258 §2) ------------------------------------------ + records: list[_Singular | _Universal] = [*premises, conclusion] + + # Named individuals, first-appearance order. + individuals: list[tuple[str, ...]] = [] + for rec in records: + if isinstance(rec, _Singular) and rec.ind not in individuals: + individuals.append(rec.ind) + + # Class groups: each attested form joins the FIRST group whose + # representative (its first-attested form) it links to — greedy, + # deterministic, closed. + group_of: dict[tuple[str, ...], int] = {} + reps: list[tuple[str, ...]] = [] + for rec in records: + forms = ( + [rec.cls] if isinstance(rec, _Singular) else [rec.subject, rec.predicate] + ) + for form in forms: + if form in group_of: + continue + for gi, rep in enumerate(reps): + if _forms_link(form, rep): + group_of[form] = gi + break + else: + group_of[form] = len(reps) + reps.append(form) + + mint: dict[tuple[int, int], str] = {} + atom_display: list[str] = [] + + def atom_for(ind_idx: int, group: int, detail: str) -> str: + key = (ind_idx, group) + if key not in mint: + if len(atom_display) >= MAX_ATOMS: + raise _Reject("too_many_atoms", detail) + mint[key] = f"a{len(atom_display)}" + atom_display.append( + f"{' '.join(individuals[ind_idx])} : {' '.join(reps[group])}" + ) + return mint[key] + + premise_formulas: list[str] = [] + for rec, body_text in zip(premises, premise_texts): + if isinstance(rec, _Singular): + atom = atom_for(individuals.index(rec.ind), group_of[rec.cls], body_text) + premise_formulas.append(f"~({atom})" if rec.negated else atom) + continue + for ind_idx in range(len(individuals)): + antecedent = atom_for(ind_idx, group_of[rec.subject], body_text) + consequent = atom_for(ind_idx, group_of[rec.predicate], body_text) + premise_formulas.append( + f"({antecedent}) -> (~({consequent}))" + if rec.negative + else f"({antecedent}) -> ({consequent})" + ) + query_atom = atom_for( + individuals.index(conclusion.ind), group_of[conclusion.cls], query_text + ) + query_formula = f"~({query_atom})" if conclusion.negated else query_atom + except _Reject as rej: + return rej.refusal + + n_universal = sum(1 for r in premises if isinstance(r, _Universal)) + n_negative = sum( + 1 for r in premises if isinstance(r, _Universal) and r.negative + ) + if n_negative: + band = EN_MEMBER_NEGATIVE + elif n_universal >= 2: + band = EN_MEMBER_CHAIN + elif n_universal == 1: + band = EN_MEMBER_SINGLE + else: + band = EN_MEMBER_ATOMIC + + return MemberArgument( + premise_formulas=tuple(premise_formulas), + query_formula=query_formula, + premise_texts=tuple(premise_texts), + query_text=query_text, + band=band, + atoms=tuple(atom_display), + ) + + +__all__ = [ + "MAX_ATOMS", + "MAX_PREMISE_SENTENCES", + "MemberArgument", + "MemberRefusal", + "read_member_argument", +] diff --git a/generate/proof_chain/render.py b/generate/proof_chain/render.py index 30a1ef66..5520559a 100644 --- a/generate/proof_chain/render.py +++ b/generate/proof_chain/render.py @@ -96,6 +96,42 @@ def render_entailment_english( return f"Given: {given}. I can't evaluate {query_text} from that as stated." +def render_entailment_member( + trace: EntailmentTrace, premise_texts: tuple[str, ...], query_text: str +) -> str: + """The user-facing surface for a member-argument (Band v3-MEM) verdict. + + Same discipline as :func:`render_entailment_english`; the UNKNOWN template + scopes itself to THIS band's reading (ADR-0258 §3): distinct names are + read as distinct individuals and class words at face value — co-reference + or an unlinked class identity could settle what the lowering leaves open, + so the claim is stated of the reading, disclosed as such. ENTAILED / + REFUTED / inconsistent survive any such refinement (instantiation is + sound and entailment is monotone) and are stated at full strength. + """ + given = "; ".join(premise_texts) + if trace.outcome is Entailment.ENTAILED: + return f"Given: {given}. Your premises entail: {query_text}." + if trace.outcome is Entailment.REFUTED: + return ( + f"Given: {given}. Your premises entail the opposite of " + f"{query_text} — it cannot hold." + ) + if trace.outcome is Entailment.UNKNOWN: + return ( + f"Given: {given}. Reading each name as one individual and each " + f"class word at face value, your premises don't settle whether " + f"{query_text} — it holds in some cases and fails in others." + ) + # REFUSED + if trace.reason == INCONSISTENT_PREMISES: + return ( + f"Given: {given}. Those premises are inconsistent — they " + f"can't all be true, so I won't assert anything from them." + ) + return f"Given: {given}. I can't evaluate {query_text} from that as stated." + + def _categorical_clause(prop: dict) -> str: """One categorical proposition dict → its English clause.""" template = _CATEGORICAL_PHRASE.get(prop.get("form", ""), "{s} ~ {p}") @@ -129,4 +165,9 @@ def render_syllogism(trace: EntailmentTrace, structure: dict, query: dict) -> st ) -__all__ = ["render_entailment", "render_syllogism"] +__all__ = [ + "render_entailment", + "render_entailment_english", + "render_entailment_member", + "render_syllogism", +] diff --git a/generate/proof_chain/shape.py b/generate/proof_chain/shape.py index b21efa11..993b8ea2 100644 --- a/generate/proof_chain/shape.py +++ b/generate/proof_chain/shape.py @@ -60,8 +60,25 @@ EN_SHAPE_BANDS: tuple[str, ...] = ( EN_ATOMIC, ) +#: Band v3-MEM (ADR-0258) — singular-membership arguments with universal +#: premises ("Socrates is a man. All men are mortal. …"), read by +#: ``generate.proof_chain.member`` via per-individual propositional lowering. +#: Same ``en_`` license discipline: a different reader must earn its own +#: per-shape record. Priority order: negative > chain > single > atomic. +EN_MEMBER_NEGATIVE = "en_member_negative" +EN_MEMBER_CHAIN = "en_member_chain" +EN_MEMBER_SINGLE = "en_member_single" +EN_MEMBER_ATOMIC = "en_member_atomic" + +EN_MEMBER_BANDS: tuple[str, ...] = ( + EN_MEMBER_NEGATIVE, + EN_MEMBER_CHAIN, + EN_MEMBER_SINGLE, + EN_MEMBER_ATOMIC, +) + #: Every serving shape-band — the ratified ledger's full key set. -ALL_SHAPE_BANDS: tuple[str, ...] = SHAPE_BANDS + EN_SHAPE_BANDS +ALL_SHAPE_BANDS: tuple[str, ...] = SHAPE_BANDS + EN_SHAPE_BANDS + EN_MEMBER_BANDS def classify_deduction_shape(premises: tuple[str, ...], query: str) -> str: @@ -99,6 +116,11 @@ __all__ = [ "EN_CONDITIONAL_CHAIN", "EN_CONDITIONAL_SINGLE", "EN_DISJUNCTIVE", + "EN_MEMBER_ATOMIC", + "EN_MEMBER_BANDS", + "EN_MEMBER_CHAIN", + "EN_MEMBER_NEGATIVE", + "EN_MEMBER_SINGLE", "EN_SHAPE_BANDS", "SHAPE_BANDS", "classify_deduction_shape", diff --git a/scripts/verify_lane_shas.py b/scripts/verify_lane_shas.py index 4f72c505..0e38dccf 100644 --- a/scripts/verify_lane_shas.py +++ b/scripts/verify_lane_shas.py @@ -51,7 +51,7 @@ PINNED_SHAS: dict[str, str] = { "public_demo": "7d8ba0dbae9287cfe0bf15d231fa78a75abc627121c14900439293e01e1cc1d3", "math_teaching_corpus_v1": "eaf160d145da29f9050ede8d58bf111b0f651dd40aeae9201857d0b97e014dd4", "deductive_logic_v1": "97a230949016e38d5e3f37a69e4245b320575ee70e5af92ff7607f7b05f74b5f", - "deduction_serve_v1": "4199bd7241aafec143b180a5dab5ae60f3c4d519ed246b4433182908c55d8317", + "deduction_serve_v1": "ec446d70a6ba2eaaf04671800924754a3cfaacfc46f3225ca73e961169cd625d", } diff --git a/tests/test_deduction_serve_e2e.py b/tests/test_deduction_serve_e2e.py index cd311020..ed1c009a 100644 --- a/tests/test_deduction_serve_e2e.py +++ b/tests/test_deduction_serve_e2e.py @@ -118,11 +118,30 @@ def test_quoted_clause_surface_is_exempt_from_realizer_guard() -> None: assert "Your premises entail: the window is open" in resp_warm.surface -def test_out_of_regime_argument_refuses_honestly() -> None: - """A 'therefore' argument NO band can read (membership shape — reserved for - a future member_chain band) gets an honest committed refusal surface, never - a fluent-but-ungrounded answer or a silent fall-through (INV-34 fail-closed).""" +def test_member_argument_is_decided_end_to_end() -> None: + """The ADR-0258 flagship: the classic instantiation syllogism ("Socrates + is a man…"), decided through the real REPL spine via per-individual + lowering, rendered over the user's own sentences — including the A-chain + into an E-form.""" rt = _runtime(True) - resp = rt.chat("Socrates is a man. Therefore Socrates is mortal.") + resp = rt.chat("Socrates is a man. All men are mortal. Therefore Socrates is mortal.") + assert resp.grounding_source == "deduction" + assert "Your premises entail: socrates is mortal" in resp.surface + + negative = rt.chat( + "Tweety is a canary. All canaries are birds. No birds are reptiles. " + "Therefore Tweety is not a reptile." + ) + assert negative.grounding_source == "deduction" + assert "Your premises entail: tweety is not a reptile" in negative.surface + + +def test_out_of_regime_argument_refuses_honestly() -> None: + """A 'therefore' argument NO band can read (verb-phrase negation — + ADR-0257 scope-out #2, morphology work reserved for a future band) gets an + honest committed refusal surface, never a fluent-but-ungrounded answer or + a silent fall-through (INV-34 fail-closed).""" + rt = _runtime(True) + resp = rt.chat("The engine doesn't start. Therefore the engine is broken.") assert resp.grounding_source == "deduction" assert "can't parse" in resp.surface # honest reader-refusal disclosure diff --git a/tests/test_deduction_serve_lane.py b/tests/test_deduction_serve_lane.py index c6cfd814..2a1c2c2c 100644 --- a/tests/test_deduction_serve_lane.py +++ b/tests/test_deduction_serve_lane.py @@ -13,6 +13,7 @@ from evals.deduction_serve.runner import _ROOT, _load, build_report _V1 = _ROOT / "v1" / "cases.jsonl" _V2_EN = _ROOT / "v2_en" / "cases.jsonl" +_V2_MEMBER = _ROOT / "v2_member" / "cases.jsonl" def test_v1_lane_wrong_is_zero() -> None: @@ -38,16 +39,33 @@ def test_v2_en_lane_wrong_is_zero() -> None: """Band v2-EN (ADR-0257): hand-authored REAL-English arguments — content deliberately disjoint from the synthetic practice lexicon — decided by the production pipeline with wrong=0, across all four inference verdicts and - six distinct honest-decline shapes.""" + five distinct honest-decline shapes (ds-en-0022, the membership decline, + was promoted declined→entailed when the member band landed — ADR-0258).""" report = build_report(_load(_V2_EN)) assert report["n"] == 26 assert report["counts"]["wrong"] == 0 assert report["all_cases_correct"] is True cbg = report["correct_by_gold"] - assert cbg.get("entailed", 0) >= 13 + assert cbg.get("entailed", 0) >= 14 assert cbg.get("refuted", 0) >= 3 assert cbg.get("unknown", 0) >= 4 - assert cbg.get("declined", 0) >= 6 + assert cbg.get("declined", 0) >= 5 + + +def test_v2_member_lane_wrong_is_zero() -> None: + """Band v3-MEM (ADR-0258): hand-authored membership/universal arguments — + real nouns exercising every number-link row-type (irregular, invariant, + each regular suffix rule) — decided with wrong=0 across all four verdicts + and seven distinct honest-decline shapes.""" + report = build_report(_load(_V2_MEMBER)) + assert report["n"] == 26 + assert report["counts"]["wrong"] == 0 + assert report["all_cases_correct"] is True + cbg = report["correct_by_gold"] + assert cbg.get("entailed", 0) >= 12 + assert cbg.get("refuted", 0) >= 3 + assert cbg.get("unknown", 0) >= 4 + assert cbg.get("declined", 0) >= 7 def test_runner_treats_wrong_verdict_as_the_only_real_failure() -> None: diff --git a/tests/test_deduction_surface.py b/tests/test_deduction_surface.py index 3d7648e3..f33a319e 100644 --- a/tests/test_deduction_surface.py +++ b/tests/test_deduction_surface.py @@ -173,6 +173,64 @@ def test_english_reader_refusal_keeps_prior_honest_surface() -> None: assert "can't parse" in surface +def test_membership_syllogism_is_decided_band_v3_mem() -> None: + """The classic instantiation syllogism — reserved by ADR-0257 §6.1, now + DECIDED by the member band (ADR-0258), authoritatively (the + ``en_member_single`` band holds an earned SERVE license), with the verdict + rendered over the user's own sentences.""" + surface = deduction_grounded_surface( + "Socrates is a man. All men are mortal. Therefore Socrates is mortal." + ) + assert surface is not None + assert "Your premises entail: socrates is mortal" in surface + assert not surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + + +def test_member_negative_universal_is_decided() -> None: + """The E-form ("no …") lowers to a negated instantiation and decides.""" + surface = deduction_grounded_surface( + "Fido is a dog. No dogs are cats. Therefore Fido is not a cat." + ) + assert surface is not None + assert "Your premises entail: fido is not a cat" in surface + + +def test_member_unknown_is_scoped_to_the_instantiated_reading() -> None: + """Member-band UNKNOWN must scope itself (ADR-0258 §3): co-reference of + distinct names or an unlinked class identity could settle what the + lowering leaves open, so the claim is stated of the reading.""" + surface = deduction_grounded_surface( + "Socrates is mortal. All men are mortal. Therefore Socrates is a man." + ) + assert surface is not None + assert "Reading each name as one individual" in surface + assert "don't settle" in surface + + +def test_member_unearned_band_would_be_hedged() -> None: + """The en_member_* bands ride the SAME earned-license gate: strip the + license and the same sound answer is served DISCLOSED, never + authoritatively.""" + surface = deduction_grounded_surface( + "Socrates is a man. All men are mortal. Therefore Socrates is mortal.", + license_lookup=lambda band: None, + ) + assert surface is not None + assert surface.startswith(_UNVERIFIED_SHAPE_DISCLOSURE) + assert "Your premises entail: socrates is mortal" in surface + + +def test_member_reader_refusal_keeps_prior_honest_surface() -> None: + """When the member band ALSO cannot read the argument (here: tense, a + deliberate ADR-0258 scope-out), the pre-existing honest surfaces are + preserved verbatim — the band only widens.""" + surface = deduction_grounded_surface( + "Socrates was a man. All men are mortal. Therefore Socrates is mortal." + ) + assert surface is not None + assert "can't parse" in surface + + def test_surface_is_deterministic() -> None: text = "If p then q. p. Therefore q." assert deduction_grounded_surface(text) == deduction_grounded_surface(text) diff --git a/tests/test_member_argument_reader.py b/tests/test_member_argument_reader.py new file mode 100644 index 00000000..3cc85f72 --- /dev/null +++ b/tests/test_member_argument_reader.py @@ -0,0 +1,236 @@ +"""Band v3-MEM (ADR-0258) — member-argument reader contract. + +The reader is pure and deterministic: closed sentence grammar (singular +membership/predicate facts + A/E universals), per-individual propositional +lowering over minted opaque atoms, closed-table number linking, refusal-first +with a typed reason vocabulary, honesty caps. Soundness rides on the ROBDD +engine; these tests pin that the reader hands it the RIGHT problem. +""" + +from __future__ import annotations + +import pytest + +from generate.proof_chain.member import ( + MAX_ATOMS, + MAX_PREMISE_SENTENCES, + MemberArgument, + MemberRefusal, + read_member_argument, +) +from generate.proof_chain.shape import ( + EN_MEMBER_ATOMIC, + EN_MEMBER_CHAIN, + EN_MEMBER_NEGATIVE, + EN_MEMBER_SINGLE, +) + + +def _read(text: str) -> MemberArgument: + arg = read_member_argument(text) + assert isinstance(arg, MemberArgument), arg + return arg + + +def _refusal(text: str) -> MemberRefusal: + ref = read_member_argument(text) + assert isinstance(ref, MemberRefusal), ref + return ref + + +# --- the flagship reading ----------------------------------------------------- + + +def test_flagship_socrates_reads_as_instantiated_modus_ponens() -> None: + arg = _read("Socrates is a man. All men are mortal. Therefore Socrates is mortal.") + # "men" links to "man" (irregular table) — the universal instantiates at + # Socrates over the SAME atom the first premise minted. + assert arg.premise_formulas == ("a0", "(a0) -> (a1)") + assert arg.query_formula == "a1" + assert arg.premise_texts == ("socrates is a man", "all men are mortal") + assert arg.query_text == "socrates is mortal" + assert arg.band == EN_MEMBER_SINGLE + assert len(arg.atoms) == 2 + + +def test_universal_before_singular_reads_identically() -> None: + arg = _read("Every man is mortal. Socrates is a man. Therefore Socrates is mortal.") + # Two-pass lowering: the universal instantiates at individuals introduced + # LATER — premise formula order stays sentence order. + assert arg.premise_formulas == ("(a0) -> (a1)", "a0") + assert arg.query_formula == "a1" + + +def test_universal_instantiates_at_every_named_individual() -> None: + arg = _read( + "Plato is a man. Aristotle is a man. All men are mortal. " + "Therefore Aristotle is mortal." + ) + assert arg.premise_formulas == ( + "a0", "a1", "(a0) -> (a2)", "(a1) -> (a3)", + ) + assert arg.query_formula == "a3" + assert len(arg.atoms) == 4 + + +def test_negative_universal_lowers_to_negated_consequent() -> None: + arg = _read("Fido is a dog. No dogs are cats. Therefore Fido is not a cat.") + assert arg.premise_formulas == ("a0", "(a0) -> (~(a1))") + assert arg.query_formula == "~(a1)" + assert arg.band == EN_MEMBER_NEGATIVE + + +def test_membership_chain_through_plural_links() -> None: + arg = _read( + "Rex is a dog. All dogs are mammals. All mammals are animals. " + "Therefore Rex is an animal." + ) + assert arg.premise_formulas == ("a0", "(a0) -> (a1)", "(a1) -> (a2)") + assert arg.query_formula == "a2" + assert arg.band == EN_MEMBER_CHAIN + + +def test_atomic_band_negation_forms() -> None: + contraction = _read("Rex isn't a cat. Therefore Rex is not a cat.") + assert contraction.premise_formulas == ("~(a0)",) + assert contraction.query_formula == "~(a0)" + assert contraction.band == EN_MEMBER_ATOMIC + + sentential = _read("It is not the case that Rex is a cat. Therefore Rex is not a cat.") + assert sentential.premise_formulas == ("~(a0)",) + assert sentential.query_formula == "~(a0)" + + +def test_case_and_comma_normalization() -> None: + arg = _read("SOCRATES IS A MAN. All men are mortal. Therefore, Socrates is mortal.") + assert arg.premise_formulas == ("a0", "(a0) -> (a1)") + assert arg.query_text == "socrates is mortal" + + +# --- number linking (the closed morphology table) ----------------------------- + + +@pytest.mark.parametrize( + ("singular", "plural"), + [ + ("man", "men"), # irregular table + ("person", "people"), # irregular table + ("child", "children"), # irregular table + ("wolf", "wolves"), # irregular table + ("sheep", "sheep"), # invariant + ("dog", "dogs"), # regular +s + ("fox", "foxes"), # regular +es + ("pony", "ponies"), # regular y↔ies + ], +) +def test_number_linking_identifies_the_class(singular: str, plural: str) -> None: + arg = _read( + f"Kai is a {singular}. All {plural} are calm. Therefore Kai is calm." + ) + assert arg.premise_formulas == ("a0", "(a0) -> (a1)") + assert arg.query_formula == "a1" + + +def test_multi_token_class_links_on_head_noun() -> None: + arg = _read( + "Rex is a guard dog. All guard dogs are loyal. Therefore Rex is loyal." + ) + assert arg.premise_formulas == ("a0", "(a0) -> (a1)") + + +@pytest.mark.parametrize( + ("form_a", "form_b"), + [ + ("specie", "species"), # invariant-table priority blocks the +s rule + ("new", "news"), # "news" is not the plural of "new" + ], +) +def test_hazard_pairs_stay_distinct_classes(form_a: str, form_b: str) -> None: + arg = _read( + f"Kai is a {form_a}. All {form_b} are calm. Therefore Kai is calm." + ) + # No link ⇒ the universal instantiates over a DIFFERENT class atom ⇒ the + # conclusion is honestly unforced (a1 vs the a0 fact) — never a false link. + assert arg.premise_formulas == ("a0", "(a1) -> (a2)") + assert arg.query_formula == "a2" + + +# --- band classification ------------------------------------------------------ + + +@pytest.mark.parametrize( + ("text", "band"), + [ + ("Bo is a cat. Therefore Bo is a cat.", EN_MEMBER_ATOMIC), + ("Bo is a cat. All cats are quick. Therefore Bo is quick.", EN_MEMBER_SINGLE), + ( + "Bo is a cat. All cats are hunters. All hunters are quick. " + "Therefore Bo is quick.", + EN_MEMBER_CHAIN, + ), + ( + "Bo is a cat. All cats are hunters. No hunters are tame. " + "Therefore Bo is not tame.", + EN_MEMBER_NEGATIVE, + ), + ], +) +def test_band_classification(text: str, band: str) -> None: + assert _read(text).band == band + + +# --- typed refusals ----------------------------------------------------------- + + +@pytest.mark.parametrize( + ("text", "reason"), + [ + ("Some men are wise. Socrates is a man. Therefore Socrates is wise.", "quantifier_out_of_band"), + ("Everyone is mortal. Therefore Socrates is mortal.", "quantifier_out_of_band"), + ("Nobody is a saint. Therefore Socrates is not a saint.", "quantifier_out_of_band"), + ("Dogs are loyal. Rex is a dog. Therefore Rex is loyal.", "bare_plural_out_of_band"), + ("Socrates is the philosopher. All philosophers are wise. Therefore Socrates is wise.", "definite_description_out_of_band"), + ("Rex is a dog that barks. All dogs are loyal. Therefore Rex is loyal.", "relative_clause_out_of_band"), + ("Socrates is a man. Therefore all men are mortal.", "universal_conclusion_out_of_band"), + ("If Socrates is a man then Socrates is mortal. Therefore Socrates is mortal.", "mixed_structure_out_of_band"), + ("Socrates is a man or a god. Therefore Socrates is a man.", "mixed_structure_out_of_band"), + ("Rex never barks. Therefore Rex is loyal.", "sentence_shape_out_of_band"), + ("Socrates was a man. All men are mortal. Therefore Socrates is mortal.", "sentence_shape_out_of_band"), + ("Is Socrates a man? Therefore Socrates is a man.", "question_sentence"), + ("Socrates is a man. Socrates is mortal.", "no_conclusion"), + ("Therefore Socrates is a man.", "no_premises"), + ("Socrates is a man. Therefore Socrates is a man. Rex is a dog.", "conclusion_not_last"), + ("", "empty"), + ], +) +def test_typed_refusals(text: str, reason: str) -> None: + assert _refusal(text).reason == reason + + +# --- honesty caps ------------------------------------------------------------- + + +def test_premise_cap_refuses_not_truncates() -> None: + facts = " ".join(f"N{i} is a cat." for i in range(MAX_PREMISE_SENTENCES + 1)) + ref = _refusal(f"{facts} Therefore N0 is a cat.") + assert ref.reason == "too_many_premises" + + +def test_atom_cap_refuses_not_truncates() -> None: + # 13 individuals × 2 classes = 26 minted pairs > MAX_ATOMS=24, within the + # premise cap (13 facts + 1 universal = 14 sentences). + n = MAX_ATOMS // 2 + 1 + facts = " ".join(f"N{i} is a dog." for i in range(n)) + ref = _refusal(f"{facts} All dogs are cats. Therefore N0 is a cat.") + assert ref.reason == "too_many_atoms" + + +# --- determinism -------------------------------------------------------------- + + +def test_reading_is_deterministic() -> None: + text = ( + "Tara is a person. All people are mortal. No immortals are people. " + "Therefore Tara is mortal." + ) + assert read_member_argument(text) == read_member_argument(text)