|
本研究の目的は、非古典論理の分野で発達した証明論あるいは意味論の手法を用いて、ソフトウェア記述システムを分析、設計するための基礎理論を確立することである。今年度の前半には、研究代表者が博士論文の研究で開発した証明論的手法が、プログラミング言語の操作的意味論に応用できるかどうかを検討するために、まず基本となる直観主義論理に対する証明論的手法について詳細に調べた。具体的には、型付きラムダ計算のベータ簡約が、直観主義論理に対するsequent計算の体系においてどのような簡約に対応するのかを理解した。そのうえで、明示的代入計算の手法を用いて、簡約の強正規化性を証明した。この結果は、「記号論理と情報科学」研究集会で発表し、参加者から意見を求めた。
今年度の後半には、前半で得られた結果と近年注目を集めているtqプロトコルと呼ばれる簡約法とを比較するために、研究指導者である桜井助教授とともにセミナーで論文を講読した。しかしながら、tqプロトコルは線形論理の証明網の簡約を基にしていることが判り、線形論理に関しても調べることとなった。これらについて、線形論理の専門家でありフランスに滞在中の浜野正浩博士に問い合わせたところ、極性を持つ線形論理との関係を指摘され、現在それらについても調査を行っている。また、2月には「論理と計算」ワークショップ及びJean-Y ves Girard教授連続講演に参加し、線形論理の最先端の話題及び関連する話題について触れる機会を得た。
|
