10. Reasoning about programs

09/03/23

data Expr a = Var a
            | Val Int
            | Add (Expr a) (Expr a)

Add (Var 'x') (Val 1) :: Expr Char

instance Monad Expr wehere
    -- return :: Expr a -> (a -> Expr b) -> Expr b
    (Var v) >>= f = f v
    (Value n) >>= f = Val n
    (Add x y) >>= f = Add (x >>= f) (y >>= f)
    

Reasoning about programs

1. How to do proofs about programs
2. How to improve program efficiency
3. Case study: compiler correctness

Equational Reasoning

One like distributive rule

$x y = yx$ ...

$(x+a)(x+b$ = $(x+a)x = (x+a)b$ = $x x + a x + c b + ab$ .... =$x^2+(a+b)x + ab$

Reasoning about Haskell

double :: Int -> Int
double x = x + x