← 研踪 PaperTrailarXiv:2610.39536 · v1
Semantic Path Orders are Generalized Weighted Path Orders
首次提交 2026-10-29 15:36
版本更新 2026-10-29 15:36
雷达观测 2026-10-30 13:28
摘要
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.
作者备注：38 pages
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v1 · 2026-10-29 15:36 · 最新观测版本
Semantic Path Orders are Generalized Weighted Path Orders
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.
查看此版本解读 →查看此版本原文 ↗