Equational Reasoning 入門

Info

この記事は 理情 Advent Calendar 2025の 19 日目の記事です。
せっかくなので Haskell Advent Calendar 2025の 17 日目の記事にもさせていただきました。

IS26er の atree4728 です。 東京大学の非本質の部分（第二外国語など）を乗り越えて、無事に理学部情報科学科に内定しました。 通学時間に中国語を Anki でセコセコ詰めたりしていた日々の面影はなく、最近は大学 2（だれも基本平均点や二外の話をせず、毎日みんなでパソコンしたり数学したりして1日がおわるマジで楽しい大学）を満喫しています。

つい先日、形式言語理論で CKY アルゴリズム（BNF 記法と文字列が与えられて構文木を列挙する問題を区間 DP で解く）を実装する課題が出て Haskell でやると楽しそうだと思いそうした のですが、これをきっかけに Haskell 熱が再燃して、積んでいた [1] を読みました。 ここで読んだ Equational Reasoning / 等式推論 というテクニックが非常に面白かったので、今回はこれを紹介しようと思います。

前提知識は Haskell の基本的な文法ですが、モナドとかは出てこないので情報科学基礎実験で Scheme を書いているなどすれば大丈夫だと思います。 また、map fold scan あたりに親しみがあると読みやすいと思います。

関数型言語

C のような手続き型言語における「関数」は、一連の処理手順を再利用可能な形にまとめたサブルーチンであり、グローバル変数の読み書きや I/O といった 副作用（Side Effect） を伴います。 そのため、同じ実引数に対しても必ずしも同じ返り値を得るとは限りません。

対して、Haskell や Scheme のような純粋関数型言語における「関数」は数学における写像と同義であり、実引数が同じならいつ呼び出しても外部の状態に依存せずに同じ結果を返すことが保証されています。 このような性質は参照透過性と呼ばれています。 参照透過性は、プログラム内の式をそれと（値として）等価な別の式に置換してもプログラム全体の振舞いが変わらないことを保証するためプログラムについて論証するのに向いています¹。

これは参照透過でない関数について考えるとわかりやすいです。 次のような C コードを考えてみましょう。

int f(int n) {
    printf("Hello\n");
    return n;
}
 
int g(int n) {
  return f(n) + f(n);
}
 
int h(int n) {
  return f(n) * 2;
}

f を呼び出すと I/O が発生するのでこれは参照透過ではありません。 そのため、値として $f(n)+f(n)=2\times f(n)$ が成立するのにもかかわらず、g と h ではプログラムの挙動が異なります。 実際、g では副作用が二回発生しますが h では一回しか発生しません。

一方関数型言語では参照透過性が担保されているので²、このような事態は発生しません。 プログラム中に現れる g を h に置換しても全体のプログラムの振舞いは変化しないため、私たちが勝手に都合のよい書き換えを行うことでプログラムについて論証することができるのです！

Equational Reasoning とは

関数型言語における Equational Reasoning とは、簡約関係によって導かれる代数的な等式変形によってプログラムについて論証したり、アルゴリズムの計算量を改善したりする形式手法のことです。

次のような簡単な例を考えてみましょう。

swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

関数 swap は、型 a と型 b を持つ値のペア (x, y) に対して適用すると (y, x) を返すものとして定義されています。 このような定義を持つ関数 $\mathsf{swap}$ について、次の命題を証明することができます。

$$\forall (x,y),\mathsf{swap}(\mathsf{swap}(x,y))=(x,y).$$

実際、次のような等式変形によってこれを証明することができます。

$$\begin{array}{rlrl}\mathsf{swap}(\mathsf{swap}(x,y))& =\mathsf{swap}(y,x)& & \text{（内側の }\mathsf{swap}\text{ の定義を展開）}\\ & =(x,y).& & \text{（外側の }\mathsf{swap}\text{ の定義を展開）}\end{array}$$

ここで重要なのは、この性質はプログラムを実行することによって特定の値に対して証明されたのではなくて、参照透過性によって可能な等価な式への代数的書き換えによって数学的に証明されたということです。 このようにして行われるプログラムの論証こそが Equational Reasoning（等式推論） です。 こうした推論を行うことにより、非自明な関数の同値性を論証したり、それによって振舞いを不変にしたまま実行効率を改善することができるのが Equational Reasoning の面白いところです。

進んだ注：評価戦略について

Warning

この節を読み飛ばしても本筋を理解することはできます。

厳密には、このような変形の正当性は Haskell の評価戦略に依存しています。 例えば OCaml や Scheme のような一般的な関数型言語の評価戦略は値呼び戦略（call-by-value）と呼ばれ、関数適用の際に先に引数を評価します。 一方で、Haskell は名前呼び戦略（call-by-name）³を採用しており、実際に値が必要になるまで評価を遅延しています。

この性質はプログラムの代数的書き換えを考えるときに本質的です。 例えば、次で定義される const 関数を考えます。

const :: a -> b -> a
const x y = x

なにか論証の仮定で等式 $\mathsf{const}xy=x$ を利用して書き換えを行ったことを考えます。 問題となるのは、項 $\mathsf{const}1\perp$ です。 ここで $\perp$ というのは意味論的に無限ループや例外によって停止しない項だとします。

名前呼び戦略で $\mathsf{const}1\perp$ を評価すると、最初に評価されるのは $\mathsf{const}$ の展開であり、$\perp$ は評価されず即座に全体が $1$ に簡約されます。 しかし、値呼び戦略では $\mathsf{const}$ の展開の前に引数の $\perp$ が評価され、全体の評価は停止しません。 これは $\mathsf{const}xy=x$ の反例になってしまっています。

参照透過性に加えて名前呼び戦略によって担保される簡約の完全性がないと、今回のような議論をすることはできません。

Equational Reasoning 実践

実際に Equational Reasoning をすることで、アルゴリズムの計算量を改善できることを確認していきます。

例 1. reverse

list に対する reverse を naive に定義してみると、次のようになるでしょう。

reverse :: [a] -> [a]
reverse [] = []
reverse (x : xs) = reverse xs ++ [x]

実はこのプログラムの計算量は $\Theta (n^2)$ になっています。 これはなぜでしょうか？ Haskell における list の結合演算子 ++ は次のように定義されています。

(++) :: [a] -> [a] -> [a]
(++) [] ys = ys
(++) (x : xs) ys = x : xs ++ ys

つまり、(++) は左辺に対して線型の計算量を必要としています。 引数のリストの長さ $n$ に対して reverse の計算量 $T(n)$ は $T(n)\sim (n-1)+T(n-1)$ というような漸化式を満たすため、$T(n)=\Theta (n^2)$ となっているのでした。

しかし、reverse なんて in-place に swap していけば $\Theta (n)$ で実装できるはずです。 純粋性を犠牲にしないと高速な定義は得られないのか……、そう思ったときが Equational Reasoning チャンス！！！

突然ですが、次のような関数 reverse' :: [a] -> [a] -> [a] を考えてみることにします。

$$\mathsf{revers}{\mathsf{e}}^{\prime }xsys=\mathsf{reverse}xs++ys.$$

第二引数として新たに list を取り、第一引数の反転にくっつけるというだけの関数です。 ここで、reverse と $\mathsf{reverse}$ は意味論的には同値な式を表現していますが、この式は Haskell コードではなくプログラムの代数的な性質なので、数式を用いることにします。 ニュアンスとしては $\mathsf{reverse}$ は「list を反転させる関数」を表現していて、reverse はその実装のひとつだと思ってもらえればよいと思います。

さらに重要なことは、この式は reverse' の定義ではなくて $\mathsf{revers}{\mathsf{e}}^{\prime }$ の特徴付けであるということです。 これは $\mathsf{reverse}$ による $\mathsf{revers}{\mathsf{e}}^{\prime }$ の特徴付けを与えていますが、自明な十分条件として逆方向の特徴付けをすることができます。

$$\mathsf{reverse}xs=\mathsf{revers}{\mathsf{e}}^{\prime }xs[].$$

今の状況を整理すると次のようになっています。

• $\mathsf{reverse}$ の効率的な定義を与えたいが、自然な実装 reverse は非効率である。
• $\mathsf{reverse}$ と $\mathsf{revers}{\mathsf{e}}^{\prime }$ は自明な特徴付けによって互いに導出することができる。

実は、これらの自明な制約から、Equational Reasoning 、つまり代数的な等式変形を行うことによって $\mathsf{revers}{\mathsf{e}}^{\prime }$ の効率的な実装 reverse' を与えることができるのです！

これはあくまでアナロジーですが、線型代数で例えると、$\mathsf{reverse},\mathsf{revers}{\mathsf{e}}^{\prime }$ は線型写像で、reverse は標準的な基底による $\mathsf{reverse}$ の行列表示です。 行列表示 reverse と $\mathsf{reverse},{\mathsf{reverse}}^{\prime }$ 間の代数的関係を用いた等式変形により、性質のよい行列表示 reverse' を導くというのが今からしようとしていることです。

$\mathsf{revers}{\mathsf{e}}^{\prime }$ の定義を $xs$ 上で帰納的に与えることを考えます。 まずは $xs=[]$ の場合の定義を考えます。

$$\begin{array}{rlrl}{\mathsf{reverse}}^{\prime }[]ys& =\mathsf{reverse}[]++ys& & \text{（特徴付け）}\\ & =[]++ys& & \text{（}\mathsf{reverse}\text{ の定義）}\\ & =ys.& & \text{（}++\text{ の定義）}\end{array}$$

得られる結果は自明なものですが、注目すべきは今までに判明している自明な代数的関係と reverse の定義を等式の変形に用いることで、$\mathsf{revers}{\mathsf{e}}^{\prime }$ に定義が与えられているというところです。 次は帰納パートについて考えてみましょう。

$$\begin{array}{rlrl}{\mathsf{reverse}}^{\prime }(x:xs)ys& =\mathsf{reverse}(x:xs)++ys& & \text{（特徴付け）}\\ & =(\mathsf{reverse}xs++[x])++ys& & \text{（}\mathsf{reverse}\text{ の定義）}\\ & =\mathsf{reverse}xs++([x]++ys)& & \text{（}++\text{ の結合則）}\\ & ={\mathsf{reverse}}^{\prime }xs([x]++ys)& & \text{（特徴付け）}\\ & ={\mathsf{reverse}}^{\prime }xs(x:ys).& & \text{（}++\text{ の定義）}\end{array}$$

なんだかガチャガチャやっていたら reverse にも ++ にも依らない $\mathsf{revers}{\mathsf{e}}^{\prime }$ の非自明な定義が得られていてびっくり！ しかもこの reverse' は length xs に対して線型の計算量で動作します！ ここまでの議論をまとめて Haskell コードにしておきます。

効率的な reverse

reverse' :: [a] -> [a] -> [a]
reverse' [] ys = ys
reverse' (x : xs) ys = reverse' xs (x : ys)
 
reverse :: [a] -> [a]
reverse xs = reverse' xs []

このように、代数的な等式変形によってプログラムについて論証することができ、さらに満たすべき制約から定義を導出できるというのが Equational Reasoning のスゴイところです。 これは、定義から満たすべき制約を証明する定理証明支援系に対して逆方向の議論を行っているという見方もできます。

例 2. flatten on Tree

次のような木構造と、それを平坦化する関数を考えることにします。

data Tree a
  = Leaf a
  | Node (Tree a) (Tree a)
 
flatten :: Tree a -> [a]
flatten (Leaf x) = [x]
flatten (Node lhs rhs) = flatten lhs ++ flatten rhs

自然な定義には忌々しい ++ が定義に現れていて、そのために計算量は最悪 $\Theta (n^2)$ になっています。 例えば左線型文法の導出木のような形状の二分木に対して最悪計算量が達成されます。

純粋性を犠牲にしないと高速な実装は得られないのか……、そう思ったときが Equational Reasoning チャンス！！！2 この flatten も同様のテクニックによって効率化することができます。

先程と同じように、次のような関数 flatten' :: Tree a -> [a] -> [a] を考えてみることにします。

$${\mathsf{flatten}}^{\prime }txs=\mathsf{flatten}t++xs.$$

先程と全く同様にして、$\mathsf{flatten}$ による $\mathsf{flatte}{\mathsf{n}}^{\prime }$ の特徴付けは自明な十分条件として逆方向の特徴付けを導きます。

$$\mathsf{flatten}t={\mathsf{flatten}}^{\prime }t[].$$

今の状況を整理すると次のようになっています。

• $\mathsf{flatten}$ の効率的な実装を与えたいが、自然な実装 flatten は非効率である。
• $\mathsf{flatten}$ と $\mathsf{flatte}{\mathsf{n}}^{\prime }$ は自明な特徴付けによって互いに導出することができる。

先程と全く同じ状況になったので、等式変形をして flatten' の定義を与えることができそうです。 Tree に対して帰納的に定義することを考えて、まずは基底パートを与えます。

$$\begin{array}{rlrl}{\mathsf{flatten}}^{\prime }(\mathtt{Leaf}x)xs& =\mathsf{flatten}(\mathtt{Leaf}x)++xs& & \text{（特徴付け）}\\ & =[x]++xs& & \text{（}\mathsf{flatten}\text{ の定義）}\\ & =x:xs.& & \text{（}++\text{ の定義）}\end{array}$$

次に帰納パートです。

$$\begin{array}{rlrl}{\mathsf{flatten}}^{\prime }(\mathtt{Node}lhsrhs)xs& =\mathsf{flatten}(\mathtt{Node}lhsrhs)++xs& & \text{（特徴付け）}\\ & =(\mathsf{flatten}lhs++\mathsf{flatten}rhs)++xs& & \text{（}\mathsf{flatten}\text{ の実装）}\\ & =\mathsf{flatten}lhs++(\mathsf{flatten}rhs++xs)& & \text{（}++\text{ の結合則）}\\ & ={\mathsf{flatten}}^{\prime }lhs(\mathsf{flatten}rhs++xs)& & \text{（特徴付け；外側）}\\ & ={\mathsf{flatten}}^{\prime }lhs({\mathsf{flatten}}^{\prime }rhsxs).& & \text{（特徴付け；内側）}\end{array}$$

なんだかまたガチャガチャやっているだけで flatten' の非自明かつ効率的な定義を得てしまいました。 実際、帰納法によって flatten' が木のサイズに対して線型に動作することがわかります。 Equational Reasoning サイコー！

効率的な flatten

data Tree a
  = Leaf a
  | Node (Tree a) (Tree a)
 
flatten' :: Tree a -> [a] -> [a]
flatten' (Leaf x) xs = x : xs
flatten' (Node lhs rhs) xs = flatten' lhs (flatten' rhs xs)
 
flatten :: Tree a -> [a]
flatten t = flatten' t []

例 3. fold, map, concat の性質

Equational Reasoning はアルゴリズムの導出にも使えますが、プログラムの論証に用いることもできます。 ここでは例として fold, map, concat について見ることにします。

まず準備として、$\mathsf{map}$ や $\mathsf{fold}$ について成立する命題を確認しておきます。 これらは次のように定義されているものとします。

map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x : xs) = f x : map f xs
 
foldl :: (b -> a -> b) -> b -> [a] -> b
foldl f z [] = z
foldl f z (x : xs) = foldl f (f z x) xs
 
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (x : xs) = f x (foldr f z xs)

Info

$(\oplus ,0)$ をモノイドとして、

$$\mathsf{foldl}(\oplus )0=\mathsf{foldr}(\oplus )0$$

が成り立ちます。 これは First Duality Theorem と呼ばれていて、これ自体後述するような帰納法によって証明することができますが、今回はこれを明らかなものとして認めることにします。 こういった文脈では $\mathsf{foldl}$ と $\mathsf{foldr}$ を区別せずに単に $\mathsf{fold}$ と書くことにします。 つまり、$\mathsf{fold}$ と書かれていたらその $\mathsf{fold}$ には可換な二項演算とその単位元が与えられていることが暗に仮定されているということです。 基本的に $\mathsf{foldr}$ の方が性質がよいので、このような状況では証明には foldr の定義を使用することします。

$\mathsf{fold}$ によって $\mathsf{concat}$ と $\mathsf{maximum}$ を用意しておきます。

$$\begin{array}{rl}\mathsf{sum}& =\mathsf{fold}(+)0,\\ \mathsf{product}& =\mathsf{fold}(\times )1,\\ \mathsf{concat}& =\mathsf{fold}(++)[],\\ \mathsf{maximum}& =\mathsf{fold}\mathsf{max}(-\infty ).\end{array}$$

ここからは、いくつかの有用な命題を証明していきます。

map の関手性

次の等式が成り立ちます。

$$\begin{array}{rlrl}(\mathsf{map}g)\circ (\mathsf{map}f)& =\mathsf{map}(g\circ f).& & \text{（}\mathsf{map}\text{の関手性）}\end{array}$$

関数型プログラミングに慣れているなら特に驚きはないと思います。 この等式は $\mathsf{map}$ の分配則とか map-map rule とも呼ばれるようですが、今回は $\mathsf{map}$ の関手性と呼ぶことにします（圏論はかっこいいので）。 また、そもそも今回は「$\mathsf{map}$ の分配則」を別の意味（$\circ$ ではなく $++$ に対して）で使います。

この等式は 2 つのループを 1 つのループにまとめているという見方ができます。 この意味で、こういったタイプの等式は loop fusion と呼ばれています。

証明

引数 $xs$ の長さについての帰納法。 $xs=[]$ のときは map の実装から明らか。 帰納部は次のようにして証明できる。

$$\begin{array}{rlrl}\mathsf{map}(g\circ f)(x:xs)& =(g\circ f)x:(\mathsf{map}(g\circ f)xs)& & \text{（}\mathsf{map}\text{ の定義）}\\ & =(g\circ f)x:((\mathsf{map}g)\circ (\mathsf{map}f)xs)& & \text{（帰納法の仮定）}\\ & =g(fx):(\mathsf{map}g((\mathsf{map}f)xs))& & \text{（}\circ \text{ の定義）}\\ & =\mathsf{map}g(fx:(\mathsf{map}f)xs)& & \text{（}\mathsf{map}\text{ の定義）}\\ & =\mathsf{map}g(\mathsf{map}f(x:xs))& & \text{（}\mathsf{map}\text{ の定義）}\\ & =(\mathsf{map}g)\circ (\mathsf{map}f)(x:xs).& & \text{（}\circ \text{ の定義）}\end{array}$$

map promotion

次の等式が成り立ちます。

$$\begin{array}{rlrl}\mathsf{map}f\circ \mathsf{concat}& =\mathsf{concat}\circ \mathsf{map}(\mathsf{map}f).& & \text{（map promotion）}\end{array}$$

一瞬ギョっとしますが、落ち着いて考えればそんなに難しい式ではありません。 concat してから map するのと、それぞれに map してから concat するのは同じというだけです。 この命題は $\mathsf{map}$ と $\mathsf{concat}$ するために使うことになります。

証明

例によって帰納法です。 基底部は省略します。

$$\begin{array}{rlrl}(\mathsf{map}f\circ \mathsf{concat})(xs:xss)& =\mathsf{map}f(\mathsf{concat}(xs:xss))& & \text{（}\circ \text{ の定義）}\\ & =\mathsf{map}f(xs++\mathsf{concat}xss)& & \text{（}\mathsf{concat}\text{ の定義）}\\ & =\mathsf{map}fxs++\mathsf{map}f(\mathsf{concat}xss)& & \text{（}\mathsf{map}\text{ の分配則）}\\ & =\mathsf{map}fxs++\mathsf{concat}(\mathsf{map}(\mathsf{map}f)xss)& & \text{（帰納法の仮定）}\\ & =\mathsf{concat}(\mathsf{map}fxs:\mathsf{map}(\mathsf{map}f)xss)& & \text{（}\mathsf{concat}\text{ の定義）}\\ & =\mathsf{concat}(\mathsf{map}(\mathsf{map}f)(xs:xss))& & \text{（}\mathsf{map}\text{ の定義）}\\ & =(\mathsf{concat}\circ \mathsf{map}(\mathsf{map}f))(xs:xss)& & \text{（}\circ \text{ の定義）}\end{array}$$

ここで、次の等式を「$\mathsf{map}$ の分配則」として利用しました。これも今までと同様に証明できるので、証明は省略します。

$$\begin{array}{rlrl}\mathsf{map}(xs++ys)& =\mathsf{map}(xs)++\mathsf{map}(ys).& & \text{（}\mathsf{map}\text{ の分配則）}\end{array}$$

fold promotion

モノイド$(\oplus ,0)$ に対して次の等式が成り立ちます。

$$\begin{array}{rlrl}(\mathsf{fold}(\oplus )0)\circ \mathsf{concat}& =(\mathsf{fold}(\oplus )0)\circ \mathsf{map}(\mathsf{fold}(\oplus )0).& & \text{（fold promotion）}\end{array}$$

さすがにギョっとしますが、$\mathsf{f}=\mathsf{fold}(\oplus )0$ とするともう少しシンプルになります。

$$\begin{array}{rlrl}\mathsf{f}\circ \mathsf{concat}& =\mathsf{f}\circ \mathsf{map}\mathsf{f}.& & \text{（fold promotion）}\end{array}$$

随分かっこいい見た目ですね。例えば $\mathsf{concat}$ や $\mathsf{sum}$ が $\mathsf{f}$ の instance です。 これも意味を考えればそんなに難しくはなくて、concat してから fold するのと、それぞれ fold してからそれらを fold するのは同じというだけです。

証明

理学部情報科学科たるもの帰納法は回せるだけ回せ！

$$\begin{array}{rlrl}(\mathsf{f}\circ \mathsf{concat})(xs:xss)& =\mathsf{f}(xs++\mathsf{concat}xss)& & \text{（}\mathsf{concat}\text{ の定義）}\\ & =\mathsf{f}xs\oplus \mathsf{f}(\mathsf{concat}xss)& & \text{（}\mathsf{fold}\text{ の準同型性）}\\ & =\mathsf{f}xs\oplus (\mathsf{f}\circ \mathsf{concat})xss& & \text{（}\circ \text{ の定義）}\\ & =\mathsf{f}xs\oplus (\mathsf{f}\circ \mathsf{map}\mathsf{f})xss& & \text{（帰納法の仮定）}\\ & =\mathsf{f}xs\oplus \mathsf{f}(\mathsf{map}\mathsf{f}xss)& & \text{（}\circ \text{ の定義）}\\ & =\mathsf{f}(\mathsf{f}xs:\mathsf{map}\mathsf{f}xss)& & \text{（}\mathsf{fold}\text{ の定義）}\\ & =\mathsf{f}(\mathsf{map}\mathsf{f}(xs:xss))& & \text{（}\mathsf{map}\text{ の定義）}\\ & =(\mathsf{f}\circ \mathsf{map}\mathsf{f})(xs:xss).& & \text{（}\circ \text{ の定義）}\end{array}$$

ここで、次の等式を「$\mathsf{fold}$ の準同型性」として利用しました。 $\mathsf{fold}$ は $(++,[])$ から $(\oplus ,0)$ へのモノイド準同型になっているというわけです。

$$\begin{array}{rlr}\mathsf{f}(xs++ys)=\mathsf{f}xs\oplus \mathsf{f}ys.& & \text{（}\mathsf{fold}\text{ の準同型性）}\end{array}$$

これも意味論的には自明なので証明は省略します。

例 4. scan, inits, tails

scan 系の関数も定義しておきます。

scanl :: (b -> a -> b) -> b -> [a] -> [b]
scanl f z [] = [z]
scanl f z (x : xs) = z : scanl f (f z x) xs
 
-- >>> scanl (+) 0 [1, 2, 3]
-- [0,1,3,6]
 
scanr :: (a -> b -> b) -> b -> [a] -> [b]
scanr f z [] = [z]
scanr f z (x : xs) = f x q : qs
  where
    qs@(q : _) = scanr f z xs
 
-- >>> scanr (+) 0 [1, 2, 3]
-- [6,5,3,0]
 
inits :: [a] -> [[a]]
inits = scanl (\xs x -> xs ++ [x]) []
 
-- >>> inits [1, 2, 3]
-- [[],[1],[1,2],[1,2,3]]
 
tails :: [a] -> [[a]]
tails = scanr (:) []
 
-- >>> tails [1, 2, 3]
-- [[1,2,3],[2,3],[3],[]]

また、あとで使うのでペアに対する fst も定義しておきます。

fst :: (a, b) -> a
fst (x, _) = x

scan lemma

モノイド $(\oplus ,0)$ と任意な値 $a$ について次の等式が成り立ちます。

$$\begin{array}{rlr}\mathsf{map}(\mathsf{foldl}(\oplus )a)\circ \mathsf{inits}=\mathsf{scanl}(\oplus )a.& & \text{（}\mathsf{scan}\text{ lemma）}\end{array}$$

これは $\mathsf{foldr}$ に対しては成立しないことに注意してください。 これもカジュアルな $\mathsf{scanl}$ の理解の下では当たり前の等式です。 そろそろ証明を書くのに疲れてきたので、具体例で確かめておくに留めます。

Example

$$\begin{array}{rl}& (\mathsf{map}(\mathsf{foldl}(\oplus )a)\circ \mathsf{inits})[x_1,x_2,x_3]\\ & =(\mathsf{map}(\mathsf{foldl}(\oplus )a))[[],[x_1],[x_1,x_2],[x_1,x_2,x_3]]\\ & =[a,a\oplus x_1,(a\oplus x_1)\oplus x_2,((a\oplus x_1)\oplus x_2)\oplus x_3]\\ & =\mathsf{scanl}(\oplus )a[x_1,x_2,x_3].\end{array}$$

この補題は本質的な計算量改善を表現しています。左辺では一旦 $\mathsf{inits}$ を計算するために $\Theta (n^2)$ の計算量がかかっていますが、右辺は $\mathsf{inits}$ を介さない in-place な計算を行うため、$\oplus$ が定数時間で計算できれば、$\Theta (n^2)$ の計算を $\Theta (n)$ に改善することができるのです。

fold-scan fusion

$(\oplus ,0),(\otimes ,1)$ が半環をなすとします。 つまり、$(\oplus ,0)$ は可換モノイド、$(\otimes ,1)$ はモノイドであり、$\oplus$ に対して $\otimes$ は分配するものとします（正確には $\oplus$ の可換性さえ必要ありません）。 このとき、任意の値 $a,b$ について 次の等式が成り立ちます。

$$\begin{array}{rlrl}\mathsf{foldl}(\oplus )a\circ \mathsf{scanl}(\otimes )b& =\mathsf{fst}\circ \mathsf{foldl}(\ast )(a\oplus b,b).& & \text{（}\mathsf{fold}\text{-}\mathsf{scan}\text{ fusion）}\end{array}$$

ただし、$(\ast )$ は次によって定められる演算です。

$$\begin{array}{rlrl}(u,v)\ast x& =(u\oplus w,w)& & \text{where }w=v\otimes x.\end{array}$$

これも $\mathsf{foldr}$ に対しては成立しないことに注意してください（そもそも $(\ast )$ は引数の型が違うので可換にはなりえませんね）。 とりあえずこれも 2 回のループを 1 回にまとめる loop fusion と呼ばれるタイプの等式であることが観察できます。 しかしこれはなかなか非自明に見えます。 とりあえずフルで証明をしてみることにします。

証明

まず基底パートです。

$$\begin{array}{rlrl}(\mathsf{foldl}(\oplus )a\circ \mathsf{scanl}(\otimes )b)[]& =\mathsf{foldl}(\oplus )a(\mathsf{scanl}(\otimes )b[])& & \text{（}\circ \text{ の定義）}\\ & =\mathsf{foldl}(\oplus )a[b]& & \text{（}\mathsf{scanl}\text{ の定義）}\\ & =\mathsf{foldl}(\oplus )(a\oplus b)[]& & \text{（}\mathsf{foldl}\text{ の定義）}\\ & =a\oplus b& & \text{（}\mathsf{foldl}\text{ の定義）}\\ & =\mathsf{fst}(a\oplus b,b)& & \text{（}\mathsf{fst}\text{ の定義）}\\ & =\mathsf{fst}(\mathsf{foldl}(\ast )(a\oplus b,b)[])& & \text{（}\mathsf{foldl}\text{ の定義）}\\ & =(\mathsf{fst}\circ \mathsf{foldl}(\ast )(a\oplus b,b))[].& & \text{（}\circ \text{ の定義）}\end{array}$$

次に帰納パートです。

$$\begin{array}{rlrl}(\mathsf{foldl}(\oplus )a\circ \mathsf{scanl}(\otimes )b)(x:xs)& =\mathsf{foldl}(\oplus )a(b:\mathsf{scanl}(\otimes )(b\otimes x)xs)& & \text{（}\mathsf{scanl}\text{ および }\circ \text{ の定義）}\\ & =\mathsf{foldl}(\oplus )(a\oplus b)(\mathsf{scanl}(\otimes )(b\otimes x)xs)& & \text{（}\mathsf{foldl}\text{ の定義）}\\ & =(\mathsf{fst}\circ \mathsf{foldl}(\ast )((a\oplus b)\oplus (b\otimes x),b\otimes x))xs& & \text{（帰納法の仮定）}\\ & =(\mathsf{fst}\circ \mathsf{foldl}(\ast )((a\oplus b,b)\ast x))xs& & \text{（}\ast \text{ の定義）}\\ & =(\mathsf{fst}\circ \mathsf{foldl}(\ast )(a\oplus b,b))(x:xs).& & \text{（}\mathsf{foldl}\text{ および }\circ \text{ の定義）}\end{array}$$

証明自体はいつものように straight-forward な帰納法で終わりましたが、まだ直感的には理解できていません。 この等式も適用例を考えてみることで、直感的な理解を得られることができます。

Example

$\oplus =+,\otimes =\times ,a=0,b=1$ とすると表式は次のように書き換えることができます。

$$\mathsf{sum}\circ \mathsf{scanl}(\times )1=\mathsf{fst}\circ \mathsf{foldl}(\ast )(1,1).$$

ただし、$(u,v)\ast x=(u+vx,vx)$ です。

例えば $[x_1,x_2,x_3]$ に両辺を適用してみます。

$$\begin{array}{rl}(\mathsf{sum}\circ \mathsf{scanl}(\times )1)[x_1,x_2,x_3]& =\mathsf{sum}[1,x_1,x_1{x}_2,x_1{x}_2{x}_3]\\ & =1+x_1+x_1{x}_2+x_1{x}_2{x}_3,\\ (\mathsf{fst}\circ \mathsf{foldl}(\ast )(1,1))[x_1,x_2,x_3]& =\mathsf{fst}(\mathsf{foldl}(1+x_1,x_1)[x_2,x_3])\\ & =\mathsf{fst}(\mathsf{foldl}(1+x_1+x_1{x}_2,x_1{x}_2)[x_3])\\ & =\mathsf{fst}(\mathsf{foldl}(1+x_1+x_1{x}_2+x_1{x}_2{x}_3,x_1{x}_2{x}_3)[])\\ & =\mathsf{fst}(1+x_1+x_1{x}_2+x_1{x}_2{x}_3,x_1{x}_2{x}_3)\\ & =1+x_1+x_1{x}_2+x_1{x}_2{x}_3.\end{array}$$

これは、$1+x_1+x_1{x}_2+x_1{x}_2{x}_3$ という量を計算するときにこれをそのまま計算するのではなくて、次のような計算をしてもよいということです（これは後述する Horner 法と同じことを言っています）。

int f(std::vector<int> a) {
    int u = 1, v = 1;
    for (const auto &x : a) {
        v *= x;
        u += v;
    }
    return u
}

explicit に unfold してから fold するのではなくて、in-place に fold することで計算量が削減できていることがわかります。 fold-scan fusion は、このようにある種の二重ループを一重ループに融合するテクニックなのです。

例 5. 最大部分和問題：Kadane のアルゴリズム

最後にもっと非自明な計算量改善を考えてみましょう。 整数のリストの最大部分和（Max Segment Sum; MSS） とは、リストの連続する部分であって和が最大であるようなものです。 この和を求めるのが最大部分和問題です。

区間は $\Theta (n^2)$ 通りあるので、naive なアルゴリズムでは $\Theta (n^3)$、和を求めるのに累積和を計算しておけば $\Theta (n^2)$ になります。 また、左端を含む最大部分和、右端を含む最大部分和、特に制約のない最大部分和を持って分割統治することで $\Theta (n\log n)$ を達成することもできます。 しかし、この問題は Kadane のアルゴリズムによって $\Theta (n)$ で解けることが知られています。

C++ による Kadane のアルゴリズムの実装

int mss(std::vector<int> a) {
    int best = 0, current = 0;
    for (const auto& x : a) {
        current = std::max(x, current + x);
        best = std::max(best, current);
    }
    return best;
}

詳細は [3] に譲りますが、これは割と技巧的で、文字列アルゴリズムとかにありがちな天才パズルに近いです。 しかし、このアルゴリズムも Equational Reasoning によって機械的に導出することができるのです！

準備：Horner 法

Horner 法というのは、多項式の評価に要する演算数を節約する初等的なテクニックです。 たぶん例を見た方が早くて、

$$x^3+2x^2+3x+4=((x+2)x+3)x+4.$$

みたいなやつです。 これをアイデアにして、次のような等式を得ることができます。

Horner 法

$$\begin{array}{rlrl}\mathsf{sum}\circ \mathsf{map}\mathsf{product}\circ \mathsf{tails}& =\mathsf{foldl}(\odot )1.& & \text{（Horner）}\end{array}$$

ただし、$x\odot y=x\times y+1.$

Example

$[x_1,x_2,x_3]$ に適用すると、次のようになります。

$$x_1{x}_2{x}_3+x_2{x}_3+x_3+1=((x_1+1)x_2+1)x_3+1.$$

証明は頑張って頑張るとできます。詳細は [4] 参照。

当たり前ですが、これは一般の半環上でも成立します。 半環というのは環の定義から加法逆元を抜いたもののことで、可換モノイド $(\oplus ,0)$ 上にモノイド $(\otimes ,1)$ が分配するやつのことです。 正確には $\oplus$ の可換性さえ必要ないはずですが、特には気にしないことにします。

$\oplus =\mathsf{max},\otimes =+$ とすると、これは半環になっています。 モノイド性は簡単に確認できて、$\mathsf{max}(a,c)+b=\mathsf{max}(a+c,b+c)$ が分配則になっています。 この半環は max-plus 代数だとかトロピカル代数と呼ばれているようです。 このバージョンの Horner 法は次のようになっています。

Horner 法 @ max-plus

$$\begin{array}{rlrl}\mathsf{maximum}\circ \mathsf{map}\mathsf{sum}\circ \mathsf{tails}& =\mathsf{foldl}(\odot )0.& & \text{（tropical Horner）}\end{array}$$

ただし、$x\odot y=\mathsf{max}(x+y,0).$ ここで $0$ というのは単に $+$ の単位元であって、max-plus 代数における「加法」$\mathsf{max}$ の単位元を表しているわけではない。

Kadane のアルゴリズムの導出

やっと本題です。 最大部分和（Maximum Segment Sum）を求める関数を $\mathsf{mss}$ とします。 今までの道具立てを使うと、とりあえず $\mathsf{mss}$ は次のように書けます。

$$\mathsf{mss}=\mathsf{maximum}\circ \mathsf{map}\mathsf{sum}\circ \mathsf{segs}.$$

ここで、

$$\mathsf{segs}=\mathsf{concat}\circ \mathsf{map}\mathsf{tails}\circ \mathsf{inits}$$

と定めました。 $\mathsf{segs}$ は連続部分列を「prefix の suffix」と見てこれを列挙する関数になっています。

Example

$$\begin{array}{rl}\mathsf{segs}[x_1,x_2,x_3]& =(\mathsf{concat}\circ \mathsf{map}\mathsf{tails}\circ \mathsf{inits})[x_1,x_2,x_3]\\ & =(\mathsf{concat}\circ \mathsf{map}\mathsf{tails})[[],[x_1],[x_1,x_2],[x_1,x_2,x_3]]\\ & =\mathsf{concat}[\\ & [[]],\\ & [[x_1],[]],\\ & [[x_1,x_2],[x_2],[]],\\ & [[x_1,x_2,x_3],[x_2,x_3],[x_3],[]]\\ & ]\\ & =[[],[x_1],[],[x_1,x_2],[x_2],[],[x_1,x_2,x_3],[x_2,x_3],[x_3],[]].\end{array}$$

$\mathsf{segs}xs$ は長さ $\Theta (n^2)$ のリストを生成して、$\mathsf{sum}$ が $\Theta (n)$-time なので $\mathsf{segs}$ でどんなに頑張ってもこのままでは $\Theta (n^3)$ です。

次のような Equational Reasoning をします。

$$\begin{array}{rlrl}\mathsf{mss}& =\mathsf{maximum}\circ \mathsf{map}\mathsf{sum}\circ \mathsf{segs}& & \text{（}\mathsf{mss}\text{ の定義）}\\ & =\mathsf{maximum}\circ \mathsf{map}\mathsf{sum}\circ \mathsf{concat}\circ \mathsf{map}\mathsf{tails}\circ \mathsf{inits}& & \text{（}\mathsf{segs}\text{ の定義）}\\ & =\mathsf{maximum}\circ \mathsf{concat}\circ \mathsf{map}(\mathsf{map}\mathsf{sum})\circ \mathsf{map}\mathsf{tails}\circ \mathsf{inits}& & \text{（map promotion）}\\ & =\mathsf{maximum}\circ \mathsf{map}\mathsf{maximum}\circ \mathsf{map}(\mathsf{map}\mathsf{sum})\circ \mathsf{map}\mathsf{tails}\circ \mathsf{inits}& & \text{（fold promotion）}\\ & =\mathsf{maximum}\circ \mathsf{map}(\mathsf{maximum}\circ \mathsf{map}\mathsf{sum}\circ \mathsf{tails})\circ \mathsf{inits}& & \text{（}\mathsf{map}\text{ の関手性）}\\ & =\mathsf{maximum}\circ \mathsf{map}(\mathsf{foldl}(\odot )0)\circ \mathsf{inits}& & \text{（tropical Horner）}\\ & =\mathsf{maximum}\circ \mathsf{scanl}\mathsf{foldl}(\odot )0& & \text{（tropical }\mathsf{scan}\text{ lemma）}\\ & =\mathsf{fst}\circ \mathsf{foldl}(\ast )(0,0).& & \text{（}\mathsf{fold}\text{-}\mathsf{scan}\text{ fusion）}\end{array}$$

ここで、各種演算は次のように定められていたのでした：

$$\begin{array}{rlrl}x\odot y& =\mathsf{max}(x+y,0),& & \\ (u,v)\ast x& =(\mathsf{max}(u,w),w)& & \text{where }w=\mathsf{max}(v+x,0).\end{array}$$

なんだかよくわかりませんが、$\Theta (n)$ に落ちています。 よく観察すると、Horner 法の適用と scan lemma の適用が本質的な計算量改善になっていて、それぞれで $n$ の指数がひとつずつ減っています。

ここで C++ による Kadane のアルゴリズムをもう一度見てみましょう。

C++ による Kadane のアルゴリズムの実装（再掲）

int mss(std::vector<int> a) {
    int best = 0, current = 0;
    for (const auto& x : a) {
        current = std::max(x, current + x);
        best = std::max(best, current);
    }
    return best;
}

これはまさに先程導出したアルゴリズムの命令型による実装を与えています！ fold の際に持っておく $(u,v)$ が (best, current) に対応していることがわかると思います。 天才パズルをせずに、代数的な変形を繰り返すことによって仕様からアルゴリズムを導出することができました！

おわりに

こんなに長くなる予定じゃなかったのになんか Kadane の準備にいろいろ必要だったのと普通に面白くて労働と学業が完全にストップしてしまった……

こんなに準備が必要なら意味ないというようにも思ってしまう気持ちもありますが、Horner 法はまだしも {map, fold} promotion や scan lemma, fold-scan fusion は汎用性のあるテクニックです。 こういったプログラムの性質を理解しておくことで見通しよくプログラムを書くことができるという利点もあります。

このような計算量改善は都合のよい例ですが、Equational Reasoning によるアルゴリズムの導出には、正当性の証明という利点もあります。 手続き的なアルゴリズムの表現に対してその正当性を証明することは往々して面倒な作業ですが、このようにしてアルゴリズムの導出そのものによってその正当性を保証するという考え方は Correct-by-Construction と呼ばれています。

Equational Reasoning には様々な応用があります。 例えば [6] では fusion や promotion といった性質をより一般化しモナドや圏の言葉で整理し、最大部分和問題について考察しています（かっこよすぎ！）。

また、このような代数的変形はコンパイラの最適化の文脈でも注目されています [7]。 項 x と x * 2 / 2 が（オーバーフローなどは考えないとして）等しいということは構文木のパターンマッチによって認識することができます。 このようにして等価であるとされた項を UnionFind の要領で管理するデータ構造は E-graph と呼ばれています。 どのような書き換えが効率的であるかというのは、ISA やそもそもハードウェアの性質に依存し、さらに書き換えの順序によっては最適な書き換えに到達できないかもしれません。 このような問題を解決するために提案されたのが、E-graph 上で書き換えを適用し続け、最適な書き換えを効率的かつ大域的に探索する手法であり、これは Equational Saturation と呼ばれていて、例えばディープラーニングのコンパイラやデータベースのクエリ最適化などで成功を収めているようです。

Equational Saturation は特に浮動小数点演算の効率化に向いていますし、独自の ISA や未知のハードウェアに対しても最適化をかけることができます。 一方でコンパイルの際に最適化をかけるので、コンパイル速度を犠牲にして実行速度をとるということになります。

いや～でも、なにか独自の CPU 上で、浮動小数点演算をたくさんするタイプの課題を解く、項書き換えに向く関数型言語で書かれた固定のプログラムについて、コンパイラを自作して、生成された機械語の実行速度を競う、なんて都合の良い機会、あるわけないか！！！！！

参考文献

[1] G. Hutton, プログラミング Haskell 第 2 版, 山本和彦訳, ラムダノート, 2019.

Haskell の入門書。読みやすくて、かつ内容も現代的で網羅的です。

[2] R. Bird, Pearls of Functional Algorithm Design. Cambridge, U.K.: Cambridge Univ. Press, 2010.

和訳は『関数プログラミング 珠玉のアルゴリズムデザイン』の原著。これは PDF が公開されています。

[3] ark4rk, Kadane’s Algorithm | 最大部分配列問題, Ark’s Blog, Jan. 8, 2018. [Online]. Available: https://ark4rk.hatenablog.com/entry/2018/01/08/002508. [Accessed: Dec. 18, 2025].

[4] R. S. Bird, Algebraic identities for program calculation, The Computer Journal, vol. 32, no. 2, pp. 122–126, Apr. 1989.

例 3 から 5 はここから取りました。読みやすいです。

[5] T. Sheard, Equational Reasoning, Lecture Notes, CS 457/557: Functional Languages, Portland State Univ., Portland, OR, USA. [Online]. Available: https://web.cecs.pdx.edu/~sheard/course/CS457-557/Notes/EquationalReasoning.pdf

[6] J. Gibbons, Maximum segment sum, monadically, arXiv preprint arXiv:1109.0782, 2011.

[7] R. Tate, M. Stepp, Z. Tatlock, and S. Lerner, Equality saturation: A new approach to optimization, in Proc. 36th Annu. ACM SIGPLAN-SIGACT Symp. Princ. Program. Lang. (POPL), Savannah, GA, USA, 2009, pp. 264–276.

Footnotes

1. このあたりは表示的意味論とかの議論が必要そうで、そんなに自信はないです。今回は基本的に停止しない関数だったり無限リストだったりは扱わないのでそのあたりはカジュアルにやっていきます。 ↩

2. 入出力は言語側でユーザの触れないブラックボックスとして提供して、ユーザ側からすれば純粋に扱えるようになっています。 ↩

3. 正確には最適化された変種の必要呼び戦略（call-by-need）を採用している。 名前呼び戦略は完全性という優れた性質を持っており、正規形に到達する評価が存在する項に対しては名前呼び戦略によって正規形に到達することができることが知られています。 ↩