# Case Study: MapReduce

## Implementation

{-@ reflect mapReduce @-} mapReduce :: Int -> (List a -> b) -> (b -> b -> b) -> List a -> b mapReduce n f op is = reduce op (f N) (map f (chunk n is)) {-@ reflect reduce @-} reduce :: (a -> a -> a) -> a -> List a -> a reduce op b N = b reduce op b (C x xs) = op x (reduce op b xs) {-@ reflect map @-} {-@ map :: (a -> b) -> xs:List a -> {v:List b | llen v == llen xs } @-} map _ N = N map f (C x xs) = f x C map f xs {-@ reflect chunk @-} chunk :: Int -> List a -> List (List a)

## Use Case: Summing List

{-@ reflect sum @-} sum :: List Int -> Int sum N = 0 sum (C x xs) = x plus sum xs {-@ reflect plus @-} plus :: Int -> Int -> Int plus x y = x + y {-@ reflect psum @-} psum :: Int -> List Int -> Int psum n is = mapReduce n sum plus is

Question: Is psum equivalent to sum?

## Proving Code Equivalence

{-@ automatic-instances sumEq @-} {-@ sumEq :: n:Int -> is:List Int -> { sum is == psum n is } @-} sumEq n is = mRTheorem n -- chunk size sum -- function to map-reduce plus -- reduction operator plusRightId -- plus has "right-identity" sumDistr -- sum is "distributive" is -- input list
Using distribution and right identity of plus
{-@ sumDistr   :: xs:List Int -> ys:List Int ->
{sum (xs ++ ys) == plus (sum xs) (sum ys)} @-}

{-@ plusRightId :: xs:List Int ->
{plus (sum xs) (sum N) == sum xs} @-}


## Higher Order Map Reduce Theorem

If f is right-id and op distributes ...

... then it is OK to map-reduce.

{-@ mRTheorem :: n:Int -> f:(List a -> b) -> op:(b -> b -> b) -> rightId:(xs:List a -> {op (f xs) (f N) == f xs } ) -> distrib:(xs:List a -> ys:List a -> {f (xs ++ ys) == op (f xs) (f ys)} ) -> is:List a -> { mapReduce n f op is == f is } / [llen is] @-}

## Right Identity

Lets prove Right Identity

{-@ plusRightId :: xs:List Int -> {plus (sum xs) (sum N) == sum xs} @-} plusRightId xs = undefined

## Warmup: Associativity of append

• Lets prove Associativity of append
{-@ appendAssoc :: xs:List a -> ys:List a -> zs:List a -> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs } @-} appendAssoc xs ys zs = undefined

## Proof automation: Associativity of Append

Proof automation flag automates all the rewriting!
{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}

{-@ automatic-instances appendAssocAuto @-} {-@ appendAssocAuto :: xs:List a -> ys:List a -> zs:List a -> { xs ++ (ys ++ zs) == (xs ++ ys) ++ zs } @-} appendAssocAuto N _ _ = trivial appendAssocAuto (C _ xs) ys zs = appendAssocAuto xs ys zs

## Back to Distribution

• Lets prove distribution
{-@ automatic-instances sumDistr @-} {-@ sumDistr :: xs:List Int -> ys:List Int -> {sum (xs ++ ys) == plus (sum xs) (sum ys)} @-} sumDistr xs ys = undefined

## Recap

• Refinement Reflection: Allow Haskell functions in Logic
• Case Study: Prove Program Equivalence

where Haskell = a general purspose programming language.

## Recap

1. Refinements: Types + Predicates
2. Automation: SMT Implication
3. Measures: Specify Properties of Data
4. Termination: Semantic Termination Checking
5. Reflection: Allow Haskell functions in Logic!
6. Case Study: Prove Program Equivalence

## Thank You!

cabal install liquidhaskell

http://www.refinement-types.org

## Map Reduce Equivalence

mRTheorem n f op rightId _ N = mapReduce n f op N ==. reduce op (f N) (map f (chunk n N)) ==. reduce op (f N) (map f (C N N)) ==. reduce op (f N) (f N C map f N ) ==. reduce op (f N) (f N C N) ==. op (f N) (reduce op (f N) N) ==. op (f N) (f N) ? rightId N ==. f N *** QED mRTheorem n f op rightId _ is@(C _ _) | n <= 1 || llen is <= n = mapReduce n f op is ==. reduce op (f N) (map f (chunk n is)) ==. reduce op (f N) (map f (C is N)) ==. reduce op (f N) (f is C map f N) ==. reduce op (f N) (f is C N) ==. op (f is) (reduce op (f N) N) ==. op (f is) (f N) ==. f is ? rightId is *** QED mRTheorem n f op rightId distrib is = mapReduce n f op is ==. reduce op (f N) (map f (chunk n is)) ==. reduce op (f N) (map f (C (take n is) (chunk n (drop n is)))) ==. reduce op (f N) (C (f (take n is)) (map f (chunk n (drop n is)))) ==. op (f (take n is)) (reduce op (f N) (map f (chunk n (drop n is)))) ==. op (f (take n is)) (mapReduce n f op (drop n is)) ==. op (f (take n is)) (f (drop n is)) ? mRTheorem n f op rightId distrib (drop n is) ==. f ((take n is) ++ (drop n is)) ? distrib (take n is) (drop n is) ==. f is ? appendTakeDrop n is *** QED

## Append of Take and Drop

{-@ appendTakeDrop :: i:Nat -> xs:{List a | i <= llen xs} -> {xs == (take i xs) ++ (drop i xs) } @-} appendTakeDrop i N = (take i N) ++ (drop i N) ==. N ++ N ==. N *** QED appendTakeDrop i (C x xs) | i == 0 = (take 0 (C x xs)) ++ (drop 0 (C x xs)) ==. N ++ (C x xs) ==. C x xs *** QED | otherwise = (take i (C x xs)) ++ (drop i (C x xs)) ==. (C x (take (i-1) xs)) ++ (drop (i-1) xs) ==. C x ( (take (i-1) xs) ++ (drop (i-1) xs)) ==. C x xs ? appendTakeDrop (i-1) xs *** QED

## List Definition

Built-in Lists are not supported for now.

(So does imports...)

{-@ data List [llen] a = N | C {lhead :: a, ltail :: List a} @-} data List a = N | C a (List a) {-@ measure llen @-} {-@ llen :: List a -> Nat @-} llen N = 0 llen (C _ xs) = 1 + llen xs

## List Manipulation

{-@ chunk :: i:Int -> xs:List a -> {v:List (List a) | if (i <= 1 || llen xs <= i) then (llen v == 1) else (llen v < llen xs) } / [llen xs] @-} chunk i xs | i <= 1 = C xs N | llen xs <= i = C xs N | otherwise = C (take i xs) (chunk i (drop i xs)) {-@ reflect drop @-} {-@ drop :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == llen xs - i } @-} drop i N = N drop i (C x xs) | i == 0 = C x xs | otherwise = drop (i-1) xs {-@ reflect take @-} {-@ take :: i:Nat -> xs:{List a | i <= llen xs } -> {v:List a | llen v == i} @-} take i N = N take i (C x xs) | i == 0 = N | otherwise = C x (take (i-1) xs) {-@ reflect ++ @-} N ++ ys = ys (C x xs) ++ ys = x C (xs ++ ys)