69a7d8bae8
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).
219 lines
9 KiB
Python
219 lines
9 KiB
Python
"""ADR-0201 — standalone tests for the propositional canonicalizer keystone.
|
||
|
||
Exercised in isolation, with no binding-graph wiring and no inference rules — the
|
||
same way :mod:`generate.math_symbolic_equivalence` is tested standalone. The point
|
||
is to prove the keystone holds ALONE before anything depends on it: equivalent
|
||
formulas collapse to one canonical key, non-equivalent ones don't, the form is
|
||
byte-deterministic, and out-of-regime / oversized inputs refuse rather than guess.
|
||
"""
|
||
|
||
from __future__ import annotations
|
||
|
||
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
|
||
|
||
|
||
def _key(formula: str) -> str:
|
||
return canonicalize(formula).canonical_key
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Canonicity: logically-equivalent formulas produce IDENTICAL keys.
|
||
# Each pair would FAIL if the diagram were not reduced/canonical.
|
||
# ---------------------------------------------------------------------------
|
||
|
||
EQUIVALENT_PAIRS = [
|
||
("P & Q", "Q & P"), # ∧ commutativity
|
||
("P | Q", "Q | P"), # ∨ commutativity
|
||
("~~P", "P"), # double negation
|
||
("P -> Q", "~P | Q"), # implication rewrite
|
||
("~(P & Q)", "~P | ~Q"), # De Morgan
|
||
("~(P | Q)", "~P & ~Q"), # De Morgan
|
||
("P <-> Q", "(P -> Q) & (Q -> P)"), # iff definition
|
||
("P & (Q | R)", "(P & Q) | (P & R)"), # distributivity
|
||
("P & P", "P"), # idempotence
|
||
("P", "P & (Q | ~Q)"), # irrelevant variable reduces out
|
||
("P | (P & Q)", "P"), # absorption
|
||
]
|
||
|
||
|
||
@pytest.mark.parametrize("a,b", EQUIVALENT_PAIRS)
|
||
def test_equivalent_formulas_share_canonical_key(a: str, b: str) -> None:
|
||
assert _key(a) == _key(b)
|
||
assert check_equivalence(a, b).verdict is Verdict.EQUIVALENT
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Discrimination: non-equivalent formulas produce DISTINCT keys.
|
||
# These guard against a degenerate canonicalizer that collapses everything.
|
||
# ---------------------------------------------------------------------------
|
||
|
||
NON_EQUIVALENT_PAIRS = [
|
||
("P & Q", "P | Q"),
|
||
("P", "Q"), # distinct atoms must not collide
|
||
("P -> Q", "Q -> P"), # implication is not symmetric
|
||
("P", "~P"),
|
||
("P & Q", "P"),
|
||
]
|
||
|
||
|
||
@pytest.mark.parametrize("a,b", NON_EQUIVALENT_PAIRS)
|
||
def test_non_equivalent_formulas_have_distinct_keys(a: str, b: str) -> None:
|
||
assert _key(a) != _key(b)
|
||
assert check_equivalence(a, b).verdict is Verdict.NOT_EQUIVALENT
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Terminals: tautologies and contradictions collapse to fixed keys.
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_tautologies_collapse_to_true_terminal() -> None:
|
||
for taut in ("P | ~P", "true", "P -> P", "(P -> Q) | (Q -> P)"):
|
||
c = canonicalize(taut)
|
||
assert c.is_tautology, taut
|
||
assert c.canonical_key == "T"
|
||
assert c.atoms == () # no variable survives a constant
|
||
|
||
|
||
def test_contradictions_collapse_to_false_terminal() -> None:
|
||
for contra in ("P & ~P", "false", "P <-> ~P"):
|
||
c = canonicalize(contra)
|
||
assert c.is_contradiction, contra
|
||
assert c.canonical_key == "F"
|
||
assert c.atoms == ()
|
||
|
||
|
||
def test_distinct_tautologies_are_the_same_truth_value() -> None:
|
||
# All tautologies are the constant-true function regardless of atoms.
|
||
assert _key("P | ~P") == _key("Q | ~Q") == _key("true")
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Surviving atoms: irrelevant variables are dropped from the support.
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_irrelevant_variable_is_dropped_from_support() -> None:
|
||
c = canonicalize("P & (Q | ~Q)")
|
||
assert c.atoms == ("P",) # Q is logically irrelevant
|
||
assert c.canonical_key == canonicalize("P").canonical_key
|
||
|
||
|
||
def test_substring_atoms_do_not_alias() -> None:
|
||
# Regression guard: atom 'a' must not be confused with atom 'ba'.
|
||
assert canonicalize("a & ba").atoms == ("a", "ba")
|
||
assert _key("a") != _key("ba")
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Determinism: same formula -> byte-identical key (the trace-hash discipline).
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
def test_canonical_key_is_byte_deterministic() -> None:
|
||
formula = "(P -> Q) & (R | ~S)"
|
||
assert canonicalize(formula).canonical_key == canonicalize(formula).canonical_key
|
||
|
||
|
||
def test_operator_spellings_are_equivalent() -> None:
|
||
assert _key("P and Q") == _key("P & Q") == _key("P ∧ Q") == _key("P && Q")
|
||
assert _key("P or Q") == _key("P | Q") == _key("P ∨ Q")
|
||
assert _key("not P") == _key("~P") == _key("¬P") == _key("!P")
|
||
assert _key("P implies Q") == _key("P -> Q") == _key("P → Q")
|
||
assert _key("P iff Q") == _key("P <-> Q") == _key("P ↔ Q")
|
||
|
||
|
||
# ---------------------------------------------------------------------------
|
||
# Refusal: out-of-grammar input and budget blowup REFUSE (wrong=0 discipline).
|
||
# ---------------------------------------------------------------------------
|
||
|
||
|
||
@pytest.mark.parametrize("bad", ["", "P &", "P Q", "(P", "P)", "P @ Q", "& P"])
|
||
def test_malformed_formula_refuses(bad: str) -> None:
|
||
with pytest.raises(LogicError):
|
||
canonicalize(bad)
|
||
v = check_equivalence(bad, "P")
|
||
assert v.verdict is Verdict.REFUSED
|
||
assert v.canonical_a is None and v.canonical_b is None
|
||
|
||
|
||
def test_budget_exceeded_refuses_rather_than_churns() -> None:
|
||
# A wide XOR-chain is the classic ROBDD blowup case; a tiny budget must
|
||
# trigger a typed refusal, not an unbounded build.
|
||
formula = " <-> ".join(f"v{i}" for i in range(40))
|
||
with pytest.raises(LogicBudgetError):
|
||
canonicalize(formula, max_nodes=8)
|
||
v = check_equivalence(formula, "true", max_nodes=8)
|
||
assert v.verdict is Verdict.REFUSED
|
||
assert "budget" in v.reason.lower()
|
||
|
||
|
||
def test_budget_error_is_a_logic_error_subclass() -> None:
|
||
# Callers that refuse on LogicError must also refuse on budget-exceeded.
|
||
assert issubclass(LogicBudgetError, LogicError)
|
||
|
||
|
||
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
|