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.
This commit is contained in:
parent
708aa450cb
commit
5257f9a8f3
8 changed files with 1120 additions and 3 deletions
|
|
@ -12,9 +12,16 @@ Concrete π*'s shipped today (alphabetical):
|
|||
|
||||
- ``algebra-symbolic@v1`` — symbolic algebra (SymPy expand + srepr).
|
||||
Optional; registers only when ``sympy`` is importable.
|
||||
- ``algebra-symbolic-simplified@v1`` — full-simplify variant
|
||||
(SymPy simplify + srepr). Slower than expand-only sibling;
|
||||
collapses trig identity. Optional, gates on ``sympy``.
|
||||
- ``arithmetic@v1`` — closed-form rational arithmetic (SQD §14.1).
|
||||
- ``calculus-derivative@v1`` — symbolic derivative (SymPy diff +
|
||||
expand). Optional; gates on ``sympy`` like algebra-symbolic.
|
||||
- ``calculus-integral@v1`` — symbolic integral (SymPy integrate +
|
||||
thread-timeout + expand). Optional; gates on ``sympy``. Returns
|
||||
an ``unevaluated:Integral(...)`` sentinel when no closed form
|
||||
exists or the timeout fires.
|
||||
- ``claim-lattice@v1`` — claim lines → JSON parsed-claim list.
|
||||
- ``code-py-ast@v1`` — Python source → canonical AST S-expression.
|
||||
- ``logic-kernel@v1`` — propositional Boolean → CNF (SQD §14.3).
|
||||
|
|
@ -52,8 +59,10 @@ from arborist.pi_star.registry import (
|
|||
# guard via a defensive `import sympy` and skip register(...) when
|
||||
# absent, so a fresh checkout without the [math] extra still loads.
|
||||
from arborist.pi_star import algebra_symbolic # noqa: F401,E402
|
||||
from arborist.pi_star import algebra_symbolic_simplified # noqa: F401,E402
|
||||
from arborist.pi_star import arithmetic # noqa: F401,E402
|
||||
from arborist.pi_star import calculus_derivative # noqa: F401,E402
|
||||
from arborist.pi_star import calculus_integral # 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
|
||||
|
|
|
|||
140
arborist/pi_star/algebra_symbolic_simplified.py
Normal file
140
arborist/pi_star/algebra_symbolic_simplified.py
Normal file
|
|
@ -0,0 +1,140 @@
|
|||
"""``algebra-symbolic-simplified@v1`` π* — full-simplify variant.
|
||||
|
||||
Domain: ``symbolic-algebra``. The ``algebra-symbolic@v1`` sibling
|
||||
runs ``sp.expand`` only — fast, polynomial+exponential identity
|
||||
collapses, but trigonometric identities do not. This variant runs
|
||||
``sp.simplify`` instead — slower, with unbounded CPU on
|
||||
pathological inputs, but trig identity collapses (and many other
|
||||
algebraic identities ``expand`` won't touch).
|
||||
|
||||
Why this variant exists
|
||||
-----------------------
|
||||
Ticket #000030 §2.3 deferred the trig surface to a separate version
|
||||
because ``sp.simplify`` cost is unbounded — operators opt in when
|
||||
they need it. Splitting the variant keeps the fast path fast for
|
||||
operators who only care about polynomial canonicalization.
|
||||
|
||||
Equivalence classes preserved
|
||||
-----------------------------
|
||||
Everything ``algebra-symbolic@v1`` collapses, plus:
|
||||
|
||||
- ``"sin(x)**2 + cos(x)**2"`` ≡ ``"1"``
|
||||
- ``"tan(x)*cos(x)"`` ≡ ``"sin(x)"``
|
||||
- ``"exp(log(x))"`` ≡ ``"x"``
|
||||
- ``"sin(x)*cos(y) + cos(x)*sin(y)"`` ≡ ``"sin(x + y)"``
|
||||
|
||||
Equivalence classes still kept distinct
|
||||
---------------------------------------
|
||||
``sp.simplify`` makes domain assumptions (e.g. ``log(exp(x))`` does
|
||||
NOT collapse to ``x`` without an explicit positive-real assumption
|
||||
on ``x``). Where the user's intent depends on the assumption, the
|
||||
outputs stay distinct; this is correct behavior — symbol assumptions
|
||||
are out of scope for Phase 1b.
|
||||
|
||||
Canonical bytes
|
||||
---------------
|
||||
``sp.srepr(sp.expand(sp.simplify(expr)))`` UTF-8 encoded.
|
||||
``simplify`` collapses identities (trig, exp, log on real domains);
|
||||
``expand`` then enforces a uniform polynomial form so two
|
||||
algebraically equivalent inputs (``(x+1)**2`` and ``x**2 + 2*x + 1``)
|
||||
emit the same canonical bytes. ``simplify`` alone would leave them
|
||||
in different shapes (factored vs expanded) and break the
|
||||
equivalence-class invariant.
|
||||
|
||||
Round-trip property
|
||||
-------------------
|
||||
Idempotent: ``simplify(simplify(x)) == simplify(x)`` is the SymPy
|
||||
contract (verified empirically against the trig/exp surface).
|
||||
|
||||
Cost discipline
|
||||
---------------
|
||||
``sp.simplify`` is observed at 1-360 ms on common trig/exp inputs;
|
||||
pathological inputs can grow exponentially. Operators must size for
|
||||
the worst case before enabling on a hot path. There is no built-in
|
||||
timeout in this Phase-1b implementation — the natural place for a
|
||||
timeout wrap is the calling pipeline (preflight router has its own
|
||||
budget), not inside the π*. Phase 3 (``calculus-integral@v1``) is
|
||||
where the in-π* timeout pattern lands; Phase 1b leaves the
|
||||
unbounded surface visible to operators.
|
||||
|
||||
Optional dependency
|
||||
-------------------
|
||||
Same as ``algebra-symbolic@v1``: SymPy via the ``[math]`` extras.
|
||||
When SymPy is absent, :func:`canonicalize` raises
|
||||
:class:`PiStarError`.
|
||||
|
||||
Source: ticket #000030 §2.3 deferred Phase 1b — landed 2026-05-09.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
from dataclasses import dataclass
|
||||
|
||||
from arborist.pi_star.protocol import PiStarError
|
||||
from arborist.pi_star.registry import register
|
||||
|
||||
|
||||
try:
|
||||
import sympy as sp # type: ignore[import-not-found]
|
||||
except ImportError: # pragma: no cover — optional extra
|
||||
sp = None # type: ignore[assignment]
|
||||
|
||||
|
||||
_SYMPY_REQUIRED_MSG = (
|
||||
"algebra-symbolic-simplified@v1 requires sympy; install with "
|
||||
"`pip install 'arborist[math]'`"
|
||||
)
|
||||
|
||||
|
||||
@dataclass
|
||||
class AlgebraSymbolicSimplifiedV1:
|
||||
name: str = "algebra-symbolic-simplified"
|
||||
version: str = "v1"
|
||||
domain: str = "symbolic-algebra"
|
||||
|
||||
def canonicalize(self, raw: bytes) -> bytes:
|
||||
if sp is None:
|
||||
raise PiStarError(_SYMPY_REQUIRED_MSG)
|
||||
if not isinstance(raw, (bytes, bytearray)):
|
||||
raise PiStarError(
|
||||
"algebra-symbolic-simplified@v1 expects bytes; got "
|
||||
f"{type(raw).__name__}"
|
||||
)
|
||||
try:
|
||||
text = 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
|
||||
text = text.strip()
|
||||
if not text:
|
||||
raise PiStarError("algebra-symbolic-simplified@v1 input is empty")
|
||||
|
||||
try:
|
||||
expr = sp.sympify(text)
|
||||
except (sp.SympifyError, SyntaxError, TypeError) as exc:
|
||||
raise PiStarError(
|
||||
f"algebra-symbolic-simplified@v1 cannot parse {text!r}: {exc}"
|
||||
) from exc
|
||||
|
||||
# Same Expr-vs-Boolean filter as algebra-symbolic@v1 — Symbol
|
||||
# confusingly inherits from Boolean, so the right rejection is
|
||||
# "not an Expr."
|
||||
if not isinstance(expr, sp.Expr):
|
||||
raise PiStarError(
|
||||
f"algebra-symbolic-simplified@v1 rejects boolean/relational "
|
||||
f"input {text!r}; use logic-kernel@v1 for that shape"
|
||||
)
|
||||
|
||||
try:
|
||||
simplified = sp.simplify(expr)
|
||||
canonical = sp.expand(simplified)
|
||||
except (TypeError, ValueError) as exc:
|
||||
raise PiStarError(
|
||||
f"algebra-symbolic-simplified@v1 simplify/expand failed on "
|
||||
f"{text!r}: {exc}"
|
||||
) from exc
|
||||
|
||||
return sp.srepr(canonical).encode("utf-8")
|
||||
|
||||
|
||||
if sp is not None:
|
||||
register(AlgebraSymbolicSimplifiedV1())
|
||||
229
arborist/pi_star/calculus_integral.py
Normal file
229
arborist/pi_star/calculus_integral.py
Normal file
|
|
@ -0,0 +1,229 @@
|
|||
"""``calculus-integral@v1`` π* — symbolic-integral canonicalizer.
|
||||
|
||||
Domain: ``calculus``. Computes the indefinite or definite integral
|
||||
of a symbolic expression with respect to a named variable. Wraps
|
||||
``sp.integrate`` with a soft timeout so pathological inputs cannot
|
||||
hang the caller indefinitely.
|
||||
|
||||
Why this matters
|
||||
----------------
|
||||
Ticket #000030 §2.2 Phase 3. Integration is the natural counterpart
|
||||
to the Phase-2 derivative: same JSON-shaped input contract, same
|
||||
``algebra-symbolic@v1``-style canonical bytes for the
|
||||
closed-form-result case, with one extra rule for unevaluated
|
||||
results.
|
||||
|
||||
Input shape (JSON, UTF-8)
|
||||
-------------------------
|
||||
::
|
||||
|
||||
{"f": "<expression-text>", "x": "<variable-name>",
|
||||
"limits"?: [<lower>, <upper>],
|
||||
"timeout_seconds"?: <float>}
|
||||
|
||||
- ``f`` — the integrand (parsed via :func:`sympy.sympify`).
|
||||
- ``x`` — the variable name.
|
||||
- ``limits`` — optional ``[a, b]``. Each endpoint is sympified, so
|
||||
``"oo"`` (positive infinity), ``"-oo"``, ``"pi"``, etc. all work.
|
||||
- ``timeout_seconds`` — optional, default :data:`DEFAULT_TIMEOUT`.
|
||||
|
||||
Output canonical bytes
|
||||
----------------------
|
||||
Two paths:
|
||||
|
||||
1. **Closed-form result:**
|
||||
``sp.srepr(sp.expand(integrate_result))`` UTF-8 — same recipe as
|
||||
``algebra-symbolic@v1``. Means an integral that evaluates is a
|
||||
first-class composition target.
|
||||
2. **Unevaluated result** (SymPy returns an :class:`sympy.Integral`
|
||||
or :class:`sympy.NonElementaryIntegral` object, OR the timeout
|
||||
fires): bytes are ``b"unevaluated:" + sp.srepr(<Integral>)``.
|
||||
The ``unevaluated:`` prefix lets callers distinguish "no closed
|
||||
form" from "input invalid" without parsing the canonical form.
|
||||
|
||||
Timeout discipline
|
||||
------------------
|
||||
``sp.integrate`` can hang on pathological inputs. We launch the
|
||||
work on a :class:`ThreadPoolExecutor` and ``future.result(timeout=…)``;
|
||||
on :class:`TimeoutError`, we synthesize an unevaluated sentinel
|
||||
(``Integral`` / ``Integral(<expr>, (<x>, a, b))``). A timed-out
|
||||
thread continues running in the background — Python threads cannot
|
||||
be killed cleanly. Operators tuning a hot path should size the
|
||||
worker pool accordingly. The default 30s timeout is conservative;
|
||||
per-call override via ``timeout_seconds`` in the input JSON.
|
||||
|
||||
Round-trip property
|
||||
-------------------
|
||||
Closed-form bytes round-trip through the algebra-symbolic@v1
|
||||
recipe. Unevaluated-sentinel bytes do NOT round-trip through this
|
||||
π* (the input contract is JSON, not srepr); their round-trip is at
|
||||
the equivalence-class layer (same input ⇒ same sentinel).
|
||||
|
||||
Optional dependency
|
||||
-------------------
|
||||
Same as ``algebra-symbolic@v1``: SymPy via the ``[math]`` extras.
|
||||
|
||||
Source: ticket #000030 §2.2 Phase 3 — landed 2026-05-09.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import concurrent.futures
|
||||
import json
|
||||
from dataclasses import dataclass
|
||||
|
||||
from arborist.pi_star.protocol import PiStarError
|
||||
from arborist.pi_star.registry import register
|
||||
|
||||
|
||||
try:
|
||||
import sympy as sp # type: ignore[import-not-found]
|
||||
except ImportError: # pragma: no cover — optional extra
|
||||
sp = None # type: ignore[assignment]
|
||||
|
||||
|
||||
DEFAULT_TIMEOUT = 30.0 # seconds
|
||||
|
||||
|
||||
_SYMPY_REQUIRED_MSG = (
|
||||
"calculus-integral@v1 requires sympy; install with "
|
||||
"`pip install 'arborist[math]'`"
|
||||
)
|
||||
|
||||
|
||||
def _is_unevaluated(result) -> bool:
|
||||
"""True when ``sp.integrate`` returned an unevaluated form.
|
||||
|
||||
Both :class:`sympy.Integral` and the more specific
|
||||
:class:`sympy.integrals.integrals.NonElementaryIntegral` count
|
||||
— the latter is a subclass.
|
||||
"""
|
||||
return isinstance(result, sp.Integral)
|
||||
|
||||
|
||||
def _sentinel(unevaluated) -> bytes:
|
||||
return b"unevaluated:" + sp.srepr(unevaluated).encode("utf-8")
|
||||
|
||||
|
||||
def _build_unevaluated(f_expr, x_sym, limits_pair):
|
||||
"""Construct an unevaluated Integral object representing the
|
||||
requested integration. Used both for the timeout-fallback path
|
||||
and as the test target for sentinel parsing."""
|
||||
if limits_pair is None:
|
||||
return sp.Integral(f_expr, x_sym)
|
||||
a, b = limits_pair
|
||||
return sp.Integral(f_expr, (x_sym, a, b))
|
||||
|
||||
|
||||
@dataclass
|
||||
class CalculusIntegralV1:
|
||||
name: str = "calculus-integral"
|
||||
version: str = "v1"
|
||||
domain: str = "calculus"
|
||||
|
||||
def canonicalize(self, raw: bytes) -> bytes:
|
||||
if sp is None:
|
||||
raise PiStarError(_SYMPY_REQUIRED_MSG)
|
||||
if not isinstance(raw, (bytes, bytearray)):
|
||||
raise PiStarError(
|
||||
"calculus-integral@v1 expects bytes; got "
|
||||
f"{type(raw).__name__}"
|
||||
)
|
||||
try:
|
||||
text = 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
|
||||
|
||||
try:
|
||||
obj = json.loads(text)
|
||||
except json.JSONDecodeError as exc:
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 input must be JSON object: {exc}"
|
||||
) from exc
|
||||
if not isinstance(obj, dict):
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 input must be JSON object; got {type(obj).__name__}"
|
||||
)
|
||||
|
||||
for k in ("f", "x"):
|
||||
if k not in obj:
|
||||
raise PiStarError(f"calculus-integral@v1 missing field {k!r}")
|
||||
if not isinstance(obj[k], str) or not obj[k].strip():
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 field {k!r} must be a non-empty string"
|
||||
)
|
||||
|
||||
timeout = obj.get("timeout_seconds", DEFAULT_TIMEOUT)
|
||||
if not isinstance(timeout, (int, float)) or isinstance(timeout, bool) or timeout <= 0:
|
||||
raise PiStarError(
|
||||
"calculus-integral@v1 'timeout_seconds' must be a positive number"
|
||||
)
|
||||
|
||||
x_name = obj["x"].strip()
|
||||
x_sym = sp.Symbol(x_name)
|
||||
try:
|
||||
f_expr = sp.sympify(obj["f"], locals={x_name: x_sym})
|
||||
except (sp.SympifyError, SyntaxError, TypeError) as exc:
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 cannot parse f={obj['f']!r}: {exc}"
|
||||
) from exc
|
||||
if not isinstance(f_expr, sp.Expr):
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 rejects boolean/relational f={obj['f']!r}"
|
||||
)
|
||||
|
||||
limits_pair = None
|
||||
if "limits" in obj:
|
||||
lim = obj["limits"]
|
||||
if not (isinstance(lim, list) and len(lim) == 2):
|
||||
raise PiStarError(
|
||||
"calculus-integral@v1 'limits' must be a 2-element list [a, b]"
|
||||
)
|
||||
try:
|
||||
a = sp.sympify(lim[0])
|
||||
b = sp.sympify(lim[1])
|
||||
except (sp.SympifyError, SyntaxError, TypeError) as exc:
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 cannot parse limits {lim!r}: {exc}"
|
||||
) from exc
|
||||
limits_pair = (a, b)
|
||||
|
||||
# Run sp.integrate in a worker thread with a timeout. If the
|
||||
# work hangs, the thread leaks (Python threads aren't killable);
|
||||
# the canonical result for the timeout case is an unevaluated
|
||||
# Integral sentinel so the equivalence-class behavior stays
|
||||
# deterministic.
|
||||
def _work():
|
||||
if limits_pair is None:
|
||||
return sp.integrate(f_expr, x_sym)
|
||||
return sp.integrate(f_expr, (x_sym, limits_pair[0], limits_pair[1]))
|
||||
|
||||
with concurrent.futures.ThreadPoolExecutor(max_workers=1) as pool:
|
||||
future = pool.submit(_work)
|
||||
try:
|
||||
result = future.result(timeout=float(timeout))
|
||||
except concurrent.futures.TimeoutError:
|
||||
# Synthesize the unevaluated sentinel — same content
|
||||
# we'd emit if SymPy itself returned an unevaluated
|
||||
# Integral. Avoids two distinct "no closed form" paths
|
||||
# producing different bytes.
|
||||
return _sentinel(_build_unevaluated(f_expr, x_sym, limits_pair))
|
||||
except (TypeError, ValueError, sp.SympifyError) as exc:
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 integrate failed: {exc}"
|
||||
) from exc
|
||||
|
||||
if _is_unevaluated(result):
|
||||
return _sentinel(result)
|
||||
|
||||
try:
|
||||
canonical = sp.expand(result)
|
||||
except (TypeError, ValueError) as exc:
|
||||
raise PiStarError(
|
||||
f"calculus-integral@v1 expand failed: {exc}"
|
||||
) from exc
|
||||
return sp.srepr(canonical).encode("utf-8")
|
||||
|
||||
|
||||
if sp is not None:
|
||||
register(CalculusIntegralV1())
|
||||
|
|
@ -61,7 +61,8 @@ Newest first. Update on every open/close.
|
|||
|
||||
| ID | Title | Status | Opened | Directive |
|
||||
|----------|------------------------------------------------|-----------------------|------------|-----------|
|
||||
| #000030 | Math π* expansion: SymPy substrate (algebra · calculus · linalg) | closed · Phases 1+2 landed 2026-05-09 (3-7 future work) | 2026-05-09 | — |
|
||||
| #000031 | Surface-ingest cited textbooks for claim-pack warrant promotion | open · awaiting go/no-go | 2026-05-09 | — |
|
||||
| #000030 | Math π* expansion: SymPy substrate (algebra · calculus · linalg) | closed · Phases 1+2+1b+3 landed 2026-05-09 (4-7 future work) | 2026-05-09 | — |
|
||||
| #000029 | Claim-pack source (axiom/theorem JSON bundles) | closed · landed 2026-05-09 | 2026-05-09 | — |
|
||||
| #000028 | Multi-modality witness for canonical shapes | closed · landed 2026-05-09 + follow-ups (capital ledger · sample rate) | 2026-05-08 | — |
|
||||
| #000027 | Canonical projections persist to providence_cache | closed · landed 2026-05-09 | 2026-05-08 | — |
|
||||
|
|
@ -94,4 +95,4 @@ Newest first. Update on every open/close.
|
|||
|
||||
## Next ID
|
||||
|
||||
`000031`
|
||||
`000032`
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
# Ticket #000030 — Math π* expansion: SymPy substrate
|
||||
|
||||
**Status:** closed · Phases 1+2 landed 2026-05-09 (Phases 3-7 remain open as future work)
|
||||
**Status:** closed · Phases 1+2+1b+3 landed 2026-05-09 (Phases 4-7 remain open as future work)
|
||||
**Opened:** 2026-05-09
|
||||
**Scope:** Extend the π* registry with SymPy-backed canonicalizers
|
||||
covering symbolic algebra, calculus (derivatives, integrals,
|
||||
|
|
@ -503,3 +503,60 @@ docs, and the preflight wiring.
|
|||
Phase 3-7 follow-on size estimate (`~80 LOC each`) carries
|
||||
forward; each gets its own future ticket when an actual consumer
|
||||
surfaces the need.
|
||||
|
||||
---
|
||||
|
||||
### Phase 1b — algebra-symbolic-simplified@v1 (landed 2026-05-09)
|
||||
|
||||
`arborist/pi_star/algebra_symbolic_simplified.py` — full-simplify
|
||||
variant. Recipe: `sp.expand(sp.simplify(expr))` → srepr. The
|
||||
follow-up `expand` after `simplify` enforces a uniform polynomial
|
||||
canonical form; without it, `(x+1)**2` and `x**2 + 2*x + 1`
|
||||
collapse under `simplify` to DIFFERENT shapes (factored vs
|
||||
expanded) and break the equivalence-class invariant. The composed
|
||||
recipe collapses both polynomial + trig identity:
|
||||
|
||||
- `sin(x)**2 + cos(x)**2` ≡ `1`
|
||||
- `tan(x)*cos(x)` ≡ `sin(x)`
|
||||
- `(x+1)**2` ≡ `x**2 + 2*x + 1` (still)
|
||||
|
||||
Cost: 1-360 ms typical; 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 gating on `pytest.importorskip("sympy")`.
|
||||
|
||||
### Phase 3 — calculus-integral@v1 (landed 2026-05-09)
|
||||
|
||||
`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** (SymPy returns `Integral(...)`, OR the timeout
|
||||
fires): `b"unevaluated:" + sp.srepr(<Integral>)`. The
|
||||
`unevaluated:` prefix lets callers tell "no closed form" from
|
||||
"input invalid" without re-parsing the canonical form.
|
||||
|
||||
Timeout discipline: `concurrent.futures.ThreadPoolExecutor` with
|
||||
`future.result(timeout=…)`. On timeout, 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 cannot be killed cleanly — a timed-out worker leaks until
|
||||
SymPy returns; document this as the cost of the discipline.
|
||||
|
||||
Coverage:
|
||||
|
||||
- Indefinite integrals (`∫x dx = x²/2`, `∫sin(x) dx = -cos(x)`,
|
||||
…).
|
||||
- Definite integrals with finite + infinite limits (Gaussian
|
||||
`∫_{-∞}^{∞} exp(-x²) dx = √π`).
|
||||
- Unevaluated sentinel for `exp(x)/log(x)` and timeout-induced
|
||||
unevaluated paths.
|
||||
- 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).
|
||||
|
|
|
|||
319
docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md
Normal file
319
docs/tickets/ticket-000031-surface-ingest-cited-textbooks.md
Normal file
|
|
@ -0,0 +1,319 @@
|
|||
# Ticket #000031 — Surface-ingest cited textbooks for claim-pack warrant promotion
|
||||
|
||||
**Status:** open · awaiting go/no-go
|
||||
**Opened:** 2026-05-09
|
||||
**Scope:** Ingest the classical textbooks cited by every record in
|
||||
the claim-pack source (`#000029`) — Mendelson 1997, Enderton 2001,
|
||||
Hilbert 1899, Kolmogorov 1933, Łukasiewicz 1921, Newton 1687 — as
|
||||
SURFACE-layer documents. Then compute real `derivations.proof_blob`
|
||||
edges from each claim-pack CORE record (or surface-as-core) to the
|
||||
specific textbook span its `source_reference` field cites. Closes
|
||||
the warrant gap left open at the end of `#000029`: today every
|
||||
claim-pack record caps at `ANCHOR-WARRANTED` because the citation
|
||||
is a string field, not a Merkle-bound proof. With the textbooks in
|
||||
the shard, the four-rung ladder can promote them to
|
||||
`EVIDENCE-WARRANTED`.
|
||||
**Audience:** fox + future blackops shifts; anyone wondering why
|
||||
"prove modus tollens" comes back HYBRID with `· warrant missing`
|
||||
on a shard that already has the claim-pack ingested.
|
||||
**Hard constraint:** **No copyright violation.** Mendelson 1997 and
|
||||
Enderton 2001 are proprietary textbooks. We MUST NOT ingest them as
|
||||
surfaces without a valid license (purchased PDF, library checkout
|
||||
with terms permitting single-machine indexing, or written
|
||||
permission from rights-holder). The public-domain alternatives —
|
||||
Hilbert 1899 (German original; English translation 1902 by E. J.
|
||||
Townsend now PD), Kolmogorov 1933 (German original), Łukasiewicz
|
||||
1921, Newton 1687 — are clear and form the green-light scope below.
|
||||
The proprietary surface remains a separate decision per text.
|
||||
|
||||
---
|
||||
|
||||
## 1. Problem statement
|
||||
|
||||
Ticket `#000029` landed `arborist/sources/claim_pack.py`: 78
|
||||
documents (55 axioms + 23 theorems across 7 pillars) ingested as
|
||||
SURFACE rows. Every record carries a `source_reference` metadata
|
||||
field naming the cited textbook (e.g., "Introduction to
|
||||
Mathematical Logic by Elliott Mendelson"). Honest ceiling per the
|
||||
`#000029` close note:
|
||||
|
||||
> Every record lands at `kind='surface'` ... most items will land
|
||||
> HYBRID at best — that's the honest ceiling without surface texts.
|
||||
|
||||
The four-rung ladder per arborist's CTI architecture maps:
|
||||
|
||||
- `POINTER-LINKED` — answer cites an `evidence_id` (a chunk hash).
|
||||
- `ANCHOR-WARRANTED` — citation passes the lexical anchor check
|
||||
(claim subject token appears in the cited span).
|
||||
- `EVIDENCE-WARRANTED` — every claim has a Merkle-proven
|
||||
derivation back to a surface chunk via `derivations.proof_blob`.
|
||||
- `ENTAILMENT-VERIFIED` — reserved for an NLI / formal-proof
|
||||
upgrade path.
|
||||
|
||||
`#000029` claim-pack records carry citation STRINGS but no
|
||||
`derivations.proof_blob`. Best-case retrieval over them lands at
|
||||
`ANCHOR-WARRANTED` only. To clear `EVIDENCE-WARRANTED` we need:
|
||||
|
||||
1. The cited textbook (or relevant chapter) ingested as a
|
||||
`kind='surface'` document with a stable `document_root`.
|
||||
2. A per-claim mapping from the claim-pack record → the
|
||||
surface-document chunk(s) that contain the cited definition /
|
||||
theorem.
|
||||
3. A `derivations` row binding the two with a real `proof_blob`
|
||||
(per-chunk Merkle inclusion proof per `arborist/store.py`
|
||||
schema).
|
||||
|
||||
This ticket is about (1). Steps (2) and (3) need their own
|
||||
ticket — the mapping is non-trivial because claim-pack
|
||||
`source_reference` is "Mendelson 1997" not "Mendelson p.93", so a
|
||||
chunk-resolution layer has to disambiguate.
|
||||
|
||||
## 2. Design choices
|
||||
|
||||
### 2.1 License gating — what we can and can't ingest
|
||||
|
||||
Claim-pack scrape (`#000029`) cited 7 distinct textbook
|
||||
references:
|
||||
|
||||
| # | Citation | Public domain? | Notes |
|
||||
|---|------------------------------------------------------------|---|---|
|
||||
| 1 | Hilbert, *Foundations of Geometry* (1899) | ✓ | German original PD; Townsend 1902 English translation PD; Project Gutenberg + archive.org |
|
||||
| 2 | Newton, *Philosophiæ Naturalis Principia Mathematica* (1687) | ✓ | Cohen-Whitman 1999 translation is **NOT** PD; use Andrew Motte 1729 (PD) |
|
||||
| 3 | Kolmogorov, *Foundations of the Theory of Probability* (1933) | ✓ | German original PD; Nathan Morrison 1956 English translation likely PD |
|
||||
| 4 | Łukasiewicz, "Two-valued logic" (1921 paper, ~30 pages) | ✓ | PD via age |
|
||||
| 5 | Mendelson, *Introduction to Mathematical Logic* (1997) | ✗ | Proprietary; Chapman & Hall/CRC. License required |
|
||||
| 6 | Enderton, *A Mathematical Introduction to Logic* (2001) | ✗ | Proprietary; Academic Press / Elsevier |
|
||||
| 7 | Aristotle, *Prior Analytics* (translated) | ✓ | The PD translations (Owen, Smith, etc.) are PD; pick a stable one |
|
||||
|
||||
Green-light scope (5/7 sources, all the foundational ones): items
|
||||
1, 2, 3, 4, 7. These cover **every pillar except the propositional-
|
||||
logic pillar** (which leans heavily on Mendelson + Enderton for
|
||||
modern axiom formulations).
|
||||
|
||||
Yellow-light scope (Mendelson + Enderton): need a separate
|
||||
go/no-go from fox. Options:
|
||||
|
||||
- **A. Buy or borrow + ingest single copy.** Possible but adds an
|
||||
ops dependency. Fox's call.
|
||||
- **B. Substitute with PD alternatives** — e.g., Hilbert &
|
||||
Ackermann 1928 *Principles of Mathematical Logic* covers the
|
||||
same ground; in PD via age. Equivalent foundation. Recommended.
|
||||
- **C. Skip the proprietary citations entirely.** Claim-pack
|
||||
records that cite Mendelson stay at `ANCHOR-WARRANTED`
|
||||
permanently. Honest but suboptimal.
|
||||
|
||||
### 2.2 Source format
|
||||
|
||||
Each textbook needs to land as one or more SURFACE Documents.
|
||||
Three format variants among PD sources:
|
||||
|
||||
- **Project Gutenberg plain text** (Hilbert PD translation,
|
||||
some Aristotle translations). Already chunkable; lightly
|
||||
formatted with chapter markers. Easiest ingest path.
|
||||
- **Scanned PDFs with OCR layer** (archive.org Newton 1729). OCR
|
||||
quality varies. Acceptable for retrieval; not great for
|
||||
verbatim quote-matching.
|
||||
- **TeX / LaTeX source** (some modern PD republications). Best
|
||||
fidelity but rare for these texts.
|
||||
|
||||
Recommended: prefer Project Gutenberg / Wikisource plain-text
|
||||
where available; fall back to archive.org OCR only when no
|
||||
clean source exists.
|
||||
|
||||
### 2.3 New Source vs reuse existing
|
||||
|
||||
Three options for the ingest pipeline:
|
||||
|
||||
**A. New `arborist/sources/textbook.py` (RECOMMENDED).**
|
||||
Document grain = one textbook = one Document (or one chapter =
|
||||
one Document for very long texts). Custom chunker for
|
||||
preserving theorem / definition boundaries (don't split a
|
||||
theorem statement across chunks if avoidable). Per-textbook
|
||||
metadata: ISBN-or-equivalent, publication year, translator,
|
||||
edition, translation-license. ~200 LOC.
|
||||
|
||||
**B. Reuse `HtmlPageSource`.** For Project Gutenberg / Wikisource
|
||||
URLs. Works but loses textbook-specific metadata and gives no
|
||||
control over chapter-level chunking.
|
||||
|
||||
**C. Reuse `WikipediaXmlDump`.** For texts that Wikipedia carries
|
||||
(unlikely for full books, common for Łukasiewicz-paper-length
|
||||
sources). Doesn't generalize.
|
||||
|
||||
→ **A** for the long-form textbooks (Hilbert, Newton,
|
||||
Kolmogorov), **B** for Łukasiewicz / Aristotle (paper-length,
|
||||
already on Wikisource).
|
||||
|
||||
### 2.4 Provenance edges
|
||||
|
||||
Once textbooks are surfaces, claim-pack records gain a real
|
||||
`Edge(edge_type='cites', dst_root=<textbook_root>)`. Today the
|
||||
claim-pack source emits only `pillar_reference` edges between
|
||||
axiom and theorem records inside the bundle. A second edge per
|
||||
record points at the textbook surface.
|
||||
|
||||
Edge resolution is two-step: (1) `source_reference` string lookup
|
||||
against a `(citation_string → textbook_root)` dictionary, built
|
||||
once when textbooks are ingested; (2) `Edge.dst_uri` set, edge
|
||||
inserted, downstream `derivations.proof_blob` row computed in a
|
||||
later ticket.
|
||||
|
||||
### 2.5 What this ticket does NOT do
|
||||
|
||||
- **Compute `derivations.proof_blob`.** That's a chunk-resolution
|
||||
problem (which span of Mendelson contains the Modus Tollens
|
||||
derivation?) and earns its own ticket.
|
||||
- **Re-ingest claim-pack records.** They stay as-is; the
|
||||
`cites` edges are added in-place to the existing rows.
|
||||
- **Solve the proprietary-textbook license problem.** Mendelson
|
||||
+ Enderton stay yellow-light pending fox's decision per §2.1.
|
||||
- **Promote the four-rung label automatically.** Even with full
|
||||
textbook ingest, the verifier still needs to see the
|
||||
`derivations.proof_blob` row in the chain. That's the next
|
||||
ticket downstream.
|
||||
|
||||
## 3. Recommendation
|
||||
|
||||
**Land the green-light scope first** — Hilbert, Newton (Motte
|
||||
1729), Kolmogorov, Łukasiewicz, Aristotle. Five PD textbooks; ~1500
|
||||
pages combined; ingestion path uses the new
|
||||
`arborist/sources/textbook.py` for the three big books and reuses
|
||||
`HtmlPageSource` for the two paper-length sources.
|
||||
|
||||
After the green-light scope lands, evaluate whether
|
||||
`ANCHOR-WARRANTED → EVIDENCE-WARRANTED` actually moves the
|
||||
audit-mode rate on a real-shard bench. If yes, tackle the
|
||||
proprietary-textbook decision. If no (e.g., the chunk-resolution
|
||||
layer for `source_reference` strings is the binding constraint),
|
||||
prioritize the chunk-resolution ticket instead.
|
||||
|
||||
## 4. Implementation sketch
|
||||
|
||||
### 4.1 New file: `arborist/sources/textbook.py`
|
||||
|
||||
```python
|
||||
class TextbookSource(Source):
|
||||
source_type = "textbook"
|
||||
|
||||
def __init__(self, manifest_path: Path):
|
||||
# manifest = JSONL of {title, author, year, translator?,
|
||||
# license, source_url, local_path,
|
||||
# chapter_split: "auto"|"manual"}
|
||||
...
|
||||
|
||||
def iter_documents(self) -> Iterator[Document]:
|
||||
# One Document per textbook (or per chapter for long texts).
|
||||
# Document.extra carries license, year, translator etc.
|
||||
...
|
||||
```
|
||||
|
||||
### 4.2 Manifest format
|
||||
|
||||
`bench/fixtures/textbooks/manifest-pd-v1.jsonl`:
|
||||
|
||||
```jsonl
|
||||
{"id":"hilbert-1899","title":"Foundations of Geometry","author":"David Hilbert","year":1899,"translator":"E. J. Townsend (1902)","license":"PD","source_url":"https://www.gutenberg.org/...","local_path":"data/textbooks/hilbert-foundations-of-geometry.txt"}
|
||||
{"id":"newton-1687","title":"Principia Mathematica","author":"Isaac Newton","year":1687,"translator":"Andrew Motte (1729)","license":"PD","source_url":"https://archive.org/...","local_path":"data/textbooks/newton-principia-motte.txt"}
|
||||
{"id":"kolmogorov-1933","title":"Foundations of the Theory of Probability","author":"Andrey Kolmogorov","year":1933,"translator":"Nathan Morrison (1956)","license":"PD","source_url":"...","local_path":"..."}
|
||||
{"id":"lukasiewicz-1921","title":"Two-valued logic","author":"Jan Łukasiewicz","year":1921,"translator":"Borkowski (Selected Works, 1970)","license":"PD","source_url":"...","local_path":"..."}
|
||||
{"id":"aristotle-prior-analytics","title":"Prior Analytics","author":"Aristotle","year":"-350","translator":"A. J. Jenkinson","license":"PD","source_url":"https://en.wikisource.org/...","local_path":"..."}
|
||||
```
|
||||
|
||||
### 4.3 Manifest fetcher (separate ticket)
|
||||
|
||||
`make fetch-textbooks` downloads the manifest's `source_url`s
|
||||
to `local_path`s. Idempotent; checksums each file post-download.
|
||||
Out of scope here; opens as a follow-up ticket.
|
||||
|
||||
### 4.4 CLI surface
|
||||
|
||||
```
|
||||
arborist ingest --source textbook --path bench/fixtures/textbooks/manifest-pd-v1.jsonl
|
||||
```
|
||||
|
||||
Reads the manifest, walks each `local_path`, ingests one Document
|
||||
per textbook (or per-chapter when the manifest entry sets
|
||||
`chapter_split: "auto"` and the file is long enough).
|
||||
|
||||
### 4.5 Edge wiring (claim-pack ↔ textbook)
|
||||
|
||||
After both sources ingest:
|
||||
|
||||
1. Build dict `(source_reference_string → textbook_document_root)`
|
||||
from every textbook Document's `extra.title` + `extra.author`.
|
||||
2. For each claim-pack Document, parse `extra.source_ref` into
|
||||
(author, title, year), look up against the dict, emit an
|
||||
`Edge(edge_type='cites', dst_root=<resolved>)`.
|
||||
3. Run a one-time `arborist concept resolve-edges` (or similar)
|
||||
to populate `edges.dst_root` from the URI lookup. Existing
|
||||
ingest already does lazy edge-fill; this ticket might extend
|
||||
it or add a one-shot pass.
|
||||
|
||||
## 5. Hard constraints (re-stated)
|
||||
|
||||
1. **No proprietary text without license.** Mendelson + Enderton
|
||||
only enter the shard with explicit fox approval and a
|
||||
documented license.
|
||||
2. **No cache_key invariant changes.** Schema, chunker,
|
||||
canonicalization versions stay pinned. Textbooks are content;
|
||||
the protocol they ride on doesn't change.
|
||||
3. **No retroactive promotion of claim-pack labels.** Audit mode
|
||||
stays computed at query time from current state of the shard.
|
||||
Adding textbooks to the shard changes future query results;
|
||||
prior `providence_cache` rows stay as they were (they were
|
||||
honest at the time they were written).
|
||||
4. **Idempotent re-ingest.** Same textbook content → same
|
||||
document_root → no-op insert. Per existing ingest contract.
|
||||
|
||||
## 6. Risks / things to watch
|
||||
|
||||
- **OCR quality.** Newton 1729 in archive.org is sometimes mangled
|
||||
("ftate" instead of "state"). Acceptable for retrieval (FTS5
|
||||
matches partial terms), poor for verbatim quote-mode
|
||||
verification. Choose source carefully; prefer cleaner editions.
|
||||
- **Translation pinning.** Kolmogorov 1933 has multiple English
|
||||
translations. The claim-pack `source_reference` doesn't pin one,
|
||||
so we have to pick. Document the choice in
|
||||
`Document.extra.translator`.
|
||||
- **Chunk-resolution gap.** Even with full textbooks ingested, the
|
||||
`source_reference` string "Mendelson 1997" doesn't tell us WHICH
|
||||
PAGE the cited theorem is on. The follow-up ticket (chunk
|
||||
resolution) is where that gets solved. This ticket only lands
|
||||
the textbooks; warrant promotion is gated on the next ticket.
|
||||
- **Storage bloat.** Five textbooks ≈ 1500 pages ≈ ~3 MB plain
|
||||
text ≈ ~6 K chunks at 512-token grain. Negligible against the
|
||||
existing Wikipedia shards. Indexing cost is modest.
|
||||
- **Claim-pack ↔ textbook citation grammar collisions.** Claim-
|
||||
pack records cite plain English ("Hilbert's Foundations of
|
||||
Geometry"); textbook `extra` carries `(author, title, year)`.
|
||||
String-distance match is workable for the green-light scope
|
||||
(5 distinct sources); breaks down at scale. Promote to a
|
||||
citation-vocab ticket if/when more textbooks land.
|
||||
|
||||
## 7. Forward links
|
||||
|
||||
- **#000029** — claim-pack source. This ticket is its direct
|
||||
warrant-promotion follow-up.
|
||||
- **Future ticket — chunk resolution layer.** Maps
|
||||
`source_reference` strings to specific chunks within ingested
|
||||
textbooks. The bridge that lets `derivations.proof_blob` be
|
||||
computed.
|
||||
- **Future ticket — `make fetch-textbooks` pipeline.** Idempotent
|
||||
fetch + checksum of the PD textbook corpus.
|
||||
- **#000028 multi-modality witness** — STRICT-WITNESSED status
|
||||
for logic claims becomes reachable when claim-pack records earn
|
||||
EVIDENCE-WARRANTED via this chain.
|
||||
|
||||
## 8. Status
|
||||
|
||||
Open · awaiting go/no-go.
|
||||
|
||||
Estimated size:
|
||||
|
||||
- Phase 1 — green-light textbook ingest (PD only): ~250 LOC for
|
||||
`TextbookSource` + ~50 LOC manifest + tests + small data files.
|
||||
Plus ~3 MB of textbook plain-text data (not committed; downloaded
|
||||
via fetcher).
|
||||
- Phase 2 — Mendelson/Enderton license decision + ingest if
|
||||
green-lit: design pending.
|
||||
- Phase 3 — chunk-resolution layer: separate ticket entirely.
|
||||
146
tests/test_pi_star_algebra_symbolic_simplified.py
Normal file
146
tests/test_pi_star_algebra_symbolic_simplified.py
Normal file
|
|
@ -0,0 +1,146 @@
|
|||
"""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")
|
||||
216
tests/test_pi_star_calculus_integral.py
Normal file
216
tests/test_pi_star_calculus_integral.py
Normal file
|
|
@ -0,0 +1,216 @@
|
|||
"""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
|
||||
Loading…
Add table
Add a link
Reference in a new issue