谓词词典路径序：项重写在原始递归函数区域的应用
逻辑
2014-06-03 v5 计算机科学中的逻辑
摘要
本文提出了一种新的终止序，即谓词词典路径序（简称 PLPO），它是词典路径序的一种句法限制。与词典路径序一样，PLPO 可用于定向若干非平凡的原始递归方程，例如带参数替换的原始递归、非嵌套多重递归或简单嵌套递归。可以证明，PLPO 仅对兼容重写系统的推导长度施加原始递归上界。这为原始递归函数类在这些非平凡原始递归方程下封闭这一经典事实提供了另一种证明。
引用
@article{arxiv.1308.0247,
title = {Predicative Lexicographic Path Orders: An Application of Term Rewriting to the Region of Primitive Recursive Functions},
author = {Naohi Eguchi},
journal= {arXiv preprint arXiv:1308.0247},
year = {2014}
}
备注
Technical Report