haskell - 等式推理的名称从何而来？

Question

我知道equational reasoning是不是在任何情况下都可以用其他代码替换，但我真的很好奇“等式推理”的名称从何而来？我用谷歌搜索了它，但找不到任何相关的答案。

Answer 1

它实际上并不是一个真正的名字，只是一个通过重复使用而变得标准化的描述。 “等式推理”就是“等式”的推理；即它涉及方程。

所涉及的想法是这一系列的重写:

fmap even . fmap (+1)
fmap (even . (+1))
fmap (\x -> even (x +1))
fmap odd

涉及与这一系列重写相同的思考:

(x + 1)(x - 1)
x^2 + x - x - 1
x^2 - 1

在这两种情况下，您都在使用像 fmap f . fmap g = fmap (f . g) 这样的方程。或 (a + b)(c + d) = ac + ad + bc + bd您知道的一般情况下，并使用它们将您的术语转换为可证明等效的术语。方程式是关键，之前已证明其成立(理想情况下由其他人;))。