型システムにおける論理的矛盾の分析による弱正規化性と強正規化性の関係の解明

多くのプログラミング言語は、基本的なデータ型や抽象データ型、多相型、関数型などのような様々な種類の「型」を持っている。型は、関数が誤った型の引数に適用されることを未然に防いだり、大規模なプログラムを部品化したりするなど、プログラミングの実践に不可欠な概念である。一般に、型をプログラミング言語を数学的に抽象・形式化した体系は「型システム」と呼ばれる。型システムは、関数型プログラミング言語や証明支援システムの基礎理論として盛んに研究が進められている。型システムを実際にプログラミング言語や証明支援システムの基礎として用いるためには、高い表現力を持つ型が必要になる。しかし、型の表現力を高め過ぎると、その型システムは論理的に矛盾してしまい、そのような型システムをそれらの基礎として用いることは危険であることが知られている。現在、プログラミングの実践において型の重要性はますます高まっており、それとて、型の表現力を高める研究が盛んに行われている。このような背景のもと、報告者は、プログラミング言語や証明支援システムの、型による拡張の安全性を保証するために、型システムの論理的矛盾の原因を究明すると共に、それを通じて「弱正規性を満たす純型システムは強正規性も満たす」という未解決問題を肯定的に解決することを目標に研究を行った。本研究を通じて報告者は、「依存型」と呼ばれる、プログラムの性質を記述および検証する上で重要な型について、それが論理的矛盾・無矛盾性にとって本質的ではないことを明らかにした。今後は、依存型が、弱正規性と強正規性という二つの性質の論理的関係に与える影響を研究していくことを計画している。

多くのプログラミング言語は、基本的なデータ型や抽象データ型、多相型、関数型などのような様々な種類の「型」を持っている。型は、関数が誤った型の引数に適用されることを未然に防いだり、大規模なプログラムを部品化したりするなど、プログラミングの実践に不可欠な概念である。一般に、型をプログラミング言語を数学的に抽象・形式化した体系は「型システム」と呼ばれる。型システムは、関数型プログラミング言語や証明支援システムの基礎理論として盛んに研究が進められている。型システムを実際にプログラミング言語や証明支援システムの基礎として用いるためには、高い表現力を持つ型が必要になる。しかし、型の表現力を高め過ぎると、その型システムは論理的に矛盾してしまい、そのような型システムをそれらの基礎として用いることは危険であることが知られている。現在、プログラミングの実践において型の重要性はますます高まっており、それとて、型の表現力を高める研究が盛んに行われている。このような背景のもと、報告者は、プログラミング言語や証明支援システムの、型による拡張の安全性を保証するために、型システムの論理的矛盾の原因を究明すると共に、それを通じて「弱正規性を満たす純型システムは強正規性も満たす」という未解決問題を肯定的に解決することを目標に研究を行った。本研究を通じて報告者は、「依存型」と呼ばれる、プログラムの性質を記述および検証する上で重要な型について、それが論理的矛盾・無矛盾性にとって本質的ではないことを明らかにした。今後は、依存型が、弱正規性と強正規性という二つの性質の論理的関係に与える影響を研究していくことを計画している。