russell@unturf.com
5257f9a8f3
Phase 1b — algebra-symbolic-simplified@v1
==========================================
arborist/pi_star/algebra_symbolic_simplified.py — full-simplify
variant of the Phase-1 expand-only sibling. Closes the trig
identity gap left open at end of Phase 1: sin(x)**2 + cos(x)**2
now collapses to 1, tan(x)*cos(x) to sin(x), exp(log(x)) to x.
Recipe is sp.expand(sp.simplify(expr)) — the follow-up expand
after simplify is load-bearing. simplify alone is non-canonical
for polynomials: it leaves (x+1)**2 in factored form while
collapsing x**2 + 2*x + 1 to expanded form, so two algebraically
equivalent inputs would emit different bytes. Composing with
expand picks one canonical polynomial shape and preserves the
equivalence-class invariant.
Cost: 1-360 ms typical on common trig/exp inputs; pathological
inputs unbounded. No in-π* timeout (the calling pipeline owns
that budget). Operators opt in by registry key — the fast Phase-1
sibling stays the default for callers that only need polynomial
canonicalization.
22 unit tests; all gate on pytest.importorskip("sympy").
Phase 3 — calculus-integral@v1
==============================
arborist/pi_star/calculus_integral.py — symbolic integration with
thread-timeout fallback. JSON-shaped {f, x, limits?,
timeout_seconds?} input. Two output paths:
1. Closed form: sp.srepr(sp.expand(integrate_result)) — same
recipe as algebra-symbolic@v1 so the output is itself a valid
algebra-symbolic input and composes naturally.
2. Unevaluated: b"unevaluated:" + sp.srepr(<Integral>). Prefix
lets callers tell "no closed form" from "input invalid"
without re-parsing the canonical form.
Timeout discipline: ThreadPoolExecutor(max_workers=1) +
future.result(timeout=...). On TimeoutError, synthesize the same
unevaluated sentinel SymPy itself would emit, so timeout +
no-closed-form converge to the same bytes for the same input.
Default 30 s; per-call override via timeout_seconds. Python
threads can't be killed cleanly — a timed-out worker leaks until
SymPy returns. Documented as the cost of the discipline.
Coverage: ∫x dx = x²/2, ∫sin(x) dx = -cos(x), ∫_{0}^{π} sin(x)
dx = 2, ∫_{-∞}^{∞} exp(-x²) dx = √π, exp(x)/log(x) →
unevaluated sentinel. 31 unit tests including a monkeypatch
deterministic timeout test (sleep-mocked SymPy so the timeout
path doesn't depend on any specific input being slow on every
CI runner).
Open #000031 — surface-ingest cited textbooks
=============================================
Design-only ticket. Closes the warrant gap left open at the end
of #000029: today every claim-pack record caps at
ANCHOR-WARRANTED because source_reference is a string field, not
a Merkle-bound proof. Ingesting the cited textbooks as surfaces
+ computing per-claim derivations.proof_blob lets the four-rung
ladder promote them to EVIDENCE-WARRANTED.
License gating: PD sources (Hilbert, Newton, Kolmogorov,
Łukasiewicz, Aristotle) form the green-light scope. Mendelson +
Enderton are proprietary and stay yellow-light pending fox's
explicit decision (purchased single copy / library license / PD
substitute via Hilbert-Ackermann 1928).
Two follow-up tickets reserved: textbook-fetch pipeline +
chunk-resolution layer (mapping source_reference strings to
specific spans within ingested textbooks; the bridge that lets
proof_blob be computed).
Test counts: 153 tests for the work in this commit (algebra
+ algebra-simplified + calculus-derivative + calculus-integral
+ preflight). All pi_star + canonical_projection tests pass
under .venv pytest.
146 lines
3.9 KiB
Python
146 lines
3.9 KiB
Python
"""algebra-symbolic-simplified@v1 π* tests (ticket #000030 Phase 1b).
|
|
|
|
The simplified variant runs ``sp.simplify`` instead of
|
|
``sp.expand``, so trig and exp identities collapse where the
|
|
expand-only sibling leaves them distinct. Whole file skips when
|
|
SymPy is absent.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import pytest
|
|
|
|
sympy = pytest.importorskip("sympy") # entire file skipped if absent
|
|
|
|
from arborist.pi_star import get # noqa: E402
|
|
from arborist.pi_star.protocol import ( # noqa: E402
|
|
PiStarError,
|
|
assert_round_trip,
|
|
equivalence_class_id,
|
|
)
|
|
|
|
|
|
@pytest.fixture
|
|
def ps():
|
|
return get("algebra-symbolic-simplified@v1")
|
|
|
|
|
|
@pytest.fixture
|
|
def expand_only():
|
|
return get("algebra-symbolic@v1")
|
|
|
|
|
|
# --- registry presence ------------------------------------------------
|
|
|
|
|
|
def test_registry_contains_simplified():
|
|
ps = get("algebra-symbolic-simplified@v1")
|
|
assert ps.name == "algebra-symbolic-simplified"
|
|
assert ps.version == "v1"
|
|
assert ps.domain == "symbolic-algebra"
|
|
|
|
|
|
# --- trig identity collapses (the main reason this variant exists) --
|
|
|
|
|
|
@pytest.mark.parametrize(
|
|
"left,right",
|
|
[
|
|
("sin(x)**2 + cos(x)**2", "1"),
|
|
("tan(x)*cos(x)", "sin(x)"),
|
|
("sin(x)*cos(y) + cos(x)*sin(y)", "sin(x + y)"),
|
|
("exp(log(x))", "x"),
|
|
],
|
|
)
|
|
def test_trig_exp_identity_collapses_under_simplify(ps, left, right):
|
|
assert ps.canonicalize(left.encode()) == ps.canonicalize(right.encode())
|
|
assert (
|
|
equivalence_class_id(ps, left.encode())
|
|
== equivalence_class_id(ps, right.encode())
|
|
)
|
|
|
|
|
|
def test_trig_collapse_distinguishes_from_expand_sibling(ps, expand_only):
|
|
"""The whole point of this variant: sin²+cos² collapses here but
|
|
not under algebra-symbolic@v1."""
|
|
a_simplified = ps.canonicalize(b"sin(x)**2 + cos(x)**2")
|
|
a_expanded = expand_only.canonicalize(b"sin(x)**2 + cos(x)**2")
|
|
one_simplified = ps.canonicalize(b"1")
|
|
one_expanded = expand_only.canonicalize(b"1")
|
|
# Under the simplified variant, both reduce to Integer(1).
|
|
assert a_simplified == one_simplified
|
|
# Under the expand-only sibling, they remain distinct.
|
|
assert a_expanded != one_expanded
|
|
|
|
|
|
# --- polynomial identity still collapses (didn't lose Phase-1 surface) --
|
|
|
|
|
|
@pytest.mark.parametrize(
|
|
"left,right",
|
|
[
|
|
("(x+1)**2", "x**2 + 2*x + 1"),
|
|
("(a+b)*(a-b)", "a**2 - b**2"),
|
|
("2*x + 3*x", "5*x"),
|
|
],
|
|
)
|
|
def test_polynomial_identity_still_collapses(ps, left, right):
|
|
assert ps.canonicalize(left.encode()) == ps.canonicalize(right.encode())
|
|
|
|
|
|
# --- distinct expressions stay distinct -------------------------------
|
|
|
|
|
|
@pytest.mark.parametrize(
|
|
"left,right",
|
|
[
|
|
("x**2", "x**3"),
|
|
("sin(x)", "cos(x)"),
|
|
# Without positivity assumption, log(exp(x)) does NOT simplify
|
|
# to x — preserves the no-domain-assumptions discipline.
|
|
("log(exp(x))", "x"),
|
|
],
|
|
)
|
|
def test_distinct_inputs_distinct(ps, left, right):
|
|
assert ps.canonicalize(left.encode()) != ps.canonicalize(right.encode())
|
|
|
|
|
|
# --- round-trip / idempotence ----------------------------------------
|
|
|
|
|
|
@pytest.mark.parametrize(
|
|
"expr",
|
|
[
|
|
"x",
|
|
"x + 1",
|
|
"(x+1)**2",
|
|
"sin(x)**2 + cos(x)**2",
|
|
"tan(x)*cos(x)",
|
|
"exp(log(x))",
|
|
],
|
|
)
|
|
def test_round_trip_idempotent(ps, expr):
|
|
assert_round_trip(ps, expr.encode())
|
|
|
|
|
|
# --- error paths ------------------------------------------------------
|
|
|
|
|
|
def test_empty_input_raises(ps):
|
|
with pytest.raises(PiStarError, match="empty"):
|
|
ps.canonicalize(b"")
|
|
|
|
|
|
def test_unparseable_input_raises(ps):
|
|
with pytest.raises(PiStarError, match="cannot parse"):
|
|
ps.canonicalize(b"$$$ %% nope")
|
|
|
|
|
|
def test_non_bytes_input_raises(ps):
|
|
with pytest.raises(PiStarError, match="expects bytes"):
|
|
ps.canonicalize("not bytes") # type: ignore[arg-type]
|
|
|
|
|
|
def test_relational_input_rejected(ps):
|
|
with pytest.raises(PiStarError, match="boolean/relational"):
|
|
ps.canonicalize(b"x > 0")
|