代数的メタプログラミングに関する基礎的研究

1997 年度 実績報告書

• 研究課題/領域番号: 08458067
• 研究機関: 名古屋大学
• 研究代表者: 濱口 毅 名古屋大学, 大学院・工学研究科, 助手 (90273284)
• 研究分担者: 河口 信夫 名古屋大学, 大学院・工学研究科, 助手 (10273286) ; 結縁 祥治 名古屋大学, 大学院・工学研究科, 助手 (70230612) ; 阿草 清滋 名古屋大学, 大学院・工学研究科, 教授 (90026360) ; 稲垣 康善 名古屋大学, 大学院・工学研究科, 教授 (10023079) ; 坂部 俊樹 名古屋大学, 大学院・工学研究科, 教授 (60111829)
• キーワード: メタ計算 / 書換え計算 / 項書換え系 / 並行計算 / 検証 / 代数的仕様 / 帰納的定理 / 被覆集合帰納法

研究概要

本年度の研究では、型推論に基づく型なしオブジェクト指向プログラムの代数的意味論を提示し、オブジェクト指向プログラムによる代数的仕様の実現が正しいことを証明する基礎を与えた。この意味論では、まず、型のないオブジェクト指向プログラムのすべての部分式にクラス名の集合からなる型を割り当てる。これは、部分式の型を表す型変数に関する代数方程式を構成し、それを解くことで行われる。割り当てられた型をソ-トと見なして、オブジェクト指向プログラムのクラスの意味である代数的仕様を抽出する。オブジェクト指向プログラムPによる代数的仕様Sの実現の正しさは、Pの意味である代数的仕様SpがSの観測的実現になっていることを、文脈帰納法、co-inductionなどを使って証明することができ、その証明の自動化に代数的メタ計算が応用できると期待される。
その他、項集合書換え系、分散型計算機への項書換え系の効率的実現、左非整合な項書換え系のクラスと関数型戦略の関係、形式的仕様からの通信プログラムの生成、ラベル付き遷移システムの視覚的デバッグ支援に関する研究も行い、プログラム検証の基礎的成果を得た。

研究成果

• [文献書誌] S.Feng, T.Sakabe, T.Inagaki: "Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus" IEICE Trans.on Information and Systems. E80-D,6. 625-645 (1997)
• [文献書誌] 結縁、坂部、稲垣: "正則な実時間通信プロセスに対するテスト擬順序の記号的特性化、" 電子情報通信学会 論文誌. J80-D-I,6. 474-484 (1997)
• [文献書誌] 粕谷、酒井、山本、阿草: "項集合書換え系とその合流性" 電子情報通信学会 論文誌. J80-D-I,4. 325-334 (1997)
• [文献書誌] 峰巣、山本、濱口、阿草: "An Efficient Implementation of Term Rewriting System on a Distributed Memory Architecture" IEICE Trans.on Information and Systems. E80-D,4. 510-517 (1997)
• [文献書誌] M.Sakai: "Left-Incompatible Term Rewriting Systems and Functional Strategy" IEICE Trans.on Information and System. E80-D,12. 1176-1182 (1997)