foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ z []     = z
foldr f z (x:xs) = f x (foldr f z xs)

infixr 5 ++
(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

concat :: [[a]] -> [a]
concat []       = []
concat (xs:xss) = xs ++ concat xss
The right fold replaces constructors by a supplied step and seed; list concatenation replaces the end of its first argument by its second; flattening concatenates each inner list. In particular,
(1)
The right fold allows different element and accumulator types; the list concatenation operations require one common element type.
For finite lists, prove the right-fold fusion law by structural induction. The empty case uses the base-image premise:
f (foldr g a []) = f a = b = foldr h b []
For the cons case, use the compatibility premise, then the induction hypothesis:
f (foldr g a (x:xs))
  = f (g x (foldr g a xs))
  = h x (f (foldr g a xs))
  = h x (foldr h b xs)
  = foldr h b (x:xs)
The assumption that f is a strict function addresses partial spines. Write for the bottom value. A right fold must inspect the outer list constructor, so
(1)
The same cons calculation therefore establishes equality for finite partial spines ending in , including partial heads, because compatibility was assumed for all arguments.
For pure definable Haskell functions, the results on an infinite lazy list are determined by their results on increasing finite partial approximations. Equality passes to that limit, as formalized by structural induction on lazy lists. Thus
(2)
For finite total inputs alone, the empty and cons cases suffice. Strictness is needed to extend the claim to undefined spines; the finite-total proof by itself does not justify the infinite-input claim.
Fix ys and instantiate the right-fold fusion law with
f = foldr fn e
g = (:)
a = ys
h = fn
b = foldr fn e ys
The right fold is a strict function of its list argument. The base-image condition is immediate. For compatibility, expand one constructor:
f (x:y) = foldr fn e (x:y)
        = fn x (foldr fn e y)
        = h x (f y)
Fusion gives foldr fn e . foldr (:) ys = foldr fn (foldr fn e ys). Apply both sides to xs and replace foldr (:) ys xs by xs ++ ys:
(1)
This is a direct application of the right-fold fusion law, with no new induction proof. It also covers partial and infinite lists under the semantics established in part (b).
First define argument reversal, with its most general polymorphic type signature:
flip :: (a -> b -> c) -> b -> a -> c
flip f y x = f x y
Use concat = foldr (++) []. In the right-fold fusion law, choose f = foldr fn e, g = (++), a = [], b = e, and h = flip (foldr fn). The base-image condition follows from foldr fn e [] = e; strictness follows because a right fold inspects its input spine. Part (c) supplies exactly the compatibility condition:
f (xs ++ ys)
  = foldr fn (foldr fn e ys) xs
  = flip (foldr fn) xs (f ys)
  = h xs (f ys)
Consequently,
(1)
The accumulator argument of foldr fn comes before the inner list, whereas the outer right fold supplies the inner list first; flip reconciles those orders. The proof uses fusion and the already proved concatenation identity, without a further induction.

Ancestors (10)

  1. Functional programming, design and analysis of algorithms
  2. 2014
  3. Past exam of the year 1 of the computer science course of the University of Oxford
  4. Year 1 of the computer science course of the University of Oxford
  5. Computer science course of the University of Oxford
  6. Undergraduate course of the University of Oxford
  7. Course of the University of Oxford
  8. University of Oxford
  9. List of universities
  10. Home

View article source

Discussion (0) New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version