Les logiques : notes en vrac

Le message précédent est écrit avec un mot inconnu, X. Ce n’est pas le seul problème de vocabulaire restant en suspend.

Il a été vu que parler de constructeur dans les termes, est inapproprié. Il avait peut‑être aussi été dit que parler de relation pour une règle, n’est pas toujours approprié non‑plus.

Parler de relation pour une règle, n’est pas toujours approprié, parce qu’une règle peut porter sur un seul terme, alors qu’une relation, suggère deux termes au moins et peut‑être plus.

Par contre, ce qui a été plusieurs appelé, constructeur, serait peut‑être à qualifier de relation. Le terme (a b) pourrait être qualifié de relation, tandis que a et b individuellement, resteraient qualifiés de constantes.

Plutôt que parler de relation, pour une règle, mieux vaut parler de substitution. C’est beaucoup en terme de substitutions, que la sémantique du langage de base avait été décrite. Cette qualification, contrairement à celle de relation, ne semble pas peu‑idéale quand une règle porte sur un seul terme.

Au lieu de parler de terme le plus externe, parler de terme substituable, serait assez évocateur. Mais la substitution étant conditionnelle, ça pourrait être trompeur. D’un autre côté, parler de terme conditionnel, pourrait surprendre.

Reste les termes internes. Peut‑être que les qualifier d’idéogrammes, serait une idée. En effet, ils ont une structure récursivement composable et exprime des relations de compossibilité (sous réserve de validation par une règle … ou pas) : ils ne sont pas entièrement arbitraires, même si le choix des noms des constantes et leur ordre d’apparition, est « arbitraire » (guillemets, parce que en pratique, on ne choisi par un nom ou un ordre par hasard, même si on pourrait aussi bien le faire ainsi). Ils seraient encore plus abstraits que les idéogrammes, mais auraient bien deux propriétés importantes en commun avec ceux d’anciennes écritures humaines : ils sont composables et représentent directement une chose concrète, même si ici, la chose concrète, est assez abstraite. La différence avec les idéogrammes des anciennes écritures, est qu’ils seraient composables « sans limite ».

Seulement, parler d’idéogrammes, pourrait surprendre, alors peut‑être qu’un mot portant la même idée mais surprenant moins, devrait être trouvé.

Justement, en parlant d’ensembles, on pourrait se demander pourquoi ne se pose pas, la question d’une représentation pour la notion d’ensembles à proprement parler.

La réponse est qu’il n’y en a pas besoin pour que le langage soit assez expressif pour parler de ses propres termes. Il y a certes l’ensemble des règles, qui est bien un ensemble comme l’ordre et les duplications sont sémantiquement sans importance, mais ça concerne l’interprétation des résultats des requêtes, le langage lui‑même ne traitant pas avec, comme il ne connait que le succès ou l’échec d’une vérification et les contextes associés. Idem avec l’ensemble des termes du corps d’une règle, dont l’ordre a des effets similaires à celui des l’ordre des règles.

Ça n’empêche pas de représenter des ensembles par des termes et opérations sur ces termes, les opérations ayant des propriétés faisant qu’elles correspondent à la définition d’un ensemble tel qu’on le comprend.

Mais alors pourquoi ne pas en dire autant de ces séquences à l’ordre arbitraire mais non‑permutable ? La raison est qu’elles sont déjà dans la sémantique du langage, mais sans avoir de représentation permettant de formuler et raisonner à leur sujet. Si le langage était de sorte que l’ordre de l’unification des termes composant un terme, a une importance (autre que technique ou pratique), alors ce ne serait pas nécessaire, mais ce n’est pas le cas. Ajouter la possibilité d’une notation explicite pour cette notion, semble plus intéressant que de modifier la sémantique du langage de sorte à ce qu’un tel ajout ne soit pas nécessaire. Si la sémantique était modifiée de manière à rendre pertinent l’ordre de l’unification, ce serait probablement sous la justification de rendre interprétable des détails techniques de l’unification de deux termes, et faute d’exemple d’une éventuelle interprétation intéressante, cette idée n’est pas retenue et me semble même alambiquée. Pour cette raison, la sémantique n’est pas changée, et à la place, une notation explicite pour une notion sémantique implicite et déjà existante, « est » ajoutée

 … ou plutôt le sera éventuellement, car ça reste sous réserve que d’autres réflexions ne suggèrent de revenir sur cette idée.

Concernant la notation, une autre idée pourrait être d’écrire "a b c d" au lieu de |a b c d|. Ça ferait écho à un cas similaire dans le langage naturel, quand une langue parle d’elle‑même en faisant de ses propres termes, un sujet. Mais les guillemets sont aussi couramment utilisés dans un autre domaine, pour représenter une séquence de caractères, du texte littéral sans interprétation autre que d’être une séquence de caractères ; mieux vaut préserver cette convention utile et répandue.

Dans le cas de |A B| lié à |a b c d|, il n’y aurait qu’une solution à l’unification, mais le développement d’une solution à une requête, se ferait quand‑même en considérant qu’il y a plusieurs développements possibles pour le A et le B de |A B|. Ça doit être posé, pour ne pas altérer la sémantique du langage, qui est le développement d’une solution à une requête, jusqu’à arriver à des termes tout entier constants, même si en pratique, ça ne se fait pas toujours à l’affichage dans une interface‑utilisateur. Une solution à une requête aurait plusieurs interprétations possibles, mais c’est déjà assez le cas même sans cet ajout, comme une requête pouvait déjà avoir plusieurs solutions possibles, même si chacune n’avait qu’une seule interprétation ; dans les deux cas, le résultat est plusieurs solutions possibles, et la différence entre les deux chemins y menant, n’a pas d’importance pour la sémantique, les termes constants résultants n’en gardant pas la trace.

Ça ne tient pas. L’idée de ce type de terme me semble toujours pertinente pour l’écriture, mais il serait peut‑être préférable de la dériver à partir des listes et d’avoir là aussi, un sucre syntaxique pour les représenter.

Pour que le langage permette de parler de lui‑même, il doit permettre de représenter ses constructions par des termes. On voit que le terme semble avoir un status particulier : c’est le terme qui représente et en même temps, il doit pouvoir être représenté.

Note : pour que les termes représentant les constructions du langage ne puissent pas être interprétés comme n’importe quels autres termes, ils doivent être distingués par des constantes non‑utilisées pour autre chose, une constante par type de construction (voilà qu’on reparle de types).

Mais même si le terme semble avoir un statut particulier, mieux vaut peut‑être le représenter comme une liste. C’est dans la question du corps des règles, dont l’ordre des termes n’est pas pertinent lui aussi, qu’est une raison de le penser.

Il y a la sémantique du langage, mais il y a sa formulation. La sémantique du langage, c’est sa formulation et tout ce qu’on peut déduire de cette formulation. Les aspects sémantiques n’ont pas tous le même status. Prenons le cas du corps des règles. Il est défini comme une liste de termes substituables, selon un processus qui a déjà été longuement décrit. Par la suite, une démonstration informelle a été faite, que l’ordre des termes n’a pas d’importance pour le caractère satisfiable ou non d’une règle dans un contexte donné. L’argument était essentiellement, que tous les termes du corps de la règle sont satisfaits par un contexte et que l’ordre des termes n’a pas d’importance dans leurs liens avec un contexte les satisfaisant.

On peut remarquer qu’on a une définition et ensuite une déduction d’une propriété. Il en va de même avec les termes eux‑même, si l’ordre dans lequel les termes composant un terme, sont unifiés, si cet ordre n’a pas d’importance, c’est pour la même raison. Le point important est que c’est un fait par déduction, pas par définition.

Il y a bien quelque chose d’assez important dans le type de terme proposé, mais c’est à poser comme concept dérivé.

L’idée est donc abandonnée, la conclusion est la même qu’avec l’idée des règles ordonnées par priorité : ce n’est pas un élément essentiel de la sémantique et ne justifie donc pas une modification du langage. Un support de ce type d’expression avec un sucre syntaxique, lui, serait cependant utile : traiter avec ce type de terme en les manipulant directement comme des listes, serait en effet laborieux, plus encore qu’ajouter des négations en quantités (avec les risque d’erreur d’écriture que ça implique) pour formuler l’idée de règles ordonnées par priorité.

Ce sucre syntaxique aurait la même notation et les propriétés des termes seraient les mêmes que précédemment décrit.

Le précédent message est une solution prudente, mais ne dissipe pas la sensation que quelque chose cloche ; l’affaire n’est pas close.

On peut informellement conclure à la non‑pertinence de l’ordre des règles, de l’ordre des termes dans le corps d’une règle ou à la non‑pertinence de l’ordre d’unification des termes dans un terme, malgré que cet ordre ait une importance pratique, on peut le conclure sous la supposition que l’ordre des solutions renvoyés ou même leurs duplications, n’a pas d’importance pour l’interprétation.

C’est là qu’est le problème. La sensation que quelque chose cloche avec le fait de représenter un terme par un liste (une question proche de la précédente), ce qui ne correspond pas à la sémantique telle qu’elle est comprise, vient du fait que cette équivalence n’est pas formulée, elle est seulement dite.

Comment, dans les termes du langage lui‑même, poser que l’interprétation est l’ensemble potentiellement infini des solutions à une requête, impliquant que la manière dont les solutions sont produites, n’a pas d’importance ? Si l’ensemble des solutions était typiquement fini, il serait possible d’imaginer définir un terme représentant un ensemble de solutions et définir une règle représentant la collecte des solutions à une requête dans un tel terme. Si les ensembles sont représentés par des listes, il faut définir une règle pour l’égalité entre deux ensembles, ce qui correspond à l’équivalence pour l’interprétation. Ce n’est qu’une idée approximative, mais qui serait probablement réalisable. Elle présente pourtant deux problèmes. Le premier, est qu’elle ressemble plus à une mise en œuvre qu’à une spécification, ce qui peut éventuellement être un mauvais signe. Le second, est qu’elle ne permet peut‑être pas de formuler l’équivalence d’ensembles infinis de solutions.

La sensation que quelque chose cloche, vient peut‑être plutôt du fait qu’il y a dans une partie informelle de la définition du langage, une notion d’équivalence, qui ne se retrouve pas dans la définition formelle du langage. Le langage n’a pas de notion d’équivalence, seulement une notion d’égalité.

L’équivalence s’applique à l’interprétation et le langage n’est pas concerné par l’interprétation effective, seulement par ce qui est interprété. Mais cette équivalence s’applique à toutes les interprétations, elle n’est donc pas spécifique aux interprétations individuellement, elle est une caractéristique de toutes les interprétations quoi‑qu’elles soient. Dans ces conditions, cette équivalence pourrait ne pas être ignoré par le langage, même s’il n’est pas concerné par les interprétations effectives (ex. l’interprétation d’un terme dans un domaine).

Mais comment intégrer au langage, une notion d’équivalence pour l’interprétation, d’une manière qui permette de formellement en déduire que l’ordre des règles et des termes du corps d’une règle, n’a pas d’importance ? Est‑ce seulement possible ? Pour les termes du langage, par quoi cette équivalence s’exprimerait‑elle ? L’égalité s’exprime par l’unification, mais l’équivalence, par quoi pourrait‑elle s’exprimer ?

Il existe un cas où ce problème ne se pose pas : quand le résultat d’une requête est Oui ou Non. Mais est‑ce pour autant une piste …

Il existe dans le langage, une notion pouvant évoquer l’équivalence, mais qui ne lui correspond pas : la substitution d’un terme unifié à la tête d’une règle, par les termes du corps de la règle, établit comme une équivalence entre les deux. Mais cette substitution participe aussi à l’élaboration de la solution pour les variables liées passant par la tête de la règle, ce qui est en dehors du domaine d’une relation d’équivalence comme elle est comprise ici. Ce serait éventuellement une équivalence à posteriori, la solution au terme, et donc le terme lui‑même, n’étant pas toujours fixé au moment de la substitution.

Une partie du problème du précédent message peut être résolu avec un cas particulier de règle, mais ça n’est toujours pas une solution.

Si on a :

A. -- Corps vide
B : A.

Le corps de A étant vide, A ne participe pas à la liaison des variables dans B. Ce type de construction pourrait faire penser à une équivalence entre B et A, mais ça n’est pas le cas, parce que « B : A. » signifie que B doit être remplacé par A et non‑pas que B peut être remplacé par A (ou une hypothèse correspondante).

L’équivalence étant ici une égalité pour l’interprétation, l’équivalence semble plus proche de l’égalité que de la substitution obligatoire.

Pourtant, une variante de l’idée précédente pourrait être ceci :

A.
B.
A : B.
B : A.

En pratique, il y a un risque de récursion infini, mais ça n’a pas d’importance pour la signification de ces règles. Le problème est plutôt que pour poser une équivalence de cette manière, A et B doivent être chacun inconditionnellement vérifiable.

Une substitution dans les deux sens correspond déjà mieux à une équivalence, mais elle n’est possible qu’entre deux termes pouvant chacun être vérifié par une règle dont le corps est vide.

De plus, en supposant qu’il soit possible de poser une relation d’équivalence entre deux termes, comment à partir de relations d’équivalence entre termes, poser l’équivalence pour l’interprétation ? Ce ne serait encore pas tout. Pour que ce soit pertinent, il faudrait que cette équivalence soit posée d’une manière faisant qu’il soit possible de formellement en conclure que l’ordre des règles n’a pas d’importance.

Le « doit » est sous‑entendu compris comme « doit, pour vérifier la règle ». L’équivalence d’un terme, n’est pas une condition de satisfaction de ce terme, là est la différence.

L’équivalence ressemble à la substitution par une définition, mais ne l’est pas, elle ressemble à l’égalité, mais ne l’est pas. Son existence est posée ici pour le besoin de tenir compte de l’interprétation, elle n’a donc pas à être démontrée par le langage, ce qui confirme encore que ce n’est pas une règle dans le sens habituel jusqu’ici.

Peut‑être faut‑il introduire la notion d’équivalence pour elle‑même, à côté des règles :

A ≣ B. -- U+2263, le symbole de l’équivalence le plus courant.

S’il ne s’affiche pas correctement : c’est le symbol avec quatre traits horizontaux, comme deux signes égal l’un au dessus de l’autre.

A == B. -- Notation alternative pour s’assurer qu’elle s’affiche.

« A == B. » ne serait pas une condition pour vérifier A, qui devrait donc être vérifié par ailleurs. Pour ne pas substituer un terme vérifié par un terme non‑vérifiée, B devrait être vérifié aussi, c’est à dire que A et B devraient être satisfaits par le même contexte. Pour que ça ne deviennent pas une recherche de solution, B devrait avoir déjà été vérifié, tout comme A. On aurait donc (A == B) => (A & B), comme avec l’égalité, même si une équivalence n’est pas l’égalité, on aurait donc pas (A == B) => (A = B).

L’équivalence en elle‑même, pourrait être démontrable, par exemple quand on a une équivalence pour une certaine interprétation, mais elle ne doit pas avoir à l’être obligatoirement, pour les cas où l’interprétation ne se fait pas connaitre autrement qu’en posant une équivalence.

Cette fois, il serait possible de poser « A == B. » tout en ayant « A : A1 & A2 & … » et « B : B1 & B2 & … ». Pour ne pas casser la sémantique du langage, comme dit plus haut, A et B devrait être satisfaits par le même contexte, et cela devrait être vérifié avant d’appliquer l’équivalence, même si la relation d’équivalence en elle‑même, n’aurait pas à être démontrée (elle pourrait l’être, mais il est trop tôt pour s’engager dans cette direction).

Comme précédemment, c’est sous réserve de futures réflexions.

Questions :

Comment à partir de cette éventuelle possibilité de poser une équivalence, formuler l’équivalence pour l’interprétation ?

L’équivalence devrait‑elle être applicable seulement à des termes pour eux‑mêmes ou devrait‑elle être aussi applicable à des conjonctions de termes ? Par exemple, devrait‑il être possible de poser quelque chose comme « A & B == C & D & E. » ?

Devrait‑il être possible de conclure une équivalence ? Par exemple de « A == B. » et « B == C. », devrait‑il être possible de conclure « A == C. » ?

Faudrait‑il poser (A = B) => (A == B) ?

Avant de revenir plus tard sur le message précédent et de revenir encore plus tard, sur des questions dont les réponses ont été mise en attente depuis deux ou trois semaines, un retour sur la notion de X notée par |…| et introduite précédemment.

Il avait été conclus qu’elle devrait être faite notion dérivée. Finalement non, c’est une notion fondamentale, qui doit avoir ses propres règles et sa propre représentation. La représentation et les règles ont déjà été décrites et ne sont pas re‑exposées. Ce qui est présenté ici, c’est de la justification à lui donner un statut de notion fondamentale et pourquoi en faire une notion dérivée, ne convient pas.

En faire une notion dérivée dont la représentation sous-jacente serait une liste, peut se concevoir dans un premier temps. Pour qu’elle ne se confonde pas avec les listes caractérisées par les constantes cons et nil, il serait possible d’utiliser d’autres constantes, disons cons2 et nil2, à défaut de trouver des noms plus originaux. Mais resterait deux problèmes. D’abord celui déjà abordé qui serait de dire une chose qu’on ne souhaite pas dire (carence d’orthogonalité, comme on pourrait le dire dans certains domaines). Ensuite, il a été vu que le nom des constantes importe peu, que ce sont essentiellement les règles et les constructions qui font le sens, pas les noms qu’on donnent, dont la seule propriété importante et d’être les mêmes ou d’être distincts. Représenter cette notion avec des listes caractérisées par des constantes cons2 et nil2, n’en ferait pas moins des listes, même si elles se distingueraient des autres listes.

Il y a plus et plus fondamentale et c’est justement l’exemple des listes qui vient facilement pour l’illustrer.

Prenons une liste dont le terme est « (a (b (c (d ())))) ». Quel est son premier élément ? C’est « a ». Maintenant, prenons une autre liste, « ((((() d) c) b) a) ». Quel est son premier élément ? C’est « a », aussi. Mais pourtant, dans le second exemple, le premier élément est à gauche alors que dans l’autre, le premier élément est à droite. Qu’est‑ce qui en fait le premier élément alors, si ce n’est pas d’être à droite ou à gauche ? Ce qui fait de « a », le premier élément, c’est qu’il est l’élément le plus externe. Une liste, c’est une paire de un premier élément éventuellement nul et un reste de liste qui n’est présent que si le premier élément n’est pas nul, le reste de liste étant lui‑même composé de la même manière, et ainsi de suite, récursivement. Le premier élément auquel on accède est « a », le second est « b », dans les deux cas, ainsi de suite, les deux listes présentent en fait leurs éléments dans le même ordre, a, b, c et d, malgré qu’elles les écrivent chacune dans un sens opposé, l’accès à leur élément produit la même séquence. On voit ici que l’ordre de la paire, n’a pas d’importance, qu’on peut placer le premier élément à droite et le reste à gauche ou le contraire, sans rien changer au sens.

Maintenant une exercice apparemment sans rapport, mais dont on finira par voir qu’il en a un. Si on ne voulait représenter des termes qu’en utilisant une constante et ce qu’offre la composition par imbrication, et rien d’autre, que pourrait‑on formuler ? On pourrait commencer par une seule constante, disons « c ». On pourrait la mettre entre parenthèses et obtenir « (c) ». Que pourrait‑on écrire encore ? Ben … pareil, en remet des parenthèses … « ((c)) ». Et encore ? Ben, … toujours pareil, « (((c))) » … heu, ça va toujours être comme ça, c’est assez pauvre quand‑même.

Que manque‑t‑il ? De pouvoir ajouter quelque chose à côté de « c ». Avec cette possibilité, alors là, ça devient beaucoup plus riche. On peut écrire « c » ou « c c » ou « ((c) c) » ou « ((c) ((c c) c) », etc. C’est déjà beaucoup plus expressif, avec pourtant une seule constante et ça le serait plus encore si on se permettait plus de constantes.

La composition par imbrication, appelons‑la, composition verticale, parce que quand on imbrique, on met une chose sous ou sur une autre. C’est plus facile à imaginer si on se représente un terme comportant des parenthèses, comme un arbre. La composition qui consiste à ajouter une chose à côté d’une autre, appelons‑la, composition horizontale. Cette dernière est tellement essentielle, que l’expressivité de la première en dépend. Les listes n’existeraient même pas sans cette composition horizontale. Cette composition horizontal, c’est justement celle dont il a été question précédemment en l’appelant X. Voilà, X, c’est la composition horizontale. Sans cette composition, même pas de liste, alors la décrire comme une liste, sémantiquement, ce n’est pas facilement acceptable.

En fait, il serait plus facile d’imaginer une écriture ne permettant que cette composition horizontale, même sans composition verticale, plutôt que l’inverse ; c’est dire son importance et la justification qu’il y à en faire une notion fondamentale au lieu d’une notion dérivée.

Ceci est à comprendre en faisant toujours attention à ne pas confondre mise en œuvre et sémantique, représentation interne d’une mise en œuvre et sémantique. On pourrait utiliser une composition horizontale pour représenter une liste de longueur fixe, ça ne fait pas pour autant de la liste, une construction non‑récursive. On peut utiliser une liste pour représenter une composition horizontale de longueur variable, ça ne fait pas pour autant de cette composition une construction récursive. Une mise en œuvre dans un langage permettant de définir des types abstraits, dont la représentation est masquée, seulement exposée par des opérations, ne présente pas de risque de confusion. Mais le langage dont il est question ici, est un langage de spécification, un langage sémantique, sont écriture ne cache rien, il expose tout et tout ce qui y est écrit, tout ce qui y est a une signification.

Rapide mais utile retour sur le parallèle qui avait été fait avec les ensembles. Qu’en‑est‑il des ensembles ? Faut‑il réviser leur statut aussi ou pas ? Est‑ce une notion fondamentale ou une notion dérivée ? Disons que jusque maintenant, ils ne s’en est jamais véritablement présenté nul‑part, même pas implicitement. Même l’ensemble des règles n’en est pas un exemple. Non‑pas seulement parce qu’il est permis d’écrire des règles en double, mais parce que ce qui fait que l’ordre des règles a moins d’importance que l’ordre des termes dans un terme, c’est seulement que cet ordre n’a qu’une seule instance. Explications ci‑dessous.

Il avait été vu que même si l’ordre des termes dans un terme, n’est pas pertinent, il est important que les positions de chacun de ces termes, soient fixées, parce que si les positions de deux termes sont permutées, il faudrait faire la même permutation partout où ce terme apparaît écrit d’une manière ou d’une autre, ce qui n’est peut‑être même pas toujours automatiquement réalisable. Mais si un terme n’est écrit qu’une seule fois quelque part, il est possible de permuter les termes qui le compose, cette permutation n’aura pas à être faite ailleurs. C’est ce qu’il se passe avec l’ordre des règles, cet ordre arbitraire peut être permuté, parce qu’il n’a qu’une seule instance. L’ensemble des règles se représenterait donc bien comme une composition horizontale de règles. Même si on peut l’appeler un ensemble, il n’en est pas un, parce qu’il peut présenter des duplications. Il est alors considéré pour le moment au moins, que le nécessité d’une représentation pour les ensembles comme notion fondamentale, ne s’est jamais présenté, et si elle ne se présente jamais, il n’y aura jamais de raison de passer son statut de notion dérivée à notion fondamentale. Les ensembles gardent leur status de notion dérivée et au passage, aucune notation ne leur a été attribuée pour le moment (les crochets « { } » sont attribués aux hypothèses, à moins que cette notation ne soit encore révisée).