2018 Fiscal Year Annual Research Report
クラス理論に基づく自己拡張可能なソフトウェア検証体系の深化
| Project/Area Number |
17H01724
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 仕様記述・検証 / 証明支援系 / 型理論 / ソフトウェアの安全性 |
|---|
| Outline of Annual Research Achievements |
近年のインターネットの爆発的な普及、それに伴う社会基盤としての計算機の重要性の増加により、ソフトウェアの安全性に対する要求はますます高まっている。しかし、実際のソフトウェア開発においては、ソフトウェア構築環境とは別に検証システムを用意しなければならないなど、安全性の面で充分とは言えず、バグを含んだソフトウェアが重要な箇所で利用され、重大な障害が発生している例も多い。
本研究は、この要求に答えるため、バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え、それを用いて(ユーザによる自己拡張を許す)ソフトウェアの実行および検証を同一の環境で可能にする自然枠組とよばれるシステムを計算機上に実装することを目的とする。
本年度は自然枠組に論理的基盤を与えるクラス理論についての基本的考察を行なった。とくにクラス構築における抽象化のプロセスについての代数的な仕組の解明についての重要な知見を得ることができた。前年度にα同値性の解明をしたが、本年度はη同値性の本質を解明することができた。とくにη簡約においては、簡約の前後で簡約の対象となる項の高さが減少するという問題があったが、この問題を異なるβ簡約の文脈におけるη同値な項の振舞に関する問題に変形することにより解決することができた。さらに、ξ規則を分析することにより範疇的判断と仮言的判断との論理的等価性についての考察を開始することができた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
η簡約においては、簡約の前後で簡約の対象となる項の高さが減少するという問題があったが、この問題を異なるβ簡約の文脈におけるη同値な項の振舞に関する問題に変形することにより解決することができた。
また、証明支援系Agdaとクラス理論に基づく本研究での支援系と具体例について比較することにより、本研究での支援系の優位性を確認することができた。
|
| Strategy for Future Research Activity |
これまでに得られている抽象体とその具体化に関する研究は、抽象体の内包的な側面を実現しているにすぎない。現実の数学を支える証明支援系においては、内
包的側面だけでなく、外延的側面も扱えるようにする必要がある。そのために、λ計算におけるη同値性について引き続き研究を進める予定である。ここにおいても変数
の概念を用いずにη同値性を定義する必要があり、従来の研究では見られない困難が予想される。
さらにξ規則を詳細に分析することにより範疇的判断と仮言的判断の関係を明きらかにしたい。
|
