# Exercise 3.11 Define ‘delmin’ as a paramorphism. Again, we seek a solution to the following for lists xs: paraL f e = delmin This gives us some (slightly gnarly) types: e ∷ Maybe (α, List α) f ∷ α → (List α, Maybe (α, List α)) → Maybe (α, List α) ... It might be helpful to define a fold equivalent to a tupled function like this: -- xs ≠ Nil delmin′ xs = (xs, (minimumL xs, deleteL (minimumL xs) xs)) Let’s try this. ... delmin′ = foldL1 f where f y (ys, (x, zs)) | y ≤ x = (Cons y ys, (y, ys)) | otherwise = (Cons y ys, (x, Cons y zs)) Back to the main challenge. The solution for the first equation, paraL f e Nil = delmin′ Nil is immediate: e = Nothing. For the second equation, we consider the cases Cons x Nil and Cons x (Cons x′ Nil). Case Cons x Nil: paraL f e (Cons x Nil) = delmin (Cons x Nil) ≡ { paraL.2, delmin.2 } f x (Nil, paraL f e Nil) = Just (minimumL (Cons x Nil), deleteL (minimumL (Cons x Nil)) (Cons x Nil)) ≡ { evaluating minimumL on a singleton list } f x (Nil, paraL f e Nil) = Just (x, deleteL x (Cons x Nil)) ≡ { deleteL.2, generalizing (paraL f e Nil) to m } f x (Nil, m) = Just (x, Nil) This gives us "the real base case". Case Cons x (Cons x′ xs). We use the induction hypothesis paraL f e (Cons x′ xs) = delmin (Cons x′ xs) The calculation proceeds: paraL f e (Cons x (Cons x′ xs)) = delmin (Cons x (Cons x′ xs)) ≡ { paraL.2, delmin.2 } f x (Cons x′ xs, paraL f e (Cons x′ xs)) = Just (minimumL (Cons x (Cons x′ xs)), deleteL (minimumL (Cons x (Cons x′ xs))) (Cons x (Cons x′ xs))) ≡ { induction hypothesis } f x (Cons x′ xs, delmin (Cons x′ xs)) = Just (minimumL (Cons x (Cons x′ xs)), deleteL (minimumL (Cons x (Cons x′ xs))) (Cons x (Cons x′ xs))) ≡ { delmin.2 } f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (minimumL (Cons x (Cons x′ xs)), deleteL (minimumL (Cons x (Cons x′ xs))) (Cons x (Cons x′ xs))) where y = minimumL (Cons x′ xs) We will need an easy lemma. Lemma 1: If x : α and x > minimumL xs, then minimumL (Cons x xs) = minimumL xs Proof: minimumL (Cons x xs) = { minimumL.1 } foldL min x xs = { foldL.2, twice } min x (minimumL xs) = { assumption } minimumL xs ∎ Lemma 2: If x ≤ minimumL xs, then minimumL (Cons x xs) = x The proof is identical to the above, with min x (minimumL xs) = x. We have two cases to consider. Case x > y: f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (minimumL (Cons x (Cons x′ xs)), deleteL (minimumL (Cons x (Cons x′ xs))) (Cons x (Cons x′ xs))) where y = minimumL (Cons x′ xs) ≡ { case statement, lemma 1 } f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (y, deleteL y (Cons x (Cons x′ xs))) where y = minimumL (Cons x′ xs) ≡ { deleteL.2, x ≠ y } f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (y, Cons x (deleteL y (Cons x′ xs))) where y = minimumL (Cons x′ xs) ≡ { generalizing (deleteL y (Cons x′ xs)) to ys } f x (Cons x′ xs, Just (y, ys)) = Just (y, Cons x ys) where y = minimumL (Cons x′ xs) ≡ { generalizing y } f x (Cons x′ xs, Just (y, ys)) = Just (y, Cons x ys) which gives us a solution for the case. So far, Case x ≤ y: ≡ { generalizing y } f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (minimumL (Cons x (Cons x′ xs)), deleteL (minimumL (Cons x (Cons x′ xs))) (Cons x (Cons x′ xs))) ≡ { lemma 2 } f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (x, deleteL x (Cons x (Cons x′ xs))) ≡ { deleteL.2 } f x (Cons x′ xs, Just (y, deleteL y (Cons x′ xs))) = Just (x, (Cons x′ xs)) ≡ { generalizing (deleteL y (Cons x′ xs)) to ys } f x (Cons x′ xs, Just (y, ys)) = Just (x, (Cons x′ xs)) which gives the solution to the remaining case. delmin = paraL f Nothing where f x (Nil, m) = Just (x, Nil) f x (Cons x′ xs, Just (y, ys)) | x > y = Just (y, Cons x ys) | otherwise = Just (x, Cons x′ xs) This completes the synthesis. Whew!