| 研究課題/領域番号 |
17H01724
|
|---|
| 研究機関 | 京都大学 |
|---|
研究代表者 |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| 研究分担者 |
桜井 貴文 千葉大学, 大学院理学研究院, 教授 (60183373)
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| キーワード | 仕様記述・検証 / 証明支援系 / 型理論 / ソフトウェアの安全性 |
|---|
| 研究実績の概要 |
近年のインターネットの爆発的な普及、それに伴う社会基盤としての計算機の重要性の増加により、ソフトウェアの安全性に対する要求はますます高まっている。しかし、実際のソフトウェア開発においては、ソフトウェア構築環境とは別に検証システムを用意しなければならないなど、安全性の面で充分とは言えず、バグを含んだソフトウェアが重要な箇所で利用され、重大な障害が発生している例も多い。
本研究は、この要求に答えるため、バグのないソフトウェアを構築するためのクラス理論に基づく理論的基盤を与え、それを用いて(ユーザによる自己拡張を許す)ソフトウェアの実行および検証を同一の環境で可能にする自然枠組とよばれるシステムを計算機上に実装することを目的とする。
本年度は自然枠組に論理的基盤を与えるクラス理論についての基本的考察を行なった。とくにクラス構築における抽象化のプロセスについての代数的な仕組の解明についての重要な知見を得ることができた。そのアイディアは以下のようである。従来、変数の抽象化と対になる概念として代入が用いられてきた。これに対して、我々は対になる概念として具体化を用いることにした。抽象化のプロセスにより得られる対象を抽象体と呼ぶことにすれば、抽象体においては抽象化に用いられた変数は消去されもはや存在しない。つまりその変数は抽象体を得るまでのプロセスを実行する間だけ一時的に必要な存在であることがわかる。これはλ計算におけるα同値性の本質でもある。この観察を用いて、抽象体の代数を変数概念を経由せずに確立することができ、それにより抽象体からそれを具体化するプロセスも変数を用いることなく実現することができた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
抽象体から変数を経由せずに具体化を実現する方法は工夫を要するものであった。
その実現にはλ計算におけるλ項の抽象化のプロセスについての考察によりヒントを得ることができた。その結果として、抽象体を変数を用いずに自由代数として実現することができた。
|
| 今後の研究の推進方策 |
これまでに得られている抽象体とその具体化に関する研究は、抽象体の内包的な側面を実現しているにすぎない。現実の数学を支える証明支援系においては、内包的側面だけでなく、外延的側面も扱えるようにする必要がある。そのために、λ計算におけるη同値性について研究を進める予定である。ここにおいても変数の概念を用いずにη同値性を定義する必要があり、従来の研究では見られない困難が予想される。
|
