5 papers
Semantic Path Orders are Generalized Weighted Path Orders
Teppei Saito, Nao Hirokawa
Monotonic semantic path orders (MSPOs) are powerful reduction orders, but their effective use in theorem proving and termination analysis raises three issues: efficient comparison…
An Applicative Multiset Path Order (Extended Version)
Nao Hirokawa, Teppei Saito, Teppei Tanaka +1
We present a variant of the multiset path order for untyped applicative term rewriting. Compared to existing work, our variant incorporates two distinctive features, dubbed arity a…
Lexicographic Combination of Reduction Pairs (Extended Version)
Teppei Saito, Nao Hirokawa
We present a simple criterion for combining reduction pairs lexicographically. The criterion is applicable to arbitrary classes of reduction pairs, such as the polynomial interpret…
Unifying Semantic Path Order and Weighted Path Order
Teppei Saito, Nao Hirokawa
Monotonic semantic path orders and weighted path orders are powerful reduction orders for proving termination of term rewrite systems. In this paper we present their simple unifica…
Generalizing Weighted Path Orders
Teppei Saito, Nao Hirokawa
We show that weighted path orders are special instances of a variant of semantic path orders. Exploiting this fact, we introduce a generalization of weighted path orders that goes…