Les logiques : notes en vrac

Précédemment, il avait été dit que l’ensemble des inférences appliquées pendant la vérification ou la recherche de solution, se comprennent mieux comme une chaîne que comme un arbre. Ce qui est expliqué dans ce message, devrait le faire percevoir. À tout moment, l’état d’une recherche de solution ou d’une vérification, peut se représenter comme un triplet : une chaîne d’inférences, un contexte, une conjonction à résoudre. La chaîne d’inférences est initialement vide, la conjonction est initialement celle de la requête. Le contexte évolue avec l’application de chaque règle, comme précédemment expliqué.

— Édit — Plutôt qu’un triplet, un quadruplet, le quatrième élément étant l’ensemble des règles.

D’abord, un rappel des règles de la relation poly, reprise de précédents exemples. Il y a juste un petit ajout dans la notation, un ajout qui se montrera utile plus loin. Le symbole § signifie le nom ou l’étiquette d’une règle, une alternative parfois plus commode que la notation #n désignant une règle par son index. Ces détails de notations ne changent rien à la sémantique.

§d0 (digit 0).
§d1 (digit 1).
§d2 (digit 2).
§poly-b (poly (p N)) : (digit N). -- b comme base
§poly-s (poly (p M N)) : (poly M) & (digit N). -- s comme succ

Une des solutions de la requête :

(poly P) ?

est :

P = (p (p 1) 2)

qui est associée à cette chaîne d’inférences, finale :

§poly-s §poly-b §d1 §d2

qui de manière détaillée, se lit ainsi :

La chaîne d’inférences est initialement vide. La conjonction à résoudre est initialement (poly P). Pour résoudre le premier (et initialement seul) terme de cette conjonction, la règle §poly-s est utilisée. Il est noté que §poly-s a été appliquée, la chaîne d’inférence initialement vide, devient §poly-s. En même temps, (poly P) est remplacé par (poly M) & (digit N). Il y a maintenant deux termes à résoudre. Pour résoudre (poly M), la règle §poly-b est utilisée. Il est noté que §poly-b a été appliquée, la chaîne d’inférence est donc maintenant §poly-s §poly-b. En même temps, (poly M) est remplacé par (digit N), la conjonction à résoudre est donc maintenant (digit N_1) & (digit N_2). Pour résoudre (digit N_1), la règle §d1 est utilisée. La chaîne d’inférence est maintenant §poly-s §poly-b §d1. En même temps, (digit N_1) est remplacé par rien, comme le corps de §d1 est vide, la conjonction à résoudre est donc maintenant (digit N_2). Pour résoudre (digit N_2), la règle §d2 est utilisée et la chaîne d’inférence est maintenant §poly-s §poly-b §d1 §d2. Comme le corps de §d2 est vide, (digit N_2) est remplacé par rien et il ne reste plus rien à résoudre, la résolution est totalement achevée, et la chaîne d’inférences associée à la résolution complète, est §poly-s §poly-b §d1 §d2, comme rapporté plus haut.

L’intention n’est que de donner une idée de la signification d’une chaîne d’inférences à partir d’une conjonction initiale, le contexte n’est pas rapporté pour ne pas alourdir ce qui est déjà pénible à lire.

Ce qui est décrit là, excepté pour la notation, peut s’appliquer en principe au Prolog standard, bien que j’ignore s’il existe des interpréteurs Prolog permettant de conserver et/ou de re‑vérifier une telle chaîne d’inférences.

On peut remarquer que l’ordre des règles n’a pas d’importance, pour une telle chaîne d’inférences, mais l’ordre des termes dans le corps d’une règle, a lui, une importante, pas pour la logique (le contraire est été formellement justifié précédemment), mais pour l’application de la chaîne d’inférences. En effet, chaque référence de règle ajoutée en bout de chaîne, s’applique au premier terme de la conjonction restant à résoudre. Si on voulait permettre de traiter les termes d’une conjonction dans un ordre libre, il faudrait que les éléments de la chaîne, renseignent aussi sur l’indexe du terme en question, en plus de renseigner sur le nom ou l’index de la règle appliquée. Ceci s’éloigne déjà de la sémantique du Prolog standard, mais cette possibilité a pourtant un sens et une utilité. On peut quand‑même remarquer qu’un ordre d’application standard pour les termes, permet d’avoir des chaînes d’inférences faisant l’économie de cette information supplémentaire, ce qui est une propriété appréciable pour une représentation canonique. Une chaîne d’inférences résolvant les termes dans un ordre libre, peut toujours être convertie dans une telle représentation canonique.

Pour ce que j’en sais, le Prolog standard ne permet pas de choisir quelle règle est appliquée à quelle moment, l’exemple qui va venir, est donc un écart supplémentaire.

Quand la relation poly a été introduite comme exemple, il avait été remarqué qu’en permutant les deux termes de la dernière règle, la recherche standard de solutions, ne permettait d’obtenir que des solutions dont les digits à droite étaient toujours zéro. C’est une bonne occasion de montrer ce que, dans les mêmes circonstance, permet la possibilité de choisir quelle règle est appliquée à quel moment.

Pour cet exemple, la dernière règle qui était :

§poly-s (poly (p M N)) : (poly M) & (digit N).

est changée en :

§poly-s (poly (p M N)) : (digit N) & (poly M).

Avec de l’attention, il devrait être possible de comprendre la séquence d’interactions ci‑dessous, qui ne sera pas détaillée pour rester bref. Le “ Rule? ” apparaissant plusieurs fois, est une invite permettant de donner le nom d’une règle. Il ne faut pas s’arrêter sur l’aspect trop austère des interactions ci‑dessous (il est possible de faire mieux, mais ce ne sera pas exposée ici), il s’agit seulement d’introduire le principe.



On peut remarquer que cette solution a put être produite, alors que la méthode de résolution standard ne l’aurait pas trouvé (rappel : les termes de la dernière règle ont été permutés).

Bien sûr, comme vu quand l’exemple poly avait été proposé, on peut toujours vérifier ce terme, même si la méthode de résolution standard ne permet pas de le trouver, et c’est sans surprise qu’il est associé à la même chaîne d’inférences que celle entrée au cours des interactions plus haut :

L’intention du message précédent n’était pas seulement de montrer qu’une chaîne d’inférences n’est pas un arbre même si une production d’une telle cette chaîne peut se faire au cours d’un processus similaire à celui de l’exploration d’un arbre (l’exploration d’un arbre n’est pas un arbre). Oui, ce n’est pas un arbre, mais ce n’est pas le fait central.

L’important est que cette chaîne est une preuve de quelque chose et que l’enregistrement de cette chaîne est une forme d’enregistrement de cette preuve. Comme la chaîne n’est pas facilement interprétable sans une conjonction initiale, une preuve serait plus concrètement une paire : une chaîne d’inférences et une conjonction, la chaîne étant la démonstration de cette conjonction. On peut imaginer que la chaîne soit interprétable même sans poser cette conjonction, ce qui reviendrait à chercher à savoir quelles sont les conjonctions vérifiables par cette chaîne d’inférences. La question est intéressante, mais à moins qu’il ne s’avère qu’elle a une utilité, elle n’est que relevée et à priori il ne sera pas tenté de lui trouver une réponse.

Il faut créer une méthode de validation de cette paire, pour qu’il ne suffise pas de la poser arbitrairement (cette méthode est réalisable sans poser de problèmes particuliers).

— Édit — La paire chaîne d’inférences et conjonction, peut sembler insuffisante pour représenter une preuve, si on note que la validation d’une preuve part d’un contexte initial. Mais le contexte initial peut être toujours vide, si la conjonction est complétée de manière à inclure les termes suffisants pour récréer un contexte donné ; dans ce cas, la chaîne d’inférences doit aussi être complétée en conséquence.

Ces chaînes d’inférences sont composables. Si on a une chaînes d’inférences S1 démontrant une conjonction C1. Si au cours de la démonstration d’une conjonction C2, on arrive à un moment à un état où on a une chaîne S3 et une conjonction C1 C3 (devant être compris comme une concaténation), alors la chaîne S1 peut être utilisée pour résoudre le fragment C1, ce qui aboutit à la chaîne S3 S1 (devant être compris comme une concaténation) laissant C3 à prouver. Ceci signifie qu’une preuve peut éventuellement être utilisée dans les démonstrations d’autres preuves, mais ça doit toujours être validé.

Le message suivant est séparé de celui‑i, parce qu’il aborde une question en rapport mais différente.

Jusque là, une limite n’a pas été dite mais peut se deviner : la conjonction à prouver peut être constante ou contenir des variables et si elle contient des variables, ces variables doivent être associées à des valeurs, des valeurs parmi d’autres. Ce que ça signifie, c’est qu’on ne peut pas prouver un terme sans fixer ses variables avec des valeurs particulières, ce qui signifie qu’on ne peut pas le prouver comme une certaine généralité.

Ce qui manque peut être rendu perceptible par un exemple. Si on reprend les règles pour la relation nat :

§nat-b (nat z).
§nat-s (nat (s N)) : (nat N).

Pour prouver que (nat (s N)), il faut prouver (nat N), et par là, donner une valeur à N, mais plusieurs valeurs sont possibles pour N. On ne peut pas jusque maintenant, prouver (nat (s N)) étant donné (nat N) quelque soit N. Il faudrait pouvoir poser (nat N), comme une hypothèse.

Mais de quelle manière ? Une idée naïve pourrait être d’ajouter une règle temporairement, par exemple :

§nat-b (nat z).
§nat-s (nat (s N)) : (nat N).
§hyp (nat N).

C’est naïf, parce que ce serait unsound. Cette interprétation de la notion d’hypothèse pourrait faire passer n’importe quoi pour un nat, y compris d’ailleurs un N qui ne serait même pas le N en particulier mais variable qu’on pourrait vouloir dire. Cette remarque reste vraie même si cette règle n’était ajoutée que le temps d’une démonstration, parce que le temps de cette démonstration, cette inopportune règle serait accessible à tous les termes correspondants à son schéma. C’est donc une mauvaise idée à exclure.

Une autre idée est de marquer ce (nat N) comme n’ayant pas besoin d’être prouvé. Il faut noter que ça n’en fait pas une règle, juste un terme n’ayant pas besoin d’être prouvé ; il n’est ainsi pas possible de faire passer n’importe quoi pour un nat comme avec la mauvaise idée précédente.

Mais en posant (nat N) comme un terme n’ayant pas besoin d’être prouvé, quel est le status de la variable N y apparaissant ? La question est d’autant plus importante que ce N peut apparaître ailleurs que seulement dans ce terme. Ce N ne peut pas être interprété comme lié à Any, sinon se poserait le même problème qu’avec la précédente mauvaise idée. Ce N ne peut pas être lié à une valeur en particulier, sinon l’hypothèse perd son caractère général et n’a donc plus le même sens. Je n’ai pour le moment pas de réponse finalisée à proposer à cette question, mais la question a une valeur en elle‑même, pour la conscience de ce qu’implique la notion d’hypothèse, ici au moins (ailleurs, je ne sais pas).

Suite du précédent message.

Une piste de réponse à ce que pourrait être le status de la variable, serait de poser ce qu’elle représente. Elle est une certaine variable apparaissant dans un certain terme qui est en fait la tête d’une règle. Cette association pourrait être représentée par une constante spéciale, spécifique à l’emplacement en question dans le terme en question.

Par exemple étant donné une règle (r X) : … , poser le terme (r Y) comme une hypothèse, correspondrait à quelque chose comme Y = c, où c désignerait la variable ou même le terme X apparaissant dans (r X). De cette manière, (r Y) pourrait correspondre à (r X), mais sans que Y ne puisse être associée à autre chose (une variable liée ne pouvant plus l’être à nouveau). Ça n’empêcherait pas de pouvoir y lier une autre variable, comme par exemple avoir Z = Y et dans ce cas, Z serait traitée comme Y, comme Z serait liée à la même chose que Y.

Un terme posé comme hypothèse devrait pouvoir correspondre à plusieurs têtes de règles, c’est inévitable. Cette constante spéciale devrait donc pouvoir correspondre à ces multiples emplacements, sans permettre de les distinguer (garanti par le fait que c’est une seule et même constante), ce qui est nécessaire, sinon le sens du terme posé comme hypothèse, ne serait plus le même (une généralité).

Si la variable apparaît dans plusieurs termes également posés comme hypothèse, ça se complique. Peur‑être faudrait‑il commencer en excluant ces cas, en les tenant d’abord pour non‑supportés.

Les termes posés comme hypothèses peuvent aussi être effectivement réalisables ou pas. Poser comme hypothèse un terme non‑réalisable, peut poser un problème de signification. Mais distinguer ce cas nécessite un niveau de langage permettant de parler des propriétés des termes et des règles, et il peut être intéressant de commencer en s’en passant. Ça peut être intéressant d’abord pour ne pas poser tout en même temps (généralement mauvais) et aussi parce qu’il peut être intéressant de faire le maximum possible sans nécessiter un niveau de langage supplémentaire, même s’il finira évidemment pas être nécessaire.

En parlant de niveau de langage supplémentaire, ce qui a été présenté comme se déroulant comme une démonstration dans un précédent message, repose entièrement sur les seules constructions du langage objet lui‑même. L’idée de pouvoir poser un terme comme hypothèse, peut garder cette propriété, temps qu’on exige pas de vérifier que le terme en question est réalisable. C’est d’ailleurs le seul intérêt qu’il y a à ne pas l’exiger (celui de se passer d’un niveau de langage supplémentaire, d’abord au moins).

En parlant de constructions dans le langage objet, poser un terme comme hypothèse et construire des terme à partir de cette hypothèse, pourrait être décrit comme une application partielle de certaines règles.

— Édit — Ce message est à la fois sur une bonne piste mais à la fois sur une mauvaise piste, pour une raison qui se expliquée plus tard.

Le précédent message est en partie mal formulé. Reprise ici, avec quelques rappels pour resituer le propos.

Note : ceci n’a plus rien à voir avec le principe de base Prolog, même si ça en dérive. Si c’est rapporté malgré tout, c’est pour l’intérêt que ça présente comme système de démonstration. Le but de ces explications n’est que d’introduire une idée, d’expliquer son intérêt, pas de donner tous les détails de la mise en œuvre.

Il a été remarqué que certains termes, pour être vérifiés en général, nécessiteraient de produire une infinité de solutions, alors que ces termes pourraient être vérifiés sans générer cette infinité de solutions, pourvu qu’un ou des termes tenus pour généraux, puissent être posés comme hypothèse. Un tel terme est supposé vérifié, sans donc procéder à sa vérification. Cette possibilité de poser des termes comme hypothèse, serait réservée aux requêtes (et peut‑être utile à un autre niveau de langage pas encore introduit), pour conserver la propriété qu’ont les règles de définir des constructions concrètes et ainsi ne pas changer leur sens. Le sens des requêtes serait modifié dans le sens où les requêtes permettraient de vérifier des faits en général, sans pourtant nécessiter un autre niveau de langage, simplement en appliquant les seules règles de construction du langage objet, moyennant une extension de celui‑ci, par l’ajout d’un type de valeur dont l’unification doit tenir compte. Il ne serait peut‑être pas insensé de permettre ces termes posés en hypothèse, dans le corps des règles (juste certainement pas la tête), mais il faudrait se poser la question de leur status. Ce ne serait pas insensé, parce qu’une requête peut être « enregistrée » sous forme d’une règle et qu’une règle, c’est après‑tout une sorte de requête.

Détails sur l’interprétation et le traitement des termes posés en hypothèse.

Si le terme (r X) est posé comme hypothèse, le X est n’importe quel X vérifiant (r X) qui est supposé réalisable (cette question sera abordée à une autre occasion). Ce X qui est n’importe quel X vérifiant (r X), ne doit pas être lié à un terme, car il doit rester une généralité ; il est au lieu d’être lié à un terme, lié à une position dans un terme. Dans ce précédent exemple, sa position est le premier terme de la relation. Si le terme posé en hypothèse était (r b X), le terme (r c X) ne peut pas être unifié avec, mais le terme (r Y X), le peut, si Y peut être lié à b. Le terme (r a X) peut aussi être unifié avec (r a Z), si Z peut être lié à X, auquel cas Z désigne la même chose que X, c’est à dire non‑pas un terme, mais une position dans un terme. Dans (r (a b) X) et (r Y X), les deux X ont la même position, de même que dans (r (a b) (c X)) et (r Y (c X)). Si un (r X) est un terme posé en hypothèse, il ne peut pas être unifié avec (r a), parce que X ne peut être lié qu’à une position dans un terme. On peut comprendre que ce X ne peut être lié qu’à une autre variable et que cette variable doit être soit libre soit désigner la même chose, c’est à dire la même position dans le même terme. Si (r X) et (r Y) sont deux termes posés en hypothèse, ils ne sont pas unifiables, parce que ce ne sont pas les deux mêmes termes, X et Y n’ayant pas de valeur, signifiant n’importe quelle valeur vérifiant (r X) et (r Y) respectivement, X et Y ne peut peuvent être ni dit égaux, ni dit différents. On peut comprendre par là que deux termes posés en hypothèse, ne sont jamais unifiables. La question ne se pose d’ailleurs pas, parce que pour que la question se pose, il faudrait qu’un terme posé en hypothèse, puisse être la tête d’une règle, ce qui n’aurait pas de sens, comme le sens d’un terme posé en hypothèse, est de supposer que le terme est vérifié, sans le vérifier, sans générer les solutions qui lui correspondent. Si seulement l’un des deux termes (r X) et (r Y) est posé en hypothèse et pas l’autre, ils sont potentiellement unifiables, comme expliqué plus haut.

Que se passe‑t‑il si ce X apparaît dans un terme lié par une variable ? Par exemple si on a (r a (c X)) en hypothèse et qu’on ai par ailleurs aboutit à un contexte dans lequel Y = (c X) ? Il faudrait que X attende de Y, d’être à la position qu’il aurait dans un terme comme (r a Y). Même si ce Y n’apparaît pas dans un terme posé comme une hypothèse, par le fait qu’il contient un X qui ne peut être lié qu’à une position dans un terme, Y est mécaniquement contraint lui aussi, à ne pouvoir être lié qu’à une position dans un terme, mais pas nécessairement un terme posé en hypothèse. La position que Y doit avoir dans le terme cible, peut se déduire de la position relative que X a dans le terme lié à Y. Si on a d’abord rencontré X dans le terme posé comme hypothèse, et qu’on rencontre ensuite une situation impliquant Y = (c X), on sait que Y doit être lié à une position dans un terme plutôt qu’au terme (c X). Mais si Y est rencontré avant, il faudrait en plus de lier Y à (c X), noter également la provenance de ce (c X), au cas où. Ça pourrait définir je crois, mais ce serait lourd à traiter (rechercher tous les termes liés dans lesquels X apparaît et revoir les liaisons des variables en conséquence) et on peut en faire l’économie en choisissant de toujours traiter les termes posés en hypothèse, avant les autres.

Il faut noter que le principe général de l’unification est préservé, mais qu’on introduit un nouveau type de valeur à côté des constantes, tuples et variables. La logique de l’unification ne change pas. Une variable ne peut être liée à une autre que si elle peuvent désigner la même chose. Une particularité apparaît pour les variables, qui est qu’une variable apparaissant dans un terme posé en hypothèse, n’est pas initialement liée à Any, mais immédiatement (et toujours seulement) liée à sa position dans le terme dans lequel elle apparaît. Pour la raison expliquée plus haut, les termes apparaissant en hypothèses, sont traités avant les autres, pas pour une raison de logique mais une raison de commodité, d’économie de calcul et de complexité.

Le cas où une variable apparaît dans plus d’un terme posé en hypothèse, n’est pas abordé et reste exclus pour le moment.

La mise en œuvre de ces idées n’a pas encore été testée. Ces explications sont informelles, mais elles sont assez détaillées. Il faudrait se préoccuper de savoir si une incohérence potentielle s’y cache ou pas.

— Édit — Ce message est à la fois sur une bonne piste mais à la fois sur une mauvaise piste, pour une raison qui sera expliquée plus tard.


Il y a une erreur ici. Si (r X) est une hypothèse, elle ne peut pas être unifié avec (r a) dans le sens où l’unification associerait X à a, mais l’hypothèse (r X) ne doit pas moins être correspondante à (r a), sinon (r X) n’est plus une généralité.

Tout ça devrait pouvoir se formuler plus clairement. Il semble au moins qu’il faille distinguer unification et correspondance.

Reste encore un problème. Dans ce qui a été appelé un terme posé en hypothèse, toutes les variables sont considérées comme des généralités, alors que ça ne devrait probablement pas être le cas. Par exemple une conjonction comme (eq Y b) & (r X Y), où (r X Y) est une hypothèse (sans notation encore pour le moment) devrait être possible, Y gardant sont status de variable normale et seulement X étant une généralité. Vu l’importance des variables, c’est peut‑être plus la variable X qui devrait être distinguée, plus que le terme (r X Y). Pourtant, il faut définir ce qu’est la généralité que représente X, alors le terme (r X Y) doit être distingué aussi.

Intuitivement, l’idée semble simple (tenir un terme pour vérifié, sans le vérifier, et faire des vérifications sous cette hypothèse), mais semble difficile à définir avec assez de précision pour être mise en œuvre.

Les seules choses certaines et pouvant se poser clairement sont : une variable représentant une généralité, n’est jamais liée à un terme, seulement à une position dans une relation (le terme de la relation, pas la constante), elle est correspondante à n’importe quel terme à cette même position, mais sans jamais être liée avec ce terme, elle ne représente aucun de ces termes en particulier, mais potentiellement n’importe lequel et un seul (mais toujours aucun en particulier), elle ne peut pas correspondre à une autre variable représentant une généralité désignant une autre position, elle correspond à une autre variable représentant une généralité, désignant la même position, auquel cas les deux variables représentent le même terme (mais toujours inconnu en particulier).

Pour le moment, le cas où une telle variable a plusieurs occurrences dans une relation posée en hypothèse, est omis, c’est déjà assez compliqué comme ça.

— Édit — Ce message est à la fois sur une bonne piste mais à la fois sur une mauvaise piste, pour une raison qui sera expliquée plus tard.


Ça implique que ce que cette variable désigne, n’est défini qu’une fois et toutes les autres occurrences de cette variable désigne la même chose (une seule chose mais inconnue en particulier). Cette position devrait être distinguée. Je n’aime pas trop ce symbole, mais le symbole @ pourrait convenir, comme il se lit “ at ”, ce qui colle bien à l’idée d’une position. Ça répond finalement à la question du cas où la variable a plusieurs occurrences : une seule de ces occurrence désigne cette position correspondant au terme unique mais quelconque qu’elle désigne. Par exemple si la relation eq précédemment présentée, était utilisée dans une hypothèse, (eq @X X) aurait un sens et d’ailleurs (eq X @X) aurait le même sens. Dans une conjonction, une seule occurrence d’une variable pourrait être décorée avec ce @. Plusieurs variables pourraient être ainsi décorée, mais chaque fois, pour une seule de leurs occurrence. L’occurrence décorée pourrait être la seule occurrence.

La description jugée assez certaine dans le précédent message, ne tourne finalement que autour des variables, elle ne parle finalement que peu des termes. Il a été dit que dans un terme posé en hypothèse, des variables normale devrait pouvoir apparaître. Ces deux points semblent suggérer que l’idée de pouvoir poser une relation comme hypothèse, devrait plutôt se formuler comme l’idée de poser une variable avec une valeur quelconque, comme hypothèse. Par exemple dans (r @X), ce ne serait pas tant (r @X) qui serait posé en hypothèse, que la présence de @X qui en ferait une hypothèse. Ce qui fait l’hypothèse, ce n’est pas la relation ainsi posée, c’est le status de la variable qui s’y trouve.

Au passage, quand je parle d’hypothèse, je penses en fait plus à une généralité (une variable avec une valeur en général mais aucune posée en particulier), mais que j’appel une hypothèse, parce que je crois que ça y correspond bien.

— Édit — Ce message est à la fois sur une bonne piste mais à la fois sur une mauvaise piste, pour une raison qui sera expliquée plus tard.

Effectivement, ce sont les variables qui sont au cœur de la question.

L’idée de pouvoir poser des termes comme hypothèse, n’est pas venue en pensant à inclure des termes entièrement constants, ce qui n’aurait été éventuellement qu’une étrangeté en marge.

Intuitivement, il est plus facile de penser à poser un terme en hypothèse, mais au fond de cette pensée, on se préoccupe surtout des variables, et c’est en envisageant le cas inattendu d’un terme constant posé en hypothèse, qu’on peut s’en apercevoir. Finalement, pourquoi l’idée de poser des termes en hypothèse a‑t‑elle été introduite en premier lieu ? Ben, pour faire des démonstrations en général sans avoir à lister tout un ensemble de solutions, sachant que cet ensemble peut être infini, ce qui pose problème à la dite démonstration. Et par quoi ce problème vient‑il, si ce n’est par les variables ?

Le seul sens utile que j’imagines, que pourrait avoir de poser un terme constant comme hypothèse, serait de vouloir le considérer démontré sans ce soucier des chaînes d’inférences éventuellement multiple pouvant le démontrer. C’est à noter, ce n’est pas un mauvais point, mais ce n’est pas le sujet actuel.

L’idée derrière cette intuition était en fait celle de variables hypothétiques, un terme n’étant hypothétique que parce qu’il contient une ou des variables hypothétiques.

Ça commence enfin à s’éclaircir un peu …

— Édit — Ce message est sur une mauvaise piste, il est quand‑même conservé pour ne pas oublier une intuition tentante mais menant à une impasse.

À propos de la possible notation, seulement.

Si cette variable désigne la même chose partout, elle n’a en théorie même pas besoin d’être décorée et pourrait être déclarée comme étant une variable ayant ce status dans toute la conjonction. Par exemple au lieu de choisir entre écrire (eq @X X) ou (eq X @X), il serait possible de déclarer X comme ayant le status particulier d’être une variable hypothétique et d’écrire (eq X X) ou même de ne pas déclarer X et d’écrire (eq @X @X), c’est à dire de décorer toutes les occurrences de X ; le sens serait le même, après‑tout. Mais je trouve préférable d’en rester à (eq @X X), parce que plus directement compréhensible et syntaxiquement plus simple. Ajouter la possibilité de déclarer X comme ayant un status particulier, encombrerait une syntaxe qui se réduit à décrire des termes et qui est bien ainsi. L’écriture (eq @X @X) est moins évidente à mettre en balance avec (eq @X X). D’un côté, elle est moins arbitraire, mais d’un autre côté, elle souligne moins le principe que X est un certain terme en particulier mais inconnu, la notation (eq @X @X) laissant moins sentir que X désigne un terme en particulier, ce qui ressort mieux avec (eq @X X), mais cette dernière notation à l’inconvénient d’être arbitraire, comme elle pourrait aussi bien être (eq X @X). Il faudrait trouver une raison justifiant un choix entre ces deux options. Un avantage de l’option de décorer un seul terme, pourrait être de permettre de souligner une position en particulier dans un terme, si souligner cette position peut aider à comprendre le sens de la conjonction concernée ; cette option apporte un plus d’expressivité, même si c’est informel (comme ça ne change pas le sens). Mais ça peut être trompeur aussi, si on voit partout X sans remarquer son occurrence décorée, @X.

Il y a une distinction syntaxique lisible entre les constantes et les variables. La distinction entre les relations et les constructeurs et moins flagrante, mais elle se voit. Il faudrait une distinction lisible entre ces deux types de variables, sans alourdir la notation. Se pose la question du problème des homonymie entre ces deux types de variable, un problème qui se pose déjà avec les constantes de relation et les constantes de constructeur. Si ce qui est appelé ici les « variables hypothétiques » sont toujours décorées, la distinction est aussi immédiate que entre les constantes et les variables, mais ajouter ce décorateur partout pourrait être lourd, à moins d’en trouver une représentation moins encombrante que @ et qui ne soit pas trop surprenante.

— Édit — Ce message est sur une mauvaise piste, il est quand‑même conservé pour ne pas oublier une intuition tentante mais menant à une impasse.

Peut‑être que l’option de décorer la variable partout, serait la meilleure, mais ça nécessite une explication.

Si la variable peut apparaître à plusieurs endroits, ça signifie que les termes à tous ces endroits, sont égaux (ou au moins doivent l’être). C’est la sémantique normale. Mais il se pose aussi la question de l’équivalence des positions dans les termes, et décorer la variable à tous ces endroits, équivaudrait à dire que toutes ces positions sont considérées comme équivalentes. Ne pas le considérer automatiquement ne serait pas un problème et permettre de le dire explicitement et donc sélectivement, pourrait ouvrir des possibilités.

Par exemple (eq @X @X) signifierait que les deux positions sont équivalentes, mais (eq @X X) signifierait que le second X est lié à un terme pouvant se trouver à la même position que le premier terme, mais sans considérer les deux positions comme équivalentes. Si toutes les positions auxquelles le terme apparaît doivent être considérées comme équivalentes, il faut seulement décorer toutes les occurrences de la variable. Implicitement, ça signifie qu’il n’y a pas d’espaces de noms séparées pour deux types de variable, seulement que les variables peuvent éventuellement être liées à l’origine d’un terme, pas toujours à un terme.

Précédemment, il a été dit que pour supporter ces variables représentant un terme en général quelque soit sa valeur effective, il faudrait que chaque liaison d’une variable à un terme, se souvienne de l’origine du terme (même quand la variable n’est pas liée à cette position) et que comme ce serait coûteux, qu’il faudrait l’éviter. Finalement, peut‑être qu’il ne faut pas y voir un problème. Se souvenir des origines des termes auxquels les variables sont liées, pourrait présenter un intérêt pour l’analyse des solutions aux requêtes. Évidemment, ce serait excessivement coûteux si on voyait le principe de base de Prolog comme un langage de programmation, mais c’est un coût acceptable si on le voit comme un langage de formulation, interrogation et analyse.