Editing Correctness of short cut fusion (section)

====<hask>destroy</hask>/<hask>unfoldr</hask>====

The <hask>destroy</hask>/<hask>unfoldr</hask>-rule, however, is not a semantic equivalence.
To see this, consider the following instance:

<haskell>
g = \x y -> case x y of Just z -> 0
p = \x -> if x==0 then Just undefined else Nothing
e = 0
</haskell>

These values have appropriate types for being used in the <hask>destroy</hask>/<hask>unfoldr</hask>-rule. But with them, that rule's left-hand side "evaluates" as follows:

<haskell>
destroy g (unfoldr p e) = g step (unfoldr p e)
                        = case step (unfoldr p e) of Just z -> 0
                        = case step (case p e of Nothing     -> []
                                                 Just (x,e') -> x:unfoldr p e') of Just z -> 0
                        = case step (case Just undefined of Nothing     -> []
                                                            Just (x,e') -> x:unfoldr p e') of Just z -> 0
                        = undefined
</haskell>

while its right-hand side "evaluates" as follows:

<haskell>
g p e = case p e of Just z -> 0
      = case Just undefined of Just z -> 0
      = 0
</haskell>

Thus, by applying the <hask>destroy</hask>/<hask>unfoldr</hask>-rule, a nonterminating (or otherwise failing) program can be transformed into a safely terminating one.
The obvious questions now are:

# Can the converse also happen, that is, can a safely terminating program be transformed into a failing one?
# Can a safely terminating program be transformed into another safely terminating one that gives a different value as result?

There is no formal proof yet, but strong evidence supporting the conjecture that the answer to both questions is "'''No!'''".

The conjecture goes that if <hask>g</hask> does not use <hask>seq</hask>, then the <hask>destroy</hask>/<hask>unfoldr</hask>-rule is a semantic approximation from left to right, that is, it holds that

<haskell>
destroy g (unfoldr p e) ⊑ g p e
</haskell>

What ''is'' known is that semantic equivalence can be recovered here by putting moderate restrictions on p.
More precisely, if <hask>g</hask> does not use <hask>seq</hask> and <hask>p</hask> is a strict function that never returns <hask>Just ⊥</hask> (where ⊥ denotes any kind of failure or nontermination), then indeed:

<haskell>
destroy g (unfoldr p e) = g p e
</haskell>