宣言型プログラミング言語のためのAC記号のあるナローイングの計算理論

声明式编程语言的 AC 符号窄化计算理论

基本信息

批准号：
14780187
负责人：
青戸等人
金额：
$ 0.7万
依托单位：
Tohoku University
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2002
资助国家：
日本
起止时间：
2002 至 2004
项目状态：
已结题

项目摘要

前年度に得られた高階項書き換え系における帰納的定理証明について解析を進めた.第1階の場合には自明に成立するが,高階では一般に成立しない帰納的定理の性質が単調性である.単調性を満たさないと高階帰納的定理の利用に様々な制約が課せられる.そこで,我々は,高階帰納的定理が単調性を持つための条件について考察した.まず,第1階項書き換え系における十分完全性の概念を拡張し,高階十分完全性の概念を与えた.そして,この概念を用いて,等式が単調高階帰納的定理となるための十分条件を明らかにした.次に,高階十分完全性の自動証明について考察を行なった.高階十分完全性の自動証明を行うため,初等性および高階図式という制約を導入し,高階十分完全性が決定可能となる単純型付き項書換え系のクラスを与えた.初等的な高階図式は多くの自然な高階関数プログラムを含む.以上の結果は,項書き換え分野の代表的な国際会議の1つであるRTA(書き換え技法と応用)'04に採録され,国際的な報告を行なった.前年度に得られた,単純型付き項書き換え系の停止性証明技法の実装について検討を行なった.その実装の第一段階として,より単純な体系である単純型付き適応的項書き換え系の停止性証明技法について考察を行なった.その過程で,適応的項書き換え系についてのみ適用可能な,非常に簡単で,しかも比較的強力な停止性証明技法を考案した.この成果は高階項書き換え系の国際ワークショップHOR'04に採録され,国際的な報告を行なった.

我们已经开始在上一年获得的高阶定期改写系统中分析归纳定理证明。归纳定理的性质在一阶情况下显然是正确的，但在较高顺序中通常不是正确的是单调的。如果不满足单调性，则会对使用高阶归纳定理施加各种限制。因此，我们考虑了具有单调性的高阶定理的条件。首先，我们在一阶术语重写系统中扩展了足够完美的概念，并给出了高阶的完美概念。然后，使用这个概念，我们阐明了方程成为单调高阶归纳定理的足够条件。接下来，我们检查了高阶的自动证明，足够完美。为了执行高阶足够完美的自动证明，我们介绍了初级和高级图的限制，并且有可能确定高阶足够完美。给出了简单的键入术语重写系统的类。基本高阶图包括许多自然的高阶功能程序。上面的结果是在RTA（重写技术和应用程序）'04上进行的，这是该术语重写领域最具代表性的国际会议之一，并在国际上进行了报告。我们检查了上一年获得的简单键入术语重写系统的终止证明技术的实施。作为此实施的第一步，我们讨论了简单的键入术语重写系统的终止证明技术，这是一个更简单的系统。在此过程中，我们设计了一种非常简单且相对强大的终止证明技术，只能应用于自适应术语重写系统。该结果是在国际研讨会HOR'04上对高级期限重写系统进行的，并提交了国际报告。