core-labs/core
core-labs/core
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

feat: propositional canonicalizer keystone + representation contract (ADR-0201/0202)

Browse source 
The proof_chain keystone: a hand-rolled ROBDD canonicalizer mirroring
math_symbolic_equivalence one domain over (normalize -> canonical key ->
byte-equality -> three-valued verdict; REFUSED preserves wrong=0).

- generate/logic_canonical.py: formula -> ROBDD identity under sorted-atom
  ordering; LogicError/LogicBudgetError refusals; inspectable canonical key.
- generate/logic_equivalence.py: EQUIVALENT/NOT_EQUIVALENT/REFUSED wrapper.
- tests/test_logic_canonical.py: 33 standalone tests (canonicity laws,
  discrimination, terminals, determinism, refusals); mutation-verified non-vacuous.
- ADR-0201: canonicalizer decision (ROBDD not CNF/DNF; hand-rolled;
  propositional-only honesty boundary).
- ADR-0202: proposition representation contract — single source the canonicalizer
  and the proof corpus conform to (formula grammar + atom layer binding to ADR-0144
  EpistemicNode + honesty boundary).

Additive: no existing file touched, zero consumers. Standalone keystone only;
binding-graph wiring, acyclicity refusal, and inference rules deferred. smoke: 67 passed.
This commit is contained in:
Shay 2026-06-02 16:24:32 -07:00
parent 1417ffad12
commit e8e0fbb014
5 changed files with 1075 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

126
docs/decisions/ADR-0201-proposition-canonicalizer.md Normal file
View file

@ -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.

213
docs/decisions/ADR-0202-proposition-representation-contract.md Normal file
View file

@ -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: `<Letter>[_<slug>]`, 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.

481
generate/logic_canonical.py Normal file
View file

@ -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),
)

88
generate/logic_equivalence.py Normal file
View file

@ -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="",
)

167
tests/test_logic_canonical.py Normal file
View file

@ -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