Quantificateurs en lambda-calcul

Question

J'apprends le lambda-calcul, mais je suis assez confus au sujet des quantificateurs dans le lambda-calcul. Pour autant que je sache, les quantificateurs tels que "∃" sont des concepts de logique du premier ordre (FOL), qui ne sont pas nécessaires pour le lambda-calcul. De plus, je n'ai rien trouvé sur les quantificateurs dans les tutoriels que j'ai lus.

Cependant, je trouve this paper (sémantique de composition basée sur la dépendance lambda ), dans la première page dont l'auteur a utilisé le quantificateur dans le lambda-calcul. Alors, les quantificateurs sont-ils utilisés dans le calcul lambda? Si oui, que veulent-ils dire? Est-ce la même chose que dans FOL?

Answer 1

Le document que vous citez utilise des quantificateurs de manière plutôt informelle, de la même manière qu'il utilise des prédicats. Si vous avez déjà un calcul lambda, vous pouvez, au moins sur le papier, l'étendre avec n'importe quel ensemble de symboles formels que vous voulez, y compris les quantificateurs de FOL. Dans ce cas, les quantificateurs sont quelque chose d'ajouté au calcul, pas une partie de celui-ci.

Les quantificateurs peuvent être définis dans tapé lambda calculus, cependant. Dans les paramètres simplement typés, vous avez les types de fonctions de base, mais ceux-ci peuvent être généralisés au quantificateur universel et dependent function/Pi types. Dans ce cas, les expressions lambda représentent des preuves d'implications et des quantifications universelles, ce qui signifie qu'elles sont construites dans des interprétations sémantiques que vous pouvez donner aux expressions lambda. Les quantificateurs existentiels peuvent alors être définis comme:

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

Qui a les mêmes données que le type de produit ordinaire.