foldr의 fusion law 증명

foldr의 정의는 다음과 같다.

foldr :: (a -> b -> b) -> b -> [a] -> b

foldr f z [] = z

foldr f z (x:xs) = f x (foldr f z xs)

그리고 foldr의 fusion law는 다음과 같다.

f . foldr g a = foldr h b

if (1) f is strict

   (2) f a = b

   (3) f (g x y) = h x (f y)

증명은 수학적 귀납법을 이용한다.

기본 가정: (f . foldr g a) [] = foldr h b []

foldr의 정의에 따라 양변을 각각 전개하면

(f . foldr g a) [] = f a

foldr h b [] = b

조건 (2)에 의해 f a = b이므로 기본 가정 성립.

재귀 가정: f . foldr g a xs = foldr h b xs이 성립한다고 가정

f . foldr g a (x:xs) = foldr h b (x:xs)임을 증명해야 한다.

foldr h b (x:xs)

= h x (foldr h b xs) 가정에 의해

= h x (f (foldr g a xs)) 조건 (3)에 의해

= f (g x (foldr g a xs)) foldr의 정의에 따라

= f . foldr g a (x:xs) 증명 끝