Where does the name of Equational Reasoning come from?

Question

I know equational reasoning is that pieces of code can be replaced by others in any context, but am really curious where does the name of "equational reasoning" come from? I have googled it but could not find any relevant answer.

Answer 1

It's actually not really a name, just a description that has become standardised through repeated use. "Equational reasoning" is just reasoning that is "equational"; i.e it involves equations.

The idea involved is that this series of rewrites:

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

Involves the same kind of thinking as this series of rewrites:

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

In both cases you're using equations like fmap f . fmap g = fmap (f . g) or (a + b)(c + d) = ac + ad + bc + bd that you know hold in general, and using them to transform your terms to ones that are provably equivalent. The equations are the key, which are previously proven to hold (ideally by someone else ;) ).