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

元方程编程基础研究

• 批准号: 04680031
• 负责人: 坂部 俊樹
• 金额: $ 1.15万
• 依托单位: Nagoya University
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for General Scientific Research (C)
• 财政年份: 1992
• 资助国家: 日本
• 起止时间: 1992 至 无数据
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-04680031/
• 关键词: メタプログラミング; メタ等式論理; 書換え型計算モデル; 構造帰納法

本研究では、メタ等式プログラミングの基礎を確立することを目的として、すでに本研究代表者のグループで提案している等式を用いたメタプログラミングのための計算モデルである動的項書換え計算(DTRC)についての研究を進めるとともに、それを単純化ならびに拡張して、新たにメタ項書換え計算(MTRC,Meta-Term Rewriting Calculus)を提案し、MTRCの表現能力を検証した。さらに、任意有限のメタレベルの計算を表現するための計算モデルの研究にも着手した。具体的な研究内容は次の通りである。(1)DTRC上で条件つき項書換え系の実行系を実現し、条件つき項書換え系の解析にDTRCの解析手法が適用できる可能性があることを示した。(2)等式理論の帰納的定理の証明法である構造帰納法、被覆集合帰納法の証明過程の記述ができることを示した。すなわち、与えられた等式理論と証明すべき等式をMTRC項に変換するアルゴリズムを与え、変換先のMTRC項の書換え結果がtrueになれば証明成功と判断できることを示した。さらに、MTRCのインタプリタを関数型プログラム言語MLで実現し、実際に自然数上の可算の結合性、可換性の証明がほとんど自動的に行なえることを明らかにした。(3)whileプログラムのMTRCへの翻訳アルゴリズムを示すとともに、Hoare公理系でのプログラム検証過程をMTRCで記述できることを示した。(3)さらに、MTRCがメタレベル1のメタ計算を表現するのに対して、任意有限のメタレベルのメタ計算を表現できる計算モデルωMRCを提案し、その意味論について検討を加えた。

This study aims to establish the basis of the equation for the calculation of dynamic term conversion calculation (DTRC), which is representative of this study.(MTRC,Meta-Term Rewriting Calculus) This is the first time that any finite element calculation has been performed. Specific research content is divided into two parts. (1)DTRC conditions on the implementation of the system, conditions on the analysis of the system DTRC analysis method is applicable to the possibility of (2)The proof method of the theorem of equation theory is described in the description of the proof process of the structural method and the covering set method. The equation theory proves that the MTRC term is true and the MTRC term is true. In this paper, MTRC's language model is realized, and the proof of computability and commutativity in natural numbers is realized. (3)While the MTRC model of the list is being described, Hoare axioms describe the MTRC model process. (3)In addition, MTRC provides a set of parameters for the calculation of performance, and any finite parameters for the calculation of performance.

项目成果

坂部 俊樹: "メタプログラミング" 電気関係学会東海支部連合大会予稿集. S6-1-S6-2 (1992)

Toshiki Sakabe：“元编程”电气工程学会东海分会会议记录 S6-1-S6-2 (1992)。

結縁 祥治: "無限構造の値を受け渡す通信プロセスのテスト等価性について" 電子情報通信学会技術研究報告. COMP92-20. 31-40 (1992)

Shoji Yuen：“论传递无限结构值的通信过程的测试等价性”IEICE COMP92-20（1992）。

Shoje Yuen: "An Extension of the Testing Method for Processes Passing Infinite values" Proceedings of the First North American Process Algebra Workshop. 10-1-10-20 (1992)

Shoje Yuen：“通过无限值的过程的测试方法的扩展”第一届北美过程代数研讨会论文集。

Su Feng: "Interpretation of Conditinal Term rewriting Systems by DTRC" 日本ソフトウェア科学会第9回全国大会論文集. 313-316 (1992)

苏峰：“DTRC对条件术语重写系统的解释”日本软件学会第九届全国会议论文集313-316（1992）。

大須賀 健: "通信プロセスにおける有限受理グラフを用いた試験等価性の証明法について" 電子情報通信学会技術研究報告. COMP92-72. 39-48 (1992)

Ken Osuka：“关于在通信过程中使用有限接受图证明测试等价性的方法”IEICE COMP92-72 (1992)。