2  Logique classique et continuations

Comme ¬¬ F ⇒ F n’est pas prouvable en NJf, il est tentant d’ajouter une règle de déduction permettant de le prouver. Cette règle correspondra à un nouveau terme à ajouter au λ-calcul. Nous obtiendrons alors un système de démonstration pour la logique classique.

En fait, nous connaissons déjà le nouveau terme à ajouter ! Il s’agit de l’opérateur C de Felleisen [FFKD87], comme l’a découvert Griffin [Gri90]. Raisonnons en effet intuitivement, au niveau des types: C prend une fonction f en argument, et cette fonction prend une continuation k en argument. Une continuation est juste une fonction de type F ⇒ ⊥, où F est le type de la valeur V à retourner, puisque k V ne retourne pas (donc k V est de type ⊥). La fonction f elle-même ne retourne pas non plus, puisque f k est censée toujours appeler une continuation, k ou autre, pour retourner son résultat; donc f est de type (F ⇒ ⊥) ⇒ ⊥ = ¬ ¬ F. Et le résultat de C f est de type F, le type de la valeur passée à la continuation. En somme, C est de type ¬ ¬ F ⇒ F, pour tout F.

Pour des raisons esthétiques, on va préférer considérer que C n’est pas une constante, mais un opérateur unaire du langage, tel que si u : ¬ ¬ F alors C u : F. Une fois qu’on a C, la construction ∇ n’est plus nécessaire: il suffit de poser ∇ u = C (λ z · u), où z n’est pas libre dans u. (On notera que ∇ est essentiellement l’opérateur “abort” A de [FFKD87].) En effet, on a la dérivation:

où la première ligne est obtenue par affaiblissement du typage donné Γ ⊢ u : ⊥ de u.

On obtient le système de déduction naturelle ND suivant pour la logique classique implicationnelle:

Ce système de déduction n’offre plus la symétrie entre règles d’introduction et d’élimination de NJm, NJf et NJi. Ceci est réparé par le λµ-calcul de Michel Parigot [Par92], que nous ne présenterons cependant pas ici.

En attendant, la syntaxe du λ C-calcul est:

et ses règles de réduction sont:

On a laissé de côté la règle ( C_R), à savoir V ( C u) → C (λ k · u (λ x · k (V x))) lorsque V est une P-valeur, car elle est inutile logiquement.

Preuve : Même preuve que pour le théorème 1, en considérant que ⊥ est un type de base, et que les termes neutres sont tous ceux qui ne commencent ni par λ ni par C; la seule différence est qu’il faut vérifier que si u ∈ RED_{¬ ¬ F}, alors C u ∈ RED_F pour tout type F. C’est, comme au théorème 2, par récurrence structurelle sur F.

Si F est un type de base, c’est par récurrence sur ν (u). En effet, C u est dans RED_F si et seulement si u ∈ SN. Soit R une réduction partant de C u. Si R commence par une réduction dans u, i.e. u → u′, alors u′ ∈ SN par hypothèse de récurrence, donc R est finie. Si R commence par une réduction au sommet, alors la seule règle possible était (η C), donc u est de la forme λ k · k u′, k non libre dans u′. Dans ce cas, rappelons que u ∈ RED_{¬¬ F}, donc u ∈ SN par (CR1), donc u′ ∈ SN, d’où R est finie de nouveau. R étant quelconque, C u est dans SN, donc dans RED_F.

Si F est de la forme F₁ ⇒ F₂, montrons que C u v ∈ RED_F2 pour tout v ∈ RED_F1. Notons d’abord que, par hypothèse de récurrence: (*) pour tout w ∈ RED_{¬ ¬ F2}, C w ∈ RED_F2. Notons aussi que C u v est neutre. Montrons alors par récurrence sur ν (u) + ν (v) que C u v ∈ RED_F2, en utilisant (CR3). Le terme C u v peut se réduire en une étape soit vers (1) C u′ v avec u → u′ (qui est donc dans RED_F2 par hypothèse de récurrence), soit vers (2) C u v′ avec v → v′ (même argument), soit vers (3) u′ v par (η C) (avec u = λ k′ · k′ u′, k′ non libre dans u′), soit vers (4) C (λ k · u (λ f · k (f v))).

Dans le cas (4), on a le raisonnement suivant. Rappelons que: (**) si a [x:=b] ∈ RED_G2 pour tout b ∈ RED_G1, alors λ x · a ∈ RED_{G1 ⇒ G2}. C’était le lemme 6, qui se démontre comme nous l’avons fait au cours de la preuve du théorème 1. Supposons que s ∈ RED_{¬ F2} et t ∈ RED_{F1 ⇒ F2} sont des termes arbitraires, s dénotant une valeur possible de k et t une de f:

1. v ∈ RED_F1 par hypothèse;
2. donc tv ∈ RED_F2, par définition de la réductibilité;
3. donc s (tv) ∈ RED_⊥, par définition de la réductibilité;
4. t étant arbitraire, λ f · s (f v) ∈ RED_{¬ (F1 ⇒ F2)}, par (**);
5. donc u (λ f · s (f v)) ∈ RED_⊥, par définition de la réductibilité;
6. s étant arbitraire, λ k · u (λ f · k (f v)) ∈ RED_{¬ ¬ F2}, par (**);
7. donc C (λ k · u (λ f · k (f v))) ∈ RED_F2, par (*).

Dans le cas (3) montrons d’abord que: (***) si λ k′ · k′ u′ ∈ RED_{¬ ¬ F} et k′ n’est pas libre dans u′, alors u′ ∈ RED_F. Ceci se démontre par récurrence structurelle sur F. Si F est un type de base, alors par (CR1) λ k′ · k′ u′ ∈ SN, donc u′ ∈ SN = RED_F. Si F est de la forme F₁ ⇒ F₂, soit v ∈ RED_F1 quelconque, et considérons le terme λ k″ · (λ k′ · k′ u′) (λ x · k″ (xv)). Ce terme est dans RED_{¬ ¬ F2}, en effet, pour tout s∈ RED_{¬ F2} (valeur de k″), pour tout t ∈ RED_F (valeur de x):

1. tv ∈ RED_F2 par définition;
2. donc s (tv) ∈ RED_⊥ par définition;
3. t étant arbitraire, par (**) λ x · s (xv) ∈ RED_{¬ F};
4. puisque par hypothèse λ k′ · k′ u′ ∈ RED_{¬ ¬ F}, (λ k′ · k′ u′) (λ x · s (xv)) ∈ RED_⊥;
5. s étant arbitraire, λ k″ · (λ k′ · k′ u′) (λ x · k″ (xv)) ∈ RED_{¬ ¬ F2}.

Mais ce terme se réduit en λ k″ · k″ (u′v), qui est dans RED_{¬ ¬ F2} aussi, par (CR2). Par hypothèse de récurrence, on en conclut u′v ∈ RED_F2. Comme v est arbitraire, u′ ∈ RED_F. On a donc démontré (***). On traite maintenant le cas (3) en remarquant que si u = λ k′ · k′ u′ ∈ RED_{¬ ¬ F}, alors u′ ∈ RED_F par (***), donc le réduit u′v du cas (3) est dans RED_F2.

En somme, tous les réduits en une étape de C u v sont dans RED_F2. Par (CR3), C u v est donc dans RED_F2, et comme v est arbitraire, C u ∈ RED_{F1 ⇒ F2}.

Le reste de la démonstration consiste à redémontrer le lemme 7, comme lors de la démonstration du théorème 1, par récurrence structurelle sur les termes.     ♦

Exercice 18 ()   Pourquoi la preuve de normalisation forte de λ C plus la règle:

( CR) V ( C u) →  C (λ k · u (λ x · k (V x)))

où V est une P-valeur, est-elle plus difficile ?