二階の書換え系における引数切り落とし法

IR HANDLE Web Site 6 References Open Access

Bibliographic Information

Other Title
  • 2カイ ノ カキカエケイ ニ オケル ヒキスウ キリオトシホウ
  • Argument Filtering Method for Second-Order Higher-Order Rewrite Systems

Search this article

Abstract

Higher-order rewrite systems are computation models of functional programming languages, and the termination property is one of the most important ones of them. Recently, static dependency pair method based on strong computability was introduced, which proves the termination effectively and efficiently. An argument filtering method plays an important role in this method. However, existing argument filtering method in higher-order rewrite systems has two problems: it cannot handle λ-abstraction, and destructs type structures. In order to overcome these problems, we extend the method. Although we did not show its soundness in general, we prove the soundness under the restriction that both sides of rules are either firmness or second-order.

Journal

References(6)*help

See more

Keywords

Details 詳細情報について

Report a problem

Back to top