| 研究課題/領域番号 |
25280025
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| 研究分担者 |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2017-03-31
|
| キーワード | 証明支援系 / クラス理論 / 型理論 |
|---|
| 研究実績の概要 |
ソフトウェアの安全性を検証するための理論として，論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行なう言語体系であるロジカル・フレームワーク(論理枠組)が提案されている．形式的な計算体系であるプログラミング言語をロジカル・フレームワークで記述することにより，ソフトウェアに求められる使用を正確に記述し，与えられたソフトウェアがその使用を満足することを厳密に検証することが可能になる．さらにロジカル・フレームワークを計算機上に実装することができれば，これらの記述・検証の機械的に正確な検査が可能になり，ソフトウェアの品質面，安全面の信頼性が高まることが期待される．
変数の束縛機構は，プログラミング言語とくに関数型言語における基本的な研究課題であり多数の研究者により長年研究がされてきている．昨年度の研究では，自由変数を含まない閉じたλ項の全体を帰納的に定義するという問題を解決することができた．しかし，昨年度の結果では伝統的な閉じたλ項以外にも余分な項が同時に定義されていた．今年度は，これら余分な項にも自然な意味を付与することができた．
クラス理論に関する研究では，クラスに適当な同値関係を導入することにより「型」をクラスとして定義可能であることがわかった．この結果を利用することにより，これまでにはなかった型の新し意味論を展開する可能性が得られる考えている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
クラス理論に関する研究では，クラスに適当な同値関係を導入することにより「型」をクラスとして定義可能であることがわかった．このことは事前に予想できなかった大きな収穫であった．
クラス理論とフレーゲの Sinn との関係についても新しい考察をすることができた．
以上のことにより，研究は順調に進展していると考える．
|
| 今後の研究の推進方策 |
自由変数を用いないで閉じたλ項を定義する方法をクラス理論に導入する．これにより，メタ定理の証明がどのように簡略化できるかについて考察し，クラスのインスタンスの実現方法を検討する予定である．
ロジカル・フレームワーク実装のためのプログラミング言語の設計の詳細化を行ない実装を行なう．
|
