Квантификаторы в лямбда-исчислении

Question

Я изучаю лямбда-исчисление, однако я довольно смущен кванторами в лямбда-исчислении. Насколько я знаю, кванторы, такие как «∃», представляют собой концепции логики первого порядка (FOL), которые не нужны для лямбда-исчисления. Более того, я не нашел ничего о квантификаторах в каких-либо учебниках, которые я прочитал.

Однако я нахожу this paper (Lambda Dependency-Based Compositional Semantics ), на первой странице которого автор использовал квантификатор в лямбда-исчислении. Итак, кванторы используются в лямбда-исчислении? Если да, то что они означают? Это то же самое, что и в FOL?

Answer 1

Бумага, которую вы цитируете, использует несколько квантификаторов несколько неофициально, так же, как использует предикаты. Если у вас уже есть лямбда-исчисление, вы можете, по крайней мере на бумаге, расширить его с помощью любого набора формальных символов, которые вы хотите, включая кванторы из FOL. В этом случае квантификаторы являются чем-то добавленным к исчислению, а не частью его.

Квантификаторы могут быть определены в набраны лямбда-исчисление, однако. В простых типизированных настройках вы имеете базовые типы функций, но их можно обобщить на универсальный квантификатор и dependent function/Pi types. В этом случае лямбда-выражения представляют собой доказательства последствий и универсальных квантификаций, то есть они построены в семантических интерпретациях, которые вы можете дать лямбда-выражениям. Экзистенциальные кванторы могут быть затем определены как;

∃ a: t. P a: = ∀Q. (∀ a: t. P a → Q) → Q

Имеет те же данные, что и обычный тип продукта.