La vie est mal configurée

Aller au contenu | Aller au menu | Aller à la recherche

mardi, mars 6 2012

Types construits dans le système F

Il arrive parfois que l'on se pose une question, qu'on ne trouve pas la réponse sur le moment, puis que cette question se rappelle à notre souvenir longtemps après.

Quand j'étais en DEA en 1998, et que j'apprenais l'encodage des types de données inductifs dans le système F (ou dans le Calcul des Constructions, même problème), je m'étais demandé si ces types pouvaient être « trop gros », c'est-à-dire contenir des termes qui ne seraient pas obtenus par application des constructeurs de ce type.

Rappelons de quoi il s'agit. On connaît bien l'encodage de Church des entiers naturels dans le λ-calcul pur : l'entier n est encodé comme une fonction qui à f associe la composée n fois de f avec elle même, soit λfλz f ( f ( … z) ). Dans le système F, on obtient ΛX λ(f: X→X) λ(x: X) f ( f ( … z) ). De même, le type des booléens peut se coder avec ΛX λ(a: X) λ(b: X) a pour « vrai » et ΛX λ(a: X) λ(b: X) b pour « faux » ; et le type Caml A of int | B of string se coderait comme le type ∀X (int→X)→(string→X)→X, avec le terme (A toto) codé par ΛX λ(a: int→X) λ(b: string→X) (a toto) et le type (B tata) codé par ΛX λ(a: int→X) λ(b: string→X) (b tata).

Selon ce même principe, le type Caml à un constructeur A of foo, trivialement isomorphe au type foo, s'encode comme ∀X (foo→X)→X, le terme (A x) s'encodant comme ΛX λ(f: foo→X) (f x). Permettez-moi maintenant une analogie (qui d'ailleurs peut sans doute se formaliser en théorie des catégorie) avec un autre domaine, l'analyse linéaire : si E est un espace vectoriel sur le corps K, et A→B désigne l'espace des applications linéaires de A dans B, alors (E→K)→K est le bidual de E, et pour tout élément x de E, λ(f: E→K) (f x) est l'élément associé par l'injection canonique de E dans son bidual. E et son bidual sont isomorphes quand E est de dimension finie, mais le bidual de E est « plus grand » que l'image de l'injection canonique de E quand E est de dimension infinie. Transposons notre doute aux types inductifs codés dans le système F : n'est-il pas à craindre que le type soit « plus gros » que l'ensemble des termes effectivement constructibles (les constructeurs étant les analogues de l'injection canonique, ce qui se comprend d'ailleurs bien dans l'interprétation catégorielle des types sommes) ?

La même question m'est revenue longtemps après, alors que je préparais un cours sur la théorie des types pour l'enseignement d'approfondissement dont je suis responsable à l'X. Ma distinguée collègue Christine Paulin a eu l'excellente idée de mettre sa remarquable thèse (de 1989 !) en ligne sur l'archive « thèses en ligne » et la réponse est au §4.3.1, p. 112 : en utilisant des types très polymorphes, il est possible de construire dans un type de la forme ∀X (N→X)→X des termes qui ne sont pas de la forme ΛX λ(f: N→X) (f n) où n est un terme clos de type N ; l'idée est que le terme n peut utiliser l'argument X dans des quantifications imprédicatives un peu compliquées.

Et là m'est arrivé une autre question, à laquelle je n'ai pas de réponse et pour laquelle je ne vois pas non plus de réponse dans la thèse de Christine Paulin...

Les constructions évoquées plus haut sont certes des termes non construits, mais je conjecture, d'une certaine façon, ils sont équivalents à des termes construits : sauf erreur de ma part, pour tout terme a du type en question, il existe un terme construit a' tel que pour tout h tel que (h a) soit d'un type construit « simple » (disons, les booléens), alors (h a)=(h a'). Autrement dit, tant qu'on ne fait pas des choses trop bizarres, les termes « en plus » ne produisent pas de comportements « inattendus ».

Il est 21 h et j'ai mal à la tête, je laisse mes lecteurs cogiter.:-)

Pour ceux que cela intéresserait, voici l'exemple de Christine Paulin, en notations pour Coq 8.3.

(Si vous voulez retrouver l'exacte définition proposée par Christine Paulin, il vous faut remplacer Type par Set et lancer Coq avec l'option -impredicative-set ; Set était naguère imprédicatif, sans doute pour permettre les codages inductifs par polymorphisme, en plus des types inductifs natifs rajoutés dans le Calcul des constructions inductives par rapport au Calcul des constructions, mais dans les versions actuelles de Coq il ne l'est plus, parce que ça posait un problème de compatibilité avec je ne sais plus quel axiome éventuellement désirable.)

Definition M (A : Type) := forall X : Type, (A->X)->X.

Definition c {A : Type} (a : A) : (M A) := fun X: Type, fun f : A->X, (f a).

Definition T := forall X : Type, X->X.

Definition t : T := fun X : Type => fun x : X => x.

Definition N := (forall D: Type, (D->T))->T.

Definition m : (M N) := fun (C : Type) (f : N -> C) => f (fun y : (forall D : Type, D->T) => y C (f (fun _ : (forall D : Type, D->T) => t))).

mercredi, janvier 18 2012

Incohérence d'une version forte de la logique classique en théorie des types

Herman Geuvers a montré que l'ajout d'un axiome fort de logique classique dans Coq (ça doit aussi marcher avec le Calcul des Constructions non inductives) aboutissait à une incohérence.

Son axiome fort est plus puissant que l'axiome habituel, qui est le tiers exclu (ou, de façon équivalente, l'axiome de Peirce) : en effet, il dit non seulement que pour tout P, P ou non P est vrai, mais qu'il y a un mécanisme qui retourne cette valeur de vérité sous forme d'un booléen au sens ordinaire de Coq (dans Set).

Mon intuition de l'argument de Geuvers, suite à un survol de l'article, est que si on a un lien si fort entre Prop et Set, on peut définir dans Set des fonctions qui dépendent par cas du contenu de termes dans Prop et aboutir à un paradoxe — mais je n'ai peut-être rien compris.

Je me demandais s'il n'y aurait pas une preuve du même fait par la calculabilité. En effet, l'axiome classique fort supposé revient, s je ne m'abuse, à supposer l'existence d'un oracle universel donnant effectivement la vérité ou la fausseté de toute proposition. On doit notamment pouvoir appliquer cela à l'arrêt d'un processus de calcul (p.ex. beta-réduction dans un système de calcul pas trop compliqué, genre lambda-calcul en indices de de Bruijn ou combinateurs SKI) et ainsi aboutir à une contradiction par diagonalisation à la Turing. Suis-je trop naïf ?

lundi, janvier 16 2012

Question technique : prédicats sur types inductifs en Coq

Lorsqu'en Coq, on a une propriété à définir sur un type inductif T, faut-il mieux définir une fonction T->Prop par point fixe, ou définir un prédicat inductif T->Prop? Le premier cas n'est évidemment pas applicable si la décision du cas à appliquer n'est pas (quasi) déterministe en fonction du constructeur de T rencontré à la racine. Le second cas oblige à utiliser des inversions, qui peuvent parfois poser problème.

Sylvain Boulmé me suggère de faire les deux en démontrant une équivalence... D'ailleurs, est-ce que ça marche bien, la réécriture Setoid par l'équivalence logique ? Je l'ai utilisée sur quelques exemples, mais y a-t-il des problèmes cachés ? Est-ce fondamentalement plus complexe ou piège que la réécriture par l'égalité de Leibniz ?

mercredi, novembre 2 2011

Pub gratuite

À lire : le blog de Claire Mathieu, anciennement connue sous le nom de Claire Kenyon.

(Je suis presque toujours plein d'admiration pour les gens qui font de l'algorithmique théorique.)

mercredi, août 3 2011

NEXPTIME-complétude

J'ai un problème d'analyse de programmes qu'il serait trop fastidieux d'expliciter ici ; il s'agit d'une généralisation du problème traité dans mon récent article avec Thomas Gawlitza. Sauf erreur (je n'ai pas mis la preuve au propre) ce problème est dans NEXPTIME. Je soupçonne qu'hélas ce problème est NEXPTIME-complet. Je m'y connais fort peu en NEXPTIME (d'habitude, je ne regarde que des problèmes dans les premiers degrés de la hiérarchie polynomiale, ou PSPACE-complets) ; connaîtriez-vous des lectures à me conseiller ?

page 2 de 2 -