Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Functional programming, design and analysis of algorithms / 4

Separate the empty prefix from the prefixes beginning with the first element:

inits :: [a] -> [[a]]
inits [] = [[]]
inits (x:xs) = [] : map (x:) (inits xs)

Every nonempty list prefix begins with x and continues with a prefix of xs. Thus the recursive order is increasing prefix length, beginning with length zero. Lazy evaluation can also expose every finite prefix of a productive infinite input.

b

 0  0

Solution

 0  0

The most general type signature is scanl :: (b -> a -> b) -> b -> [a] -> [b]. The left fold step consumes an accumulator of type b and an input of type a, returning the next accumulator. A left scan retains all these accumulator values, including the initial one.

c

 0  0

Solution

 0  0

Use map k (u:us) = k u : map k us, list-map fusion, and the left fold equation

foldl f e (x:ys) = foldl f (f e x) ys

For the empty list, the prefix definition immediately gives scanl f e [] = [e]. For a nonempty list, calculate:

scanl f e (x:xs)
  = map (foldl f e) ([] : map (x:) (inits xs))
  = e : map ((foldl f e) . (x:)) (inits xs)
  = e : map (foldl f (f e x)) (inits xs)
  = e : scanl f (f e x) xs

The second-to-third line uses the displayed fold equation as an equality of functions of ys. Hence the efficient left scan is:

scanl :: (b -> a -> b) -> b -> [a] -> [b]
scanl f e [] = [e]
scanl f e (x:xs) = e : scanl f (f e x) xs

On a finite input of length

n

, fully demanding the original prefix-fold results performs

0 + 1 + \dots + n = n (n + 1) /2

accumulator updates. The recurrence performs

n

. Thus the update count improves from $Θ (n^{2})$ to $Θ (n)$ , assuming constant-cost updates. Both return

n + 1

results. This does not assert constant space for arbitrary accumulators or imply that lazy accumulators are evaluated strictly.

d

 0  0

Solution

 0  0

Prove the natural-number fold fusion law pointwise. At Zero,

f (foldNat g a Zero) = f a = b = foldNat h b Zero

Assuming the equation at m, the Succ m calculation is:

f (foldNat g a (Succ m))
  = f (g (foldNat g a m))
  = h (f (foldNat g a m))
  = h (foldNat h b m)
  = foldNat h b (Succ m)

The compatibility premise f . g = h . f justifies the middle rewrite. This proves the theorem for finite total constructor values by structural induction.

For the full lazy Haskell interpretation, also handle the bottom value: foldNat g a is strict in its outer Natural constructor, so its value on bottom is bottom; the assumed strict function property of f makes the left side bottom too. The same zero/successor induction now covers finite partial constructor chains. Pure definable functions preserve the limits of these information approximations, extending equality to infinite Succ chains. This explains the strictness premise; finite total induction alone would not use it.^[ref]

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Functional programming, design and analysis of algorithms / 4

a

Solution

b

Solution

c

Solution

d

Solution

 Ancestors (10)

 Discussion (0) New discussion

 Articles by others on the same topic (0)

Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Functional programming, design and analysis of algorithms / 4

 Discussion (0)  Subscribe (1) New discussion

 Discussion (0) New discussion