Les logiques : notes en vrac

Encore un dernier complément au précédent message, avant de passer à la suite plus tard.

Cette composition horizontale, pourrait aussi être appelée la relation (*) Ça peut surprendre, après avoir d’abord qualifié de relation, le terme le plus englobant de la tête d’une règle puis avoir fait remarquer que ce qui avait été appelé des constructeurs dans les termes internes des termes en général, pourrait être qualifié de relation aussi. Ça n’est pourtant pas étonnant, justement pour la raison que dans les deux cas, c’est cette composition horizontale, qui y exprime une relation.

(*) Sa cousine, la composition verticale peut de son côté être appelée, imbrication, comme déjà fait dans le précédent message.

Dans « (nat (s N)) », il est établit une relation entre le terme « (s N) » et la notion d’entier naturel, représentée par la constante nat. Dans le terme « (s (s z)) », le terme « (s z) » et mis en relation avec son successeur, plus exactement, sous cette successeur, la notion de successeur étant représentée par la constante s et de même, z, représentant le zéro ou la cas de base, est mis en relation avec cette même notion de successeur représentée par s. La seule chose qui distingue les deux relations, est la différence récemment re‑soulignée, qui est que le terme « (nat (s N)) » est sujet à substitution par le corps de la règle, « (nat N) », une substitution qui porte peut‑être mal son nom, comme sémantiquement, le terme « (nat N) » ne se substitue pas au terme « (nat (s N)) ». Ce qui fait diverger une n‑ième fois encore vers nouvelle question de vocabulaire : il faudra penser à trouver un autre nom pour cette notion, ça n’est pas une substitution, au moins, pas sémantiquement.

Une autre manière encore de voir cette composition horizontale ou relation, est d’y voir une notion d’axe, tandis que l’imbrication pourrait être vue comme une notion de dimensions, au pluriel. Si on a un repère dans l’espace, en trois dimensions, ou en deux dimensions, sur une feuille de papier, mais que la graduation de chaque axe est limitée à une seule position, par exemple zéro, alors on ne pourra rien y représenter, on pourrait même ajouter autant de dimension qu’on le veut, on aurait toujours rien de plus que cette unique position, juste sur un axe supplémentaire. C’est ce qu’il se passait dans le message précédent, avec la constante c qui ne pouvait que être imbriquée dans un plus ou moins grand nombre de parenthèses, rien de plus. Permettre d’ajouter quelque chose après c autant qu’on veut l’écrire, est l’équivalent d’avoir un axe avec plusieurs graduations, et ainsi sur l’axe de chacune des dimensions.

On comprend mieux pourquoi l’expressivité de la composition verticale est à ce point dépendante de l’expressivité de la composition horizontale et pourquoi la composition horizontale seule même sans composition verticale est beaucoup plus expressive que la composition verticale seule.

Il y a la question de l’ordre. Telle‑quelle, cette analogie a une limite, qui est que typiquement, on se représente un axe comme ordonné, mais ce n’est finalement pas une obligation, même si ça l’est dans la plupart des cas, comme pour un repère spatial. Disons qu’ils s’agit d’une notion d’espace pas habituel, avec des positions non‑ordonnées sur les axes, tandis que au contraire, les dimensions ont une relation d’ordre entre elles.

Ne pas oublier qu’avec cette notion, une solution unique pour les liaisons des variables, peut signifier plusieurs solutions pour le développement des variables en termes constants.

Ça suggère peut‑être que au lieu de z, la représentation du cas de base, devrait plutôt être (z). Parce dans (s (s z)), (s z) est sous la relation s, mais dans (s z), z n’est pas sous la relation s, il est au même niveau, ce qui me semble dissonant.

Corrigées, la représentation et les règles pour nat, seraient :

(nat (z)). -- Au lieu de (nat z).
(nat (s N)) : (nat N).

En plus, ça souligne bien le caractère récursif de nat.

Les questions laissées en suspend, sur la question de l’idée d’équivalence. Peu de réponse pour le moment.


Cette question restera en suspend jusqu’à ce que toutes les autres soient éclaircies.


La nécessité de l’équivalence a pour le moment été posée pour le besoin de formuler l’équivalence des ensembles de solutions renvoyés, pour l’interprétation. Elle pourrait être dans un premier temps, limitée aux termes produits par les résolutions et ne pas être appliquées aux termes sujets à validations, les termes externes. Sinon, pour diverger un instant, en parlant de conjonctions de termes : elles peuvent apparaître dans le corps d’une règle, dans une requête, qui est considérée comme un corps de règle à résoudre, mais pas comme tête de règle. La possibilité de formuler que des conjonctions de termes puissent avoir des conditions de validités spécifiques en plus de celles des termes individuellement qui les compose, peut être sensée, mais pas une nécessité, ce qui ne signifie pas qu’elle serait sans intérêt. Cette possibilité, qui aurait d’importantes conséquences sur la couverture des cas d’une hypothèse, restera en arrière plan, l’idée pour le moment étant que le langage soit assez expressif pour parler de lui‑même et parler de l’interprétation des solutions qu’il décrit.

Donc pour le moment, non, pas d’application des équivalences à des conjonctions de termes et les équivalences ne s’appliquent qu’à des termes produits comme solutions, pas à des termes substituables (si un terme peut être dans les deux cas, c’est le cas dans lequel il est qui compte). Une question reste quand‑même en suspend à ce propos : l’équivalence appliquée à des termes produits comme solutions, doit‑elle l’être seulement sur leur développement constants ou peut‑elle aussi l’être sur leurs représentations avec des variables ?


Il est nécessaire de pouvoir dériver des équivalences autres que celles posées initialement. L’équivalence ne doit pas participer à la résolution, parce qu’elle est un jugement sur le produit de la résolution, alors elle ne peut de toutes manières pas produire autre chose que de nouvelles équivalences, raison pour laquelle cette règle d’inférence ne peut que être nécessaire. Donc oui, il faut poser « A == B & B == C => A == C ». Il faudrait aussi poser « A == B => B == A » ; à moins que cette relation ne puisse se déduire ?


Oui, parce que c’est le cas de base de l’équivalence et même celui qui fait son sens. En fait, si (A = B) => (A == B) n’était pas vérifiée, l’équivalence serait incohérente. L’équivalence, c’est l’égalité après (ou à travers ?) une interprétation. Mais l’équivalence pourrait aussi être utilisée pour dire qu’une chose peut avoir plusieurs représentations équivalentes, ce qui finalement est une autre manière de dire la même chose. Si l’interprétation est représentée par une fonction f, alors dire que A est équivalent à B pour f, c’est dire que f de A est égale à f de B. Par ailleurs, cette relation entre l’égalité et l’équivalence, indique que l’équivalence peut devoir être associée explicitement, pour savoir l’équivalence vis à vis de quoi. Pour l’instant, l’équivalence n’a pas besoin de l’être, elle l’est implicitement, c’est l’équivalence des ensembles de solutions produits par les résolutions. Mais quand l’équivalence pourra être utilisée pour d’autre chose, si elle le sera, elle devra éventuellement être qualifiée ou peut‑être sera‑t‑il possible de s’en passer ou peut‑être y aura‑t‑il une autre notion d’équivalence avec un statut autre que celui de celle dont il est question pour le moment, mais ayant pourtant la même logique. Un exemple de ce cas est avec les ensembles. Ajouter un élément à un ensemble puis ajouter à nouveau le même élément à l’ensemble résultant ou ne pas l’ajouter une seconde fois, donne un résultat équivalent pour l’opération indiquant si un élément appartient à un ensemble. L’équivalence pourrait être une notion commode pour représenter ce fait, même s’il pourrait l’être d’autres manières. Avoir cette notion, permettrait peut‑être de simplifier les raisonnements à ce propos. La question du rapport des équivalences de ce type avec celle dont il est question pour le moment, devrait être étudiée : est‑ce la même, peuvent‑elle être confondues ? Doivent‑elles être distinguées parce qu’elles sont de nature différentes ou distinguées bien qu’elles soient de natures identiques ? Peut‑être d’autres questions encore.

Intuitivement, je crois que l’équivalence devrait être utile à décrire les interprétations au sens large. Dans le cas où une même chose peut avoir une infinité de représentations au moins en théorie, les regroupements par équivalence, seraient peut‑être plus qu’une commodité, une nécessité.

Il y a un an, en introduisant l’idée d’une notation pour prouver la satisfiabilité des règles, il a été remarqué qu’une colle se pose avec la règle de l’égalité.

La satisfiabilité générale d’une règle se prouve soit par une règle inconditionnelle précédente ou par une règle conditionnelle précédente, dont la satisfiabilité générale a déjà été démontrée. En fait, ces preuves pourraient être générées automatiquement. La notation explicite a surtout un intérêt pédagogique, et permet aussi de donner des exemples de satisfiabilité en particulier, pour illustration, ce qui peut aider la compréhension de certaines règles par des exemples.

Justement avec l’égalité, la preuve de la satisfiabilité ne peut se faire qu’avec des exemples en particulier, elle ne peut pas être prouvée en générale.

Précédemment, une relation a été souligné entre l’équivalence et l’égalité.

L’égalité qui était formulée par une règle comme les autres, devraient avoir un statut particulier, parce qu’elle est particulière. La raison est que sa satisfiabilité ne peut pas être prouvée en générale et que la notion d’unification suppose celle d’égalité. Définir une règle de l’égalité en se reposant sur l’unification, pour expliquer l’unification, a un intérêt pédagogique, mais n’est pas sémantiquement correcte, parce que l’unification repose sur l’égalité : l’égalité doit être posée avant l’unification.

Pour ces raisons, il faut donner à l’égalité un statut de notion fondamentale. Elle pourrait continuer à être noter comme les autres vérifications, excepté qu’elle se verrait attribuer une constante réservée, « = ». Au lieu de par exemple « (eq A B) », l’écriture serait « (= A B) ». Définir la règle « (eq A A). » resterait possible.

L’égalité ayant un status de notion fondamentale, l’équivalence est‑elle une notion dérivée ou malgré‑tout une notion fondamentale ?

Juste pour s’amuser, mais sérieusement, on peut trouver que ça fait vraiment une différence. Imaginons que l’on veuille que le zéro de nat soit plus abstrait, et qu’on le remplace par une variable ou un terme constant quelconque. En général, les règles fonctionneront toujours, parce qu’il est probable qu’elles n’interpréteront pas ce terme ou celui liée à la variable, à moins qu’il ne s’agisse d’un terme que les règles interprètent, justement. Si on remplace le z par un nat, par exemple « (s (s z)) », dans ce cas là, avec l’ancienne représentation, le zéro se trouverait pouvoir avoir un prédécesseur, une incohérence aurait été introduite. Avec la nouvelle représentation, ce n’est plus le cas, le concept de zéro est structurellement protégé d’une autre interprétation.

Ça fait une bonne raison de conserver cette nouvelle représentation, définitivement.

Avec l’idée de faire de la composition horizontale une notion fondamentale, vient la notion d’arité d’une variable. Cette notion n’existait pas avant.

Pour qu’une requête ne tente pas des unifications inutiles, surtout qu’elle pourrait éventuellement avoir plus d’options à tenter alors, il faudrait pouvoir poser qu’une variable est d’arité 1 ou d’une autre arité ou d’une arité variable, avant une requête avec cette variable.

Pour une arité fixe, il serait possible de d’abord lier la variable à un terme générique de la même arité. Si on considère que le nom spécial, Any, est d’arité 1, et que les nouvelles variables sont toujours initialement liées à Any par défaut, alors il n’y a rien de particulier à faire. Si on souhaite qu’une variable soit d’arité 2, alors il serait possible de préalablement la lier à un terme comme |Any Any|. Pour une arité variable, il faudrait introduire une autre version de Any, qui pourrait peut‑être s’appeler Any-N.

Mais dans ce cas, Any, d’arité 1, porterait mal son nom, et ce devrait plutôt être le nom du terme générique d’arité variable, qui correspondrait mieux à l’idée de “ anything ”. Dans ce cas, au lieu de Any, le terme générique d’arité 1, s’appellerait Any-1. Mais ce serait un peu lourd, comme ce serait le cas le plus fréquent, voir quasiment toujours le cas, en général.

Cette question du nom peut être laissée en suspend, elle n’est pas la plus importante. Ce qui est important, c’est que maintenant les variables ont une arité, fixe ou variable, et que ça a les conséquences mentionnées plus haut.

Ça peut s’objecter, c’est à voir. Soit deux termes différents avec chacun leur solution. Pour simplifier, on peut imaginer que cette solution est unique. Imaginons que ces deux termes solutions sont équivalents pour une interprétation quelconque. Il serait alors surprenant de ne pas considérer les deux premiers termes, ceux qui les produisent, comme équivalents aussi.

D’un autre côté, si l’équivalence indique une possible substitution, alors non, ce n’est pas surprenant. Si les deux termes solutions sont équivalents comme possible solution pour une variable d’un troisième terme à vérifier, alors on peut y substituer l’un ou l’autre des deux termes solutions, mais pas les termes dont ils sont une solution (les deux premiers termes).

Mais si l’équivalence est définie de telle sorte qu’elle vaille justement pour une tête de règle dans laquelle une substitution est possible, alors considérer les deux premiers termes comme équivalents, autant que leurs deux solutions, ne pose pas de problème, parce que ça ne signifie pas qu’on puisse les substituer à autre chose n’importe où.

En résumé et peut‑être plus clairement. Soit trois termes sujets à vérification, (r1 A), (r2 B) et (r3 C D). Imaginons que r1 ait pour solution unique A = a et que r2 ait pour solution unique, B = b. Imaginons que pour r3, C = a ou C = b, soient deux solutions partielles possibles, pour lesquelles le reste de la solution est D = d, dans les deux cas. Dans ce cas là, les constantes « a » et « b » sont équivalente pour r3. Cette équivalence doit porter d’une manière ou d’une autre, l’indication que cette équivalence vaut pour le C de r3. Comme « a » est l’unique solution de r1 et « b » est l’unique solution de r2, alors on a une équivalence de r1 et de r2 aussi. Mais cette équivalence ne permet pas de substituer C par (r1 A) ou par (r2 B) dans (r3 C D).

Que l’équivalence doive porter une indication de où l’équivalence est applicable, ne fait pas de doute. Reste à savoir comment le représenter. Que l’équivalence se propage à l’origine de termes équivalents, peut faire sens, mais pose question, mais il y a bien un lien entre les deux.

La question des équivalences est encore confuse, mais intuitivement, deux choses peuvent être pressenties.

Elles sont sujettes à des inférences et le langage a déjà un système d’inférence. Si c’est possible, l’idéal serait de réutiliser le même, parce que s’il fallait en réintroduire un nouveau spécialement pour les équivalences, ce serait inquiétant. Ce serait inquiétant parce qu’il faut que l’ajout de concepts pour compléter la langage afin qu’il puisse parle de lui‑même, il faut que ce processus aboutisse. Si le problème s’étend plus qu’il ne se réduit, ce processus risque de ressembler à une récursion infinie.

Les équivalences sont sujettes à inférence, ne doivent pas modifier les liaisons des variables ou les solutions. Ça pourrait indiquer qu’elles ne doivent pas avoir accès au contexte des résolutions. Pourtant, d’une égalité, on doit pouvoir conclure une équivalence et le contexte des résolutions, est constitué d’égalités entre variables et termes et d’égalités entre variables et variables. Les équivalences doivent pouvoir y accéder mais sans pouvoir les modifier.

Le passage de l’équivalence à la substitution, est intuitivement naturel, mais n’a pas été justifié.

Sans la substitution, l’équivalence serait peut‑être impraticable ou créerait probablement des situations pas idéales.

Un cas parmi d’autres, pourrait être celui où l’équivalence est utilisée pour démontrer qu’une mise en œuvre du langage est une interprétation conforme à la définition. L’ordre des règles et des termes a une importance en pratique, il serait possible d’avoir une procédure de résolution respectant cet ordre, en supposant que lui est donné une interprétation en marge de celle de la définition. Il pourrait rester intéressant d’avoir une procédure de résolution ne se souciant que de l’équivalence de ce qu’elle produit et se permettant de permuter l’ordre des règles ou des termes dans les corps de règle, pour diverses raisons pratiques. Sans la substitution, il faudrait, soit effectivement soit virtuellement, avoir une solution considérée comme solution de référence et de l’autre, une solution produite, dont il serait prouvé qu’elle est équivalent à la solution de référence. Ça pourrait éventuellement compliquer les choses et rendre l’équivalence impraticable. Un second problème serait qu’un terme quelconque se verrait donner un status particulier, alors que quand deux termes (ou plus) sont équivalents, aucun des deux n’est plus équivalent que l’autre. C’est informel, mais ça peut suffire à intuitivement faire pressentir que sans la substitution, l’équivalence poserait des problèmes à l’usage.

L’idée d’équivalence était déjà implicitement présente, même avant d’avoir été introduite pour parler de l’équivalence des solutions, mais elle l’était sous une forme plus abstraite.

Quand il a plusieurs fois été remarqué que des ensembles de règles peuvent signifier la même chose même s’ils n’utilisent pas les mêmes constantes ou le même ordre des termes, c’était une notion d’équivalence. Mais cette équivalence là, est plus abstraite, celle qui a été introduite, n’est pas préservée par les renommages de constantes ou les permutations de termes.

Introduire explicitement cette équivalence plus abstraite, pourrait être intéressant, mais ce n’est pas une nécessité (ou au moins, pas pour le moment).