12. Making Append Vanish

20/03/23

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

How many steps for reverse

reverse [1,2]
=
reverse [2] ++ [1]
= 
(reverse [] ++ [2]) ++ [1]
=
([] ++ [2]) ++ [1]

reverse xs takes 1+2+...+(n+1) steps, where n = length xs

Conductive Induction

reverse' xs ys = (reverse xs) ++ ts Base Case:

reverse' [] ys
=
(reverse []) ++ ys
=
[] ++ ys
=
ys

reverse' [] ys = ys

Inductive Case:

reverse' (x:xs) ys
= reverse (xs:xs) ++ ys
= (reverse xs ++ [x]) ++ ys
= reverse xs ++ ([x] ++ ys)
= reverse xs ++ (x:ys)
= reverse' xs (x:ys)

reverse' :: [a] -> [a] -> [a]
reverse' [] ys = ys
reverse' (x:xs) ys = reverse' xs (x:ys)

reverse :: [a] -> [a]
reverse xs = reverse' xs []