[Haskell-cafe] Re: Equational Reasoning goes wrong

[apfelmus]

Neil Mitchell wrote:
> Haskell is known for its power at equational reasoning - being able to
> treat a program like a set of theorems. For example:
> 
> break g = span (not . g)
> 
> Which means we can replace:
> 
> f = span (not . g)
> 
> with:
> 
> f = break g
> 
> by doing the opposite of inlining, and we still have a valid program.
> 
> However, if we use the rule that "anywhere we encounter span (not . g)
> we can replace it with break g" then we can redefine break as:
> 
> break g = break g
> 
> Clearly this went wrong! Is the folding back rule true in general,
> only in specific cases, or only modulo termination?

Well, from the equational point of view, the equation

  break p = break p

is trivially valid, so nothing is wrong with equational reasoning. Of
course, the definitions

  break p := span (not . p)

and

  break p := break p

are clearly different, since the latter implies  break p = _|_ . It
seems that "de-inlining" can make things less defined. But I think that
this phenomenon is an artifact of working with named functions, similar
to name capture. I guess it's not present for anonymous lambda terms.

Regards,
apfelmus