Как я могу убедить Sympy прийти к тому же упрощению, которое SAINT делает для задачи по математическому анализу MIT 1961 года?

Программа для тезиса Джеймса Р. Слэгла в Массачусетском технологическом институте Эвристическая программа, которая решает проблемы символьного интегрирования в исчислении для первокурсников, символьный автоматический интегратор (SAINT) известна (иш) тем, что является первый практический символьный интегратор экспертной системы, способный решить все проблемы теста MIT Undergraduate Calculus (педантично, пару пропустили, но он мог бы их решить; подробности здесь в этом отличном видео на YouTube)

Его диссертация находится в свободном доступе здесь: https://dspace.mit.edu/handle/1721.1/11997

Я был рад попробовать Sympy на этом, потому что это выглядело доступным и было достаточно сложным упрощением, на которое у меня уже был ответ ... однако Sympy не упрощает интеграл до такого хорошего (субъективного?) Упрощения, как программа 1961 года. (хотя он возвращает эквивалентный результат!)

Вопросы и предположения

Как я могу убедить Sympy упростить то же уравнение?
Почему это не приводит к тому же, казалось бы, более простому результату?

Может быть, он выбирает первый возможный исход, или tan**3 определено, что он будет хуже? если да, то почему это не упрощает вывод SAINT?)

Возможно, он откроет другую ветку, когда найдет подходящую подпрограмму Fu?

Экзаменационная задача 3c

Симпийное упрощение

from sympy import *
x = symbols("x", real=True)  # should this be assumed?
expr_inner = (x**4) / ((1 - x**2)**Rational(5,2))
expr_integral = integrate((expr_inner), x)
print(simplify(expr_integral))

(x**4*asin(x) + 4*x**3*sqrt(1 - x**2)/3 - 2*x**2*asin(x) - x*sqrt(1 - x**2) + asin(x))/(x**4 - 2*x**2 + 1)

Доказательство равенства

from sympy import *
x = symbols("x", real=True)  # should this be assumed?
expr_saint = asin(x) + Rational(1,3)*tan(asin(x))**3 - tan(asin(x))
expr_sympy = (x**4*asin(x) + 4*x**3*sqrt(1 - x**2)/3 - 2*x**2*asin(x) - x*sqrt(1 - x**2) + asin(x))/(x**4 - 2*x**2 + 1)
expr_saint.equals(expr_sympy)  # alternatively simplify(expr_saint - expr_sympy) https://stackoverflow.com/a/37115190/

True

Отображение уравнений

sympy equation simplification

ti7 10.01.2021 источник

Ответы (2)

arrow_upward
1
arrow_downward

Основная часть - это вычленение asin(x) и отделение его от дроби. После этого sympy может доказать, что эти два выражения равны:

from sympy import *
from IPython.display import Math, display
x = symbols("x", real=True)  # should this be assumed?
expr_saint = asin(x) + Rational(1,3)*tan(asin(x))**3 - tan(asin(x))
expr_sympy = (x**4*asin(x) + 4*x**3*sqrt(1 - x**2)/3 - 2*x**2*asin(x) - x*sqrt(1 - x**2) + asin(x))/(x**4 - 2*x**2 + 1)

r=[]
r.append(latex(expr_sympy))
expr_sympy = expr_sympy.collect(asin(x))
r.append(latex(expr_sympy))
expr_sympy = apart(expr_sympy,asin(x))
r.append(latex(expr_sympy))

display(Math(" \\Longrightarrow ".join(r)))

display(simplify(expr_saint - expr_sympy))

Выход:

wsdookadr 10.01.2021

arrow_upward
1
arrow_downward

@wsdookadr дал мне пропущенный шаг упрощения; показывая apart(), можно легко получить asin(x) (что, очевидно, является обычным фактором) сам по себе, и таким образом создать очень похожую, но более упрощенную форму, чем результат SAINT.

Если подумать больше в этом направлении, вывод SAINT не так упрощен, как мог бы, и поэтому его следует дополнительно упростить перед сравнением (насколько мне известно, SAINT не был разработан для дальнейшего упрощения после интеграции)

сначала приведение результата к единственной дроби с помощью ratsimp() подталкивает Sympy чтобы очистить знаменатель (это объединяет дроби)
вызов apart() разделяет их на части, хотя они остаются упрощенными

Это дает более ожидаемое совпадение

ti7 11.01.2021