数理論理学のプログラミング言語理論への応用

今年度の最初の成果としては、現在プログラム言語理論や並列アルゴリズムといった分野から注目されている線型論理(linear logic)の、非可換な体系についての研究に関する論文を完成させたことである。岡田光弘(慶應大)との共同研究によってNon-commutative proof netのCharacterization Theoremを得たが、この研究においては、Non-commutative Linear Logicの特徴づけとしてstrong planarityとstack conditionによって定められるmarked Danos-regnier graphのサブクラスという新しい概念を定義した。strong planarityという概念は、結び目理論におけるRidemeister Moveを用いてplanar graphの交差を取り除く方法を分析し、その結果として得られた概念である。現在進めている研究では、linear logicにおける計算モデルについて調べている。従来型の関数型プログラミング言語の理論的な基礎となるtype theoryのframe workに対し、linear logicよるtype-freeな推論をさらに付け加えて、higher order predicate logicより強力で無矛盾な体系が作れないかと言うことに興味をもっている。1989年の古森の論文にChurchのIntuitionistic Simple Type Theoryとtype-free affine ligicを含む体系を紹介したものがあり、その無矛盾性がopen problemであった。しかし、その体系が矛盾していることがGirard paradoxを埋め込むことにより証明できた。従って、そのparadoxを導くために使われた推論法則を分析し、無矛盾な体系に改良できないか検討中である。その結果、できるだけtype-freeの集合論に近いframe workの中で関数型プログラミング言語の基礎が作れないかということについて調べていきたい。

今年度の最初の成果としては、現在プログラム言語理論や並列アルゴリズムといった分野から注目されている線型論理(linear logic)の、非可換な体系についての研究に関する論文を完成させたことである。岡田光弘(慶應大)との共同研究によってNon-commutative proof netのCharacterization Theoremを得たが、この研究においては、Non-commutative Linear Logicの特徴づけとしてstrong planarityとstack conditionによって定められるmarked Danos-regnier graphのサブクラスという新しい概念を定義した。strong planarityという概念は、結び目理論におけるRidemeister Moveを用いてplanar graphの交差を取り除く方法を分析し、その結果として得られた概念である。現在進めている研究では、linear logicにおける計算モデルについて調べている。従来型の関数型プログラミング言語の理論的な基礎となるtype theoryのframe workに対し、linear logicよるtype-freeな推論をさらに付け加えて、higher order predicate logicより強力で無矛盾な体系が作れないかと言うことに興味をもっている。1989年の古森の論文にChurchのIntuitionistic Simple Type Theoryとtype-free affine ligicを含む体系を紹介したものがあり、その無矛盾性がopen problemであった。しかし、その体系が矛盾していることがGirard paradoxを埋め込むことにより証明できた。従って、そのparadoxを導くために使われた推論法則を分析し、無矛盾な体系に改良できないか検討中である。その結果、できるだけtype-freeの集合論に近いframe workの中で関数型プログラミング言語の基礎が作れないかということについて調べていきたい。