Semantic path orders unified with weighted path orders for better term comparison
Semantic Path Orders are Generalized Weighted Path Orders
Logic in Computer Science
Summary
Some computer programs need to prove that processes always finish, rather than running forever. The authors study special mathematical rules called 'semantic path orders' used to compare different steps in these programs to help show they end. They introduce a new, more general rule system that combines earlier methods, making comparisons more efficient and covering more cases. They also adapt this system to advanced techniques used in proving program termination, showing it to be both practical and effective.
What this means in practice
- •For software verification teams: Improve automated checks that confirm a program will complete by using more efficient and comprehensive term comparison rules.
- •For automated theorem proving developers: Enhance theorem provers' ability to prove termination by incorporating generalized weighted path orders that unify existing comparison methods.
Authors
Teppei Saito, Nao Hirokawa
Abstract
Monotonic semantic path orders (MSPOs) are powerful reduction orders, but their effective use in theorem proving and termination analysis raises three issues: efficient comparison of terms, ground totality, and a reduction-pair formulation. Inspired by weighted path orders (WPOs), we introduce generalized weighted path orders (GWPOs) which encompass both WPOs and MSPOs. GWPOs and MSPOs coincide as classes of reduction orders, thereby yielding efficient and ground-total subclasses of MSPOs. We further formulate the reduction-pair version of the GWPO for the dependency pair method, from which a reduction-pair version of the MSPO is obtained. In contrast to the reduction-order setting, the correspondence between GWPOs and MSPOs no longer fully carries over, establishing the GWPO as a framework of independent interest. Effectiveness of the resulting reduction pairs is assessed by standard termination benchmarks.