On Proving Termination of Term Rewriting Systems with Higher-Order Variables

スポンサーリンク

概要

• 論文の詳細を見る

• We define term rewriting systems with higher-order variables, which are defined without a meta-language like the λ-calculus. On the other hand, our systems express actual functional programming languages like ML and Haskell. In this paper, we extend the recursire path order, the dependency pair and the argument filtering method to our systems. In a different framework, Nipkow also introduced higher-order rewriting systems (HRSs). However, it is more complicated and restricted to extend the recursire path order and the dependency pair method to HRSs. Moreover the argument filtering method cannot be designed essentially in HRSs. These fact proves a usefulness of our systems.

• 一般社団法人情報処理学会の論文
• 2001-07-15

著者

• Kusakari Keiichirou

  Research Institute Of Electrical Communication Tohoku University

関連論文

• On Proving Termination of Term Rewriting Systems with Higher-Order Variables
• On Proving AC-Termination by AC-Dependency Pairs

スポンサーリンク