研究課題/領域番号 |
10139237
|
研究種目 |
特定領域研究(A)
|
配分区分 | 補助金 |
研究機関 | 慶応義塾大学 |
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部, 教授 (30224025)
|
研究期間 (年度) |
1998
|
研究課題ステータス |
完了 (1998年度)
|
配分額 *注記 |
1,400千円 (直接経費: 1,400千円)
1998年度: 1,400千円 (直接経費: 1,400千円)
|
キーワード | タイプ理論 / 項書き換え系 / タイプ推論 / Inductive Types / 停止性 / 並行計算 / 高階関数 / 構成論理 |
研究概要 |
昨年までに確立した融合言語の計算モデル〔これは構成論理と頭書き換え系との両停止性証明(強制規化定理証明)を融合して得られた〕に基づいて、マルチパラダイム・プログラミング方法論の開発を行った。特に、昨年度までに与えたInductive Type推論機構をさらに強めることによって、より一般的なInductive Type推論を我々の融合言語の中で供給できることとなった。また、それに合わせたrecursors等の高階関数定義の枠組の拡張がなされ、これによって高階関数の使用に関して、項書換え(代数的仕様)パラダイムとタイプ理論パラダイムを融合した新しいプログラミング方法論が導入された。 他方、項書き換えパラダイムを、伝統的な項書き換え系のかわりに、並行書き換え処理を遂行うるマルチセット書き換え系(しばしば、並行項書き換え系とも呼ばれる)を利用して拡張することにより、我々の融合言語の枠組が、並行計算プログラミングや実時間システムのプログラミングに適していることも示された。
|