= Solution
On two finite total <lists>, the equations agree. If either <list> is empty they return the other; if both have heads, expanding `twiddle` twice gives `x : y : twiddle xs ys`, exactly the third equation for `twiddle'`. The same finite-prefix reasoning proves agreement on infinite inputs with defined spines.
They differ on <partial lists>. Take the first argument `[1]` and the second argument $\bot$. The original definition can emit its first head immediately:
$$
\operatorname{twiddle}\ [1]\ \bot
=1:\operatorname{twiddle}\ \bot\ []
=1:\bot.
$$
After recognizing the nonempty first argument, `twiddle'` must inspect the second argument to distinguish its second and third equations. That inspection diverges, so
$$
\operatorname{twiddle}'\ [1]\ \bot=\bot,\qquad
\boxed{\operatorname{twiddle}'\ne\operatorname{twiddle}.}
$$
For example, demanding only the head distinguishes them: the original returns `1`, while the primed version diverges. Equality of <functions> under <lazy evaluation> requires agreement on these partial inputs too.
Back to article page
