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.

翻译：逻辑约束项重写系统（LCTRSs）是一种程序分析形式化方法，其原生支持非（共）归纳定义的数据类型。作为一种一阶形式化方法，LCTRSs目前仅适用于命令式程序的分析。本文提出了一种LCTRS形式化方法的高阶变体，可用于分析函数式程序。进而我们研究了终止性问题，并为这一新形式化方法定义了高阶递归路径序（HORPO）。