muratak

:warning: これは 2017 年 12 月 8 日に執筆された記事を、Qiita から移植したものです。2020 年 3 月に見直してみると「ちょっとどうかな」と思うところもあるのですが、手を入れるのもめんどうなので、最低限、Markdown の処理環境が変化したことにより必要な修正等を除いてそのまま移植してます。

はじめに

この記事は， 数学とコンピュータⅡ Advent Calendar 2017 の 8 日目の記事です．

本記事では，私が最近知った楽しい定理の「第三リスト準同型定理」について書きたいと思います．私自身による新しい結果はなく，以下の article に基づきつつ，自分の言葉での解説を試みたもの (つまり劣化コピー？) です1．

もちろん，誤りなどのご指摘は有り難く承ります．できる限りいただいたご指摘には対処するつもりです．

記法の注意

Haskell風の記法を使います．あくまでHaskell”風”であって Haskell として動くコードではないことに注意してください(Haskell の シンタックスハイライトがなされていますが，すべてが動く Haskell コードというわけではありません)．

また，等式変形には，プログラム運算でよく見る次のような記法を用います(こちらも Haskell の シンタックスハイライトがなされていますが， 動く Haskell コードというわけではありません)：

   f x
==  {-- 補題hogeより -}
   g x
==  {-- 補題fugaより -}
   h x

これは，補題hogeによってf x == g xがいえ，さらに補題fugaによってg x == hxが言える，ということです．要するに，イコール(==)が成り立つ理由を，{--と-}の間に書いてあると言うことです[^-1]．

また， 本記事では， Markdown での

引用記法

を，引用のためではなく，定理の証明を書くために使います．

関数のイコールの扱いについて

以下はちょっと神経質な注意ですから，わからなければ無視しても構いません

．Haskell では， 関数は普通 Eq 型クラスに属していません．したがって，例えば

(\x -> x + 1) == (\x -> 1 + x)

を評価すると， True が返ってくるのではなく，「関数の等価性なんざ知らねえ（もしかして引数足りねんじゃね？）」という（ややお節介な）エラーが返ってくるはずです2：

    • No instance for (Eq (a0 -> a0)) arising from a use of ‘==’
        (maybe you haven't applied a function to enough arguments?)

一方，数学の世界では，関数の等価性は外延的等価性により定義されることが多いのではないかと思います(←よくわかっていないので，誤りがありましたら特にご指摘を歓迎します)．どういうことかというと，関数f :: a -> b と g :: a -> b が等しいとは，「任意のx :: aに対して，f x == g xが成り立つこと」というように定義します．つまり，関数fとgが等しいとは，(計算の過程や関数自体の定義がどうであっても，)fとgに同じ入力を与えると常に同じ出力が返ってくることだというわけです．本記事では，このことを f == g と書くことにします．

本題の前に：ちょっとだけ Haskell 関数の定義

さて，本題に入る前に，本稿で使う Haskell の関数をいくつか定義したいと思います．主にリスト操作関数を定義していくことになります3．

リストの結合 (++)

2つのリストを結合する演算子が(++)です．次のように定義できます．

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

畳み込みの foldr と foldl

Haskell ユーザーにとっては，2つの畳み込み foldr と foldl はお馴染みでしょう4

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr op e []     = e
foldr op e (x:xs) = x `op` (foldr op e xs) 

foldl :: (b -> a -> b) -> b -> [a] -> b
foldl op e []     = e
foldl op e (x:xs) = foldl op (e `op` x) xs

直観的には，foldr と foldl は以下のような計算をします．

foldr (⊙) e [x0,x1..xn] == x0 ⊙ (x1 ⊙ (... ⊙ (xn ⊙ e) ...))
foldl (⊙) e [x0,x1..xn] == (... ((e ⊙ x0) ⊙ x1) ⊙ ...) ⊙ xn

要するに，foldrは右から左に向かって畳み込み，foldlは左から右に向かって畳み込むわけです．

リストの構造に関する帰納法とfoldr/foldlの性質の証明

リスト[a]というデータ構造は，次のように帰納的に定義されています．

したがって，リスト型[a]についての性質 P を示したい時にはリストの構造に関する帰納法が使えます．P を示すには，以下のことをすればよいというわけです．

では，実際に帰納法を使って foldr について次の性質を示してみましょう．

補題1-1

任意の (⊙) :: a -> b -> b, x y :: [a] に対して，以下のことが成り立つ．

foldr (⊙) e (x ++ y) == foldr (⊙) (foldr (⊙) e y) x

証明

リスト x の構造に関する帰納法による．

1) [] のとき

   foldr (⊙) e ([] ++ y)
==  {-- (++) の定義より -}
   foldr (⊙) e y 
==  {-- foldr の定義より -}
   foldr (⊙) (foldr (⊙) e y) []

2) 帰納法の仮定として， x のとき結論が成り立つと仮定して， (h:x)のときも結論が成り立つことを示す．

   foldr (⊙) e ((h:x) ++ y)
==  {-- (++) の定義より -}
   foldr (⊙) e (h:(x ++ y))
==  {-- foldr の定義より -}
   h ⊙ (foldr (⊙) e (x ++ y)) 
==  {-- 帰納法の仮定より -}
   h ⊙ (foldr (⊙) (foldr (⊙) e y) x)
==  {-- foldr の定義より -}
   foldr (⊙) (foldr (⊙) e y) (h:x)

foldlについても同様の性質が成り立ちます．これは練習問題にしましょう．

補題1-2

任意の (⊙) :: a -> b -> b, x y :: [a] に対して，以下のことが成り立つ．

foldl (⊙) e (x ++ y) == foldl (⊙) (foldl (⊙) e x) y

証明

練習問題とする (xとyのどちらについての帰納法を使うかに注意！)．

リスト準同型関数

さて，第三リスト準同型定理定理のステートメント(主張)にも登場するリスト準同型関数なる概念を定義します．

リスト準同型関数

2項演算 (⊙) :: b -> b -> b に対し， 関数 h :: [a] -> b が ⊙-準同型(homomorphism) であるとは，任意の x y :: [a] に対して，

h (x ++ y) == (h x) ⊙ (h y)

がなりたつことです．また，単に h が準同型であるとは，ある2項演算子 (⊙) が存在して， h が⊙-準同型となっていることをいいます．

リスト準同型関数の例

例えば，和を求める関数 sum :: [Int] -> Int はリスト準同型関数です．なぜならば，

sum (x ++ y) == (sum x) + (sum y)

と表せるからです．

Leftwards と Rightwards

もう少し用語の定義をします．

2項演算子 (⊕) :: a -> b -> a に対して， h :: [a] -> b が ⊕-leftwards であるとは，

h = foldr (⊕) e
  where
    e = h []

となっていることであり，また h が単に leftwards であるとは，ある2項演算子(⊕)に対して ⊕-leftwards となっていることです．要するに foldr を使って定義できることですね．

同様に，h :: [a] -> b が ⊕-rightwards であるとは，

h = foldl (⊕) e
  where
    e = h []

となていることであり，h が単に rightwards であるとは，ある2項演算子(⊕)に対して ⊕-rightwards となっていることです．要するに foldl を使って定義できることです．

foldr で定義できるのに “Left”wards で， foldl で定義できるのに “Right”wards とは少しややこしい気がしますが，「foldrはリストを右から左へ畳み混むので『左方向へ計算が進んでいく』から”Left”wards，foldlはリストを左から右へたたみこむので『右方向へ計算が進んでいく』から”Right”wards」と思うと自然な気もします．

第三リスト準同型定理

さて，いよいよ第三リスト準同型定理のステートメントを紹介します．

定理(第三リスト準同型定理)

h が leftwards かつ rightwards ならば， h は準同型である．

第三リスト準同型定理の証明

以下では，第三リスト準同型定理の証明をします．そのためにいくつか補題を立てて示していきます．

補題2

型 a は要素を枚挙可能である (すなわち，x :: a となる x がすべて計算できる)5 とする．このとき，任意の計算可能な全域関数 h :: a -> b に対して，計算可能な部分関数 g :: b -> c が存在して，h . g . h = h となる．

補題2の証明

g を見つける方法は h 毎に様々であるが，一般的には次のようにして g を構成することができる． まず， a は要素を枚挙可能だから，aの要素を枚挙した(無限かもしれない)リストl = [x0,x1,x2..]が存在する．このlを用いると，

g t = dropWhile (/= t) $ map h l

としてg tを計算することができる．要するに， h x0, h x1, h x2, … を t が見つかるまで順に計算していって， h xi == t となった時点での xi を返すわけである．この g は必ずしも停止するとは限らないが6， g . h は必ず停止する7．したがって， (g . h) x = xi …(1) なる xi :: a が存在して， h xi == h x …(2) を満たしている．以上により，このgは，

   (h . g . h) x
==   {-- 合成 (.) の定義 -}
   h ((g . h) x)
==   {-- (1) より -}
   h xi
==   {-- (2) より -}
   h x

となるから，確かに h . g . h == h を満たしている．[証明終わり]

以下では，特に断らない限り， リスト関数 h :: [a] -> b は，全域でドメイン[a]が枚挙可能であるとします．

補題3

リスト関数 h :: [a] -> b についての以下の 2 つの条件は同値である．

  1. h はリスト準同型である．
  2. 任意の v w x y :: [a] に対して， h v == h x かつ h w == h y ならば， h (v ++ w) == h (x ++ y)．

補題3の証明

(1 ==> 2) h :: [a] -> b をリスト準同型とする．すると，ある 2 項演算子 ⊙ :: b -> b が存在して，hは⊙-準同型になる．したがって， h v == h x かつ h w == h y $\cdots$(a) とすれば，

   h (v ++ w)
==   {-- h は ⊙-準同型なので -} 
   (h v) ⊙ (h w)
==   {-- (a)より -}
   (h x) ⊙ (h y)
==   {-- h は ⊙-準同型なので -}
   h (x ++ y)

となる．

(2 ==> 1) h :: [a] -> b が，「任意の v w x y :: [a] に対して， h v == h x かつ h w == h y ならば， h (v ++ w) == h (x ++ y)」$\cdots$(b) を満たすと仮定する．補題 2 より， h . g . h == h を満たす g が存在するから，その g をとる．さらに，その g を用いて，二項演算子(⊙)を，

t ⊙ u = h (g t ++ g u)

と定義する．すると実は h は⊙-準同型になる．以下では h は⊙-準同型であることを示す． g の定義により， h x == h (g (h x)) かつ h y == h (g (h y)) $\cdots$(c) であることにに注意すれば，

   h (x ++ y)
==   {-- (b) と (c) より -}
   h (g (h x) ++ g (h y))
==   {-- ⊙ の定義より -}
   (h x) ⊙ (h y)

となるから， h は⊙-準同型である．[証明終わり]

さて，以上の準備のもと，いよいよ第三リスト準同型定理を示します．

定理(第三リスト準同型定理)【再掲】

h :: [a] -> b が leftwards かつ rightwards ならば， h は準同型である．

定理の証明

h :: [a] -> b が leftwards かつ rightwards であるとする． このhが，条件「任意の v w x y :: [a] に対して， h v == h x かつ h w == h y ならば， h (v ++ w) == h (x ++ y)」を満たしていることを示せば，あとは補題3によって h が準同型であることが示される．したがって以下では，hが前述の条件を満たしていることを示す．

h は leftwards かつ rightwards より，

h = foldr (⊕) e   where  e = h []   {-- h は leftwards なので -}
h = foldl (⊗) e   where  e = h []   {-- h は rightwards なので -}

を満たす (⊕)，(⊗) が存在する． いま，h v == h x かつ h w == h yとすると，

   h (v ++ w)
==   {-- h = foldr (⊕) e より -}
   foldr (⊕) e (v ++ w)
==   {-- 補題 1.1 より -}
   foldr (⊕) (foldr ⊕ e w) v
==   {-- h = foldr (⊕) e  より -}
   foldr (⊕) (h w) v
==   {-- h w == h y  より -}
   foldr (⊕) (h y) v
==   {-- h = foldr (⊕) e  より -}
   foldr (⊕) (foldr (⊕) e y) v
==   {-- 補題 1.1 より -}
   foldr (⊕) (v ++ y)
==   {-- h = foldr (⊕) e  より -}
   h (v ++ y)
==   {-- 今度は h = foldl (⊗) e を利用してこれまでと同様に変形すれば -}
   h (x ++ y)

となる．[証明終わり]

ソートの大変身

第三リスト準同型定理を使うと， insertion sort に使用する insert 関数から，ごく自然に merge sort に使用する merge を得ることができます．

左へ進む insertion sort と右へ進む insertion sort

まず， insertion sort は，以下のように， foldr を使った Haskell プログラム insertion_sortl として表せます(実際に動くコードです)．

insertion_sortl :: (Ord a) => [a] -> [a]
insertion_sortl = foldr ins []

ins :: (Ord a) => a -> [a] -> [a]
ins x []     = [x]
ins x (y:ys)
  | x <= y     = x : y : ys
  | otherwise  = y : (ins x ys)

また， foldl 版の insertion sort プログラム insertion_sortr も次のように書けます．

insertion_sortr :: (Ord a) => [a] -> [a]
insertion_sortr = foldl ins' []

ins' :: (Ord a) => a -> [a] -> [a]
ins' x y = ins y x

ソートの変身

さて，2つの insertion sort によって，ソートは foldl を使っても， foldr と使っても，どちらでも書けるということがわかりました．したがって， 第三リスト準同型定理より，ソートをする関数は準同型であることがわかります．ですから，sort == insertion_sortr == insertion_sortl を満たす sort に対して，

 sort (x ++ y) == (sort x) ⊙ (sort y)

を満たす(⊙)が存在することがわかります．

さて，この(⊙)は一体何者なのか分析するため，補題3の証明(2$\Longrightarrow$1)に立ち返ってみましょう．まず， sort は，条件2

を明らかに満たします(sortの意味を考えれば明らかでしょう)．また， sort . g . sort == sort を満たす関数 g として， g = id という関数があります(今回は，補題2を使うまでもなく簡単にgが見つかります)．実際，sort . id . sort == sort となることも，意味を考えれば明らかです．したがって，補題3の証明で (⊙) を構成したのと同じように，

 t ⊙ u = sort (id t ++ id u)

と構成します．この(⊙)は，

   t ⊙ u
==  {-- (⊙) の定義より -}
   sort (id t ++ id u)
==  {-- id の定義より -}
   sort (t ++ u)
==  {-- sort の定義より -}
   insertion_sortl (t ++ u)
==  {-- insertion_sortl の定義より -}
   foldl ins' [] (t ++ u)
==  {-- 補題 1.2 より -}
   foldl ins' (foldl ins' [] t) u
==  {-- 補題 1.2 より -}
   foldl ins' (sort t) u

さて，試しにtがソート済みである，すなわち，sort t == tであるとして，さらに変形してみましょう．

   foldl ins' (sort t) u
==  {-- sort t == t より -}
   foldl ins' t u

となります．すなわち，もしtがソート済みであるならば，t ⊙ u == foldl ins' t uとなるわけですから， ⊙は，まさにマージソートのmergeを表していることになるわけです．

ここからmergeのプログラムを得るのはもう難しくありません．merge t u = t ⊙ uとすれば，

   merge t [] 
==   {-- t ⊙ u == foldl ins' t u  より -}
   foldl ins' t []
==   {-- foldl の定義より -}
   t

かつ

   merge t (h:u)
==   {-- t ⊙ u == foldl ins' t u  より -}
   foldl ins' t (h:u)
==   {-- foldl の定義より -}
   foldl ins' (ins' t h) u
==   {-- t ⊙ u == foldl ins' t u  より -}
   merge (ins' t h) u

ですから，

merge t [] = t
merge t (h:u) = merge (ins' t h) u

なるプログラムが得られるわけです．もちろん，この merge は

sort (x ++ y) == (sort x) `merge` (sort y)

を満たします．

おわりに

最後はかなり駆け足になってしまいましたが，「第三リスト準同型定理」を紹介しました．ある人から紹介された article をほぼ半日で読んで半日で記事を書くという荒技(苦行)をやってしまいましたが，なかなか楽しかったです．と，同時に，また社会に一つ「人様に見せるようなクオリティじゃない」ものを追加してしまったかと悔しい気もします．

実は，当初この Advent Calendar には， Curry-Howard 同型対応の入門記事を書くつもりでした．しかし，書き始めてみると，「この話をするにはそれが必要で，そしてその話をするにはあれが必要で…」という感じでどんどんと勝手に風呂敷が広がっていき，一向に筆が進まなかったので，ギリギリのところであきらめて，もう少し手軽(?)な内容の「第三リスト準同型定理」に切り替えて記事を急いで執筆したわけです．いつかCurry-Howard同型対応の記事は書き上げてリベンジ(?)したいですね．

脚注

  1. ちなみに，元 article は，単に”Third Homomorphism Theorem”(第三準同型定理)といっていて，「リスト」はついていないのですが，本記事では，プログラミングの話とすぐにわかるように「第三リスト準同型定理」というタイトルをつけてみました． ↩

  2. これは当たり前のことで，与えられたプログラムが等しいか否かなんぞ決定不能問題です． ↩

  3. 実際には，foldr や foldl はリストに限らず Fordable なデータ構造全般に使えるものですが，ここではリストに限った定義をしています． ↩

  4. 実用上は foldl は使い物にならないという罠があるのですが，それはまた別の話ということで． ↩

  5. 厳密には，「x :: a となる要素 x を，(重複を許して)全て集めた無限リスト l :: [a] が任意の長さまで計算できる」ということです．（ちょっと自信ないですが）多分，Haskell の Enum 型クラスに属すると言い換えても良いのではないかと思います． ↩

  6. h が全射とは限らないので， map h l に b の要素が全て枚挙されているとは限らない．したがって，もし map h l にない値 t :: b に対して g t を走らせると，計算が止まらないわけである． ↩

  7. (g . h) x == g (h x) を計算することを考える．hは計算可能な全域関数だから，h xは必ず停止する．さて問題はg (h x)が停止するかどうかである．リスト l の中には必ず x がいるわけだから， map h lの中には必ずh xがいる．したがって，最悪でも g はその h x にたどり着けば間違いなく h x を返せるので，この計算は必ず停止することがわかる． ↩