数学基礎論による代数のプログラミング言語理論への応用

現在注目されている分野の中に、substructural logicsと呼ばれる非古典論理がある。今年度当初は、非可換な論理についての決定性問題に取り組んできた。その中の肯定的な結果の一つが、finite model property for FL_W-logicである。これは、FL_Wと呼ばれるimplicational logicが決定的であることを示した。だが、それ以外の非可換な論理については、めぼしい結果は得られなかった。一般の非可換論理は非常に難しい。そこで、現在プログラム言語理論や並列アルゴリズムといった分野から注目されている線型論理(linearlogic)の、非可換なものについての研究を進めた。現在準備中の論文では、非可換線型論理のcharacterization theoremを示している。これは、非可換線型論理における証明図をグラフ理論の概念を用いて特長づけ試みである。今までもAbrusci,Yetterといった研究者が、phase semantics,量子力学といった興味から、似たような論理に同様の試みがなされていた。一方で自然言語学において、研究が進んでいるLambek Calculusが、直観主義非可換線型論理の一つであることから、RoordaによるLambek Calculusのcharacterization theoremも得られていた。だが、これらの試みは全て証明図として扱う図形に厳しい条件をつけており、その下での特長づけはいわば自明になっていた。我々の結果は、図形についてラベル付き有効グラフ以外条件をつけておらず、特長づけ自身もグラフ理論的に意味のあるstrong planityという概念に対応している。今後net re-writingといった計算理論に応用があるのではないかと期待している。

現在注目されている分野の中に、substructural logicsと呼ばれる非古典論理がある。今年度当初は、非可換な論理についての決定性問題に取り組んできた。その中の肯定的な結果の一つが、finite model property for FL_W-logicである。これは、FL_Wと呼ばれるimplicational logicが決定的であることを示した。だが、それ以外の非可換な論理については、めぼしい結果は得られなかった。一般の非可換論理は非常に難しい。そこで、現在プログラム言語理論や並列アルゴリズムといった分野から注目されている線型論理(linearlogic)の、非可換なものについての研究を進めた。現在準備中の論文では、非可換線型論理のcharacterization theoremを示している。これは、非可換線型論理における証明図をグラフ理論の概念を用いて特長づけ試みである。今までもAbrusci,Yetterといった研究者が、phase semantics,量子力学といった興味から、似たような論理に同様の試みがなされていた。一方で自然言語学において、研究が進んでいるLambek Calculusが、直観主義非可換線型論理の一つであることから、RoordaによるLambek Calculusのcharacterization theoremも得られていた。だが、これらの試みは全て証明図として扱う図形に厳しい条件をつけており、その下での特長づけはいわば自明になっていた。我々の結果は、図形についてラベル付き有効グラフ以外条件をつけておらず、特長づけ自身もグラフ理論的に意味のあるstrong planityという概念に対応している。今後net re-writingといった計算理論に応用があるのではないかと期待している。