等式推論

programming-paradigmtype-theory

純粋関数型では「式をその値と等しいもので自由に置き換えられる」（参照透過性）。これを使い、プログラムを数式のように変形・証明する手法。リファクタリングの正当性も最適化も性質証明も、同じ「等式の連鎖」で扱える。

根拠 — 参照透過性

同じ入力には同じ出力、副作用なし。ゆえに x をその定義で置換しても、定義を x に畳んでも意味が変わらない。各等式は左右どちらに読んでもよい（簡約は向きを付けた適用）。

導出例 — map f . map g = map (f . g)

これは Stream Fusion の core にある map 融合則。リストへの2パス（g で1周、f でもう1周、中間リストを生成）を1パスに潰せることを、定義からの等式変形だけで示す。

定義（これらを書き換え規則として使う）:

map f []       = []                  -- (M1)
map f (x:xs)   = f x : map f xs      -- (M2)
(f . g) x      = f (g x)             -- (.)

リスト xs に関する構造帰納法。示したいのは全 xs で map f (map g xs) = map (f . g) xs。

base case (xs = []):

  map f (map g [])
= map f []                   -- (M1) で内側を書き換え
= []                         -- (M1)
= map (f . g) []             -- (M1) を逆向き ⇒ 一致 ∎

inductive case (xs = x : xs'、帰納法の仮定 IH: map f (map g xs') = map (f . g) xs'):

  map f (map g (x:xs'))
= map f (g x : map g xs')         -- (M2)
= f (g x) : map f (map g xs')     -- (M2)
= f (g x) : map (f . g) xs'       -- IH を適用
= (f . g) x : map (f . g) xs'     -- (.) を逆向き
= map (f . g) (x:xs')             -- (M2) を逆向き ⇒ 一致 ∎

両ケースが閉じたので帰納法より全 xs で成立。この等式が成り立つ＝中間リスト除去（融合）は意味を変えない、という最適化の正当性証明そのものになっている。

用途

なぜ副作用を隔離するのか

副作用（IO・可変状態）があると「同じ式が同じ値」が崩れ、置換ができない＝等式推論が破れる。関数型が副作用を IO 型やeffectに隔離する動機のひとつが、純粋部分で等式推論を保つこと。

-- 純粋: let で括り出しても値は同じ（参照透過）
f (g x) + f (g x)  ==  let y = f (g x) in y + y

-- 不純: getLine を括り出すと「2回読む」が「1回読んで複製」に変わり、意味が壊れる
getLine >> getLine  =/=  let l = getLine in l >> l

証明の道具立て

道具いつ使う例
定義の展開/畳み込み等式の片側を定義で書き換えるmap f (x:xs) = f x : map f xs
構造帰納法帰納的データ（リスト・木）上の全称命題reverse (reverse xs) = xs
自由定理型だけから従う等式（実装を見ずに）f . map g = map g' . f（多相 f の自然性）
余帰納法 (coinduction)無限/遅延データの等価性（双模倣）無限ストリームの等しさ
等式書き換え系機械的に向きを付けて適用fusion 則、コンパイラのリライトルール

帰納と等式変形は補完関係: 等式変形で1ステップを進め、再帰呼び出しの箇所で帰納法の仮定 (IH) を差し込む、というのが上の導出の骨格。

関連

押さえどころ（カード化候補）

Graph

Backlinks