core/generate/quantitative_expr.py
Shay 0951d80e04 feat(comprehension): the divisive comparative frame — "half as many" as exact integer division (PR-6c)
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 "<WORD> 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).
2026-06-06 20:18:39 -07:00

191 lines
7.4 KiB
Python
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

"""Typed expression IR for the arithmetic reader (PR-4).
The READER's source of meaning for an equation's right-hand side. The binding-graph
deliberately keeps ``BoundEquation.rhs_canonical`` a *string* (a decoupling layer that
does not import the symbolic substrate); this IR lives ABOVE that boundary in the reader,
serializes DOWN to the canonical string (``to_canonical_string``), and is read directly by
the projection (``to_relation``) so meaning is never recovered by re-parsing the string.
``to_canonical_string`` is byte-identical to the strings the reader emitted before PR-4
("ref + delta", "ref - delta", "a + b") — so the binding-graph and every downstream hash
are unchanged. Deterministic; no clock, no randomness.
"""
from __future__ import annotations
from dataclasses import dataclass
from typing import Any, Union
@dataclass(frozen=True, slots=True)
class Literal:
"""A grounded integer operand (a value sourced from the text)."""
value: int
@dataclass(frozen=True, slots=True)
class Symbol:
"""A reference to another bound symbol."""
symbol_id: str
@dataclass(frozen=True, slots=True)
class Add:
left: "Expr"
right: "Expr"
@dataclass(frozen=True, slots=True)
class Sub:
left: "Expr"
right: "Expr"
@dataclass(frozen=True, slots=True)
class Mul:
"""A scalar multiple of a symbol — the multiplicative comparative ("twice/N times
as many"). ``left`` is the referenced symbol, ``right`` a dimensionless literal
factor; the product keeps the symbol's unit (``count × scalar = count``).
Scalar-only contract (the wrong=0 boundary). The *only* admitted shape is
``Mul(Symbol, Literal)`` — a unit-bearing symbol times a dimensionless integer.
``right`` being a :class:`Literal` (an ``int`` with no unit field) is what makes the
factor dimensionless *by construction*: a unit-bearing literal multiplication is not
representable, not merely unchecked. ``Mul(Symbol, Symbol)`` (a ``count × count``
product) and any compound factor are deliberately NOT projected — see
:func:`to_relation`, which refuses them. This refusal lives at the projection
boundary, NOT in the dimensional admissibility checker: ``check_admissibility``'s
``multiply`` dispatch products operand units generally (``foot × pound → length·mass``,
no refusal), so it would happily admit a ``count × count`` product as ``count²``. The
scalar-only guarantee is therefore enforced HERE, by what we project, not there."""
left: "Expr"
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)."""
parts: tuple[Symbol, ...]
Expr = Union[Literal, Symbol, Add, Sub, Mul, Div, SumOf]
def to_canonical_string(expr: Expr) -> str:
"""Serialize to the canonical rhs string — byte-identical to the pre-IR format."""
match expr:
case Literal(value):
return str(value)
case Symbol(symbol_id):
return symbol_id
case Add(left, right):
return f"{to_canonical_string(left)} + {to_canonical_string(right)}"
case Sub(left, right):
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
def dependencies(expr: Expr) -> frozenset[str]:
"""The symbols the expression reads (the equation's dependency set)."""
match expr:
case Literal(_):
return frozenset()
case Symbol(symbol_id):
return frozenset({symbol_id})
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()
for p in parts:
out |= dependencies(p)
return out
raise TypeError(f"not an Expr: {expr!r}") # pragma: no cover
def operation_kind(expr: Expr) -> str:
"""The binding-graph ``operation_kind`` an expression lowers to."""
match expr:
case Add(_, _) | SumOf(_):
return "add"
case Sub(_, _):
return "subtract"
case Mul(_, _):
return "multiply"
case Div(_, _):
return "divide"
case _:
raise TypeError(f"expression has no operation_kind: {expr!r}")
def to_relation(lhs: str, expr: Expr) -> dict[str, Any] | None:
"""Project to a relational_metric relation, read from STRUCTURE (no string parse).
``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 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)):
return {"kind": "more_than", "entity": lhs, "ref": ref, "delta": delta}
case Sub(Symbol(ref), Literal(delta)):
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 _:
return None
__all__ = [
"Add",
"Div",
"Expr",
"Literal",
"Mul",
"Sub",
"SumOf",
"Symbol",
"dependencies",
"operation_kind",
"to_canonical_string",
"to_relation",
]