feat: principled out-of-regime detector — typed out_of_decidable_regime (ADR-0201.1)
GPT-5.5's independent corpus caught that the canonicalizer refused quantified/ predicate input only by accident (tokenizer chokes on '.'), not by design — a by-luck-not-by-design refusal the wrong=0 discipline rejects. ADR-0202 §3 names a typed `out_of_decidable_regime` refusal; the keystone emitted a generic grammar error. - logic_canonical.py: LogicRegimeError(LogicError) + OUT_OF_DECIDABLE_REGIME; _reject_out_of_regime_text (quantifier words forall/exists + symbols ∀/∃, pre-scan) and _reject_out_of_regime_tokens (predicate-application ATOM-then-LPAREN), run BEFORE the generic grammar error. Refusal only — no predicate/FOL capability added. - logic_equivalence.py: typed regime branch (before the generic LogicError branch). - tests: 43 total (10 new) — OOR refuses with typed reason; equivalence path too; genuine grammar errors stay plain LogicError (no over-fire); `not (P)` not mistaken for predicate application. Mutation-verified by-design (neuter -> falls through to generic grammar error). - ADR-0201.1: additive sub-ADR of 0201 (not an amendment; sub-number preserves the landed ADR-0203 forward refs + phase-2 plan numbering). Honesty boundary load-bearing. Corpus now 22/22 (PC-OOR-001/002 agree on the principled reason). Full canonicalizer suite green; smoke 67 passed. modus_ponens rule-reasons remain deferred to ADR-0205 (2.3).
This commit is contained in:
Shay
parent
f715c54e3c
commit
69a7d8bae8
4 changed files with 252 additions and 3 deletions
112
docs/decisions/ADR-0201.1-out-of-regime-detector.md
Normal file
112
docs/decisions/ADR-0201.1-out-of-regime-detector.md
Normal file
|
|
@ -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.
|
||||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in a new issue