1  Types simples et logique minimale

1.1  Types simples

Essayons quelques idées simples pour attribuer des types à des λ-termes. Nous revenons ici au λ-calcul pur, avec variables, applications et abstractions uniquement.

Nous nous donnons une algèbre de types simples, qui sont des expressions F obéissant à la grammaire:

où b parcourt un ensemble de types de base, typiquement nat, int, string, bool, etc. Intuitivement, la sémantique d’un type est un ensemble de valeurs, par exemple nat pourra représenter l’ensemble N des entiers naturels. Intuitivement encore, un type de la forme F₁ ⇒ F₂ dénote l’ensemble de toutes les fonctions de F₁ vers F₂.

Syntaxiquement, nous utiliserons des parenthèses pour désambigüer les expressions de types. Nous noterons F₁ ⇒ F₂ ⇒ F₃ pour F₁ ⇒ (F₂ ⇒ F₃), le type des fonctions à deux arguments de types respectifs F₁ et F₂, retournant un résultat de type F₃.

Dans une application uv, il est alors naturel de supposer que u a un type de la forme F₁ ⇒ F₂: l’expression uv n’est légale que si u est une fonction, ici du type F₁ vers F₂. Nous demandons alors que v soit aussi de type F₁, alors uv sera naturellement de type F₂. Ceci mène à une règle provisoire de la forme:

Pour typer les variables, c’est plus délicat, et il y a principalement deux solutions. La première est de supposer que toute variable x a un type uniquement déterminé précisé à l’avance; si F est ce type, on notera x_F au lieu de x pour le préciser clairement. Cette solution est celle des λ-calculs typés, et on aura la règle suivante pour typer les variables:

tandis que pour les abstractions, on aura:

Cette première solution a l’avantage que si un terme est typable, alors il a un type unique, mais présente notamment l’inconvénient d’être incompatible avec l’α-renommage tel qu’il a été présenté jusqu’ici: remplacer une variable liée x_F par une y_F′ ne doit être autorisé que si F′ = F. La deuxième solution est d’utiliser des jugements de typages, ou séquents, de la forme x₁ : F₁, …, x_n : F_n ⊢ u : F. La partie gauche Γ =_def x₁ : F₁, …, x_n : F_n est appelée le contexte de typage, et enregistre les hypothèses de typage sur les variables libres de u (et éventuellement d’autres variables). Rendre explicite ce contexte aura d’autres avantages, comme on le verra par la suite. Formellement:

La règle (Var) se lit: x est de type F dans tout contexte contenant la liaison x : F. En effet, un tel contexte est exactement un contexte de la forme Γ, x : F pour un certain Γ. Dans la règle (Abs), l’introduction de y dans la prémisse permet d’inclure le α-renommage dans les règles de typage. Nous ferons cependant toujours l’hypothèse (abusive) que les termes sont vus à α-renommage près, alors (Abs) se simplifie en:

en supposant que x peut toujours être renommée implicitement de sorte à ne pas être dans le domaine de Γ.

Exercice 8 ()   Montrer que le terme de Maurey G_{V, F} est typable, mais que bien que l’on ait:

GV, F ⌈m⌉ ⌈n⌉ →*

⎧ ⎨ ⎩

V si m≤ n F sinon

G_{V, F} n’a le type nat_F1 ⇒ nat_F2 ⇒ bool_F3, pour aucun types F₁, F₂, F₃, et dans aucun contexte.

Une propriété importante que les λ-termes possèdent est la suivante, qui exprime que les programmes ne changent pas de type pendant l’exécution. Cela peut paraître trivial, mais il faut le vérifier.

Preuve : Par récurrence d’abord sur la longueur de la réduction de u vers v, ensuite sur la profondeur du rédex contracté dans u. Les cas de récurrence sont triviaux, traitons donc des cas de base, où u est lui-même le rédex contracté.

(β)

u est de la forme (λ x · s) t et v = s[x:=t]. Le typage de u se termine donc forcément par:

Il ne reste plus qu’à montrer que Γ ⊢ s [x:=t] : F est dérivable aussi. Nous montrons plus généralement que si Γ, x : F₁, Δ ⊢ s : F a une dérivation π₁, alors Γ, Δ ⊢ s[x:=t] : F est dérivable aussi, par récurrence structurelle sur π₁.

• Si π₁ se termine par une règle (Var), alors soit s ≠ x, donc s est une variable y telle que y : F est dans Γ, Δ, s[x:=t] = y, et nous dérivons Γ, Δ ⊢ s[x:=t] : F par la règle (Var); soit s = x. Dans ce dernier cas, F = F₁, et nous devons dériver Γ, Δ ⊢ t : F, sachant que nous avons déjà une preuve π₂ de Γ ⊢ t : F₁. C’est une conséquence du lemme suivant, qui dit essentiellement qu’on peut toujours ajouter des hypothèses de typage inutiles:
  Lemme 2 (Affaiblissement)   Si Γ ⊢ t : F est dérivable, alors Γ, Δ ⊢ t : F aussi.
  Preuve : Récurrence structurelle facile sur la dérivation de typage donnée. Intuitivement, on ajoute Δ à gauche de tous les jugements dans la dérivation.     ♦
• Si π₁ se termine par une règle (App), alors s est de la forme s₁ s₂ et π₁ se termine par:

  

  Par récurrence, Γ, Δ ⊢ s₁[x:=t] : F′₁ ⇒ F et Γ, Δ ⊢ s₂[x:=t] : F′₁ sont dérivables, donc aussi Γ, Δ ⊢ s[x:=t] : F par (App), puisque s[x:=t] = (s₁[x:=t]) (s₂[x:=t]).

• Si π₁ se termine par une règle (Abs), alors s est de la forme λ y · s₁, F est de la forme F′₁ ⇒ F′₂ et π₁ se termine par:

  

  Par récurrence (avec Δ remplacé par Δ, y : F′₁), on peut dériver Γ, Δ, y : F′₁ ⊢ s₁ [x:=t] : F′₂, donc Γ, Δ ⊢ λ y · (s₁[x:=t]) : F′₁ ⇒ F′₂ par (Abs). Mais λ y · (s₁[x:=t]) = (λ y · s₁) [x:=t] = s[x:=t] car y n’est pas libre dans t et x≠ y. En effet, y n’est pas libre dans t car toutes les variables libres de t sont dans domΓ (ceci vient du lemme suivant), et y n’est pas dans domΓ par construction.

  Lemme 3   Si Γ ⊢ t : F est dérivable, alors fv(t) ⊆ domΓ.

  Preuve : Récurrence structurelle triviale sur la dérivation donnée.     ♦

(η)

u est de la forme λ x · vx avec x non libre dans v, F est de la forme F₁ ⇒ F₂, et le typage de u doit se terminer par:

Mais la sous-dérivation π₁ conclut déjà Γ, x : F₁ ⊢ v : F₁ ⇒ F₂. On conclut par le lemme:

Lemme 4 (Amincissement)   Si Γ, x : F₁ ⊢ v : F est dérivable et x n’est pas libre dans v, alors Γ ⊢ v : F est dérivable.

Preuve : Récurrence structurelle triviale sur la dérivation donnée.     ♦

    ♦

Le lemme 1 dit que si u se réduit en v, v a tous les types que u possède, mais v peut en acquérir de nouveaux:

Le λ-calcul simplement typé est alors confluent:

Preuve : Il existe un λ-terme v tel que u₁ →^* v et u₂ →^* v parce que le λ-calcul (non typé) est confluent. Ce terme v est alors lui-même typable, car tout typage de u en est un de v, par le lemme 1.     ♦

La propriété la plus intéressante du λ-calcul simplement typé, et qui le distingue du λ-calcul non typé est le théorème suivant:

Preuve : Il suffit de le démontrer pour →_βη. L’argument le plus simple est dû à W. W. Tait, cf. [GLT89], que l’on peut présenter comme une version corrigée d’une tentative de preuve qui ne fonctionne pas. (Cette façon de présenter est due à Jean Gallier.)

Soit SN l’ensemble de tous les λ-termes fortement normalisants (pour “Strongly Normalizing”). On voudrait démontrer que si Γ ⊢ u : F est dérivable, alors u ∈ SN. Essayons de le démontrer par récurrence structurelle sur u. Si u est une variable, c’est évident car u est normal. Si u est une abstraction λ x · u₁, alors les seules réductions partant de u sont dans u₁ (ces réductions sont finies, par récurrence) ou bien de la forme u →_ηv →^* …, avec u₁ = vx, x non libre dans v, auquel cas l’hypothèse de récurrence s’applique encore et les réductions obtenues sont encore finies. Toutes les réductions partant de u sont finies, donc u ∈ SN. Malheureusement, dans le dernier cas où u est une application u₁ u₂, on ne peut pas conclure, et cette démonstration échoue.

Dans cette tentative de démonstration, il y a un ingrédient que nous n’avons pas utilisé: le fait que u était typable. Nous allons donc introduire une notion, dite de réductibilité mais n’ayant que peu de choses à voir avec l’existence de réductions, faisant intervenir les types et qui impliquera la normalisation forte.

Disons que u est réductible au type F, en abrégé u ∈ RED_F si et seulement si:

• F est un type de base b et u ∈ SN;
• ou F est de la forme F₁ ⇒ F₂, et pour tout v ∈ RED_F1, uv ∈ RED_F2.

Il s’agit d’une définition licite, par récurrence structurelle sur le type F.

Nous utiliserons dans la suite trois principes de récurrence.

1. D’abord, nous aurons la récurrence structurelle sur le type F comme ci-dessus;
2. ensuite, nous aurons la récurrence structurelle sur les dérivations de typage;
3. enfin, pour tout terme v ∈ SN, nous aurons le principe de récurrence sur ν (v), où ν (v) est la longueur de la plus grande réduction partant de v.

La quantité ν (v) existe pour v ∈ SN parce qu’il n’existe pas de réduction infinie partant de v: organisons les réduits de v en arbre, dont v est la racine, les fils d’un nœud étant ses réduits en une étape; comme v ∈ SN, cet arbre n’a pas de branche infinie; de plus, l’arbre est à branchement fini, c’est-à-dire que tout nœud n’a qu’un nombre fini de successeurs; dans ces conditions, le lemme de Kőnig énonce que l’arbre est fini, et il a donc une plus longue branche.

Le lemme important à observer est le suivant. Sa démonstration est immédiate.

Pour les formalistes, on pourrait préférer au principe de récurrence sur ν (v) le principe de récurrence le long de la relation de réduction →, qui s’exprime comme suit: pour prouver que la propriété P est vraie de tous les termes v de SN, il suffit de la prouver sous l’hypothèse de récurrence que P (v′) est vraie pour tout réduit en une étape de v. (Le cas de base est implicite dans cette définition: c’est celui des termes normaux, qui n’ont aucun réduit en une étape.) La validité de ce principe de récurrence est équivalente au fait que ∀ v · (∀ v′ · v → v′ ⇒ P (v′)) ⇒ P (v) implique ∀ v ∈ SN · P (v). Ce principe serait valide même en l’absence de la propriété de branchement fini, et est justifié comme suit. Si cette dernière implication était fausse pour une certaine propriété P, il existerait un terme v ∈ SN tel que P (v) soit fausse. Mais comme ∀ v · (∀ v′ · v → v′ ⇒ P (v′)) ⇒ P (v), il existerait un terme v′ avec v → v′ tel que P (v′) soit fausse aussi; donc de nouveau un terme v″ avec v′ → v″ tel que P (v″) soit fausse, et ainsi de suite: ceci fournirait une réduction infinie à partir de v, contredisant le fait que v ∈ SN.

1em Montrons maintenant que tout terme réductible est fortement normalisant. C’est la propriété (CR1) ci-dessous, les autres sont des propriétés que nous devons montrer par récurrence simultanée sur les types F. Un terme est dit neutre s’il n’est pas une abstraction.

• (CR1) Si u ∈ RED_F, alors u ∈ SN.
• (CR2) Si u ∈ RED_F et u →_βη u′, alors u′∈ RED_F.
• (CR3) Si u est neutre et pour tout u′ tel que u →_βη u′, u′ ∈ RED_F, alors u ∈ RED_F.

Démontrons donc ces propriétés par récurrence simultanée sur F. Si F est un type de base, (CR1) est vérifiée par définition; (CR2) est évidente, car toute sous-suite d’une réduction finie est finie; pour (CR3), supposons que pout tout u′ tel que u →_βη u′, u′ ∈ SN: toute réduction partant de u passe après une étape par un tel u′ et est donc finie, donc u ∈ SN = RED_F.

Considérons maintenant le cas inductif, où F est de la forme F₁ ⇒ F₂:

• (CR1): soit u ∈ RED_F. Par définition, pour tout v ∈ RED_F1, uv ∈ RED_F2. Posons v =_def x, une variable. Par hypothèse de récurrence sur F₁, cas (CR3), x ∈ RED_F1; en effet, x est neutre et ne se réduit en aucun terme. Donc ux ∈ RED_F2. Par hypothèse de récurrence sur F₂, cas (CR1), ux ∈ SN. Mais toute réduction partant de u induit une réduction correspondante dans ux, et est donc finie. Ainsi u ∈ SN.
• (CR2): soit u ∈ RED_F, u →_βη u′. Fixons un v ∈ RED_F1 arbitraire. Par définition, uv ∈ RED_F2. Mais uv →_βη u′v, donc par hypothèse de récurrence sur F₂, cas (CR2), u′v ∈ RED_F2. Comme v ∈ RED_F1 est arbitraire, u′ ∈ RED_F.
• (CR3): soit u neutre tel que: (*) pour tout u′ tel que u →_βη u′, u′ ∈ RED_F. Nous devons montrer que u ∈ RED_F, et pour ceci nous disposons d’hypothèses de récurrence, parmi lesquelles: (**) pour tout v ∈ RED_F1, tout réduit v′ en une étape de v est dans RED_F1, laquelle est l’hypothèse de récurrence (CR2) sur F₁; et (†) pour tout terme neutre w dont tous les réduits en une étape sont dans RED_F2, alors w aussi: c’est l’hypothèse de récurrence (CR3) sur F₂.

  Pour montrer que u ∈ RED_F, il suffit de montrer, par définition, que uv ∈ RED_F2 pour tout v ∈ RED_F1. Nous démontrons ceci par récurrence sur ν (v), qui est bien défini car RED_F1 ⊆ SN, par hypothèse de récurrence sur F₁. Comme u est neutre, uv ne peut se réduire qu’en un terme de la forme u′v avec u → u′, ou bien en un terme uv′ avec v → v′. Mais par (*), u′ ∈ RED_F, donc u′v ∈ RED_F2; d’autre part, par (**) v′ ∈ RED_F1, donc l’hypothèse de récurrence s’applique, impliquant que uv′ aussi est dans RED_F2. Comme tous les réduits en une étape de uv sont dans RED_F2, on peut utiliser (†) avec w = uv et en déduire que uv ∈ RED_F2, comme on voulait le démontrer. Finalement, ce que nous avons démontré par récurrence c’est que: pour tout v ∈ SN, si v ∈ RED_F1 alors uv ∈ RED_F2. Mais par hypothèse de récurrence (CR1) sur F₁, tout v ∈ RED_F1 est dans SN. Donc nous avons montré que pour tout v ∈ RED_F1, uv ∈ RED_F2. Comme v ∈ RED_F1 est arbitraire, par définition de la réductibilité u ∈ RED_F.

Dans la suite, nous aurons besoin du lemme suivant, qui se démontre par une technique similaire à celle du cas (CR3) ci-dessus:

Preuve :

Posons Q (u) la propriété: u [x:=v] ∈ RED_F2 pour tout v ∈ RED_F1. Pour démontrer le résultat, il suffit par définition de montrer que (λ x · u) v ∈ RED_F2 pour tout u vérifiant Q (u) et tout v ∈ RED_F1. C’est la définition de RED_{F1 ⇒ F2}.

Nous le démontrons par récurrence double faible sur ν (u) + ν (v). Notons que ν (u) est bien défini, parce que Q (u) appliqué à v=x implique que u est dans RED_F2, donc dans SN par (CR1); et que ν (v) est bien défini car v ∈ RED_F1 ⊆ SN, de nouveau par (CR1).

Les réduits en une étape de (λ x · u) v sont soit de la forme (λ x · u′) v où u′ est un réduit en une étape de u, soit de la forme (λ x · u) v′ où v′ est une réduit en une étape de v, soit de la forme u [x:=v] (par β-réduction), soit de la forme u₁ v où u = u₁ x est x n’est pas libre dans u₁ (η-réduction). Dans le premier cas, on applique l’hypothèse de récurrence, en notant que ν (u) + ν (v) > ν (u′) + ν (v). On doit vérifier que Q (u′) est toujours vraie: c’est parce que u [x:=v] → u′ [x:=v], et en utilisant (CR2) sur F₂. Dans le deuxième cas, on applique de nouveau l’hypothèse de récurrence, en vérifiant que v′ est encore dans RED_F1, par (CR2) de nouveau, sur F₁ cette fois-ci. Dans le troisième cas, u [x:=v] est dans RED_F2 parce que Q (u) est vérifiée. On vérifie aisément que le quatrième et dernier cas est un cas particulier du troisième. Donc tous les réduits en une étape de (λ x · u) v sont dans RED_F2. Or (λ x · u) v est neutre, donc (CR3) s’applique: (λ x · u) v lui-même est dans RED_F2.     ♦

Montrons maintenant par récurrence sur les termes que tout terme typable est réductible. Plus précisément, on aimerait démontrer que si Γ ⊢ u : F est dérivable, alors u ∈ RED_F. Mais ceci se heurte à exactement le même genre de problèmes que le fait d’essayer de démontrer directement que tout λ^*-terme termine (lemme 3 du premier poly).

Nous démontrons donc que:

Preuve : Rappelons que la notation u [x₁:=v₁, …, x_n:=v_n] dénote ici la substitution en parallèle de x₁ par v₁, …, de x_n par v_n.

Montrons le résultat par récurrence structurelle sur la dérivation de typage donnée de u. Si la dernière règle est (Var), alors u est une variable x_i, 1≤ i≤ n, par hypothèse u [x₁:=v₁, …, x_n:=v_n] = v_i ∈ RED_Fi, et F_i = F par typage, donc u [x₁:=v₁, …, x_n:=v_n] ∈ RED_F.

Si la dernière règle de la dérivation est (App), alors u est une application u₁ u₂, où l’on a dérivé Γ ⊢ u₁ : G ⇒ F est Γ ⊢ u₂ : G pour un certain type G par des dérivations plus petites. (On abrège x₁:F₁, …, x_n:F_n en Γ; de même, notons σ la substitution [x₁:=v₁, …, x_n:=v_n].) Donc par hypothèse de récurrence u₁ σ ∈ RED_{G ⇒ F} et u₂ σ ∈ RED_G, d’où, par définition de RED_{G ⇒ F}, u σ = (u₁ σ) (u₂ σ) ∈ RED_F.

Si la dernière règle est (Abs), fixons d’abord v₁ ∈ RED_F1, …, v_n ∈ RED_Fn. Comme la dernière règle est (Abs), u est de la forme λ x· u₁, et l’on peut de plus supposer par α-renommage que x n’est pas libre dans v₁, …, v_n, et différente de x₁, …, x_n. De plus, F est de la forme F_n+1 ⇒ G pour certains types F_n+1 et G, et l’on a dérivé x₁: F₁, …, x_n:F_n, x:F_n+1 ⊢ u₁ : G par une dérivation plus petite. Par hypothèse de récurrence, u₁ [x₁:=v₁, …, x_n:=v_n, x:=v] ∈ RED_G pour tout v ∈ RED_Fn+1. Mais l’on remarque que u₁ [x₁:=v₁, …, x_n:=v_n, x:=v] = u₁ [x₁:=v₁, …, x_n:=v_n] [x:=v], car x n’est pas libre dans v₁, …, v_n. Par le lemme 6, λ x · (u₁ [x₁:=v₁, …, x_n:=v_n]) ∈ RED_F. De nouveau parce que x n’est pas libre dans v₁, …, v_n, et que x est différente de x₁, …, x_n, u [x₁:=v₁, …, x_n:=v_n] = λ x · (u₁ [x₁:=v₁, …, x_n:=v_n]), et l’on conclut.     ♦

Appliquons maintenant le lemme 7 au cas où v₁=x₁, …, v_n=x_n. C’est certainement possible, car par (CR3) toute variable est réductible à tout type. Donc u ∈ RED_F. Par (CR1), u ∈ SN.     ♦

En somme, un programme simplement typé finit toujours par s’arrêter. Ce n’est pas le cas dans la plupart des langages de programmation, y compris Pascal et OCaml, qui sont pourtant des langages typés. La raison principale est que ces langages fournissent tous une construction primitive de boucles ou de récursion (let rec en OCaml). De façon analogue, on peut voir cette capacité de récursion comme l’existence dans ces langages d’un opérateur de point fixe Y de type (F ⇒ F) ⇒ F, avec comme règle de réduction Y f → f (Y f). Le λ-calcul simplement typé enrichi avec un tel opérateur Y n’est alors plus fortement normalisant.

La propriété de normalisation forte, pour étrange qu’elle paraisse dans un cadre de langage de programmation, sera centrale dans la section qui suit.

1.2  Logique minimale

Si l’on regarde les règles de typage simple du λ-calcul, et que l’on efface les λ-termes et les variables des jugements de typage, on obtient les règles suivantes, formant le système NJm:

Or si on lit maintenant ces règles en interprétant les types F comme des formules, le symbole ⇒ comme l’implication logique, et les jugements F₁, …, F_n ⊢ F comme des affirmations de la forme “sous les hypothèses F₁, …, F_n, la formule F est vraie”, alors ces règles fournissent un système de déduction logique tout à fait correct. La première règle dit que l’on peut toujours déduire une formule faisant partie de l’ensemble d’hypothèses, la deuxième est le modus ponens, ou élimination de l’implication, qui permet les déductions logiques: si F₁ implique F₂, et d’autre part F₁ est vraie, alors F₂ l’est aussi; la troisième est le théorème de la déduction, ou introduction de l’implication: pour prouver que F₁ implique F₂ (conclusion de la règle), il suffit de poser F₁ en nouvelle hypothèse et de démontrer F₂ (prémisse).

Un tel système de déduction est appelé système de déduction naturelle, et a été inventé par Gerhard Gentzen dans les années 30. Un tel système est caractérisé par le fait que toutes les règles agissent sur les formules à droite du symbole ⊢.

On ne peut pas démontrer toutes les formules valides de la logique propositionnelle classique en NJm. Par exemple, ((F₁ ⇒ F₂) ⇒ F₁) ⇒ F₁, la loi de Peirce, n’est pas prouvable en NJm, bien qu’elle soit vraie en logique classique (exercice: tester la valeur de la formule quand F₁ et F₂ parcourent l’ensemble des booléens, et vérifier cette dernière assertion). La logique que le système de déduction NJm définit est une logique différente, appelée logique intuitionniste minimale, ou logique minimale.

Comme on le voit, il y a correspondance bijective entre les règles de déduction de logique minimale et les règles de typage du λ-calcul. Ceci implique qu’il y a correspondance entre preuves en logique minimale et λ-termes simplement typés: on obtient un λ-terme u tel que x₁:F₁, …, x_n:F_n ⊢ F à partir d’une preuve de F₁, …, F_n ⊢ F en NJm en remplaçant les axiomes F₁, …, F_n, …, F_k ⊢ F_i par une variable x_i, les éliminations de l’implication par des applications et les introductions de l’implication par des abstractions.

Réciproquement, tout λ-terme u dénote un squelette de preuve, qui peut être complété en une preuve réelle si et seulement si u est simplement typable. Ces considérations nous permettront de voir les dérivations de typage comme des preuves en NJm, décorées par des λ-termes décrivant le squelette de la preuve.

Que signifient alors les propriétés d’auto-réduction et de normalisation forte ? La β-réduction réécrit des λ-termes, donc des squelettes de preuve. Un β-rédex correspond à une preuve de la forme suivante:

et son β-réduit est, par auto-réduction, encore une preuve de F sous les hypothèses Γ. Le processus de β-réduction est donc un processus de transformation de preuves. Par la propriété de normalisation forte, ce processus s’arrête toujours. La β-normalisation est donc un processus de simplification, de mise en forme normale de preuves.

Il a pour effet d’éliminer des détours. Considérons la preuve correspondant au β-rédex ci-dessus. Elle consiste à prouver F en commençant par prouver F sous l’hypothèse supplémentaire F₁ (par la preuve π₁), et à prouver F₁ d’autre part (par la preuve π₂). Réduire le β-rédex consiste à éliminer le détour via le lemme auxiliaire F₁, et à démontrer F directement.

Formellement, un détour est une règle (⇒ I) introduisant le connecteur ⇒ dans la prémisse majeure (celle de gauche, qui contient le connecteur ⇒ éliminé) d’une règle (⇒ E). On obtient ainsi:

Preuve : Soit Γ =_def F₁, …, F_n. Si Γ ⊢ F est prouvable en NJm, alors il existe un terme u tel que x₁ : F₁, …, x_n : F_n ⊢ u : F soit dérivable. La forme normale de u existe par la propriété de normalisation forte, et correspond donc à une preuve sans détour de Γ ⊢ F en NJm.     ♦

Les preuves sans détour, à leur tour, ont leurs squelettes décrits par des λ-termes en forme normale. Ce sont donc des termes de la forme:

où x est la variable de tête et u₁, …, u_n sont eux-mêmes normaux. (Voir le théorème de standardisation en partie I, et la notion d’arbres de Böhm.)

Une preuve sans détour a donc la forme (où les variables du contexte sont supposées être x_m+1, …, x_p, d’autre part x est x_i pour un certain i, 1≤ i≤ p, et F_i est de la forme F_i1 ⇒ … ⇒ F_im ⇒ F):

En éliminant les λ-termes de la preuve, on a donc effectué une étape de preuve de la forme:

où Δ est F₁, …, F_p et contient F_i =_def F_i1 ⇒ … ⇒ F_im ⇒ F, suivie éventuellement d’une de la forme:

où m≥ 1.

Si la dernière n’est qu’une généralisation de la règle d’introduction de l’implication (à droite de ⊢), la première est plus intéressante et agit en partie à gauche du signe ⊢: pour démontrer F sachant qu’une hypothèse prouve F_i1 ⇒ … ⇒ F_im ⇒ F, il suffit de prouver F_i1, …, F_im. Il s’agit d’une forme de chaînage arrière (backchaining; ceci généralise naturellement le mécanisme d’exécution de Prolog, cf. [MNPS91]).

Preuve : Soit F n’importe quel type de base. S’il existe une preuve ⊢ u : F, alors on peut supposer que u est normal. Alors la dernière règle était soit (BC) soit (⇒⁺ I). Mais (BC) ne s’applique pas, puisqu’on n’a pas d’hypothèse à gauche de ⊢, et (⇒⁺ I) ne s’applique pas, parce que F est un type de base.     ♦

Ce résultat pouvait être démontré de façon beaucoup plus simple:

D’autres conséquences de la technique d’élimination des détours sont moins évidents, comme nous allons le voir. On obtient le système NJf pour le fragment implicatif de la logique intuitionniste en ajoutant au langage des types une constante ⊥ dénotant le faux (en tant que valeur de vérité), et en ajoutant la règle:

D’un point de vue logique, (⊥ E) exprime que du faux on peut tout déduire. Il n’y a pas de règle d’introduction du faux, car il est dans notre intention que ⊥ ne soit pas prouvable. D’un point de vue calculatoire, on ajoute la construction ∇ u à la grammaire du λ-calcul. Intuitivement, si u : ⊥, alors l’évaluation de u ne termine pas, et on peut donc convertir le résultat inexistant de l’évaluation de u à n’importe quel type, en ∇ u : F.

Cette construction n’introduit pas de nouveau détour (introduction d’un connecteur en prémisse majeure suivie de son élimination), mais elle permet à certaines autres simplifications de se produire:

Ceci est appelé une conversion commutative, et mène à la règle de calcul ∇ u v → ∇ u. (Nous avons déjà vu quelques conversions commutatives à l’exercice 10.) Appelons le calcul combinant (β) et la conversion commutative ci-dessus le λ∇-calcul.

Preuve : Même preuve que pour le théorème 1, en considérant que ⊥ est un type de base; les seules différences sont dans la définition des termes neutres — que l’on définira maintenant comme les termes qui ne commencent pas par un λ ou un ∇ —, et qu’il faut vérifier que si u ∈ RED_⊥, alors ∇ u ∈ RED_F pour tout type F. C’est par récurrence structurelle sur F. Comme u ∈ RED_⊥, u∈ SN. Si F est un type de base, alors ∇ u ne peut se réécrire qu’à l’intérieur de u, et est donc dans SN, donc dans RED_⊥. Si F est de la forme F₁ ⇒ F₂, alors par hypothèse de récurrence ∇ u ∈ RED_F2 (*). On montre par récurrence sur ν (u) + ν (v) que pour tout v ∈ RED_F1, ∇ u v est dans RED_F2. C’est par (CR3), en regardant où se déroule la première réduction: si elle s’effectue dans u ou dans v, on utilise l’hypothèse de récurrence, et si c’est ∇ u v → ∇ u, alors c’est par (*). Donc ∇ u v ∈ RED_F2, et v étant quelconque, ∇ u ∈ RED_F.     ♦

Preuve : Comme pour le corollaire 2, les formes normales u, où ⊢ u : b est dérivable, sont nécessairement de la forme h u₁ … u_n, où h est une variable ou le symbole ∇ (auquel cas n=1). Le seul ingrédient nouveau est que nous effectuons une récurrence structurelle sur u. Si u est tel que ⊢ u : b est dérivable, pour b un type de base, alors h ne peut pas être une variable car le côté gauche du jugement est vide. Donc h est ∇ et n=1. Mais alors on a une dérivation plus petite de ⊢ u₁ : ⊥, ce qui est impossible par hypothèse de récurrence.     ♦

On a démontré en particulier que le faux ⊥ n’était pas prouvable. Mais on peut dire mieux. Notons ¬ F pour F ⇒ ⊥: il s’agit de la négation de F, représentée par le fait que ¬ F est vraie exactement lorsque F implique une contradiction ⊥. En logique classique, ¬ ¬ F et F sont équivalentes, mais pas en NJf:

Preuve : Prenons F un type de base b différent de ⊥. Soit u un terme normal clos de type ¬ ¬ b ⇒ b. Par typage et comme u est clos, u est nécessairement de la forme λ x · u₁, où x : ¬ ¬ b ⊢ u₁ : b. Le symbole de tête de u₁ ne peut être que x ou ∇. Si c’est x, u₁ est de la forme x ou x u₂; mais aucun des deux cas n’est possible, le premier impliquant ¬ ¬ b = b, et le second impliquant ⊥ = b. Donc u₁ = ∇ u₂, avec x : ¬ ¬ b ⊢ u₂ : ⊥. Par des arguments sémantiques comme dans l’exercice 11, on peut conclure directement qu’une telle preuve du faux à partir de ¬¬ b n’existe pas.

Mais montrons comment des arguments syntaxiques mènent à la même conclusion. Nous allons montrer qu’il n’y a pas de terme normal v tel que Γ ⊢ v : ⊥, pour aucun Γ ne contenant que des liaisons de la forme x:¬¬ b ou y:b. Supposons le contraire, et choisissons v de taille minimale. Alors v ne peut que s’écrire x w pour une variable x de type ¬¬ b dans Γ et un terme w tel que Γ ⊢ w : ¬ b, ou ∇ v′ avec Γ ⊢ v′ : ⊥. Mais le deuxième cas contredirait la minimalité de la taille de v, donc seul le premier cas est possible. Si le terme w ne commence pas par λ, alors il s’écrit xw′ pour un x : ¬¬ b ou bien y pour un y : b dans Γ, mais ceci donnerait à w le type ⊥ ou le type b, ce qui est impossible. Donc w est de la forme λ z · v′, avec Γ, z′:b ⊢ v′ : ⊥. Mais ceci contredit l’hypothèse de minimalité de la taille de v, encore une fois.     ♦

On voit donc que la logique NJf n’est pas la logique classique, puisque ¬ ¬ F ⇒ F est vraie que F soit vraie ou fausse. Il s’agit d’une logique intuitionniste, dont les principes remontent au mathématicien hollandais Luitzen Egbertus Jan Brouwer au début du vingtième siècle. La logique intuitionniste est constructive au sens où une formule est vue comme l’ensemble de ses preuves, ⊥ est l’ensemble vide et F ⇒ G est l’ensemble des algorithmes prenant en entrée une preuve de F et retournant une preuve de G. Elle joue un grand rôle en informatique théorique.

Exercice 14 ()   On peut aussi donner une sémantique plus fine de la logique. Soit ( W, ≤) un ensemble ordonné quelconque dit de mondes, et ρ un environnement envoyant chaque type de base b vers un ensemble de mondes ρ (b) tel que si w∈ ρ (b) et w≤ w′, alors w′∈ ρ (b). On définit la relation w, ρ ⊨ F, où w ∈ W, par:

• w, ρ ⊨ b si et seulement si w ∈ ρ (b) (autrement dit, ρ (b) est l’ensemble des mondes où b est vrai);
• w, ρ ⊨ ⊥ est toujours faux;
• w, ρ ⊨ F ⇒ G si et seulement si pour tout w′ ≥ w, si w′ ⊨ F alors w′ ⊨ G.

Montrer que si ⊢ u:F est dérivable, alors w, ρ ⊨ F pour tout w ∈ W, pour tout ρ comme ci-dessus, pour tout ( W, ≤). Montrer qu’il existe ( W, ≤), ρ et w∈ W tels que w, ρ ⊨ ¬ ¬ b ⇒ b ne soit pas vrai. En déduire une autre preuve du lemme 9. (La sémantique ci-dessus est la sémantique de Kripke de la logique intuitionniste; elle est complète au sens où si w, ρ ⊨ F pour tout w ∈ W, pour tout ρ comme ci-dessus, pour tout ( W, ≤), alors F est prouvable en NJf.)

On peut encore enrichir la logique et obtenir le système NJi de logique intuitionniste en ajoutant au langage des types des constructions F₁ ∧ F₂ (conjonction) et F₁ ∨ F₂. Nous le mentionnons ici, mais repartirons de NJm dans les sections suivantes, car NJm contient déjà l’essentiel. Nous ajoutons les règles:

Les règles (∧ E₁) et (∧ E₂) permettent de déduire F₁, respectivement F₂ à partir de F₁ ∧ F₂; de même, (∨ E₁) et (∨ E₂) permettent de déduire F₁ ∨ F₂ à partir de F₁ ou de F₂. La règle (∧ I) permet de prouver F₁ ∧ F₂ en prouvant F₁ et F₂ séparément, et la règle (∨ E) permet le raisonnement par cas: si F₁ ∨ F₂ est vrai, et que l’on sait prouver F en supposant soit F₁ (cas 1) soit F₂ (cas 2), alors c’est que F est vraie dans tous les cas.

À ces règles de preuves correspondent les constructions indiquées venant enrichir le λ-calcul. Les termes sont maintenant définis par la grammaire:

La sémantique intuitive des nouvelles constructions est la suivante: ⟨ u, v ⟩ est le couple formé de u et de v, π₁ récupère la première composante et π₂ la seconde; la conjonction F₁ ∧ F₂ est donc un produit cartésien de F₁ et F₂. La disjonction F₁ ∨ F₂ peut-être vue comme une somme disjointe de F₁ et de F₂: ι₁ u est une conversion permettant de voir u ∈ F₁ comme un élément de F₁ ∨ F₂, et similairement pour ι₂ et F₂; réciproquement, tout u dans F₁ ∨ F₂ est soit de la forme ι₁ t₁, t₁ dans F₁, soit de la forme ι₂ t₂, t₂ dans F₂, alors case u {

} retourne la valeur de v₁ [x₁:=t₁] dans le premier cas, et celle de v₂ [x₂:=t₂] dans le second.

Outre la règle (β), l’élimination des détours demande à faire les transformations suivantes sur les preuves:

ce qui se traduit dans notre λ-calcul enrichi par les règles π₁ ⟨ u₁, u₂ ⟩ → u₁ et π₂ ⟨ u₁, u₂ ⟩ → u₂, et:

où la dérivation de droite est obtenue comme dans le cas (β) du lemme 1. Ceci mène à la règle:

On a aussi des conversions commutatives, dont la liste complète est: