Les logiques : notes en vrac

Suite, … et enfin fin.

Il avait été dit il y a deux ou trois mois, que pour évaluer une logique, il faut d’abord se préoccuper de son expressivité. La raison de cette remarque, a été donnée dans un précédent message. Dans le précédent message, a été ébauché une piste du domaine d’un langage qui pourrait être assez expressif pour formuler le sens d’un programme et ses propriétés. Le message se terminait en disant que cependant un langage expressif ne suffit pas, il faut pouvoir vérifier la validité de ce qui est formulé avec ce langage, tout en faisant remarquer que le domaine du langage en question y fait référence lui‑même, avec une notion de définitions des choses (des choses qui sont appelées des structures) par leur logique interne.

Un précédent message a abordé trois importantes propriétés des logiques : consistency, completeness et soundness.

Plusieurs précédents messages ont parlé de système de déduction et de langage objet. Il faut revenir assez longuement sur ces deux derniers, pour les distinguer d’un autre niveau de langage, avant de poursuivre.

Le langage objet, décrit une logique, celle sur laquelle on se repose pour écrire un programme, celle qui décrit le sens des éléments du programme. Le système de déduction n’est techniquement pas nécessaire, mais ici, on ne fera pas l’impasse dessus, on va seulement le mettre de côté pendant qu’il sera question d’un troisième niveau de langage présenté plus loin, ce qui sera l’occasion d’expliquer ce qu’est concrètement le langage objet.

Le système de déduction a sa propre logique (elle peut parfois être similaire à celle du langage objet). Il a été dit qu’on peut même parler de logique tout‑court pour parler d’un système de déduction, tant qu’on ne confond pas le système de déduction avec le langage objet. Autant la logique du langage objet dit ce que signifient les expressions du langage d’un programme en termes de valeur produite par une fonction, effets d’une opération, etc, autant le système de déduction dit ce que signifie les expressions de la logique du langage objet, en termes qui ne peuvent que être plus abstraits, comme cohérence, incohérence, possibilité, impossibilité, etc, selon les interprétations et les formulations.

La logique du langage objet est surtout exprimée par des séquents définis en grand nombre, qu’on reconnait au suspect symbole ⊢. La logique du système de déduction est surtout exprimée par des règles d’inférence définies en petit nombre, qu’on reconnait à leur fanfaronnant grand trait horizontal, remplacé ici pour raison pratique, par le symbole ∴ .

Le langage objet utilise lui aussi le principe de la règle d’inférence, mais se distingue par les séquents qu’il définit, que le système de déduction ne fait que manier à travers ses propres règles d’inférence.

Il a été dit qu’il ne faut pas confondre le langage objet et le système de déduction. Mais il n’a encore pas été dit que le langage objet ne doit pas être confondu avec le langage de programmation. Il n’en sera pas question en détail ici, mais il est décrit pour le situer et ne pas se perdre par confusion.

Un langage de programmation, un langage concret, est d’abord définit par une syntaxe, la syntaxe concrète. C’est la forme de validité la plus élémentaire qu’on retrouve partout, même avec les langages non‑typés. Par exemple la syntaxe concrète dit qu’une expression peut commencer par une parenthèse ouvrante, se terminer par une parenthèse fermante, que la parenthèse fermante est requise et que une expression entre parenthèses peut elle‑même contenir des expressions entre parenthèses, récursivement. C’est la syntaxe concrète.

À la syntaxe concrète, correspond une syntaxe abstraite, celle dont sera dérivée le sens du programme. Abstraite, parce qu’elle fait abstraction de détails d’écriture. Par exemple, la syntaxe abstraite des langages typiques, sera la même pour ces deux expressions : ((1 + 2) + 3) et 1 + 2 + 3. La syntaxe abstraite est en fait une représentation des éléments du programme, tout comme l’est la syntaxe concrète.

La syntaxe abstraite, est la véritable source du programme, mais ce n’est pas le langage objet dont il a été question, mais il dit des choses sur les expressions dits dans la syntaxe abstraite. Dans la syntaxe abstraite, les expressions sont typiquement déclinées en grandes catégories. Certaines expressions signifient qu’on réserve de la place pour une variable, d’autres signifient qu’on calcul une expression, etc. On pourra dire que ce sont des types ou des classes d’expression. Le langage objet dont il a été question plusieurs fois, est surtout concerné par ces types d’expression plus que par les valeurs exactes de ces expressions.

Par exemple, le langage objet pourra dire qu’il distingue les variables d’entier et les variables de caractère, et dire implicitement qu’il n’est pas valide de mettre un caractère dans une variable d’entier, en ne donnant aucune règle l’autorisant (tout ce qu’il n’autorise pas explicitement, est implicitement considéré comme non‑valide). On pourrait imaginer une règle comme « C ⊢ V : entier ∴ V <-- expression d’entier », pour dire que le langage objet valide l’intention de garder le résultat d’une expression d’entier dans une variable préalablement déclarée comme une variable d’entier. S’il ne donne aucune règle validant de garder un caractère dans une variable d’entier, c’est qu’il le considère implicitement comme non‑valide.

Une subtilité arrive maintenant. Dans une langage qui vérifie les types avant l’execution du programme, les règles de typage sont le plus souvent sans importance pour décrire l’execution du programme, puisque les types ont été vérifiés avant. L’exemple du précédent paragraphe, serait celui du langage objet décrivant la sémantique statique, ou pour le dire avec un mot en plus, la logique de la sémantique statique, c’est à dire la logique du programme quand il est statique, quand il n’est pas en cours d’execution, sa condition de validité avant même de pouvoir parler de le démarrer. Il peut donc exister (ce n’est pas toujours le cas), quand cette distinction existe, y avoir encore un langage objet décrivant la sémantique dynamique (c’est à dire la logique / le sens de l’execution du programme). C’est un autre langage objet, décrivant pourtant le même langage concret, mais décrivant un autre de ces aspects. Un exemple imaginaire de sémantique dynamique, pourrait être « C ⊢ V <-- expression ∴ C ⊢ V initialisée », pour exprimer le fait qu’une variable dans laquelle on a gardé le résultat d’une expression, peut être considérée comme initialisée, ce qui est une distinction importante, comme une variable à laquelle aucune valeur n’a été donnée, n’a à priori pas de sens dans le cas où on voudrait lire son contenu, mais ça ne change rien quand on veut l’écrire, qu’elle ait été initialisée avant ou pas. Il pourrait aussi dire « C ⊢ v1 initialisée ∴ v2 <-- f(v1) », pour dire que si une variable a été initialisée, on peut utiliser cette variable comme paramètre d’une fonction, sous entendu que c’est invalide si elle n’a pas été initialisée. Mais comme le programme tourne, le jugement que cette expression est invalide, s’exprimera plutôt sous la forme d’un arrêt du programme avec un message d’erreur, plutôt que comme un arrêt de la compilation du programme avec un message d’erreur aussi. Je parle de message d’erreur, mais ça peut être signalé d’autres manières, il ne sera pas question de ces détails.

Attention aux symboles : le symbole de la disjonction ressemble beaucoup à la lettre v, dans le précédent paragraphe, c’est bien de la lettre v qu’il s’agit, pas du symbole de la disjonction.

Pourquoi est‑il appelé ici, langage objet ? Ben, parce qu’il est l’objet du discours qu’en fait le système de déduction. Dans un autre contexte, le langage objet pourrait aussi bien être la syntaxe abstraite, si elle était l’objet d’un discours (discours d’un système de déduction ou autre). le langage objet, comme il est appelé ici, pourrait aussi bien être appelé le langage de la sémantique. Mais comme les systèmes de déduction ont des usages assez généraux, il est de coutume de parler de langage objet pour désigner le sujet de leur discours, pour être plus neutre.

Cette distinction entre le langage de programmation et le langage objet donnant sa signification au langage de programmation, étant posée, il est possible de revenir aux questions de logique, celle du langage objet (même quand il y en a plusieurs, je parle au singulier, pour simplifier) et celle du système de déduction.

On peut se dire, après les exemples précédents, que la logique décrite par le langage objet, ne doit pas être prise à la légère. Quand le langage objet dit qu’une opération est valide, cette règle s’applique pour chaque cas où cette opération apparaît. Si cette opération apparaît un millier de fois dans le texte d’un programme, il n’y aura toujours qu’une seule règle de validation pour l’opération en question, mais appliquée un millier de fois, sans faire de cas particulier. Le règle doit donc être pensée de manière à être valide dans tous les cas où elle doit s’appliquer. Mais si un programme peut être bogué à cause d’une erreur de raisonnement, de supposition erronée, faute d’avoir pensé à tout, n’est‑il pas envisageable que ce même genre d’erreur ait été introduite dans un langage objet décrivant la sémantique d’un langage concret ? La réponse est oui. C’est la raison pour laquelle la logique décrivant la sémantique du programme, doit elle‑même être validée, avec une logique plus concise (la logique, pas les preuves), et c’est sa concision qui fait qu’il y a moins de risque d’erreur de la part de cet autre logique, qu’elle peut avoir été validée humainement, par des mathématiciens, philosophes, scientifiques et autres, et avoir été mise à l’épreuve dans des domaines variées, avoir vu ses propriétés minutieusement étudiées.

Cette autre logique, c’est celle du système de déduction. Qu’il s’agisse de s’assurer de la cohérence de la logique formulée par un langage décrivant la sémantique d’un langage concret ou de la cohérence d’un programme vis à vis de la formulation de ce qu’il est censée faire ou ne pas faire, le principe est le même : s’assurer que les affirmations ne peuvent que être vraies dans tous les cas sous les conditions définies. Il ne s’agit plus de sémantique au sens ou on l’entend au sens large, mais de cohérence et de tautologie en générale ou sous les hypothèses d’un contexte. C’est le seul propos de ces logiques, raisons pour laquelle elles disposent de moins de règles que la logique d’un langage de programmation par exemple. Leur rôle est de distinguer le vrai du faux, le possible de l’impossible.

En plus de pouvoir avoir soit la qualité d’être sound ou complete, au choix, une logique peut être plus ou moins tatillonne avec la signification de ce qu’est une preuve.

Se distinguent d’abord deux importantes classes de système de déduction : ceux appliquant la logique classique et ceux appliquant la logique intuitionniste ou dite constructiviste.

La logique classique, c’est celle que la plupart des gens connaissent, c’est celle qui est parfois confondue avec l’algèbre de Bool, tellement les deux semblent avoir la même interprétation du vrai et du faux. Elle fonctionne bien, mais il lui est parfois reproché de ne pas être assez terre à terre, de se contenter d’être convaincante sans toujours faire la preuve pratique de ce qu’elle affirme. Plus précisément, ce qui lui est reproché, c’est de se contenter de chose comme ça : non non A ==> A. Cette expression peut se lire comme « il est faut d’affirmer que A est faux, donc A est vrai ». Ce n’est pas incohérent, mais ça peut laisser sur sa faim : pourquoi donc prendre ce détour pour démontrer que A est vrai ? Ne pourrait‑on démontrer que A est vrai tout‑court ?

C’est le propos de la logique intuitionniste. Pour cette logique, le type de démonstration appelé preuve par contradiction, n’est pas acceptable. Cette logique suppose que si A est vrai, ça doit pouvoir se démontrer directement et que aucune autre démonstration n’en est accepter autre que sous cette forme positive. Une nuance sémantique explique la différence de point de vue. Pour cette logique, A est vrai, signifie A existe ou A est réalisable, selon les cas. C’est cette nuance sémantique qui fait que la logique intuitionniste est parfois qualifiée de constructiviste. Au regard des exigences de la logique constructiviste, la logique classique aurait l’air plus intéressée par la rhétorique que par la réalité.

Note : bien que la logique intuitionniste n’inclut pas la possibilité de démontrer par l’absurde, l’existence d’une chose, elle inclut quand‑même la possibilité de démontrer par l’absurde, qu’une chose ne peut pas se produire. Ça peut faire une différence importante en informatique, quand il faut couvrir un ensemble de cas possibles et qu’un de ces cas ne peut en fait jamais se produire, qu’il faut justement le montrer, pour ne pas se retrouver à devoir faire une démonstration sous une hypothèse impossible, celle d’un cas impossible, qui pourrait être une impasse et amener à l’échec de toute une démonstration.

Mais la logique intuitionniste n’est pas moins mise en cause. Une troisième classe de logique reste pantois devant cette formule : ⊥ ⊢ A, généralement évoquée comme, « de l’absurde, on peut tout conclure ». Là aussi, ça semble cohérent dans un sens, si on considère que l’absurde ne se produit en principe pas et que si l’impossible est arrivé, alors tout peut arriver. Mais cette logique voit ça avec autant de suspicion qui si au bas d’un contrat elle lisait « Si un matin la Lune est carrée, vous nous devrez mille bouteilles de champagnes  », elle se dit, « c’est en principe impossible, mais si ça arrivait, je gère ça comment ? » Cette logique, c’est la logique minimale (il me semble qu’il en existe plusieurs dans cette catégorie).

Note : on peut dire que la logique minimale a une immunité naturelle contre les éventuelles incohérences de l’objet de son discours, par lequel elle ne se laisse pas contaminer.

On peut remarquer que la logique intuitionniste et la logique minimale, rejette mécaniquement une interprétation de la négation (la proposition ⊥ se dérivant souvent de “A et non A”). La négation d’une proposition, ça ne semble pas poser de problème si on tient le vrai et le faux comme ne prêtant pas plus à conséquence que dans l’algèbre de Bool, mais si on tient les propositions comme des discours sur les choses, on peut se dire que la négation d’une proposition, ça n’est pas si anodin que de faire la soustraction 1 - 1, que la négation peut peut‑être avoir un sens avec certaines propositions, mais pas avec toutes.

Il y a encore plus tatillon.

Si on vous dit, « Les vaches sont bleue, donc l’herbe est verte », il y a de quoi sourciller, mais ça ne prête pas à conséquence, en tous cas bien moins qu’une démonstration par l’absurde ou l’idée d’accepter que quelqu’un vous conclut tout de l’impossible. Ici, la conclusion est vraie, mais c’est la dérivation qui est douteuse. Ce n’est même pas que les vaches ne sont pas bleues, le problème c’est : quel rapport peut‑il bien y avoir entre la couleur des vaches et la couleur de l’herbe ? Rien ne lie les deux, donc l’affirmation ne peu que être vrai, quoi qu’on pose comme condition à l’implication, mais quand‑même, pourquoi la formuler ? Cette catégorie de logique, c’est la logique de la pertinence, ou relevant logics. Il en existe plusieurs variantes, certaines sont des logiques minimales (la catégorie précédemment présentée), mais pas toutes. L’exigence de cette classe de logique est un peu plus technique à formuler. Disons qu’elles exigent que la conclusion d’une implication et sa condition, aient un terme en commun, rendant la conclusion forcément dépendante de la prémisse. En terme encore plus technique, on dit que la conclusion et la prémisse doivent avoir au moins une variable libre en commun. Il faut voir du côté du lambda calcul pour comprendre le sens de cette phrase, et ce ne sera pas le sujet ici.

Les logiques intuitionnistes retirent une règle à la logique classique, et les logiques minimales, retirent à leur tour une règle à la logique intuitionniste, ce qui fait parfois dire qu’elles sont dans une relation d’inclusion, que la logique classique inclue la logique intuitionniste(s) qui elle‑même inclue la logique minimale(s). Cette vision des choses est apparemment mise en doute par un document dont je ne comprends pas les démonstrations dans une formulation que je ne connais pas, mais qui me semble à garder. Le document en question veut montrer que ces logiques traitent la négation de manière assez différente pour que la relation d’inclusion ne soit pas une bonne image : Separating Minimal, Intuitionist and Classical Logic (projecteuclid.org) [PDF], David Meredith, 1983.

Interprétations et raisons.

La raison d’avoir fait ce cours exposé sur ces catégories de logiques, est de montrer que les logiques ne viennent pas nul‑part, elle ne sont pas ésotériques, elles proviennent de la philosophie, de l’interrogation sur le sens que ça a de dire qu’une chose est vraie ou qu’une chose est fausse. Pour l’intuitionnisme, la différence entre le vrai et le faux se base sur les faits, il ne suffit pas qu’une démonstration soit convaincante pour dire la vérité sur une chose, elle considère que dire la vérité, c’est dire ce qui est et ce qui n’est pas ou ne peut pas être, distinguer le réalisable du non–réalisable. La logique minimale se méfie qu’une clause qu’elle dangereusement explosive ne se puisse réaliser et la logique de la pertinence, ne valide pas les affirmations gratuites même si leur conclusion est vraie.

La porte d’entrée dans la logique des démonstration, est là (et dans les séquents), pas besoin de se noyer dans des documents trop spécialisés. C’est juste un peu simplifié, l’exclusion de certaines règles pouvant se faire en mode « soit l’une, soit l’autre », pas nécessairement comme je l’ai résumé, la nuance me semblant surtout importante avec la logique minimale et la logique de la pertinence. Quelques recherches peuvent permettre d’en savoir plus.

Plus on retire de règles d’inférence à une logique d’un système de déduction, plus ses jugement seront à priori solidement fondés, mais plus il ne pourra pas juger digne de confiance ce qui n’est suspect qu’en apparence, et même s’il y concède, plus faire les démonstrations de la vérité pourra être difficile à mener à bien.

Il ne faut pas interpréter trop rapidement ce qui a été dit, surtout sous l’éclairage du résumé ci‑dessus. Le choix d’une logique est a évaluer selon le sens qu’on donne aux formules du langage objet, selon l’interprétation du vrai et du faux, de la vérité et de la fausseté, pour ce langage objet toujours, aussi selon ce à quoi le langage objet s’applique et dont doit normalement être dérivé l’interprétation du vrai et du faux (définir le modèle de cette logique, peut aider). J’ai à priori une préférence personnelle selon deux cas, mais garde personnelles ces préférences et leurs raisons.

Une dernière chose à souligner : la distinction entre la logique d’un langage et celle servant à faire des démonstrations sur ce langage. La logique des démonstrations peut permettre de s’assurer de la cohérence de l’autre, juste sous la condition que cette notion de cohérence ait été formulée. Les exigences envers l’une et l’autre ne sont pas les mêmes.


Voilà, c’est fini

 — Heu … c’est tout ? J’espérais une solution aux affreux problèmes racontés précédemment
 — Ben, toute la matière première est là : des pistes de cadre expressifs décrire le sens d’un programme, un présentation courte mais suffisante sur les différents niveaux de langage, leurs rôles et relations entre eux, et le pompom qui permet se s’assurer que tout tient debout, que ce soit la sémantique d’un langage ou la sémantique d’un programme : des pistes sur comment choisir la logique d’un système de déduction et précédemment des pistes sur l’interprétation des séquents dans un système de déduction.
 — Okay, … ben je peux dormir alors, … la nuit porte conseil.
 — (en réalité il y avait encore des choses à dire à propos du choix, pour un langage de programmation, du modèle de la sémantique dynamique, fonctionnel vs impératifs, un choix qui ne doit pas nécessairement être celui qu’on croit, mais je viens juste de le mentionner en collant un doute, alors c’est comme si je l’avais dit ; j’aurais aussi dut parler de la différence entre les preuves sur un langage et les preuves sur un programme dans ce langage, mais il est possible de deviner le chemin entre les deux ; si j’avais le temps j’aurais encore aussi parlé de  … bon, stop)


Quelques liens intéressants sur la théorie des catégories, des descriptions de certaines logique et un lien sur la logique linéaire qui n’a été que évoquée et pas abordée (parce que je ne saurais pas en parler et que je vais préférer faire sans pour diverses raisons). Certains de ces liens ont put être déjà mentionnés dans ce sujet (au moins un).

• Introduction to sequent calculus (jku.at) [PDF], Todor Jebelean, 2019, pour le principe de base des démonstrations.
• nLab (ncatlab.org), sur les catégories et plusieurs logiques.
• LLWiki (ens-lyon.fr), sur la logique linéaire.
• Mathematical Structures (chapman.edu), par curiosité et au cas où.
• AbstractMath (abstractmath.org), sur les catégories, pour des idées.
• A structural approach to operational semantics (umich.edu) [PDF], Plotkin, 1981, à garder.
• Natural semantics (inria.fr) [PDF], Kahn, 1987, à garder.

L’équivalence est une égalité sous une abstraction. Deux choses équivalentes sont égales dans certains contextes.

La conclusion d’une implication est‑elle en fait un contexte et n’est‑il pas souvent plus pertinent de lire l’implication en sens inverse ?

La définition classique de l’implication, A ==> B est que si on a A, alors on a toujours B, mais qu’on peut avoir B sans avoir A.

On peut déjà remarquer que dans cette définition, B est plus permanent que A, ce qui fait qu’il n’est pas insensé d’en parler comme d’un contexte.

Si A est la présence d’une vache est que B est l’existence d’une prairie, alors il n’est certes pas insensé de dire A ==> B (on peut voir la prairie sans la vache mais pas la vache sans la prairie), et peut‑être plus encore serait‑il souvent plus pertinent de dire que A est une possibilité dans B.

Une autre chose me perturbant encore plus souvent avec l’implication, est la non‑distinction entre conséquence et causalité (et ce n’est pas tout, il reste une autre tracasserie pour après). Quand on a A ==> B, a‑t‑on une cause ou une causalité ? La formulation a‑t‑elle même un intérêt quelconque si elle ne permet pas de distinguer les deux ? Ou la formulation est‑elle sous une ignorance implicite ? On voit là comment la logique et la philosophie se rejoignent (la première provient en effet de la seconde), et que la philosophie (la vraie), ce n’est pas de la rhétorique.

Il reste encore autre chose.

Si A est la présence de farine et d’eau, que B est la présence de pain, on peut dire A ==> B aussi, comme on peut avoir du pain sans avoir de farine et d’eau, mais que si on a de la farine et de l’eau, on est sûr d’avoir du pain … Ou pas ? Parce qu’il faut encore le faire, ce pain, et peut‑être n’en avons nous simplement pas envie ou pas besoin.

Dans ce cas là, A ==> B n’est ni une relation de causalité ni une relation de corrélation, elle est une relation de nécessité, une condition. Une condition ? Mais pourtant dans l’analogie du contexte proposée plus haut, c’est B qui serait le contexte et l’idée de nécessité renvoie plutôt à l’idée d’un contexte remplissant les conditions de la nécessité ; et plus difficile encore de voir le pain comme un contexte dans lequel la présence d’un sac de farine et d’une bouteille d’eau serait une possibilité, plutôt à l’opposé, la présence d’un sac de farine est d’une bouteille d’eau, serait un contexte dans lequel la future présence d’un pain serait une possibilité.

Cette dernière relation, qui est en fait celle d’une fonction, ne correspond pas du tout au précédentes manières de voir cette relation, elle est la plus éloignée de l’idée courante d’implication, et pourtant, la relation définie par une fonction est souvent décrite comme celle d’une implication, la remarque semble alors s’égarer, mais ce n’est pas une surprise quand un mot mélange tout. D’où viennent les arguments d’une fonction, si ce n’est pas d’un contexte ? Des arguments qui peuvent d’ailleurs provenir des résultats d’autres fonctions et devenir des arguments d’autres fonctions. Cette relation est en fait celle du maillon d’une chaîne, d’où la confusion a essayer de distinguer les deux côtés : les deux côtés sont des contextes. Dans les descriptions des paragraphes précédentes, cette idée de chaîne ressort moins ou alors cette chaîne serait très courte.

Bref, aussi problématique que la notion de négation, la notion d’implication mélange tout, il faudrait toujours être plus précis que ça, en distinguant au moins ces cas :

• N’a‑t‑on pas plutôt à faire à une relation dans l’autre sens, c’est à dire celle d’une prémisse qui serait en fait une possibilité et la conclusion en fait un contexte ?
• La conclusion est‑elle dépendante de la prémisse ? Est‑ce en fait un maillon dans une chaîne de nécessités ?
• La conclusion est‑elle une conséquence automatique de la prémisse ?
• Est‑on dans une ignorance faisant qu’on ne peut relever la relation que comme une corrélation faute d’en savoir plus ?

Pour distinguer les deux dernières puis éventuellement les trois dernières : les deux côtés de la relation sont‑t‑ils simultanés ou pas ? Est‑il pertinent de voir comme un contexte ou une nécessité, l’un des deux côtés ? Ou plus encore, les deux côtés ?

Personnellement, je restes surtout sur l’impression de la première phrase : souvent, la relation d’implication se lit mieux de la droite vers la gauche que de la gauche vers la droite (dans le sens opposé de la flèche quand‑même !).

Possible que la question soit semblable à celle d’aller du particulier au général vs aller du général au particulier.

La relation qu’il y a entre les deux côtés d’une implication, évoque la question des logiques de la pertinence (je traduis “ relevance logics ”). Comme dit précédemment, dans ces logiques, la conclusion de l’implication doit obligatoirement être « physiquement » liée à la prémisse (par au moins une variable qu’elles ont effectivement en commun, pas juste une variable homonyme).

Cette relation me fait penser à une contrainte d’intégrité que je me définis souvent : pour un certain terme, il n’est pas suffisant d’être d’un certain type, il doit aussi être dérivé d’un certain autre terme. Par exemple si y est le résultat d’une fonction f, y = f(x) alors un exemple serait quand z = g(x, y) n’a de sens que si les deux x sont les mêmes (ou parfois le second x, produit d’une certaine dérivation du premier x). Je le schématise, donner des examples concrets ne ferait que noyer le propos. Ces derniers jours je me faisais remarquer que ça se présente quand‑même assez souvent et je me demandais si ça ne serait pas quand‑même un exemple d’application utile des types dépendants dont je n’ai pas dit du bien. Peut‑être serait‑il possible de dire que le type de y est contraint par le terme x.

Mais ça soulève une question et pose un problème. La question serait : pourquoi ce type d’exemple n’est jamais donné et n’ais‑je vu que des exemples à base de listes et de vecteurs ? C’est bizarre de ne donner que des exemples qui ont un intérêt si limité et de ne pas donner cet exemple qui serait bien plus généralement intéressant. Le problème est : un terme apparaissant dans un type ne peut pas être un terme apparaissant en argument d’une fonction, on ne peut pas injecter des notions de la sémantique dynamique dans la sémantique statique, la première repose sur la seconde mais la seconde ne peut pas reposer sur la première. Quand un type dépendant est contraint par une valeur, c’est par une valeur qui n’est pas d’un type mais d’un kind (dans la terminologie HOL) ou sort (dans la terminologie du calcul des constructions). Ça complique déjà la formulation, et en effet, avec les types dépendants, on a en pratique souvent des termes en double, l’un dans le statique et l’autre dans le dynamique, une redondance qui finit par lasser et ne pas faciliter la lecture. De plus, un document sur le calcul des constructions, semblait lui‑même dire que les types dépendants pour représenter des choses au delà du trivial, ça devient vite compliqué.

Mais cette relation peut s’exprimer avec une logique sans nécessiter les types dépendants, et la solution que je vois  (non‑donnée ici) me semble plus commode. Surtout que, pour bifurquer un instant, je vois d’autres relations dans la même catégorie qui renverraient plutôt à la logique linéaire (pour le très peu que j’en connais) qui est encore différente et d’ailleurs même une autre, étrangère à la logique linéaire pour ce que j’en sais. Je crois de plus, que pour la logique appliquée à l’informatique, il n’y a pas nécessairement besoin de la logique linéaire mais seulement d’un petit fragment de celle‑ci. En fait, j’avais réinventé ce fragment il y a longtemps et en qualifiant des types de linéaires (le mot me semblait tellement évident) puis en cherchant si des gens y avaient pensé, j’ai découvert l’existence de cette logique … seulement je trouve que réinventer les choses ça peut ne pas être si mauvais que des gens le font croire, quand ça permet de mieux fonder, mieux aborder et simplifier à l’essentiel. Possible qu’il en soit de même pour les types dépendants avec cette relation décrite plus haut, qui me semble essentielle mais tout autant ne pas nécessiter les types dépendants.

Précédemment avait été abordée la question des logiques sound vs les logiques complete.

La même distinction peut être faite avec les représentations. Une représentation d’une chose réelle (qui peut elle‑même être abstraite), peut permettre des formulations qui ne représentent aucune de ces choses réelles. C’est assez comparable à ce que fait une logique unsound en faisant passer pour réelle une proposition qui n’est pas. En posant une représentation, ce qui peut être même en définissant un type, il faut se poser la question des cas semblant particuliers et voir si oui ou non leur représentation a un sens ; si certains de ces cas représenteraient juste des choses sans intérêt mais pas insensées et que les inclure permet de ramener une représentation à une autre représentation plus générale, ça peut aller à mon avis, mais il revient à chaque personne d’évaluer la situation personnellement.

Il y a quelques semaines, j’avais vu passer quelques mots à propos d’une syntaxe (une syntaxe, c’est une représentation) incomplete pour une logique, c’est à dire une syntaxe qui ne permet pas de représenter tout ce qu’il serait pourtant valide de représenter. Là aussi, c’est similaire à une logique incomplete, qui ne permet pas de dire tous ce qui est vrai d’une chose réelle, excepté que dans le cas d’une représentation, c’est ne pas pouvoir tout représenter.

Moins intéressant mais aussi important, est le fait qu’une représentation, comme une conclusion logique, peut n’être valable que dans un contexte ou ne pas signifier la même chose dans des contextes différents. Là aussi, c’est un point commun avec les logiques. Un exemple trivial peut être les variables homonymes mais différentes ou la définition d’un type qui ne peut se faire que dans un contexte où les autres types auxquels il se réfère, ont été définis.

Je vois personnellement une autre relation entre représentation et logique : je crois qu’une logique qui ne repose pas sur une représentation directe, est soit peu commode, soit possiblement (ça dépend des domaines) pas assez digne de confiance.

Elle peut correspondre à la conception habituelle de l’implication, mais seulement en surface. Ce qui suit est d’abord en oubliant volontairement de prendre une fonction pour son type seulement, en la voyant comme ayant un type plutôt que comme étant un type. Si on considère que étant donné une fonction t1 -> t2, t2 peut provenir d’autres fonctions, alors ce t2 peut être sans que t1 ne soit. Mais cette instance d’un t2 ne vient pas de nul part. Avant d’aller plus loin, il y a une distinction à faire entre les fonctions : les constructeurs de valeur et les fonctions renvoyant une valeur issue d’un de ces constructeurs. Si la fonction est une fonction au sens le plus courant, une fonction du deuxième cas, ça n’a pas d’intérêt de dire que la valeur qu’elle renvoie peut exister sans l’application de cette fonction, sinon pourquoi cette fonction serait‑elle définie si ce qu’elle renvoi est supposée pouvoir exister sans même qu’elle ne soit définie. De plus, cette fonction au sens courant, ne crée pas elle‑même la valeur qu’elle renvoie, elle renvoi une valeur crée par un autre type de fonction (souvent implicite dans beaucoup de langages), qui crée une valeur du type (un constructeur de valeur, à ne pas confondre avec un constructeur de type). Et là encore, ça n’a pas de sens de dire que le résultat peut être sans ce constructeur. Même si le type a plusieurs constructeurs, comme c’est souvent le cas, certaines des valeurs qu’il crée sont typiquement uniques, un ou des équivalents du zéro servant d’élément de base. Là aussi, ça n’a même pas de sens de dire que la valeur peut exister sans (précédemment, pas d’intérêt, là, pas de sens), et ça a même encore moins de sens quand le constructeur crée quelque chose à partir de rien (en théorie), comme c’est le cas de tout ceux qui crée des éléments initiaux.

Si une fonction est prise pour son type, ça a déjà plus de sens, mais c’est alors un type qui dit peu de choses, tellement abstrait que en effet tout ce qui pose problème comme décrit plus haut ne se voit plus. Dans ce cas, oui, t1 -> t2 dit qu’un terme de type t2 peut exister sans qu’un terme de type t1 n’existe, mais t1 -> t2 ne dit rien, c’est juste un minimum pour construire des expressions, sans encore leur donner un sens, on ne peut pas en tirer de conclusion autre que de dire que telle ou telle expression est valide, qu’on peut avoir une expression t2 sans nécessairement une expression t1 mais que si on a une expression t1 alors on peut toujours avoir une expression t2. Mais c’est peu pour faire des conclusions intéressantes, alors que l’implication est normalement plus prometteuse pour un raisonnement.

Les fonctions au sens courant, sont plus des relations tout‑court, difficilement des implications A ==> B où B peut être sans que A ne soit. La relation qu’est une fonction, est quand‑même le plus souvent orientée, elle ne peut généralement pas autant se lire dans les deux sens.

Ces types, qui s’appellent des types simples, définissent comme une syntax. C’est là leur intérêt mais aussi leur limite. C’est leur intérêt, parce qu’ils garantissent que au moins les termes ne sont pas n’importe quel assemblage de n’importe quoi. C’est leur limite, par le principe connu que toute phrase syntaxiquement correcte n’a pas nécessairement du sens.

L’intérêt et la limite des types simples, pourrait expliquer pourquoi les types plus complexes sont inadaptés. Ils jouent aussi ce rôle des types simples mais voulant définir une grammaire garantissant que le sens est correcte. Intuitivement, on peut comprendre qu’une grammaire garantissant que les phrases écrites avec cette grammaire sont toujours sensées, ne peut que être une grammaire excessivement compliquée à l’usage. On procède plutôt autrement : on voit d’abord si c’est grammaticalement correcte, puis ensuite on s’intéresse au sens, ce qui doit encore être précisé.

Je crois que ces remarques s’appliquent même à l’idée de “ proposition as type ”. En marge et à ce propos, le typage simple ne doit pas être confondu avec le typage à la Pascal, qui est encore différent. Ce typage là, fonctionne un peu comme si tous les types étaient abstraits, ce qui me semble être une tentative simpliste d’avoir un type en temps que proposition.

Une autre solution peut se comprendre intuitivement et est déjà concrétisée par la solution trop partielle qu’apportent les types simples : les types simples sont comme une grammaire sur une grammaire, implicitement sous la condition que les termes soient d’abord syntaxiquement correctes tout‑court. C’est une couche sur une autre, un langage dans les termes d’un autre langage.

Cette solution pourrait être poursuivie avec des couches supplémentaires, comme une couche au dessus des types, qui garantie que toutes les fonctions se terminent et qui vérifieraient d’autres choses éventuellement aussi. Ça ne serait toujours pas suffisant pour garantir le sens (qui doit encore être formulé, un problème à lui tout‑seul), mais ce serait déjà un progrès et une couche encore au dessus pourrait être définie, toujours sous l’hypothèse que la couche précédente a été validée.

Justement en parlant de fonctions qui se terminent, un typage qui s’appel Système F est connue pour garantir, par son seul système de typage, que toutes les fonctions dont le type est valide, se terminent, mais ce typage est aussi réputé inutilisable en pratique. Il est possible de sentir que c’est une illustration du problème précédent, celui de vouloir tout traiter simultanément.

Chaque couche pourrait nécessiter des démonstrations d’ailleurs, la validation ne serait pas nécessairement calculable (*) comme l’est l’inférence des types avec les types simples. Et justement, avoir des démonstrations séparées par couche, on peut intuitivement comprendre que ça faciliterait les démonstrations elles‑mêmes : il ne peut que être plus commode de démontrer qu’une fonction se termine (et démontrer ou être sous l’hypothèse de, tout ce qui est nécessaire à cette démonstration), puis ensuite, quand cette démonstration a été faite pour toutes les fonctions, démontrer que cette fonction a une autre caractéristique, que de démontrer cette caractéristique tout en démontrant en même temps qu’elle se termine parce que les deux propriétés sont fusionnées en une seule.

Concernant la relation entre types et propositions, je crois plutôt aux propositions à côté des types ou au dessus des types, comme suggéré plus haut.

Pour ce que j’en ai lu, le calcul des constructions défini comme des couches de langages les unes au dessus des autres, mais ses fondements me semblent bien trop complexes pour en faire une solution abordable (je suppose implicitement que les fondements doivent pouvoir être présentés et compris par des gens avec seulement un sérieux intérêt pour les principes mais n’ayant pas fait NN années d’études spécialisées). De plus, le calcul des constructions repose sur une théorie des types dépendants ce qui amène tous les problèmes pratiques qui viennent avec (dans les maths, c’est autre chose, mais le sujet ici est la logique appliquée à l’informatique).

Note en marge : j’avais oublié de dire que j’ai lu il y a longtemps, que l’égalité n’est même pas certainement définie, avec les types dépendants ; je ne sais plus si c’était qu’elle n’est pas calculable ou que les avis divergent sur la définition de l’égalité. Quoiqu’il en soit, une logique qui a un problème avec l’égalité, si essentielle, me donne un doute sur sa praticité.


(*) On a besoin de faire des démonstrations, quand il n’existe pas de méthode de vérification dont il est garanti qu’elle se termine … et en pratique, qui devrait se terminer dans un temps raisonnable et avec une consommation de mémoire qui ne dépasse pas celle disponible.

À ce propos, et comme précédemment a été mentionné le principe de base de Prolog, et qu’il était dit ceci dans « Les références partielles (d’ISO Prolog) » :


Même pour résoudre des problèmes, on se retrouve facilement avec des exécutions qui ne vont pas nécessairement se terminer. Le problème de la récursivité en Prolog (ou Prolog‑like) est connu, mais je voulais juste dire que la récursivité infinie, elle mord vite. À moins que les termes d’une requête soient constants ou toutes les variables soient liées, on est jamais sûr que ça se termine. Plus que dire que Prolog permet de résoudre des problèmes, il faudrait dire qu’il ne garanti que de vérifier des solutions trouvées à des problèmes. En fait, il tient plus du système de démonstration que du solveur. En temps que système de démonstration, il ne connait pas la négation … à noter, comme le problème de la signification de la négation a été mentionné.

En marge, c’est un interpréteur Prolog maison, qui sera le sujet de la première tentative en pratique, de démonstration des propriétés d’un logiciel. Je ne rapporterai pas de détails, mais je dirai quand‑même si ça aura réussi ou pas (probablement pour dans longtemps). Pour l’instant, je ne sais encore même pas comment les choses vont être représentées, formulées, ni même si justement il sera nécessaire de définir une notion de négation ou s’il sera possible de faire sans.

Quand je dis que je ne rapporterai pas de détails, je rapporterai quand‑même des notes pouvant avoir un intérêt en général pour ce sujet.

En me posant la question d’une possible notation pour cette vue de l’implication et me disant que permuter A et B et utiliser une flèche dans l’autre sens ne serait pas particulièrement lisible car perturbant, j’ai pensé au mot “ in ”, quelque chose comme “ A in B ”. Ça n’est pas parfait, parce que l’occurrence de A dans le contexte B n’est qu’une possibilité, pas une certitude. Mais ce qui intéressant c’est que ça évoque l’implication du point de vue ensembliste, ou A ==> B peut se lire comme l’ensemble A est inclus dans l’ensemble B (*).

Il y a autre chose. Une dérivation signifiant que A est une possibilité dans B, serait une dérivation à partir d’au moins un des éléments d’une disjonction représentant le contexte B. Je ne sais pas si les logiques mentionnées il y a une dizaine de jours supporte ce cas ou pas, c’est à vérifier, mais je le trouve assez intéressant pour l’inclure si ça ne l’est pas (même si ça n’est pas supporté explicitement, j’espère que ça se dérive).

Il y a alors au moins trois types de dérivations remarquables : 

• À partir de tous les éléments d’une conjonction.
• À partir de chacun des éléments d’une disjonction.
• À partir d’au moins un des éléments d’une disjonction.

Ça peut faire se demander si le cas qui ne figure pas dans cette liste, celui d’une dérivation à partir d’au moins un des éléments d’une conjonction, n’a juste pas été remarqué ou s’il n’est jamais intéressant. On pourrait se dire que ce ne serait alors plus une conjonction et je penche donc pour la seconde option ; mais question analyse de formules, ça peut être différent.

À partir de l’idée de démontrer que A est une possibilité dans B avec une dérivation à partir d’un des éléments d’une disjonction représentant B, on peut même se dire que lire A ==> B comme A est une possibilité dans B, est non‑seulement souvent plus intuitivement lisible, mais aussi plus sensé, parce que ça signifie que A ==> B a vraiment de la pertinence, dans le sens que A est vraiment possible. En effet, dans A ==> B, rien n’implique que A soit vraiment possible et comme mentionné précédemment, certaines logiques n’aiment pas ça (moi non‑plus).


(*) Une malheureuse notation rapportée en début d’année, utilise le symbole de l’inclusion ensembliste dans le sens opposé, en écrivant A ⊃ B au lieu de A ⊂ B ; mais inutile de se lamenter encore sur ça.

Plusieurs choses mêlées en partant de ça, et il ne faut pas que ça ressemble à de la salade trop retournée. Le message suivant celui‑ci sera plus intéressant, mais celui‑ci n’est pas sans intérêt quand‑même.

Pour commencer, la précédente citation aurait put inspirer un doute du genre « mais si dans A ==> B, rien ne garanti que A est vraiment possible, n’en est‑il en conséquence pas de même de B ? ». Oui en général, mais non dans l’image proposée en particulier. Il a été proposé de tenir B pour un contexte, et ici, un contexte, est à comprendre dans le même sens que celui des séquents. En fait, en plus de proposer de parfois lire l’implication en sens inverse du sens habituel, il y avait aussi une suggestion implicite et involontaire à préférer les implications non‑hypothétiques.

C’est à partir de là que ça va partir dans plusieurs directions, mais ça peut se résumer en trois gros points.

Il y a longtemps, environ deux ou trois ans de ça, avait été dit que la différence entre l’implication et le séquent (qui a ce moment là n’était encore qu’un incompréhensible symbole ésotérique semblant important), était que l’implication appartiendrait au langage objet et le séquent au langage des démonstrations. C’était à moitié faux. L’implication n’appartient pas plus à la déduction qu’au langage objet. En fait, tous les connecteurs du langage objet, quelqu’ils soient, n’ont rien de particulier, y compris l’éventuel connecteur d’implication que pourrait avoir un langage objet. L’implication apparaît bien dans plusieurs règle des logiques de démonstrations. La seule différence entre le séquent est l’implication, n’est pas là, elle est que à gauche de l’implication, on a des hypothèses, et comme déjà trop répété, à gauche des séquents, on a des faits. La seule différence tient dans ce point, le raisonnement hypothétique, qui est une exclusivité de l’implication. Mais si un langage objet dispose d’un connecteur pour l’implication, il est alors nécessaire (vraiment nécessaire, ce n’est pas une simple commodité) que son symbole se distingue de celui utilisé pour l’implication dans la logique des démonstrations. C’est probablement la raison pour laquelle on voit l’implication tantôt écrite avec une flèche à hampe double, tantôt écrite avec une flèche à hampe simple. La double hampe est apparemment typique des démonstrations et la hampe simple, typique des langages objets. C’était une bourde, qui est donc maintenant corrigée, avec une précision en plus. À ne pas oublier : dans tous les cas, la logique des démonstrations n’interprète pas l’éventuel connecteur d’implication du langage objet, il n’est pour elle qu’un connecteur parmi les autres, et si elle l’interprète, ce n’est qu’indirectement à travers les séquents à son propos.

Un détail qui pourrait perturber : il est possible qu’il soit difficile de comprendre la différence entre un fait et une hypothèse, comme les faits de la logique ne sont pas nécessairement des réalités automatiques, mais peuvent toujours l’être. Voilà justement, la différence est là : « peuvent toujours l’être ». Un séquent a toujours deux origines : soit il est produit par d’autres séquents (dans une conclusion), soit il est posé à comme un des quelques faits généraux toujours vrais. Les séquents posés comme toujours vrais et en général, sont effectivement toujours vrais. Un exemple, serait la sémantique d’un langage qui poserait qu’il existe un nombre qui s’appel zéro, qu’il existe un type s’appellant les entiers naturels, et que ceci est toujours vrai. Tous les autres séquents dériveront, soit de ces séquents toujours vrais, soit d’autres séquent, et transitivement, ils sont donc toujours réalisables. Une hypothèse, elle peut venir de nul‑part, on peut même la poser arbitrairement ; mais ça ne reste toujours qu’une hypothèse, ça signifie pas qu’on peut affirmer n’importe quoi gratuitement. Les raisonnements hypothétiques peuvent quand‑même parfois avoir un intérêt, il ne faut pas croire qu’ils sont à exclure inconditionnellement.

Le retour sur la distinction entre séquent et implication, fait penser à revenir sur les questionnements à propos des fonctions dont il a été dit qu’elles sont difficiles à voir comme des implications. En parlant de séquents, on peut justement plus facilement voir des similitudes entre les séquents et les fonctions, qu’entre les implications et les fonctions. Il avait été relevé que à gauche de la flèche d’une fonction, on a plus qu’une prémisse, un contexte satisfaisant des nécessités ou parfois rien, que à droite de la flèche d’une fonction, on a autant un nouveau contexte qu’une conclusion, que les fonctions produisent des choses à partir de nécessités. Ces caractéristiques évoquent mieux celles des séquents que celles des implications. Comme dit dans un ou deux messages en arrière, en parlant des fonctions, ici, il faut comprendre les fonctions en générale et en pratique — entre autres, pas les fonctions réduites à leur type.

— Édit — Il y a autre chose à ajouter, mais ce sera pour demain.