関数のパターンマッチング f(x) = [...] による関数の圏論的構成法

といったような変数を用いない射の構成が当たり前のようにされてきたが、これは「必然的にそういった意味論的 (semantical) な構成を経る必要性があったから」であって決して「Point-free な関数の定義がスタイリッシュだから」などといった単なる嗜好によるものではなかったという点に注意してほしい。

余談

変数 (variable) の使用を必須としない「Function-level programming (Wikipedia 記事)」と呼ばれるプログラミングの流儀も存在するとのこと。

詳しいことは知らないので何とも言えないが、この用語を借りれば、この記事でやりたいことというのは「Function-level programming の言語で、関数のパターマッチングによって定義されるような射を定義する方法を考える」といったところになるのだろうか。

とはいえ、そうなるとプログラミング言語で関数を定義する際に頻繁に採用される次のような

\begin{aligned} f (0, 0) & = 2 \\ f (0, 1) & = 5 \\ f (1, 0) & = 15 \\ f (1, 1) & = 3 \end{aligned}

といった感じの「関数のパターンマッチング」を用いた関数の構成というのは圏論的には許されないのかという話になる。

これについては、関数型プログラミング言語 (ラムダ計算) の環境設定の一つとして捉えられている「カルテシアン閉圏 (デカルト閉圏とも訳される)」に「全ての有限余積を持つ」という公理を加えた圏を周囲圏に考えると、その一般論の中でその種の関数のパターンマッチングによって特徴づけられる射の構成が実際にできることがわかる。

因みに前回の「圏論的にIf文を組み立てる」で紹介したような方法でも似たようなことはできるが、ここでは自然数対象を介さずともそういった射が具体的に構成できることを確認していく。

具体例

具体例として

\begin{aligned} [3] & := (1 + 1) + 1 \\ [9] & := (((((((1 + 1) + 1) + 1) + 1) + 1) + 1) + 1) + 1 \\ 0 & := {i n j}_{1} ⨟ {i n j}_{1} \\ 1 & := {i n j}_{2} ⨟ {i n j}_{1} \\ 2 & := {i n j}_{2} \end{aligned}

としたとき、以下の

\begin{aligned} f (0, 0) & = 0 \\ f (0, 1) & = 1 \\ f (0, 2) & = 2 \\ f (1, 0) & = 1 \\ f (1, 1) & = 2 \\ f (1, 2) & = 0 \\ f (2, 0) & = 2 \\ f (2, 1) & = 0 \\ f (2, 2) & = 1 \end{aligned}

という記号群として与えた関係式をすべて満たすような射

f : [3] \times [3] \to [3]

の構成方法を紹介する。

写像のグラフを構成する

まず与えられた記号群をもとに以下に示す対象

([3] \times [3]) \times [3]

の9つの要素

1 \to ([3] \times [3]) \times [3]

を得る。

\begin{aligned} ⟨ ⟨ 0, 0 ⟩, 0 ⟩ \\ ⟨ ⟨ 0, 1 ⟩, 1 ⟩ \\ ⟨ ⟨ 0, 2 ⟩, 2 ⟩ \\ ⟨ ⟨ 1, 0 ⟩, 1 ⟩ \\ ⟨ ⟨ 1, 1 ⟩, 2 ⟩ \\ ⟨ ⟨ 1, 2 ⟩, 0 ⟩ \\ ⟨ ⟨ 2, 0 ⟩, 2 ⟩ \\ ⟨ ⟨ 2, 1 ⟩, 0 ⟩ \\ ⟨ ⟨ 2, 2 ⟩, 1 ⟩ \end{aligned}

ここで余積の定義より、これら9つの要素は次の射

h : [9] \to ([3] \times [3]) \times [3]

(i.e. 写像

f

のグラフ) を引き起こす。

h = [[[[[[[[⟨ ⟨ 0, 0 ⟩, 0 ⟩, ⟨ ⟨ 0, 1 ⟩, 1 ⟩], ⟨ ⟨ 0, 2 ⟩, 2 ⟩], ⟨ ⟨ 1, 0 ⟩, 1 ⟩], ⟨ ⟨ 1, 1 ⟩, 2 ⟩], ⟨ ⟨ 1, 2 ⟩, 0 ⟩], ⟨ ⟨ 2, 0 ⟩, 2 ⟩], ⟨ ⟨ 2, 1 ⟩, 0 ⟩], ⟨ ⟨ 2, 2 ⟩, 1 ⟩]

(縦長になってしまうので、ここでは余積の定義により射

α, β

から引き起こされる射を

(\begin{matrix} α \\ β \end{matrix})

ではなく

[α, β]

と書いている。)

こうして得られた写像のグラフを射影を用いて「入力のパート」と「出力のパート」の2つのパーツに分解することで以下の2つの射

[9] \to [3] \times [3]

[9] \to [3]

\begin{array}{r} h ⨟ {p r j}_{1} \\ h ⨟ {p r j}_{2} \end{array}

が得られるが、もし値の割り当てが漏れなくできていれば、前者の射

h ⨟ {p r j}_{1}

のインヴァースが構成できる。

そして

h ⨟ {p r j}_{1}

のインヴァース

(h ⨟ {p r j}_{1})^{- 1} : [3] \times [3] \to [9]

と後者の射

(h ⨟ {p r j}_{2}) : [9] \to [3]

の合成射が求める射

f : [3] \times [3] \to [3]

になる。

f = (h ⨟ {p r j}_{1})^{- 1} ⨟ (h ⨟ {p r j}_{2})

一見すると、これで一件落着のように思えるが、実は「インヴァースの構成」という大問題が一つ残っている。これについてを次節で考えていく。

インヴァース構成の概観

前節で、写像のグラフを介した

f

の定義方法を紹介したが、その定義の中に射

(h ⨟ {p r j}_{1})

のインヴァースが使用されている。

ただでさえこの段階にいたるまでの過程も、なかなかに煩雑であったわけだが、実はこの「インヴァースの "具体的" な構成」という問題は更に厄介なものとなる。

まず本題に入る前のウォーミングアップとして、次で定義される射

g : [4] \to [2] \times [2]

g = [[[⟨ {i n j}_{1}, {i n j}_{1} ⟩, ⟨ {i n j}_{1}, {i n j}_{2} ⟩], ⟨ {i n j}_{2}, {i n j}_{1} ⟩], ⟨ {i n j}_{2}, {i n j}_{2} ⟩]

のインヴァースを構成してみよう。

まず重要になるのは、「全ての有限余積を持つカルテシアン閉圏」が「分配的圏 (distributive category)」であるという事実である。

具体的に言い換えると、現在の設定において以下で定義されるカノニカルな射

(X \times Y) + (X \times Z) \to X \times (Y + Z)

(\begin{matrix} X \times {i n j}_{1} \\ X \times {i n j}_{2} \end{matrix})

はインヴァース

X \times (Y + Z) \to (X \times Y) + (X \times Z)

\begin{aligned} {(\begin{array}{c} X \times {i n j}_{1} \\ X \times {i n j}_{2} \end{array})}^{- 1} \\ := & t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times X) ⨟ e v \end{aligned}

を持つ (上のインヴァースの構成を見ての通り、この構成には少なくとも「カルテシアン閉」であることが必要なので、単なる一般の「全ての有限余積と積を持つ圏」という設定の中ではこのインヴァースの構成はできない) ということだが、そのインヴァースが存在することによって「余積対象同士の積」を「積対象同士の余積」へと展開していくことが実現するのである。

ここまでいえば、大体やることに察しがつくだろう。

おおよそやることとしては、「

A \times 1

と

A

を結ぶ同形射」と上手く併用しながら「余積対象同士の積」を「終対象だけからなる余積」の形にまず全て展開し、最後に余積の仲介射と入射をゴリゴリ組み合わせて「求める形の余積」への道筋を組み立てるのである。

具体的には

\begin{aligned} k_{1} & = t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times (1 + 1)) ⨟ e v \\ k_{2} & = {p r j}_{1} + {p r j}_{1} \\ k_{3} & = [[{i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], [{i n j}_{2} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{2}]] \end{aligned}

としたとき、以下を見てほしい。

(1 + 1) \times (1 + 1) \overset{k_{1}}{\to} ((1 + 1) \times 1) + ((1 + 1) \times 1) \overset{k_{2}}{\to} (1 + 1) + (1 + 1) \overset{k_{3}}{\to} ((1 + 1) + 1) + 1

ちょうど

k_{1}, k_{2}

の合成射が「余積対象同士の積」を「終対象だけからなる余積」へと展開する射、そして

k_{3}

が「求める形の余積」への道筋になっていることがわかると思う。

実際、それらの全ての合成射

k : [2] \times [2] \to [4]

\begin{aligned} k = & k_{1} ⨟ k_{2} ⨟ k_{3} \\ = & (t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times (1 + 1)) ⨟ e v) ⨟ ({p r j}_{1} + {p r j}_{1}) ⨟ ([[{i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], [{i n j}_{2} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{2}]]) \end{aligned}

が

g

のインヴァースになっている。(疑う場合は、実際に射を合成して恒等射を定めるのかを確認してみよう。)

本題となる射

(h ⨟ {p r j}_{1}) : [9] \to [3] \times [3]

のインヴァースについても、基本的に上で紹介したものと大体同じような流れで構成することができる。

ちょっと考えてみればわかると思うので、ここではその過程は端折って結果だけを載せておくことにする。

\begin{aligned} (h ⨟ {p r j}_{1})^{- 1} & = {(\begin{array}{c} ((1 + 1) + 1) \times {i n j}_{1} \\ ((1 + 1) + 1) \times {i n j}_{2} \end{array})}^{- 1} ⨟ (((1 + 1) + 1) + {p r j}_{1}) ⨟ ({(\begin{array}{c} ((1 + 1) + 1) \times {i n j}_{1} \\ ((1 + 1) + 1) \times {i n j}_{2} \end{array})}^{- 1} + ((1 + 1) + 1)) ⨟ (({p r j}_{1} + {p r j}_{1}) + ((1 + 1) + 1)) ⨟ [[[[{i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], [[{i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}]], [[{i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1}], {i n j}_{2}]] \\ = t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times ((1 + 1) + 1)) ⨟ e v ⨟ (((1 + 1) + 1) + {p r j}_{1}) ⨟ (t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times ((1 + 1) + 1)) ⨟ e v + ((1 + 1) + 1)) ⨟ (({p r j}_{1} + {p r j}_{1}) + ((1 + 1) + 1)) ⨟ [[[[{i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], [[{i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}]], [[{i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1}], {i n j}_{2}]] \end{aligned}

余談

僕は最初、「全ての有限余積を持つカルテシアン閉圏」という設定の中で例の射のインヴァースを構成すること自体できないものなのかなと思ってたのだけど、そもそも「カルテシアン閉圏」であれば「ある対象

X

との積を取る関手」が左随伴になるわけで、左随伴の持つ基本的な性質の１つである「余極限を保存する」という点を考慮すれば明らかに「

X \times (A + B)

は

(X \times A) + (X \times B)

と同形であるはず (それら対象の間に同形射が組めるはず) だよな」ということに気付き、ちょっと考え直してみたら普通に構成できてしまったという。

誤魔化しのない最終的な構成式

さて、ここまでくれば冒頭に示した

\begin{aligned} f (0, 0) & = 0 \\ f (0, 1) & = 1 \\ f (0, 2) & = 2 \\ f (1, 0) & = 1 \\ f (1, 1) & = 2 \\ f (1, 2) & = 0 \\ f (2, 0) & = 2 \\ f (2, 1) & = 0 \\ f (2, 2) & = 1 \end{aligned}

という関係式をすべて満たすような関数

f : [3] \times [3] \to [3]

の誤魔化しのない構成が実際にどのようにして実現するのかを具体的に確認することができる。

１つの式で綺麗にまとめると、

\begin{aligned} f & = (h ⨟ {p r j}_{1})^{- 1} ⨟ (h ⨟ {p r j}_{2}) \\ = (h ⨟ {p r j}_{1})^{- 1} ⨟ (([[[[[[[[⟨ ⟨ 0, 0 ⟩, 0 ⟩, ⟨ ⟨ 0, 1 ⟩, 1 ⟩], ⟨ ⟨ 0, 2 ⟩, 2 ⟩], ⟨ ⟨ 1, 0 ⟩, 1 ⟩], ⟨ ⟨ 1, 1 ⟩, 2 ⟩], ⟨ ⟨ 1, 2 ⟩, 0 ⟩], ⟨ ⟨ 2, 0 ⟩, 2 ⟩], ⟨ ⟨ 2, 1 ⟩, 0 ⟩], ⟨ ⟨ 2, 2 ⟩, 1 ⟩]) ⨟ {p r j}_{2}) \\ = t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times ((1 + 1) + 1)) ⨟ e v ⨟ (((1 + 1) + 1) + {p r j}_{1}) ⨟ (t w ⨟ ((\begin{array}{c} λ [t w ⨟ {i n j}_{1}] \\ λ [t w ⨟ {i n j}_{2}] \end{array}) \times ((1 + 1) + 1)) ⨟ e v + ((1 + 1) + 1)) ⨟ (({p r j}_{1} + {p r j}_{1}) + ((1 + 1) + 1)) ⨟ [[[[{i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], [[{i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}], {i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1} ⨟ {i n j}_{1}]], [[{i n j}_{2} ⨟ {i n j}_{1} ⨟ {i n j}_{1}, {i n j}_{2} ⨟ {i n j}_{1}], {i n j}_{2}]] ⨟ (([[[[[[[[⟨ ⟨ 0, 0 ⟩, 0 ⟩, ⟨ ⟨ 0, 1 ⟩, 1 ⟩], ⟨ ⟨ 0, 2 ⟩, 2 ⟩], ⟨ ⟨ 1, 0 ⟩, 1 ⟩], ⟨ ⟨ 1, 1 ⟩, 2 ⟩], ⟨ ⟨ 1, 2 ⟩, 0 ⟩], ⟨ ⟨ 2, 0 ⟩, 2 ⟩], ⟨ ⟨ 2, 1 ⟩, 0 ⟩], ⟨ ⟨ 2, 2 ⟩, 1 ⟩]) ⨟ {p r j}_{2}) \end{aligned}

である。(「対象 / 恒等射」と「余積対象の1つの要素」のそれぞれに同じ「

1

」という記号が使われている点に注意。)

「これ本当なの？」と疑いたくなる場合は、最後の節で「Haskell で上の構成を実際に行い、そうして得られる関数が本当に求める動作をするのか」という点をしっかり検証しているので是非確認していただきたい。

ともかく、普段何気なく当たり前のごとく行っている「関数のパターンマッチング」による関数の定義付けの背後で、実はこんなカオスな構成が隠れていたことを少しでも認識していただけたらと思う。

おまけ

この手続きによる関数の構成の応用例

応用1: 非自明な群を構成してみよう！

圏論的には最低限、圏が「全ての有限積の存在」さえ保証していれば、その圏の中で「群」の概念を考えること自体はできたのであった。

一方で、その最低限の「全ての有限積の存在しか課されていない圏の一般論」の中で、具体的に構成できる群というのは自明な群 (つまりは「単集合群 (singleton group)」) 程度しかないという側面もあり、その事実だけをみて

結局「群の定義」そのものは純粋圏論的に提供できたとしても、自明なものを除く具体的な群の構成が純粋圏論的にできないのであれば無駄。

と思う人も少なくないだろう。

幸いにも、一般論の舞台を単なる「全ての有限積を持つ圏」から「全ての有限余積を持つカルテシアン閉圏」にまで拡張し、このページで紹介したような「関数のパターンマッチング」を用いた関数の構成が許される状況になれば、面白い群の構成が、純粋圏論的かつ厳密に実現することになる。

具体的には、このページで例として構成した関数

f

に加えて、

\begin{aligned} g (0) & = 0 \\ g (1) & = 2 \\ g (2) & = 1 \end{aligned}

を満たすような関数

g

を用意できれば、以下の構造一式は群を成す。(実際に構成してみよう！)

対象 $[3]$
射 $(\cdot_{G}) := f$
$[3]$ の要素 $e_{G} := {i n j}_{1} ⨟ {i n j}_{1}$
射 $(-)_{G}^{- 1} := g$

因みに、それらの射たちが実際に「群」であるための条件を満たしているかを確かめることも、現在の設定として与えている「全ての有限余積を持つカルテシアン閉圏」の一般論の舞台の上で完結させられる。

おさらいをすると、適当な周囲圏の設定の下で「群 (group)」

G

は

対象 $A_{G}$
射 $(\cdot_{G}) : A_{G} \times A_{G} \to A_{G}$
$A_{G}$ の要素 $e_{G} : 1 \to A_{G}$
射 $(-)_{G}^{- 1} : A_{G} \to A_{G}$

の一式の内、以下の条件をすべて満たすものとして定義されたのだった。

\begin{aligned} ⟨! ⨟ e_{G}, A_{G} ⟩ ⨟ (\cdot_{G}) & = A_{G} \\ ⟨ A_{G}, (-)_{G}^{- 1} ⟩ ⨟ (\cdot_{G}) & =! ⨟ e_{G} \\ ⟨ (-)_{G}^{- 1}, A_{G} ⟩ ⨟ (\cdot_{G}) & =! ⨟ e_{G} \\ A_{G} \times (\cdot_{G}) ⨟ (\cdot_{G}) & = ⟨ ⟨ {p r j}_{1}, {p r j}_{2} ⨟ {p r j}_{1} ⟩, {p r j}_{2} ⨟ {p r j}_{2} ⟩ ⨟ (\cdot_{G}) \times A_{G} ⨟ (\cdot_{G}) \end{aligned}

ここで上の3つの条件式が成り立つのかどうかを具体的に確認したいのであれば

終対象同士の余積 $[n]$ をドメインにとる射 $f, g : [n] \to Λ$ について、余積対象の普遍性より、その余積対象の要素 $1 \to [n]$ と $f, g$ の合成射が漏れなく全て等しくなる場合、それら射 $f, g$ は同一でなければならない

という点に着目すれば示すことができるだろう。(well-pointedness までは必要にならない)

4つ目の式については、現在考えている圏が「分配的圏」であることによって構成が実現する同形射を用いた Pre-composition を介して、出発点となる

[3] \times ([3] \times [3])

を

[27]

に一旦置き換えた後、同様の議論を適用すればよい。

Haskell での動作確認

例によって今回も Haskell による動作確認をしておく。

まず対応の規則となる記号列として与えたものは

\begin{aligned} f (0, 0) & = 0 \\ f (0, 1) & = 1 \\ f (0, 2) & = 2 \\ f (1, 0) & = 1 \\ f (1, 1) & = 2 \\ f (1, 2) & = 0 \\ f (2, 0) & = 2 \\ f (2, 1) & = 0 \\ f (2, 2) & = 1 \end{aligned}

だが、右辺の記号を本来の形に戻すと

\begin{aligned} f (0, 0) & = {i n j}_{1} ⨟ {i n j}_{1} \\ f (0, 1) & = {i n j}_{2} ⨟ {i n j}_{1} \\ f (0, 2) & = {i n j}_{2} \\ f (1, 0) & = {i n j}_{2} ⨟ {i n j}_{1} \\ f (1, 1) & = {i n j}_{2} \\ f (1, 2) & = {i n j}_{1} ⨟ {i n j}_{1} \\ f (2, 0) & = {i n j}_{2} \\ f (2, 1) & = {i n j}_{1} ⨟ {i n j}_{1} \\ f (2, 2) & = {i n j}_{2} ⨟ {i n j}_{1} \end{aligned}

となる。これを踏まえたうえで、以下のコードの実行結果と比較してみてほしい。

ghci> printEl $ pair(i3_0, i3_0) -: f
inj1;inj1
ghci> printEl $ pair(i3_0, i3_1) -: f
inj2;inj1
ghci> printEl $ pair(i3_0, i3_2) -: f
inj2
ghci> printEl $ pair(i3_1, i3_0) -: f
inj2;inj1
ghci> printEl $ pair(i3_1, i3_1) -: f
inj2
ghci> printEl $ pair(i3_1, i3_2) -: f
inj1;inj1
ghci> printEl $ pair(i3_2, i3_0) -: f
inj2
ghci> printEl $ pair(i3_2, i3_1) -: f
inj1;inj1
ghci> printEl $ pair(i3_2, i3_2) -: f
inj2;inj1

見ての通り、しっかりと始めに与えた関係式が満たされている関数が構成できていることがわかる。

ソースコード

{-# LANGUAGE TypeOperators #-}

import Data.Void

main :: IO ()
main = do

  printEl $ pair(i3_0, i3_0) -: f
  printEl $ pair(i3_0, i3_1) -: f
  printEl $ pair(i3_0, i3_2) -: f
  printEl $ pair(i3_1, i3_0) -: f
  printEl $ pair(i3_1, i3_1) -: f
  printEl $ pair(i3_1, i3_2) -: f
  printEl $ pair(i3_2, i3_0) -: f
  printEl $ pair(i3_2, i3_1) -: f
  printEl $ pair(i3_2, i3_2) -: f


class (MyShow a) where
  myShow :: a -> String

instance MyShow () where
  myShow = const "*"

instance (MyShow a, MyShow b) => MyShow (Either a b) where
  myShow = either
    (\z -> if (myShow z == "*") then "inj1" else (myShow z) ++ ";inj1")
      (\z -> if (myShow z == "*") then "inj2" else (myShow z) ++ ";inj2")

instance (MyShow a, MyShow b) => MyShow (a,b) where
  myShow (x,y) = "(" ++ myShow x ++ "," ++ myShow y ++ ")"

instance MyShow Int where
  myShow = show

instance MyShow (a -> b) where
  myShow = const "(AN ARROW)"


-- X の要素を圏論に倣って終対象から X への射(Global element)として扱うための関数
el :: a -> (Pt -> a)
el = (const::a -> (Pt -> a))


-- Global elements 用 ユーティリティ
(===) :: Eq a =>  (Pt -> a) -> (Pt -> a) -> Bool
(===) x y = (x() == y())

showEl :: MyShow a => (Pt -> a) -> String
showEl x = (myShow $ x())

printEl :: MyShow a => (Pt -> a) -> IO ()
printEl = putStrLn . showEl


-- Diagrammatic-order な射の合成演算
(-:) = flip (.)

-- # 始対象と終対象
type Empty = Void
type Pt = ()

initArr :: Empty -> a
initArr = absurd

termArr :: a -> Pt
termArr = const ()

point :: Pt -> Pt
point = id

const' x = termArr -: x

-- # 余積対象と積対象
type (+++)  a b = Either a b
type (***) a b = (a,b)

-- 入射
inj1 :: a -> a +++ b
inj1 = Left

inj2 :: b -> a +++ b
inj2 = Right

-- 射影
prj1 :: a *** b -> a
prj1 = fst

prj2 :: a *** b -> b
prj2 = snd

-- 余積対象の仲介射
coPair :: (a -> c, b -> c) -> (a +++ b -> c)
coPair = uncurry either

-- 積対象の仲介射
pair   :: (c -> a, c -> b) -> (c -> a *** b)
pair = uncurry $ (<*>) . fmap (,)

-- 畳み込み
fol = coPair(id, id)

-- 対角射
dup = pair(id, id)

-- 射同士の余積
(+++) :: (a1 -> b1) -> (a2 -> b2) -> (a1 +++ a2 -> b1 +++ b2)
(+++) f g = coPair(f -: inj1 , g -: inj2)

-- 射同士の積
(***) :: (a1 -> b1) -> (a2 -> b2) -> (a1 *** a2 -> b1 *** b2)
(***) f g =   pair(prj1 -: f, prj2 -: g)

-- Twist の形式的双対
coTw :: a +++ b -> b +++ a
coTw = coPair(inj2, inj1)

-- Twist
tw :: a *** b -> b *** a
tw = pair(prj2, prj1)

-- # Exponential 対象
type (^) b a = a -> b

-- 評価射
ev :: (b ^ a) *** a -> b
ev = uncurry id

-- 射の転置 (transpose) の構成
trans :: (c *** a -> b) -> (c -> b ^ a)
trans = curry

-- 射 h:a->b の Exponential 対象 (Exp b a) の要素への変換
arrToEl :: (a -> b) -> (Pt -> b ^ a)
arrToEl h = trans(prj2-:h)

elToArr x = pair(termArr, id) -: (x *** id) -: ev

distributivityArrow :: ((x *** y) +++ (x *** z)) -> (x *** (y +++ z))
distributivityArrow = coPair(id***inj1, id***inj2)


inverseOfDistributivityArrow :: (x *** (y +++ z)) -> ((x *** y) +++ (x *** z))
inverseOfDistributivityArrow =
  tw-:(coPair(trans(tw-:inj1),trans(tw-:inj2))***id)-:ev

type Int_3 = (Pt +++ Pt) +++ Pt

i3_0 :: Pt -> Int_3
i3_1 :: Pt -> Int_3
i3_2 :: Pt -> Int_3

i3_0 = inj1 -: inj1
i3_1 = inj2 -: inj1
i3_2 = inj2

h =
  coPair(coPair(coPair(coPair(coPair(coPair(coPair(coPair(pair(pair(i3_0,i3_0),i3_0)
  ,pair(pair(i3_0,i3_1),i3_1)),pair(pair(i3_0,i3_2),i3_2)),pair(pair(i3_1,i3_0),i3_1))
  ,pair(pair(i3_1,i3_1),i3_2)),pair(pair(i3_1,i3_2),i3_0)),pair(pair(i3_2,i3_0),i3_2))
  ,pair(pair(i3_2,i3_1),i3_0)),pair(pair(i3_2,i3_2),i3_1))

inverseOf'h1' = 
  inverseOfDistributivityArrow -: (id +++ prj1) -:(inverseOfDistributivityArrow +++ id) -:
  ((prj1 +++ prj1) +++ id) -: (coPair(coPair(coPair(coPair(inj1-:inj1-:inj1-:inj1-:inj1-:inj1-:
  inj1-:inj1, inj2-:inj1-:inj1-:inj1-:inj1-:inj1-:inj1-:inj1), inj2-:inj1-:inj1-:inj1-:inj1-:
  inj1-:inj1),coPair(coPair(inj2-:inj1-:inj1-:inj1-:inj1-:inj1, inj2-:inj1-:inj1-:inj1-:inj1), inj2-:
  inj1-:inj1-:inj1)),coPair(coPair(inj2-:inj1-:inj1, inj2-:inj1), inj2)))

f :: Int_3 *** Int_3 -> Int_3
f = inverseOf'h1' -: (h -: prj2)

Show ALL

タグ: 数学圏論

タグ一覧:

物理学 (18)
古典力学 (9)
量子力学 (5)
数学 (56)
圏論 (32)
位相 (1)
線形代数 (7)
高校数学 (4)
プログラミング (32)
C言語 (4)
Haskell (36)
Java (1)
Python (2)
PureScript (3)
日記 (47)
小ネタ (21)
音楽 (4)
ピアノ (12)
ゲーム (18)
YouTube (36)

ページの先頭へ

TakuLabo

関数のパターンマッチング f(x) = [...] による関数の圏論的構成法