|
今年度は、パラメトリシティーの理論の背景的な基礎付けを行なった。
まず、パラメトリックな多相型の理論によって、循環的構造を扱う論理体系を作ることが出来た。
通常、有理木など、循環的構造のあるデータは、循環経路のある有向グラフによって表現される。循環的構造においては、その循環経路を展開したものも意味としては同じである、という意味論がとられる。その意味論の公理化は、従来、等式の範囲に留まっていた。しかし、循環的構造をデータ型として把える為には、単なる等式論理では足りず、関数の引数になったり返り値になったりするような振る舞いをも把えられなくてはならない。
今回の研究では、循環的構造を表す有向グラフをλ式に翻訳し、循環的構造はそのようなλ式の上の一種の同値類であると定義する。そうすると、循環経路の展開など、循環的構造として同じ意味をもつものは同じ同値類に入ることが、バラメトリシティーの理論によって証明された。
これは、バラメトリシティーの理論が様々なデータ型を扱う上で優れた理論であることを示すものである。
また、計算モデルの上で定義されたデータ型によって、通常の数学がどの程度展開できるかについても研究した。
その為に多項式時間計算可能な関数の型によって、数学の理論を記述した。そして、自己相似図形に関する幾つかの定理が証明できることが解った。
|
