048 sym decide integral

✓ Passing This code compiles and runs correctly.

Code

import std/io
import std/sym

// elementary: polynomial integrand -> constructed antiderivative
std/sym:lit(((2e0*x)+3e0))
| exact a |> std/sym:decide-integral(a, max-order: 3, max-deg: 3)
    | elementary m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unresolved m |> std/io:print.ln("un:{{ m:s }}")
    | not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
    | non-rational |> std/io:print.ln("nr")
    | non-analytic |> std/io:print.ln("na")
    | bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")

// holonomic-special via structural cert: 1/(1-x) -> -h1 + (1-x) h2 = 0
std/sym:lit(inv((1e0+(-1e0*x))))
| exact a |> std/sym:decide-integral(a, max-order: 3, max-deg: 3)
    | elementary m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unresolved m |> std/io:print.ln("un:{{ m:s }}")
    | not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
    | non-rational |> std/io:print.ln("nr")
    | non-analytic |> std/io:print.ln("na")
    | bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")

// holonomic-special via discovery fallback: (1+x)^(1/4)
std/sym:lit(√(√((1e0+x))))
| exact a |> std/sym:decide-integral(a, max-order: 3, max-deg: 3)
    | elementary m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unresolved m |> std/io:print.ln("un:{{ m:s }}")
    | not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
    | non-rational |> std/io:print.ln("nr")
    | non-analytic |> std/io:print.ln("na")
    | bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")

// unresolved: same integrand, bounds too tight — named bound recorded
std/sym:lit(√(√((1e0+x))))
| exact a |> std/sym:decide-integral(a, max-order: 0, max-deg: 0)
    | elementary m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unresolved m |> std/io:print.ln("un:{{ m:s }}")
    | not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
    | non-rational |> std/io:print.ln("nr")
    | non-analytic |> std/io:print.ln("na")
    | bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")

// decide-ode: y2 = 2y -> liouvillian exp form
std/sym:lit(2e0)
| exact r |> std/sym:decide-ode(r)
    | liouvillian m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unclassifiable m |> std/io:print.ln("uc:{{ m:s }}")
    | bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")

// decide-ode: y2 = -y -> liouvillian trig form
std/sym:lit((-1e0))
| exact r |> std/sym:decide-ode(r)
    | liouvillian m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unclassifiable m |> std/io:print.ln("uc:{{ m:s }}")
    | bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")

// decide-ode: y2 = x*y (Airy) -> unbounded -> holonomic-special
std/sym:lit((x))
| exact r |> std/sym:decide-ode(r)
    | liouvillian m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unclassifiable m |> std/io:print.ln("uc:{{ m:s }}")
    | bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")

// decide-ode: y2 = y/x -> pole at 0 -> unbounded -> holonomic-special
std/sym:lit(inv(x))
| exact r |> std/sym:decide-ode(r)
    | liouvillian m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unclassifiable m |> std/io:print.ln("uc:{{ m:s }}")
    | bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")

// decide-ode: y2 = sqrt(x)*y -> r not rational -> unclassifiable
std/sym:lit(√(x))
| exact r |> std/sym:decide-ode(r)
    | liouvillian m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unclassifiable m |> std/io:print.ln("uc:{{ m:s }}")
    | bad m |> std/io:print.ln("bad:{{ m:s }}")
| bad |> std/io:print.ln("bad-lit")

// decide-field: extract antiderivative cert for registry composition
std/sym:lit(inv((1e0+(-1e0*x))))
| exact a |> std/sym:decide-integral(a, max-order: 3, max-deg: 3)
    | elementary m |> std/io:print.ln("{{ m:s }}")
    | holonomic-special m |> std/sym:decide-field(blob: m, name: "antiderivative")
        | exact c |> std/io:print.ln("{{ c:s }}")
        | not-found |> std/io:print.ln("field-nf")
    | unresolved m |> std/io:print.ln("un:{{ m:s }}")
    | not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
    | non-rational |> std/io:print.ln("nr")
    | non-analytic |> std/io:print.ln("na")
    | bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")

// decide-field: absent field name -> not-found
std/sym:lit(((2e0*x)+3e0))
| exact a |> std/sym:decide-integral(a, max-order: 3, max-deg: 3)
    | elementary m |> std/sym:decide-field(blob: m, name: "antiderivative")
        | exact c |> std/io:print.ln("{{ c:s }}")
        | not-found |> std/io:print.ln("field-nf")
    | holonomic-special m |> std/io:print.ln("hs:{{ m:s }}")
    | unresolved m |> std/io:print.ln("un:{{ m:s }}")
    | not-holonomic m |> std/io:print.ln("nh:{{ m:s }}")
    | non-rational |> std/io:print.ln("nr")
    | non-analytic |> std/io:print.ln("na")
    | bad |> std/io:print.ln("bad")
| bad |> std/io:print.ln("bad-lit")

input.k

Actual

decide(layer=elementary)|integral=[0,3,1]|note=polynomial-termwise-constructed
hs:decide(layer=holonomic-special)|note=no-risch-elementary-form-not-constructed;integrand-cert-theorem-grade|integrand=ode(k=1,d=1,via=of)|p0=[-1]|p1=[1,-1]|antiderivative=ode(k=2,d=1,via=shift)|p0=[0]|p1=[-1]|p2=[1,-1]
hs:decide(layer=holonomic-special)|note=no-risch-elementary-form-not-constructed;seed-finite-witness|integrand=ode(k=1,d=1,via=verified)|p0=[-1,0]|p1=[4,4]|antiderivative=ode(k=2,d=1,via=shift)|p0=[0]|p1=[-1,0]|p2=[4,4]
un:decide(layer=unresolved)|note=no-holonomic-certificate-within-bounds(order<=0,deg<=0);structural=sqrt-nonpoly
decide(layer=liouvillian)|r=2|form=y=C1*exp(sqrt(r)*x)+C2*exp(-sqrt(r)*x)|note=kovacic-check-bounded
decide(layer=liouvillian)|r=-1|form=y=C1*cos(sqrt(|r|)*x)+C2*sin(sqrt(|r|)*x)|note=kovacic-check-bounded
hs:decide(layer=holonomic-special)|note=kovacic-pole-structure-unbounded:proven-no-liouvillian-solution
hs:decide(layer=holonomic-special)|note=kovacic-pole-structure-unbounded:proven-no-liouvillian-solution
uc:r-not-rational-function
ode(k=2,d=1,via=shift)|p0=[0]|p1=[-1]|p2=[1,-1]
field-nf

Expected output

decide(layer=elementary)|integral=[0,3,1]|note=polynomial-termwise-constructed
hs:decide(layer=holonomic-special)|note=no-risch-elementary-form-not-constructed;integrand-cert-theorem-grade|integrand=ode(k=1,d=1,via=of)|p0=[-1]|p1=[1,-1]|antiderivative=ode(k=2,d=1,via=shift)|p0=[0]|p1=[-1]|p2=[1,-1]
hs:decide(layer=holonomic-special)|note=no-risch-elementary-form-not-constructed;seed-finite-witness|integrand=ode(k=1,d=1,via=verified)|p0=[-1,0]|p1=[4,4]|antiderivative=ode(k=2,d=1,via=shift)|p0=[0]|p1=[-1,0]|p2=[4,4]
un:decide(layer=unresolved)|note=no-holonomic-certificate-within-bounds(order<=0,deg<=0);structural=sqrt-nonpoly
decide(layer=liouvillian)|r=2|form=y=C1*exp(sqrt(r)*x)+C2*exp(-sqrt(r)*x)|note=kovacic-check-bounded
decide(layer=liouvillian)|r=-1|form=y=C1*cos(sqrt(|r|)*x)+C2*sin(sqrt(|r|)*x)|note=kovacic-check-bounded
hs:decide(layer=holonomic-special)|note=kovacic-pole-structure-unbounded:proven-no-liouvillian-solution
hs:decide(layer=holonomic-special)|note=kovacic-pole-structure-unbounded:proven-no-liouvillian-solution
uc:r-not-rational-function
ode(k=2,d=1,via=shift)|p0=[0]|p1=[-1]|p2=[1,-1]
field-nf

048 sym decide integral

Code

Actual

Expected output

Flows

Test Configuration