类型正确的逻辑程序不是错误的。
摘要：逻辑程序的规范类型系统中的陈述性类型系统（如Goedel或Mercury）被考虑在内。在这样的系统中，类型是静态的，但保证了一个操作特性：如果程序“类型良好”，那么在“类型良好”查询开始的所有推导也再次是“类型良好”的。这个特性被称为主题约简。我们证明了这个特性也可以用逻辑程序的证明论语义的特性来表述，从而抽象出平常的操作（自顶向下）语义。这个证明论观点使我们对通常被认为是主题约简必需的条件即头条件进行了质疑。它声明每个子句的头部必须具有一个类型，该类型是声明类型的变体（而不是适当实例）。我们提供了一个更一般的条件，从而重新建立了头部和身体原子之间的一定对称性。这个条件确保在推导中两个统一的术语的类型本身可以统一。我们讨论了这个结果可能的影响。我们还讨论了头条件和多态递归之间的关系，这是函数式编程中已知的一个概念。
作者：Pierre Deransart and Jan-Georg Smaus
论文ID：cs/0012015
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23