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

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

基本信息

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

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

项目摘要

完備化に基づくプログラム融合変換が失敗した場合には,どのような条件を追加すれば変換が成功するかを調べた.さらに,より広いクラスのプログラムに対して変換が成功するように,完備化手続きの改良を行った.具体的には、項書き換えシステムに基づいた融合変換手続きの形式化を行い、融合変換手続きの停止条件に焦点を絞った解析を行った.その結果,変換途中で生成される項のパターンが高々有限となるための条件と,融合変換手続きの停止条件は密接に関係していることが明らかになった.この成果に基づき,項の反復パターンを発見すると新しい関数として自動的に定義するメカニズムを,完備化手続きに組み込んだ.この拡張された完備化手続き上でプログラム融合変換の実験を計算機上で行ない,従来は完備化が発散して失敗して例に対しても,融合変換が可能となることを示した.さらに,本研究で目指している完備化に基づくプログラム変換の適用範囲を広げることを目的として,帰納的定理の判定問題が決定可能となるための十分条件を解析し,融合変換に帰納的定理を自動適用する可能性を検討した.帰納的定理の判定問題を一般化し,抽象的なリダクションシステムの等価性判定問題としてとらえることにより,書き換え帰納法に基づく簡明で見通しの良い判定条件を与えることに成功した.この条件は,従来知られていた結果の拡張になっている.ここで与えられた決定可能条件は,Kapurら(2000,2001)の条件の一般化となっており,より広いクラスの決定問題に対して適用可能である.

如果基于完成的程序融合转换失败，则添加了哪些条件以使转换成功。此外，改进了完成程序，以确保转换成功为更广泛的程序。具体而言，融合转换过程是根据一词重写系统正式化了正式的，而分析的重点是停止融合转换程序的条件。结果，揭示了转换过程中产生的术语模式的条件最多成为有限的，并且停止融合转换过程的条件密切相关。基于这一成就，将术语自动定义为新功能的迭代模式的机制被整合到完成过程中。在此扩展的完成过程中，我们在计算机上进行了一个实验，以编程融合转换。过去，即使完成分歧和失败，即使是示例，也可以证明融合转换也是可能的。此外，为了基于完成，为了扩大程序转换的范围，我们分析了足够的条件，以确定要确定的归纳定理的确定，并检查了自动将归纳定理应用于融合的可能性，以使归纳定理的确定性和依赖性的确定性为准，以使其逐步确定一个问题，以使其逐步确定，以使我们的判断性更改为一个问题，我们将取消依赖性的确定问题，我们将取消定义问题，以使我们的确定性逐渐确定，我们可以将其逐步确定，以便我们进行了一个平等的确定性问题，我们将基于重写诱导的条件。此条件是先前已知的结果的扩展。此处给出的决定性条件是对Kapur等人的条件的概括。（2000，2001），可以应用于更广泛的决策问题。