Les logiques : notes en vrac

Une parenthèse (puis une autre plus tard), sur les notions de définition predicative et impredicative.

Je recite juste plus loin, quelque chose que j’ai répondu à quelqu’un ailleurs et je dois resituer le contexte.

Cette personne qui est versée dans la philosophie à laquelle je ne connais presque rien, fait parfois mumuse avec la logique, qui me parle un peu plus, et s’était amusé cette fois, en posant ce classique :

• La phrase suivante est vraie.
• La phrase précédente est fausse.

J’avais bêtement dit que la formulation n’est pas valide parce qu’elle fait référence à elle‑même, quoique j’aurais plutôt dut dire qu’on ne peut rien en dériver de certain.

Il me fait alors remarquer que pourtant en linguistique par exemple, les propositions auto‑référentielles sont fréquentes et ne sont pas vues comme problèmatique.

Avec du retard, je lui ai écrit ceci, qui est est utile à rapporter ici aussi :

Une seconde parenthèse.

Je ne sais plus si ça avait été abordé, si ça l’a été, ce sera juste une répétition utile :

Il ne faut pas confondre ⊤ avec « vrai » et de même, ne pas confondre ⊥ avec « faux ». En particulier, ne surtout pas tenir « non A » comme prouvant une équivalence entre A et ⊥ (il en irait autrement de “ A ∧ not A ”).

Le symbole ⊤ est souvent appelé truth, à distinguer de true. Le symbole ⊥ est souvent appelé falsity, à distinguer de false.

En marge, un second rappel résumé, de chose déjà dites, sur false et true : ce ne sont pas des réductions de propositions, mais des propriétés de propositions, comme expliqué quand a été abordé la distinction entre la logique et l’algèbre Booléen. C’est à dire que “ A true ” peut se lire lire comme “ A is true ” mais pas comme “ A = true ” ni comme “ A is the true ”. Un exemple du monde moins abstrait peut faire comprendre la différence : une souris peut être discrète, mais elle n’est pas égale à discrète dans le sens où elle n’est pas la discrétion, n’est pas en elle‑même la notion abstraite de discrétion. Quand on dit qu’elle est discrète, c’est une caractéristique qu’elle a, ce n’est pas ce à quoi elle se réduit, puisqu’elle est une souris, « seulement » égale à elle‑même. De même “ A true ” qui peut se lire “ A is true ”, signifie que A a la propriété d’être true, mais n’est pas réductible à ça. Même remarque pour “ A false ”.

⊤ et ⊥, ne sont justement pas des propriétés de propositions, ⊤ et ⊥ sont des propositions. Elles sont des propositions spéciales dans le sens où elles ne sont généralement pas posées (ou je ne connais pas de cas où ce soit pertinent) comme propositions mais peuvent être produites comme propositions dérivées après applications de règles d’inférence.

Dans les logiques où de ⊥ on peut tout conclure (pas dans toutes), on ne peut pas tout conclure de A dans un contexte où on a “ non A ” en confondant false et ⊥, ne serait‑ce que A est peut être elle‑même une négation, comme dans “ non (non B) ” (A = non B), tandis qu’il est sûr que ⊥ n’est rien d’autre que ⊥, elle n’est pas décomposable.

De la même manière, dans une couverture de cas A1, A2, A3, …, si l’un des cas An est ⊤, on doit faire sans, parce qu’il ne signifie rien d’autre que lui‑même, la proposition ⊤ pouvant être dérivée de n’importe quoi dans certaines logiques (peut‑être même dans toutes ?), mais rien ne pouvant en être dérivé (il faut alors que le contexte fournisse d’autres éléments).

On peut remarquer que dans beaucoup de logiques, ⊤ et ⊥ vont en sens inverse l’une de l’autre : on peut souvent dériver ⊤ de n’importe quoi mais on ne peut rien en dériver, tandis qu’on peut dériver n’importe de ⊥ mais on ne doit normalement pas pouvoir le dériver, parce que sinon ça signifie qu’on a peut‑être un problème (ça dépend des points de vu), si par exemple on est dans une logique où ⊥ se dérive de “ A ∧ not A ”.

Ici, en lisant « souvent » ou « moins souvent », il faut comprendre ce qui est permis dans les systèmes de déduction, qui ne se ressemblent pas tous sur ce point. Au passage, le mot « logique » doit souvent en réalité être lu comme « système de déduction », mais ça ne pose pas trop de problème de les confondre, temps qu’on ne confond pas deux niveaux de langage.

Certaines logiques n’incluent pas ⊥ ou encore certaines ne permettent pas d’en dériver n’importe quoi, c’est le cas des paraconsistent logics, dont il sera brièvement question plus tard.

Les logiques linéaires sont peut‑être ou pas des cas à part, je ne saurais pas en parler.

Il ne faut pas, en lisant trop vite, croire comprendre qu’ayant obtenu la démonstration de cette proposition “ A ∧ not A ”, on peut conclure n’importe quoi en général, parce que ça signifierait plutôt que la logique est inconsistent et que tout ce qu’on a conclut avec cette logique, est à ne pas retenir. Il faut plutôt lire en oubliant jamais que dans un système de déduction, une conclusion se dérive toujours dans un contexte, n’existe que dans ce contexte et que même dans les logiques qui acceptent à partir de “ A ∧ not A ” de dériver ⊥ puis n’importe quoi, cette proposition “ A ∧ not A ”, peut éventuellement (c’est même préférable) n’être jugée vraie que dans un contexte représentant des conditions, et c’est alors seulement sous ces conditions, dans ce contexte, pas dans les autres, que cette conclusion existe. Si par contre cette conclusion se produit dans un contexte vide, c’est à dire avec aucun séquent plus à gauche et rien comme antécédent du séquent, ce qui au passage peut être le contexte global par défaut, implicitement ou explicitement, alors dans ce cas, qui est le cas général, comme dit plus haut, c’est la logique qui a un problème, parce qu’elle est inconsistent.

La remarque précédente inspire de parler de la distinction entre consistency, soundness et completeness, qui sont des propriétés des logiques et systèmes de déduction.

La première propriété, la cohérence, est toujours requise. Les deux suivantes, la capacité à ne démontrer comme vraie, que les choses vraiment vraies, et la capacité à démontrer comme vraies, toutes les choses vraies, sont généralement mutuellement exclusives. La première et la deuxième ne doivent pas être confondues.

On parle d’inconsistency, quand une logique permet la démonstration en général, d’une proposition et de sa négation. Comme souligné dans le précédent message, c’est à ne pas confondre avec le cas où on conclut à une absurdité dans un contexte en particulier, sous des conditions en particuliers ; c’est plus grave que ça, ça correspond au cas où cette dérivation peut apparaître en général, sans condition particulière, c’est à dire que le contexte général suffit à conclure à une absurdité et par là à l’absurdité de la logique en cause. Cette propriété n’est jamais acceptée. Une logique qui n’est pas inconsistent, est dite consistent.

On parle d’unsoundness quand une logique permet de démontrer comme vraie des choses qui sont fausses en réalité, et malheureusement, il est impossible de savoir quelles propositions sont en causes. Qu’une logique permette de conclure comme vraie en général une chose fausse en réalité, n’est pas à confondre avec le cas où elle jugerait elle‑même à la fois comme vraie et comme fausse, une même chose et en général, ce qui est l’inconsistency. Quand la logique est unsound, elle est en contradiction avec la réalité à laquelle elle a été associée (un modèle), mais pas en contradiction avec elle‑même . Quand une logique n’est pas unsound, elle est dite sound.

On parle d’incompleteness, quand une logique ne permet pas de démontrer comme vrai tout ce qui est pourtant vrai dans la réalité, et malheureusement, on ne sais jamais avec quelles propositions ça se produit. Contrairement à une logique unsound, elle ne démontre jamais comme vraie des choses qui sont fausses en réalité, une propriété appréciable, mais elle ne peut pas faire faire aboutir les démonstrations de tout ce qui est pourtant vrai. Quand une logique n’est pas incomplete, elle est dite complete.

Dans le deuxième et troisième cas, la logique n’est jamais en contradiction avec elle‑même. Dans le deuxième cas, la logique peut être en contradiction avec la réalité. Dans le troisième cas, la logique n’est jamais en contradiction avec la réalité, mais au prix de ne pas pouvoir dire toute la réalité.

Par « réalité », il faut comprendre le modèle de la logique, la logique de quoi elle est censée représenter. Quand il y a dissociation entre la logique et la réalité (à la manière unsound ou à la manière incomplete, les logiques inconsistent étant hors du propos), ça ne signifie pas que la logique de la réalité soit à mettre cause, elle s’applique comme il en a toujours été (à moins d’avoir tenté de formuler la logique d’une réalité qu’on ne comprend pas avec certitude), ça signifie seulement qu’il n’est pas possible de faire des prédictions ou faire des généralisations, à partir de certains cas, quand la logique est incomplete, ou croire qu’on a put le faire alors qu’en fait non et rester dans cette illusion sans le savoir, quand la logique est unsound.

Pour des logiques représentant des réalités triviales, par exemple une chose élémentaire comme l’arithmétique avec seulement l’addition, il existe des logiques pour raisonner sur cette réalité avec toutes les qualités requises : elles ne se contredisent jamais, ne contredisent jamais la réalité et ne cachent rien de la réalité. C’est aussi le cas de la logique des propositions du premier ordre, du calcul des propositions du premier ordre, de l’arithmétique de Presburger (qui n’a pas la multiplication non‑plus), et de la géométrie de Tarski (apparemment des axiomes semblables à la géométrie enseignée au collège), au moins.

Pour des logiques représentant des choses plus compliquées, on doit toujours exiger d’une logique qu’elle ne soit pas auto‑contradictoire, mais on ne peut pas espérer à la fois soundness, c’est à dire qu’elle ne contredisent pas la réalité, et completeness, c’est à dire qu’elle ne cache rien de la réalité. Les seules options, sont un choix exclusif entre l’une ou l’autre de ces deux qualités, mais en étant libre du choix de la logique quand‑même (dans la limite de l’existant ou de ce qu’on sait définir en prouvant que la logique définie n’est pas incohérente).

Dans le monde des mathématiques, le choix le plus populaire mais ne faisant pas pour autant l’unanimité, est d’avoir completeness au prix de ne pas avoir soundness. Dans le monde de l’informatique théorique et quelquefois appliquée, le choix le plus populaire et peu mis en cause, est d’avoir soundness au prix de ne pas avoir completeness.

Si j’ai bien compris, les logiques qui sont à la fois sound et complete, permettent d’énumérer tous les théorèmes valides, et c’est même à ça qu’on les reconnait ; mais ça ne s’observe pas, ça se démontre.

J’espère ne pas avoir dit de bêtises dans les précédents messages, parce que ce serait plus grave qu’avec les autres questions .

Finalement il y a eu plus de deux parenthèses.

Suite et fin de la tentative d’étude sur les séquents (seulement de ça, deux autres messages importants vont suivre plus tard, avant de mettre le sujet en pause) et surtout de leur contexte. Il en aura longuement été question, parce que les contextes, c’est essentiel, je ne pourrais pas mettre assez de traits en dessous pour le souligner assez, alors je ne souligne rien. Les contextes, c’est essentiel et c’est aussi universel, ça se retrouve partout où il est question de logique, qu’ils soient implicites ou explicites.

Comme dit précédemment, il n’y a malheureusement pas de définition suffisamment précise permettant de mécaniser la manipulation des contextes des séquents, une mécanisation souhaitable non‑pas seulement pour réduire la difficulté, mais encore plus pour se prémunir des erreurs, sans quoi je trouve les démonstrations personnelles même sans intérêts (et même des spécialistes font parfois des erreurs, juste qu’ils retombent souvent miraculeusement sur leur pieds en faisant une autre erreur plus tard qui corrige la première). L’utilité de cette mécanisation est largement reconnue.

Le dernier message à propos des séquents, s’était conclut par la remarque que les contextes ne s’imbriquent peut être pas toujours comme longuement et d’abord décrit, la logique linéaire semblant effacer des contextes ou des éléments des contextes, et l’imbrication des contextes et ce qui l’accompagne, la visibilité permanente de ce qui se trouve dans les contextes englobants, serait en contradiction avec la logique linéaire au moins (pour ce que je crois en comprendre) et ne serait donc pas un modèle universel pour la manipulation des séquents.

Je me lamentais que si les séquents de la logique linéaire fonctionnent si différemment des autres, il faudrait au moins les noter différemment. En cherchant s’il existe un symbole autre que ⊢ comme connecteur entre les antécédents et le succédant de ces séquents, j’ai trouvé un document parlant d’utiliser la logique linéaire comme base pour la spécification de la manipulation des séquents dans la variété des logiques. Cette approche me semble crédible, vu l’expressivité de la logique linéaire, mais s’il faut étudier la logique linéaire pour comprendre comment manipuler les séquents, c’est aussi peu engageant que si à l’école primaire il fallait étudier la théorie des groupes avant d’apprendre à poser une addition et une multiplication. Il doit y avoir un autre chemin, pour lequel suffit l’intuition élémentaire qu’on peut avoir en pensant à l’informatique comme domaine d’application de la logique.

Je rapporte quand‑même le lien vers le document mentionné : Linear logic as a logical framework for specifying sequent calculus (polytechnique.fr) [PDF], Dale Miller, Elaine Pimentel, 2002.

Peut‑être que des gens assez doués pourront allez directement à ce document et en tirer quelque chose. J’envisage une autre voie personnellement, celle de tenter de poser une spécification assez générique, avec l’espoir qu’elle pourra répondre à tous les cas aperçus jusque maintenant et ceux qui devront être testés et envisagés à l’avenir (pas un avenir immédiat).

Ce qui suit est ennuyeusement détaillé, vraiment, de plus en mêlant sémantique basique, détails d’une possible implémentation et questionnements, sans les séparer.


D’abord, pour aborder les séquents comme des touts, sans les décomposer, il existe au moins deux cas au fil de l’arbre des inférences : le cas où les séquents forment des contextes imbriqués et le cas où un séquent produit par une règle d’inférence prend la place du contexte précédent et donc transitivement est toujours à lui seul le contexte de l’inférence suivante. Il faut remarquer que les règles d’inférences ne produisent toujours qu’un seul séquent, pour ce que j’en ai constaté, ce qui est heureux, comme ça ne crée pas d’ambiguïté avec le second cas, et si une logique est dans un autre cas, cette logique ne sera pas supportée ou alors des règles seront générées automatiquement comme suggéré quelque part plus loin. Le second cas ne signifie pas qu’il n’est pas nécessaire de garder l’arbre des inférences, il signifie seulement que dans ce cas, on ne remonte jamais en arrière dans l’arbre pour y chercher des éléments de contexte, ce qui ne correspond qu’à une branche conditionnelle dans la méthode d’accès aux contextes.

Une autre idée pour exprimer qu’il n’est pas possible de remonter en arrière dans les contextes, plutôt que de le faire par une spécialisation de types de contexte, serait peut‑être un élément spécial des contextes, un élément qui serait une barrière indiquant de ne pas remonter plus loin en arrière, à la manière du cut de Prolog, qui empêche de remonter en arrière dans l’arbre des tentatives d’unifications ; cette solution serait même plus souple est pourrait avoir une représentation explicite dans l’écriture et l’affichage, ce qui est une qualité appréciable. On pourrait arguer que le cut du Prolog a mauvaise réputation, parce qu’il rend les clauses sensibles à leur ordre de déclaration, mais dans une logique comme la logique linéaire, l’ordre des inférences ne peut que avoir une importance ; l’utilisation de cette barrière par une logique, signifierait que cette logique est sensible à l’ordre de certaines inférences.

Toujours en abordant les séquents comme des touts, leur ordre est toujours important, les séquents ne sont jamais réordonnés par aucune règle d’inférence. Je ne vois même pas comment elles le pourraient, et de plus, les séquents n’ont rien qui permettrait de les désigner, contrairement aux éléments qui les constituent, qui ont des noms. Là aussi, c’est heureux, parce que ça n’entre pas en contradiction avec le premier cas du paragraphe précédent, ça n’aurait pas de sens de réordonner la hiérarchie des contextes imbriquées, pour les logiques qui imbriquent les contextes (les plus nombreuses).

Entrons dans la structure des séquents.

À gauche, c’est une conjonction, à droite, c’est une disjonction, même si la disjonction à droite n’a pas l’air souvent significative, comme je n’y ai toujours vu qu’un seul élément.

La partie gauche et la partie droite, sont susceptibles de contenir des éléments des mêmes types, bien que certains types semblent être l’exclusivité de la partie gauche, il n’est pas insensé d’envisager que la partie droite puisse contenir des éléments des même types. En effet, on trouve à gauche des résultats de cumuls des élaborations du langage objet, et il n’est pas insensé de supposer qu’un langage objet puisse produire les mêmes choses directement en une seule expression. De toutes manières, prévoir que la partie droite soit autant polymorphe que la partie gauche, ça ne coûte rien.

Si les types des éléments des deux côtés sont possiblement les mêmes, il faut envisager à priori que les contraintes sur un des deux côtés, soient applicables à l’autre côté aussi, mais seulement à priori.

Certaines logiques nécessitent qu’il n’y ai qu’un seul succédant à droite du séquent, d’autres nécessitent qu’il y en ai au plus un, sous entendu il peut y en avoir zéro, même si ayant des doutes sur le sens général ou l’utilité de ce cas (A ⊢ B ⊢ C, devrait simplement être A, B ⊢ C, je ne vois pas quelle différence il pourrait y avoir), je suis tenté de considérer qu’il ne doit pas se produire, il ne coûte pas trop de prévoir ce cas. Ou alors prévoir une transformation automatique de ces cas, comme suggéré dans la précédente parenthèse. D’autres logiques en permettent plusieurs ou un, sans que je ne sache si elles en permettent zéro, toujours avec le même doute sur le zéro succédant. Le cas à zéro antécédent se rencontre souvent, mais il peut signifier un contexte de base par défaut. Ça ne semble à priori pas applicable au succédant, mais il arrive que des éléments du succédant soient omis et considérés comme implicites aussi (vu dans la formalisation de la sémantique de SML). Après tout, ce n’est pas plus étrange qu’un contexte par défaut à gauche, même si c’est plus élaboré, comme les éléments par défaut dans le succédant, ne peuvent que parfois changer au fil des dérivations.

Il faudrait prévoir qu’aux nœuds de l’arbre des inférences, puissent être attachés des éléments par défaut, pour les séquents qui sont sous ce nœud. Dans ce cas, un contexte global par défaut, serait simplement des éléments de contexte par défaut, attachés au nœud racine. Prévoir aussi la possibilité d’annuler certains de ces éléments par défaut, par un nœud plus imbriqué.

Certaines de ces attaches pourraient être automatiques, comme celle au nœud racine pour l’environnement par défaut, mais aux autres nœuds, je ne sais pas, je crois qu’il s’agirait plutôt d’omettre l’affichage de certains éléments qui ne changent pas, comme par exemple un élément représentant un état dans l’antécédent, qui serait rapporté inchangé dans le succédant. Dans ce cas, il n’y aurait pas vraiment d’élément à ajouter par défaut, seulement certains à ne pas représenter dans une image textuelle ou graphique de l’état de l’arbre d’inférence. Quoique si c’est implicite à l’affichage, il faut prévoir que ce puisse être implicite à l’écriture aussi. Dans ce cas, les éléments ajouté automatiquement à un séquent proviendrait d’un séquent antérieur et il faudrait prévoir la possibilité de décrire ce qui est rapporté automatiquement même quand ce n’est pas écrit. Un sélecteur dans l’esprit des XPath (mais en bien moins complexe) serait peut‑être une idée

L’ordre des éléments à gauche est parfois significatif, parfois ne l’est pas. Ça s’exprime typiquement par le fait que le système de déduction en question, n’admet pas une ou plusieurs règles structurelles issues d’autres logiques qu’ils contraignent.

Il peut exister des manières d’optimiser tel ou tel cas particulier, mais il faut prévoir pour une généralisation, que la liste à gauche, puisse être une liste à proprement parler, pas être exclusivement représentée par un ensemble par exemple, même si elle peut être un ensemble ordonné ou non‑ordonné, une collection d’ensembles, ou autres combinaison d’ordre et d’ensembles (je l’ai vu ailleurs aussi décrit dans des termes semblables, ce n’est pas que ma conclusion personnelle), dont la représentation la plus générale ne faisant perdre aucun aspect significatif, ne peut que être une liste ordinaire, c’est à dire acceptant les doublons. Si un système de déduction permet l’élimination des doublons et le ré‑ordonnancement parce que pour ce système, la liste est un ensemble, il l’exprime assez sûrement par des règles structurelles de toutes manières et alors la liste ordinaire est bien une solution universelle, même si il est possible de prévoir des spécialisations pour certains cas. Le cas général resterait cependant préférables, pour l’enregistrement d’une démonstration dans un fichier permettant de rejouer la démonstration pour la vérifier.

L’ordre des éléments à droite, il est difficile d’en dire quelque chose, tant il semble n’y en avoir toujours qu’un seul. Ce qui est à droite appartient plus au langage objet que ce qui est à gauche, il pourrait sembler étrange qu’il soit attendu que le système de déduction puisse modifier cet ordre, dans le cas où cette partie droite contiendrait plusieurs éléments.

Note : quand plus haut il est question d’éléments, il faut comprendre des éléments du séquent, pas des éléments des expressions du langage objet.

Ça pourrait être une liste, mais cette liste ne contiendrait typiquement qu’un seul élément. Comme de plus ce qui est à gauche est une disjonction, pour quelle raison avoir par exemple A ⊢ B, C quand pour la condition d’une inférence, on pourrait avoir une règle avec A ⊢ B comme condition et une règle avec A ⊢ C comme condition, et de même pour une conclusion. Vu comme ça, il serait possible de générer automatiquement les règles d’inférence correspondantes, qui sont ne pas en grand nombre, au pire, alors que les séquents sont inévitablement produits en grande nombre dans n’importe quelle preuve non‑triviale, ce qui indique de les rendre le plus léger possible. Ça indiquerait d’utiliser un type à un ou zéro élément. Mais je n’ai que rarement vu des séquents avec rien à droite. Quoique ça ne coûte que peu d’avoir un type option pour la droite du séquent, ça coûte en tous cas moins qu’une liste.

En continuant à descendre dans la structure, on arrive aux éléments des antécédents et succédants. À priori, il ne peuvent pas appartenir au système de déduction et ne peuvent que être spécifiques aux concepts du langage objet, mais pas sûr qu’il puisse en être ainsi et au moins la transformation d’un terme en un terme équivalent, est souvent nécessaire aux démonstrations.

Il ressort que les éléments à gauche, sont souvent des dictionnaires ou des listes ou des ensembles. Parfois, un de ces éléments apparaît à droite appelé comme une fonction, prenant un terme en argument et semblant renvoyer un terme, ce qui est conforme à un dictionnaire.

Je me demandais si les éléments à gauche, peuvent être modifiés implicitement par ajout d’un élément les suivant dans une conclusion. Par exemple je me demandais si dans A ⊢ B ∴ A,x ⊢ C, s’il faut comprendre que x peut devoir être ajouté à A ou ne reste que simplement ajouté à l’antécédent du séquent produit dans la conclusion. Après avoir imaginé plusieurs intentions possibles, ll me semble plutôt maintenant, que A,x ⊢ C dans une conclusion, signifie que la conclusion impose une condition aux éventuelles inférences qui feraient usage de cette conclusion. Si ça n’était pas le cas, cette possibilité manquerait.

J’ai déjà vu une conclusion d’une inférence, où ce qui apparaissait à droite du séquent dans la conclusion, ne pouvait que être indiscutablement ajouté au contexte produit. Après tout, si dans une conclusion on a C ⊢ e, comment cela ne pourrait‑il pas correspondre à C ⊢ e dans une condition, et ceci, quelque soit e pourvu qu’il corresponde d’une manière restant à définir. La notation C ⊢ e est en fait la notation de l’augmentation du contexte, que je cherchais sans l’avoir trouvé. Ça me semble maintenant tellement évident que je m’en veux de ne pas l’avoir compris avant.

Si un élément à gauche d’un séquent, est une sorte de conteneur, alors ce qu’il contient pourrait devoir être considéré comme étant des éléments du contexte. Il faudrait le revérifier en relisant des documents qui m’ont fait me poser certaines questions à propos de leurs types. En tous cas, ce serait aussi une réponse à une interrogation sur des notations que je vois parfois, où apparaissent des séquences clairement de longueurs variables (exprimées sous une forme du genre A1, A2, … An) à gauche de séquents. Ça suggère que ces éléments agissant comme des conteneurs, ne soient pas opaques pour le système de déduction générique.

Il me semble en même temps, que le vision des éléments du contexte comme conteneurs, n’est qu’une vision dérivée. Je crois que les éléments d’un contexte, les symboles qui y apparaissent, sont en fait simplement une identification d’un ou plusieurs contextes pouvant correspondre à cette désignation. La vision comme conteneur, serait en fait la collecte de ces correspondances. Dans ce cas, le type de ces conteneurs, qui seraient virtuels, doit se déduire des règles d’inférence du système de déduction.

Il serait cohérent que l’identification des conteneurs par les symboles qui y apparaissent, se comprennent assez comme la tête d’une clause Prolog, mais de trois manières au lieu d’une seul. Le nom de la clause serait composé par les symbols apparaissant dans l’antécédent, en respectant l’ordre ou pas et/ou en respectant le nombre d’occurrence du symbol ou pas ; c’est à dire que la nom de la clause devrait être normalisé avant de tenter de trouver ses correspondances. La notation A ⊢ B, signifierait que pour une des clauses A, le corps correspond à B.

L’analogie avec des clauses Prolog pourrait se poursuivre avec la partie droite des séquents, une correspondance en accord avec une notion d’équivalence des expressions du langage objet, une question abordée plus loin.

La différence avec Prolog, serait qu’il n’y aurait pas d’unification par instantiation de variables (à moins que ?), seulement un test d’unification.

En fait, il serait peut‑être utile d’envisager des constantes avec un indexe, les symboles à gauche, seraient alors des paires symbol × indexe. Ça répondrait à deux questions : celle des éléments apparaissant en plusieurs exemplaires et celle des notations évoquant des séquences, donc des élément indexés. Reste à savoir si ces indexes seraient des entiers naturel ou pourrait aussi être des constantes. En même temps, je me demande si ces indexes ne devraient pas plutôt être exprimés dans ce qui serait le corps de la clause, ce qui simplifierait la description et rendrait les conclusions des inférences, plus lisibles. De plus, il serait préférable que ce soit le langage objet, qui les exprime, il n’en serait que plus explicite et donc lisible. J’ai vu un élément de contexte semblant être appelé comme une fonction, à la droite d’un séquent, ce qui pourrait suggérer que l’arité des clauses n’est pas nécessairement zéro. Dans ce cas, il y aurait bien unification avec instantiation de variable. Ça serait aussi une réponse à la question des indexes, l’index étant une variable devant correspondre à un numéro. Mais ça ne répond pas à la question des listes.

L’analogie avec Prolog semble assez bien coller, et ça me rassure personnellement, car correspondante à une intuition que j’avais d’un système de démonstration élémentaire, avant de m’intéresser aux séquents et à la déduction naturelle.

Note : quand je parle de Prolog, je ne parle pas d’ISO Prolog (une monstruosité, à mon avis), je parle de son principe de base.

En dehors des symboles représentant des objets abstraits ou pas dans les séquents, il y a toujours dans la logique appliquée, des expressions dans un langage objet. Inutile de partir dans la définition d’une grammaire pour chaque langage objet, c’est trop de problèmes (problème des grammaires ambiguës, problème du nombre d’éléments de prédiction, problème de lisibilité de la grammaire, etc). La solution qui me vient immédiatement et je n’en vois pas d’autres, c’est de prévoir une spécification de la notation, sous la forme de mixfix, qui est d’ailleurs utilisée dans les assistants de démonstration HOL4 et Isabelle/HOL. Les mixfix sont une extension de la classique définition des opérateurs unaires et binaires par précédence et associativité, qui permet des opérateurs ternaires ou même de plus grande arité et permet aussi des opérateurs englobants jouant le même rôle que les parenthèses (je pense en fait à une extension de ces mixfix, mais je ne la décrit pas ici, et n’ai pas encore les idées claires à ce sujet). Ce serait en tous cas visiblement approprié aux expressions que je vois typiquement apparaître, des expressions faites d’opérateurs et de noms, des expressions pour lesquelles une spécification de syntaxe à base de mixfix suffirait, sans nécessiter de grammaire dans le genre BNF et autres variantes qui n’apporteraient rien de plus, si ce ne sont des difficultés à l’usage.

Les séquents ne sont pas tout, même s’ils sont au cœur et générés en grand nombre, il y a aussi les règles d’inférences, sans quoi les séquents ne servent à rien. Visiblement, il ne faut prévoir aucun ensemble fix de règles et permettre de toutes les définir à partir d’un ensemble initialement vide. Elles seraient appliquées par pattern-matching sur la syntax abstraite (pas sur la syntax concrète, ce serait trop limitant) et substitutions (si c’est suffisant). Ça n’empêcherait pas de prévoir des méthodes dédiées pour certaines règles, comme la règle de la contraction ou la règle de l’échange, qui si elles apparaissent effectivement dans la liste des règles d’inférences, pourraient même être appliquées automatiquement dans certains cas (pendant l’écriture interactive d’une preuve, mais pas pendant la validation d’une preuve).

Pour certains systèmes de déduction, l’application des règles d’inférence nécessite au moins une condition supplémentaire en plus de la correspondance par pattern‑matching : dans les relevant logics, l’introduction d’une implication par une règle d’inférence, nécessite que la partie droite et gauche de l’implication produite dans la conclusion, ait au moins une variable libre en commun (comme garantie que l’implication n’est pas insensée au sens intuitif du mot). Je ne sais pas si c’est le seul cas particulier de ce genre ou s’il y en a d’autres. S’il y en a d’autres, je ne vois pas comment faire une généralisation de ce type de nécessité.

Mais en même temps, c’est un concept du lambda calcul, ce qui n’est pas inattendu, alors peut‑être que simplement prévoir la possibilité des opérations et tests typiques du lambda calcul non‑typé, sur les éléments des séquents, pourrait être une piste de réponse. Non‑typé, pour être plus souple, les éventuelles contraintes s’exprimeraient dans les règles d’inférence et les expressions initiales seraient déjà contraintes par les règles du langage objet, surtout si la syntax des expressions ne permet pas d’exprimer une quelconque surcharge des opérateurs. Ça conviendrait pour la transformation d’un terme, mais pas toujours pour tester l’équivalence de deux termes, à moins que les incompatibilités par le type, ne soient représentées par des constantes, qui sont non‑réductibles et seulement égale à elles‑mêmes et à leurs copies. Ça pourrait au moins suggérer de supporter le lambda calcul simplement typé, pour les tests d’équivalence de termes, mais je doute que le simplement typé soit suffisant d’après ce que j’ai lu et les systèmes de typage du lambda calcul ont tendance à être compliqués. Disons que ces logiques ne seraient alors pas supportées. De toutes manières, il n’y a aucun intérêt à vouloir supporter des logiques aux typages si compliqués qu’elle vont contre un critère d’accessibilité souhaitable depuis le domaine d’application posé (logique appliquée à l’informatique, en tenant pour contexte de l’informatique, des notions générales provenant de SML). De plus, ces logiques aux typages compliqués, ne me semblent pas incontournables (ex. théorie des catégories vs théorie des types).

Ça peut suggérer que les substitutions doivent être définies comme elles le sont dans le lambda calcul (en espérant que ce ne soit pas trop limitant). Peut‑être envisager aussi que les termes soient tous formulées sous cette forme, mais ce serait une applicabilité implicitement limitée, s’ils contiennent beaucoup de constantes rendant les réductions sans effets. Cette forme aurait au moins l’avantage de pouvoir définir l’équivalence des termes, dans un formalisme pertinent et connu.

Les précédentes remarques inspirent, avant de conclure, de revenir sur les termes du langage objet. Il est sûrement utile de prévoir la possible application de règles structurelles aux termes du langage objet, comme il peut en exister dans le système de déduction. À la règle weak, pourrait correspondre l’insertion d’un terme neutre pour un opérateur, à la règle contr, pourrait correspondre la suppression d’une expression idempotente (ce qui peut impliquer les termes neutres), à la règle xch, pourrait correspondre la commutativité pour un opérateur, à la règle subst devrait correspondre l’incontournable substitution par un terme équivalent, même si je ne vois pas comment la règle structurelle subst, est une substitution pour un système de déduction malgré que son nom soit parlant, et à la règle cut, pourrait correspondre la suppression d’un terme non‑utilisé. Il serait intéressant de voir comment la règle subst, se dérive en déduction naturelle, ça permettrait peut‑être de comprendre pourquoi elle s’appel ainsi et de peut‑être constater que la substitution dans des termes du langage objet, peut ou doit, se dériver d’autres règles structurelles de ces termes.

L’idée est seulement de vérifier les étapes de démonstrations, pas de générer automatiquement des démonstrations, quoique que des étapes simples pourraient être générées automatiquement ou suggérées. Je trouve que les démonstrations automatiques aident plus souvent à se perdre qu’à comprendre quelque chose.

Il faut prévoir au minimum, une validation informelle, en testant sur des cas réels, pour voir si les inférences de preuves réelles (et qui ne sautent pas d’étapes, ça ne va alors pas être facile à trouver), sont effectivement validées par la mise en œuvre.

Garder la mise en œuvre le plus simple possible (ne pas se ruer sur des optimisations non‑triviales pour des cas particuliers), pour que ses fonctionnalités puissent être démontrées un jour. Seulement à ce moment là, envisager une mise en œuvre dérivée plus efficace s’il y a besoin, et non‑pas sans preuves de son équivalence. Je crois que le minimum, pour un système formelle, et qu’il soit lui‑même formellement vérifié, ce que je n’ai pourtant encore jamais vu (si c’est parce que c’est impossible ou trop difficile en pratique, je l’apprendrai alors et je penserai à le rapporter).

Juste deux notes avant les deux messages annoncés hier‑soir.

D’abord le message précédent a beaucoup été modifié depuis qu’il a été posté hier‑soir, il y aurait encore beaucoup d’affinage à faire, mais je vais le laisser ainsi, il défriche déjà assez (la suite que je lui donnerai, sera personnelle).

Ensuite, une idée qui m’est venu à propos d’un récent message sur les définitions impredicative vs predicative. Pour résumer, je disais que les définitions impredicative sont de mauvaises définitions selon moi, qu’elles devraient plutôt être des propositions à posteriori. Puis dans l’après‑midi je me suis dis que la formule pourrait quand‑même bien être posée à priori, mais pas en temps que définition.

Quand on pose une équation, on peut trouver une solution mais parfois sans être sûr du résultat. Dans ce cas, on teste la solution en appliquant la formule de l’équation à la valeur trouvée, pour voir si ça colle. Dans ce cas là, la formule de l’équation est utilisée comme une proposition qu’on vérifie.

Peut‑être alors qu’il serait possible d’assimiler les formules impredicative à des équations, quand elles sont posées à priori. Reste toujours qu’une équation n’est pas une définition, une équation est quelque chose à résoudre  et la méthode de résolution reste centrale.

Ce sujet avait été ouvert il y a longtemps, le 19 Novembre 2013, cela fera 7 ans dans un peu plus d’un mois et demi. Il a été ouvert comme sujet, en apparence comme ça, sans cause ni but, mais il y avait bien une intention d’aboutir à quelque chose en l’ouvrant, et une cause aussi ; c’est ce que je vais essayer de résumer en deux messages distinctes.

Le premier, celui‑ci, parlera de ce que je cherchais, de comment j’en suis venu à commencer ce sujet et des difficultés et déceptions que j’ai rencontré en cherchant ce que je cherchais. Je ne suis revenu sur ce thème que épisodiquement, faute de temps, même si parfois j’y revenais sans toujours rapporter quelque chose dans ce sujet dédié. Le second message qui suivra celui‑ci et qui sera probablement le dernier avant longtemps sur ce sujet, décrira en gros les idées que je tenterai un jour de mettre en œuvre.

Ce que je cherchais, c’était un moyen de décrire la logique de programmes et de vérifier qu’ils correspondent bien à cette logique, ce qu’on appellerait la correspondance à une spécification, mais pas par conviction souvent déçue, plutôt par démonstration, la démonstration, si elle échoue, devant permettre de savoir ce qui ne va pas.

Si je cherchais ça, c’est parce que je me suis souvent trouvé complètement perdu avec des erreurs de logiques que je ne parvenais pas à résoudre dans certains cas ou dépité devant des erreurs énormes que les systèmes actuels laissent passer. Je ne cite que le premier que j’ai rencontré, qui était avec un interpréteur Basic de Microsoft (QBasic). En écrivant une fonction pour je ne sais plus quoi (soit quelque chose qui faisait des dessins en arabesques ou quelques chose à voir avec les langues), j’ai eu la surprise de voir que le programme ne répondait plus sans pourtant s’arrêter en signalant une erreur. Je l’ai arrêté, redémarré, arrêté une seconde fois ou une troisième encore, et ai compris à la position du curseur qui se positionnait à la dernière instruction en cours, que le programme était coincé dans une boucle sans fin, que j’avais écrit avec une erreur bête. Je n’y croyais pas, tellement l’erreur était bête, je croyais que l’interpréteur aurait du me signaler une erreur. Pour m’assurer de ce qu’il en était, j’ai écrit une boucle infini, sans rien dedans et ai lancé le programme, … qui est parti dans une boucle infinie qui ne faisait strictement rien, sans que l’interpréteur ne refuse de lancer un programme qui n’avait pourtant aucun sens. Je me suis dit « mais c’est complètement stupide ».

Je cite quelqu’un en gros, que j’ai déjà rapporté ici : « Avec l’informatique, c’est facile d’écrire quelque chose, surtout n’importe quoi, c’est beaucoup plus difficile de faire quelque chose de correcte ». Il poursuivait en disant que beaucoup de gens qui pourtant devraient le savoir, n’en sont généralement pas conscients et ne le découvre que petit à petit.

Il a trop raison. Le problème et que rien n’aide à faire les choses correctement, et il n’y a même rien pour formuler ce qui est correcte. Les langages typés, c’est la base élémentaire, c’est bien, mais le typage est trop peu, et de plus, on est actuellement dans pire que ça encore, la domination des langages non‑typés (dont certains commencent à comprendre après longtemps, que le typage, c’est peut‑être bien finalement quand‑même, après s’en être moqué pendant des années ou deux décennies, et se trouve à essayer de le coller sur des choses qui n’ont pas été conçues pour ça).

Deux problèmes se posent donc. Le premier, le plus flagrant, est que les langages en vigueur, et c’est encore plus vrai pour les langages les plus populaires, ne sont pas du tout adaptés à ça, et sincèrement, je crois que si c’est ainsi c’est parce que « tout le monde » s’en moque. Ce contexte n’aide déjà pas. Il y a en plus le second problème, celui de la formulation logique de ce que le programme est censé faire, la question de cette formulation n’a pas de réponse venant toute seule.

Partant de ce deuxième problème à résoudre et sans m’arrêter au premier, j’ai simplement cherché un peu partout ce qu’il se fait dans le domaine de la logique appliquée à l’informatique, ce qui est souvent appelée l’informatique théorique, qui ne me semble pas souvent appliquée. Sans m’arrêter à cette autre constat, j’ai quand‑même continué à chercher.

Ce qui ressortait le plus devant moi, c’était trois choses, qui à priori pouvaient sembler prometteuses : proposition as type, type theory et HOL, qui est une logique présentée comme celle d’un lambda calcul typé et dont l’histoire remonte à un système nommé LCF, pour Logic for Computable Functions. Les deux premiers domaines sont surtout des sujets de recherche non‑directement applicables, le troisième semblait plus appliqué, comme il existe des assistants de preuve inspiré d’un système qui avait été lui‑même conçue pour étudier la logique des fonctions calculables, mais dont j’ai appris plus tard qu’il avait surtout été utilisé pour la conception de circuits intégrés.

J’ai passé beaucoup de temps à essayer d’apprendre à utiliser deux de ces systèmes, surtout Isabelle/HOL, puis un peu HOL4, en faisant quelques écarts vers Coq dont la logique n’est pas la même bien qu’étant en rapport sur un point (les types dépendants).

Avant de me lancer, j’ai lu des documents, suivit des discussions dans et posé des questions sur des mailings lists, et tout le monde semblait affirmatif sur un point : ce système est adapté à la démonstration des propriété de programmes. J’ai eu confiance en ces réponses, d’après des choses que j’avais lu ailleurs avant.

Je n’ai rencontré que des difficultés à essayer de reformuler des choses qui m’avaient posé problème avec des langages ordinaires et à démontrer leurs caractéristiques, et j’ai échoué à chaque fois.

Le type de problèmes que j’ai rencontré peut donner une idée des difficultés. J’ai plus tard, tardivement, compris pourquoi je n’y arrivais pas, mais c’est pour la suite juste après.

Une fois, au cours d’une démonstration, j’arrive à la conclusion qu’un ensemble contient un certain élément. Plus loin, il était nécessaire de démontrer que cet ensemble n’est pas vide. Je me disais que ça devrait être assez trivial à démontrer. Eh bien non, après d’abord des heures, puis deux jours à tenter de le démontrer, j’ai fini par abandonner : un ensemble contient un élément, et sous cette hypothèse, pas moyen de démontrer que alors cet ensemble n’est pas vide.

Une autre fois, au cours d’une autre démonstration, je me retrouve avec une formule dont je devait démontrer qu’elle valait, 5, je crois, en tous cas, une valeur bien déterminée et précise, pas un vague nombre flottant. Le terme dont je devais démontrer l’égalité avec cette valeur, était une formule simple et qui aurait dut être directement calculable par substitutions successives. Ça aurait donc dut être trivial, mais non, là aussi, après beaucoup de temps passé à chercher une solution, j’ai abandonné.

Pour autre chose, je décrivais les propriétés d’un type de donné, et au cours d’une démonstration, j’échoue à démontrer une chose à partir d’une autre. Intrigué, tellement c’était évident, je test comme ça la démonstration de la négation de la première chose, et la démonstration a put être faite, j’avais démontré une chose et son contraire à propos des propriétés de ce type. J’ai compris par la suite que le langage dans lequel j’avais fait cette formulation, ne se lisais pas comme je le lisais, des démonstrations que je croyais faire sous un contexte, se faisait sous en fait je ne sais quelles hypothèses, je n’ai jamais put le savoir, tellement le langage dans lequel les termes étaient formulés, prêtait à confusion (il pouvait par exemple être difficile de savoir où se terminait une série de déclarations à propos d’une chose et où commençait une série de déclarations à propos d’une autre chose, rien ne les délimitait explicitement).

Je ne parvenais donc pas à démontrer la moindre propriété d’un programme de cette manière, sans parler des difficultés à formuler les choses avant de pouvoir formuler les propriétés à démontrer.

Persévérant et restant sur ce système parce que j’étais convaincu que ce système était la solution, je lisais une documentation sur une théorie des mots de 16 bits qui avait été démontré avec, me disant que ça au moins, c’était applicable à l’informatique et que je pouvais alors étudier cette théorie pour découvrir comment m’y prendre. Mais des choses me semblaient étranges. En posant une question à quelqu’un, on m’a répondu sans le dire trop explicitement, que ce système n’est pas vraiment fait pour ça, qu’on peut en théorie, mais que en pratique, ça n’est pas fait pour ça. Ceci après qu’on m’ai assuré du contraire à plusieurs reprises (c’est idiot et je ne sais pas dans quel but).

C’est après plus de quatre années passées à avoir persévéré avec, par périodes espacées, qu’on me l’a dit. Et pendant tout ce temps, j’ai cru que c’était moi qui m’y prenais mal ou n’y comprenais rien, tout en en étant déçu, parce que je croyais que la solution était dans cette logique ou ce système.

Ce type de bilan (discours théorique peu préoccupé par la réalité concrète et pratique, logiques inadéquates) s’est répété avec d’autres systèmes et des logiques partageant des points communs et variant sur d’autres, je ne vais pas tout raconter, il y en aurait pour des pages, les quelques exemples concrets rapportés en donnent une idée.

C’est avec le temps, au fil de mes tentatives de comprendre ces systèmes, que j’ai ouvert ce sujet, pensant qu’avoir une idée du monde des logiques en général, pourrait aider à y voir clair. C’est aussi en pensant à ce que devrait être un système réellement conçu pour faciliter la conception et la maintenance de programme, que j’ai fini par arriver à la conclusion, que mieux vaut peut‑être encore tenter les pistes, formelles aussi, qui venait à l’esprit sur ce qui serait adéquate, puisque l’existant ne l’est pas.

Ce qu’est une solution plus adaptée selon moi, sera l’objet du prochain message.

Pour l’instant je résume la situation avec l’existant.

Les systèmes de démonstrations actuels doivent leur popularité, non‑pas à des auteurs de logiciels, mais à des chercheurs essentiellement en mathématiques et logiques, mais pas logique concrètement appliquée à l’informatique, seulement en théorie applicable à l’informatique. Ces systèmes sont plus faits pour les démonstrations mécaniquement vérifiables de théorèmes divers, dont le théorème des quatre couleur et un des théorème de Gödel qui ont été démontré avec ces systèmes, et de nombreux autres théorèmes encore (des centaines ou des milliers si on compte tous les systèmes de démonstration), mais dont aucun n’aide en quoique ce se soit quand il s’agit de démontrer les propriétés d’un programme.

La logique la plus populaire est de loin avec les systèmes de démonstration, assistants de démonstration, etc, c’est la théorie des types dépendants, et cette théorie a une réputation surfaite concernant sont applicabilité à l’informatique, simplement parce que tout le monde se contente de discours, cite des documents théoriques, sans jamais s’étonner de l’absence ou de la rareté des applications pratiques ayant abouti.

Je n’ai pas parlé des systèmes venant s’ajouter en surcouche ou à côté de langages qui au départ n’avaient pas été conçus pour ça (ex. pour Ada, C, etc), ils sont décevants aussi, et quand le compilateur est bogué, ça ne sert à rien, mais comme dit précédemment, je ne vais pas faire des dizaines et dizaines de pages d’exemples.

S’ajoute à ces problèmes techniques, des problèmes humains, comme l’intrusion idéologique tout‑court ou la pollution idéologique par ceux pour qui « tout est politique » et qui dictent la communication, lynchent tout ce qui est contraire à leur idéologie et auxquels trop de gens croient devoir se soumettre en croyant ne pas avoir le choix . D’autres problèmes humains comme l’élitisme dans la tour d’ivoire parfois jamais perchée assez haute, la déconnexion d’avec la réalité dut aux classes sociales les plus représentées dans ces milieux, etc. Un problème humain, pour lequel je n’ai pas d’explication certaine, est la publicité mensongère ; oui, elle existe dans ces domaines aussi, et elle fait perdre beaucoup de temps et d’énergie pour du vent. Ces problèmes humains, je n’y reviendrai pas, je n’ai que voulu au moins les mentionner, parce que la réalité pratique, c’est important.

Inévitablement, j’en suis arrivé à chercher la solution, ailleurs, et à plus voir comme une solution crédible, la mise en œuvre d’intuitions que j’ai depuis longtemps (depuis environ l’époque peu après ce dépit devant cet interpréteur Basic qui me semblait si stupide), que j’avais mis de côté en me disant que ce serait trop gros, que des gens plus à même d’y parvenir y seraient déjà parvenu avant, etc. Finalement, peut‑être finalement, si, il serait intéressant de tenter de mettre ces intuitions en œuvre, vu le résultat d’avoir essayé ce qui se présentait comme le plus prometteur.

Dans le prochain message, j’expliquerai pourquoi les types dépendants et d’autres théories, ne me semblent pas adaptés à l’informatique appliquée, et dirai en gros ce qui me semble peut‑être de meilleures pistes et pourquoi.

Plus de détails sur l’inadéquation des systèmes de déduction mentionnés précédemment et tentative d’apercevoir d’autres solutions.

Retour sur les types dépendants d’abord.

Les types dépendants, je les surnomme les types indexés, tout‑court, parce que c’est environ tout ce à quoi il correspondent pour le typage. On les retrouve décrits ainsi dans tous les documents d’introduction à leur sujet et c’est la seule forme sous laquelle je les ai connu avec un langage se promouvant comme basé sur les types dépendants, alors que cet aspect était peu significatif dans ce langage, mais le concept des types dépendants est tellement vendeur dans ce domaine, que c’est sur cet aspect que l’accent est mis pour la communication sur ce langage.

L’exemple qui revient systématiquement en présentant les types dépendants, c’est la catégorisation des listes par longueurs ou parfois des vecteurs par longueurs (c’est la même chose finalement, mais ça donne l’impression de varier les examples), je ne sais pas pourquoi l’exemple de classifier les ensembles par cardinaux n’a jamais été donné, mais ça n’irait pas plus loin non‑plus.

Que peut‑on formuler avec ça ? Peu de choses ; la longueur d’une liste, c’est un aspect important d’une liste, mais c’est loin d’être un concept suffisamment expressif pour formuler les conditions de validité d’un programme ou plus généralement, les propriétés d’un programme. Les types indexés sont peut‑être assez expressifs pour beaucoup de choses, je le crois d’après le nombre de démonstrations qu’ils ont permis dans plusieurs domaines des mathématiques, mais pas pour le domaine d’application dans lequel se place ce sujet.

Un document sur le calcul des constructions, à la base de Coq, un autre système de déduction, parlait de HOL comme d’une logique plus concernée par les propriétés des termes que par les calculs. Mais si Coq est plus concerné par les calculs, il reste basé sur une théorie des types dépendants, il n’est pas plus expressif pour le domaine d’application d’intérêt ici. Ce même document décrivait les types dépendants avec toujours un de ces mêmes exemples maintes fois vus : la classification des vecteurs par leurs longueurs. Juste après il donne un exemple semblant pour une fois plus intéressant mais le terminant aussitôt par une douche froide. Il dit qu’on peut utiliser les types dépendants pour par exemple exprimer l’ensemble de tous les nombres paires, mais en disant immédiatement ensuite, que en pratique, ça devient rapidement inextricable, parce que se pose des problèmes d’égalité de types que le système de déduction supporte mal.

Que HOL soit plus concerné par les propriétés des termes que par les calculs, comme l’affirmait ce document sur le calcul des constructions, ne m’étonne pas, comme j’ai toujours abandonné par désespoir en tentant de faire des démonstrations non‑pas sur des propriétés de termes en eux‑mêmes, mais sur des relations entre des choses (incluant des composants de ces termes) ; par « choses », il faut comprendre des termes de natures variées, plus que de types différents, pouvant être de genres différents. Un programme se décrit plus facilement comme des relations entre des choses que comme des propriétés d’un terme en lui‑même. Pour prendre l’exemple générique du programme comme opérations sur des entrées‑sorties, on a plus à l’esprit des relations entre l’entrée et la sortie, que des propriétés d’un hypothétique terme entrée‑sortie, qui est une structure peu commode à aborder comme un terme (je viens de lâcher un mot un important un peu trop en avance). Mais malgré que le calcul des constructions se dise plus préoccupé par les propriétés des calculs que HOL qui ne le serait que par les propriétés des termes, il ne permet pas mieux d’exprimer ces relations.

Un autre exemple de plutôt inadéquation, est plus immédiat. Dans la théorie des types, avant de poser un type, il faut poser un terme de ce type (ça fait penser aux définitions impredicative dont il a été question précédemment). Dans ce domaine, on dit qu’il faut démontrer que le type est habité avant de pouvoir poser l’existence de ce type. Dans l’informatique, il est pourtant courant de définir un type pour seulement ensuite définir des fonctions créant des termes de ce type, ou de définir un type tout en décrivant des constructeurs de ce type, ça n’a jamais posé de problèmes ou peu, le problème essentiel n’est simplement pas là. C’est à contre courant des pratiques courantes donc, mais on pourrait arguer que oui, ça n’a pas de sens de poser un type dont il ne peut exister aucun terme. Seulement, c’est implicite dans les langages typés : s’il est impossible de créer un terme d’un type préalablement défini, ben ça ne va pas plus loin et c’est tout ( … ou pas tout‑à‑fait, l’environnement d’execution d’un programme pouvant s’accorder des pouvoirs magiques, mais c’est pour plus loin), ce n’est même pas une erreur d’execution, c’est une impossibilité statique. De plus, les expressions permettant de définir des types, garantissent, sauf cas particuliers, qu’un terme du type existera, inductivement, comme ces types sont définis par composition, comme produit ou somme (au sens du domaine, pas exactement au sens courant) de types qui incluent des types prédéfinis pour lesquels il est garanti qu’il existe des termes de ce type. Ce concept n’apporte pas l’expressivité attendue non‑plus, il exprime juste statiquement à priori, ce qui dans un autre domaine, se constate tout autant statiquement, juste à posteriori.

Dans d’autres cas encore, cette théorie pourrait se montrer prometteuse mais s’avère décevante, comme avec les types énumérés (ou équivalents à des types énumérés) par exemple, mais je ne vais pas en faire des pages.

Les échecs du genre impossibilité (ou difficultés apparemment sans fin) de démontrer qu’un ensemble est non‑vide sous l’hypothèse où pourtant cet ensemble contient un certain élément, je ne sais pas si c’est un résultat de la théorie des types, je suis seulement sûr que c’est un résultat du domaine d’application de la théorie des ensembles tel que formulée dans ce système de démonstration (et idem dans d’autres). La formulation convient apparemment bien pour certains domaines, mais pas pour celui de ce sujet. On peut poser avec un langage comme SML, une définition de ce qu’est un ensemble, d’où découle comme une évidence (mais SML ne permet pas de dériver une évidence, ce n’est pas un langage de démonstrations, ou seulement dans une logique limitée), qu’un ensemble contenant un élément quelconque, n’est pas vide, en le dérivant de la définition de « e est inclus dans S » et de la définition de « S est vide », pour certaines de ces définitions au moins, ce qui est raisonnablement garanti, comme les définitions qui viennent le plus trivialement, en font partie. Ce cas servira d’exemple plus tard.

Le précédent exemple est un autre exemple d’un type d’impasse qui peut souvent se produire, mais là aussi, mieux vaut abréger.

Ça donne une idée de l’impasse des systèmes de déduction basés sur les types dépendants et des environnements de démonstrations conçus surtout pour les mathématiques, dans le contexte de la démonstration de propriétés de programmes : cette théorie et ces systèmes, n’ont pas l’expressivité attendue.

Note : il peut sembler surprenant de lire une expression comme « la théorie des ensembles dans ce système de démonstration ». Oui, il existe plusieurs théories des ensembles, pas une seule, et oui aussi, un système de démonstration peut avoir sa propre théorie des ensembles. Pour le comprendre, il faut penser que une théorie, c’est un ensemble de définitions ou d’axiomes, en nombre autant réduit que possible (ça dépend des points de vu quand‑même), et de théorèmes démontrés à partir de ces faits de bases préalablement posés, ou de théorèmes dérivés de ces faits et d’autres théorèmes, et ainsi de suite. C’est ça, une théorie, et il n’est alors pas étrange qu’un système de démonstration ait sa propre théorie des ensembles et que même en dehors de ce système de démonstration, il existe plusieurs théories des ensembles, y compris dans le monde des mathématiques sans informatique, des théories des ensembles équivalentes en certains points, peut‑être pas en d’autres, différentes en ce qu’elles permettent plus facilement ou plus difficilement de démontrer ou de formuler telle ou telle chose, que dans une autre théorie. Il en va ainsi d’autres théories, pas seulement de la théorie des ensembles. Même quand il peut être prouvé que certaines de ces différentes théories sont équivalentes dans ce qu’elle permettent de démontrer ou autres propriétés, elles différent presque toujours dans les aspects pratiques que sont la formulation ou la démonstration d’une chose ou d’une autre.

Ce que je pensais écrire en un message, en un second message après le précédent, sera finalement écrit en deux messages. Ce qui aurait dut être la deuxième partie de ce message, sera en fait un message suivant.

Suite …

C’est implicite et alors important à souligner explicitement : l’informatique, c’est beaucoup une histoire de représentations et de conversions d’une représentation(s) à une autre(s). Deux examples de natures différentes, l’illustrent.

La première illustration est technique. L’affichage d’une image à l’écran, c’est une représentation dans la mémoire de la carte graphique, qui aboutit à une représentation à l’écran, sur laquelle on reconnait une chose, c’est une représentation de coordonnées dans un espace à deux dimensions, celui des pixels, chacune associée à une coordonnée dans un espace à trois dimensions, un espace de couleurs, pouvant lui‑même être variable. Ces représentations finissent en représentation visuelle où elles s’arrêtent, le reste de l’interprétation ne relevant plus que de l’humain. Cette représentation dans la mémoire de la carte graphique, est elle‑même le résultat d’une éventuelle conversion d’un espace de couleurs à un autre, c’est à dire entre deux représentations possibles des couleurs. On pourrait aller ainsi jusqu’au fichier dans lequel est enregistré l’image, au système de fichiers qui a la responsabilité de son stockage pérenne, etc. Chacune des ces représentations représente la même chose (éventuellement modulo quelque chose), mais a des caractéristiques techniques propres, qui sont à l’origine de ces différences de représentation. Pour un espace de couleurs, ça peut être la consommation mémoire par pixel en tenant compte des capacités d’affichage effectives de l’écran. On veut consommer le moins de mémoire possible, et ne pas gaspiller de la mémoire à y représenter des nuances de couleurs que l’écran ne peut pas distinguer. Idem pour le fichier stockant l’image, on peut vouloir le préférer petit parce qu’on en a beaucoup, quitte à perdre un peu en finesse de grain ou nuance de couleur ou vraiment tenir à préserver autant que possible les nuances de couleurs parce que l’image est celle de quelque chose d’important, quitte à ce que le fichier soit plus gros.

Le seconde illustration est plus humainement pratique. Imaginons qu’on se préoccupe de savoir quels sont les effets des événements météorologiques successifs sur des bilans de récoltes de diverses cultures. On ne va évidemment pas mettre la météo ni les récoltes dans l’ordi’, on va seulement faire abstraction de presque tout, ne gardant que ce qui permettra de donner une réponse aux questions s’il y en a une : les relevés météorologiques de chaque journée et les quantités récoltées avec leurs dates. Ces choses, qui sont pourtant déjà abstraites, nécessitent des représentations pour ne pas être oubliées, et cela, même sans l’informatique. Entre parenthèses, c’est pour ces raisons que l’écriture, les nombres, l’arithmétique et la géométrie ont chacune à leur tour été inventées. Disons qu’on a trouvé une représentation qui convient bien pour préserver nos notes sans trop de perte de précision, on se contente de relevés de températures à un chiffre après la virgule et de mesures de poids de récoltes à environ dix grammes près. Ça ne répond toujours pas à la question d’origine, mais on a au moins mis en sécurité (sous réserve d’absence d’accident de disque dur par exemple) des précieux relevés qu’on aurait vite oublié sinon et sans lesquels on ne pourrait pas répondre à la question. On va s’intéresser à des corrélations, et il faudra les représenter, par exemple les cumuls de températures entre la date de semis et la récolte, qui seront des sommes dérivées des relevés. On va associer ces sommes à chacune des cultures, et à chaque culture on associera aussi une date de semis et de récolte, ce qui est encore une représentation. Cette représentation permettra pour une date donnée, de savoir quel semis ont été fait, et réciproquement, pour un semis donné, à quelle date il a été fait. Cette représentation est commode, moyennant des méthodes de consultation conçue avec cette représentation, elle permet de naviguer dans les deux sens, sans dupliquer les choses comme en écrivant un double index, avec les risque d’erreurs qui en découlerait. Rien que ces représentations aideront à consulter nos relevés sous une forme plus lisibles ou moins fatigante. On pourrait aller plus loin, et trouver des représentations qui nous feront encore plus avancer vers une réponse à la question.

Ça semble trivial, mais c’est important à souligner explicitement : on a des représentations, des conversions entre des représentations, des relations entre des représentations, ces choses étant elles‑mêmes des représentations. Pour se replacer brièvement dans le contexte de l’exposé de sources de déceptions du message précédent, on a ici, pas de termes à proprement parler, on a que des choses autant composables que décomposables, on a pas des types indexés, ça ne colle même pas de loin.

Je vais faire comme un raccourci parce que je ne sais pas comment l’introduire autrement, mais il existe une autre notion considérée comme aussi importante que la théorie des types, qui est la théorie des catégories. C’est un vaste sujet que je ne connais que très peu, mais qui me parle, et je crois, pas qu’à moi.

Ayant un ensemble de types de données, un ensemble d’opérations définies sur ces types, il peut arriver de se dire « tiens, ces aspects là, ça marche exactement comme une arithmétique, juste que ce ne sont pas des nombres », « ces propriétés là, on croirait beaucoup celles de relations entre des ensembles, partitions, etc » et que ça colle tellement bien que on a aucun mal à formuler informellement des choses sur nos types et opérations, dans ces termes là. Ce genre d’observations n’ont pas été faites qu’en informatique, elles se sont produites aussi dans les mathématiques, peut‑être même avant l’informatique ou sa démocratisation.

Comme il a été question de listes avec les types indexés ou les types dépendants, prenons un exemple à base d’une liste. Comme dit précédemment, ce qu’un type indexé permet d’exprimer sur une liste, est assez limité. En termes de représentations dérivées, on peut dire plus de choses, sur cette liste, selon ce qu’elle représente, justement. Disons qu’on se préoccupe de savoir si la liste est un fragment de texte composé de mots commençant tous par une majuscule. À la liste, on peut associer un ensemble, et dire que cet ensemble doit être inclus dans l’ensemble des lettres et des espaces. On peut ensuite sous cette hypothèse, dire que la liste est une liste de listes, une séquence de listes dont chacune est elle‑même associée à un ensemble, soit l’ensemble de seulement l’espace ou l’ensemble de seulement les lettres. À cette liste de liste, on associe un ensemble de listes (même opérations de pensée à nouveau) ou plutôt un sous ensemble de listes, celui des listes dont l’ensemble de caractères est inclus dans celui des lettres seulement. Chacune de ces listes est vue comme un ensemble, mais ça n’empêche pas de la voir aussi comme une liste en même temps, et on pose donc que le premier caractère de cette liste, est dans l’ensemble des lettres majuscules. À aucun moment on est obligé de par exemple construire réellement dans le programme, l’ensemble des caractères d’une de ces listes, c’est seulement qu’on voit la liste comme étant virtuellement un ensemble et qu’on définit une fonction qui virtuellement produirait l’ensemble des caractères d’une liste.

Alors oui, ça ne se lit pas comme du langage naturel, mais c’est bien plus expressif que les types indexés ou même que les types simples tout‑court (qui sont finalement plus utiles).

Ce que je veux exposer par cet exemple, c’est que cette notion de représentations diverses d’une même chose, qui peuvent ou pas exister dans la mémoire du programme selon les besoins, est une base coulant plus de source, pour parler de ce qui compose un programme, de ce qui en découle, que les types dépendants, qui sont pourtant omniprésents partout, chaque fois qu’on fait des recherches de documentations sur la logique appliquée à l’informatique ou les types et les propositions appliqués à l’informatique.

Une longue parenthèse sur un cas particulier que je veux souligner. La notion de représentation peut aussi être importante pour la formulation d’une condition de validité courante et malheureusement typiquement seulement implicite (faute de pouvoir être vraiment prouvée), celle de la réciprocité de deux fonctions. Comme on est presque toujours dans les manipulations de représentations, et souvent dans les conversions d’une représentation à une autre, une attente qu’on a souvent, consciemment ou pas, pourrait se formuler ainsi : f(g(x)) = x. Avec f, on passe de la représentation x à y, on a typiquement autant de besoin de le faire dans l’autre sens, avec g pour passer de y à x. F et g sont‑elles valides ? Ça se formule comme f(g(x)) = x. Le besoin de cette démonstration est souvent centrale et ne repose généralement que sur la conviction que oui, même quand la réponse est non.

Fin de la longue parenthèse.

Tout ceci est plus facile à raconter qu’à faire, malgré qu’il y ait du concret derrière comme on le verra dans quelques instants. La théorie des catégories, comme la logique de Hoare, sont plus des concepts que des théories directement applicables. La théorie des catégories, c’est une approche qui s’intéresse à la découverte de catégories en mathématiques, mais ne donne pas de méthodes pour les découvrir (ça serait probablement assez impossible). Elle tire quand‑même des leçons de ses découvertes, en notant des principes pour les avoir retrouvé un peu partout, comme la notion de structure et de foncteur. Si ces deux mots font tiquer parce qu’ils évoquent les notions des mêmes noms en SML, je répond tout de suite à la question même pas posée : oui, les notions de structure et de foncteur en SML, correspondent assez bien pour ce que j’en comprends des deux côtés, aux notions des mêmes noms dans la théorie des catégories. C’est tellement flagrant que je me dis qu’il est quasi‑impossible que ces appellations ne fassent pas volontairement référence à la théorie des catégories. Ce langage a pourtant été défini dans les années 1980 et 1990, alors j’imagines que cette théories des catégories dans les mathématiques, existait déjà et était à ce moment déjà bien avancée.

Bref, c’est un concept, mais qui a fait ses preuves en mathématiques, et aussi en informatique. Les structures et foncteurs en SML, ont bien plus d’applications que les types indexés, et sont bien plus commodes à manipuler. Même si ça peut devenir compliqué aussi, c’est au moins après avoir bien avancé.

Ceci dit, ce n’est pas que théorique. Ça va sembler trivial après coup, mais il existe un autre concept dans la théorie des catégories, qui n’existe pas en SML, parce que SML n’est pas un système de démonstration, c’est la notion de logique interne ou d’internalisation d’une logique. C’est à dire qu’on ne pose pas arbitrairement que tels éléments d’une structure peuvent être vus comme ceux de telle autre structure, moyennant des fonctions d’interprétation de la structure d’origine à la structure cible, il faut aussi montrer que la logique de la structure résultante est bien la même que celle de la structure avec laquelle on voit une équivalence.

Parenthèse encore. Là aussi, un cas particulier est à relever, celui de l’équivalence de deux fonctions ou procédures, la première étant souvent une formulation naïve posant des problèmes pratique, la seconde ayant des qualité pratiques, et étant censée faire la même chose que la première, mais bien plus rapidement ou en consommant bien moins de mémoire ou d’autres qualités. « Censée faire » … voilà le problème. La relation d’équivalence entre deux fonctions ou procédures, voilà encore quelque chose qui nécessiterait souvent d’être démontré, mais qui ne l’est pas, faute de pouvoir faire les formulations et démonstrations nécessaires à ça. Ce cas particulier me semble aussi important que le précédent, et ils se ressemblent, quelque part.

Fin de la précédente parenthèse.

J’ai utilisé l’expression « fonction d’interprétation » parce qu’elle m’est venu spontanément, mais je ne sais pas si elle est strictement correcte dans le domaine de cette théorie. Cependant, il y a deux ou trois ans, j’ai lu des choses en diagonale dont j’ai plus ou moins consciemment retenu qu’il existe une relation entre la théorie des modèles, c’est à dire le fait d’associer une logique à une chose lui donnant par là un sens concret, et la théorie des catégories, alors je crois que l’expression convient. Et au passage, cette idée de la théorie des catégories pour expliquer ou généraliser la notion de modèle, me semble à retenir.

Ce sont des visions assez naturelles, qui viennent rapidement toutes seules. Personnellement, si je suis parti sur la piste d’autre chose, ce n’était pas par manque de ces intuitions, au contraire, c’était seulement intéressé par la « promesse » de pouvoir faire des formulations démontrables, comme en pratique et en dehors de petites choses triviales, les intuitions n’empêchent pas les erreurs, de perdre le fil des relations, etc. De plus, les erreurs ne s’additionnent pas toujours, parfois elle se factorisent, d’où la tentation d’aller vers une direction prometteuse pour la vérification (l’échec de la vérification pouvant aider à savoir où ça ne va pas), aux prix de s’éloigner d’intuitions premières, parce qu’elles n’étaient « que » des intuitions.

Ce sera tout pour les représentations, catégories, structures, foncteurs, interprétations et compagnie, place aux questions de logiques et démonstrations. Il semble pertinent de retenir (ou revenir à, selon les cas) la théorie des catégories comme une approche ou un langage abstrait avec lequel on peut exprimer les choses qui comptent le plus dans un programme, mais il faut encore s’assurer que ce qu’on dit est vraiment vrai.

Vu la longueur déjà, je vais devoir encore couper et continuer dans un autre message, encore.