Les logiques : notes en vrac

Comme il est question de substitutions, il faut re‑éclaircir le sens du mot, qui a été égaré en chemin.

Un bref retour sur ce qui a déjà été expliqué, sur l’application des règles. Soit une règle « A : B. » et un terme « C », ce terme pouvant se trouver où que ce soit, dans le corps d’une règle ou d’une requête. Quand l’unification de C et A réussit, C est remplacé par B ; excepté que le dire comme ça est trompeur par omission. Ce n’est pas C qui est remplacé par B, c’est un reste de condition à vérifier, une partie l’ayant déjà été avec l’unification de C et A. Si « A : B. » est vu comme une définition, ce qui a donné l’idée du symbole « : » pour séparer la tête de la règle et le corps de la règle, B n’est pas la définition de A, c’est « A : B. » tout entier, qui est une définition (*). Quand a lieu la tentative d’unification de C avec A, on peut déjà dire qu’il est tenté de remplacer C par A, et qu’on revient en arrière en cas d’échec, de même qu’on revient en arrière en cas d’échec de la vérification de B. C’est « A : B. » qui une est définition et cette définition, c’est celle de C ou de tous autres termes vérifiables par cette règle. Le terme C n’est pas seulement remplacé par B, il est remplacé par A d’abord, puis par B. Au final, A ayant été déjà interprété, B est remplacé aussi après son interprétation, éventuellement celle d’un corps vide, et ne reste que le contexte produit par A et par B. Le sens de C se trouve alors dans le contexte et de même pour les éventuels autres termes.

L’équivalence, elle, peut justifier de substituer un terme par un autre, par là, une application d’une règle par une autre (que ce soit une autre règle à proprement parler ou une même règle avec un autre contexte).

Avant de revenir sur les équivalences, un complément au message précédent, qui comme lui, se replace en amont en revenant sur des choses déjà abordées, pour les clarifier mieux.

Plus haut il est dit que quand le terme C est vérifié par la règle « A : B. », c’est la règle toute entière qui est une définition, pas B tout‑seul. Ça semble contradictoire avec l’analogie de l’année précédente, celle du dictionnaire, mais ça l’est moins si on repense à une analogie plus récente, celle qu’un terme est bien assez comparable à un idéogramme, seulement plus abstrait et plus composable. Un idéogramme porte déjà du sens en lui‑même, ce qui rend moins surprenant que le terme défini, A, fasse partie de la définition, B étant un complément de précision (une précision qui doit être vérifiée, donc aussi une condition). Il y a un an, cet aspect avait déjà été relevé et il avait été fait remarquer qu’une règle peut s’écrire de manière à déplacer une partie du sens porté par la tête de la règle, vers le corps de la règle. Par exemple au lieu d’écrire « (nat (s N)) : (nat N). » il est en principe possible d’écrire « (nat N) : (eq N (s N2)) & (nat N2). ». Il avait cependant été suggéré que la première forme est préférable et que les usages de eq dans un corps de règle, peuvent être considérés comme à éviter, à moins qu’ils ne servent à incrémentalement composer des termes complexes, qui serait illisibles s’ils étaient écrits d’un trait. L’analogie du dictionnaire est valable, mais avec une nuance. Lire les règles, c’est comme chercher la définition d’un mot dont on a déjà une vague idée du sens d’après sa forme, pour lequel on a besoin d’un complément de précision. Ça ne vaut pas pour les règles au corps vide, qui représentent des concepts posés tels‑quels, des concepts issus du domaine pour lequel on écrit des représentations, ce domaine qui est le domaine d’interprétation. Disons que l’ensemble des règles est un dictionnaire où il est vain de chercher la définition d’un mot, si en le voyant on a vraiment aucune idée de ce qu’il pourrait peut‑être signifier … et en pratique, c’est vrai d’un dictionnaire. Si on a vraiment aucune idée de ce sur quoi porte un mot en le voyant, donner des précisions n’aidera pas plus et il faut plutôt trouver une introduction au domaine auquel appartient le mot, et seulement alors, le mot commencera à avoir vaguement un sens et sa compréhension pourra être complétée par quelques précisions.

En parlant d’idéogramme, il s’est posé la question de trouver un mot qui surprendrait moins mais porterait le même sens. Apparemment, non, il n’en existe pas. Les mots « signe » ou « symbole », qui en seraient des synonymes d’après le CNRTL, sont plus généraux. Par exemple dans la définition de l’idéogramme, le mot « symbole » est utilisé pour parler de signes phonétiques en précisant que l’idéogramme se distingue de ce type de signe. Parler de symbole, serait trop général et favoriserait l’égarement. Parler se signe pourrait peut‑être un peu mieux convenir, mais la définition de ce qu’est un signe sur le CNRTL toujours, suggère que ce mot peut être utilisé pour parler de la justification à un prédiction ou à un pressentiment, ce qui est trop générale aussi ou tend même vers la notion d’inférence.

En conclusion, parler d’idéogramme, est ce que me semble le moins trompeur et le plus directement évocateur. Même s’il existait un autre mot, il serait peut‑être tellement spécifique ou pompeux qu’il en serait moins compréhensible.

C’est officiel, les termes du langage dont il est question ici, sont des idéogrammes.

Certaines précédentes questions concernant l’équivalence, était de savoir si elle doit s’appliquer aux termes externes, comment désigner les sites valides pour des substitutions de termes internes, comment qualifier les différentes équivalences, vu qu’il peut y en avoir plusieurs et savoir si l’équivalence pourrait réutiliser le système d’inférence déjà existant.

À la première question, une réponse avait été donnée, mais elle doit être révisée pour le besoin d’une réponse à la seconde question. Il avait été dit que l’équivalence pourrait d’abord seulement s’appliquer aux termes internes. Mais cette réponse était une réponse temporaire par défaut, justifiée par la raison pour laquelle l’équivalence a été introduite (les résultats des résolutions, qui sont des termes internes, jusque maintenant). Mais ça ferait obstacle à une possible réponse à la seconde question, celle de désigner les lieux valides pour une substitution donnée.

S’il existe une relation d’équivalence pour le terme A de (r A B) par exemple, une bonne solution pour le désigner, serait justement d’écrire ce terme avant et après substitution, dans une règle. Par exemple « (r A1 B) == (r A2 B) » en faisant une description de A2 par rapport à A1 ou la réciproque. L’emplacement valide pour une substitution, est bien désignée, et est désignée en posant l’équivalence de deux termes externes. Non seulement l’idée de substitution vient naturellement après l’idée d’équivalence, et peut‑être qu’en plus, il y a dans la formulation de l’équivalence même, l’idée de substitution, comme cet exemple semble le suggérer. En fait, les deux termes de la règle d’équivalence, pourraient aussi bien être des termes internes, comme ce sera envisagé plus loin.

Concernant la possible réutilisation du système d’inférence actuel pour l’équivalence, à la suite du paragraphe précédent on pourrait avoir l’idée de valider une substitution, par une sorte d’unification, mais qui ne lierait rien, qui ne ferait que vérifier la correspondance de deux termes. Étant donné l’exemple « (r A1 B) == (r A2 B) », étant donné un terme correspondant, « (r A12 B) », la mise en correspondance de « (r A12 B) » avec « (r A1 B) », pourrait justifier la substitution de A12 par un A22, donnant « (r A22 B) ».

Resterait à préciser ce qu’est en détails, une formulation comme « (r A1 B) == (r A2 B) ». Peut‑être pourrait‑elle être complété par une condition, comme avec les règles ordinaires. Par exemple « (r A1 B) == (r A2 B) : (eq A1 A2). » L’exemple peut faire sourire par sa naïveté, mais sa naïveté le rend clair et montre de quelle manière cohérente, une équivalence et une possible substitution, les deux à la fois, pourraient être définies par une règle, dont la logique serait semblable à celle des règles ordinnaires.

Il reste deux questions en suspend. D’abord que serait un test de correspondance de deux termes, sans liaison de variables ? Techniquement, ça se conçoit facilement, mais sémantiquement, ça pose question, quand une variable n’est pas encore entièrement définie par une résolution. En même temps, il n’est pas insensé d’imaginer qu’une équivalence puisse être établie pour une solution partielle. Si une équivalence nécessite une résolution complète, alors si la résolution ne l’est pas, la mise en correspondance échoue et la substitution n’est pas applicable. Ça reste vague et informel, mais ça pourrait être une idée.

La seconde question en suspend, est moins délicate, mais présente quand‑même un nouveau type de mise correspondance de deux termes. Précédemment, un exemple a été donné avec une équivalence entre deux termes externes. Mais il serait aussi possible d’imaginer que l’équivalence soit décrite pour des termes internes, pourvu qu’ils correspondent. Par exemple il serait possible de définir « (c A) == (c B) : (d A B). » et d’après cette règle, il pourrait être possible de faire une substitution dans « (r (c A2)) ». Ce qui serait nouveau, c’est qu’un terme apparemment externe, défini par une règle, mais seulement dans le cas d’une règle d’équivalence, pourrait être mis en correspondance avec un terme interne.

Concernant la qualification de l’équivalence. L’équivalence, contrairement à l’égalité, n’est pas unique, il peut y en avoir plusieurs, non‑compatibles entre elles. D’ailleurs, elles sont généralement qualifiées par un complément dans leur nom, comme par exemple “ alpha-equivalence ” ou “ beta-equivalence ”, les noms de deux équivalences spécifiques au lambda‑calcul. En même temps, il peut être commode d’avoir à ne pas qualifier partout, une équivalence unique. Dans le cas où un système de règles ne se réfère qu’à une seule forme d’équivalence, il n’a pas besoin de la qualifier. Si plusieurs équivalences sont désignées, il n’y a peut‑être pas besoin d’introduire un concept nouveau pour les distinguer, comme on peut déjà distinguer des termes par une constante les caractérisant. La constante représentant l’équivalence en elle‑même, notée « == » ici, parce que le véritable symbole ne s’affiche pas, cette constante caractériserait une règle comme décrivant une équivalence, invoquant sa sémantique spécifique. Cette constante, comme toutes les autres, ne pourrait s’unifier qu’avec elle‑même, et par prudence, elle ne pourrait pas être unifiée avec une variable. L’unifier avec une variable, ne semble pas avoir de sens et il faut éviter de permettre ce qui semble ne pas pouvoir avoir de sens. Utiliser cette constante ailleurs comme une constante ordinaire, ne serait pas possible, comme cette constante donnerait automatiquement un status à part au terme qui la contient.

Au lieu d’être notée « A == B », l’équivalence serait notée « (== A B) », pour raison d’harmonie avec les notations habituelles dans le langage. Peut‑être que « (equiv A B) » serait plus évocateur, le symbole « == » pouvant ne pas être immédiatement compris comme celui de l’équivalence et pouvant être mal compris comme l’égalité stricte, c’est à dire sans conversion de type, de certains langages non‑typés. Le nom de la constante equiv, serait pour être en harmonie avec le nom de la constante eq.

Ça reste vague, mais c’est au moins, moins confus.

Remarque : il n’y aura pas de tests sur une mise en œuvre avant un temps indéterminé, qui sera probablement long. Tout ce qui est rapporté depuis fin‑Novembre 2020 environ, est basés des projections, des réflexions, sans être testé sur une mise en œuvre. Des exemples vérifiés sur une mise en œuvre, pour une version moins expressive du langage, ont été présentés vers fin‑Octobre ou courant‑Novembre 2020. C’était le cas par exemple du message détaillant le principe de la résolution avec des exemples où le cas des messages démontrant l’utilité de termes posés en hypothèses, même en l’absence de déduction structurée.

Une question posée, était celle de comment représenter l’équivalence des ensembles de solutions, l’interprétation ne se préoccupant ni de l’ordre ni des duplications. La question de l’exhaustivité des solutions est laissée à plus tard (et cette question me fait peur).

L’ensemble des solutions est supposé représenté par une liste, donc un seul terme, représentant une liste de termes. Une requête est supposée porter sur un seul terme, une solution de la liste de solutions, étant le développement complet du terme de la requête, après la production de chaque solution.

Les requêtes présentées en parlant du langage, peuvent être des conjonctions, mais il est possible de les représenter par un seul terme, pourvu qu’une règle correspondante soit écrite. La restriction d’une requête à un seul terme pour l’ensemble des solutions destinée à l’interprétation standard, simplifie la représentation de l’ensemble des solutions et semble correspondre à ce qui était suggéré dans des documents présentés vers Septembre ou début‑Octobre 2020, où l’ensemble des solutions était décrit comme un ensemble de termes.

L’utilisation d’une liste peut être mise en question. Le concept de composition horizontale ayant été introduit, il serait possible d’imaginer que l’ensemble des solutions soit représenté sous cette forme. Il peut y avoir des arguments pour et des arguments contre, cette idée. Pour le moment, la solution imaginée suppose une représentation sous forme d’une liste, mais rien ne dit que ce soit la seule possibilité.

Pour la représentation de la non‑pertinence de l’ordre des termes, une règle d’équivalence pourrait permettre de conclure à l’équivalence de toutes les permutations de cette liste. Une règle pourrait suffire : dire que les deux premiers éléments d’une liste peuvent être permutés. La notion de liste étant récursive, cette règle s’appliquerait au deux premiers termes d’une liste comportant au moins deux termes, autant qu’au reste de la liste. Le trie‑bulle illustre que cette seule règle suffit. En partant d’une liste d’éléments dans n’importe quel ordre, par permutation de deux éléments adjacents, il peut aboutir après un certain nombre de réitérations, à une liste triée. Un nombre suffisant de permutations de deux termes adjacents (pas toujours les mêmes), peut permettre d’aboutir à toutes les permutations possibles.

D’après le message précédent, cette règle pourrait ressembler à :

(equiv (cons A (cons B R)) (cons B (cons A R))) : (list R).
-- La notion de list est supposée préalablement définie.

Comment utiliser cette règle jusqu’à prouver qu’une règle peut être tentée avant une autre, malgré l’ordre dans lequel les règles sont écrites, est laissé à plus tard.

La non‑pertinence des duplications, pourrait être représentée d’une manière proche :

(equiv (cons A (cons A R)) (cons A R)) : (list R).
-- Dans un contexte où les permutations sont équivalentes.

Au lieu de cons, le constante pourrait être une autre constante spécifique aux listes de solutions, pour que cette équivalence ne s’applique pas à toutes les listes ; idem pour nil et list.

Une question avait été de savoir s’il faut poser la règle « A == B => B == A ». On pourrait penser la dériver de la symétrie de l’égalité, qu’il faut d’ailleurs poser, mais on ne peut pas en dériver la symétrie de l’équivalence dans tous les cas, seulement la symétrie de l’équivalence dérivée de l’égalité. De même que la symétrie de l’égalité doit être posée, celle de l’équivalence doit l’être aussi, même si la symétrie de l’équivalence est partiellement redondante, parce que en partie dérivable de celle de l’égalité. Si l’équivalence était toujours entièrement justifiée par l’égalité, ce ne serait pas nécessaire. Mais il est possible d’imaginer une interprétation qui ne soit pas formulée, mais qui formule quand‑même des équivalences. Poser la symétrie de l’équivalence ou pas, se discute. Le choix est fait ici de la poser, pour couvrir les deux cas, celui de l’équivalence entièrement formulée à partir de l’égalité et celui de l’équivalence posée telle‑quelle.

En parlant de ces règles, une précision : il ne s’agit pas de règles écrites comme nat, int, et les autres, ce sont des règles qui n’apparaîtront que dans la définition du langage, auxquels il n’y a pas besoin de se référer explicitement, comme elles s’expriment implicitement dans la sémantique. Par exemple l’égalité s’exprime dans l’unification. Ceci dit, il est espéré que cette définition du langage, puisse être écrite avec la syntaxe du langage lui‑même. La syntaxe seulement, parce que formellement, ça ne pourrait pas être le langage lui‑même. Cette première définition ne pourrait être compréhensible que pour un lecteur humain (moyennant un exposé explicatif en langage naturel), le langage ne pouvant pas exister avant sa définition. La syntaxe et les constructions seraient les mêmes, pour que une fois la définition posée, le langage existant alors, il puisse valider sa propre définition. À vrai dire, techniquement, on peut tricher, par exemple une mise en œuvre d’une version précédente du langage, avait été faite sans définition formelle. Mais formellement, logiquement, le langage ne peut pas exister avant sa définition, et ce qui a donc été réalisé, c’était au plus, quelque chose de plus ou moins comparable au langage, mais pas égale à lui‑même.

Par exemple, ce qui semble être l’interprétation standard du langage de base initial, ne pose qu‘une équivalence, et encore, généralement implicitement, en ne mentionnant juste jamais l’ordre comme pertinent ou en parlant d’un ensemble. Jamais une interprétation formellement définie n’est donnée et il n’est même pas exigé qu’il en existe une, le reste de l’interprétation semblant entièrement libre. Une interprétation concrète, formelle ou pas, semble seulement implicitement supposée faire avec cette équivalence comme préalable.


Précédemment avait été posée la question de savoir si l’équivalence est une notion dérivée ou fondamentale. Il a déjà expliqué pourquoi elle est une notion fondamentale. Cet exemple peut être une illustration des deux idées. L’écriture de ces règles, ne nécessite pas d’en faire une notion fondamentale, laissant un temps croire qu’on peut en faire une notion dérivée. Mais alors, on ne ferait que suggérer l’idée de l’équivalence, parce que pour la sémantique, ces règles signifieraient des termes à résoudre. Ors, en posant ces équivalences, on n’exprime pas le souhait de lister les solutions de ces règles, on exprime le fait que en cas de correspondance d’un terme avec un des deux côtés de l’équivalence, on peut lui substituer le terme de l’autre côté (expression de la symétrie de l’équivalence), sous réserve de vérifier l’éventuelle condition.

En le disant, on peut trouver que justement cette notation ressemble trop à celle des règles ordinaires et favorise la confusion entre les deux. Une règle d’équivalence peut avoir une condition, comme une règle ordinaire, mais contrairement à une règle ordinaire, elle a deux têtes. Ce seul fait pourrait suffire à la distinguer, s’il était mieux affiché. Peut‑être que finalement la notation infix, c’est à dire avec un opérateur entre les deux termes, serait préférable. Cette notation séparerait nettement les deux termes, rendant bien l’idée que ce type de règle a deux têtes (et que ce n’est pas une conjonction) :


(cons A (cons B R)) == (cons B (cons A R)) : (list R).

(cons A (cons A R)) == (cons A R) : (list R).

L’égalité, peut continuer à être notée (= A A) ou (eq A A), elle correspond exactement aux règles ordinaires.

Comment poser l’exhaustivité des solutions, quand elles peuvent être en nombre infini ? Surtout avec un langage constructiviste (dans le sens de « n’existe, que ce qui est constructible ») … Se limiter aux cas des ensembles de règles non‑récursives serait trop limité et la récursion n’implique pas toujours la récursion infinie. Limiter la preuve à celle que les termes constants qui sont des solutions sont effectivement vérifiés et ne le sont jamais dans le cas contraire, ne couvrirait que trop peu : ni la recherche de plusieurs solutions ni les requêtes avec des variables. Pour certains ensembles infinis de termes, les hypothèses pourraient être une idée (elle peuvent représenter des ensembles infinis de solutions à des termes en particulier), mais je ne me souviens pas avoir vu une telle chose dans les sémantiques standards vaguement abordée précédemment. Cette représentation pourrait quand‑même nécessiter de distinguer les récursions infinies des autres, parce que si des règles récursives produisent un ensemble fini de solutions, il serait compréhensible de préférer une représentation en extension de cet ensemble fini.

Si cet ensemble de solution ne peut pas être représenté, l’équivalence a commencé à être introduite pour rien, au moins pour le moment, parce qu’elle a un intérêt par ailleurs.

À moins qu’aucune ne convienne et qu’il faille en redéfinir une autre (par exemple en permettant que des hypothèses apparaissent dans les solutions), sur les sémantiques standards, ces documents qui avaient été présentés, seraient à revoir̄ :

• Herbrand Semantics (inria.fr), Michael Genesereth, Eric Kao, 2009 ?
• Tarskian Semantics, or No Notation Without Denotation (wiley.com) [PDF], Drew MacDermott, 1978.

En supposant que l’ensemble des solutions à des règles puisse être représenté en utilisant des hypothèses, alors cette représentation de l’ensemble des solutions existe déjà implicitement, dans la preuve de la satisfiabilité des règles comme elle a été définie : sous une forme générale avec des hypothèses.

Alors rien d’autre à ajouter et pas besoin d’équivalence (pour le moment) ? Il faudrait quand‑même montrer que l’ensemble des solutions ainsi représenté, est exhaustif, ce qui ne devrait pas être irréalisable.

Mettre cette interprétation en rapport avec celles déjà existantes, serait quand‑même intéressant, même si ce n’est pas une nécessité absolue, surtout pour un langage supposé pouvoir être abordé sans études spécialisées préalables, en partant du sens courant et de notions abstraites vu tôt en maths, vers la fin du collège. Malgré ça, un éventuel pont vers les sémantiques déjà existantes, reste intéressant, à condition qu’il soit assez naturellement faisable.

Avant de poursuivre avec la sémantique, une rapide réponse à cette importante question dans la citation, qui avait été laissée sans réponse, alors qu’elle en avait une, seulement pas encore écrite.

La question était celle‑ci : en relaxant la règle faisant qu’un terme commence toujours par une constante, une variable peut se trouver à cette place ou même à la place d’un terme externe. Ce faisant, elle peut se trouver en même temps à la place d’un terme externe, désignant donc une condition et à la place d’un terme interne, n’ayant pas ce rôle mais plutôt un rôle de « valeur », dans un sens informel et intuitif. La question était de savoir s’il faut voir un problème dans cette possibilité possiblement inquiétante.

Personnellement, j’ai cherché en vain un exemple de cas pouvant poser un problème insoluble. Ne voyant pas du tout comment aborder la question de produire un cas posant problème, est venu l’idée de reformuler la question autrement : si l’incohérence est qu’une chose puisse en désigner une et une autre à la fois, alors cette possibilité d’avoir une variable à la place d’une constante de relation ou à la place d’un terme externe, peut‑elle produire une telle incohérence ?

La réponse est étonnamment simple et brève : non, parce que l’unification ne le permet pas. C’est tout.

En fait, il reste une possibilité d’incohérence, mais elle ne serait pas dans le langage, elle serait dans l’interprétation de ses formules. Si une interprétation tient deux constantes pour différentes malgré qu’elles aient le même nom, parce que l’interprétation suppose qu’elles ne peuvent pas être confondues étant donné qu’elles se distinguent par leurs positions, alors là oui, une constante peut désigner une autre chose que ce qu’elle est supposée désigner, mais seulement dans l’interprétation.

Ce dernier problème a une solution simple : ne jamais donner un même nom a deux choses qui sont différentes. Donner des noms identiques a des notions différentes reste possible, ça ne produit pas automatiquement d’incohérence, mais ne jamais donner un même nom à des notions différentes, garanti que ça n’arrivera pas.

Ces remarques seront importantes pour la suite, qui reviendra sur la sémantique.

Le lien “ Natural Semantics ” a été supprimé, il portait sur une sémantique opérationnelle, ce qui est trop éloignée de la sémantique du langage décrit ici. Ce n’est pas que le langage décrit ici, s’oppose à une sémantique opérationnelle, il est même prévu qu’il puisse les formuler, c’est seulement qu’il n’a justement pas de sémantique opérationnelle, volontairement.

Pour la sémantique de Tarski, ce lien la décrit mieux que celui donné plus haut : Tarski’s Truth Definitions (plato.stanford.edu), 2001-2018.

Mais inutile de lire ces documents en détails pour comprendre de quoi il est question ici, aucune de ces deux sémantiques ne conviendrait. Ça apparaît comme évident dès les premiers paragraphes. Les raisons seront expliquées plus tard.

Le pont éventuellement envisagé ne sera pas fait, il ne se ferait qu’en cherchant les similitudes et les différences, ce qui n’aiderait pas la compréhension, même au contraire. Au lieu de ça, les principales incompatibilités seront rapidement décrites et une tentative de définition d’une autre sémantique sera commencée, sans savoir si elle existe déjà et si oui, quel nom elle a peut‑être.