| 研究課題/領域番号 |
25540023
|
|---|
| 研究種目 |
挑戦的萌芽研究
|
| 研究機関 | 筑波大学 |
|---|
研究代表者 |
亀山 幸義 筑波大学, システム情報系, 教授 (10195000)
|
|---|
| 研究期間 (年度) |
2013-04-01 – 2015-03-31
|
| キーワード | ソフトウェア基礎論 / プログラミング言語 / 計算モデル |
|---|
| 研究概要 |
本研究は、必要呼び計算体系においてコントロールオペレータの果たす役割を考察し、適切な定式化を行うことを目的としている。特に、「限定継続」を扱うコントロールオペレータを持つ体系について検討する。
平成２５年度は、futureに基づいた並行計算系における限定継続コントロールオペレータの役割と、限定継続コントロールオペレータ特有の機能である「返り値型の変化（Answer-Type Modification）」について考察を行った。
（１）Scheme言語におけるfutureは、並列計算を導入するためのプリミティブであるが、計算結果が必要になった時点で主計算との間で同期が発生するという点で必要呼び計算と類似した特徴がある。本年度は、futureと限定継続コントロールオペレータを持つ体系を設計し、その体系が意味的に透過であること、すなわち、futureによる並列化が意味を変化させないこと、すなわち、同一の意味を持つ体系における異なる戦略を表現していることを厳密に証明した。
（２）限定継続コントロールオペレータの中で shift/resetと呼ばれるものは、「返り値型の変化」機能を持ち、これは、従来の型理論の範囲では説明がつかない。本年度の研究では、「返り値型の変化」機能を持つコントロールオペレータを、その機能がない（すなわち従来理論で定式化できる）コントロールオペレータに帰着するためのプログラム変換について検討し、そのプログラム変換が適用可能となる十分条件（の１つ）を型システム上の構文的条件として与えた。また、実用的プログラムにおいて返り値型が変化するもののほとんどが、上記の条件を満たすことを示し、本研究の有効性を確認した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究は挑戦的萌芽であり、手がかりが非常に少ない中での検討であったが、限定継続コントロールオペレータと様々な計算戦略の関係、および、その型理論的・論理学的定式化について一定の成果を得たため。（２つの主要成果のうち１つは発表済であり、他方は平成２６年度に発表を計画している。）
|
| 今後の研究の推進方策 |
平成２６年度は、平成２５年度に築いた基本的考察に基づき、限定継続コントロールオペレータを持つ必要呼び計算体系を定式化する。また、その型理論と論理の関係について考察し、論文としてまとめる。
|
| 次年度の研究費の使用計画 |
本研究は基礎理論の構築とそれを実装するシステムの作成の２点からなるが、初年度は基礎理論の構築を行ったため、人件費・謝金（プログラミング作成補助等）の支出がなかったため。
平成２６年度は２年計画の最終年度にあたり、システム作成等のための人件費・謝金等により予算を使用をする計画である。
|
