haskell - 数学公式 : parsing and canonical *programming* form

Question

是否有任何常规范式来表示可以被计算机读取的数学公式？

我正在研究一些数学问题，并有某种 TDD 方法来解决它。每次我陷入一个证明(或者只是我还没有证明，但是对结果应该是什么的一些直觉)时，我倾向于编写一个小程序来检查到目前为止一切都像我认为的那样表现.我通常在我的证明中为一些中间结果编写一个 Haskell 函数，通过 GHCi 玩它直到我确信我仍在朝着正确的方向前进。

我的绝对理想是为数学公式提供一些规范形式，我可以使用某种工具将其输出到 LaTeX 和 Haskell。我可以在它上面运行 QuickTest，如果一个步骤错了，它会告诉我。 LaTeX 的数学符号实际上非常接近于规范形式，尽管很多是由读者推断出来的(你不想明确地写出 每个 括号)。

这个理想的工具似乎好得令人难以置信；相反，为计算机拼出数学公式的正确方法是什么，可能还会对其进行解析？环顾四周，我看到了很多仅使用 * 的简单公式。 , + , - , /之类的。没有什么包含像总和(例如集合)、导数、所有“很酷”的东西。而且，这种解析器的输出大多用于计算结果，为变量提供一些值；不是为了将它翻译成其他语言(我猜是语言不可知论者)。看起来像这样的东西应该已经存在，或者应该有一个很好的理由为什么不存在。我错过了哪一个？

Answer 1

数学符号的标准计算机表示是 MathML .请注意，它包括 Presentation MathML ，表示数学表达式的书写方式，可以是 converted to LaTeX , 和 Content MathML它旨在表示表达式的含义，并且是您将其翻译为 Haskell 或其他编程语言所需的内容(但我不知道有任何工具可以进行此类翻译)。

当然，您不想手动编写(任何一种)MathML；有一些编辑制作它，但我不能推荐一个。

否则，OpenMath可能是一个选择。它似乎完全面向“在计算机上使用数学”的人。