Avendia20

日記 (2020 年 5 月 31 日)

再帰的定義は関数型プログラミングにおいて欠かせない重要な要素であるが、 その実現方法には主に 2 種類ある。 1 つ目の方法は、 不動点コンビネータを用いるものである。 例えば、 以下は全ての要素が 0 であるような無限リストを作る Haskell のプログラムである。

fix $ \list -> 0 : list

Haskell では let 束縛における定義式でこれから定義する識別子が使えるので、 以下のようにも書ける。 数学において形式的な計算体系を扱う場合、 このような再帰的な let 束縛は、 上記の不動点コンビネータを用いた式のシンタックスシュガーとすることも多い (例えば Pierce†4 の 11.11 節ではそのような定義がなされている)。

let list = 0 : list in list

2 つ目の方法は、 値のフィードバックを利用するものである。 Haskell では、 この方法で再帰関数を定義するためのコンビネータとして loop が用意されている。 これを用いて、 全ての要素が 0 であるような無限リストは以下のようにも作ることができる。

loop func $ 0
where func = \(a, l) -> (l, a : l)

さて、 この 2 つの再帰の方法それぞれに対して、 その圏論的対応物がいくつか提唱されている。 この記事では、 前者に対応するものとして Bloom–Ésik†1 による Conway 演算子を、 後者に対応するものとして Joyal–Street–Verity†3 によるトレースを紹介し、 その同値性を示す。 なお、 以下では射の合成は左から右に行い、 記号を変えて 󰖡 で表す。

まず、 Bloom–Ésik による Conway 演算子の定義を行う。 これには様々な同値な定式化があるが、 ここでは Hasegawa†2 に従って不動点演算子であることが分かりやすいものを採用する。

定義 1.

カルテシアン圏 󰒚 の対象 A,X に対し、 関数 fixAX:Hom(A×X,X)→Hom(A,X) が定まっており、 7 条件

  1. 任意の射 f:A×X→X に対し、 (idA,fixAXf)󰖡f=fixAXf が成り立つ。 すなわち、 fix はパラメータ付き不動点演算子である。
  2. 任意の射 f:A×X→X,g:A󰎘→A に対し、 fixA󰎘X((g×idX)󰖡f)=g󰖡fixAXf が成り立つ。 すなわち、 fix は A に関して自然である。
  3. 任意の射 f:A×X󰎘→X,g:X→X󰎘 に対し、 fixAX󰎘(f󰖡g)=fixAX((idA×g)󰖡f)󰖡g が成り立つ。 すなわち、 fix は X に関して自然である。
  4. 任意の射 f:A×X×Y→X,g:A×X×Y→Y に対し、 fixAX×Y(f,g)=(idA,fixAX((idA×X,fixA×XYg)󰖡f))󰖡(sndAX,fixA×XYg) が成り立つ。

を全て満たすとする。 このとき、 fix を Conway 演算子 (— operator) という。

次に、 Joyal–Street–Verity によるトレースの定義を行う。 もともとの論文では、 組み紐付きモノイダル圏 (テンソル積の左右を入れ替える射 σ が必ずしも σ󰖡σ=id を満たさないもの) 上に定義されているが、 ここでは簡単のため対称モノイダル圏上に定義する。

定義 2.

対称モノイダル圏 󰒚 の対象 A,B,X に対し、 関数 trABX:Hom(A⊗X,B⊗X)→Hom(A,B) が定まっており、 7 条件

  1. 任意の射 f:A⊗X→B⊗X,g:A󰎘→A に対し、 trA󰎘BX((g⊗idX)󰖡f)=g󰖡trABXf が成り立つ。 すなわち、 tr は A に関して自然である。
  2. 任意の射 f:A⊗X→B⊗X,g:B→B󰎘 に対し、 trAB󰎘X(f󰖡(g⊗idX))=trABXf󰖡g が成り立つ。 すなわち、 tr は B に関して自然である。
  3. 任意の射 f:A⊗X󰎘→B⊗X,g:X→X󰎘 に対し、 trABX󰎘(f󰖡(idB⊗g))=trABX((idA⊗g)󰖡f) が成り立つ。 すなわち、 tr は X に関して自然である。
  4. 任意の射 f:A→B に対し、 trAB⊤(ρA󰖡f󰖡ρB−1)=f が成り立つ。 なお、 ρA:A⊗⊤→A は対称モノイダル圏に定まる同型射である。
  5. 任意の射 f:A⊗X⊗Y→B⊗X⊗Y に対し、 trABX(trA⊗X,B⊗XYf)=trABX⊗Yf が成り立つ。
  6. 任意の射 f:A⊗X→B⊗X に対し、 trC⊗A,C⊗BX(idC⊗f)=idC⊗trABXf が成り立つ。
  7. 常に trXXX(σX)=idX が成り立つ。 なお、 σX:X⊗X→X⊗X は対称モノイダル圏に定まるテンソル積の左右を入れ替える同型射である。

を全て満たすとする。 このとき、 tr をトレース (trace) という。

そして、 この 2 つの概念は実質同じものである。

定理 3.

カルテシアン圏 󰒚 において、 Conway 演算子とトレースとの間には 1 対 1 対応がある。

証明.

Conway 演算子 fix が与えられたとして、 対象 A,B,X に対し、 trABX: Hom(A×X,B×X) ⟶ Hom(A,B) f ⟼ fixAB×X((idA×sndBX)󰖡f)󰖡fstBX とおくと、 これはトレースを定める。 逆に、 トレース tr が与えられたとして、 対象 A,X に対し、 fixAX: Hom(A×X,X) ⟶ Hom(A,X) f ⟼ trAAX(f,f) とおくと、 これは Conway 演算子を定める。 さらに、 これら 2 つの構成は互いに逆になっていることが確かめられる。 具体的な計算過程については、 Hasegawa†2 の A.2 節を参照すると良い。

参考文献

  1. S. Bloom, Z. Ésik (1993) 「Fixed-point operations on ccc's. part I」 『Theoretical Computer Science』 155(1):1–38
  2. M. Hasegawa (1997) 「Models of sharing graphs: a categorical semantics of let and letrec」 Ph. D. thesis, The University of Edinburgh
  3. A. Joyal, R. Street, D. Verity (1996) 「Traced monoidal categories」 『Mathematical Proceedings of the Cambridge Philosophical Society』 119(3):447–468
  4. B. C. Pierce (2002) 『Types and Programming Languages』 The MIT Press