高阶模式补集与严格 Lambda 演算
计算机科学中的逻辑
2008-10-22 v1 编程语言
摘要
我们解决高阶模式在无本具变量重复的情况下的补集问题。与一阶情况不同，模式的补集通常不能由模式或有限的模式集合来描述。因此，我们推广了单类型 Lambda 演算，引入内部严格函数概念，以便直接表达术语必须依赖于给定变量。我们展示，在这种更具表达力的演算中，无重复变量的有限模式集合在补集和交集下是封闭的。我们的主要应用是高阶逻辑程序中基于转换的否定方法。
引用
@article{arxiv.cs/0109072,
title = {Higher-Order Pattern Complement and the Strict Lambda-Calculus},
author = {Alberto Momigliano and Frank Pfenning},
journal= {arXiv preprint arXiv:cs/0109072},
year = {2008}
}
备注
37 pages