CSCC24 2024 Summer Assignment 1

This assignment is about

• induction proofs for recursive functions
• recursive data structures in Haskell

As usual, you should aim for reasonably efficient algorithms and reasonably organized, comprehensible code.

Code correctness (mostly auto-testing) is worth 90% of the marks; code quality is worth 10%.

Question 1: Induction Proofs [10 marks]

The following definitions are given.

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

t :: Integer -> [Integer] -> Integer
t a [] = a
t a (x:xs) = t (a+x) xs

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

s :: Integer -> [Integer] -> [Integer]
s a [] = a : []
s a (x:xs) = a : s (a+x) xs

Prove the following two statements by structural induction on finite lists.

1. [3 marks] for all finite list xs: map g (map f xs) = map (g . f) xs

2. [7 marks] for all finite list xs: for all integer a: map (t a) (inits xs) = s a xs

You will find these helpful:

• (g . f) = \x -> g (f x)
• When proving (b), it really helps to assume (a).
• You may do algebra inside a lambda.
• (\x -> f x) = f

Please hand in your solution in proof.txt.

Question 2: AVL Trees [10 marks]

AVL trees are binary search trees with an extra condition on shapes to ensure logarithmic height, so lookup is guaranteed to stay within logarithmic time. Evidently, insert and delete must perform shape checks and rotations to fulfill the extra condition. Evidently again, shape checks and rotations must not add more than logarithmic time either!

Whether this is the first time, second time, or last time you see AVL trees, please consult my past lecture slides for details.

In this question, you will implement insert. Please consult AVLDef.hs for definitions and basic helpers. For simplicity, we just have a key, no value.

Suggestions:

• Write a helper function for rebalancing one node. (Or, for making a balanced node from parts.) Then insert can use it.
• Write helper functions for rotations. Then the rebalancing function can use them. Separating them out reads nicer.
• In the lecture slides, the rotation pictures literally tell you what patterns to match for and what results should look like. :)
• Write a helper function for making or updating a node with auto-setting its height field. It is highly reusable.
• There is a painless way to ensure bottom-up rebalancing by adding it at the right place in recursive insert.

Please hand in your solution in AVL.hs. (Template provided.)