用塔斯基的不动点定理扩展构造演算
摘要：用Tarski的最小不动点定理作为在归纳构造演算中定义递归函数的基础。这扩大了可以在基于类型论的定理证明工具中建模的函数类别，包括潜在的非终止函数。只有我们通过添加对应于经典逻辑的公理来扩展逻辑框架，才有可能实现这一点。我们声称扩展的框架使得可以推理终止和非终止计算，并且我们证明了归纳构造演算常见的功能，如程序提取，也可以用于处理新的函数。
作者：Yves Bertot (INRIA Sophia Antipolis)
论文ID：cs/0610055
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23