Predicative Lexicographic Path Orders - An Application of Term Rewriting to the Region of Primitive Recursive Functions
Predicative Lexicographic Path Orders - An Application of Term Rewriting to the Region of Primitive Recursive Functions
复制标题
谓词词典路径顺序 - 术语重写在原始递归函数区域中的应用
DOI：
10.1007/978-3-319-12466-7_5
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Naohi Eguchi
中科院分区：
文献类型：
--
作者：
浅見拓哉;和久 剛;全 孝静;松本 健;高橋 智;依馬 正次;Naohi Eguchi
本文提出了一种新的终止顺序--谓词性词典路径顺序（PLPO），它是对词典路径顺序的一种句法限制。除了字典式路径顺序之外，还有几个非平凡的原始递归方程，例如，带有参数替换的原始递归、非嵌套多递归或简单嵌套递归可以用PLPO定向。然而，可以表明PLPO仅在兼容重写系统的导出长度上诱导原始递归上界。这产生了一个经典事实的替代证明，即原始递归函数类在那些非平凡的原始递归方程下是封闭的。
In this paper we present a novel termination order thepredicative lexicographic path order(PLPO for short), a syntactic restriction of the lexicographic path order. As well as lexicographic path orders, several non-trivial primitive recursive equations, e.g., primitive recursion with parameter substitution, unnested multiple recursion, or simple nested recursion, can be oriented with PLPOs. It can be shown that the PLPO however only induces primitive recursive upper bounds on derivation lengths of compatible rewrite systems. This yields an alternative proof of a classical fact that the class of primitive recursive functions is closed under those non-trivial primitive recursive equations.