SearcharxivSearch

arXiv subjects

Teppei Saito

Publications and source records attributed to Teppei Saito.

3 recordsLinked to original sources

Lexicographic Combination of Reduction Pairs (Extended Version)

We present a simple criterion for combining reduction pairs lexicographically. The criterion is applicable to arbitrary classes of reduction pairs, such as the polynomial interpretation, the matrix interpretation, and the Knuth-Bendix order. In addition, we investigate a variant of the matrix interpretation where the lexicographic order is employed instead of the usual component-wise order. Effectiveness is demonstrated by experiments and examples, including Touzet's Hydra Battle.

cs.LO

Unifying Semantic Path Order and Weighted Path Order

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 unification as reduction orders and reduction pairs. We also discuss the use of it as ground total reduction orders.

cs.LO

Generalizing Weighted Path Orders

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 beyond the realm of simple termination. Experimental data show that generalized weighted path orders are viable.

cs.LO