基于强可计算性的高阶重写系统静态依赖对方法
计算机科学中的逻辑
2011-09-27 v1
摘要
高阶重写系统(HRS)和简单类型项重写系统(STRS)是函数式程序的计算模型。我们最近提出了一种极其强大的方法——基于强可计算性概念的静态依赖对方法，用于证明STRS中的终止性。在本文中，我们将该方法扩展到HRS。由于HRS包含-抽象而STRS不包含，我们重构了静态依赖对方法以允许-抽象，并表明静态依赖对方法在没有新限制的情况下同样适用于HRS。
引用
@article{arxiv.1109.5468,
title = {Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems},
author = {Keiichirou Kusakari and Yasuo Isogai and Masahiko Sakai and Frédéric Blanqui},
journal= {arXiv preprint arXiv:1109.5468},
year = {2011}
}
备注
IEICE Transactions on Information and Systems (2009)