| 研究課題/領域番号 |
14J04528
|
|---|
| 研究機関 | 総合研究大学院大学 |
|---|
研究代表者 |
内田 早俊 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2014-04-25 – 2016-03-31
|
| キーワード | プログラミング言語理論 / 型理論 / 数理論理学 |
|---|
| 研究実績の概要 |
多くのプログラミング言語は、基本的なデータ型や抽象データ型、多相型、関数型などのような様々な種類の「型」を持っている。型は、関数が誤った型の引数に適用されることを未然に防いだり、大規模なプログラムを部品化したりするなど、プログラミングの実践に欠かすことのできないものである。一般に、型を持つプログラミング言語を抽象・形式化した体系は「型システム」と呼ばれる。型システムは、Haskellのような関数型プログラミング言語やCoqのような証明支援システムの基礎として現在盛んに研究が進められている。
型システムを実際にプログラミング言語や証明支援システムの基礎として用いるためには、高い表現力を持つ型が必要になる。しかし、型の表現力を高め過ぎると、その型システムは論理的に矛盾してしまい、そのような型システムをプログラミング言語や証明支援システムとして用いることは危険であることが知られている。現在、プログラミングの実践において型の重要性はますます高まっており、それと相まって、型の表現力を高める研究が盛んに行われている。
このような背景のもと、報告者は、プログラミング言語の安全性を保証するために、型システムの論理的矛盾の原因を究明し、またその結果を用いて、「弱正規性を満たす純型システムは強正規性も満たす」という未解決問題を肯定的に解決することを目標に研究を行っている。より具体的には、純型システムと呼ばれる、様々な型システムを一様に定義するフレームワークにおいて、型システムを論理的に矛盾しているものと無矛盾なものとに分類し、無矛盾なものに対して強正規性を示すことによって、上述の未解決問題を解決することを目指す。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
3: やや遅れている
理由
研究目的の達成度がやや遅れている理由は、簡潔には、他のアプローチも同時に検討していたがあまり上手くいかなかったことと、当初援用することを計画していた先行研究の証明中に誤りと思われる点が見つかったからである。
報告者は、「弱正規性を満たす純型システムは強正規性も満たす」（BGK予想）という未解決問題を解決するに当たって、論理的矛盾の分析によるアプローチ以外にも、様々なアプローチを試みてきたが、どれも一筋縄ではいかないことが明らかとなった（あるアイデアについては、重大な反例が見つかった）。しかし、現時点では研究目的の達成に直接結び付いてはいないものの、BGK予想の解決につながる見込みのある結果（Berardi-Paulin translationの一般化）を得たという収穫もあった。
論理的矛盾の分析によるアプローチに関して、報告者はまず、既に論理的に矛盾していることが知られているシステムλU-のあらゆる部分システムが論理的に無矛盾であることの証明を試みた。当初、その論理的無矛盾性を、MelliesとWernerによって考案された証明手法を用いて証明することを計画していたが、彼らの証明中に誤りと思われる点が見つかったため、別の証明手法の検討を余儀なくされた。
|
| 今後の研究の推進方策 |
今後はより、論理的矛盾の分析によるアプローチに焦点を絞って、研究を進めていく。とりわけまず、MeillesとWernerの証明を、彼らと意見交換をしながら修正し、λU-の部分システムの論理的無矛盾性の証明を完成させる。次に、当初の計画通り、純型システムを論理的に矛盾しているものと無矛盾なものとに分類し、論理的に無矛盾な純型システムの強正規性を示すことによって、BGK予想を解決することを目指す。
|
