Higher-Order LCTRSs and Their Termination

TL;DR

This paper introduces a higher-order extension of logically constrained term rewriting systems (LCTRSs) to analyze functional programs and develops a termination analysis method using a higher-order recursive path ordering (HORPO).

Contribution

It presents the first higher-order LCTRS formalism and a novel termination ordering, expanding the applicability of LCTRSs to functional programming analysis.

Findings

Defined a higher-order LCTRS formalism.

Developed a higher-order recursive path ordering (HORPO).

Laid groundwork for termination analysis of higher-order systems.

Abstract

Logically constrained term rewriting systems (LCTRSs) are a program analyzing formalism with native support for data types which are not (co)inductively defined. As a first-order formalism, LCTRSs have accommodated only analysis of imperative programs so far. In this paper, we present a higher-order variant of the LCTRS formalism, which can be used to analyze functional programs. Then we study the termination problem and define a higher-order recursive path ordering (HORPO) for this new formalism.