Les types

La notion de type est bien connue des informaticiens, enfin de ceux qui ne se complaisent pas dans les hacks foireux à base de javascript ou de LISP, bref, de toutes les hideuses manières d'encoder n'importe quoi dans n'importe quoi en suppliant dieu que ça marche. Saint Jacques, patron des informaticiens priez pour nous.

Le "type" est au contraire un concept puissant, au coeur des spéculations encore irrésolues des plus hautes mathématiques contemporaines.

https://www.ias.edu/ideas/2013/homotopy-type-theory

C'est Grothendick lui même, juste avant son départ vers l'absolu qui signala la chose: de nouveaux fondements des mathématiques sont en cours de creusement:

https://www.ias.edu/ideas/2014/voevodsky-origins

L'incroyable complexité de ces considérations m'est évidemment hors d'atteinte, mais je remarquerai d'une part que je ne suis pas le seul, et d'autre part que les confessions de Voevodsky me vont droit au coeur: ses démonstrations buggées à mort que seuls de rares vérificateurs peuvent corriger, et que donc, seul des "assistants de preuve" peuvent vérifier font partie d'un monde qui s'avance à grands pas, et qui est celui de l'information pure, devenue vivante dans les ordinateurs receptacles actifs de la vérité et donc du réel (hmmh).

Néanmoins, il convient de réaliser que cette idée de type fait apparaitre d'autres idées parfaitement fascinantes, et dont la beauté extérieure vaut le détour.

D'abord que la structure d'existence des objets les fait surgir du néant et que la manière dont sont définis les types par exemple vaut absolument d'être considéré. Bien au delà des ensembles qu'on me força à apprendre en sixième, ce qui ruina (en fait non, je ne crois pas) mes capacités ultérieures, les types tout commes les catégories, et maintenant les groupoïdes, sont des objets vivants, animaux d'un bestiaire qui fait tenir les conceptions modernes de l'intelligible. Même si Voevodsky dit que personne ne peut comprendre ce qu'on en fait (ou presque) je reste persuadé qu'on peut les approcher d'une manière ou d'une autre, de façon à se rincer l'oeil, c'est la seule chose qui importe.

Les "types" (tels que décrit par Martin-Löf, qui est une seule personne malgré l'aspect composite son nom, son prénom est Per, mais il est vrai qu'il a beaucoup travaillé avec son frère Anders) permettent de fonder les mathématiques, soit, mais surtout forment la texture théorique des languages de programmation modernes, Idris, le successeur autoproclamé de Haskell, étant connu pour implementer les types dépendants, invention de Per et augmentant énormément l'expressivité des "vrais" languages, les langages de programmation...

Il faut mentionner que le language fonctionnel Haskell (du prénom de Curry) est (plus ou moins)  l'héritier main stream du système F de Girard, tentative des années 70 pour faire un lambda calcul "typé", le compilateur d'un vrai language étant d'abord le calculateur du type des expressions tapées, tâche fondamentale et amicale qui en fait le meilleur ami de l'homme. Je ne plaisante pas: qui ne sait pas ce qu'il doit au merveilleux robot capable de deviner pareille chose de façon exacte n'est qu'un disciple de saint Jacques, un malheureux.

Bien sur il faut mentionner les langages de la lignée de ML, qui firent les assistants de preuve LCF, HOL, Isabelle et aussi Coq. Au fait, les théorèmes ne sont bien sur pas démontrés dans le langage de programmation, bien sur: c'est le modèle de preuve qui est programmé (hacké avec fureur et immense difficulté) dans le langage en question, à qui on demande simplement d'être le plus agréable possible à manipuler, et donc d'avoir un système de types le plus puissant possible, la circularité qui découle de tout ça étant réjouissante.

En parlant de la guerre des Maths, il faut aussi mentionner que Martin-Löf, en voulant généraliser le système F, se fit recadrer par Girard qui démontra son inconsistance. Il se rattrapa par la suite, au demeurant, sa théorie des types a plusieurs versions toutes mieux débuggées que les autres.

En parlant de Curry, il faut mentionner, cela le fut déjà ici le fameux isomorphisme de Curry Howard, parangon de la vraie rencontre entre les maths et l'informatique, mais quel est il exactement ?

La correspondance fonction programme.

Tout d'abord, on commence doucement, il faut réaliser que la notion de fonction est d'abord logique et ensembliste. L'associer à un programme qui calcule à partir d'une entrée x la "valeur" de f(x) demande un effort. Un petit. Mais ce n'est pas cela dont il s'agit...

Ensuite, on passe à plus dur: la mise en correspondance d'une proposition (une sorte de fonction de ses variables libres, mais calculable dans un langage primitif de connecteurs logiques qui n'ont rien à voir) avec l'ensemble de toutes ses preuves... Caractériser une chose par un ensemble indéfini est typique d'une approche particulière de la vie, surtout quand cet ensemble contient des choses aussi "spéciales" que des preuves, voire est défini, précisément, par le fait que ses éléments sont des "preuves".

Surtout que la caractérisation se complète: une implication entre propositions se trouve associée à l'en semble des fonctions entre les deux ensembles de preuves. Nous y sommes. La correspondance des quantificateurs vaut aussi le coup d'oeil, ExAB étant l'exhibition d'un élément a de A et de l'ensemble des preuves de B ayant lié a; AxAB étant le produit de toutes les preuves de B liées à chaque élément de A.

Cette "interprétation", typiquement intuitionniste, est dite celle de BHK (Brouwer, Heyting et aussi Kolmogorov). Elle revient à identifier vérité et preuve et à ne considérer valide que ce qui est prouvable et aussi à identifier calcul sur des ensembles de preuves et calculs de validité de propositions.

 Les fondamentaux

On reprend tout depuis zéro, les mots ont un sens.

Un terme est un objet, peut être composite mais objectif, par exemple x+1. Dans un terme, on trouve des constantes, des variables et des fonctions qui définissent des termes en fonction d'autres termes.

Un prédicat est une relation, ou l'affirmation d'une relation entre termes, par exemple x<y

Une formule ou proposition est un assemblage de prédicats portant sur des termes. Les ou et/ou et permettent d'assembler des formules entre elles. Les formules quantifiées sont des sortes de prédicats sur les formules. Ainsi donc, une proposition est une "affirmation".

A partir de là tout explose, car on a l'affirmation de "vérité" en logique classique et l'affirmation "a une preuve" en logique intuitionniste. C'est toute la différence, la notion de "vérité" étant for discutée, on n'a pas fini de voir comment. Tout d'abord l'identification faite plus haut est rejetée par Per: il y a une distinction fondamentale entre le texte de la proposition et l'assertion qu'elle "implique", le jugement à son sujet.

On trouve partout des articles de Per au sujet des DEUX niveaux de la logique, répétant qu'il y a bien deux domaines de discours, identifiés par  le "|-" des "propositions" et la grande barre horizontale des "assertions" qui les sépare. Le "raisonnement" (on en a parlé précédemment) est bien le calcul des assertions...

http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf

Per considère que son travail philosophique consiste à clarifier ces deux notions, c'est dire que j'avais bien compris qu'il y avait bien un truc là.

Le lambda calcul

Il faut mentionner cette formalisation du calcul, inventée par Alonzo Church: l'idée est d'abstraire les opérations sur des objets par la notion de fonction, capacité d'application à un argument d'une procédure operatoire. xF, avec F contenant des réferences à x (on note lambda ""). L'application de xF à une valeur a, notée F[x/a] est le calcul élementaire, dit "béta reduction".

Pour faire vite, on démontre que le lambda calcul (l'ensemble des "lambda termes" et de leur combinaisons et application) est confluent (de la garonne), c'est à dire que les bétas se réduisent finalement en une forme dite "normale" unique. C'est le théorème de Church Rosser, qui s'applique à ce système là de réécriture. 

C'est pour cela qu'on peut "raisonner" sur des programmes écrits avec des lambdas: on applique et on réduit "à la main" (ou à l'oeil), et on est sur que l'ordi fera pareil. 

Au passage, alpha désigne l'équivalence entre deux termes qui ne diffèrent que par le nom de leur variables liées:

x.x est alpha équivalent à y.y  

Au passage, le caractère lambda ressemble à une flèche dirigée vers la droite, vous ne trouvez pas? 

Les points fixes

On ne peut pas ne pas pouvoir (ad infinitum) citer la notion de "point fixe", l'opérateur "fix" qui s'applique aux fonctions leur calculant leur point fixe (ou du moins l'un d'entre eux), soit la valeur qu'elle ne transforme pas.  

Une implémentation de "fix" est le célèbre combinateur Y (la société de venture capital "Y combinator" a choisi ce nom pour cela). Un combinateur est une expression sans variable libres et on a : 

Y = f. <corps d'une lambda sur la fonction f >

    x.f(x x)   $   x.f(x x ) 

Pour lire ça, on notera que "x x " désigne l'application de la fonction x sur x, et que "$" met entre parenthèses ce qui suit.

Si on réduit béta-ément Y f, on trouve:

Y f =  x.f(x x)   $   x.f(x x )  = f(x x)  [x = x.f(x x ) ] = f ( Y f) 

Ce qui prouve ce qu'on veut, c'est à dire que Y f est bien un point fixe de f, mais ne le donne pas pour autant...

Par contre, Y est super utile.

Parcequ'il permet de béta réduire une définition de fonction récursive, interdite par le lambda calcul:

"f=x.x==0?1:f(x-1)" (= "f=<B(f)>") est interdit: f comme variable libre, ne peut référer la fonction courante... 

Soit F = f.<B(f)>

F est une expression valide, et pour calculer une valeur de notre fonction qu'on voudrait récursive au point p=2,  on va réduire (Y F) 2: 

(Y F) 2 = (F ( Y F)) 2 =( <B(f)> [f=YF]  ) 2  = x==0?1:( F Y) (x-1) [ x = 2 ]  =  (F Y) (1)  

On a donc l'opérateur de point fixe, pure magie, qui rend récursif ce qui ne peut pas l'être... 

Les types

C'est le moment de passer aux types. Le lambda calcul est en effet typé et il s'agit de définir une notion de typage pour ce calcul là qui permette et c'est là l'immense apport de Per, de servir de fondements à la totalité des mathématiques, rien que ça. Les types deviennent l'équivalent des ensembles pour tout, absolument tout, formaliser.

Cette mise en concurrences des ensembles et des types pour les fondements est tout sauf évidente, et repose sur toute une série de conventions dérivées de la considération du fameux isomorphisme. Il faut donc préciser que les formules des démonstrations mathématiques sont représentés par les spécifications de certains types spéciaux, les types "propositionnels", les lambdas termes typés par eux étant les programmes à écrire pour prouver les formules.

Le calcul des types résultants de ces programmes EST le système de preuve, décidable, je dirais bien sur, tout est fait pour cela.

La spécfication et la programmation

 Mais le programmeur que je suis ne peut que se réjouir de voir des langages spécialement définis pour pouvoir exprimer simultanément dans le même formalisme spécification et programme, l'objectif (un object académique au plein sens du mot) étant bien sur de dériver le programme de sa spec, afin, bien sur, de se faciliter la vie.

Car la correspondance est un exemple du célèbre pattern de la projection avantageuse depuis un monde hostile vers un monde où tout est facile. Le meilleur ami de l'homme, le calculateur des types super facile à faire (du moins pour certains) se trouve l'image de l'horreur infaisable qui consiste à démontrer des théorèmes. C'est précisément cette facilité algorithmique qui rendit brutalement envisageable de prouver des théorèmes, et donc de programmer des assistants de preuve. Merci Curry, merci Howard, merci Per.

Par contre, pour représenter toutes les maths (les assistants de preuve, on l'a vu, ont vocation à TOUT décrire et tout prouver, notamment l'absolument imb(f)aisable), il faut un typage "assez" (au sens de suffisamment) élaboré. Les types (dépendants) de Marin Löf (A theory of types, 1971 étant le fameux texte que Girard déclara incohérent) le permettent et forment donc la base de toute l'avancée scientifique (absolument gigantesque) en question.

Le fantasme suprême

Il s'agit bien donc d'exprimer le fantasme du "calculus ratiocinator" (Leibniz, 1666), le langage total qui permettrait de tout exprimer, et donc de tout décider... Ce langage est programmatique, bien sur et il a des effets de bords !!!