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

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

基本信息

批准号：
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'从文献中收集的融合转换示例等。（ii）官员重写系统R组成为（iii）r（iii）r（iii）r，并将完整的终止程序应用于R进行R比较在系统r上获得了R'和p'，确定通过完全增强的融合转换是否成功，如果转换失败，则还添加了任何主题。此外，针对实验的程序包括自然数，列表处理功能和BOOL功能的功能。通过这些实验，我们能够收集最初计划的基本数据。（2）对于成功融合转换条件的分析函数类型程序的融合转换程序的条件，Wadler（1988），Chan（1994），Seidl（1994），Seidl-Sorensen（1998）和其他研究是已知的。但是，由于评估机制的差异，很难将这些成功条件应用于术语替代系统。因此，创建了基于术语重写系统的融合转换过程的形式模型，并促进了针对融合转换过程停止条件的分析。结果，揭示了转换过程中产生的常规形式的数量是高度有限的，并且融合转换过程的停止条件密切相关。