基于 Girard 可归约性概念的 $\lambda$-项重写关系终止性
计算机科学中的逻辑
2015-09-03 v1 逻辑
摘要
在本文中，我们展示了如何将 Girard 引入的可归约性概念进行扩展，以证明 -项上各类重写关系的终止性。Girard 最初引入该概念是为了证明多态 -演算中 -归约的终止性。我们的扩展利用了可计算性闭包的概念，涵盖了模某等式理论的重写以及模 匹配的重写。这为各种高阶重写框架提供了强大的终止性判据，包括带有简单类型的 Klop 组合归约系统和 Nipkow 高阶重写系统。
引用
@article{arxiv.1509.00649,
title = {Termination of rewrite relations on $\lambda$-terms based on Girard's notion of reducibility},
author = {Frédéric Blanqui},
journal= {arXiv preprint arXiv:1509.00649},
year = {2015}
}