From 0951d80e04147627cf39433c5b01ec928fe9a6c9 Mon Sep 17 00:00:00 2001 From: Shay Date: Sat, 6 Jun 2026 20:18:39 -0700 Subject: [PATCH] =?UTF-8?q?feat(comprehension):=20the=20divisive=20compara?= =?UTF-8?q?tive=20frame=20=E2=80=94=20"half=20as=20many"=20as=20exact=20in?= =?UTF-8?q?teger=20division=20(PR-6c)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PR-6c adds the divisive comparative frame: "half as many" read as EXACT INTEGER DIVISION. It is the divisor twin of PR-5c's multiplicative frame, and moves the independent R1 gold's r1-02-half from refused → correct. No serving path touched. No rational/fractional answer support added. Non-exact division refuses. Design (ADR-0134 amended — divide made symmetric with multiply): - `_check_divide` now admits a SINGLE-DEP divide-by-dimensionless-literal (item / dimensionless = item), the exact twin of single-dep multiply. The 2-dep rate-divide path is untouched. This keeps the IR's "literal operands are not deps" invariant (proven in PR-6a) uniform across Mul AND Div, so the reader builds both without a per-op special case and WITHOUT synthesizing a divisor symbol that would pollute the setup-oracle's unit signature. - `Div(Symbol, Literal)` IR node: "ref / divisor", operation_kind "divide", projects to `divide_by`. Divisor-only contract mirrors the scalar-only one. - Reader: `_DIVISOR_WORDS={half:2}` slots into the same 8-token " as many" template as the factor words; graph carries only the two entities. - Gold reconciliation: r1-02 placeholder `times_as_many factor 0.5` → exact `divide_by divisor 2` (gold 4). Makes the INDEPENDENT gold integer-faithful. The wrong=0 boundary — exact divisibility: the oracle admits `divide_by` only when `base % divisor == 0`. An odd base halved REFUSES (gold_error), never floors to a wrong integer. Divisor must be a nonzero int (0, 0.5, 1.5, bool all refuse); divisor=1 is intentionally the identity (pinned). admissibility proves DIMENSION; the oracle proves EXACT VALUE. Meaningful-fail (CLAUDE.md Schema-Defined Proof Obligations), both verified red: - drop the `% divisor` guard → test_oracle_refuses_non_exact_division fails (returns 3). - disable the single-dep divide branch → the admissibility test AND the reader's `half` test fail (admissibility refuses → reader refuses → half stays refused). Gates: R1 setup: 3 correct / 0 wrong / 7 refused R1 answers: 3 correct / 0 wrong / 7 refused / setup_wrong 0 / gold_error 0 15-case setup: 15 / 0 / 0 91 PR-6c tests + 60 relational lanes + 56 architectural invariants + 502 binding-graph/proof-chain/adapter tests green. All 8 SHA-content lanes match (serving unmoved; admissibility has no generate.derivation/reliability_gate consumer). --- .../ADR-0134-binding-graph-admissibility.md | 35 ++++++- evals/relational_metric/oracle.py | 24 ++++- evals/setup_oracle/r1_gold.jsonl | 2 +- evals/setup_oracle/signature.py | 2 + generate/binding_graph/admissibility.py | 24 ++++- generate/quantitative_comprehension.py | 54 +++++++++-- generate/quantitative_expr.py | 40 +++++++- tests/test_binding_graph_admissibility.py | 57 ++++++++++++ tests/test_quantitative_comprehension.py | 22 +++++ tests/test_quantitative_expr.py | 58 ++++++++++++ tests/test_setup_oracle.py | 92 +++++++++++++++++-- 11 files changed, 376 insertions(+), 34 deletions(-) diff --git a/docs/decisions/ADR-0134-binding-graph-admissibility.md b/docs/decisions/ADR-0134-binding-graph-admissibility.md index 4c941148..e3187b51 100644 --- a/docs/decisions/ADR-0134-binding-graph-admissibility.md +++ b/docs/decisions/ADR-0134-binding-graph-admissibility.md @@ -48,7 +48,7 @@ Add three deliverables under `generate/binding_graph/`: | `add` / `subtract` / `compare_additive` / `transfer` | all dep units equal; lhs == that unit | | `compare_multiplicative` | dep units cancel; lhs dimensionless | | `multiply` | lhs == product of dep units | - | `divide` | requires one dividend + one `*__divisor` literal; lhs == quotient | + | `divide` | **single dep**: divide by an implicit dimensionless literal, lhs == dividend unit (`x / dimensionless = x`); **two deps**: one dividend + one `*__divisor` literal, lhs == quotient | | `apply_rate` | dep with `semantic_role='rate'` carries `X/Y`; other dep carries `Y`; lhs == `X` | Refusal is typed: every `AdmissibilityError` carries a `reason` from @@ -170,3 +170,36 @@ None. The binding graph still has no runtime wiring outside `generate/binding_graph/`. `chat/runtime.py`, the cognition eval lane, the field invariant, the algebra backend, and every other production hot path are unaffected. Cognition eval lane byte-equal to main. + +## Amendment 2026-06-07 — single-dep `divide` (divide by a dimensionless literal) + +**What changed.** `_check_divide` now admits a **single-dep** form in addition +to the original two-dep `dividend + *__divisor` form: a quantity divided by an +implicit *dimensionless literal*, with `lhs == dividend unit`. + +**Why.** The off-serving comprehension reader's typed expression IR +(`generate/quantitative_expr.py`, PR-4/5c/6a) carries literal operands *inside* +the IR and deliberately does **not** make them dependencies — a `Mul(Symbol, +Literal)` ("twice as many") has `dependencies = {ref}`, and `_check_multiply` +already admits that single dep (`item × dimensionless = item`). "half as many" +(`Div(Symbol, Literal(2))`) is the exact divisive twin: same shape, same single +dep, the divisor is a dimensionless `Literal` in the IR. The original two-dep +convention (a synthesized `*__divisor` *symbol*) collides with that IR design and +would force a per-op special case in the reader plus an extra graph symbol. The +single-dep form makes `divide` **symmetric with `multiply`** so the IR's +"literal operands are not deps" invariant holds uniformly for both. + +**Safety.** +- The two-dep rate-adapter path (`*__divisor`) is unchanged. +- Soundness: dividing a unit-bearing quantity by a dimensionless constant + preserves the unit by construction — identical to the multiply twin. +- Exactness (the *value*, not the unit) is the answer oracle's responsibility: + `evals.relational_metric.oracle` admits `divide_by` only when + `base % divisor == 0`, refusing a non-exact division (an odd base over 2) + rather than flooring to a wrong integer. Admissibility proves *dimension*; the + oracle proves *exact integral value*. +- Off-serving: `admissibility.py` has no `generate.derivation` / + `core.reliability_gate` consumer; the frozen GSM8K serving metric cannot move. +- Pinned by `tests/test_binding_graph_admissibility.py` + (`test_divide_single_dep_dimensionless_keeps_unit`, + `test_divide_refuses_zero_or_three_deps`). diff --git a/evals/relational_metric/oracle.py b/evals/relational_metric/oracle.py index 7f6ccbb6..da7cede1 100644 --- a/evals/relational_metric/oracle.py +++ b/evals/relational_metric/oracle.py @@ -16,11 +16,16 @@ Supported relation kinds (the v1 + PR-6b forward-substitutable grammar): - ``more_than`` : ``entity = ref + delta`` - ``fewer_than`` : ``entity = ref - delta`` - ``times_as_many`` : ``entity = ref * factor`` (dimensionless integer scalar) +- ``divide_by`` : ``entity = ref // divisor`` (exact integer division only) - ``sum_of`` : ``entity = sum(parts)`` (part-whole / total) Every relation's references must already be resolved (forward-substitutable / -triangular). The oracle refuses anything else, never guesses. PR-6b keeps this -off-serving: it lets setup-correct R1 cases compute answers in the eval lane only. +triangular). The oracle refuses anything else, never guesses. PR-6b/6c keep this +off-serving: they let setup-correct R1 cases compute answers in the eval lane only. + +``divide_by`` is exact-only: a non-exact division (``base % divisor != 0``, e.g. an +odd base halved) REFUSES rather than flooring to a wrong integer — the wrong=0 boundary +for the "half as many" frame (PR-6c). """ from __future__ import annotations @@ -32,7 +37,9 @@ class OracleError(ValueError): """Malformed or out-of-grammar case — the oracle refuses, never guesses.""" -_SUPPORTED = frozenset({"fact", "more_than", "fewer_than", "sum_of", "times_as_many"}) +_SUPPORTED = frozenset( + {"fact", "more_than", "fewer_than", "sum_of", "times_as_many", "divide_by"} +) def oracle_answer(relations: list[dict[str, Any]], query: dict[str, Any]) -> int: @@ -75,6 +82,17 @@ def oracle_answer(relations: list[dict[str, Any]], query: dict[str, Any]) -> int if not isinstance(factor, int) or isinstance(factor, bool): raise OracleError(f"factor must be int: {rel!r}") values[entity] = values[ref] * factor + elif kind == "divide_by": + ref = rel.get("ref") + divisor = rel.get("divisor") + if ref not in values: + raise OracleError(f"forward reference to unresolved {ref!r}") + if not isinstance(divisor, int) or isinstance(divisor, bool) or divisor == 0: + raise OracleError(f"divisor must be a nonzero int: {rel!r}") + if values[ref] % divisor != 0: + # Exact-only: refuse rather than floor to a wrong integer (wrong=0). + raise OracleError(f"non-exact division {values[ref]}/{divisor}: {rel!r}") + values[entity] = values[ref] // divisor else: # sum_of parts = rel.get("parts") if not isinstance(parts, list) or not parts: diff --git a/evals/setup_oracle/r1_gold.jsonl b/evals/setup_oracle/r1_gold.jsonl index ad8e80c7..6cb9d356 100644 --- a/evals/setup_oracle/r1_gold.jsonl +++ b/evals/setup_oracle/r1_gold.jsonl @@ -1,5 +1,5 @@ {"id": "r1-01-twice", "text": "Anna has 6 apples. Bella has twice as many apples as Anna. How many apples does Bella have?", "relations": [{"kind": "fact", "entity": "anna", "value": 6}, {"kind": "times_as_many", "entity": "bella", "ref": "anna", "factor": 2}], "expected_units": {"anna": "item", "bella": "item"}, "query": {"entity": "bella", "unit": "item"}, "gold": 12, "notes": "Multiplicative: bella = 2 * anna. The reader has no multiplicative template AND 'twice' is non-digit -> must REFUSE, never misread as a fact/additive."} -{"id": "r1-02-half", "text": "Carl has 8 coins. Dora has half as many coins as Carl. How many coins does Dora have?", "relations": [{"kind": "fact", "entity": "carl", "value": 8}, {"kind": "times_as_many", "entity": "dora", "ref": "carl", "factor": 0.5}], "expected_units": {"carl": "item", "dora": "item"}, "query": {"entity": "dora", "unit": "item"}, "notes": "Multiplicative (factor 0.5). 'half' is non-digit -> must REFUSE."} +{"id": "r1-02-half", "text": "Carl has 8 coins. Dora has half as many coins as Carl. How many coins does Dora have?", "relations": [{"kind": "fact", "entity": "carl", "value": 8}, {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2}], "expected_units": {"carl": "item", "dora": "item"}, "query": {"entity": "dora", "unit": "item"}, "gold": 4, "notes": "Divisive: dora = carl / 2 = 4 (exact integer division). 'half as many' fits the [Y has WORD as many UNIT as X] template; the WORD maps to a divisor, not a factor (PR-6c). Exact-divisibility is the wrong=0 boundary: an odd base would refuse, never round."} {"id": "r1-03-more-total", "text": "Finn has 10 books. Evan has 5 more books than Finn. How many books do Evan and Finn have altogether?", "relations": [{"kind": "fact", "entity": "finn", "value": 10}, {"kind": "more_than", "entity": "evan", "ref": "finn", "delta": 5}, {"kind": "sum_of", "entity": "total", "parts": ["evan", "finn"]}], "expected_units": {"finn": "item", "evan": "item", "total": "item"}, "query": {"entity": "total", "unit": "item"}, "notes": "Additive + aggregate. 'altogether' (not the bare 'have') may fall outside the strict query template -> likely REFUSE; if read, structure must match exactly."} {"id": "r1-04-fewer-total", "text": "Gail has 20 cards. Hank has 6 fewer cards than Gail. How many cards do Gail and Hank have in total?", "relations": [{"kind": "fact", "entity": "gail", "value": 20}, {"kind": "fewer_than", "entity": "hank", "ref": "gail", "delta": 6}, {"kind": "sum_of", "entity": "total", "parts": ["gail", "hank"]}], "expected_units": {"gail": "item", "hank": "item", "total": "item"}, "query": {"entity": "total", "unit": "item"}, "notes": "Additive(fewer) + aggregate. 'in total' qualifier likely outside the query template -> REFUSE expected."} {"id": "r1-05-chain", "text": "Ivy has 4 pens. Jon has 3 times as many pens as Ivy. Kim has 2 more pens than Jon. How many pens does Kim have?", "relations": [{"kind": "fact", "entity": "ivy", "value": 4}, {"kind": "times_as_many", "entity": "jon", "ref": "ivy", "factor": 3}, {"kind": "more_than", "entity": "kim", "ref": "jon", "delta": 2}], "expected_units": {"ivy": "item", "jon": "item", "kim": "item"}, "query": {"entity": "kim", "unit": "item"}, "gold": 14, "notes": "Multi-step derived chain: jon=3*ivy (intermediate), kim=jon+2. The multiplicative middle step has no template -> must REFUSE the whole reading, never read a partial/wrong chain."} diff --git a/evals/setup_oracle/signature.py b/evals/setup_oracle/signature.py index 061fc2ca..2d633c25 100644 --- a/evals/setup_oracle/signature.py +++ b/evals/setup_oracle/signature.py @@ -45,6 +45,8 @@ def relation_signature(relations: list[dict[str, Any]]) -> tuple[tuple, ...]: out.append((kind, r["entity"], r["ref"], int(r["delta"]))) elif kind == "times_as_many": out.append(("times_as_many", r["entity"], r["ref"], r["factor"])) + elif kind == "divide_by": + out.append(("divide_by", r["entity"], r["ref"], int(r["divisor"]))) elif kind == "sum_of": out.append(("sum_of", r["entity"], tuple(sorted(r["parts"])))) else: # an unknown relation kind is itself a structural difference, not a crash diff --git a/generate/binding_graph/admissibility.py b/generate/binding_graph/admissibility.py index 896efd6a..ceabf6cc 100644 --- a/generate/binding_graph/admissibility.py +++ b/generate/binding_graph/admissibility.py @@ -218,14 +218,30 @@ def _check_multiply( def _check_divide( dep_units: list[tuple[SymbolBinding, UnitVector]], ) -> UnitProof: - """Dividend / divisor. Divisor identified by ``__divisor`` suffix. + """Dividend / divisor. Two admissible forms: - Refuses with ``operand_arity`` if dep set is not exactly one dividend - + one ``*__divisor`` literal. The adapter is responsible for naming. + - **single dep** — divide by an implicit *dimensionless literal* (the reader's + "half as many"). The divisor is carried in the reader's typed IR as a + dimensionless :class:`~generate.quantitative_expr.Literal`, NOT as a graph + symbol, exactly as the multiplicative factor is. This is symmetric with + :func:`_check_multiply`'s single-dep dimensionless scaling: the quotient keeps + the dividend's unit (``x / dimensionless = x``). + - **two deps** — dividend + a ``*__divisor`` literal (the rate-adapter convention). + lhs == quotient of the two units. The adapter is responsible for naming. + + Refuses with ``operand_arity`` for any other arity. """ + if len(dep_units) == 1: + # Divide by an implicit dimensionless literal — symmetric with single-dep + # multiply. No graph divisor symbol exists, so there is nothing to quotient + # against; the quotient keeps the dividend's unit by construction. + only = dep_units[0][1] + return UnitProof( + operation_kind="divide", lhs_unit=only, operand_units=(only,) + ) if len(dep_units) != 2: raise AdmissibilityError( - "operand_arity", f"divide requires exactly 2 deps; got {len(dep_units)}" + "operand_arity", f"divide requires 1 or 2 deps; got {len(dep_units)}" ) dividend: UnitVector | None = None divisor: UnitVector | None = None diff --git a/generate/quantitative_comprehension.py b/generate/quantitative_comprehension.py index ba56be3f..f96f29e1 100644 --- a/generate/quantitative_comprehension.py +++ b/generate/quantitative_comprehension.py @@ -43,6 +43,7 @@ from generate.binding_graph.units import UnitAlgebraError, parse_unit from generate.meaning_graph.reader import Refusal, _split_sentences from generate.quantitative_expr import ( Add, + Div, Expr, Literal, Mul, @@ -154,25 +155,48 @@ class _Mul: unit: str -#: Word factors for "twice/double/triple ... as many". 'half' (a /2, the divide path) -#: is deliberately ABSENT — divide-by-literal is a separate admissibility path, deferred. +@dataclass(frozen=True, slots=True) +class _Div: + """Divisive comparative: entity = ref / divisor (R1, "half as many"). The + divisor is a dimensionless integer literal; the quotient keeps ref's unit.""" + + entity: str + ref: str + divisor: int + unit: str + + +#: Word factors for "twice/double/triple ... as many" (a multiply by a dimensionless int). _FACTOR_WORDS: dict[str, int] = {"twice": 2, "double": 2, "triple": 3, "quadruple": 4} +#: Word divisors for "half ... as many" (a divide by a dimensionless int). The divisive +#: twin of ``_FACTOR_WORDS``; both slot into the same 8-token " as many" template. +#: 'third'/'quarter' (non-power-of-two surface forms with an article) are deferred. +_DIVISOR_WORDS: dict[str, int] = {"half": 2} -def _try_multiplicative(entity: str, toks: list[str], detail: str) -> "_Mul | None": - """Match "Y has as many as X" or "Y has times as many - as X" → ``_Mul``. Returns None if the clause is not multiplicative (the - caller then tries the digit-led fact/additive templates).""" - # [Y, has, FACTORWORD, as, many, UNIT, as, X] + +def _try_multiplicative(entity: str, toks: list[str], detail: str) -> "_Mul | _Div | None": + """Match the comparative templates → ``_Mul`` (multiply) or ``_Div`` (divide). + + - "Y has as many as X" → ``_Mul`` (twice/double/triple/quadruple) + - "Y has as many as X" → ``_Div`` (half) + - "Y has times as many as X" → ``_Mul`` + + Returns None if the clause is not comparative (the caller then tries the digit-led + fact/additive templates).""" + # [Y, has, WORD, as, many, UNIT, as, X] — factor and divisor words share this shape. if ( len(toks) == 8 - and toks[2] in _FACTOR_WORDS and toks[3] == "as" and toks[4] == "many" and toks[6] == "as" ): - return _Mul(entity, _ident(toks[7], detail), _FACTOR_WORDS[toks[2]], - _resolve_unit(_ident(toks[5], detail))) + ref = _ident(toks[7], detail) + unit = _resolve_unit(_ident(toks[5], detail)) + if toks[2] in _FACTOR_WORDS: + return _Mul(entity, ref, _FACTOR_WORDS[toks[2]], unit) + if toks[2] in _DIVISOR_WORDS: + return _Div(entity, ref, _DIVISOR_WORDS[toks[2]], unit) # [Y, has, N, times, as, many, UNIT, as, X] if ( len(toks) == 9 @@ -240,6 +264,7 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh facts: list[_Fact] = [] eqs: list[_Eq] = [] muls: list[_Mul] = [] + divs: list[_Div] = [] queries: list[tuple] = [] try: @@ -253,6 +278,8 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh eqs.append(spec) elif isinstance(spec, _Mul): muls.append(spec) + elif isinstance(spec, _Div): + divs.append(spec) else: queries.append(spec) except _QReject as rej: @@ -269,6 +296,8 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh unit_of[e.entity], role_of[e.entity] = e.unit, "count" for m in muls: unit_of[m.entity], role_of[m.entity] = m.unit, "count" + for d in divs: + unit_of[d.entity], role_of[d.entity] = d.unit, "count" query = queries[0] sum_eq: tuple[str, tuple[str, ...]] | None = None @@ -288,6 +317,8 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh referenced.update((e.entity, e.ref)) for m in muls: referenced.update((m.entity, m.ref)) + for d in divs: + referenced.update((d.entity, d.ref)) if sum_eq is not None: referenced.add(sum_eq[0]) referenced.update(sum_eq[1]) @@ -321,6 +352,9 @@ def comprehend_quantitative(text: str, source_id: str = "input") -> QuantCompreh expr_specs.extend( (m.entity, Mul(Symbol(m.ref), Literal(m.factor))) for m in muls ) + expr_specs.extend( + (d.entity, Div(Symbol(d.ref), Literal(d.divisor))) for d in divs + ) if sum_eq is not None: lhs, parts = sum_eq expr_specs.append((lhs, SumOf(tuple(Symbol(p) for p in parts)))) diff --git a/generate/quantitative_expr.py b/generate/quantitative_expr.py index 6cfa3d0c..3e6af860 100644 --- a/generate/quantitative_expr.py +++ b/generate/quantitative_expr.py @@ -65,6 +65,27 @@ class Mul: right: "Expr" +@dataclass(frozen=True, slots=True) +class Div: + """Exact integer division of a symbol by a dimensionless literal divisor — the + fractional comparative ("half/a third as many"). ``left`` is the referenced symbol, + ``right`` a dimensionless literal divisor; the quotient keeps the symbol's unit + (``count / scalar = count``). + + "half as many" is modelled as ``Div(Symbol, Literal(2))``, NOT ``Mul`` by a rational: + the system is integer-exact end to end (``oracle_answer -> int``) and :class:`Literal` + is a dimensionless *integer* (the contract PR-6a proved load-bearing), so a fractional + factor is not representable. Division by an integer divisor keeps everything integral. + + Divisor-only contract (the wrong=0 boundary). The only admitted shape is + ``Div(Symbol, Literal)`` — see :func:`to_relation`, which refuses every other shape. + Exactness is enforced downstream: the answer oracle admits the quotient ONLY when + ``base % divisor == 0`` (an odd base over 2 refuses, never floors to a wrong integer).""" + + left: "Expr" + right: "Expr" + + @dataclass(frozen=True, slots=True) class SumOf: """An aggregate over ≥2 symbols (the part-whole total).""" @@ -72,7 +93,7 @@ class SumOf: parts: tuple[Symbol, ...] -Expr = Union[Literal, Symbol, Add, Sub, Mul, SumOf] +Expr = Union[Literal, Symbol, Add, Sub, Mul, Div, SumOf] def to_canonical_string(expr: Expr) -> str: @@ -88,6 +109,8 @@ def to_canonical_string(expr: Expr) -> str: return f"{to_canonical_string(left)} - {to_canonical_string(right)}" case Mul(left, right): return f"{to_canonical_string(left)} * {to_canonical_string(right)}" + case Div(left, right): + return f"{to_canonical_string(left)} / {to_canonical_string(right)}" case SumOf(parts): return " + ".join(to_canonical_string(p) for p in parts) raise TypeError(f"not an Expr: {expr!r}") # pragma: no cover - exhaustive above @@ -100,7 +123,7 @@ def dependencies(expr: Expr) -> frozenset[str]: return frozenset() case Symbol(symbol_id): return frozenset({symbol_id}) - case Add(left, right) | Sub(left, right) | Mul(left, right): + case Add(left, right) | Sub(left, right) | Mul(left, right) | Div(left, right): return dependencies(left) | dependencies(right) case SumOf(parts): out: frozenset[str] = frozenset() @@ -119,6 +142,8 @@ def operation_kind(expr: Expr) -> str: return "subtract" case Mul(_, _): return "multiply" + case Div(_, _): + return "divide" case _: raise TypeError(f"expression has no operation_kind: {expr!r}") @@ -129,9 +154,11 @@ def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None: ``None`` for a shape the projection does not handle — the caller refuses rather than emit a guessed relation (wrong=0 boundary). Each ``case`` is intentionally a *narrow* structural pattern, not a kind tag: ``Mul(Symbol, Literal)`` is the only multiplicative - shape projected (the scalar-only contract — a ``count × count`` ``Mul(Symbol, Symbol)`` - or a compound factor falls through to ``None``). The dimensional checker would not catch - such a masquerade (it products units happily), so this boundary is load-bearing. + shape projected and ``Div(Symbol, Literal)`` the only divisive one (the scalar/divisor + contracts — a ``count × count`` ``Mul(Symbol, Symbol)``, a compound factor, or a + symbol-over-symbol ``Div`` falls through to ``None``). The dimensional checker would not + catch such a masquerade (it products/quotients units happily), so this boundary is + load-bearing. """ match expr: case Add(Symbol(ref), Literal(delta)): @@ -140,6 +167,8 @@ def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None: return {"kind": "fewer_than", "entity": lhs, "ref": ref, "delta": delta} case Mul(Symbol(ref), Literal(factor)): return {"kind": "times_as_many", "entity": lhs, "ref": ref, "factor": factor} + case Div(Symbol(ref), Literal(divisor)): + return {"kind": "divide_by", "entity": lhs, "ref": ref, "divisor": divisor} case SumOf(parts): return {"kind": "sum_of", "entity": lhs, "parts": [p.symbol_id for p in parts]} case _: @@ -148,6 +177,7 @@ def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None: __all__ = [ "Add", + "Div", "Expr", "Literal", "Mul", diff --git a/tests/test_binding_graph_admissibility.py b/tests/test_binding_graph_admissibility.py index a4088954..4d6158e0 100644 --- a/tests/test_binding_graph_admissibility.py +++ b/tests/test_binding_graph_admissibility.py @@ -247,6 +247,63 @@ def test_divide_refuses_three_deps() -> None: assert ei.value.reason == "operand_arity" +# --------------------------------------------------------------------------- # +# ADR-0134 amendment 2026-06-07 — single-dep divide (divide by a dimensionless literal) +# --------------------------------------------------------------------------- # + + +def test_divide_single_dep_dimensionless_keeps_unit() -> None: + """A single-dep divide (the reader's "half as many") divides by an implicit + dimensionless literal and keeps the dividend's unit — symmetric with single-dep + multiply. + + Meaningful-fail: if the ``len == 1`` branch were removed (reverting to ``!= 2`` + refuse), this admission turns into an ``operand_arity`` refusal and the assert fails. + """ + symbols = {"carl": _sym("carl", unit="item")} + proof = check_admissibility( + _eq(kind="divide", deps=frozenset({"carl"})), symbols=symbols + ) + assert proof.operation_kind == "divide" + assert proof.lhs_unit == parse_unit("item") # item / dimensionless = item + assert proof.operand_units == (parse_unit("item"),) + + +def test_divide_refuses_zero_or_three_deps() -> None: + """The single-dep extension is narrow: zero deps and three deps still refuse with + ``operand_arity`` — only one (dimensionless divide) or two (rate divide) are admitted. + """ + with pytest.raises(AdmissibilityError) as ei0: + check_admissibility(_eq(kind="divide", deps=frozenset()), symbols={}) + assert ei0.value.reason == "operand_arity" + + symbols = { + "a": _sym("a", unit="foot"), + "b": _sym("b", unit="hour"), + "op_000__divisor": _sym("op_000__divisor", unit="hour"), + } + with pytest.raises(AdmissibilityError) as ei3: + check_admissibility( + _eq(kind="divide", deps=frozenset({"a", "b", "op_000__divisor"})), + symbols=symbols, + ) + assert ei3.value.reason == "operand_arity" + + +def test_divide_two_dep_rate_path_unchanged_by_amendment() -> None: + """The original two-dep rate divide (dividend + ``*__divisor``) is untouched — the + amendment only ADDED the single-dep form.""" + symbols = { + "q_actor_foot_t0": _sym("q_actor_foot_t0", unit="foot"), + "op_000__divisor": _sym("op_000__divisor", unit="hour"), + } + proof = check_admissibility( + _eq(kind="divide", deps=frozenset({"q_actor_foot_t0", "op_000__divisor"})), + symbols=symbols, + ) + assert proof.lhs_unit.exponents == (1, -1, 0, 0, 0, 0) # foot / hour = speed + + # --------------------------------------------------------------------------- # apply_rate # --------------------------------------------------------------------------- diff --git a/tests/test_quantitative_comprehension.py b/tests/test_quantitative_comprehension.py index ea41ada6..2d87275f 100644 --- a/tests/test_quantitative_comprehension.py +++ b/tests/test_quantitative_comprehension.py @@ -196,3 +196,25 @@ def test_multiplicative_missing_base_refuses() -> None: # never fabricate a base quantity. comp = comprehend_quantitative("Quinn has twice as many toys as Rosa. How many toys does Quinn have?") assert isinstance(comp, Refusal) + + +def test_half_as_many_builds_divide_equation() -> None: + # PR-6c: "half as many" is the divisive twin of "twice as many" — operation_kind + # "divide", a single symbol dep (the divisor literal is in the IR, not a graph symbol), + # and the REAL single-dep admissibility check (item / dimensionless = item) admits it. + comp = _comp("Carl has 8 coins. Dora has half as many coins as Carl. How many coins does Dora have?") + eq = next(e for e in comp.binding_graph.equations if e.lhs_symbol_id == "dora") + assert eq.operation_kind == "divide" + assert eq.rhs_canonical == "carl / 2" + assert eq.dependencies == frozenset({"carl"}) # uniform with Mul: literal not a dep + assert eq.admissibility_status == "admitted" + assert single_unknown(comp.binding_graph).symbol_id == "dora" + # The graph carries ONLY the two entities — no synthesized __divisor symbol pollutes + # it (that is why the symmetric single-dep divide was chosen over divisor synthesis). + assert {s.symbol_id for s in comp.binding_graph.symbols} == {"carl", "dora"} + + +def test_half_as_many_missing_base_refuses() -> None: + # "half as many ... as Rod" with no value for Rod -> ungrounded base -> REFUSE. + comp = comprehend_quantitative("Sue has half as many pears as Rod. How many pears does Sue have?") + assert isinstance(comp, Refusal) diff --git a/tests/test_quantitative_expr.py b/tests/test_quantitative_expr.py index 5fbdc156..40b29036 100644 --- a/tests/test_quantitative_expr.py +++ b/tests/test_quantitative_expr.py @@ -169,3 +169,61 @@ def test_scalar_only_guard_is_load_bearing() -> None: assert proof.operation_kind == "multiply" # But the projection REFUSES the same shape — the boundary that keeps wrong=0. assert to_relation("c", Mul(Symbol("a"), Symbol("b"))) is None + + +# --------------------------------------------------------------------------- # +# PR-6c — the divisive comparative (Div), the divisor twin of Mul +# --------------------------------------------------------------------------- # + + +def test_div_serialization_and_derivations() -> None: + from generate.quantitative_expr import Div + + d = Div(Symbol("carl"), Literal(2)) + assert to_canonical_string(d) == "carl / 2" + assert dependencies(d) == frozenset({"carl"}) # the literal divisor is NOT a dep + assert operation_kind(d) == "divide" + assert to_relation("dora", d) == { + "kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2, + } + + +def test_div_projection_admits_only_symbol_over_literal() -> None: + """``Div(Symbol, Literal)`` is the ONLY shape that projects to ``divide_by``; every + other ``Div`` shape REFUSES (``to_relation`` → None) — the divisor-only twin of the + scalar-only Mul contract. + + Meaningful-fail: a ``Div(Symbol, Symbol)`` is a quantity-over-quantity ratio (the + rate-divide family), NOT a divide-by-dimensionless-literal; projecting it as + ``divide_by`` would fabricate a divisor. These asserts fail the moment that guard is + loosened. + """ + from generate.quantitative_expr import Div + + # The one admitted shape. + assert to_relation("dora", Div(Symbol("carl"), Literal(2))) == { + "kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2, + } + # Quantity over quantity (a ratio), not a dimensionless divide → refuse. + assert to_relation("dora", Div(Symbol("a"), Symbol("b"))) is None + # Commuted (literal dividend) → refuse. + assert to_relation("dora", Div(Literal(8), Symbol("a"))) is None + # Compound divisor → refuse. + assert to_relation("dora", Div(Symbol("a"), Add(Symbol("b"), Literal(1)))) is None + # A bare literal quotient carries no symbol to reference → refuse. + assert to_relation("dora", Div(Literal(8), Literal(2))) is None + + +def test_div_is_symmetric_with_mul_in_the_ir() -> None: + """``Div`` and ``Mul`` are structural twins: single-symbol dep, dimensionless literal + operand, the operand is never a dependency. This symmetry is what lets the reader + build BOTH uniformly (``deps = dependencies(expr)``) without a per-op special case. + """ + from generate.quantitative_expr import Div, Mul + + mul = Mul(Symbol("anna"), Literal(2)) + div = Div(Symbol("carl"), Literal(2)) + assert dependencies(mul) == frozenset({"anna"}) + assert dependencies(div) == frozenset({"carl"}) # identical shape: literal not a dep + assert operation_kind(mul) == "multiply" + assert operation_kind(div) == "divide" diff --git a/tests/test_setup_oracle.py b/tests/test_setup_oracle.py index cf7d8a91..c92ccba8 100644 --- a/tests/test_setup_oracle.py +++ b/tests/test_setup_oracle.py @@ -152,19 +152,21 @@ def test_reader_units_read_from_the_binding_graph() -> None: # --------------------------------------------------------------------------- # -def test_r1_multiplicative_supported_rest_refused_wrong_zero() -> None: +def test_r1_comparative_supported_rest_refused_wrong_zero() -> None: r = run_r1() assert r["total"] == 10 - # THE invariant through the first capability slice: NO R1 case is misread. Adding the - # multiplicative frame turned refusals into correct readings without any setup_wrong. + # THE invariant through every capability slice: NO R1 case is misread. Each frame + # turns refusals into correct readings without ever producing a setup_wrong. assert r["setup_wrong"] == 0 - # The multiplicative frame (PR-5c) reads "twice as many" (r1-01) and the multi-step - # chain whose middle step is "N times as many" (r1-05); the rest stay safe refusals. by_id = {d["id"]: d["outcome"] for d in r["details"]} + # Multiplicative frame (PR-5c): "twice as many" (r1-01) + the multi-step chain whose + # middle step is "N times as many" (r1-05). assert by_id["r1-01-twice"] == "correct" assert by_id["r1-05-chain"] == "correct" - assert r["setup_correct"] == 2 - assert r["setup_refused"] == 8 + # Divisive frame (PR-6c): "half as many" (r1-02). + assert by_id["r1-02-half"] == "correct" + assert r["setup_correct"] == 3 + assert r["setup_refused"] == 7 # No detail is ever WRONG, and every non-correct one is a typed refusal. for d in r["details"]: assert d["outcome"] in ("correct", "refused") @@ -209,12 +211,82 @@ def test_r1_answer_lane_scores_only_setup_correct_fixtures() -> None: assert r["setup_wrong"] == 0 assert r["wrong"] == 0 assert r["gold_error"] == 0 - assert r["correct"] == 2 - assert r["refused"] == 8 + assert r["correct"] == 3 + assert r["refused"] == 7 by_id = {d["id"]: d for d in r["details"]} assert by_id["r1-01-twice"] == {"id": "r1-01-twice", "outcome": "correct", "answer": 12} + assert by_id["r1-02-half"] == {"id": "r1-02-half", "outcome": "correct", "answer": 4} assert by_id["r1-05-chain"] == {"id": "r1-05-chain", "outcome": "correct", "answer": 14} for fixture_id, detail in by_id.items(): - if fixture_id not in {"r1-01-twice", "r1-05-chain"}: + if fixture_id not in {"r1-01-twice", "r1-02-half", "r1-05-chain"}: assert detail["outcome"] == "refused" assert detail.get("reason") + + +# --------------------------------------------------------------------------- # +# PR-6c — off-serving answer oracle support for divide_by ("half as many") +# --------------------------------------------------------------------------- # + + +def test_oracle_computes_divide_by_exact() -> None: + assert oracle_answer( + [ + {"kind": "fact", "entity": "carl", "value": 8}, + {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2}, + ], + {"entity": "dora"}, + ) == 4 + + +def test_oracle_refuses_non_exact_division() -> None: + """The wrong=0 boundary of the divisive frame: a non-exact division REFUSES rather + than flooring to a wrong integer. ``7 // 2 == 3`` would be WRONG; the oracle raises. + + Meaningful-fail: if the ``base % divisor != 0`` guard were dropped, this would return + 3 (a fabricated answer) instead of raising — the assert flips from pass to fail. + """ + with pytest.raises(OracleError): + oracle_answer( + [ + {"kind": "fact", "entity": "xio", "value": 7}, + {"kind": "divide_by", "entity": "yon", "ref": "xio", "divisor": 2}, + ], + {"entity": "yon"}, + ) + + +def test_oracle_rejects_bad_divisor_and_forward_ref() -> None: + """The full ``divide_by`` refusal contract — every bad-divisor / unresolved-base class + raises ``OracleError`` (never a ZeroDivisionError, never a silent float/floor).""" + base = {"kind": "fact", "entity": "carl", "value": 8} + + def _bad_divisor(divisor: object) -> None: + with pytest.raises(OracleError): + oracle_answer( + [base, {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": divisor}], + {"entity": "dora"}, + ) + + _bad_divisor(0.5) # non-integer (fractional < 1) + _bad_divisor(1.5) # non-integer (fractional > 1) + _bad_divisor(0) # zero divisor — never ZeroDivisionError + _bad_divisor(True) # bool is not an admissible int divisor (isinstance(True, int) is True) + # Forward reference to an unresolved base → refuse. + with pytest.raises(OracleError): + oracle_answer( + [{"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 2}], + {"entity": "dora"}, + ) + + +def test_oracle_divide_by_one_is_identity() -> None: + """``divisor=1`` is intentionally ALLOWED: base / 1 = base, exact. The reader never + constructs it (``_DIVISOR_WORDS`` only maps 'half'→2), but the oracle's grammar admits + it mathematically. Pinned so the choice stays deliberate, not accidental.""" + assert oracle_answer( + [ + {"kind": "fact", "entity": "carl", "value": 8}, + {"kind": "divide_by", "entity": "dora", "ref": "carl", "divisor": 1}, + ], + {"entity": "dora"}, + ) == 8