BEGIN 16_12_01_Reasoning_about_Programs.part_1.lhs

REASONING ABOUT PROGRAMS AND VERIFICATION OF PROGRAMS (PART 1)

-##########################################################
READING: Search for "reasoning about programs" and "program
varification" on the Web. More directly related to the material
in this handout, read Chapter 9, especially Sections 9.1 and 9.6, 
and Section 14.7 in Simon Thompson's book "Haskell, the Craft of 
Functional Programming".
-##########################################################

REASONING ABOUT PROGRAMS takes different forms, requiring different
degrees of formalisms and mathematical rigor. Whatever form it takes,
it is naturally easier to reason about small program fragments or modules 
than about whole software packages (with thousands or hundreds of thousands
lines of codes). And whatever form it takes, REASONING ABOUT PROGRAMS and
VERIFICATION OF PROGRAMS are about predictability -- predicting that
programs will behave in desirable/expected/efficient ways.

Depending on the approach (and there are many approaches!), it may or may 
not be easy to compose local/localized formal verifications to produce a 
global verification (that the whole program satisfies some desirable 
specifications). Composability of formal reasoning and formal verification
has been, and continues to be, an area of intensive research.

We have already encountered elements of reasoning about programs in this
course. For example, when we declare "x :: Int", we mean that x will 
always be an integer and that every program phrase using x can safely
rely on that fact being enforced. A type discipline is therefore a
systematic/formalized method for enforcing invariants (such as the
invariant "x :: Int"). 

But "types as invariants" are not the only kinds of invariants in program
analysis. We discussed "loop invariants" in earlier lectures (see the 
handout 16_11_15_InvariantExamples.lhs), which are introduced to confirm
that an iteration or a recursion performs as expected.

In fact, handling INVARIANTS (how to define them, formalize them, compose
them) can be taken as the bread-and-butter of any form of program analysis.

In this handout, we reason about equivalence between different programs
or different program fragments. Our reasoning about programs here takes the
form of an induction on the size or the structure of the data consumed by
the programs. And again we use invariants -- an INDUCTION HYPOTHESIS is 
exactly an INVARIANT.

-############################################################

EXERCISE 1: Consider the following function definitions

> fooA f g lst = map (f . g) lst
> fooB f g     = map (f . g) 
> fooC f g lst = map f (map g lst)
> fooD f g     = \ lst -> map f (map g lst)

Explain why these are equivalent definitions. Is there one
which is easiest to compute (i.e. cheapest w.r.t. time and/or
space complexity)? 

EXERCISE 2: Consider the following function definitions

> fooE f lst1 lst2 = (map f lst1) ++ (map f lst2)
> fooF f lst1 lst2 = map f (lst1 ++ lst2)

Explain why these are equivalent definitions. Is one easier
to computer than the other?

EXERCISE 3: The definition of "(++)" in Prelude.hs is

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

Based on this definition, prove the two following equations:

xs ++ [] = xs
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

EXERCISE 4: The function "elem" is already defined in Prelude.hs.
Here is an equivalent definition of "elem", called "myElem", a 
little different from that in Prelude.hs:

> myElem :: Eq a => a -> [a] -> Bool
> myElem x [] = False
> myElem x (y:ys) = (x == y) || (myElem x ys)

Based on this definition of "myElem", prove the following
equation:

myElem z (xs ++ ys) = myElem z xs  || myElem z ys

EXERCISE 5: The function "filter" is already defined in Prelude.hs.
Here is an equivalent definition of "filter", called "myFilter",
a little different from that in Prelude.hs:

> myFilter :: (a -> Bool) -> [a] -> [a]
> myFilter p [] = []
> myFilter p (x:xs)
>     | (p x)              = x : (myFilter p xs)
>     | not (p x)          = myFilter p xs

Based on this definition of "myFilter", prove the following
equation:

myFilter p (xs ++ ys) = (myFilter p xs) ++ (myFilter p ys)

EXERCISE 6: Based on the definition of "(++)" in Exercise 3
above, and the following definition of "length" (already in
Prelude.hs):

length :: [a] -> Int
length []     = 0
length (x:xs) = 1 + length xs

Prove the following equation:

length (xs ++ ys) = length xs + length ys

EXERCISE 7: Based on the definition of "(++)" in Exercise 3
above, and the following definition of "reverse" (already in
Prelude.hs):

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

Prove the following equation:

reverse (xs ++ ys) = reverse ys ++ reverse xs

-###################################################

BEGIN EXAMPLE 1:

The material in this example is taken from Section 11.6 in
Simon Thompson's book.

Given the following definitions of "map" and "reverse":

  map f []       = []                           -- (map.1)
  map f (x:xs)   = f x : map f xs               -- (map.2)

  reverse []     = []                           -- (reverse.1)
  reverse (z:zs) = reverse zs ++ [z]            -- (reverse.2)

prove the following equation:

  map f (reverse xs) = reverse (map f xs)       -- (map/reverse)

This is proved by induction -- on the length of "xs"

(1) BASE STEP: "xs" has length 0, i.e. "xs = []".

In this case, the LHS of (map/reverse) is:

  map f (reverse [])
    = map f []                                -- by (reverse.1)
    = []                                      -- by (map.1)

The RHS of (map/reverse) is:

  reverse (map f [])
    = reverse []                              -- by (map.1)
    = []                                      -- by (reverse.1)

Hence, map f (reverse []) = reverse (map f []).

(2) INDUCTION STEP: Assuming we have proved (map/reverse) for
a list "xs" of length "n" (this is the INDUCTION HYPOTHESIS), 
we have to prove (map/reverse) for a list "x:xs" of length "n+1".

The LHS of what we have to prove is:

  map f (reverse (x:xs))
    = map f (reverse xs ++ [x])               -- by (reverse.2)

Here is another equation, whose proof is left to you (it is also
[HCFP, Exercise 11.31, p 261]:

  map f (ys ++ zs) = map f ys ++ map f zs     -- (map++)

Based on (map++), we simplify LHS of (map/reverse) further:

    = map f (reverse xs) ++ map f [x]         -- by (map++)
    = map f (reverse xs) ++ [f x]             -- by (map.2)
    = reverse (map f xs) ++ [f x]             -- by IND HYP

The RHS of what we have to prove is:

  reverse (map f (x:xs))
    = reverse (f x : map f xs)                -- by (map.2)
    = reverse (map f xs) ++ [f x]             -- by (reverse.2)

Which shows that the LHS and the RHS are the same. This completes
the INDUCTION STEP and the proof.

END EXAMPLE 1.

-###################################################

SEVERAL DECLARATIONS for Exercises 8, 9 and 10:

> square :: Int -> Int
> square x = x * x

> mapSq lst = map square lst

> mySum [] = 0
> mySum (x : xs) = x + mySum xs

> fooG lst = mySum (mapSq lst)

> fooH [] = 0
> fooH (x : xs) = square x + fooH xs

> fooI :: [Int] -> Int
> fooI lst = foldr (\ x y -> x*x + y) 0 lst

EXERCISE 8. Prove following equality for every list "lst" of integers:

   fooG lst = fooH lst

i.e., fooG and fooH are equivalent. Give reasons for why fooH will
likely lead to a more efficient implementation than fooG.

EXERCISE 9. Prove following equality for every list "lst" of integers:

   fooH lst = fooI lst

i.e., fooH and fooI are equivalent. Do you have reasons for preferring 
fooH over fooI, or vice-versa? Explain.  

EXERCISE 10. Similar to the declaration of fooI above, complete the
following declaration (enter the missing code at the ellipses):

  fooJ :: [Int] -> Int
  fooJ lst = foldl (\ x y -> ... ) 0 lst

and show that fooI and fooJ are equivalent.

SEVERAL DECLARATIONS for Exercises 11 and 12:

> delA x []               = []
> delA x (y:ys) 
>     | x == y            = ys
>     | otherwise         = y : delA x ys

> delB x lst = myFilter (\ y -> x /= y) lst

EXERCISE 11. The functions delA and delB are not equivalent, i.e.,
there are input values, "x" and "lst", for which "(delA x lst)" and
"(delB x lst)" return different values. State a condition on the input
"lst" -- as simple as possible -- so that delA and delB are
equivalent. Adjust delA to produce a new function delA' equivalent to
delB. Finally, for the most complicated part of this exercise, adjust 
delB to produce a new function function delB' equivalent to delA.

HINT: "delA" deletes the first occurrence of "x" in "lst",
"delB" deletes every occurrence of "x" in "lst".

EXERCISE 12. Under the condition stated on "lst" in Exercise 11, prove
the equality delA lst = delB lst.  

SEVERAL DECLARATIONS for Exercises 13, 14, 15 and 16:

> nubA [] = []
> nubA (x:xs) =
>      let ys = nubA xs 
>      in if x `elem` ys 
>         then ys
>         else x : ys

> nubB [] = []
> nubB (x:xs) = x : filter (\ y -> x /= y) (nubB xs)

EXERCISE 13.  An alternative definition for nubA is the following:

> nubA' [] = []
> nubA' (x:xs) 
>     | elem x (nubA' xs)         = nubA' xs
>     | otherwise                 = x : nubA' xs

Give reasons for preferring nubA over nubA'.

EXERCISE 14. Describe in English what the output of "nubA lst" is for
an arbitrary input list "lst".  HINT: "nubA" eliminates duplicated
entries in "lst".  

EXERCISE 15. Describe in English what the output of "nubB lst" is for
an arbitrary input list "lst".  HINT: "nubB" also eliminates
duplicated entries in "lst", but in an order different from that of
"nubA".

EXERCISE 16. Prove that "nubA" and "nubB" are NOT equivalent, i.e.,
there is an input list "lst" such that "nubA lst" and "nubB lst"
return different values.

-##################################################

END 16_12_01_Reasoning_about_Programs.part_1.lhs