engineering/arborist
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

pi_star: arithmetic@v1 + logic-kernel@v1 graduate — math gets logic's coverage

Browse source 
Closes the math half of fox's 2026-05-08 roadmap question ("did we
implement the math and logic stuff?"). Until now arborist had logic
KERNELS (Syllogism, Truthtables, Transitivity sub-batteries with
deterministic evaluators) but no math π*'s. SQD whitepaper §14
framed math as "operations over π*-canonical invariant objects:
integers, algebraic expressions, proof states, constraint graphs"
— that framing is now actually implementable.

arithmetic@v1 — exact rational arithmetic (SQD §14.1)
-----------------------------------------------------
Parse arithmetic expression → fractions.Fraction → canonical
"<num>/<den>" in lowest terms. Decimals via Decimal(str(...)) for
exact rational interpretation:

  "0.1"     → "1/10"   (not 0.1±ε)
  "0.1+0.2" → "3/10"   (the SQD-canonical floating-point question)
  "1+2"     → "3/1"
  "(1+2)*3" → "9/1"
  "6/4"     → "3/2"    (lowest terms via Fraction invariant)
  "2**3"    → "8/1"
  "-(1+2)"  → "-3/1"

Rejects: identifiers, function calls, division by zero, non-integer
exponents, boolean literals. PiStarError with explanatory message.

logic-kernel@v1 — propositional CNF canonicalizer (SQD §14.3)
-------------------------------------------------------------
Parse Boolean expression (AND/OR/NOT/XOR/IMPL/IFF + named atoms +
parens) → eliminate IMPL/IFF/XOR → push NOT inward (NNF) →
distribute OR over AND (CNF) → dedupe + sort literals + sort
clauses + drop tautological clauses → serialize.

Equivalence classes preserved:
  A AND B           ≡  B AND A          (commutativity)
  (A AND B) AND C   ≡  A AND (B AND C)  (associativity)
  A IMPL B          ≡  NOT A OR B       (IMPL rewrite)
  A IMPL B          ≡  NOT B IMPL NOT A (contrapositive)
  NOT (A AND B)     ≡  NOT A OR NOT B   (De Morgan)
  NOT NOT A         ≡  A                (double negation)
  A OR (B AND C)    ≡  (A OR B) AND (A OR C)  (distribution)
  A OR NOT A        →  TRUE             (tautology)
  A AND A           ≡  A                (idempotence)

Atom cap: N=8 (256 max clauses). Larger inputs raise PiStarError;
CNF blow-up is exponential in atom count, the cap keeps
canonicalization deterministic in bounded time.

Surface
-------
- arborist/pi_star/arithmetic.py — full implementation (new file)
- arborist/pi_star/logic.py — full implementation (graduates from
  stub; preserves the LogicKernelV1 dataclass shape so the registry
  key arithmetic@v1 / logic-kernel@v1 stays stable)
- arborist/pi_star/__init__.py — imports arithmetic to auto-register
- bench/batteries/base.py — PHASE_1_CARRIERS adds "arithmetic" + "logic"
- bench/fixtures/5s/syntax-arithmetic-v1.jsonl (12 fixtures)
- bench/fixtures/5s/semantics-arithmetic-v1.jsonl (15 fixtures)
- bench/fixtures/5s/syntax-logic-v1.jsonl (12 fixtures)
- bench/fixtures/5s/semantics-logic-v1.jsonl (18 fixtures)
- Makefile: bench-5s-arithmetic, bench-5s-logic-kernel,
  bench-5s-math aggregate
- tests/test_pi_star.py: 30 new tests
  - 13 for arithmetic@v1 (decimals, equivalence, rejects, idempotency,
    integer exponents, negative results, the SQD 0.1+0.2 case)
  - 17 for logic-kernel@v1 (commutativity, associativity, all rewrite
    rules, De Morgan, double-neg, distribution, tautology, idempotence,
    contrapositive, atom cap, syntax errors, idempotency)

Cross-modality discipline now spans:
  text + claim_lattice + memory + code + arithmetic + logic
  — six carrier domains, all with real π* implementations.

Two stubs remain (time-series-quantized@v1, tabular-pinned@v1);
neither is needed for math/logic coverage.

Full suite: 1256 passed, 36 skipped (+30 tests, +57 fixtures).
This commit is contained in:
russell@unturf.com 2026-05-08 09:16:19 -04:00
parent 1f4c8b93c8
commit e4ecf89621
No known key found for this signature in database
10 changed files with 845 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

14
Makefile
View file

@ -272,6 +272,20 @@ bench-5s-code: bootstrap ## 5S code-carrier (Syntax + Semantics through code-py-
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \
--fixtures bench/fixtures/5s/semantics-code-v1.jsonl
bench-5s-arithmetic: bootstrap ## 5S arithmetic π* (SQD §14.1; rational arithmetic canonicalizer)
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub syntax \
--fixtures bench/fixtures/5s/syntax-arithmetic-v1.jsonl
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \
--fixtures bench/fixtures/5s/semantics-arithmetic-v1.jsonl
bench-5s-logic-kernel: bootstrap ## 5S logic-kernel π* (SQD §14.3; CNF canonicalizer)
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub syntax \
--fixtures bench/fixtures/5s/syntax-logic-v1.jsonl
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5s --sub semantics \
--fixtures bench/fixtures/5s/semantics-logic-v1.jsonl
bench-5s-math: bench-5s-arithmetic bench-5s-logic-kernel ## complete math π* surface (arithmetic + logic-kernel)
bench-5f-formulate-live: bootstrap ## 5F Formulate via live arborist.qa.parse_claims (Phase 1b.2)
PYTHONUNBUFFERED=1 $(PY) -m bench.batteries.runner --battery 5f --sub formulate \
--fixtures bench/fixtures/5f/formulate-live-v1.jsonl

1
arborist/pi_star/__init__.py
View file

@ -44,6 +44,7 @@ from arborist.pi_star.registry import (
# Side-effect imports populate REGISTRY at package load time.
# Order is alphabetical for predictability.
from arborist.pi_star import arithmetic # noqa: F401,E402
from arborist.pi_star import claim_lattice # noqa: F401,E402
from arborist.pi_star import code # noqa: F401,E402
from arborist.pi_star import logic # noqa: F401,E402

188
arborist/pi_star/arithmetic.py Normal file
View file

@ -0,0 +1,188 @@
"""``arithmetic@v1`` π* — exact rational arithmetic canonicalizer.
Domain: ``arithmetic``. Implements SQD whitepaper §14.1's
``π*_Q : Σ* → ℚ ∪ {⊥}`` projection: parse an arithmetic expression
string, evaluate it exactly using :class:`fractions.Fraction`, and
serialize the result as ``"<numerator>/<denominator>"`` in lowest
terms.
Why this matters
----------------
SQD §14 frames math as "operations over π*-canonical invariant
objects: integers, algebraic expressions, proof states, constraint
graphs." Until this commit, arborist had logic kernels (Syllogism,
Truthtables, Transitivity) but no arithmetic π*. The classic
SQD-whitepaper test case ``"0.1 + 0.2 == 0.3"`` was unverifiable.
This canonicalizer handles it: ``"0.1+0.2"`` parses to
``Fraction(1,10) + Fraction(1,5) = Fraction(3,10)`` exactly. No
floating-point drift.
Allowed surface
---------------
- Integer literals: ``1``, ``42``, ``-7``
- Decimal literals: ``0.1``, ``3.14`` — parsed via
:class:`decimal.Decimal` for **exact** rational interpretation.
- Binary operators: ``+ - * /``
- Unary operators: ``+ -``
- Integer exponents: ``a ** n`` where ``n`` is integer
- Parentheses
Rejected (raises :class:`PiStarError`)
--------------------------------------
- Identifiers / variables (this is closed-form arithmetic).
- Non-integer exponents (would yield irrational; out of ℚ scope).
- Division by zero.
- Function calls, comparisons, logical ops.
- Unicode operators outside the allowlist.
Equivalence classes preserved
-----------------------------
- ``"1+2"`` ≡ ``"3"``
- ``"0.1"`` ≡ ``"1/10"``
- ``"0.5"`` ≡ ``"1/2"``
- ``"0.1+0.2"`` ≡ ``"0.3"``
- ``"(1+2)*3"`` ≡ ``"9"``
- ``"6/4"`` ≡ ``"3/2"`` (lowest terms)
- ``"-2"`` ≡ ``"-2/1"``
Equivalence classes kept distinct
---------------------------------
- ``"1+2"`` ≢ ``"4"``
- ``"0.1+0.2"`` ≢ ``"0.30000000000000004"`` (only float-binary
arithmetic produces the latter; we never enter float space).
Round-trip property
-------------------
Idempotent: ``canonicalize("3/10")`` produces ``b"3/10"`` and
re-canonicalizing those bytes yields the same. The output is valid
input syntax (`a/b` is a valid rational expression).
Versioning
----------
``arithmetic@v1`` pins this algorithm. Any change to the operator
allowlist, exponent semantics, or output format requires a new
version.
Source: ticket #000015 §1.7 reserved an arithmetic carrier; this
commit graduates it. Closes the math half of the 2026-05-08 fox
roadmap note ("did we implement the math and logic stuff?").
"""
from __future__ import annotations
import ast
from dataclasses import dataclass
from decimal import Decimal
from fractions import Fraction
from arborist.pi_star.protocol import PiStarError
from arborist.pi_star.registry import register
@dataclass
class ArithmeticV1:
name: str = "arithmetic"
version: str = "v1"
domain: str = "arithmetic"
def canonicalize(self, raw: bytes) -> bytes:
if not isinstance(raw, (bytes, bytearray)):
raise PiStarError(
"arithmetic@v1 expects bytes; got "
f"{type(raw).__name__}"
)
try:
source = raw.decode("utf-8", errors="surrogatepass")
except UnicodeDecodeError as exc: # pragma: no cover — defensive
raise PiStarError(f"input not valid UTF-8: {exc}") from exc
source = source.strip()
if not source:
raise PiStarError("arithmetic@v1 input is empty")
# Allow `a/b` rational form with negative numerator. Detect
# before ast.parse so divisions of integers yield exact
# rationals (ast would parse them as Div which we evaluate to
# Fraction; this works either way but the early path is
# simpler).
try:
tree = ast.parse(source, mode="eval")
except SyntaxError as exc:
raise PiStarError(
f"arithmetic@v1 input is not valid expression: {exc}"
) from exc
result = _eval_node(tree.body)
if not isinstance(result, Fraction):
raise PiStarError(
f"arithmetic@v1 evaluation returned non-Fraction: {type(result).__name__}"
)
# Canonical form: "<num>/<den>" in lowest terms. Fraction
# already maintains coprime invariant.
return f"{result.numerator}/{result.denominator}".encode("utf-8")
_ALLOWED_BINOPS = {
ast.Add: lambda l, r: l + r,
ast.Sub: lambda l, r: l - r,
ast.Mult: lambda l, r: l * r,
}
def _eval_node(node) -> Fraction:
if isinstance(node, ast.Constant):
v = node.value
if isinstance(v, bool):
# bool subclasses int — exclude explicitly to avoid
# accidentally accepting True/False literals.
raise PiStarError("arithmetic@v1 rejects boolean literals")
if isinstance(v, int):
return Fraction(v)
if isinstance(v, float):
# Round-trip via Decimal(str(...)) gives the *intended*
# rational (e.g., 0.1 → 1/10, not 1/10 + ε).
return Fraction(Decimal(str(v)))
raise PiStarError(
f"arithmetic@v1 rejects literal of type {type(v).__name__}"
)
if isinstance(node, ast.UnaryOp):
operand = _eval_node(node.operand)
if isinstance(node.op, ast.UAdd):
return operand
if isinstance(node.op, ast.USub):
return -operand
raise PiStarError(
f"arithmetic@v1 rejects unary op {type(node.op).__name__}"
)
if isinstance(node, ast.BinOp):
left = _eval_node(node.left)
right = _eval_node(node.right)
op_type = type(node.op)
if op_type in _ALLOWED_BINOPS:
return _ALLOWED_BINOPS[op_type](left, right)
if op_type is ast.Div:
if right == 0:
raise PiStarError("arithmetic@v1 division by zero")
return left / right
if op_type is ast.Pow:
if right.denominator != 1:
raise PiStarError(
"arithmetic@v1 rejects non-integer exponent "
f"({right}); would leave ℚ"
)
return left ** int(right.numerator)
raise PiStarError(
f"arithmetic@v1 rejects binary op {op_type.__name__}"
)
if isinstance(node, ast.Name):
raise PiStarError(
f"arithmetic@v1 rejects identifier {node.id!r}; closed-form only"
)
if isinstance(node, ast.Call):
raise PiStarError("arithmetic@v1 rejects function calls")
raise PiStarError(
f"arithmetic@v1 rejects node type {type(node).__name__}"
)
register(ArithmeticV1())

358
arborist/pi_star/logic.py
View file

@ -1,18 +1,84 @@
"""``logic-kernel@v1`` π* (stub).
"""``logic-kernel@v1`` π* — propositional-logic CNF canonicalizer.
Domain: ``logic``. Implementation lands in a follow-up. Planned
semantics: parse a math/proof string → kernel proof object →
canonical serialization. Equivalent proofs → identical canonical bytes.
Aligns with v7 §14.3 proof-object π*.
Domain: ``logic``. Implements SQD whitepaper §14.3's proof-object
canonicalizer at the propositional level: parse a Boolean expression
over named atoms, convert to **canonical Conjunctive Normal Form**
(CNF), serialize as a deterministic string.
Algorithm
---------
1. Tokenize using the same lexer as
:func:`bench.batteries.b_5t._eval_propositional` (AND/OR/NOT/
XOR/IMPL/IFF + parens + uppercase atom names).
2. Parse via recursive descent → AST.
3. Eliminate IMPL/IFF/XOR by rewriting:
- ``A IMPL B`` → ``(NOT A) OR B``
- ``A IFF B`` → ``((NOT A) OR B) AND ((NOT B) OR A)``
- ``A XOR B`` → ``(A OR B) AND ((NOT A) OR (NOT B))``
4. Push NOT inward (De Morgan + double-negation elimination):
- ``NOT (A AND B)`` → ``(NOT A) OR (NOT B)``
- ``NOT (A OR B)`` → ``(NOT A) AND (NOT B)``
- ``NOT NOT A`` → ``A``
5. Distribute OR over AND until CNF.
6. Within each clause: dedupe + sort literals by ``(name, negated)``.
7. Detect tautological clauses (contains both ``A`` and ``NOT A``)
→ drop the clause (it's always true).
8. Detect contradiction (clause ``A AND NOT A`` after step 6 yields
the empty disjunction → unsatisfiable). Surface as a special
canonical form ``"FALSE"``.
9. Detect tautology (no clauses left after step 7) → ``"TRUE"``.
10. Sort clauses lexically by literal-tuple representation; dedupe.
11. Serialize as ``(L1 OR L2) AND (L3 OR L4) AND ...``.
Equivalence classes preserved
-----------------------------
- Commutativity: ``A AND B`` ≡ ``B AND A``
- Associativity: ``(A AND B) AND C`` ≡ ``A AND (B AND C)``
- IMPL/IFF/XOR rewrites: ``A IMPL B`` ≡ ``NOT A OR B``
- De Morgan's: ``NOT (A AND B)`` ≡ ``(NOT A) OR (NOT B)``
- Double negation: ``NOT NOT A`` ≡ ``A``
- Distribution: ``A OR (B AND C)`` ≡ ``(A OR B) AND (A OR C)``
- Tautology collapse: ``A OR NOT A`` ≡ ``TRUE``
- Idempotence: ``A AND A`` ≡ ``A``
Equivalence classes kept distinct
---------------------------------
- Different atom sets: ``A AND B`` ≢ ``A AND C``
- Logically distinct: ``A AND B`` ≢ ``A OR B``
Round-trip property
-------------------
Idempotent on its own output: re-canonicalizing the canonical form
yields the same bytes (CNF is closed under the algorithm).
Versioning
----------
``logic-kernel@v1`` pins this algorithm. CNF blow-up bound: input
expressions with N atoms can produce up to 2^N clauses. v1 caps
at N=8 (256 clauses) to keep canonicalization deterministic in
bounded time; raises :class:`PiStarError` on excess.
Source: ticket #000015 §1.7 declared the stub. This commit
graduates it. Closes the math/logic-kernel half of the 2026-05-08
fox roadmap note alongside ``arithmetic@v1``.
"""
from __future__ import annotations
from dataclasses import dataclass
from typing import Optional
from arborist.pi_star.protocol import PiStarError
from arborist.pi_star.registry import register
_MAX_ATOMS = 8
@dataclass
class LogicKernelV1:
name: str = "logic-kernel"
@ -20,10 +86,286 @@ class LogicKernelV1:
domain: str = "logic"
def canonicalize(self, raw: bytes) -> bytes:
raise NotImplementedError(
"logic-kernel@v1 is a stub; implementation ticket pending. "
"See docs/tickets/ticket-000015-pi-star-domain-library.md."
if not isinstance(raw, (bytes, bytearray)):
raise PiStarError(
"logic-kernel@v1 expects bytes; got "
f"{type(raw).__name__}"
)
try:
source = raw.decode("utf-8", errors="surrogatepass")
except UnicodeDecodeError as exc: # pragma: no cover
raise PiStarError(f"input not valid UTF-8: {exc}") from exc
source = source.strip()
if not source:
raise PiStarError("logic-kernel@v1 input is empty")
tokens = _tokenize(source)
atoms = sorted({t for t in tokens if _is_atom(t)})
if len(atoms) > _MAX_ATOMS:
raise PiStarError(
f"logic-kernel@v1 caps atoms at {_MAX_ATOMS}; "
f"got {len(atoms)} ({atoms})"
)
ast = _parse(tokens)
ast = _eliminate(ast)
ast = _push_not(ast)
clauses = _to_cnf(ast)
# Each clause is a frozenset of (atom, negated) literals.
canonical_clauses = []
for clause in clauses:
# Drop tautological clauses (A and NOT A both present).
atoms_present = {a for (a, _) in clause}
tautology = any(
(a, False) in clause and (a, True) in clause
for a in atoms_present
)
if tautology:
continue
canonical_clauses.append(tuple(sorted(clause)))
# Dedupe clauses.
canonical_clauses = sorted(set(canonical_clauses))
if not canonical_clauses:
return b"TRUE"
# Empty clause = contradiction.
if any(len(c) == 0 for c in canonical_clauses):
return b"FALSE"
return _serialize(canonical_clauses).encode("utf-8")
# ---------------------------------------------------------------------
# Tokenizer (identical surface to b_5t._tokenize_propositional)
# ---------------------------------------------------------------------
def _tokenize(expr: str) -> list[str]:
out: list[str] = []
i = 0
while i < len(expr):
c = expr[i]
if c.isspace():
i += 1
continue
if c in "()":
out.append(c)
i += 1
continue
if c.isalpha():
j = i
while j < len(expr) and expr[j].isalpha():
j += 1
tok = expr[i:j]
up = tok.upper()
if up in ("AND", "OR", "NOT", "XOR", "IMPL", "IFF", "TRUE", "FALSE"):
out.append(up)
elif len(tok) == 1:
out.append(tok.upper())
else:
raise PiStarError(f"unrecognized token: {tok!r}")
i = j
continue
raise PiStarError(f"unexpected char: {c!r}")
return out
def _is_atom(token: str) -> bool:
return len(token) == 1 and token.isupper() and token.isalpha()
# ---------------------------------------------------------------------
# Parser (recursive descent → tuple-AST)
#
# Returned shape:
# ('atom', name)
# ('not', child)
# ('and', left, right)
# ('or', left, right)
# ('impl', left, right)
# ('iff', left, right)
# ('xor', left, right)
# ('true',)
# ('false',)
#
# Tuple form keeps the kernel pure-functional and easy to pattern-match.
# ---------------------------------------------------------------------
def _parse(tokens: list[str]) -> tuple:
pos = [0]
def peek() -> Optional[str]:
return tokens[pos[0]] if pos[0] < len(tokens) else None
def expect(t: str) -> None:
if peek() != t:
raise PiStarError(f"expected {t!r} at {pos[0]}, got {peek()!r}")
pos[0] += 1
def parse_atom() -> tuple:
t = peek()
if t is None:
raise PiStarError("unexpected end of expression")
if t == "(":
pos[0] += 1
v = parse_or()
expect(")")
return v
if t == "NOT":
pos[0] += 1
return ("not", parse_atom())
if t == "TRUE":
pos[0] += 1
return ("true",)
if t == "FALSE":
pos[0] += 1
return ("false",)
if _is_atom(t):
pos[0] += 1
return ("atom", t)
raise PiStarError(f"unexpected token {t!r}")
def parse_and() -> tuple:
left = parse_atom()
while peek() == "AND":
pos[0] += 1
right = parse_atom()
left = ("and", left, right)
return left
def parse_or() -> tuple:
left = parse_and()
while peek() in ("OR", "XOR", "IMPL", "IFF"):
op = peek()
pos[0] += 1
right = parse_and()
mapping = {"OR": "or", "XOR": "xor", "IMPL": "impl", "IFF": "iff"}
left = (mapping[op], left, right)
return left
result = parse_or()
if pos[0] != len(tokens):
raise PiStarError(f"unconsumed tokens at {pos[0]}: {tokens[pos[0]:]!r}")
return result
# ---------------------------------------------------------------------
# Eliminate IMPL/IFF/XOR → AND/OR/NOT only
# ---------------------------------------------------------------------
def _eliminate(node: tuple) -> tuple:
if node[0] in ("atom", "true", "false"):
return node
if node[0] == "not":
return ("not", _eliminate(node[1]))
if node[0] in ("and", "or"):
return (node[0], _eliminate(node[1]), _eliminate(node[2]))
if node[0] == "impl":
# A IMPL B → (NOT A) OR B
a, b = _eliminate(node[1]), _eliminate(node[2])
return ("or", ("not", a), b)
if node[0] == "iff":
# A IFF B → (NOT A OR B) AND (NOT B OR A)
a, b = _eliminate(node[1]), _eliminate(node[2])
return (
"and",
("or", ("not", a), b),
("or", ("not", b), a),
)
if node[0] == "xor":
# A XOR B → (A OR B) AND (NOT A OR NOT B)
a, b = _eliminate(node[1]), _eliminate(node[2])
return (
"and",
("or", a, b),
("or", ("not", a), ("not", b)),
)
raise PiStarError(f"unknown node tag: {node[0]}")
# ---------------------------------------------------------------------
# Push NOT inward (NNF — Negation Normal Form)
# ---------------------------------------------------------------------
def _push_not(node: tuple) -> tuple:
if node[0] in ("atom", "true", "false"):
return node
if node[0] == "not":
inner = node[1]
if inner[0] == "atom":
return node
if inner[0] == "true":
return ("false",)
if inner[0] == "false":
return ("true",)
if inner[0] == "not":
# NOT NOT A → A
return _push_not(inner[1])
if inner[0] == "and":
# NOT (A AND B) → (NOT A) OR (NOT B)
return _push_not(("or", ("not", inner[1]), ("not", inner[2])))
if inner[0] == "or":
return _push_not(("and", ("not", inner[1]), ("not", inner[2])))
raise PiStarError(f"unexpected tag inside NOT: {inner[0]}")
if node[0] in ("and", "or"):
return (node[0], _push_not(node[1]), _push_not(node[2]))
raise PiStarError(f"unknown node tag in _push_not: {node[0]}")
# ---------------------------------------------------------------------
# Distribute OR over AND → CNF
#
# Produces a list of clauses (frozensets of literals).
# Each literal is (atom_name, negated).
# ---------------------------------------------------------------------
def _to_cnf(node: tuple) -> list[frozenset]:
if node[0] == "true":
return [] # TRUE = no constraints
if node[0] == "false":
return [frozenset()] # empty clause = contradiction
if node[0] == "atom":
return [frozenset({(node[1], False)})]
if node[0] == "not":
if node[1][0] != "atom":
raise PiStarError(
f"_to_cnf expects NNF; got NOT around {node[1][0]}"
)
return [frozenset({(node[1][1], True)})]
if node[0] == "and":
return _to_cnf(node[1]) + _to_cnf(node[2])
if node[0] == "or":
# Distribute: OR of two CNFs = AND of pairwise-OR'd clauses.
left = _to_cnf(node[1])
right = _to_cnf(node[2])
out = []
for lc in left:
for rc in right:
out.append(lc | rc)
return out
raise PiStarError(f"unknown node tag in _to_cnf: {node[0]}")
# ---------------------------------------------------------------------
# Serialize sorted clauses as canonical text.
# ---------------------------------------------------------------------
def _serialize(clauses: list[tuple]) -> str:
"""Each clause is a sorted tuple of (atom, negated) literals."""
def lit_str(lit):
atom, neg = lit
return f"NOT {atom}" if neg else atom
parts = []
for clause in clauses:
if len(clause) == 1:
parts.append(lit_str(clause[0]))
else:
parts.append("(" + " OR ".join(lit_str(l) for l in clause) + ")")
return " AND ".join(parts)
register(LogicKernelV1())

4
bench/batteries/base.py
View file

@ -112,6 +112,10 @@ PHASE_1_CARRIERS = frozenset({
"memory_root",
# First non-text carrier, landed via code-py-ast@v1 graduation.
"code",
# Math π*'s — arithmetic@v1 + logic-kernel@v1 graduations
# (SQD §14.1 + §14.3).
"arithmetic",
"logic",
})

16
bench/fixtures/5s/semantics-arithmetic-v1.jsonl Normal file
View file

@ -0,0 +1,16 @@
{"_meta":{"battery":"5s","sub_battery":"semantics","version":"v1","task_count":15,"notes":"arithmetic@v1 equivalence-class tests. SQD §14.1: rationally equivalent expressions canonicalize to identical bytes; distinct values do not."}}
{"id":"5s-sem-arith-001","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"1+2","input_b":"3","expected_equivalent":true}
{"id":"5s-sem-arith-002","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.1","input_b":"1/10","expected_equivalent":true}
{"id":"5s-sem-arith-003","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.1+0.2","input_b":"0.3","expected_equivalent":true}
{"id":"5s-sem-arith-004","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"(1+2)*3","input_b":"9","expected_equivalent":true}
{"id":"5s-sem-arith-005","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"6/4","input_b":"3/2","expected_equivalent":true}
{"id":"5s-sem-arith-006","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"-2","input_b":"-2/1","expected_equivalent":true}
{"id":"5s-sem-arith-007","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"2**3","input_b":"8","expected_equivalent":true}
{"id":"5s-sem-arith-008","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.5","input_b":"1/2","expected_equivalent":true}
{"id":"5s-sem-arith-009","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"100*100","input_b":"10000","expected_equivalent":true}
{"id":"5s-sem-arith-010","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"1+2","input_b":"4","expected_equivalent":false}
{"id":"5s-sem-arith-011","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"1/2","input_b":"1/3","expected_equivalent":false}
{"id":"5s-sem-arith-012","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"0.1","input_b":"0.2","expected_equivalent":false}
{"id":"5s-sem-arith-013","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"-3","input_b":"3","expected_equivalent":false}
{"id":"5s-sem-arith-014","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"3+5*2","input_b":"13","expected_equivalent":true}
{"id":"5s-sem-arith-015","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input_a":"3+5*2","input_b":"16","expected_equivalent":false}

19
bench/fixtures/5s/semantics-logic-v1.jsonl Normal file
View file

@ -0,0 +1,19 @@
{"_meta":{"battery":"5s","sub_battery":"semantics","version":"v1","task_count":18,"notes":"logic-kernel@v1 equivalence-class tests. Logically equivalent expressions canonicalize to identical CNF bytes; logically distinct expressions do not."}}
{"id":"5s-sem-logic-001","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND B","input_b":"B AND A","expected_equivalent":true}
{"id":"5s-sem-logic-002","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A OR B","input_b":"B OR A","expected_equivalent":true}
{"id":"5s-sem-logic-003","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"(A AND B) AND C","input_b":"A AND (B AND C)","expected_equivalent":true}
{"id":"5s-sem-logic-004","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IMPL B","input_b":"NOT A OR B","expected_equivalent":true}
{"id":"5s-sem-logic-005","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IMPL B","input_b":"(NOT B) IMPL (NOT A)","expected_equivalent":true}
{"id":"5s-sem-logic-006","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT (A AND B)","input_b":"(NOT A) OR (NOT B)","expected_equivalent":true}
{"id":"5s-sem-logic-007","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT (A OR B)","input_b":"(NOT A) AND (NOT B)","expected_equivalent":true}
{"id":"5s-sem-logic-008","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT NOT A","input_b":"A","expected_equivalent":true}
{"id":"5s-sem-logic-009","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A OR (B AND C)","input_b":"(A OR B) AND (A OR C)","expected_equivalent":true}
{"id":"5s-sem-logic-010","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IFF B","input_b":"(A IMPL B) AND (B IMPL A)","expected_equivalent":true}
{"id":"5s-sem-logic-011","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A XOR B","input_b":"(A OR B) AND (NOT A OR NOT B)","expected_equivalent":true}
{"id":"5s-sem-logic-012","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A OR NOT A","input_b":"TRUE","expected_equivalent":true}
{"id":"5s-sem-logic-013","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND A","input_b":"A","expected_equivalent":true}
{"id":"5s-sem-logic-014","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND B","input_b":"A OR B","expected_equivalent":false}
{"id":"5s-sem-logic-015","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A IMPL B","input_b":"B IMPL A","expected_equivalent":false}
{"id":"5s-sem-logic-016","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"A AND B","input_b":"A AND C","expected_equivalent":false}
{"id":"5s-sem-logic-017","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"NOT A","input_b":"A","expected_equivalent":false}
{"id":"5s-sem-logic-018","battery":"5s","sub_battery":"semantics","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input_a":"(A IMPL B) AND (B IMPL C)","input_b":"A IMPL C","expected_equivalent":false}

13
bench/fixtures/5s/syntax-arithmetic-v1.jsonl Normal file
View file

@ -0,0 +1,13 @@
{"_meta":{"battery":"5s","sub_battery":"syntax","version":"v1","task_count":12,"notes":"arithmetic@v1 parse-pass tests. Each input is an arithmetic expression that must canonicalize without raising."}}
{"id":"5s-syn-arith-001","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"3","expected":"pass"}
{"id":"5s-syn-arith-002","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"1+2","expected":"pass"}
{"id":"5s-syn-arith-003","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"-7","expected":"pass"}
{"id":"5s-syn-arith-004","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"0.1","expected":"pass"}
{"id":"5s-syn-arith-005","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"0.1+0.2","expected":"pass"}
{"id":"5s-syn-arith-006","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"(1+2)*3","expected":"pass"}
{"id":"5s-syn-arith-007","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"6/4","expected":"pass"}
{"id":"5s-syn-arith-008","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"2**3","expected":"pass"}
{"id":"5s-syn-arith-009","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"-(1+2)","expected":"pass"}
{"id":"5s-syn-arith-010","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"3.14","expected":"pass"}
{"id":"5s-syn-arith-011","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"((1+2)*(3-4))/5","expected":"pass"}
{"id":"5s-syn-arith-012","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"arithmetic","domain":"rational","pi_star_ref":"arithmetic@v1","input":"7*8 - 2","expected":"pass"}

13
bench/fixtures/5s/syntax-logic-v1.jsonl Normal file
View file

@ -0,0 +1,13 @@
{"_meta":{"battery":"5s","sub_battery":"syntax","version":"v1","task_count":12,"notes":"logic-kernel@v1 parse-pass tests. Each input is a propositional expression that must canonicalize without raising."}}
{"id":"5s-syn-logic-001","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A","expected":"pass"}
{"id":"5s-syn-logic-002","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A AND B","expected":"pass"}
{"id":"5s-syn-logic-003","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A OR B","expected":"pass"}
{"id":"5s-syn-logic-004","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"NOT A","expected":"pass"}
{"id":"5s-syn-logic-005","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A IMPL B","expected":"pass"}
{"id":"5s-syn-logic-006","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A IFF B","expected":"pass"}
{"id":"5s-syn-logic-007","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A XOR B","expected":"pass"}
{"id":"5s-syn-logic-008","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"(A AND B) OR (C AND D)","expected":"pass"}
{"id":"5s-syn-logic-009","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"NOT (A OR (B AND C))","expected":"pass"}
{"id":"5s-syn-logic-010","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"TRUE","expected":"pass"}
{"id":"5s-syn-logic-011","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A IMPL (B IMPL C)","expected":"pass"}
{"id":"5s-syn-logic-012","battery":"5s","sub_battery":"syntax","version":"v1","carrier":"logic","domain":"propositional","pi_star_ref":"logic-kernel@v1","input":"A AND B AND C AND D","expected":"pass"}

230
tests/test_pi_star.py
View file

@ -127,9 +127,10 @@ def test_claim_lattice_empty_input_returns_empty_array():
@pytest.mark.parametrize(
"key",
[
# code-py-ast@v1 graduated from stub to real implementation —
# see test_code_py_ast_* below.
"logic-kernel@v1",
# code-py-ast@v1 graduated to real implementation — see
# test_code_py_ast_*.
# logic-kernel@v1 graduated to real CNF canonicalizer — see
# test_logic_kernel_*.
"time-series-quantized@v1",
"tabular-pinned@v1",
],
@ -234,6 +235,229 @@ def test_code_py_ast_equivalence_class_id_format():
assert eid == equivalence_class_id(pi_star, b"x = 1")
# --- arithmetic@v1 (graduated from stub) -----------------------------
def test_arithmetic_canonicalizes_integer():
pi_star = get("arithmetic@v1")
assert pi_star.canonicalize(b"3") == b"3/1"
assert pi_star.canonicalize(b"-7") == b"-7/1"
def test_arithmetic_canonicalizes_decimal_exactly():
"""SQD §14.1: 0.1 must canonicalize to 1/10 exactly."""
pi_star = get("arithmetic@v1")
assert pi_star.canonicalize(b"0.1") == b"1/10"
assert pi_star.canonicalize(b"0.5") == b"1/2"
assert pi_star.canonicalize(b"0.25") == b"1/4"
def test_arithmetic_solves_classic_floating_point_question():
"""The SQD canonical example: 0.1 + 0.2 == 0.3 exactly."""
pi_star = get("arithmetic@v1")
a = pi_star.canonicalize(b"0.1+0.2")
b = pi_star.canonicalize(b"0.3")
assert a == b == b"3/10"
def test_arithmetic_collapses_equivalent_expressions():
pi_star = get("arithmetic@v1")
assert pi_star.canonicalize(b"1+2") == pi_star.canonicalize(b"3")
assert pi_star.canonicalize(b"(1+2)*3") == pi_star.canonicalize(b"9")
assert pi_star.canonicalize(b"6/4") == pi_star.canonicalize(b"3/2")
def test_arithmetic_distinguishes_distinct_values():
pi_star = get("arithmetic@v1")
assert pi_star.canonicalize(b"1+2") != pi_star.canonicalize(b"4")
assert pi_star.canonicalize(b"1/2") != pi_star.canonicalize(b"1/3")
def test_arithmetic_supports_integer_exponent():
pi_star = get("arithmetic@v1")
assert pi_star.canonicalize(b"2**3") == b"8/1"
assert pi_star.canonicalize(b"3**2") == b"9/1"
def test_arithmetic_rejects_division_by_zero():
from arborist.pi_star.protocol import PiStarError
pi_star = get("arithmetic@v1")
with pytest.raises(PiStarError, match="division by zero"):
pi_star.canonicalize(b"1/0")
def test_arithmetic_rejects_variables():
from arborist.pi_star.protocol import PiStarError
pi_star = get("arithmetic@v1")
with pytest.raises(PiStarError, match="identifier"):
pi_star.canonicalize(b"x + 1")
def test_arithmetic_rejects_non_integer_exponent():
from arborist.pi_star.protocol import PiStarError
pi_star = get("arithmetic@v1")
with pytest.raises(PiStarError, match="non-integer exponent"):
pi_star.canonicalize(b"2 ** 0.5")
def test_arithmetic_rejects_function_calls():
from arborist.pi_star.protocol import PiStarError
pi_star = get("arithmetic@v1")
with pytest.raises(PiStarError, match="function call"):
pi_star.canonicalize(b"abs(-5)")
def test_arithmetic_rejects_invalid_syntax():
from arborist.pi_star.protocol import PiStarError
pi_star = get("arithmetic@v1")
with pytest.raises(PiStarError):
pi_star.canonicalize(b"1 +")
def test_arithmetic_rejects_empty_input():
from arborist.pi_star.protocol import PiStarError
pi_star = get("arithmetic@v1")
with pytest.raises(PiStarError, match="empty"):
pi_star.canonicalize(b"")
def test_arithmetic_canonical_form_is_idempotent():
pi_star = get("arithmetic@v1")
once = pi_star.canonicalize(b"6/4")
twice = pi_star.canonicalize(once)
assert once == twice == b"3/2"
def test_arithmetic_handles_negative_results():
pi_star = get("arithmetic@v1")
assert pi_star.canonicalize(b"-(1+2)") == b"-3/1"
assert pi_star.canonicalize(b"3 - 5") == b"-2/1"
# --- logic-kernel@v1 (graduated from stub) ---------------------------
def test_logic_kernel_canonicalizes_simple_and():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"A AND B") == b"A AND B"
def test_logic_kernel_commutativity():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"A AND B") == pi_star.canonicalize(b"B AND A")
assert pi_star.canonicalize(b"A OR B") == pi_star.canonicalize(b"B OR A")
def test_logic_kernel_associativity():
pi_star = get("logic-kernel@v1")
a = pi_star.canonicalize(b"(A AND B) AND C")
b = pi_star.canonicalize(b"A AND (B AND C)")
assert a == b
def test_logic_kernel_impl_rewrite():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"A IMPL B") == pi_star.canonicalize(b"NOT A OR B")
def test_logic_kernel_iff_rewrite():
pi_star = get("logic-kernel@v1")
a = pi_star.canonicalize(b"A IFF B")
b = pi_star.canonicalize(b"(NOT A OR B) AND (NOT B OR A)")
assert a == b
def test_logic_kernel_xor_rewrite():
pi_star = get("logic-kernel@v1")
a = pi_star.canonicalize(b"A XOR B")
b = pi_star.canonicalize(b"(A OR B) AND (NOT A OR NOT B)")
assert a == b
def test_logic_kernel_de_morgans():
pi_star = get("logic-kernel@v1")
a = pi_star.canonicalize(b"NOT (A AND B)")
b = pi_star.canonicalize(b"(NOT A) OR (NOT B)")
assert a == b
def test_logic_kernel_double_negation():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"NOT NOT A") == pi_star.canonicalize(b"A")
def test_logic_kernel_distribution():
pi_star = get("logic-kernel@v1")
a = pi_star.canonicalize(b"A OR (B AND C)")
b = pi_star.canonicalize(b"(A OR B) AND (A OR C)")
assert a == b
def test_logic_kernel_tautology_collapses_to_true():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"A OR NOT A") == b"TRUE"
assert pi_star.canonicalize(b"TRUE") == b"TRUE"
def test_logic_kernel_idempotence():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"A AND A") == pi_star.canonicalize(b"A")
assert pi_star.canonicalize(b"A OR A") == pi_star.canonicalize(b"A")
def test_logic_kernel_distinguishes_logically_distinct():
pi_star = get("logic-kernel@v1")
assert pi_star.canonicalize(b"A AND B") != pi_star.canonicalize(b"A OR B")
assert pi_star.canonicalize(b"A IMPL B") != pi_star.canonicalize(b"B IMPL A")
def test_logic_kernel_caps_atom_count():
from arborist.pi_star.protocol import PiStarError
pi_star = get("logic-kernel@v1")
expr = b"A AND B AND C AND D AND E AND F AND G AND H AND I"
with pytest.raises(PiStarError, match="caps atoms at"):
pi_star.canonicalize(expr)
def test_logic_kernel_rejects_empty():
from arborist.pi_star.protocol import PiStarError
pi_star = get("logic-kernel@v1")
with pytest.raises(PiStarError, match="empty"):
pi_star.canonicalize(b"")
def test_logic_kernel_rejects_invalid_syntax():
from arborist.pi_star.protocol import PiStarError
pi_star = get("logic-kernel@v1")
with pytest.raises(PiStarError):
pi_star.canonicalize(b"A AND")
def test_logic_kernel_canonical_form_is_idempotent():
pi_star = get("logic-kernel@v1")
src = b"(A OR B) AND (NOT A OR C)"
once = pi_star.canonicalize(src)
twice = pi_star.canonicalize(once)
assert once == twice
def test_logic_kernel_contrapositive_equivalence():
"""A IMPL B ≡ NOT B IMPL NOT A"""
pi_star = get("logic-kernel@v1")
a = pi_star.canonicalize(b"A IMPL B")
b = pi_star.canonicalize(b"(NOT B) IMPL (NOT A)")
assert a == b
# --- composition --------------------------------------------------