1987 Fiscal Year Annual Research Report
| Project/Area Number |
62460220
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
佐藤 雅彦 東北大学, 電気通信研究所, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
亀山 幸義 東北大学, 電気通信研究所, 助手 (10195000)
|
|---|
| Keywords | 構成的数学 / 直観主義論理 / 証明 / 検証 / プログラム合成 |
|---|
| Research Abstract |
本年度の研究では, 関数型論理型プログラム言語Qutyと, 構成的数学体系QJを発展させ, 集合に対する記法を持ち体系SST(Symbolic set thepry)を新たに構築した. SSTの特徴は以下の通りである. 1.S式に基づいているため, 論理式や証明をSSTの枠内で表現し, それを計算機の上で処理することが可能になる. 2.型の制約でないλ計算に基づいているので, 不動点演算子により一般の再帰的関数を定義できる. 3.集合を表現する記号Σやπが導入された. これにより, プログラムの仕様を簡潔に書くことができるようになった. 4.SSTの基本関数は, S式に対する操作関数であるが, そのまま関数型プログラム言語を構成する. このプログラム言語sstにより, SST自身を記述することが可能である. 体系SSTに対して, 次の理論的成果を得た. 1.SSTのモデルを作り, 無矛盾であることを示した. 2.realizablity inter pretationにより, 仕様の証明からプログラムを合成できることを示した.
次に, 本年度購入のワークステーションを用いて, プログラム言語sstの処理系を実現した. 最終的には, sstにより, SSTの証明を全て実現するのが目標しため, そのために必要な機能が何であるかを, 実際の処理系をワークステーション上で作動させることにより研究した. また, sstによる自分自身の処理系をワークステーション上に実現し, sstのプログラム言語としての能力が十分あることを実証した.
また, ワークステーションを通信に用いることによって, 国内外の研究者との情報交換を行い, SSTおよびsstを洗練したものにするために, 大いに役立った.
|
Research Products
(1 results)
