数学公式:解析和规范*编程*形式

Question

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

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

我绝对的理想是有一些规范形式的数学公式，我可以使用一些工具，都输出到LaTeX和Haskell。我可以在上面运行QuickTest，如果步错了，它就会告诉我。LaTeX的数学符号实际上非常接近规范形式，尽管读者可以推断出很多(您不想显式地编写每个括号)。

这个理想的工具似乎太好了，不可能是真的；相反，怎样才是正确的方法来为计算机列出一个数学公式，可能也会解析它呢？在环顾四周的时候，我看到了很多简单的公式，它们只使用*、+、-、/等等。什么都不包括和(例如集合上)，导数，所有“酷”的东西。此外，此类解析器的输出主要用于计算结果，给出变量的一些值，而不是将其翻译成其他语言(我猜，语言不可知论)。似乎这样的东西应该已经存在了，或者应该有一个很好的理由不存在。我错过了哪一个？

Answer 1

数学表示法的标准计算机表示是MathML。请注意，它包括表示MathML (表示数学表达式的编写方式并可以是转换为LaTeX )和内容MathML (用于表示表达式的含义)，这是将表达式翻译到Haskell或另一种编程语言所需要的(但我不知道有任何工具可以进行这种转换)。

当然，您不想手动编写(两种风格的) MathML；有一些编辑器可以生成它，但我不能推荐。

否则，OpenMath可能是一种选择。它似乎正是面向“在计算机上与数学打交道”的人。