2020 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 |
近年のインターネットの爆発的な普及、それに伴う社会基盤としての計算機の重要性の増加により、ソフトウェアの安全性に対する要求はますます高まっている。しかし、実際のソフトウェア開発においては、ソフトウェア構築環境とは別に検証システムを用意しなければならないなど、安全性の面で充分とは言えず、バグを含んだソフトウェアが重要な箇所で利用され、重大な障害が発生している例も多い。
本研究は、この要求に答えるため、バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え、それを用いて(ユーザによる自己拡張を許す)ソフトウェアの実行および検証を同一の環境で可能にする自然枠組とよばれるシステムを計算機上に実装することを目的とする。
本年度は以下の2点について研究を進めた。
(1)クラス概念については、概念の階層化により、上位概念・下位概念を用いて、概念を線型に順序付けすることができた。これにより、従来型理論においては型の間の部分型関係の取扱いが困難であったのに対して、クラス間の順序関係が自然なものであることを示した。
(2)変数の束縛について。代数においては、例えば環論において、任意の環に変数を不定元として追加することにより、環を拡大することができる。この観点からは、λ計算においても、まず(自由)変数を一切含まない項の全体に代数的な構造を付与し、その構造に不定元としての自由変数を追加することにより代数系を拡大するという方針が得られる。この考えのもとで、クラス理論における抽象化のプロセスを記述することができるようになった。これは、将来においては、λ計算とCombinatory Logicが本質的に同等であることを示すことが期待される成果である。
|
| Research Progress Status |
令和2年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
令和2年度が最終年度であるため、記入しない。
|
