diff --git a/docs/decisions/ADR-0201.1-out-of-regime-detector.md b/docs/decisions/ADR-0201.1-out-of-regime-detector.md new file mode 100644 index 00000000..25c2a9ca --- /dev/null +++ b/docs/decisions/ADR-0201.1-out-of-regime-detector.md @@ -0,0 +1,112 @@ +# ADR-0201.1 — Principled Out-of-Regime Detector (`out_of_decidable_regime`) + +**Status:** Accepted (additive hardening of ADR-0201; phase-1 canonicalizer) +**Date:** 2026-06-02 +**Relates to:** **ADR-0201** (propositional canonicalizer — this hardens it; see +§amend-vs-additive), ADR-0202 §3 (the contract that names this typed refusal), +ADR-0203 (the prior additive-not-amend precedent). + +--- + +## Context + +GPT-5.5's independent proof-chain corpus (the separate-author oracle for +`logic_canonical.py`) cross-checked **22/22** cases against the *real* +canonicalizer. Twenty agreed exactly; two — the out-of-regime probes +`forall x. rains(x) -> wet(x)` and `exists x. wet(x)` — agreed on **outcome** +(both refused) but disagreed on the **reason**: + +- ADR-0202 §3 names a typed refusal: quantified/predicate input "must REFUSE + (`out_of_decidable_regime`)." +- The keystone refused, but with a generic `LogicError: "unexpected character + '.' at position 8"` — it had **no regime detector**. It refused these inputs + only because the tokenizer incidentally chokes on the `.` (or trips on the + predicate `(`). + +That is a **by-luck-not-by-design refusal** — the exact failure mode the +`wrong == 0` discipline rejects. The propositional-only boundary that ADR-0202 +declares load-bearing was being enforced by accident, not on purpose. Blessing +it (relaxing the contract) would write the accident into the contract. The +corpus caught precisely the thing an independent oracle exists to catch. + +## Decision + +Make the boundary principled. Add a typed regime refusal, checked **before** the +generic grammar error: + +- **`LogicRegimeError(LogicError)`** carrying the typed reason + `OUT_OF_DECIDABLE_REGIME = "out_of_decidable_regime"`. A `LogicError` subclass, + so callers refusing on `LogicError` still refuse — but the regime boundary is + now distinguishable from a malformed-propositional-formula grammar error. +- **`_reject_out_of_regime_text(formula)`** — a raw-text pre-scan (before + tokenizing) for quantifier markers: the words `forall`/`exists` (word-boundary, + case-insensitive) and the symbols `∀`/`∃`. `forall`/`exists` are thereby + reserved — not usable as atom ids. +- **`_reject_out_of_regime_tokens(tokens)`** — a token-stream scan for + **predicate-application shape**: an `ATOM` immediately followed by `(`. In the + propositional grammar an atom is never followed by `(`, so `ATOM (` is a + predicate (`rains(x)`), not a well-formed formula. Keyword operators (`not`, + `and`, …) are not `ATOM` tokens, so `not (P)` is unaffected. +- `canonicalize` runs `_reject_out_of_regime_text` → `_tokenize` → + `_reject_out_of_regime_tokens` → parse. `check_equivalence` surfaces the typed + reason via a `LogicRegimeError` branch placed before its generic `LogicError` + branch. + +This is a **refusal**, not new capability: the engine still does no +predicate/FOL reasoning. It now refuses it **on purpose**, with an inspectable +typed reason, instead of by tokenizer accident. + +## amend-vs-additive + +**This is a new additive sub-ADR (ADR-0201.1), not an amendment of the landed +ADR-0201** — same discipline as ADR-0203-vs-0132: the regime detector became +load-bearing only when the corpus surfaced the incidental-refusal gap; recording +it additively preserves that *why-added-later* history rather than rewriting the +closed canonicalizer record. + +Chosen as a **sub-number (0201.1), not a fresh top-level number**, for two +reasons: (a) it is specifically a hardening of the ADR-0201 canonicalizer (same +module, same phase-1 keystone), which the sub-number communicates precisely; and +(b) a top-level `ADR-0204` would collide with the forward references in the +already-merged ADR-0203 and the recorded phase-2 plan (`0204` = wiring, `0205` = +modus_ponens, `0206` = grounding). The sub-number keeps those intact. + +## Honesty boundary (load-bearing — carried by every phase-2 ADR, 0203–0205) + +Through phase 2.3, `proof_chain` is **sound over its declared atoms**, not +grounded in recognized input (grounding is phase 2.4). This ADR does **not** +soften that, and it does not add predicate/FOL reasoning — it makes the +**propositional-only** boundary principled by refusing out-of-regime input with a +typed reason. The boundary is enforced by design, never "reasons over input." + +## Evidence + +- `tests/test_logic_canonical.py` — 43 tests (33 keystone + 10 new): quantifier + words/symbols and predicate application refuse with `LogicRegimeError` / + `out_of_decidable_regime`; the equivalence path surfaces the typed reason; + genuine grammar errors (`P &`, `P @ Q`, `(P`) still raise *plain* `LogicError` + (detector does not over-fire); `not (P)` is not mistaken for predicate + application. +- **Mutation-verified by-design:** neutering both detectors makes + `forall x. …` fall through to the generic grammar error + (`unexpected character '.'`) instead of the typed reason — + `test_out_of_regime_refuses_with_typed_reason` would fail. The boundary holds + on purpose, not by luck. +- **Corpus now 22/22:** the two OOR cases (PC-OOR-001/002) now agree on the + principled `out_of_decidable_regime` reason. +- Full canonicalizer suite green; smoke: 67 passed. + +## Note carried to the corpus (rule-reasons pending 2.3) + +The 3 `modus_ponens` corpus cases were validated only at the **entailment** level +the canonicalizer provides (`(⋀premises) → conclusion` is/ isn't a tautology). +Their typed *rule* reasons (`modus_ponens_conclusion_mismatch`, +`modus_ponens_missing_implication`) are **deferred to ADR-0205** (phase 2.3), when +the `modus_ponens` rule is built. The corpus should carry an explicit +"rule-reasons pending 2.3" marker on those cases so the deferral is recorded, not +assumed validated. + +## Scope + +Phase-1 canonicalizer hardening only. Does **not** build `modus_ponens`, +binding-graph wiring, or any predicate/FOL support. diff --git a/generate/logic_canonical.py b/generate/logic_canonical.py index 8933de8b..bf13cd2d 100644 --- a/generate/logic_canonical.py +++ b/generate/logic_canonical.py @@ -30,6 +30,7 @@ hand-rolled symbolic normalizer. from __future__ import annotations +import re from dataclasses import dataclass from typing import Final @@ -50,6 +51,21 @@ class LogicBudgetError(LogicError): math gate refusing rather than churning.""" +class LogicRegimeError(LogicError): + """Raised when the input is outside the decidable **propositional** regime — + quantified or predicate logic (ADR-0201.1; the typed refusal ADR-0202 §3 + names). A subclass of :class:`LogicError` so callers that refuse on + ``LogicError`` refuse here too, but it carries the typed + :data:`OUT_OF_DECIDABLE_REGIME` reason so the regime boundary is + distinguishable from a generic malformed-formula grammar error. + + Crucially, the boundary is enforced **by design** (see + :func:`_reject_out_of_regime_text` / :func:`_reject_out_of_regime_tokens`), + not by the tokenizer incidentally choking on an out-of-grammar character — + the latter is the by-luck-not-by-design refusal the ``wrong == 0`` + discipline rejects.""" + + # --------------------------------------------------------------------------- # Public defaults # --------------------------------------------------------------------------- @@ -460,11 +476,69 @@ class CanonicalProposition: is_contradiction: bool +# --------------------------------------------------------------------------- +# Out-of-regime detection (ADR-0201.1) +# +# Propositional logic is the only regime with a canonical form + decidable +# equivalence. Quantified / predicate input must REFUSE with the typed +# `out_of_decidable_regime` reason (ADR-0202 §3) — by DESIGN, recognized as +# out-of-regime, not by accident of the tokenizer choking on an out-of-grammar +# character. These checks run BEFORE the generic grammar error so the regime +# boundary is principled, typed, and inspectable. +# --------------------------------------------------------------------------- + +OUT_OF_DECIDABLE_REGIME: Final[str] = "out_of_decidable_regime" + +# Quantifier markers: ASCII keywords (word-boundary, case-insensitive) and the +# logic symbols ∀ / ∃. Their presence means first-order/predicate reasoning, +# which has no ROBDD canonical form and is undecidable in general. `forall` and +# `exists` are therefore reserved — not usable as atom ids. +_QUANTIFIER_WORD_RE: Final[re.Pattern[str]] = re.compile(r"\b(forall|exists)\b", re.IGNORECASE) +_QUANTIFIER_SYMBOLS: Final[frozenset[str]] = frozenset({"∀", "∃"}) # ∀ ∃ + + +def _reject_out_of_regime_text(formula: str) -> None: + """Refuse raw input that carries a quantifier marker. Runs before tokenizing + so quantifier symbols (∀/∃) and the ``forall x. …`` / ``exists x. …`` shape + refuse with the typed regime reason rather than a generic 'unexpected + character' grammar error from the trailing ``.``/predicate syntax.""" + for sym in sorted(_QUANTIFIER_SYMBOLS): + if sym in formula: + raise LogicRegimeError(f"{OUT_OF_DECIDABLE_REGIME}: quantifier symbol {sym!r}") + match = _QUANTIFIER_WORD_RE.search(formula) + if match is not None: + raise LogicRegimeError(f"{OUT_OF_DECIDABLE_REGIME}: quantifier {match.group(0)!r}") + + +def _reject_out_of_regime_tokens(tokens: list[tuple[str, str]]) -> None: + """Refuse predicate-application shape — an atom immediately applied to an + argument list, e.g. ``rains(x)``. In the propositional grammar an atom is + never followed by ``(`` (grouping only follows an operator or opens an + expression), so ``ATOM (`` is a predicate, not a well-formed propositional + formula. Runs before the parser's generic trailing-token error so the regime + boundary is the reason that surfaces. (Keyword operators such as ``not`` are + NOT ``ATOM`` tokens, so ``not (P)`` is unaffected.)""" + for (kind, lexeme), (next_kind, _next_lexeme) in zip(tokens, tokens[1:]): + if kind == "ATOM" and next_kind == "LPAREN": + raise LogicRegimeError( + f"{OUT_OF_DECIDABLE_REGIME}: predicate application {lexeme!r}(…)" + ) + + def canonicalize(formula: str, *, max_nodes: int = DEFAULT_MAX_NODES) -> CanonicalProposition: """Canonicalize ``formula`` to its ROBDD identity under the sorted-atom - ordering. Raises :class:`LogicError` on out-of-grammar input and - :class:`LogicBudgetError` if the diagram exceeds ``max_nodes``.""" - ast = _Parser(_tokenize(formula)).parse() + ordering. Refusal-first: + + * :class:`LogicRegimeError` (``out_of_decidable_regime``) if the input is + quantified / predicate logic — checked *before* grammar, so the regime + boundary is principled, not an incidental tokenizer failure; + * :class:`LogicError` on out-of-grammar (malformed propositional) input; + * :class:`LogicBudgetError` if the diagram exceeds ``max_nodes``. + """ + _reject_out_of_regime_text(formula) + tokens = _tokenize(formula) + _reject_out_of_regime_tokens(tokens) + ast = _Parser(tokens).parse() declared = tuple(sorted(_collect_atoms(ast))) # fixed variable ordering index_of = {name: i for i, name in enumerate(declared)} bdd = _Bdd(var_count=len(declared), max_nodes=max_nodes) diff --git a/generate/logic_equivalence.py b/generate/logic_equivalence.py index 55d2da75..3a3693e0 100644 --- a/generate/logic_equivalence.py +++ b/generate/logic_equivalence.py @@ -19,8 +19,10 @@ from typing import Final from generate.logic_canonical import ( DEFAULT_MAX_NODES, + OUT_OF_DECIDABLE_REGIME, LogicBudgetError, LogicError, + LogicRegimeError, canonicalize, ) @@ -65,6 +67,15 @@ def check_equivalence( canonical_b=None, reason=f"canonicalization_budget_exceeded: {exc}", ) + except LogicRegimeError as exc: + # Out of the decidable propositional regime (quantified/predicate). + # Caught before the generic LogicError branch since it is a subclass. + return EquivalenceVerdict( + verdict=Verdict.REFUSED, + canonical_a=None, + canonical_b=None, + reason=f"{OUT_OF_DECIDABLE_REGIME}: {exc}", + ) except LogicError as exc: return EquivalenceVerdict( verdict=Verdict.REFUSED, diff --git a/tests/test_logic_canonical.py b/tests/test_logic_canonical.py index 1674fe5c..325e15ea 100644 --- a/tests/test_logic_canonical.py +++ b/tests/test_logic_canonical.py @@ -13,8 +13,10 @@ import pytest from generate.logic_canonical import ( DEFAULT_MAX_NODES, + OUT_OF_DECIDABLE_REGIME, LogicBudgetError, LogicError, + LogicRegimeError, canonicalize, ) from generate.logic_equivalence import Verdict, check_equivalence @@ -165,3 +167,53 @@ def test_bounded_formula_stays_within_default_budget() -> None: # A realistic proof-step proposition canonicalizes well within budget. c = canonicalize("(P -> Q) & (Q -> R) & P", max_nodes=DEFAULT_MAX_NODES) assert c.canonical_key # non-empty, did not refuse + + +# --------------------------------------------------------------------------- +# Out-of-regime: quantified / predicate input REFUSES with the typed reason +# (ADR-0201.1). The boundary is enforced by DESIGN, before the generic grammar +# error — not by the tokenizer incidentally choking on '.' or a predicate '('. +# --------------------------------------------------------------------------- + +OUT_OF_REGIME_INPUTS = [ + "forall x. rains(x) -> wet(x)", # universal (the PC-OOR-001 corpus case) + "exists x. wet(x)", # existential (PC-OOR-002) + "∀ x rains", # quantifier symbol + "∃ y wet", # quantifier symbol + "rains(x)", # predicate application, no quantifier word + "P & wet(y)", # predicate application mid-formula + "FORALL z holds", # case-insensitive keyword +] + + +@pytest.mark.parametrize("text", OUT_OF_REGIME_INPUTS) +def test_out_of_regime_refuses_with_typed_reason(text: str) -> None: + with pytest.raises(LogicRegimeError) as exc: + canonicalize(text) + assert OUT_OF_DECIDABLE_REGIME in str(exc.value) + # And the equivalence path surfaces the typed reason, not a generic one. + v = check_equivalence(text, "P") + assert v.verdict is Verdict.REFUSED + assert OUT_OF_DECIDABLE_REGIME in v.reason + + +def test_regime_error_is_a_logic_error_subclass() -> None: + # Callers refusing on LogicError still refuse on out-of-regime. + assert issubclass(LogicRegimeError, LogicError) + + +def test_genuine_grammar_errors_are_not_misreported_as_out_of_regime() -> None: + # The detector is principled: malformed *propositional* input is a plain + # LogicError (grammar), NOT a regime refusal. Guards against over-firing. + for bad in ["P &", "P @ Q", "P -> -> Q", "(P", "P)"]: + with pytest.raises(LogicError) as exc: + canonicalize(bad) + assert not isinstance(exc.value, LogicRegimeError), bad + assert OUT_OF_DECIDABLE_REGIME not in str(exc.value), bad + + +def test_keyword_operators_before_paren_are_not_predicate_application() -> None: + # `not (P)` is valid: NOT is a keyword operator, not an ATOM, so the + # ATOM-then-LPAREN predicate rule must not fire. + assert canonicalize("not (P)").canonical_key == canonicalize("~P").canonical_key + assert canonicalize("not(P)").canonical_key == canonicalize("~P").canonical_key