Term Orders for Optimistic Lambda-Superposition

TL;DR

This paper introduces two new variants of classical term orders, λKBO and λLPO, tailored for the λ-superposition calculus, and demonstrates their properties through encodings into standard first-order orders.

Contribution

The paper presents novel λ-variants of KBO and LPO specifically designed for λ-superposition, extending the applicability of these orders in higher-order rewriting.

Findings

λKBO and λLPO are effective for λ-superposition

Properties are established via encodings into first-order KBO and LPO

Enhances termination proving in higher-order rewriting systems

Abstract

We introduce $\lambda$KBO and $\lambda$LPO, two variants of the Knuth-Bendix order (KBO) and the lexicographic path order (LPO) designed for use with the $\lambda$-superposition calculus. We establish the desired properties via encodings into the familiar first-order KBO and LPO.