| 研究課題/領域番号 |
14J04528
|
|---|
| 研究種目 |
特別研究員奨励費
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 国内 |
|---|
| 研究分野 |
情報学基礎理論
|
|---|
| 研究機関 | 総合研究大学院大学 |
|---|
研究代表者 |
内田 早俊 総合研究大学院大学, 複合科学研究科, 特別研究員(DC2)
|
|---|
| 研究期間 (年度) |
2014-04-25 – 2016-03-31
|
| 研究課題ステータス |
完了 (2015年度)
|
| 配分額 *注記 |
1,900千円 (直接経費: 1,900千円)
2015年度: 900千円 (直接経費: 900千円)
2014年度: 1,000千円 (直接経費: 1,000千円)
|
|---|
| キーワード | 型理論 / 数理論理学 / プログラミング言語理論 |
|---|
| 研究実績の概要 |
多くのプログラミング言語は、基本的なデータ型や抽象データ型、多相型、関数型などのような様々な種類の「型」を持っている。型は、関数が誤った型の引数に適用されることを未然に防いだり、大規模なプログラムを部品化したりするなど、プログラミングの実践に不可欠な概念である。一般に、型をプログラミング言語を数学的に抽象・形式化した体系は「型システム」と呼ばれる。型システムは、関数型プログラミング言語や証明支援システムの基礎理論として盛んに研究が進められている。
型システムを実際にプログラミング言語や証明支援システムの基礎として用いるためには、高い表現力を持つ型が必要になる。しかし、型の表現力を高め過ぎると、その型システムは論理的に矛盾してしまい、そのような型システムをそれらの基礎として用いることは危険であることが知られている。現在、プログラミングの実践において型の重要性はますます高まっており、それとて、型の表現力を高める研究が盛んに行われている。
このような背景のもと、報告者は、プログラミング言語や証明支援システムの、型による拡張の安全性を保証するために、型システムの論理的矛盾の原因を究明すると共に、それを通じて「弱正規性を満たす純型システムは強正規性も満たす」という未解決問題を肯定的に解決することを目標に研究を行った。
本研究を通じて報告者は、「依存型」と呼ばれる、プログラムの性質を記述および検証する上で重要な型について、それが論理的矛盾・無矛盾性にとって本質的ではないことを明らかにした。今後は、依存型が、弱正規性と強正規性という二つの性質の論理的関係に与える影響を研究していくことを計画している。
|
| 現在までの達成度 (段落) |
27年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
27年度が最終年度であるため、記入しない。
|
