数学公式：解析和规范*编程*形式答案

【问题标题】：Mathematical formulas: parsing and canonical *programming* form数学公式：解析和规范*编程*形式
【发布时间】：2015-07-31 11:14:39
【问题描述】：

是否有任何传统的格式来表示计算机可以读取的数学公式？

我正在研究一些数学问题，并且有某种 TDD 方法来解决它。每次我陷入证明中（或者只是我还没有证明，但对结果应该有一些直觉）时，我倾向于编写一个小程序来检查到目前为止的所有行为是否符合我的想法.我通常为我的证明中的一些中间结果编写一个 Haskell 函数，通过GHCi 使用它，直到我确信我仍然朝着正确的方向前进。

我的绝对理想是拥有一些数学公式的规范形式，我可以使用一些工具将其输出到 LaTeX 和 Haskell。我可以在上面运行 QuickTest，如果某个步骤有误，它会告诉我。 LaTeX 的数学符号实际上非常接近规范形式，尽管很多内容是由读者推断出来的（你不想明确写出 every 括号）。

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

【问题讨论】：

github.com/leftaroundabout/Symbolic-math-HaTeX。它还没有真正完成，我已经有一段时间没有工作了，但它证明了“输出到 LaTeX 和 Haskell”并不是那么牵强：将公式写成或多或少的普通 Haskell 代码，然后让 @987654327 @eDSL monad 从中生成 LaTeX 代码。
这方面有很多先前的工作，请参阅 Maple 或 Mathematica 或 Sage 或许多其他计算机代数系统。这些涵盖了您有兴趣探索的部分领域。但我认为你应该放弃它们是一种真正的规范形式的想法——我的记忆变得模糊了，但我记得有一个数理逻辑的基本定理，没有也不能是单一的规范形式表示系统的任何表达式，例如数学。想想x^2-1 vs (x+1)(x-1).
@HighPerformanceMark 感谢您的意见。你用f1(x) = x^2-1 和f2(x) = (x+1)(x-1) 指出的不是问题，恰恰相反：一旦你把它们都用自己的canonical 形式拼写出来，你就可以检查f1而f2 实际上为任何x 输出相同的结果。关于Mathematica之类的东西我自己的记忆越来越模糊，所以是时候复习了。
@leftaroundabout 我喜欢 HaTeX 和您的项目背后的想法（实际上我最近开始研究 Ruby 等价物）。我认为您的评论绝对可以被视为（至少部分）答案。
@NicolasMattia：好吧，让我们先看看是否有人有一个完整的答案！

标签： haskell math tex

【解决方案1】：

数学符号的标准计算机表示是MathML。请注意，它包括Presentation MathML，它表示数学表达式的编写方式，可以是converted to LaTeX，和Content MathML，它旨在表示表达式的含义，是你想要的需要翻译成 Haskell 或其他编程语言（但我不知道有任何工具可以进行这种翻译）。

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

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

【讨论】：

只是没有人在发现后感到失望：MathML 中的 ML 与 ML 无关，而是与 XML。
内容 MathML 非常有趣。在阅读它时，我还遇到了 OpenMath，它似乎范围更大。我会继续寻找，看看是否存在这样的翻译工具；否则我想是时候写一篇了。
@NicolasMattia 我认为您的编辑应该是一个单独的答案；你被允许回答你自己的问题。