Les logiques : notes en vrac

Au cas où, même si ça avait peut‑être déjà été dit : la contradiction ne doit pas être confondue avec la multiplicité des solutions. Dire qu’une chose est une solution et qu’une autre chose est aussi une solution, n’est pas la même chose que dire qu’une chose est une solution et dire que cette même chose n’est pas une solution.

C’est trop restrictif à cause d’avoir parlé trop vite : plutôt l’observation ou ce qui est imaginé hypothétiquement. Une règle peut représenter une réalité observable ou une réalité qu’on imagine ou pose comme une hypothèse (qui n’est pas la même chose qu’un terme en hypothèse).

Mais ce qui était dit vaut toujours : si on imagine la négation d’une chose c’est qu’on imagine cette chose.

D’un certain point de vue seulement, parce que telles que formulées là, les deux négations n’appartiennent pas au même monde. L’une est dans la conception du langage en pensée, l’autre fait référence à une notion du langage. Reste qu’y voir une double‑négation n’est pas une idée folle, mais juste une idée.

Les règles négatives sont exclues, pourtant dans certains domaines, des invariants sont souvent exprimés comme des négations, l’exclusion absolue d’une possibilité. De même qu’avec le modus tollens, ce n’est pas exprimable tel‑quel dans le langage, mais peut pourtant y exister indirectement. Pour exprimer un tel invariant, on pourrait vérifier une règle positive dont le corps aurait un seul terme négatif. Ça ne s’exprimerait donc pas comme une définition, mais comme une chose à vérifier par définition, pour un ensemble de règles.

L’idée d’ajouter au langage, une validation d’un ensemble de règles par d’autres règles, avait déjà été présentée (une occasion d’y revenir va se présenter plus tard), c’en serait un autre exemple. Il y aurait des règles signifiant des définitions et des règles signifiant des choses devant être vérifiées dans le contexte vide, dans l’absolu. Ces règles devant être vérifiées seraient listées comme telles, mais ne serait pas séparées des autres règles, puisque par principe, elles seraient cohérentes avec. Existerait‑il des cas pratiques pertinents ou des règles entreraient dans les deux catégories en même temps ?

De retour sur cette négation n’existant que en pensée mais pas dans le langage. Une question est de savoir si cette idée justement, pourrait être rendue exprimable dans le langage. Spontanément, on pourrait se dire que non, que le langage ne peut probablement pas exprimer tous les concepts qui permettent de l’imaginer et de le définir et que cette idée là en fait peut‑être bien partie. Pourtant, peut‑être que si. Cette idée reviendrait à introduire une forme d’introspection dans le langage et l’idée plus haut de formuler des impossibilités par des règles positives que les règles qui sont des définitions, devraient vérifier, y ressemble. Ça signifierait que cette idée de règles validant un ensemble de règles, n’apparaîtrait pas seulement dans les applications du langage, mais aussi dans sa définition.

Ce n’est qu’une idée, mais on ne rencontre peut‑être pas une limite à l’expressivité ici. En parlant de lacune dans l’expressivité du langage, une lacune délicate sera abordée plus tard.

En marge, peut‑être pas très intéressant, mais peut‑être à noter quand‑même. À l’origine, l’idée du langage était de remédier à la trop faible expressivité des types simples. Ces types sont comme des règles de validation des programmes. Dans le langage censé se substituer aux types simples, a fini par être introduit un concept similaire, puis plus haut, il a été envisagé que ce principe pourrait devoir en plus, être mise à l’œuvre dans la définition du langage lui‑même. Il y a peut‑être quelque chose de fondamentale, dans cette sorte d’auto‑vérification.

Pas encore le message annoncé sur une question d’expressivité. C’est à propos de la négation et de choses en rapport, un petit complément sur la cohérence et un début de tentative de définir l’idée de sens, le sens en lui‑même.

Quand il est dit qu’il n’est pas possible de poser des définitions négatives, que la raison est la garantie de la cohérence, il ne faut pas comprendre que le seul fait de poser une définition négative, introduirait toujours une incohérence, qu’elle soit directe ou indirecte. Il faudrait plutôt le démontrer au cas par cas, démontrer pour chaque définition négative ajoutée, que l’ensemble des définitions reste cohérent malgré la règle négative ajoutée. C’est peut‑être possible, mais faute d’avoir une idée de comment s’y prendre, et encore plus faute de savoir comment le faire automatiquement, c’est plutôt exclus pour le moment au moins. La preuve qu’une règle positive est satisfiable est plus facile et peut à priori même toujours être faite automatiquement, à moins qu’elle ne le soit pas, satisfiable. C’est une qualité pratique importante.

Il est possible d’imaginer préserver la même cohérence en posant toujours des règles négatives et en ne permettant pas de poser des règles positives. Mais c’est un problème de pertinence qui se poserait alors, celui évoqué en expliquant la raison de la non‑disponibilité du modus tollens : poser une chose négative, suppose d’une manière son éventuelle existence, ce qui peut faire douter de l’utilité de poser sa non‑existence plutôt que son existence. Mais cette question de la non‑pertinence est moins inquiétante que celle de l’incohérence. Sans voir de raison de le faire, cette possibilité est quand‑même utile à noter, pour ne pas oublier qu’elle est envisageable.

Une exception est peut‑être dans l’idée du sens. Peut‑être que le sens se définit mieux par des choses posées en négatif et trop difficilement par des choses posées en positif. Il est difficile de dire ce qu’est avoir du sens en général, il semble plus facile de caractériser ce qui n’a pas de sens, ça sort plus spontanément. Pour ce début de tentative, trois de ces choses sortant facilement. Ce qui n’a pas d’explication, ce qui est totalement inconnu, c’est à dire indéfinissable, ce qui est incohérent, évoquent immédiatement l’insensé. Ces définition sont toutes négatives, mais définissent un notion elle aussi négative, le non‑sens. L’idée est de définir le sens comme tout ce qui n’est pas du non‑sens.

Un exemple pratique de chose incohérente, serait de voir une casserole d’eau geler en la mettant sur le feu. Une définition de l’incohérence pourrait être « A : B & non B » ou peut‑être même plus simplement « A : non A ». Pour s’assurer de la cohérence du langage, il faudrait démontrer inconditionnellement la règle « soundness : non A ». Deux choses sont à noter. L’utilisation de variables à la place de termes, qui n’est pas que pour illustrer avec des exemples abstraits comme parfois fait, mais qui est nécessaire pour définir une généralité. C’est un exemple de cas où permettre qu’une variable puisse prendre toute la place d’un terme externe, est une nécessité. Rien ne garanti à priori que « soundness : non A » soit démontrable, faute d’avoir une idée de comment s’y prendre, mais rien ne dit que c’est impossible non‑plus. C’est une raison de plus d’introduire une classification des règles, celles‑ci serait à vérifier si possible, mais sans nécessairement l’être. À défaut d’être vérifiée, ces règles seraient une intention écrite formellement. Cette classification des règles inclurait leur possible utilisation ou pas dans les inférences en général.

Un exemple pratique d’indéfinissable, serait d’avoir été témoins d’une chose tellement incompréhensible qu’on ne sait même pas ce qu’on sait alors encore moins comment la décrire. Une définition de l’indéfinissable est plus difficile à imaginer dans l’hypothèse du monde clos (qui signifie que ce qui n’est pas connu d’un système de règles, est supposé ne pas exister). Peut‑être faudrait‑il introduire une constante représentant l’inconnu, mais cette constante ne devrait pas pouvoir être utilisée comme les autres et resterait à définir ses conditions d’utilisation, ces conditions étant une formulation de sa sémantique. Ce n’est qu’une idée vague à clarifier ou peut‑être plus tard à abandonner.

Un exemple pratique de chose sans explication, c’est de voir soudainement apparaître devant soi, une chaussette posée sur la table par exemple, une chaussette posée sur une table n’étant ni une chose incohérente ni une chose indéfinissable, la situation soudainement établie restant quand‑même sans explication. Ce qui n’a pas d’explication est autant difficile à définir que ce qui est indéfinissable, mais n’est pas la même chose, même si ça en a l’air pendant un instant. Il existe déjà des choses sans explications dans le langage, avec les règles inconditionnelles. Ces règles n’évoquent pourtant pas l’insensé, même si on peut les trouver mystérieuses quand on y pense beaucoup. L’insensé pour cause d’absence d’explication, serait plutôt alors, non‑pas ce qui n’a pas de condition ou d’origine connue, mais ce qui est défini comme ayant une condition ou une origine et a pourtant été produit sans utiliser d’inférences. Ça, oui, c’est insensé, tellement que personnellement je ne vois pas comment il serait possible de l’écrire dans les termes du langage, de poser une définition positive ou même négative qui l’impliquerait si elle était vérifiée ou non‑vérifiée. Peut‑être est‑ce une notion qui ne peut exister que dans l’interprétation externe du langage, pas dans le langage lui‑même.

Ou ça existe, mais temporairement. Une hypothèse qui ne sera démontrée qu’à posteriori, est dans ce cas, mais elle devra être démontrée par la suite et alors ne reste pas dans ce cas, raison pour laquelle elle est supposée sensée quand elle est utilisée.

Un autre cas d’une définition de l’insensé, tout autant peut‑être impossible à formuler dans le langage, est la récursion infinie. Ce cas est à la fois similaire et différent d’une chose apparaissant sans raison. Mais est‑ce vraiment de l’insensé ou plutôt de la non‑pertinence ? Ça fait penser qu’il faudrait tenter aussi une définition de la non‑pertinence ; en attendant, en supposant que la récursion infinie est un cas d’insensé, on a jusque maintenant :

• Ce qui est incohérent
• Ce qui est indéfinissable
• Ce qui ne vient de nul‑part
• Ce qui ne va nul‑part

Les deux derniers cas sont sujet à d’autres interprétations. Le troisième cas est parfois acceptable et il est même nécessaire qu’il le soit parfois, et le quatrième cas peut être vu comme insensé pour moitié seulement et comme non‑pertinent pour l’autre moitié. Ça suggère que cette définition de l’insensé par ces cas, devra être révisée.

Il n’est pas suffisant d’évoquer leur limite, il faut l’expliquer. Une introduction à la question peut être de reprendre le cas de l’égalité, plutôt de la non‑égalité, entre des choses de types différents, qui avait déjà été remarquée. Et de plus, en fait, le problème de l’expressivité des types n’est pas spécifique aux types.

Quand on s’exclame qu’on ne peut pas comparer ce qui n’est pas comparable, c’est surtout quand on tient pour égales deux choses non‑comparables, jamais quand on tient pour différentes deux choses non‑comparables. Si deux choses ne sont pas comparables, il n’est pas incohérent de dire qu’elles sont différentes, seulement incohérent d’espérer dire qu’elles sont égales.

Avec les types, l’égalité n’existe qu’entre des choses du même type. Ils ne permettent pas de dire que deux choses non‑comparables sont différentes. Que permettent‑ils d’en dire alors ? Rien, et cette remarque est importante. C’est un cas simple qui montre que les types bloquent l’incohérence en limitant ce qui peut être dit tout‑court. Ils ne distinguent pas le correcte de l’incorrecte, ils ne permettent de dire que le correcte dans la limite de ce qu’ils permettent de dire.

Les types ont quand‑même un avantage pratique à côté de cette limitation. Les erreurs de types sont généralement faciles à comprendre et à corriger, sauf constructions sophistiquées, justement rendues nécessaires par la limite de leur expressivité. Reste quand‑même qu’ils produisent des diagnostiques décidables et assez faciles à comprendre. Et même s’ils ne sont pas naturels au premier abord, ils peuvent le devenir pas trop difficilement.

Même avec un langage plus expressif, il pourrait être intéressant en pratique, de distinguer des idiomes qui seraient une reformulation du principe des types, pour retrouver dans ces idiomes, les mêmes qualités que celle rapportées plus haut. Mais au moins, ce serait sans y être enfermé, en pouvant en sortir quand c’est ailleurs qu’est le chemin le plus clair qui se présente.

Une limitation des types est qu’ils ne décrivent pas tant des relations en général qu’ils ne décrivent que des relations hiérarchiques dans lesquelles la duplicité n’a pas de place. Les relations entre les choses ne sont pas toujours des arbres, elles sont souvent des graphes et elles sont rarement subordonnées, elles peuvent être en relation avec plus d’une chose en ayant dans chaque relation, un rôle différent.

Les types dépendants sont plus expressifs pour ce qui est des relations, mais ils ne permettent pas plus de par exemple dire qu’une chose fait partie de deux types différents, alors que cette possibilité est naturelle pour tout le monde. Par exemple une lettre en particulier, sans que ce ne soit nécessairement le cas de toute, peut tout à la fois être une lettre de l’alphabet, un logo ou un pictogramme. Avec les types, il est pourtant peu évident de faire passer un caractère en particulier pour une image, excepté si c’est le cas de tous les autres aussi.

Le problème de l’expressivité des types n’est pas spécifique aux types. Le problème des types n’est pas tant qu’ils sont des types, qu’ils sont une solution à un type de problème particulier. Ils résolvent bien un type de problème, mais dont le champs est trop limité. C’est en fait le cas de toutes les solutions ad‑hoc, peu générales. On se retrouve autant facilement devant l’impossibilité de dire des choses qui ont pourtant du sens, avec par exemple en SML, l’impossibilité de définir un foncteur imbriqué dans une structure ou de renommer un foncteur comme il est pourtant possible de le faire avec une structure. Si on ne peut pas formuler ces choses qui ont pourtant du sens, c’est parce que le sens, n’est pas le propos de ces langages, qu’ils soient ceux des types ou ceux de la modularité ou autres encore. La même remarque qu’en parlant précédemment des qualités que les types ont malgré tout, s’applique : reformuler ces constructions dans un langage dont le sens est le propos, peut être une solution pour les retrouver sans s’y enfermer.

La négation joue encore un de ces tour en suggérant d’ajouter une nouvelle distinction entre les règles, d’après le comportement de leur satisfiabilité. Elle amène aussi à réviser l’appréciation de l’hypothèse du monde clos.

Ça a initialement été remarqué en imaginant à quoi pourrait ressembler la modularité avec le langage décrit ici, comme en pratique la nécessité de la modularité fini toujours par se poser.

La question délicate du masquage n’est pas la plus intéressante à ce sujet, celle de l’extension l’est, c’est elle qui a fait remarquer quelque chose.

Le masquage pose un problème (à résoudre un jour), en ne permettant plus de vérifier des choses qui dépendrait de règles masquées, c’est à dire rendues inaccessibles. L’extension, l’ajout de règles à un contexte, semble plus innocente en y pensant vite, mais pourtant pose un autre problème aussi, avec la satisfiabilité des règles en présence de termes négatifs.

La simple règle « A : non b » est trivialement satisfiable dans un contexte où il n’existe aucune tête de règle « b ». Mais si une règle correspondante est ajoutée et qu’elle n’a pas de condition, la règle passe de satisfiable à non‑satisfiable. L’ajout de règles n’est pas plus anodin que le masquage de règles, mais seulement par le fait des termes négatifs. Si dans un ensemble de règle, il n’y a aucun terme négatif, alors les règles satisfiables, le restent toujours, quelque soit les règles éventuellement ajoutées ultérieurement.

La négation justifie de distinguer les satisfiabilités stables de celles qui ne le sont pas, et donc de distinguer les règles concernées. L’idée est simple à formuler ainsi, mais en pratique, la distinction peut ne pas être évidente, en tout cas pas si on veut éviter les faux positifs.

Ça suggère aussi de réviser l’appréciation qu’on peut se faire de l’hypothèse du monde clos. On peut y voir une limite dommageable mais contre laquelle on ne peut rien. Les remarques précédentes ont une importance à ce propos aussi : elles disent que cette hypothèse ne change rien au moins à la satisfiabilité de certaines règles, en tout cas rien dont on pourrait se désoler. C’est une autre bonne raison de trouver une solution applicable en pratique, pour distinguer ces règles qui ont une propriété qui ne dépend pas de la taille du monde connu, quelque chose sur quoi on peut compter avec une certitude absolue, même sous l’hypothèse du monde clos dans une monde potentiellement plus vaste.

Une idée de manière de traiter formellement une écriture faisant omission de détails pour raison de lisibilité.

L’implicite permet d’alléger la communication, autant dans les langues naturelles que dans les langages formels. Mais l’implicite présente des risques d’incompréhension, et avec les langages formels, les incompréhensions deviennent facilement décourageante.

Un exemple bien plus simple que des cas réels, serait une expression qui serait une séquence de termes de la forme (a X Y). On imagine que écrire “(r (a x1 y1) (a x2 y2) (a x3 y3))” est trop lourd à lire, surtout dans le cas d’expressions imbriqués. Imaginons que l’attention sur porte plus sur les X et que les Y, malgré qu’ils soient formellement nécessaires, sont secondaires pour un certain propos. On pourrait préférer alors écrire “(r (a x1) (a x2) (a x3))”, plus léger mais incorrecte, les Y étant nécessaires.

Si une chose peut être implicite, il y a généralement des raisons, comme la possibilité de recouvrer l’information manquante connue par ailleurs et qu’on ne répète seulement pas. C’est finalement une application d’une forme de résolution quelconque.

Si on imagines que les termes (a X Y) sont définis par une interprétation, une règle comme “(a X Y) : …” on pourrait imaginer qu’une règle de cette forme soit aussi possible : “(a X) : (a X Y).” Cette règle pourrait se comprendre ainsi : on peut parler de (a X) si on peut parler de (a X Y).

Si une solution pour (a X Y) ne peut pas être trouvée étant donné (a X), alors on considère qu’on ne peut pas parler de (a X) avec Y implicite et qu’on doit parler de (a X Y) explicitement. Dans le cas contraire, si la résolution est possible, implicitement une résolution automatique, alors on peut parler de (a X) , en laissant le Y implicite.

Concrètement, il faudrait quand‑même prévoir explicitement la possibilité de l’implicite, c’est à dire prévoir de pouvoir remplacer les (a X Y) par des (a X) dans (r …).

Informel, concernant la lisibilité d’une notation pour dire qu’on dérive une chose d’une autre.

Si f est une fonction alors f(x) est une valeur dérivée de x. En français on le dit « f de x », suggérant que le résultat est une propriété attachée à x. L’équivalent se dit aussi en anglais. Mais cette lecture ne rend pas toujours bien l’intention.

Parfois, le résultat de la fonction se comprend mieux comme une propriété d’une autre chose que comme une propriété de l’argument, même si cette propriété est dérivée de l’argument.

Deux exemples concrets de ces deux lectures possibles. On peut lire “ size list ” comme une propriété de la liste, ce cas n’est pas trompeur. Comme cas différent et potentiellement trompeur, imaginons qu’un type soit une paire de deux listes, left et right, et que la taille des deux listes bout à bout, soit une valeur constante, count. Dans ce cas « count - size left » définit la taille que doit avoir right. Cette valeur se dérive de left mais est une propriété de right. Dans ce cas, lire cette fonction comme “ f of left ” est trompeur, “ f from left ”, ou mieux encore mais plus verbeux “ f of right from left ”, dit mieux le sens. Le mot “ from ”, peut éventuellement mal se lire, un meilleur choix serait souhaitable, mais sans en voir un autre pour le moment.

On peut souvent se faire des remarques sur des idées de notations est d’autres, mais là il s’agit d’une notion essentielle, la lecture d’une chose dérivée d’une autre et à quoi on l’attache.

Pour être complet, il faudrait envisager le cas où la fonction définit une propriété à la fois de l’argument et d’une autre chose, même si je n’en vois pas d’exemple concret. Il n’y aurait pas besoin d’introduire un nouveau mot, le dire “ f of (x, y) from x ”, pourrait convenir, ou peut‑être remplacer le x par un mot restant à choisir, pour souligner que l’argument apparaît des deux côtés.