12. November, 2005.
立木 秀樹私の一連の研究は、 [1] において、{0,1,⊥}-無限列を用いた実数の表現(グレイコード表現) と、{0,1,⊥}-無限列上で動作する非決定性多ヘッドマシン(IM2-マシン) の概 念を導入し、それを用いて実数上の計算概念を導入したことから始まっている。
計算機科学の重要な研究テーマの一つは、止まらない計算の表示である ボト ム(⊥) についての理解を深めることであろう。ゲーデルやチューリングが計 算可能性の研究の中で導入した「止まらない計算」「決定不可能」という現象 は、数理論理学やプログラムの意味論において中心的な話題でありつづけてき た。
一方で、実数などの連続性の本質は、Dedekind Cut が示す様に、2つの集合 に分けたときにその境界の値が存在することである。 境界の入り方 はすなわち、位相構造を規定するものと言っていいだろう。
この、境界という位相空間論的な対象を⊥ という計算論的な仕組みを用いて
解釈できるという [1] の結果は、実数の計算という実用的な目的にとどまら
ず、プログラム言語の意味論などで培われてきた計算機科学的な道具を数学研
究に用いるという新たな研究手法と、ボトム入り文字列の上の計算という、数
学への応用を目指した計算機科学の研究という、数学と計算機科学を結びつけ
る、新たな研究の可能性を開いたと考えている。
2. それを発展させた仕事
その後、表現を通した実数などの空間の連続性に関する数学的研究と、ボトム 入り無限列を扱う計算に関する計算機科学的研究の両方をおしすすめてきた。 数学の計算機科学という2つの分野の境界で研究をしてきた訳だ。その分野は、 位相空間論とプログラミング言語理論にとどまらない。実際、私は、計算可能 性解析学、ドメイン理論、力学系など、様々な分野において、研究集会に参加 し、論文発表を行ってきた。主だった結果について説明する。
[1] Hideki Tsuiki. Real number computation through Gray code embedding. Theoretical Computer Science, Vol 284, Number 2, pp.467--485, 2002.}
一連の研究の出発点となる論文。実数のグレイコードと、IM2 マシン、それに より導出される計算可能性と、Type2 マシンによる通常の計算可能性との同値 性などが述べられている。[2] Hideki Tsuiki. Computational Dimension of Topological Spaces. In Proc. Computability and Complexity in Analysis, Lecture Notes in Computer Science vol. 2064, 323-336, edited by Blanck et al., Springer. 2001.
[1] の埋め込みを一般の距離空間に拡張し、 可分距離空間において、空間の次元と⊥入り文字列での表現に必要な⊥の個数 が等しいことを述べた論文。これ自体は、計算機科学を離れた、位相空間に関 する「数学的事実」であるが、⊥の個数は、それを入出力する IM2 マシンの 余分なヘッドの個数と等しいので、「次元」がそういう計算的構造だと主張し ている。
[3] 立木秀樹, 実数計算のGHC による実現. コンピュータソフトウェア, Vol.18, No.2, pp40-53, 2001.
IM2 マシンが、並列論理型プログラミング言語 GHC によって自然に実現でき ることを述べた論文。これによって、[1] の中で紹介していた実数の足し算な どのアルゴリズムが、実際のコンピュータで動かすことができた。[7] Hideki Tsuiki. Real Number Computation with Committed Choice Logic Programming Languages. Journal of Logic and Algebraic Programming, 64, pp.61-84, 2005.
[3] の結果をさらに精密化し、GHC 計算可能ということと IM2 計算可能ということの関係を、領域構造との関係で調べた。[9] Hideki Tsuiki and Keiji Sugihara. Streams with a bottom in funcitonal languages. In Proceedings ESOP 2005: The European Symposium on Programming, LNCS 3444, pp.201-216, 2005.
関数型言語の枠組みの中で、⊥入り文字列の入出力を実現すべく、Hags とい う Haskell 言語の処理系に手を加えた。それによって分かったことは、⊥入 り文字列の入出力に現れる非決定性は、グラフ簡約のレベルでは決定的であり、 同じ式に対するグラフ表現の違いが、非決定性となって関数型言語に現れてい ること。グラフ簡約の研究が重要であることを示唆される。
[8] Hideki Tsuiki. Dyadic subbases and efficiency properties of the induced {0,1,⊥}ω-representations. Topology Proceedings, 28(2), pp.673-687, 2004.
私の考えているグレイコード的な埋め込みは、位相空間論の言葉で言えば、二 分的部分基という、一種の部分基を与えることと等価である。この部分基に対 し、それから導出されるコードが効率的であるという性質に対応する3つの条 件を考え、その関係を調べた。[10] Haruto OHTA, Hideki Tsuiki and Shuji Yamada. Independent subbases and non-redundant codings of separable metrizable spaces . Submitted.
[8] で述べた効率的な二分的部分基が、どのような位相空間について存在する か、特徴付けた論文。孤立点が存在しない距離空間については、必ず存在する ことを構成して見せた。
[11] 立木秀樹, 山田修司. 力学系により生成される二分的部分基 In 力学系の研究 -- トポロジーと計算機による新展開}、京都大学数理解析研究所講究録, to appear.
[8] で述べた効率的な二分的部分基の中で、本当に計算的といえるのは、1文 字シフトという基本操作が関数を意味することが本質であると考える。それに よって、1ビット反転が関数となること、コードが再帰的な構造を持つことが 保障される。1文字シフトが関数となるというのは、力学系の旅程となっている ことである。そのような、力学系により生成される二分的部分基が、 I や I x I の上でどれだけ存在するか、調べた。
[4] Hideki Tsuiki. Compact metric spaces as minimal-limit sets in domains of bottomed sequences. Mathematica Structures in Computer Science 14(6), pp.853--878, 2004.
[2] における、距離空間の次元と表現に必要な⊥の個数の関係は、代数的なド メインにおいて、極限要素集合の順序としての高さとスコット位相の部分位相 による次元とが一致することを証明した。こちらの一般的な結果の証明の方が、 帰納法が直接使えて、容易な証明となる。また、それを用いて、⊥入り文字列 表現を、代数的ドメイン表現に一般化した。[5] Hideki Tsuiki. Representations of Complete Uniform Spaces via Uniform Domains. In Proc. Computability and Complexity in Analysis, ENTCS Vol 66, Number 1, pp.1-13, 2002.
一様空間の構成と、ドメインの構成とを関係付けた論文。可算基をもつ一様空 間(つまり、可分距離空間)の normal sequence に対応する構造を持ったド メインというものを考え、その極限要素集合が一様空間を retract とするこ とを述べた。[6] 立木秀樹. 整合的ドメインの極限要素集合の次元について. %In {代数・論理・幾何と情報科学}、京都大学数理解析研究所講究録 1318, pp.15-20, 2003.
[4] の証明の中の本質的な部分を、ローソン位相でコンパクトということによ る位相的な証明に置き換えた解説。