如何实现一个触发身份证明算法

Question

我怎么能实现一个程序，它需要在trig方程的两边（可以推广到任何东西，但现在我将它留在只是触发身份），程序将输出将一方转换为另一方（或转换它们）的步骤，以表明它们实际上是平等的。该计划将首先假设他们是平等的。我非常难以理解如何实现一个算法来做到这一点。我的第一个想法是与图形有关，但我想不到除此之外的任何事情。从那里，我认为我应该首先将方程的两边解析为树。例如(cot x * sin)/(sin x + cos x)应该是这样的：

 division 
    / \ 
    *  + 
/\ /\ 
cot sin sin cos 

在此之后，我有两个类似的想法，这两者都有问题。第一个想法是挑选叶子数量最少的一面，并尝试通过使用“树型正则表达式”表示的等价性将其操作到另一端。这些“树型正则表达式”的例子将是csc = 1/sin或cot = cos/sin（当然是树形式）等等。我的第二个想法是挑选更多叶子的一面，并试图找到一些表达式，当乘以该表达式将等于另一个表达式侧。使用倒数这不会太糟糕，但是，我将不得不证明我乘以的东西等于1.我又回到了这个“树正规表达式”的东西。

这两个问题的主要缺陷是按什么顺序/我如何应用这些替换。它会不会是一个大混乱的if语句，还是有一个更优雅的解决方案？实际上是否有一种我没有看到的基于图形的解决方案。 什么（如果有的话）可能是证明触发身份的好算法。

需要明确的是，我不是在谈论“解决X”型问题，如tan(x)sin(x) = 5，求x的所有值，而是证明sqrt((1 + sin x)/(1 - sin x)) = sec x + tan x

Answer 1

看看计算机代数（我没有）的文本，我敢肯定你会在那里找到聪明的想法。

我的方法是基于图的搜索，因为我怀疑转换的线性应用将可靠地导致解决方案。

按照您已经开始的方式将整个方程表达为表达式树，但包括上面的“equals”节点。

对于搜索图视图，将一个表达式树作为一个搜索状态。搜索目标是一个可判定的表达式树，如1 = 1或1 = 0。当搜索时（扩展搜索状态），通过在你的表达式上应用等价变换来创建子状态（类似于正则表达式的声音对我而言很合理）。定义一个计算表达式总体复杂度的评估函数（例如，表达式树中的节点数）。做一个定向搜索，最小化评估函数（首先扩展最低复杂度的表达式），从而简化表达式，直到达到可决定的形式。

根据表达式，很有可能不受限制的搜索永远不会终止。我不知道你会如何处理这个问题，也许可以通过将表达式允许的复杂度限制在原来的几倍。这样可以减少无限期运行的风险，但给你留下未确定的情况。

Answer 2

这是决定三角恒等式，可以简单的算法被带进形式polynomial(sin x, cos x) = 0：

1. 摆脱tan x，cot x，sec x，...，sin 2x，...利用的明显替换（tan x -> (sin x)/(cos x)，... sin 2x -> 2 (sin x) (cos x)，...）

2. 变换身份的平方（隔离）根（标识中摆脱重根的多项式可能会非常棘手，虽然），与分母扩大所有条款乘以使一侧

3. 用1 - sin^2 x替换多项式（cos^3 x = (cos^2 x)(cos x),cos^4 x = (cos^2 x)(cos^2 x)，...）中的所有项cos^2 x并展开多项式。

4. 最后计算一个没有cos^2 x的多项式。如果它与0相同，则证明身份，否则身份不成立。

你的榜样sqrt((1 + sin x)/(1 - sin x)) = sec x + tan x：

1. 使用替代sec x -> 1/(cos x)和tan x -> (sin x)/(cos x)我们得到

sqrt((1 + sin x)/(1 - sin x)) = 1/(cos x) + (sin x)/(cos x)。

为了简洁，让我们写出s代替sin x和c代替cos x，这使我们：

sqrt((1 + s)/(1 - s)) = 1/c + s/c

平方方程和乘以两侧(1 - s)c^2我们得到

(1 + s)c^2 = (1 + s)^2(1 - s)。

扩大括号并且使寄托都向一侧，我们得到

c^2 - sc^2 + s^3 + s^2 - s - 1 = 0

代c^2 = 1 - s^2成多项式，我们得到

(1 - s^2) - s(1 - s^2) + s^3 + s^2 - s - 1它将扩展为0。

1. 因此，身份证明。