Improving Static Dependency Pairs for Higher-Order Rewriting
Authors: Carsten Fuhs and Cynthia Kop
Paper Information
Title: | Improving Static Dependency Pairs for Higher-Order Rewriting |
Authors: | Carsten Fuhs and Cynthia Kop |
Proceedings: | WST WST2018proceedings |
Editor: | Salvador Lucas |
Keywords: | higher-order term rewriting, termination analysis, computability, static dependency pairs |
Abstract: | ABSTRACT. We revisit the static dependency pair method for termination of higher-order term rewriting. In this extended abstract, we generalise the applicability criteria for the method. Moreover, we propose a static dependency pair framework based on an extended notion of computable dependency chains that harnesses the computability-based reasoning used in the soundness proof of static dependency pairs. This allows us to propose a new termination proving technique to use in combination with static dependency pairs: the static subterm criterion. |
Pages: | 1 |
Talk: | Jul 19 16:30 (Session 136H: Higher-Order) |
Paper: |