The Haskell type signatures are take :: Int -> [a] -> [a] and drop :: Int -> [a] -> [a]. These definitions also handle nonpositive counts as the Prelude does:
take n _ | n <= 0 = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs

drop n xs | n <= 0 = xs
drop _ [] = []
drop n (_:xs) = drop (n-1) xs
The wildcard in the first equation matters under lazy evaluation: take 0 undefined yields [] without inspecting its list argument. The remainder of this question uses nonnegative counts.[ref]
For finite, defined lists, structural induction requires and for every head and tail . This proves for every finite list.
An infinite list cannot be reached by finitely many constructor steps. For structural induction on lazy lists, also check , where is the bottom value, and require an admissible predicate on lazy lists: if increasingly defined finite approximations all satisfy , their limit does too. Together with the empty-list and constructor cases this covers finite, partial and infinite lists. Merely asserting the two finite-list cases is insufficient; “the list is finite” itself satisfies those cases but fails on infinite lists.
Use mathematical induction on , which is finite even when the list is infinite. At , the left side is [] ++ xs = xs. For the successor step, an empty list gives []; for x:xs, the defining equations and list concatenation give
take (n+1) (x:xs) ++ drop (n+1) (x:xs)
= (x : take n xs) ++ drop n xs
= x : (take n xs ++ drop n xs)
= x : xs
The last step applies the induction hypothesis to the tail. A bottom value tail is allowed: for a wholly undefined list and a positive count both sides are undefined. Thus the equality is observationally valid for finite and infinite lists; no evaluation of an infinite length is used.
For finite lists and , the answers are
reverse (xs ++ ys) = reverse ys ++ reverse xs
length (drop n xs) = max 0 (length xs - n)
The maximum is necessary when the count exceeds the list length.
Write u = take n xs, v = drop n xs, and len = length xs. Part (c) gives xs = u ++ v; part (d) gives length v = len-n because . Use the finite-list laws take (length v) (v ++ w) = v, length (reverse v) = length v, and reverse (reverse v) = v. Then equational reasoning gives
reverse (take (len-n) (reverse xs))
= reverse (take (length v) (reverse (u ++ v)))
= reverse (take (length (reverse v)) (reverse v ++ reverse u))
= reverse (reverse v)
= v
= drop n xs
The first and second steps use the decomposition and the length equation; the third uses reversal of a concatenation; the fourth uses the stated take law. This is an algebraic proof using established laws, rather than a new induction proof.

Ancestors (10)

  1. Functional programming, design and analysis of algorithms (resit)
  2. 2016
  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