| 研究課題/領域番号 |
02J02624
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 東北大学 (2004)
千葉大学 (2002-2003) |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助手 (40396528)
|
|---|
| 研究期間 (年度) |
2002 – 2004
|
| 研究課題ステータス |
完了 (2004年度)
|
| 配分額 *注記 |
3,400千円 (直接経費: 3,400千円)
2004年度: 1,000千円 (直接経費: 1,000千円)
2003年度: 1,200千円 (直接経費: 1,200千円)
2002年度: 1,200千円 (直接経費: 1,200千円)
|
|---|
| キーワード | 数理論理学 / 理論計算機科学 / プログラム理論 |
|---|
| 研究概要 |
本研究の目的は、非古典論理の分野で発達した証明論あるいは意味論の手法を用いて、ソフトウェア記述システムを分析、設計するための基礎理論を確立することである。昨年度までの研究により、直観主義論理に対するsequent計算の体系と明示的代入計算の間の関係についての結果が得られた。具体的には、型付きラムダ計算のベータ簡約が、直観主義論理に対するsequent計算の体系においてどのような簡約に対応するのかを理解し、そのうえで、明示的代入計算の手法を用いて、簡約の強正規化性を証明した。本年度は、この結果をまとめた論文を「The Seventh International Symposium on Functional and Logic Programming (FLOPS 2004)」で発表し、海外からの参加者からもコメントを頂いた。この結果は、sequent計算に基づく型システムに対する最も基本なものであるため、様々な方向へ拡張することが可能である。現在、特にインターセクション型システムへの拡張と、古典論理・ラムダミュー計算への拡張について検討している。
一方、博士論文の研究で開発した部分直観主義論理に対するsequent計算の体系を、tree sequentの手法を用いて述語論理へ拡張し、それを通してヒルベルト流の公理系の完全性を証明した。部分直観主義論理の述語論理に対する公理系を与えることは未解決問題となっていたが、完全な公理系を与えたのは本研究が初めてである。
|
