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.
216 lines
6.5 KiB
Python
216 lines
6.5 KiB
Python
"""calculus-integral@v1 π* tests (ticket #000030 Phase 3).
|
|
|
|
Covers indefinite integrals, definite integrals (with finite and
|
|
infinite limits), unevaluated-sentinel emission, timeout fallback,
|
|
and the JSON-shaped input contract. Whole file skips when SymPy is
|
|
absent.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import json
|
|
|
|
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 PiStarError # noqa: E402
|
|
|
|
|
|
@pytest.fixture
|
|
def ps():
|
|
return get("calculus-integral@v1")
|
|
|
|
|
|
@pytest.fixture
|
|
def algebra():
|
|
return get("algebra-symbolic@v1")
|
|
|
|
|
|
def _q(**kwargs) -> bytes:
|
|
return json.dumps(kwargs).encode("utf-8")
|
|
|
|
|
|
# --- registry presence ------------------------------------------------
|
|
|
|
|
|
def test_registry_contains_calculus_integral():
|
|
ps = get("calculus-integral@v1")
|
|
assert ps.name == "calculus-integral"
|
|
assert ps.version == "v1"
|
|
assert ps.domain == "calculus"
|
|
|
|
|
|
# --- indefinite integrals ---------------------------------------------
|
|
|
|
|
|
@pytest.mark.parametrize(
|
|
"f,x,expected",
|
|
[
|
|
("x", "x", "x**2/2"),
|
|
("x**2", "x", "x**3/3"),
|
|
("sin(x)", "x", "-cos(x)"),
|
|
("cos(x)", "x", "sin(x)"),
|
|
("exp(x)", "x", "exp(x)"),
|
|
("1/x", "x", "log(x)"),
|
|
("1", "x", "x"),
|
|
],
|
|
)
|
|
def test_indefinite_integral_matches_expected(ps, algebra, f, x, expected):
|
|
got = ps.canonicalize(_q(f=f, x=x))
|
|
want = algebra.canonicalize(expected.encode())
|
|
assert got == want
|
|
|
|
|
|
# --- definite integrals (finite limits) ------------------------------
|
|
|
|
|
|
@pytest.mark.parametrize(
|
|
"f,x,a,b,expected",
|
|
[
|
|
("x", "x", "0", "1", "1/2"),
|
|
("x**2", "x", "0", "1", "1/3"),
|
|
("sin(x)", "x", "0", "pi", "2"),
|
|
("1", "x", "0", "5", "5"),
|
|
],
|
|
)
|
|
def test_definite_integral_matches_expected(ps, algebra, f, x, a, b, expected):
|
|
got = ps.canonicalize(_q(f=f, x=x, limits=[a, b]))
|
|
want = algebra.canonicalize(expected.encode())
|
|
assert got == want
|
|
|
|
|
|
# --- definite integrals with infinite limits -------------------------
|
|
|
|
|
|
def test_definite_integral_gaussian(ps, algebra):
|
|
"""∫_{-∞}^{∞} exp(-x²) dx = √π."""
|
|
got = ps.canonicalize(_q(f="exp(-x**2)", x="x", limits=["-oo", "oo"]))
|
|
want = algebra.canonicalize(b"sqrt(pi)")
|
|
assert got == want
|
|
|
|
|
|
# --- unevaluated sentinel --------------------------------------------
|
|
|
|
|
|
def test_unevaluated_integral_emits_sentinel(ps):
|
|
"""Some integrands have no elementary closed form. SymPy returns
|
|
an Integral object; this π* prefixes the canonical bytes with
|
|
``unevaluated:`` so callers can distinguish "no closed form"
|
|
from "input invalid"."""
|
|
out = ps.canonicalize(_q(f="exp(x)/log(x)", x="x"))
|
|
assert out.startswith(b"unevaluated:")
|
|
# Sentinel body is an Integral S-expression.
|
|
body = out[len(b"unevaluated:"):]
|
|
assert b"Integral" in body
|
|
assert b"Symbol('x')" in body
|
|
|
|
|
|
def test_unevaluated_sentinel_is_deterministic(ps):
|
|
"""Same unevaluated input → same sentinel bytes."""
|
|
a = ps.canonicalize(_q(f="exp(x)/log(x)", x="x"))
|
|
b = ps.canonicalize(_q(f="exp(x)/log(x)", x="x"))
|
|
assert a == b
|
|
|
|
|
|
# --- timeout fallback -------------------------------------------------
|
|
|
|
|
|
def test_timeout_fallback_emits_unevaluated_sentinel(ps, monkeypatch):
|
|
"""A timeout forces the worker to abort. The sentinel matches
|
|
what SymPy would emit for the unevaluated form, so timeout and
|
|
no-closed-form converge to the same bytes for the same input.
|
|
(Equivalence-class invariant under cost variance.)
|
|
|
|
We monkeypatch ``sp.integrate`` to sleep so the test is
|
|
deterministic across hardware, rather than depending on a
|
|
pathological input being slow enough on every CI runner.
|
|
"""
|
|
import time as _time
|
|
import arborist.pi_star.calculus_integral as mod
|
|
|
|
real_integrate = mod.sp.integrate
|
|
|
|
def slow_integrate(*args, **kwargs):
|
|
_time.sleep(2.0)
|
|
return real_integrate(*args, **kwargs)
|
|
|
|
monkeypatch.setattr(mod.sp, "integrate", slow_integrate)
|
|
|
|
out = ps.canonicalize(_q(f="x**2", x="x", timeout_seconds=0.05))
|
|
assert out.startswith(b"unevaluated:")
|
|
|
|
|
|
# --- error paths ------------------------------------------------------
|
|
|
|
|
|
def test_non_bytes_input_raises(ps):
|
|
with pytest.raises(PiStarError, match="expects bytes"):
|
|
ps.canonicalize("not bytes") # type: ignore[arg-type]
|
|
|
|
|
|
def test_non_json_input_raises(ps):
|
|
with pytest.raises(PiStarError, match="JSON"):
|
|
ps.canonicalize(b"not json")
|
|
|
|
|
|
def test_missing_f_raises(ps):
|
|
with pytest.raises(PiStarError, match="missing field 'f'"):
|
|
ps.canonicalize(_q(x="x"))
|
|
|
|
|
|
def test_missing_x_raises(ps):
|
|
with pytest.raises(PiStarError, match="missing field 'x'"):
|
|
ps.canonicalize(_q(f="x**2"))
|
|
|
|
|
|
def test_unparseable_f_raises(ps):
|
|
with pytest.raises(PiStarError, match="cannot parse"):
|
|
ps.canonicalize(_q(f="$$$ %% nope", x="x"))
|
|
|
|
|
|
def test_relational_f_rejected(ps):
|
|
with pytest.raises(PiStarError, match="boolean/relational"):
|
|
ps.canonicalize(_q(f="x > 0", x="x"))
|
|
|
|
|
|
def test_limits_must_be_two_element_list(ps):
|
|
with pytest.raises(PiStarError, match="'limits'"):
|
|
ps.canonicalize(_q(f="x", x="x", limits=[1]))
|
|
with pytest.raises(PiStarError, match="'limits'"):
|
|
ps.canonicalize(_q(f="x", x="x", limits="0,1"))
|
|
|
|
|
|
def test_unparseable_limits_raises(ps):
|
|
with pytest.raises(PiStarError, match="limits"):
|
|
ps.canonicalize(_q(f="x", x="x", limits=["$$%", 1]))
|
|
|
|
|
|
@pytest.mark.parametrize("bad_t", [0, -1, "1.0", True, False])
|
|
def test_timeout_must_be_positive_number(ps, bad_t):
|
|
with pytest.raises(PiStarError, match="positive number"):
|
|
ps.canonicalize(_q(f="x", x="x", timeout_seconds=bad_t))
|
|
|
|
|
|
# --- equivalence-class behavior --------------------------------------
|
|
|
|
|
|
def test_equivalent_integrands_collapse(ps):
|
|
"""∫(x+1)² dx ≡ ∫(x²+2x+1) dx — same closed form output."""
|
|
a = ps.canonicalize(_q(f="(x+1)**2", x="x"))
|
|
b = ps.canonicalize(_q(f="x**2 + 2*x + 1", x="x"))
|
|
assert a == b
|
|
|
|
|
|
# --- composition / output is algebra-symbolic@v1 input ---------------
|
|
|
|
|
|
def test_closed_form_output_is_algebra_symbolic_input(ps, algebra):
|
|
"""A closed-form integral byte sequence is itself a valid
|
|
algebra-symbolic@v1 input; canonicalizing it again is idempotent."""
|
|
raw = ps.canonicalize(_q(f="x**2", x="x"))
|
|
assert not raw.startswith(b"unevaluated:")
|
|
once = algebra.canonicalize(raw)
|
|
twice = algebra.canonicalize(once)
|
|
assert once == twice
|