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