氏名: 渡辺 啓嗣 (289634520)
論文題目: 高階項書換え系の停止性に関する研究
論文概要
高階項書換え系(Higher Order Rewriting Systems, HRS)は、高階関数の計
算を形式的に表すモデルとして近年注目され、関数型言語の計算モデルや、
定理自動証明、代数的仕様記述などに利用されている。また、HRSの性質の一つと
して停止性がある。停止性とは、計算がその過程によらず必ず停止し、値
を返すことを保証する非常に重要な性質である。しかし、HRSの停止性は決
定不可能な問題であるため、停止性を保証する十分条件が研究されている。
一方、一階の項を書き換え対象とする項書換え系(Term Rewriting
Systems, TRS)に対し、近年ArtsとGieslにより依存対を用いた停止性判定手
法が提案された。この手法を用いることによって、より多くのTRSの停止性を
検証することが可能である。
本論文では、HRSに対して依存対を用いた場合の問題点を考察し、依存対を
HRS上に自然に拡張する。また、依存対と停止性の関係を明らかに
し、HRSの停止性を判定する新しい手法を提案する。
さらに、停止性判定に必要となる擬順序をTRS上の擬順序であるGPO(General
Path Ordering)をHRS上に拡張す
ることによって提案する。この擬順序は代入に関して安定になるよう改良
されている。
目次に戻る