方程式可以在运行时期间构建为AST树,字符串或其他格式.
方程式主要是简单的代数方程式,对未知函数有一些假设.域,将是整数算术(没有浮点问题,因为相关问题是众所周知的 – 感谢@hardmath强调它,我认为它是已知的).
示例：输入可能包含函数phi,假设它(大多数情况下)phi(x,y)= phi(y,x)并尝试求解：
equality_test(phi((a 1)*(a 1),a b)= phi(b a,a * a 2a 1)
它可以是模糊的或任何相等的测试 – 我的意思是,它不必总是成功(即使方程式相等,它也可能返回“假”).
如果支持上述关于phi函数的假设存在问题,我可以处理这个问题,所以也欢迎简单的线性代数方程等式测试人员.
>你能推荐一些C/C++编程库或Unix工具吗？ (开源)
>如果可能的话,您能否附上一些示例,如何在给定的库/工具中进行这样的相等测试？
附：如果这样的equality_test可以(在成功的情况下)返回同构 – (我的意思是,一种“映射”) – 在两个给定的方程之间,将非常受欢迎.但是,没有这种功能的工具也非常受欢迎.
附：通过“模糊测试器”,我的意思是在内部方程求解器在寻找两个函数的“同构”方面将是“模糊的”,而不是在对随机输入的测试方面 – 我可以实现这一点,当然,但我试图找到更精确的东西.
P.P.S.还有另一个问题,为什么我需要更好的性能解决方案,而不是蛮力的“所有输入测试”.上面的等式是我内部问题的简单形式,我没有方程中的变量之间的映射.也就是说,我有eq1 = phi((a 1)*(a 1),ab)和eq2 = phi(lk,k * k 2k 1),我必须找出a == k和b ==湖但是这个子问题我可以用“暴力”方法处理(甚至这种方法的渐近复杂性),只有几个变量,让它为8.所以我需要为每个可能的映射做这个equation_test.如果有一个工具可以完成整个工作,我会非常感激,并且可以为这样的项目做出贡献.但我不需要这样的功能,只需通过equation_test()即可,我可以轻松处理休息.
把它们加起来：
> equality_test()只是我必须解决的许多子问题之一,因此计算复杂性很重要.
>它不一定是100％可靠,但更高的可能性,而不仅仅是测试具有一些随机输入和变量映射的方程式非常受欢迎:).
>输出“是”或“否”(所有其他信息可能有用,但将来,在此阶段我需要“是”/“否”)
解决方法
处理方程的抽象主题将是数学家称之为varieties的理论.这些理论在其模型的存在性和规律性方面具有很好的性质.
你可能会想到专门处理实数或其他系统的方程式,这会为寻求证据的理论增加一些公理.
如果原则上存在一种算法来确定逻辑陈述是否可以在理论中得到证实,那么该理论就被称为可判定的.例如,正如Tarski在1951年所展示的那样,the theory of real closed fields是可判定的.然而,这种算法的实际实现是缺乏的,也许是不可能的.
以下是一些开源软件包,可能值得学习如何指导您的设计和开发：
Tac: A generic and adaptable interactive theorem prover
Prover9: An automated theorem prover for first-order and equational logic
