Graphics Programming

foldr의 fusion law 증명 본문

Season 1/하스켈

foldr의 fusion law 증명

minseoklee 2016. 6. 23. 20:53

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) 증명 끝



Comments