完備化に基づくプログラム自動変換の研究

基于完备性的程序自动转换研究

基本信息

批准号：
13224003
负责人：
外山芳人
金额：
--
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research on Priority Areas (C)
财政年份：
2001
资助国家：
日本
起止时间：
2001 至无数据
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-13224003/
关键词：
プログラム変換完備化融合交換自動証明

项目摘要

関数型言語MLによるプログラムを対象として、完備化に基づくプログラム融合変換の実験を計算機上で行ない、その動作確認を行うとともに、その変換能力の拡張を試みた。また、融合変換を書き換えシステムの等価変換手続きとしてモデル化し、その動作原理の理論的な解明を進めた。(1)完備化による変換例の収集完備化による融合変換能力を調査するための基礎データとして、計算機上の実験による融合変換の成功例・失敗例の収集を進めた。実験方法は次の通りである。(i)MLプログラムPからP'への融合変換例を文献等から収集(ii)Pに対応する項書き換えシステムRを構成(iii)Rに対して完備化手続きを適用して完備な項書き換えシステムR'に自動変換(iv)得られたR'とP'を比較して完備化による融合変換が成功か否かを判定さらに、変換が失敗した場合には、どのような補題を追加すれば変換が成功するかの実験も合わせて行った。なお、実験対象としたプログラムは、自然数上の関数、リスト処理関数、ブール関数などである。以上の実験を通して当初予定していた基礎データを収集することができた。(2)融合変換の成功条件の解析関数型プログラムの融合変換手続きが必ず成功するための条件に関しては、Wadler(1988)、Chin(1994)、Seidl(1994)、Seidl-Sorensen(1998)らの研究が知られている。しかし、評価メカニズムの違いから、これらの成功条件をそのまま項書き換えシステムに適用することは困難である。そこで、項書き換えシステムに基づいた融合変換手続きの形式的モデルを作成し、融合変換手続きの停止条件に焦点を絞った解析を進めた。その結果、変換途中で生成される項の正規形の個数が高々有限となるための条件と、融合変換手続きの停止条件は密接に関係していることが明らかになった。

对于使用功能语言ML的程序，我们在计算机上进行了一个实验，以根据完成进行程序融合转换，并进行了操作检查，并试图扩展其转换功能。此外，将融合转换建模为重写系统的等效转换程序，并进行了理论上的操作原理。（1）通过完成作为基本数据收集转换示例，以调查通过完整完成的融合转换能力，我们开始使用计算机实验收集成功和失败的融合转换案例。实验方法如下：（i）收集从ML程序P到P'的融合转换示例。此外，如果转换失败，还进行了一个实验，以确定要添加哪种引理以使转换成功。用作实验的程序包括关于自然数，列表处理功能和布尔功能的功能。通过上述实验，我们能够收集最初计划的基本数据。（2）对融合转化的成功条件分析有关在功能程序中融合转化程序的条件的成功条件，Wadler（1988），Chin（1994），Seidl（1994）和Seidl-Sorensen（1998）的研究已知。但是，由于评估机制的差异，很难将这些成功条件直接应用于术语重写系统。因此，创建了基于术语重写系统的融合转换过程的形式模型，并分析着重于停止融合转换过程的条件。结果，揭示了转换过程中产生的正常术语数量的条件最多是有限的，并且停止融合转换过程的条件密切相关。