[Haskell-cafe] Proof of induction case of simple foldl identity.
Marcin Kosiba
marcin.kosiba at gmail.com
Sat Mar 14 17:44:55 EDT 2009
On Saturday 14 March 2009, Daniel Fischer wrote:
> Am Samstag, 14. März 2009 21:45 schrieb R J:
> > Can someone provide the induction-case proof of the following identity:
> >
> > foldl (-) ((-) x y) ys = (foldl (-) x ys) - y
> >
> > If foldl is defined as usual:
> >
> > foldl :: (b -> a -> b) -> b -> [a] -> b
> > foldl f e [] = e
>
> (R) foldl f e (x : xs) = foldl f (f e x) xs
>
> > The first two cases, _|_ and [], are trivial.
> >
> > Here's my best attempt at the (y : ys) case (the left and right sides
> > reduce to expressions that are obviously equal, but I don't know how to
> > show it):
> >
> > Case (y : ys).
> >
> > Left-side reduction:
> >
> > foldl (-) ((-) x y) (y : ys)
> > = {second equation of "foldl"}
> > foldl (-) ((-) ((-) x y) y) ys
> > = {notation}
> > foldl (-) ((-) (x - y) y) ys
> > = {notation}
> > foldl (-) ((x - y) - y) ys
> > = {arithmetic}
> > foldl (-) (x - 2 * y) ys
> >
> > Right-side reduction:
> >
> > (foldl (-) x (y : ys)) - y
> > = {second equation of "foldl"}
> > (foldl (-) ((-) x y) ys) - y
> > = {induction hypothesis: foldl (-) ((-) x y) ys = (foldl (-) x ys)
> > - y} ((foldl (-) x ys) - y) - y
> > = {arithmetic}
> > (foldl (-) x ys) - 2 * y
> >
> > Thanks as always.
>
> Consider a one-element list.
> foldl (-) (x-y) [z] = (x-y)-z
> (foldl (-) x [z]) - y = (x-z)-y
>
> So a necessary condition for the identity to generally hold is that the Num
> instance obeys the law
>
> (L) forall u v w. (u - v) - w = (u - v) - w
Typo? :)
(L) forall u v w. (u - v) - w = (u - w) - v
> Then take as inductive hypothesis that zs is a list such that
> forall a b. foldl (-) (a-b) zs = (foldl (-) a zs) - b
>
> Let z be an arbitrary value of appropriate type, x and y too.
> Then
>
> foldl (-) (x - y) (z:zs)
> = foldl (-) ((x-y)-z) zs (R)
> = (foldl (-) (x-y) zs) - z (IH, a = x-y, b = z)
> = ((foldl (-) x zs) - y) - z (IH, a = x, b = y)
> = ((foldl (-) x zs) - z) - y (L, u = foldl (-) x zs, v = y, w = z)
> = (foldl (-) (x-z) zs) - y (IH, a = x, b = z)
> = (foldl (-) x (z:zs)) - y (R)
>
> The trick is to formulate the inductive hypothesis with enough generality,
> so you have strong foundations to build on.
--
Pozdrawiam,
Marcin Kosiba
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: This is a digitally signed message part.
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090314/0a2fd360/attachment.bin
More information about the Haskell-Cafe
mailing list