[Haskell-cafe] Unfold fusion
dan.doel at gmail.com
Wed May 6 17:20:22 EDT 2009
On Wednesday 06 May 2009 4:26:15 pm Dan Doel wrote:
> unfortunately it looks like I'm doing something wrong in that "coinductive
Sorry about the self-reply, but I realized where I went wrong. The principle
of proof by coinduction for defining a function 'f' goes something like this
(expressed all point-free like):
null . f = p'
(and when not null)
head . f = f'
tail . f = f . g'
f = unfold p' f' g'
now we have:
null . (unfold p f g . h) = p . h = p'
head . (unfold p f g . h) = f . h = f'
tail . (unfold p f g . h) = unfold p f g . g . h
= unfold p f g . h . g'
= (unfold p f g . h) . g'
now we have a system of equations for (unfold p f g . h) that fits the format,
so by coinduction we have:
unfold p f g . h = unfold p' f' g'
And we're done.
More information about the Haskell-Cafe