我正在学习 lambda 演算，但是我对 lambda 演算中的量词感到很困惑。据我所知，“∃”等量词是一阶逻辑（FOL）的概念，lambda演算不需要。此外，在我读过的任何教程中，我都没有找到任何关于量词的内容。
但是，我发现 this paper（基于 Lambda 依赖的组合语义 )，在第一页中作者在 lambda 演算中使用了量词。那么，量词是否用于 lambda 演算？如果是这样，它们是什么意思？和FOL一样吗？
【问题讨论】：
标签： lambda nlp semantics lambda-calculus
您引用的论文在某种程度上使用了量词，就像它使用谓词一样。如果您已经有了 lambda 演算，那么至少在纸面上，您可以使用您想要的任何形式符号集来扩展它，包括 FOL 中的量词。在这种情况下，量词是添加到微积分中的东西，而不是它的一部分。
量词可以在 typed lambda 演算中定义，但是。在简单类型的设置中，您有基本的函数类型，但这些可以推广到通用量词和dependent function/Pi types。在这种情况下，lambda 表达式代表含义的证明和通用量化，这意味着它们构建在您可以赋予 lambda 表达式的语义解释中。存在量词可以定义为;
∃ a : t 。 P a := ∀Q 。 (∀ a : t . P a → Q) → Q
与普通产品类型数据相同。
【讨论】：