如何在Python中使用Z3找到拉格朗日插值多项式？

Question

我正在用Z3库和Python语言学习数学，但我不知道怎么根据拉格朗日插值多项式找到一个多项式。

I have
f(0) = y0
f(1) = y1
f(2) = y2
....

我想找到f(X)。

我在使用Scipy时一切都很好，但换到Z3库后，找不到更多的文档了，真让人沮丧 :(

Answer 1

我不知道如何在Z3的上下文中回答你的问题。Z3并没有内置的拉格朗日插值求解器。你可以设置一个多项式方程组，其中的系数保持为符号形式。然后你可以问Z3这个方程组是否有解。通常情况下，它会给出系数的代数数值，所以我不太确定这是否适合你的应用。

当然，在Python中你可以这样写：

a, b, c = Real('a b c')
def f(X):
    return a*X*X + b*X + c

solve(f(0) == y0, f(1) == y1, f(2) == y2)

其中y0、y1、y2是常量。