In this short paper, we present a simple variant of the recursive path ordering, specified for Logically Constrained Simply Typed Rewriting Systems (LCSTRSs). This is a method for curried systems, without lambda but with partially applied function symbols, which can deal with logical constraints. As it is designed for use in the dependency pair framework, it is defined as reduction pair, allowing weak monotonicity.
翻译:在这篇短文中,我们提出了一种递归路径排序的简单变体,专为逻辑约束的简单类型重写系统(LCSTRSs)而设计。该方法适用于柯里化系统,不含lambda但允许部分应用的函数符号,并能处理逻辑约束。由于该排序旨在应用于依赖对框架,其被定义为允许弱单调性的约化对。