日々の流転

λ. “Much Ado about Two: A Pearl on Parallel Prefix Computation” by Janis Voigtländer

POPL 2008メモ1日目 - sumiiの日記(2008-01-11) より。 積読消化。

結合的な二項演算 ⊕ と入力 x1, …, xn とから x1, x1⊕x2, …, x1⊕x2⊕…⊕xn を計算するのが parallel prefix computation。 で、多相的な parallel prefix computation の関数 (α→α→α)→[α]→α の実装の正しさは、αが3値のデータ型のときだけ確かめればOKという話。

パラメトリシティ(free theorem)から正しい実装(scanl1)と結果が等しくなることを証明していて、確かにちゃんと追いかけるとそうなっているんだけど、なんだか不思議な感じ。 あと、整数全体ではなくて3値で十分であることの証明が賢いなぁと思った。 他のアルゴリズムに対しても系統的にこういうことを言えるようになると楽しそうだなぁ。