[Haskell-cafe] Equational Reasoning goes wrong

[Claus Reinke]

> Haskell is known for its power at equational reasoning - being able 
> to treat a program like a set of theorems. 

when you're trying to do equational reasoning, you better make
sure that you're reasoning with equations. as others have pointed
out some of the more interesting relations between programs are
inequations, where one side is defined in all cases in which the 
other is, and both sides are equal whenever both are defined.

the interesting bit here is that the equation you're trying to use is
also part of the program in which you're going to use it (unlike flat
sets of theorems), and if you apply the equation to parts of itself, 
you might change it. by sawing off the branch of logic you're 
working from, you might then find yourself suspended in mid air.

at the point of definition for an equation 'lhs = rhs', we have an 
inequation: lhs is not yet defined, rhs presumably is, and then we 
declare them to be equivalent, so that lhs is defined whenever
rhs is, and both have equal values whenever both are defined.

in other words, as long as/whereever our new definition holds, 
we can use it as an equation, whereas we only have an 
inequation if we start fiddling with the definition itself.

if we replace lhs with rhs in the definition (making the left hand
side "more defined"), we get something valid (semantically, 
though not necessarily syntactically) but useless - a tautology 
that only "defines" what already was.

if we replace rhs with lhs in the definition (making the right hand
side "less defined"), we get another valid but useless equation - 
a tautology that does not add any information to help make a 
useful new definition. [this is the variant that loops, making no
progress towards producing information]
 
if our definition is recursive, and we replace an occurrence
of lhs in rhs with an instance of rhs, we have not changed
the information content of the definition.

a very useful group of transformations in non-strict languages
(when you want to make your code less strict, eg in cyclic
programming) are the eta-expansions: 

    f --> \x.(f x)              -- f is a function
    p --> (fst p,snd p)     -- p is a pair
    l --> (head l:tail l)     -- l is a list
    ..

all of which add information by "borrowing from the future" -
if f,p,l turn out to be defined, the above are equations, 
otherwise they are inequations, the rhs being more defined 
than the lhs (because the future payback never happens).

in particular:

    Prelude> let x = x
    Prelude> :t x
    x :: t

    Prelude> let r = (\y->x y,(fst x,snd x),(head x:tail x))
    Prelude> :t r
    r :: (t -> t1, (a, b), [a1])

    Prelude> let f (a,(_,_),(_:_)) = a `seq` ()
    Prelude> :t f
    f :: (t, (t1, t2), [t3]) -> ()

    Prelude> f r
    ()

while 

    Prelude> f (x,x,x)
    Interrupted.

well, at least that is my naive way of looking at these things;-)

claus