Generalizing Weighted Path Orders

TL;DR

This paper introduces a generalized form of weighted path orders, extending their applicability beyond termination proofs, supported by experimental evidence of their viability.

Contribution

It presents a novel generalization of weighted path orders based on semantic path orders, broadening their scope beyond simple termination.

Findings

Generalized weighted path orders are viable in practice.

They are special cases of semantic path orders.

Experimental results support their effectiveness.

Abstract

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.