Généralité absolue et généricité dans les modèles de la calculabilité

Ce texte est un travail rendu à Brice Halimi (Université Paris-Cité) en mai 2024, dans le cadre du cours de philosophie des mathématiques.

Résumé

Ici nous voulons montrer que la généricité et la généralité absolue sont naturellement distinctes dans les modèles de la calculabilité, et en particulier dans le $\lambda$-calcul. Nous faisons dialoguer deux désirs antagonistes : celui d’un formalisme intégral, permettant de parler de toute chose, et celui d’un modèle de calcul associé qui “termine” toujours. Nous remarquons que la logique ne recouvre pas tout le domaine du calculable (à cause des points-fixes), et que la logique (la nécessité) permet de garantir la bonne terminaison des calculs.

1. Le calculable comme général

1.1 Calculemus : la réduction leibnizienne des problèmes

“Pour résoudre une question ou terminer une controverse, les adversaires n’auront qu’à prendre la plume, en s’adjoignant au besoin un ami comme arbitre, et à dire : « Calculons! ».”
— Couturat expliquant Leibniz

Dans notre analyse des modèles de calcul nous voulons partir du rêve leibnizien du calculus ratiocinator pour explorer les différents modes que l’on peut attribuer au calcul. Pour ce faire, nous nous appuyons sur les concepts de généricité et de généralité absolue. La généralité absolue est le fait de parler de toutes choses en général en visant tous les objets (la science des choses en générale est appelée métaphysique), tandis que la généricité est le fait de viser un objet quelconque en général.

Nous pouvons ici mobiliser le Principe Ensembliste de Généricité :

Etant donné un ensemble, la référence à un membre quelconque de cet ensemble est garantie.

Cela, nous pouvons avantageusement le transposer dans le monde des types, dans lesquels vivent des variables, et c’est que nous ferons en étudiant le $\lambda$-calcul typé. Dans ce monde, nous pouvons faire référence à un membre quelconque d’un type habité.

Nous explorerons d’abord succinctement les problèmes qui se sont présentés aux logiciens et mathématiciens qui voulaient mettre en place un calculus ratiocinator sur une langue universelle, puis nous explorerons la question des objets dégénérés de la généralité absolue, et enfin nous verrons que la logique, c’est-à-dire la nécessité est la garante d’un bon calcul, un calcul qui termine.

1.2 Hilbert, Ackermann et l’entscheidungsproblem

Les mathématiciens du début de XXe siècle ont essayé de trouver des méthodes de calcul et de prouver que l’Entscheidungsproblem¹ était décidable, c’est-à-dire que toute proposition bien formulée dans le langage d’une théorie axiomatique suffisamment puissante (celle de Peano, voire celle des Principia Mathematica), était décidable.

Pour ce faire, les mathématiciens se sont peu à peu dotés d’une définition de la calculabilité, à commence par les fonctions récursives, que l’on peut faire remonter à Dedekind, mais dont le formalisme est surtout associé à Skolem, Ackermann, puis Gödel.

Les fonctions primitives récursives sont des fonctions totales, au sens où leur calcul termine pour n’importe quelle valeur. Le contre-exemple de la fonction d’Ackermann montre cependant qu’il y a une fonction non-primitive récursive, mais qui est cependant totalement récursive, montrant ainsi que le calculable s’étendait plus que cela.

La citation de l’épigraphe montre qu’en son temps déjà, Leibniz formulait le vœu d’une syntaxe qui puisse exprimer toute chose (que le problème soit mathématique, scientifique ou métaphysique), et d’une procédure de calcul permettant de réduire ces problèmes. Ce désir nécessitait deux choses : — Une Characteristica universalis, syntaxe pouvant exprimer toute chose (également vue comme langue internationale), que l’on doit donc associer à la généralité absolue; — Un Calculus ratiocinator, ou procédure de calcul permettant de réduire tous les problèmes formulés dans la Characteristica universalis.

Le rêve leibnizien fut partagé par de nombreux philosophes au début du XXe siècle, y compris par Bertrand Russell et Louis Couturat qui étaient tous deux de grands lecteurs de Leibniz pour avoir publié sur lui.

Déjà en son temps, Leibniz considérait le raisonnement comme diagrammatique, même si ses ébauches de syntaxe doivent être vus comme une curiosité historique. Nous verrons dans les prochaines parties que les logiciens du début du XXe siècle se sont lancés à corps perdu dans cette quête leibnizienne d’une langue universelle et d’un calcul confluant et fortement normalisant, mais que le modèle diagrammatique du calcul est idée qui fera date chez de nombreux logiciens et informaticiens. Kluge (1980) soutient que le Begriffschrift de Frege était inspiré par ce problème leibnizien.

1.3 Fin du jeu : les théorèmes de Gödel

Le premier théorème de Gödel marque comme on le sait la fin de l’espérance d’un calcul sur une syntaxe absolument générale, une characteristica universalis qui termine toujours. Certains problèmes sont, nous le savons, indécidables, si bien qu’il est voué à l’échec de construire un calcul fondé sur une langue universelle qui a réponse à toute chose en général, du moins dans le domaine des mathématiques².

Le second théorème de Gödel montre qu’en particulier, l’énoncé qui prouve la cohérence d’un système formalisant a minima l’arithmétique est lui aussi indécidable.

2. Exploration : la généralité absolue comme lieu des antinomies

2.1 Le paradoxe de Russell : punition de la généralité absolue ?

Épisode bien connu de la crise des fondements des mathématiques, le paradoxe de Russell fait s’effondrer la structure trop générale, trop logiciste de la théorie naïve des ensembles, qui fut développée (entre autres) par Gottlob Frege dans Grundgesetze der Arithmetik à la fin du XIXe siècle. Le paradoxe est dévastateur : il consiste à utiliser toute la généralité de la syntaxe de Frege (rêve fou mais impossible de faire tenir les mathématiques dans une syntaxe, dont les entités sont ce que l’on peut y écrire) pour écrire un ensemble dégénéré (dit ensemble de Russell) : ${x \mid \neg x \in x}$.

La solution adoptée par les logiciens et mathématiciens est toujours d’introduire une hiérarchie entre les entités considérées (ce que fait Russell avec la théorie des types ramifiés dans les Principia Mathematica), une hiérarchie entre les ensembles et les classes dans ZF, en ajoutant un axiome de fondation qui interdit à un ensemble d’appartenir à lui-même, et en ne considérant de facto comme seule entité mathématique les ensembles, et non les classes (même si c’est discutable, plusieurs objets importants étant des classes, je pense à la classe des ordinaux par exemple).

Un autre parti pris fut (pour les logiciens-philosophes) d’inventer un formalisme beaucoup moins expressif, qui n’est pas soumis au paradoxe de Russell, mais qui ne permet pas d’exprimer grand-chose : la méréologie. Ce dernier formalisme ne fait pas de hiérarchie entre des types d’objets, ni entre les individus et les prédicats, mais n’est pas adéquat pour fonder les mathématiques (sauf dans une perspective hyper-finitiste, dans laquelle on considère que les mathématiques s’arrêtent à un certain entier, disons trois milliards). C’est pour cette raison que la méréologie est régulièrement prise pour ontologie par les philosophes analytiques (Lewis notamment), à cause de sa réputation de neutralité et simplicité³ quant aux entités postulées, ce qui est conforme au rasoir d’Occam.

En somme, le paradoxe de Russell est un point fixe⁴ qui advient dans les systèmes généraux, c’est-à-dire les systèmes qui veulent beaucoup dire sans se brider par une hiérarchie des entités. L’analogie entre la théorie naïve des ensembles et le $\lambda$-calcul pur est d’ailleurs frappante :

Soit $M$ un terme involutif (tel que $MMx = x$).

Il faut prendre “$\in$” pour l’application de deux $\lambda$-termes et “$\neg$” pour le terme involutif $M$. On reconnaît ici le $\lambda$-terme $\Omega$ qui ne se normalise jamais. C’est un exemple frappant qui dégénère à cause de sa trop grande généralité, et de son manque de nécessité, ce qui accrédite la thèse selon laquelle le nécessaire ne sature pas l’universel (contraire de la thèse de corrélation).

2.2 $\lambda$-calcul

Le $\lambda$-calcul est un formalisme inventé par Alonzo Church à la suite des Principia Mathematica de Russell et Whitehead, dans lesquels l’abstraction de $x$ était notée “$\hat{x}$”, ce que Church notait “$\hat{\cdot}x$” puis naturellement “$\lambda x$”, en toute généralité.

Comme nous l’avons vu, le $\lambda$-calcul, qui abstrait toute chose, est le lieu de la généralité, ce qui se traduit concrètement par l’existence de $\lambda$-termes paradoxaux, qui ne se réduisent jamais sous forme normale.

Tout comme les fonctions partielles récursives, le $\lambda$-calcul possède mutatis mutandis son équivalent générique, qui garantit sa terminaison. Ce qui est intéressant ici, c’est que concernant le $\lambda$-calcul, c’est directement la logique (le nécessaire) qui est utilisée pour éviter les boucles!

Ce $\lambda$-calcul générique est typé, c’est-à-dire empêché de boucler à l’infini par une sorte de surmoi logique. Ici, nous nous intéressons au $\lambda$-calcul simplement typé pour des raisons de concision.

Le système de types repose sur un unique jugement de typage, noté $\Gamma \vdash M : \tau$ (dans le contexte $\Gamma$, le terme $M$ a pour type $\tau$). Ce jugement se dérive à partir des trois règles suivantes :

Ces règles sont en fait des règles de construction de $\lambda$-termes. Elles garantissent la bonne construction et la bonne terminaison des calculs, grâce à la propriété de normalisation forte du $\lambda$-calcul typé. C’est ce formalisme qui va servir de base théorique aux langages de programmation (typés), qui ne peuvent pas se permettre de planter comme dans le cas général, qui renferme en lui des objets complètement dégénérés⁵.

S’intéresser aux règles de construction des $\lambda$-termes, c’est en fait s’intéresser aux conditions de possibilité de la généricité, c’est-à-dire à comment restreindre un système trop général en lui ajoutant des règles logiques (nécessité). Ici, la nécessité est directement la logique, elle-même, car lorsqu’on enlève les $\lambda$-termes, (qualifiés de “décorations” en théorie de la démonstration) on obtient le système logique suivant :

On aura reconnu la logique minimale, que l’on peut étendre à d’autres systèmes logiques via l’ajout de règles.

2.3 Le surmoi du calcul : la logique

Dans le calcul, ce qui empêche la généricité de dégénérer en généralité absolue, c’est donc la nécessité, qui n’est nulle autre que la logique elle-même. Comme nous l’avons vu, c’est frappant dans le $\lambda$-calcul : le $\lambda$-calcul typé s’est doté d’un surmoi logique qui prévient le $\lambda$-inceste⁶.

C’est à cet endroit que nous pouvons remarquer que dans les modèles de calcul également, l’universalité n’est pas saturée par la nécessité, car il existe des endroits (l’universalité générale) dans lesquels la nécessité logique n’est pas présente. Cependant, lorsque nous parlons de $\lambda$-calcul typé, nous parlons bien de généricité et de nécessité, puisque les types sont précisément issus de la logique.

Dans ce contexte, la logique acquiert un nouveau rôle : celui de la garantie mécanique de la terminaison du calcul, montrant que le calcul sans logique est chose risquée, soumise aux paradoxes et au plantage des ordinateurs.

3. La logique comme garante de la généralité du calcul

3.1 L’isomorphisme de Curry-Howard : isomorphisme du général

Nous avons vu que concernant le calcul, la logique était l’introduction du nécessaire dans un système trop général, ce qui avait pour conséquence de rendre le système générique, et donc de garantir la terminaison des calculs.

L’isomorphisme de Curry-Howard désigne le fait (dont nous avons discuté dans la section 2.2) que les $\lambda$-termes sont les “décorations” des formules logiques, et que réciproquement les formules logiques sont les “types” des $\lambda$-termes. Mais nous pouvons étendre plus loin cette correspondance et retrouver quelques concepts jumeaux de part et d’autre de la logique et du calcul :

Ce tableau⁷ permet de remarquer l’étendue conceptuelle de l’isomorphisme de Curry-Howard. Cet isomorphisme est du domaine du générique, il ne permet que de parler de l’universel générique, c’est-à-dire l’universel guidé par la nécessité logique.

3.2 La logique linéaire ou la géométrisation du générique

La logique linéaire, émanant directement de l’isomorphisme de Curry-Howard, a été conçue dès ses origines en 1986 comme un système de typage pour les $\lambda$-termes. Elle se distingue par une approche originale des ressources calculatoires : une fois qu’une ressource est utilisée, elle ne peut plus être réutilisée. Cette caractéristique se manifeste pleinement dans le fragment vraiment linéaire MLL, et permet d’envisager les preuves, et donc les $\lambda$-termes bien construits, comme des graphes, dont les graphes de correction (induits pas les &) sont connexes et acycliques, autrement dit, ayant une structure d’arbre.

L’élimination des coupures dans ce cadre peut être vue comme une transformation de graphes, simplifiée par deux règles fondamentales dans les réseaux de preuve :

Première réduction :

     ax      πm
      \     /
       cut         ⇝      πm

(Axiome-coupure : la coupure avec un axiome se simplifie)

Seconde réduction :

    πm   πn            πo   πp
      \ /              \ /
       ⊗                &
        \              /
         ---- cut ----

               ⇝

      πm              πn
      |               |
     cut             cut
      |               |
      πo              πp

(Tenseur-Par : la coupure entre un tenseur et un par se décompose en deux coupures sur les sous-preuves)

Où $\pi_m, \pi_n, \pi_o$ et $\pi_p$ sont des preuves.

Gardant à l’esprit l’isomorphisme de Curry-Howard, nous pouvons établir un parallèle entre les $\lambda$-termes et les formules logiques, et entre la $\beta$-réduction (le calcul) et l’élimination des coupures. Cette perspective nous autorise également à considérer les “réseaux d’interaction” (étudiés par Yves Lafont) comme des représentations graphiques de la $\beta$-réduction.

Nous obtenons ainsi un modèle géométrique du calcul, observable de manière élégante dans des démonstrations dynamiques telles que celles des Interaction nets (Yves Lafont, 1995). Cette visualisation géométrique du calcul fait le lien avec la plus ancienne branche des mathématiques : la géométrie.

3.3 Le point aveugle de la logique : la convergence statistique, ou comment atteindre notre but avec très grande probabilité

Mais il ne faudrait pas pour autant enterrer à jamais le projet leibnizien. Même si dans le monde de la certitude, le désir de concilier un système générique, pouvant parler de toute chose, avec un modèle de calcul terminant toujours est démontré vain (problème de l’arrêt, indécidabilité de l’Entscheidungsproblem, terme $\Omega$), il subsiste un monde dans lequel tout semble possible : celui des statistiques.

L’universalité n’est pas saturée par la nécessité comme nous l’avons vu, mais rien n’empêche une machine de décider avec grande probabilité de l’arrêt de n’importe quelle autre machine⁸. Le property testing est une discipline post-logique dans laquelle plutôt que d’étudier si une propriété est vraie ou fausse avec certitude, on étudie si elle l’est avec grande probabilité (une probabilité arbitrairement grande que l’on peut atteindre avec certitude).

Aujourd’hui, la characteristica universalis et le calculus ratiocinator font bien rire les logiciens, mais il se peut que le problème soit aujourd’hui formulé en d’autres termes : existe-t-il une machine qui peut dire avec une probabilité arbitrairement grande si tout énoncé est vrai ou faux ? Il se peut que la characteristica universalis soit des vecteurs de grande dimension, et le calculus ratiocinator un réseau de neurones particulièrement vaste.

Conclusion

Nous avons vu que dans les modèles de calculs que nous avons considérés, les fonctions totales récursives et le $\lambda$-calcul typé pouvaient être associés au concept de généricité, et les fonctions partielles récursives et le $\lambda$-calcul pur au concept de généralité absolue. Nous avons pu exploiter cette distinction avec profit en montrant que l’on obtient la généricité en introduisant la logique, c’est-à-dire la nécessité. Nous avons finalement exploré le nouveau paradigme interactionniste ou géométrique des modèles de calculs génériques, introduits par la logique linéaire et les réseaux d’interaction.