diff --git a/docs/decisions/ADR-0201-proposition-canonicalizer.md b/docs/decisions/ADR-0201-proposition-canonicalizer.md new file mode 100644 index 00000000..b9b1cc3e --- /dev/null +++ b/docs/decisions/ADR-0201-proposition-canonicalizer.md @@ -0,0 +1,126 @@ +# ADR-0201 — Propositional Canonicalizer (the `proof_chain` keystone) + +**Status:** Proposed (Phase 1 of `proof_chain`; standalone keystone shipped, not yet wired) + +**Date:** 2026-06-02 + +**Relates to:** ADR-0131.1.B (`math_symbolic_equivalence` — the sibling pattern this +mirrors), ADR-0132/0133/0134/0135 (binding-graph data model / adapter / +admissibility / question-target — the future consumer), the `wrong == 0` +self-verification doctrine in `generate/derivation/verify.py`. + +## Context + +CORE has confirmed three things about building `proof_chain` as a real reasoning +primitive (not a declared label): + +1. The ledger "operators" (`proof_chain`/`causal`/`modal`) are classification + labels, not executors — `proof_chain` is green-field. +2. The `wrong == 0` self-check is **soundness, not correctness**: it fires only + when grounded+licensed derivations collapse to **one unique canonical + conclusion** and rivals are checked for agreement. It needs a *canonical, + comparable* conclusion. For arithmetic, exact numeric equality gave that for + free. +3. The ADR-0132 binding graph is already the DAG substrate proof trees need + (`BoundEquation.dependencies` + per-node admissibility + provenance), with a + shipped, hand-rolled sibling — `math_symbolic_equivalence` — that already + demonstrates the `normalize → canonical-string → byte-equality → + three-valued-verdict-with-REFUSED` discipline for algebra. + +Logic does **not** get a comparable canonical conclusion for free: two +syntactically different formulas can be logically equivalent (`P∧Q ≡ Q∧P`, +`¬¬P ≡ P`, `P→Q ≡ ¬P∨Q`). Without a canonical form, the uniqueness/disagreement +rule cannot fire and `proof_chain` degrades from sound to merely cautious. This +ADR scopes the canonical form — the keystone everything else (rule checkers, the +disagreement rule) depends on. + +## Decision + +Canonicalize a propositional formula to a **Reduced Ordered Binary Decision +Diagram (ROBDD)** under a fixed (sorted-atom) variable ordering, and use a +canonical *string* serialization of the reduced diagram as the byte-equality +discriminator (the logic analog of `Polynomial.to_canonical_string()`). + +- **ROBDD, not CNF/DNF.** For a fixed ordering the ROBDD is *canonical* — two + formulas are logically equivalent **iff** their reduced diagrams are isomorphic. + CNF/DNF are merely *normal* (standardized shape), not canonical, and have no + poly-time equivalence-preserving transform. Free bonuses for later: tautology = + the 1-terminal, contradiction = the 0-terminal, `f→g` valid iff + `apply(f, ¬g, ∧)` = the 0-terminal — so `contradiction` and proof "conclusion + follows" reduce to ROBDD checks. +- **Hand-rolled minimal**, no external BDD library (operator-confirmed). Stays in + CORE's idiom (the symbolic substrate is entirely hand-rolled), deterministic by + construction, fully inspectable, zero opaque dependencies. ~370 LOC: + tokenizer + recursive-descent parser + `mk`/`apply`/`negate` + unique table + + canonical serialization. +- **`wrong == 0` discipline preserved.** No approximate path. Out-of-grammar input + raises `LogicError`; a diagram exceeding the node budget raises + `LogicBudgetError` (a `LogicError` subclass, so callers refusing on `LogicError` + refuse on budget too). Both surface as a `REFUSED` verdict — refuse rather than + guess or churn. + +## Honesty boundary (stated, not hidden) + +- **Propositional logic** (finite Boolean variables): canonical and decidable. + ROBDD gives a unique form + constant-time equivalence. The full soundness gate + transfers. **This is the only regime this module claims.** +- **Cost caveat:** ROBDD *size* can be exponential in the worst case and is + ordering-sensitive. Canonicity is cheap to *compare* but not always cheap to + *build*. For bounded proof-step propositions (a handful of atoms) this is a + non-issue; the node budget refuses on adversarial blowup rather than hanging. +- **Predicate / first-order logic:** NOT canonical in general — undecidable. There + is no ROBDD-style canonical form for full FOL. **We do NOT claim `wrong == 0` + for quantified reasoning** with this machinery. Quantifier-free fragments and + specific decidable theories are later, separately-scoped steps, each with their + own honest decidability claim. + +## What shipped in this phase (standalone) + +- `generate/logic_canonical.py` — `canonicalize(formula, *, max_nodes) -> + CanonicalProposition{canonical_key, atoms, is_tautology, is_contradiction}`; + `LogicError` / `LogicBudgetError`. +- `generate/logic_equivalence.py` — `check_equivalence(a, b) -> + EquivalenceVerdict{EQUIVALENT|NOT_EQUIVALENT|REFUSED}` (close mirror of + `math_symbolic_equivalence`). +- `tests/test_logic_canonical.py` — 33 standalone tests: canonicity laws + (commutativity, double-negation, De Morgan, implication rewrite, distributivity, + absorption, irrelevant-variable elision), discrimination (non-equivalent → + distinct keys), terminal collapse, byte-determinism, operator-spelling parity, + and the refusal paths (malformed → `LogicError`; budget blowup → `LogicBudgetError`). + +Tested **in isolation**, exactly as the sibling is standalone — proving the +keystone holds alone before anything depends on it. + +## Proof obligation (per CLAUDE.md §Schema-Defined Proof Obligations) + +The canonicity tests must be able to *meaningfully fail*. Verified by mutation: +disabling the redundant-node reduction rule (`low == high → low`) flips +`P ∧ (Q ∨ ¬Q) ≡ P` to false, failing `test_irrelevant_variable_is_dropped_from_support`. +The equivalent-pairs and non-equivalent-pairs suites are mutually constraining: a +collapse-everything canonicalizer fails discrimination; a no-reduction +canonicalizer fails equivalence. The suite is non-vacuous by construction. + +## Explicitly deferred (NOT in this phase) + +- **Binding-graph wiring.** `proof_chain` would be the binding graph's *first* + consumer — there is no existing graph-builder→serving path to join. The + integration is **net-new wiring**, scoped separately. The canonical key is + designed to drop into `BoundEquation.rhs_canonical` (a string field) when that + wiring is built. +- **The acyclicity refusal.** A cycle in a proof DAG is circular reasoning; the + binding graph currently checks referential integrity but not cycles. The + `circular_dependency` refusal is net-new and must land *before* the structure + is load-bearing — not in this standalone phase. +- **Inference rules.** No `operation_kind` logic vocab and no `_check_modus_ponens` + yet. One sound rule (`modus_ponens`) + the disagreement rule on the canonical + key is the next phase, once this keystone is accepted. + +## Alternatives considered + +- **CNF/DNF canonical string** — rejected: not canonical (clause/literal ordering + is non-unique), and no poly-time equivalence-preserving transform exists. +- **External BDD library (`dd` / CUDD)** — rejected: the only opaque dependency in + an otherwise hand-rolled substrate; determinism/`trace_hash` risk from + hash-based node ids and reordering heuristics; CUDD is a C build/footprint cost; + and the canonical-string serialization would still need to be hand-controlled + for determinism, so the library does not save the load-bearing work. diff --git a/docs/decisions/ADR-0202-proposition-representation-contract.md b/docs/decisions/ADR-0202-proposition-representation-contract.md new file mode 100644 index 00000000..06a606d9 --- /dev/null +++ b/docs/decisions/ADR-0202-proposition-representation-contract.md @@ -0,0 +1,213 @@ +# ADR-0202 — Proposition Representation Contract (`proof_chain`) + +**Status:** Accepted (normative contract — single source for the canonicalizer and the proof corpus) +**Date:** 2026-06-02 +**Relates to:** ADR-0201 (propositional canonicalizer — the formula layer's implementation), +ADR-0144 (PropositionGraph epistemic carrier — the atom layer's home), +ADR-0143/0142 (recognition outcome / epistemic state taxonomy), +ADR-0132 (binding-graph data model — the proof DAG substrate), +ADR-0131.3 (bounded-grammar word-problem lane — the eval-case shape this slots into). + +--- + +## Why this document exists + +`proof_chain` introduces propositional formulas to CORE. Two producers must agree +on **one** representation or they diverge: the canonicalizer +(`generate/logic_canonical.py`) and the proof corpus authored in parallel. + +CORE already carries four "proposition"-named structures — the articulation +`Proposition`/`PropositionGraph` (`generate/`), the ADR-0144 epistemic carrier +(`recognition/`), and the ADR-0132 symbolic-math binding graph. **None** is a +truth-functional propositional-logic formula representation. So the formula +language is net-new; but its *atoms* must ground to the existing epistemic carrier, +not float free — otherwise `proof_chain` becomes a fifth, disconnected proposition +dialect, the exact fragmentation ADR-0144 was created to resolve. + +This contract is that single source. **The canonicalizer is authoritative for the +formula grammar**; any grammar change updates this doc in the *same* PR (mirroring +the `docs/runtime_contracts.md` discipline). + +The representation is **two layers**: + +- **Atom layer** (authoritative, existing) — atoms are declared stable symbol ids + that bind to ADR-0144 `EpistemicNode`/`FeatureBundle` carriers. +- **Formula layer** (net-new — ADR-0201) — truth-functional formulas over those + atoms, canonicalized to ROBDD identity. + +--- + +## 1. Formula layer — grammar (exact, from `generate/logic_canonical.py`) + +### 1.1 Tokens + +- **Atom:** an identifier — first char `[A-Za-z_]`, subsequent `[A-Za-z0-9_]`. + Atom ids are **case-sensitive** (`P` ≠ `p`). Reserved keywords (below) are not atoms. +- **Constants:** `true`, `false` (keywords, case-insensitive). +- **Operators** — each kind has multiple accepted spellings (ASCII, doubled, + unicode, keyword). All spellings of a kind are interchangeable and produce the + identical canonical key: + + | Kind | Spellings | + |---|---| + | NOT (unary) | `not`, `~`, `!`, `¬` | + | AND | `and`, `&`, `&&`, `∧` | + | OR | `or`, `\|`, `\|\|`, `∨` | + | IMPLIES | `implies`, `->`, `→`, `⊃` | + | IFF | `iff`, `<->`, `↔`, `≡` | + | grouping | `(` … `)` | + + Keyword operators are matched case-insensitively (`AND` = `and`). Whitespace is + insignificant. Any character outside this grammar is a refusal (§3). + +### 1.2 Precedence and associativity + +Lowest → highest binding: + +``` +IFF < IMPLIES < OR < AND < NOT < atom / ( … ) +``` + +- `IMPLIES` is **right-associative**: `P -> Q -> R` ≡ `P -> (Q -> R)`. +- `IFF`, `OR`, `AND` are left-associative (associativity is semantically + irrelevant under ROBDD, but the parse is fixed so errors are crisp). +- `NOT` is prefix unary. Parentheses override precedence. + +### 1.3 Grammar (EBNF) + +```ebnf +formula = iff ; +iff = implies , { IFF , implies } ; +implies = or , [ IMPLIES , implies ] ; (* right-assoc *) +or = and , { OR , and } ; +and = unary , { AND , unary } ; +unary = NOT , unary | atom ; +atom = ATOM | "true" | "false" | "(" , iff , ")" ; +``` + +### 1.4 Canonical form + +A formula is canonicalized to a **Reduced Ordered Binary Decision Diagram (ROBDD)** +under the **sorted-atom variable ordering** (the atoms appearing in the formula, +sorted lexicographically). The reduced diagram is serialized to the +`canonical_key` string. Contract: + +- **Equivalence = byte-equality** of `canonical_key`. Two formulas are logically + equivalent **iff** their keys are identical. +- **Tautology → `"T"`**, **contradiction → `"F"`** (every tautology shares the key + `T` regardless of atoms; likewise `F`). +- **Logically-irrelevant atoms are dropped from the support**: `P` and + `P ∧ (Q ∨ ¬Q)` produce the same key; `Q` is not in the result's `atoms`. +- The key is **byte-deterministic across processes** (structural serialization — + no object ids, no hashing, no dict-order dependence), satisfying the + `trace_hash` discipline. It is human-inspectable, not an opaque digest: + e.g. `(P→Q)∧(R∨¬S)∧P` → `0:S?F:T;1:R?T:@0;2:Q?@1:F;3:P?@2:F`. + +The key is the propositional twin of `BoundEquation.rhs_canonical` (ADR-0132): when +`proof_chain` wires to the binding graph, the canonical key occupies `rhs_canonical`, +the discharged premises occupy `dependencies`, and the inference rule occupies +`operation_kind`. + +--- + +## 2. Atom layer — declared symbol ids that bind to the epistemic carrier + +**Atoms are not free-form prose.** Each atom is a declared, stable symbol id +(matching the §1.1 atom grammar) that **will bind** to an ADR-0144 `EpistemicNode` +carrying a recognized `FeatureBundle`. A corpus case declares its atoms explicitly. + +### 2.1 Declaration rules + +- Atom ids are unique within a case; the same id denotes the same proposition + throughout that case. Recommended convention: `[_]`, e.g. + `P_rains`, `Q_ground_wet`. +- Every atom declares a human-readable `gloss`. +- **Where an atom maps to a recognizable fact, the case MUST record the intended + `FeatureBundle` binding** (the feature name→value mapping per ADR-0143/0144), + so the corpus is future-compatible with the grounding-half wiring and needs **no + second pass** when atom-grounding lands. The actual `EpistemicNode.node_id` + (`teaching_set_id:turn_index`) is assigned at recognition time and is therefore + **not** authored into the corpus; the binding resolves by matching the recorded + feature mapping. +- Atoms that are pure logical variables with no recognizable-fact referent (e.g. + abstract `P`/`Q` in a rule-shape case) record `gloss` only and `binding: null`. + This is allowed and expected for schematic cases. + +### 2.2 Per-case atom block (normative shape) + +```json +{ + "atoms": { + "P_rains": { + "gloss": "it is raining", + "binding": { + "features": { "agent": "sky", "relation": "is", "state": "raining" } + } + }, + "Q_ground_wet": { + "gloss": "the ground is wet", + "binding": { "features": { "agent": "ground", "relation": "is", "state": "wet" } } + }, + "R": { "gloss": "an abstract proposition", "binding": null } + }, + "premises": ["P_rains -> Q_ground_wet", "P_rains"], + "conclusion": "Q_ground_wet", + "rule": "modus_ponens", + "expected": "provable" +} +``` + +`features` keys are the `FeatureBundle` feature names (ADR-0143 `BoundFeature.name`); +values are their bound values. The bundle's canonical sorted-by-name order is +enforced by `FeatureBundle.__post_init__` at grounding time — authors need not +pre-sort. `premises`/`conclusion`/`rule`/`expected` fields compose with the +ADR-0131.3 bounded-grammar case shape; this contract governs only `atoms` and the +formula strings. + +--- + +## 3. Honesty boundary (binding) + +- **Propositional logic only** — finite Boolean atoms. In this regime the ROBDD is + canonical and equivalence is decidable, so the `wrong == 0` soundness gate + transfers intact. +- **No predicate / first-order / quantified logic.** Equivalence over quantifiers + on infinite domains is undecidable; there is no ROBDD-style canonical form. + **Do NOT claim `wrong == 0` for quantified reasoning.** A formula that requires + quantifier reasoning is out of regime and must **REFUSE** + (`out_of_decidable_regime`), not be silently dropped to a weaker check. + Quantifier-free fragments and specific decidable theories are later, + separately-scoped work, each with its own honest decidability claim. +- **Refusal-first, no approximation.** The canonicalizer either returns the exact + canonical key or refuses: + - out-of-grammar input → `LogicError` → `REFUSED`; + - ROBDD exceeds the node budget → `LogicBudgetError` (a `LogicError` subclass) → + `REFUSED` (`canonicalization_budget_exceeded`) — refuse rather than churn. + Corpus cases that expect refusal must name the typed reason. + +--- + +## 4. Conformance checklist (corpus authors) + +A case conforms to this contract iff: + +- [ ] every formula uses only the §1 grammar — no invented connectives or spellings; +- [ ] every atom referenced in a formula is declared in the case's `atoms` block; +- [ ] atom ids match the §1.1 atom grammar and are stable within the case; +- [ ] every declared atom carries a `gloss`; recognizable-fact atoms carry an + intended `FeatureBundle` `binding`, schematic atoms carry `binding: null`; +- [ ] no quantifiers, predicates, or function symbols appear; +- [ ] the expected outcome is one of `provable` / `not_provable` / `refused` + (with a typed reason for `refused`); +- [ ] equivalence/identity claims rely on the `canonical_key`, never on formula + surface string equality. + +--- + +## 5. Source-of-truth rule + +`generate/logic_canonical.py` is authoritative for the formula grammar and +canonical form. This document is authoritative for the atom layer and the honesty +boundary. Any change to the formula grammar updates §1 of this doc in the **same +PR** as the code change. The proof corpus conforms to this doc; it does not extend +the grammar or the atom convention on its own. diff --git a/generate/logic_canonical.py b/generate/logic_canonical.py new file mode 100644 index 00000000..8933de8b --- /dev/null +++ b/generate/logic_canonical.py @@ -0,0 +1,481 @@ +"""ADR-0201 — Propositional canonicalizer (the ``proof_chain`` keystone). + +Boolean-logic twin of :mod:`generate.math_symbolic_normalizer` / +:mod:`generate.math_symbolic_equivalence`. Where the algebra side normalizes an +expression to a canonical *polynomial string* and compares by byte-equality, this +module canonicalizes a propositional formula to a **Reduced Ordered Binary Decision +Diagram (ROBDD)** under a fixed (sorted) variable ordering and emits a canonical +*string* serialization of the reduced diagram. + +Why ROBDD, not CNF/DNF: for a fixed variable ordering the ROBDD is canonical — +two formulas are logically equivalent **iff** their reduced diagrams are +isomorphic. CNF/DNF are merely normal (standardized shape), not canonical, and +have no poly-time equivalence-preserving transform. The reduced diagram collapses +logically-irrelevant variables, so ``P`` and ``P ∧ (Q ∨ ¬Q)`` produce the same key. + +``wrong == 0`` discipline (mirrors the sibling): the canonicalizer **refuses** +rather than guesses. Out-of-grammar input raises :class:`LogicError`; a diagram +that would exceed the node budget raises :class:`LogicBudgetError` (a subclass, so +callers catching :class:`LogicError` refuse on both) rather than churning. There is +no approximate path — an answer is either the exact canonical form or a refusal. + +Honesty boundary: this is **propositional** logic only (finite Boolean variables — +decidable, canonical). It does NOT canonicalize quantifiers/predicate logic and +must not be used to claim ``wrong == 0`` for first-order reasoning. + +Hand-rolled (no external BDD library) to stay in CORE's idiom: deterministic by +construction, fully inspectable, zero opaque dependencies — the same posture as the +hand-rolled symbolic normalizer. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from typing import Final + +# --------------------------------------------------------------------------- +# Errors (twin of math_symbolic_normalizer.SymbolicError) +# --------------------------------------------------------------------------- + + +class LogicError(ValueError): + """Raised when a formula cannot be canonicalized. Refusal-first; never + coerces a malformed or out-of-regime input into a guess.""" + + +class LogicBudgetError(LogicError): + """Raised when the ROBDD would exceed the node budget (the exponential-blowup + guard). A subclass of :class:`LogicError` so callers that refuse on + ``LogicError`` refuse on budget-exceeded too — the proof-domain analog of the + math gate refusing rather than churning.""" + + +# --------------------------------------------------------------------------- +# Public defaults +# --------------------------------------------------------------------------- + +DEFAULT_MAX_NODES: Final[int] = 100_000 +"""Default cap on reduced-diagram nodes. Bounded proof-step propositions relate a +handful of atoms; this is generous for that regime and refuses on adversarial +blowup rather than hanging.""" + +# Terminal node ids. 0 = constant false, 1 = constant true. Non-terminal ids >= 2. +_FALSE: Final[int] = 0 +_TRUE: Final[int] = 1 + + +# --------------------------------------------------------------------------- +# Tokenizer +# --------------------------------------------------------------------------- + +# Multi-character / unicode operator spellings, longest first so the scanner is +# unambiguous. Each maps to a canonical token kind. +_OPERATOR_SPELLINGS: Final[tuple[tuple[str, str], ...]] = ( + ("<->", "IFF"), + ("↔", "IFF"), + ("≡", "IFF"), + ("->", "IMPLIES"), + ("→", "IMPLIES"), + ("⊃", "IMPLIES"), + ("∧", "AND"), + ("&&", "AND"), + ("&", "AND"), + ("∨", "OR"), + ("||", "OR"), + ("|", "OR"), + ("¬", "NOT"), + ("~", "NOT"), + ("!", "NOT"), + ("(", "LPAREN"), + (")", "RPAREN"), +) + +# Keyword operators / constants (matched on word boundaries, case-insensitive). +_KEYWORDS: Final[dict[str, str]] = { + "and": "AND", + "or": "OR", + "not": "NOT", + "implies": "IMPLIES", + "iff": "IFF", + "true": "TRUE", + "false": "FALSE", +} + + +def _is_ident_start(ch: str) -> bool: + return ch.isalpha() or ch == "_" + + +def _is_ident_char(ch: str) -> bool: + return ch.isalnum() or ch == "_" + + +def _tokenize(text: str) -> list[tuple[str, str]]: + """Scan ``text`` into ``(kind, lexeme)`` tokens. Raises :class:`LogicError` + on any character that is not part of the propositional grammar.""" + tokens: list[tuple[str, str]] = [] + pos = 0 + n = len(text) + while pos < n: + ch = text[pos] + if ch.isspace(): + pos += 1 + continue + # Symbolic operators (longest spelling first). + matched = False + for spelling, kind in _OPERATOR_SPELLINGS: + if text.startswith(spelling, pos): + tokens.append((kind, spelling)) + pos += len(spelling) + matched = True + break + if matched: + continue + # Identifiers / keywords. + if _is_ident_start(ch): + start = pos + pos += 1 + while pos < n and _is_ident_char(text[pos]): + pos += 1 + word = text[start:pos] + kind = _KEYWORDS.get(word.lower()) + if kind is not None: + tokens.append((kind, word)) + else: + tokens.append(("ATOM", word)) + continue + raise LogicError(f"unexpected character {ch!r} at position {pos}") + return tokens + + +# --------------------------------------------------------------------------- +# Parser (recursive descent — twin of math_symbolic_normalizer._Parser) +# +# Precedence, lowest to highest: IFF < IMPLIES < OR < AND < NOT < atom/paren. +# IMPLIES is right-associative; the rest left-associative (associativity is +# semantically irrelevant under ROBDD but a fixed parse keeps errors crisp). +# +# The AST is a nested tuple, e.g. ('and', ('atom','P'), ('not',('atom','Q'))). +# --------------------------------------------------------------------------- + +_Ast = tuple + + +class _Parser: + def __init__(self, tokens: list[tuple[str, str]]) -> None: + self._tokens = tokens + self._pos = 0 + + def _peek(self) -> tuple[str, str] | None: + return None if self._pos >= len(self._tokens) else self._tokens[self._pos] + + def _consume(self) -> tuple[str, str]: + if self._pos >= len(self._tokens): + raise LogicError("unexpected end of formula") + tok = self._tokens[self._pos] + self._pos += 1 + return tok + + def parse(self) -> _Ast: + if not self._tokens: + raise LogicError("empty formula") + ast = self._iff() + if self._pos != len(self._tokens): + raise LogicError(f"unexpected trailing token {self._tokens[self._pos]!r}") + return ast + + def _iff(self) -> _Ast: + node = self._implies() + while (tok := self._peek()) is not None and tok[0] == "IFF": + self._consume() + node = ("iff", node, self._implies()) + return node + + def _implies(self) -> _Ast: + node = self._or() + if (tok := self._peek()) is not None and tok[0] == "IMPLIES": + self._consume() + # right-associative: recurse into _implies for the RHS + node = ("implies", node, self._implies()) + return node + + def _or(self) -> _Ast: + node = self._and() + while (tok := self._peek()) is not None and tok[0] == "OR": + self._consume() + node = ("or", node, self._and()) + return node + + def _and(self) -> _Ast: + node = self._not() + while (tok := self._peek()) is not None and tok[0] == "AND": + self._consume() + node = ("and", node, self._not()) + return node + + def _not(self) -> _Ast: + tok = self._peek() + if tok is not None and tok[0] == "NOT": + self._consume() + return ("not", self._not()) + return self._atom() + + def _atom(self) -> _Ast: + tok = self._consume() + kind, lexeme = tok + if kind == "ATOM": + return ("atom", lexeme) + if kind == "TRUE": + return ("const", True) + if kind == "FALSE": + return ("const", False) + if kind == "LPAREN": + inner = self._iff() + close = self._consume() + if close[0] != "RPAREN": + raise LogicError(f"expected ')'; got {close[1]!r}") + return inner + raise LogicError(f"unexpected token {lexeme!r}") + + +def _collect_atoms(ast: _Ast) -> set[str]: + kind = ast[0] + if kind == "atom": + return {ast[1]} + if kind == "const": + return set() + if kind == "not": + return _collect_atoms(ast[1]) + # binary + return _collect_atoms(ast[1]) | _collect_atoms(ast[2]) + + +# --------------------------------------------------------------------------- +# ROBDD manager (hand-rolled, minimal: mk + apply + negate + unique table) +# --------------------------------------------------------------------------- + + +class _Bdd: + """A single-formula ROBDD builder. Variables are addressed by index into a + fixed (sorted) ordering; ``var_count`` is the terminal sentinel level.""" + + __slots__ = ("var_count", "max_nodes", "_nodes", "_unique", "_and_c", "_or_c", "_neg_c") + + def __init__(self, var_count: int, max_nodes: int) -> None: + self.var_count = var_count + self.max_nodes = max_nodes + # node id -> (var_index, low_id, high_id); ids 0/1 are terminals (absent here). + self._nodes: list[tuple[int, int, int]] = [] + self._unique: dict[tuple[int, int, int], int] = {} + self._and_c: dict[tuple[int, int], int] = {} + self._or_c: dict[tuple[int, int], int] = {} + self._neg_c: dict[int, int] = {} + + def _var(self, node: int) -> int: + # Terminals sit "below" every variable: use var_count as +inf sentinel. + if node <= _TRUE: + return self.var_count + return self._nodes[node - 2][0] + + def _low(self, node: int) -> int: + return self._nodes[node - 2][1] + + def _high(self, node: int) -> int: + return self._nodes[node - 2][2] + + def mk(self, var: int, low: int, high: int) -> int: + """Make-or-reuse a node, applying the two reduction rules. This is the + only node-creation site, so the budget is enforced here.""" + if low == high: + return low # redundant-node rule + key = (var, low, high) + existing = self._unique.get(key) + if existing is not None: + return existing # shared-subgraph rule (hash-cons) + if len(self._nodes) >= self.max_nodes: + raise LogicBudgetError( + f"ROBDD exceeded node budget ({self.max_nodes}); refusing rather " + f"than churn" + ) + node_id = len(self._nodes) + 2 + self._nodes.append(key) + self._unique[key] = node_id + return node_id + + def var_node(self, var: int) -> int: + """The diagram for a bare variable: if var then true else false.""" + return self.mk(var, _FALSE, _TRUE) + + def negate(self, f: int) -> int: + if f == _FALSE: + return _TRUE + if f == _TRUE: + return _FALSE + cached = self._neg_c.get(f) + if cached is not None: + return cached + result = self.mk(self._var(f), self.negate(self._low(f)), self.negate(self._high(f))) + self._neg_c[f] = result + return result + + def conj(self, f: int, g: int) -> int: + if f == _FALSE or g == _FALSE: + return _FALSE + if f == _TRUE: + return g + if g == _TRUE: + return f + if f == g: + return f + key = (f, g) if f <= g else (g, f) # commutative -> canonical cache key + cached = self._and_c.get(key) + if cached is not None: + return cached + result = self._apply(self.conj, f, g) + self._and_c[key] = result + return result + + def disj(self, f: int, g: int) -> int: + if f == _TRUE or g == _TRUE: + return _TRUE + if f == _FALSE: + return g + if g == _FALSE: + return f + if f == g: + return f + key = (f, g) if f <= g else (g, f) + cached = self._or_c.get(key) + if cached is not None: + return cached + result = self._apply(self.disj, f, g) + self._or_c[key] = result + return result + + def _apply(self, op, f: int, g: int) -> int: + """Shannon expansion on the top variable of ``f``/``g`` (Bryant apply).""" + v = min(self._var(f), self._var(g)) + f0, f1 = self._cofactor(f, v) + g0, g1 = self._cofactor(g, v) + return self.mk(v, op(f0, g0), op(f1, g1)) + + def _cofactor(self, f: int, v: int) -> tuple[int, int]: + if self._var(f) == v: + return self._low(f), self._high(f) + return f, f # v does not occur at the top of f + + def compile(self, ast: _Ast, index_of: dict[str, int]) -> int: + kind = ast[0] + if kind == "atom": + return self.var_node(index_of[ast[1]]) + if kind == "const": + return _TRUE if ast[1] else _FALSE + if kind == "not": + return self.negate(self.compile(ast[1], index_of)) + left = self.compile(ast[1], index_of) + right = self.compile(ast[2], index_of) + if kind == "and": + return self.conj(left, right) + if kind == "or": + return self.disj(left, right) + if kind == "implies": + return self.disj(self.negate(left), right) + if kind == "iff": + # (a -> b) ∧ (b -> a) + return self.conj(self.disj(self.negate(left), right), + self.disj(self.negate(right), left)) + raise LogicError(f"unknown AST node {kind!r}") # pragma: no cover + + def serialize(self, root: int, names: tuple[str, ...]) -> str: + """Canonical, construction-order-independent serialization of the reduced + diagram reachable from ``root``. Post-order DFS (low subtree fully before + high subtree) assigns canonical indices; nodes reference variable *names* + so diagrams over different atoms never collide, while terminals collapse + (every tautology -> 'T', every contradiction -> 'F'). Because the diagram + is reduced and the ordering fixed, isomorphic diagrams emit identical + strings.""" + if root == _TRUE: + return "T" + if root == _FALSE: + return "F" + order: dict[int, int] = {} + lines: list[str] = [] + + def ref(node: int) -> str: + if node == _TRUE: + return "T" + if node == _FALSE: + return "F" + return f"@{order[node]}" + + def visit(node: int) -> None: + if node in order or node <= _TRUE: + return + visit(self._low(node)) + visit(self._high(node)) + idx = len(order) + order[node] = idx + lines.append( + f"{idx}:{names[self._var(node)]}?{ref(self._high(node))}:{ref(self._low(node))}" + ) + + visit(root) + return ";".join(lines) + + def support(self, root: int) -> set[int]: + """The set of variable indices that occur in the reduced diagram — + i.e. the atoms that survive reduction (irrelevant ones are absent).""" + seen: set[int] = set() + out: set[int] = set() + + def visit(node: int) -> None: + if node <= _TRUE or node in seen: + return + seen.add(node) + out.add(self._var(node)) + visit(self._low(node)) + visit(self._high(node)) + + visit(root) + return out + + +# --------------------------------------------------------------------------- +# Public API (twin of math_symbolic_equivalence) +# --------------------------------------------------------------------------- + + +@dataclass(frozen=True, slots=True) +class CanonicalProposition: + """The canonical form of a propositional formula. + + ``canonical_key`` is the byte-equality discriminator — two formulas are + logically equivalent iff their keys are equal. ``atoms`` are the variables + that *survive* reduction (logically-irrelevant ones are dropped), so it can be + a strict subset of the atoms written in the input.""" + + canonical_key: str + atoms: tuple[str, ...] + is_tautology: bool + is_contradiction: bool + + +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() + 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) + root = bdd.compile(ast, index_of) + key = bdd.serialize(root, declared) + # Atoms that actually occur in the reduced diagram (irrelevant ones dropped). + support_idx = bdd.support(root) + surviving = tuple(name for i, name in enumerate(declared) if i in support_idx) + return CanonicalProposition( + canonical_key=key, + atoms=surviving, + is_tautology=(root == _TRUE), + is_contradiction=(root == _FALSE), + ) diff --git a/generate/logic_equivalence.py b/generate/logic_equivalence.py new file mode 100644 index 00000000..55d2da75 --- /dev/null +++ b/generate/logic_equivalence.py @@ -0,0 +1,88 @@ +"""ADR-0201 — Propositional equivalence check. + +Boolean-logic twin of :mod:`generate.math_symbolic_equivalence`. Given two +propositional formulas A and B, produces an :class:`EquivalenceVerdict` of +EQUIVALENT, NOT_EQUIVALENT, or REFUSED, by canonicalizing each to its ROBDD +identity (:mod:`generate.logic_canonical`) and comparing the canonical keys by +byte-equality. + +REFUSED preserves ``wrong == 0``: out-of-grammar input or a diagram that exceeds +the node budget refuses rather than emitting a verdict — the same posture as the +algebra sibling refusing on out-of-scope expressions. +""" + +from __future__ import annotations + +from dataclasses import dataclass +from enum import Enum +from typing import Final + +from generate.logic_canonical import ( + DEFAULT_MAX_NODES, + LogicBudgetError, + LogicError, + canonicalize, +) + + +class Verdict(str, Enum): + EQUIVALENT = "equivalent" + NOT_EQUIVALENT = "not_equivalent" + REFUSED = "refused" + + +@dataclass(frozen=True, slots=True) +class EquivalenceVerdict: + verdict: Verdict + canonical_a: str | None + canonical_b: str | None + reason: str + + +REFUSED_VERDICTS: Final[frozenset[Verdict]] = frozenset({Verdict.REFUSED}) +"""Helper set for callers that need to gate on refusal vs decision.""" + + +def check_equivalence( + formula_a: str, + formula_b: str, + *, + max_nodes: int = DEFAULT_MAX_NODES, +) -> EquivalenceVerdict: + """Return whether two propositional formulas are logically equivalent. + + Equivalence is decided by ROBDD canonical-key byte-equality, which is exact + for propositional logic. Refuses (rather than guesses) on malformed input or + on diagram blowup beyond ``max_nodes``. + """ + try: + canon_a = canonicalize(formula_a, max_nodes=max_nodes).canonical_key + canon_b = canonicalize(formula_b, max_nodes=max_nodes).canonical_key + except LogicBudgetError as exc: + return EquivalenceVerdict( + verdict=Verdict.REFUSED, + canonical_a=None, + canonical_b=None, + reason=f"canonicalization_budget_exceeded: {exc}", + ) + except LogicError as exc: + return EquivalenceVerdict( + verdict=Verdict.REFUSED, + canonical_a=None, + canonical_b=None, + reason=f"canonicalize refused: {exc}", + ) + + if canon_a == canon_b: + return EquivalenceVerdict( + verdict=Verdict.EQUIVALENT, + canonical_a=canon_a, + canonical_b=canon_b, + reason="", + ) + return EquivalenceVerdict( + verdict=Verdict.NOT_EQUIVALENT, + canonical_a=canon_a, + canonical_b=canon_b, + reason="", + ) diff --git a/tests/test_logic_canonical.py b/tests/test_logic_canonical.py new file mode 100644 index 00000000..1674fe5c --- /dev/null +++ b/tests/test_logic_canonical.py @@ -0,0 +1,167 @@ +"""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, + LogicBudgetError, + LogicError, + 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