2019 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 |
これまでに得られている抽象体とその具体化に関する研究は、抽象体の内包的な側面を実現しているにすぎない。現実の数学を支える証明支援系においては、内
包的側面だけでなく、外延的側面も扱えるようにする必要がある。そのために、λ計算におけるη同値性について引き続き研究を進める予定である。ここにおい
ても変数
の概念を用いずにη同値性を定義する必要があり、従来の研究では見られない困難が予想される。
さらにξ規則を詳細に分析することにより範疇的判断と仮言的判断の関係を明きらかにしたい。
|
