第二双対定理
演算子 ⊕, ⊗ および a は全ての x, y, z について, つぎの関係を満たすものとする.
x ⊕ (y ⊗ z) = (x ⊕ y) ⊗ z
x ⊕ a = a ⊗ xつまり, ⊕ と ⊗ はたがいに結合的であり, ⊕ の右側に a があることと ⊗ の左側に a があることが等しいということである.
これらの条件のもとで, 任意の有限リスト xs に対して,foldr (⊕) a xs = foldl (⊗) a xsが成り立つ.
出典: 「関数プログラミング」p.72
だそうだ.
xs の要素を x1, x2, x3, … xn
とすると
foldr (⊕) a xs ⇒ x1 ⊕ (x2 ⊕ (x3 ⊕ … (xn ⊕ a) … ))
foldl (⊗) a xs ⇒…(((a ⊗ x1) ⊗ x2) ⊗ x3) … ⊗ xn
foldl (⊗) a xs ⇒…(((a ⊗ x1) ⊗ x2) ⊗ x3) … ⊗ xn
であり, 上の条件化ではこの二つは等しいからだ.
GHCi で, Haskell における reverse の再実装をしてみよう.
Prelude> :{
Prelude| let revr = foldr postfix []
Prelude| where postfix a xs = xs ++ [a]
Prelude| :}
Prelude> revr [1, 2, 3, 4]
[4,3,2,1]
Prelude> :{
Prelude| let revl = foldl prefix []
Prelude| where prefix xs a = [a] ++ xs
Prelude| :}
Prelude> revl [1, 2, 3, 4]
[4,3,2,1]
a `postfix` xs はリスト xs の後に, a だけからなるリストを連結したリスト.
xs `prefix` a は a だけからなるリストの前に, リスト xs を連結したリスト.
x `postfix` (y `prefix` z) と (x `postfix` y) `prefix` z は等しい.
x `postfix` [] と [] `prefix` x は等しい.
x `postfix` [] と [] `prefix` x は等しい.
ので, revr と revl は（数学的には）等しい.
ふむ… わかったようなわからんような.
学部時代, 本著の翻訳者である武市先生の授業の教科書でした.
当時（1997年だったかな）C言語で計測値に対する解析計算をするプログラムを書くのに精一杯だった私にとっては, 実用性の無い数学論に見えましたが, Haskell や他の関数型言語を齧った現在読むと, とても系統的に関数型言語についてまとめられていることが分かります.
翻訳も, 翻訳であることを意識させない滑らかさです. 元の英語を括弧書きする頻度も抜群です.
当時（1997年だったかな）C言語で計測値に対する解析計算をするプログラムを書くのに精一杯だった私にとっては, 実用性の無い数学論に見えましたが, Haskell や他の関数型言語を齧った現在読むと, とても系統的に関数型言語についてまとめられていることが分かります.
翻訳も, 翻訳であることを意識させない滑らかさです. 元の英語を括弧書きする頻度も抜群です.
動く様を見ないでも, 理論からその世界を想像できる方は, いきなりこれを読んでもよいでしょう.
実際に動かしてみないと分からない私のような人は, なんらかの関数型言語のチュートリアルを終えた後に読むと理解が系統立ってくるので良いと思います.