Equational Reasoning的名字来自哪里？

Question

我知道等式推理(https://wiki.haskell.org/Equational_reasoning_examples#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您知道的方程式一般,并使用它们将您的术语转换为可证明等效的术语.该公式是关键,这是以前被证明持有(最好由别人;)).