2011 Fiscal Year Annual Research Report
非同期通信するプログラムを形式的証明から抽出してバグを防ぐ研究
| Project/Area Number |
11J06978
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
平井 洋一 東京大学, 大学院・情報理工学系研究科, 特別研究員(DC2)
|
|---|
| Keywords | 非同期計算 / 中間論理 / 証明論 |
|---|
| Research Abstract |
研究実施計画に記述した通り、「直観主義知識様相を持つ型付きラムダ計算と、ゲーデル=ダメット論理の演繹体系を組み合わせた、waitfree計算のための型付きラムダ計算についての研究を行い、国際会議に投稿」し、FLOPS 2012という国際学会に受理された。この研究に関しては当初のもくろみどおり、「この型付ラムダ計算で記述したプログラムは、すべてwaitfreeという制限のもとで計算できるものであり、逆に、waitfreeという制限のもとで計算できることは、従来の型付ラムダ計算で計算できないような複雑なものを除けば、すべて計算できるという性質である」ということを確かめることができた。これは数理論理学と分散計算という異なる分野の成果をつなげる点で、重要な成果である。ただし平成23年度内の発表を目標としていたが、発表は翌年度5月となった。計画の次の段階「研究したプログラミング言語を、実装して実際の計算機で動かす」を終え、その次の「実際の計算機で動くプログラムを、証明から抽出するという枠組みも実装する」を達成しない段階で、年度を終えた。以上をもって、大まかな目標として掲げた二点のうち一点「直観主義知識様相を持つ型付きラムダ計算を定義して、その分散環境における非同期通信を使った実行を定義し、型がついた項は必ず正常に実行されることを証明する」ということを達成することができた。二点目「プログラム抽出の理論的基盤であるmodified realizabilityの議論に、修士論文で提案した直観主義知識様相を追加する」という点は本研究のためには必要ではないということが、あきらかとなった。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
年次計画に挙げた1年目に挙げた事項2点のうち、1点目「直観主義知識様相を持つ型付きラムダ計算を定義して、その分散環境における実行を定義し、型がついた項は必ず正常に実行されることを証明する」は達成した。2点目「プログラム抽出の理論的基盤であるmpdified realizabilityの議論に、修士論文で提案した直観主義知識様相を追加する」は不要とわかった。さらに2年目に挙げた事項のうち「HaskellまたはOCamlといったような型つきラムダ計算に基づくプログラミング言語の型にも直観主義知識様相を追加して、1年目に考案した型付きラムダ計算の実行系に即した挙動をするように、実行系も改良する。」も達成した。
|
| Strategy for Future Research Activity |
研究課題達成のために必要な段階の半数を、二年間中最初の一年間でこなすことができた。ここで、最終的な目標であるプログラム抽出を厳密に正しいように実装するためには、本年度行った研究を定理証明系を用いて形式化することが得策であるという感触を得ている。この形式化は、研究計画に挙げた意味論の研究の代替となるものである。
|
Research Products
(5 results)
