研究課題
基盤研究(C)
本研究では,ストリームデータなどの無限概念を含む計算と古典論理との関連を明らかにすることを目的とし,そのような計算モデルの一つであるラムダ・ミュー計算をはじめとする計算体系の基本性質を明らかにした.また,とくに合流性の証明のために提案した合成的Z定理が他の多くの計算体系の合流性の簡潔な証明を与えることを示した.さらに,古典論理の対称性を反映したシーケント計算に対応する計算体系に対し,完全かつ強正規化性を特徴付ける交叉型理論を与えた.
プログラミング言語,数理論理学