Formulae-as-Types for an Involutive Negation
Résumé
Negation is not involutive in the λC calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by Felleisen and Clements. We introduce polarised, untyped, calculi compatible with extensionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The involution is due to the ℓ delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a constructive interpretation to falsity. We describe the isomorphism there is between A and ¬¬A, and thus between ¬∀ and ∃¬.
La négation n'est pas involutive dans le calcul λC car celui-ci échoue à distinguer les piles capturées des continuations. On montre qu'il y a une correspondance " formule pour type " entre la négation involutive de la théorie de la démonstration, et une notion d'accès de haut niveau aux piles étudiée par Felleisen et Clements. On introduit des calculs polarisés, non typés, compatibles avec l'extensionnalité, à la fois pour le calcul des séquents classique et le déduction naturelle classique, avec des connecteurs pour une négation involutive. L'involution est due à l'opérateur de contrôle délimité ℓ qu'on introduit, qui permet d'implémenter l'idée que les piles capturées, contrairement aux continuations, peuvent être inspectées. Délimiter le contrôle donne par ailleurs une interprétation constructive à l'absurdité. On décrit les isomorphismes qu'il y a entre A et ¬¬A, et par conséquent entre ¬∀ et ∃¬.
Domaines
Logique en informatique [cs.LO]
Origine : Fichiers produits par l'(les) auteur(s)