Fusion Property of fold

foldつづき.

Fusion Property

以下の形の等式を考えます.

h o fold g w = fold f v

これは一般に成り立つわけではありませんが、
成り立つ場合にはUniversal Propertyによって次のような表現と同等であると言えます.

(h o fold g w)     [] = v
(h o fold g w) (x:xs) = f x ((h o fold g w) xs)

これは,関数融合により以下のように書き直すことが出来ます.

h (fold g w [])     = v
h (fold g w (x:xs)) = f x (h (fold g w xs))

foldの定義(fold g w [] = w)により、

h w [] = v 
h (g x (fold g w xs)) = f x (h (fold g w xs))

ここで(y = fold g w xs)とおくと,

h w = v
h (g x y) = f x (h y)

となる.

h w = v
h (g x y) = f x (h y)
<=>
h o fold g w = fold f v

この形(が成り立つ事)をfoldのFusion Propertyと云う.

使う

このfusion propertyも証明に用いる基本的な原則としてに役に立ちます.
前回と同じく以下の式を考えます.

((+1) o sum = fold (+) 1

foldによるsumの定義(sum = fold (+) 0)によって以下のように変形します.

(+1) o fold (+) 0 = fold (+) 1

これはfusion propertyの形にマッチするので

((+) 1) 0 = 1
((+) 1) ((+) x y) = (+) x (((+) 1) y)

これを中置記法に直すと

1 + 0 = 1
1 + (x + y) = x + (1 + y)

となり、元の式が正しいことが証明できます.
fusion propertyを使うことで、明示的な帰納を使わなくとも証明が行えました.

より一般的には、任意の中置演算子について以下のようになります.

// 通じるような気がする
 (op) :: infix
 ((op) a) o fold (op) b = fold (op) (b op a)


参考