依赖类型λ演算中的冗余性及其对证明搜索的意义
计算机科学中的逻辑
2010-07-07 v1
摘要
依赖类型λ演算（如逻辑框架LF）能够通过类型表示项之间的关系。通过利用“公式即类型”的概念，此类演算还可以在类型判断中编码公式与其证明之间的对应关系。因此，这些演算为指定各种形式系统提供了一种自然且强大的手段。此类规范可以转化为一种更直接的形式，该形式使用基于简单类型λ项上的谓词公式，从而为使用传统逻辑编程技术对其进行动态执行提供了基础。然而，天真地使用这一想法会因依赖类型表达式通常包含大量冗余的类型信息而导致效率低下。我们研究了识别并因此消除此类冗余的句法判据。特别地，我们识别了LF类型中约束变量的一个称为“刚性”的属性，并形式化地证明了：为了确保整个表达式的良构性，检查此类变量的实例化是否符合类型限制是不必要的。我们展示了如何在基于翻译的方法中利用这一属性来执行Twelf语言中的规范。识别冗余性也与设计依赖类型表达式的紧凑表示相关。我们强调了工作的这一方面，并讨论了它与该背景下提出的其他方法的联系。
引用
@article{arxiv.1007.0779,
title = {Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search},
author = {Zachary Snow and David Baelde and Gopalan Nadathur},
journal= {arXiv preprint arXiv:1007.0779},
year = {2010}
}