Les logiques : notes en vrac

Précédemment a été définie une relation nat-lt, qui n’a de sens que entre deux termes vérifiant les définition de nat.

Faudrait‑il définir aussi une relation nat-eq ? Et puis pour la relation (eq A A) on ne s’est pas embarrassé de s’assurer que A vérifie une règle quelconque comme on l’a pourtant fait avec nat-lt. Justement, en parlant de cette relation eq, peut‑elle être utilisée comme une relation nat-eq ?

La relation nat-lt est définie en mentionnant explicitement la forme d’un terme nat, le nom du constructeur s, le successeur, y apparaît. Même sans la condition de la première règle de nat-lt, on y voit la signature d’un nat. Pour définir eq, on a besoin que de s’assurer qu’on a deux occurrences du même terme, à priori ou à posteriori, après, si c’est nécessaire et possible, que des variables aient été associées aux termes appropriés. L’égalité est neutre vis à vis de la nature du terme, le terme se trouve en fait comparé à lui‑même, comme l’expose bien le texte de l’unique règle de la relation eq. On peut intuitivement avoir la conviction que l’égalité de deux termes s’accompagne de l’égalité des ensembles des relations qu’ils vérifient, c’est tellement trivial que je ne sais même pas si l’idée de le démontrer pourrait avoir un sens (ou ça reviendrait à démontrer que le principe de l’unification est cohérent). Ce n’est pas le cas de la relation nat-lt, qui ne vérifie la relation que entre deux termes différents et c’est le cas de toutes les relations entre deux termes, elles incluent toutes la possibilités de deux termes différents, la relation d’égalité étant l’unique cas particulier (modulo toutes les définitions équivalentes qu’on peut en faire) et c’est une relation particulière, même si elle se défini facilement d’une manière qui n’a rien de particulier.

Si dans beaucoup d’autres contextes en informatique on ne peut pas comparer deux termes de types différents, ce n’est pas parce que ce serait logiquement incohérent, c’est surtout parce que ça n’aurait pas d’intérêt, deux termes de types différents, ne pourraient jamais être égaux, au moins pour une définition des types qui associe à chaque type, un ou des constructeurs propres qui ne sont pas partagés par les autres types (parler de types plus élaborés n’est pas le propos). L’égalité entre deux termes de types inconnus serait à priori moins inutile, elle comparerait le type en même temps et pourrait être soit vérifiée soi non‑vérifiée, au lieu de toujours être non‑vérifiée. Mais les contraintes de typage font que ce cas ne peut jamais se produire, l’idée de deux types inconnus liés en aucune manière étant exclue. Eh non, ce n’est même pas le cas des variables de type en SML, l’égalité ne pouvant être testée qu’entre deux termes du même eqtype. En bref, ce ne serait pas logiquement incohérent, mais c’est exclus pour la raison de contrainte de typage, et j’imagine que ça n’aurait pas assez souvent d’intérêt pratique dans ces contextes qu’une exception soit faite pour l’égalité.

On peut imaginer d’autres contextes, plus ou moins théoriques, mais ce serait inutilement risquer de se perdre et le cas d’un langage typé comme SML est assez représentatif, les mêmes remarques pouvant s’appliquer au Pascal et d’autres.

Pour revenir à la question, oui, on peut utiliser la règle eq avec des termes vérifiant nat et même tous les termes sans exception, c’est logiquement cohérent.

Note : il n’y a pas de type à proprement parler, en Prolog, même si on peut y formuler des conditions de cohérence que ailleurs on ferait reposer sur les types. Au passage, il faut rappeler que Prolog n’est pas destiné à être un langage de programmation, il est encore plus un langage de modélisation que ne l’est SML. Ce n’est pas impossible, mais ce ne sera jamais le propos ici où il ne sera vu que comme un langage de modélisation, d’interrogation et d’analyse.

Le message promis à propos de quelque compléments sur la récursion dans les règles. Il ne sera pas trop long.

Précédemment a été faite, l’expérience de requêtes ne se terminant jamais, car piégées dans une récursion infinie, quand elles sont faites pour des variables, mais se terminant, quand elles sont faites avec des termes tout entier constants. Il avait été dit qu’il ne faut pas s’y tromper, que la récursion infinie peut quand‑même se produire même avec des requêtes ne contenant que des constantes.

En voici un exemple simple :

peu-importe : peu-importe.
peu-importe ?

Intuitivement on peut comprendre que les variables nécessitent une recherche de solution qui a plus de chance d’aboutir à une récursion infinie, mais l’absence de variable ne garanti rien, comme le montre cet exemple. Ceci dit, on peut remarquer que la règle plus haut n’a pas de sens pour la logique de la pertinence, comme aucune variable ne lie l’antécédent et la conclusion. On peut pourtant avoir un cas de récursion infinie vérifiant ce critère :

(peu-importe X) : (peu-importe X).
(peu-importe X) ?

Le résultat est le même. Soit, mais même si la logique de la pertinence s’en dirait satisfaite, ça n’a toujours pas de pertinence.

Personnellement, je ne devine pas de cas où une requête sans variables se terminerait en récursion infinie alors que les règles ont toutes du sens et de la pertinence. J’imagine que d’une manière ou d’une autre, la requête devrait aboutir à une mise en correspondance pas à pas et que si les règles font que ça ne progresse pas, c’est qu’elles n’aboutissent jamais à rien avec quoique ce soit. Mais je ne saurais pas le monter, même pas informellement, ce n’est qu’une intuition.

Il avait été constaté qu’en permutant deux termes d’une des règles de la relation poly, la recherche de solutions était décevante, qu’elle énumérait mal, ne faisait varier qu’un terme et jamais l’autre. Il avait été dit qu’il est parfois utile de préférer placer le terme ayant un nombre de solutions fini, à droite de la conjonction et le terme récursif avec un nombre de solutions infini, à gauche de la conjonction, pour assurer une meilleure exploration des cas possibles (revoir le message concerné pour plus de détails).

Cette suggestion n’est pas toujours appropriée, elle doit être améliorée. D’abord un exemple la contredisant :

peu-importe : peu-importe & zzz-zzzz.
peu-importe ? -- Récursion infinie.

peu-importe : zzz-zzz & peu-importe.
peu-importe ? -- Échec sans récursion infinie.

Le point important n’est pas que « peu-importe » soit une définition récursive, le plus significatif est que zzz-zzz n’est pas définie, que ce terme ne peut que échouer (il pourrait aussi échouer en étant défini). Dans le premier cas, la recherche de solution fait varier le premier terme à l’infini, cherchant un contexte vérifiant le second terme, mais c’est impossible. Dans le deuxième cas, zzz-zzz est le premier terme, impossible à vérifier, la règle échoue avant d’entrer dans la récursion infinie.

Dans H : C1 & C2, s’il y a un risque que C2 ne puisse pas être vérifiée et que C1 fait entrer dans une récursion (directement ou indirectement), alors mieux vaut placer C2 devant C1. S’il n’y a pas de risque que C2 soit une condition infranchissable, que les solutions pour C2 sont en nombre fini et que C1 est récursive et surtout a un nombre de solution infini, alors mieux vaut placer C2 après C1.

Cette heuristique est plus fiable. Elle signifie qu’on ne peut pas à la fois à priori éviter la récursion sans fin et s’attendre à des résultats représentatifs et qu’on ne peut se permettre les résultats représentatifs que si on sait qu’il n’y a aura pas un obstacle infranchissable piégeant la recherche de solution dans une récursion sans fin.

Je ne crois pas qu’un cas équivalent existe pour l’ordre des règles, c’est à dire un cas où une règle récursive avant une règle non‑récursive offrirait un avantage, ne serait‑ce que parce la disjonction est trop différente de la conjonction. Pour l’ordre des règles, la recommandation ne change pas : les non‑récursives avant les récursives (au moins pour les règles ayant une terme de tête compatible).

Quelques fois a été mentionnée la question des termes récursifs. Ce n’est pas dans le principe de base standard de Prolog, alors je ne devrais pas dévier vers cette question, mais comme je l’avais introduit, je rapporte quelques pensées à ce sujet pour ne pas laisser de vaisselle sale sur la table. Certaines récursions infinies produisent finalement un terme récursif. S’il est prévu dans une interprétation non‑standard, de supporter les termes récursifs, alors pour que ça soit cohérent, il faudrait que ces termes puissent être une solution pour ces règles récursives. Quand les termes récursifs sont supportés, ils doivent de plus avoir une notation. Sans ça, les termes récursif ne sont finalement qu’une bizarrerie produite par certaines manières de calculer l’unification, sans correspondance ni dans la notation des termes ni dans les solutions aux règles, et il serait justifié de voir ces sérieuses lacunes comme des incohérences.

Je crois que ça clôturera ce qui concerne la récursivité, à moins que par surprise quelque chose ne montre le bout de ses oreilles quelque part.

Quand le principe de l’application des règles a été présenté, il a été précisé que les règles sont instanciées, c’est à dire qu’il en est fait des copies équivalentes mais avec des noms de variables n’existant pas encore dans le contexte, que ce ne sont pas des copies comme on ferait un copier/coller avec du texte. Mais il n’a avait pas été expliqué pourquoi.

C’est parce que si ça n’était pas ainsi, les incohérences arriveraient vite. Si la règle (eq A A) était copiée au sens littéral, alors cette conjonction échouerait : (eq abc abc) & (eq def def). abc est égale à abc et def est égal à def, c’est sémantiquement évident, mais ça ne serait pas le cas si la règle était copiée littéralement, parce que A serait liée d’abord à abc, puis ne pourrait pas être liée à def, comme def n’est pas le même terme. Ce n’est pas qu’en particulier avec cette règle que l’incohérence se présenterait, ce serait en général, mais cette règle en est l’exemple le plus immédiat.

Le même principe est appliqué dans le lambda calcul et bien d’autres langages formels.

Un cycle et une récursion, ce n’est pas la même chose.

X = (f X) ferait un terme cyclique (avec une autre notation quand‑même), mais l’infinie séquence de (s (s … z)) ne peut pas être formulée comme un terme cyclique. Le premier cas s’étend par le terme le plus interne, le second cas s’étend par le terme le plus externe. Aussi, le premier cas représente un terme infini, le second cas représente une infinité de termes. C’est aussi comme si le premier cas partait de l’infini pour chercher zéro et comme si le second cas partait de zéro pour chercher l’infini.

Je dis représentation même pour le second cas, parce que je crois qu’il serait autant utile d’avoir une notation pour le second cas que pour le premier. Sans représentation d’une chose, il est difficile de raisonner sur cette chose.

Le second cas ne représenterait pas la récursion en général, mais un terme récursif, c’est différent ; c’est à dire un terme qui n’a pas besoin de référence à autre chose que lui‑même pour se définir, comme il en va avec un terme cyclique. Ça n’empêche pas le terme mentionné d’être lui‑même constitué de tels termes. Par exemple le terme cyclique mal représenté plus haut par X = (f X), pourrait être composé d’un terme cyclique par une autre variable.

En parlant de terme cyclique, il ne faut pas confondre les termes cycliques avec les graphes cycliques en général. Un graphe peut avoir plusieurs points d’entrée, un terme est d’abord un arbre, il faut plus le comprendre comme des « arbres » cycliques que comme des graphes cycliques en général. Je ne sais pas s’il existe un mot pour le dire.

Ce ne sont que des idées aventureuses, il ne faut pas y faire trop attention.

Ce qui concerne la sémantique sera en deux messages avec une parenthèse entre les deux. Celui‑ci rassemble les remarques éparses sur les éléments constituant le sens pour en faire un sorte de synthèse. Une message suivant abordera des notions nouvelles, celles qui donnent un sens à ce qui est constitué de ces éléments. Entre ce message suivant et celui‑ci, viendra s’intercaler un autre en guise de parenthèse à propos de celui‑ci. Ce message est un condensé, ses paragraphes sont longs, je les espère malgré tout pas trop difficiles à lire, la finalité étant de rendre plus claires les choses en les re‑exposants toutes ensembles, pour donner une meilleure idée du tout et des liens entre ce qui le constitue. Ce tout n’est encore pour le moment que celui des éléments de base, mais chaque chose en sont temps. Ce message, bien que long, ne rappel pas absolument tous les détails déjà expliqués, il reformule certaines choses tirant profit du fait qu’elles sont reformulées toutes à la suite. Ça ne se substitue pas à ce qui a déjà été expliqué, ça le complète et le consolide.

Les éléments constituant du sens en Prolog, peuvent être compris en faisant référence à la notion de langage au sens courant du mot, pas au sens des langages formels, même si le principe de base de Prolog est un formalisme et que sa notation est un langage formel.

Les éléments :

• Constantes, variables et tuples.
• Les termes bien formés.
• La mise en correspondance de termes.
• La partition entre relation et constructeurs.
• Le signifiant et le signifié.
• Le contexte de la signification.
• L’instantiation et le contexte.

Toutes ces choses sont des éléments essentiels, pas seulement la mise en correspondance, c’est à dire l’unification (la notion souvent trop exclusivement mise en avant au point de négliger les autres).

Constantes, variables et tuples, sont des notions si élémentaires qu’elles sont difficiles à définir en termes d’autres choses et peut‑être même que le faire semblera une perte de temps de lecture. Il faut au moins leur donner cette place, comme tout le reste en dépend. Une constante pourrait se définir comme une chose qui n’est égale qu’à elle‑même, en précisant que si elle a plusieurs occurrences, toutes ses occurrences sont toujours égales entre elles et tout autant toujours différentes des autres constantes. Une variable pourrait se définir comme une chose à la place de laquelle on peut mettre une autre chose, et dire que la variable désigne cette chose qu’on met à sa place en intention, à moins qu’on ne substitue totalement cette chose à la variable. Contrairement aux constantes, des variables différentes peuvent être égales entre elles, même si elles ne sont pas les mêmes, parce que des variables différentes peuvent désigner la même chose. On peut aussi préciser que toutes les occurrences d’une même variable, désignent la même chose si la variable désigne quelque chose. Pour définir un tuple, disons que c’est plusieurs choses prises ensemble comme un tout qu’on forme à partir de ces choses. Comme les seules choses qu’on a défini jusque maintenant, sont des constantes et des variables, ces choses qu’on met ensemble, peuvent donc être des constantes et/ou des variables, mais comme par là on vient de définir ce que sont des tuples, on peut dire, des constantes et/ou des variables et/ou des tuples, et les tuples sont alors des compositions pouvant être récursives. Oops, il aurait fallut définir les notions d’égalité et d’occurrence, aussi … tant‑pis, on continue.

Les termes bien formés le sont d’après une syntaxe. En terme linguistique, ça ne correspond pas encore à la grammaire, mais à des mots qui seraient composés, comme il en existe des exemples avec les langues dont les mots sont constitués à partir de racines et de schèmes, excepté que là, la notion de composition est uniformément généralisée. Les termes initiaux sont des constantes et des variables. Un terme commence toujours par une constante ou est constitué uniquement d’une constante seule sans rien avec. Si la constante n’est pas seule, elle est, avec des parenthèses — qui sont la notation d’un un tuple — suivie d’autres termes qui peuvent être d’autres constantes ou des variables ou d’autres termes plus internes constitués de la même manière. Examples de termes avec la convention que ce qui commence par une majuscule est une variable : abc, (abc Def), (abc def), (abc Def), (abc (def Def)), etc. À noter que Def, seule, n’est pas un terme valide, car ne commençant pas par une constante, mais (abc Def) est un terme valide, parce que Def est un terme interne, pas le terme entier  le terme entier commence bien par une constante. La notation classique écrit juste la première constante d’un terme avant la parenthèse ouvrante, c’est à dire abc(Def) au lieu de (abc Def) comme noté ici.

La mise en correspondance de termes, se fait selon les règles de l’unification. En linguistique, elle correspondrait à des mots semblant avoir un schéma similaire, à partir de quoi on déduirait quelque chose de leur sens par établissement de correspondance. Cette notion de mise en correspondance semble liée à celle des termes bien formés et c’est en effet le cas. La mise en œuvre de l’unification nécessite plus de calculs que la description intuitive qui en est faite ici, mais l’idée est que la forme des termes est comme schématique, parce qu’à des parties variables peuvent correspondre d’autres termes, mais qu’une fois qu’une variable a été fixée, elle ne peut plus changer. Par exemple, les deux termes (abc D E) et (abc (def def) (def D)) sont différents, mais on peut voir une similitude de forme entre les deux, une constante abc suivie de deux termes, il peuvent correspondre, modulo ce que désigneraient les variables D et E. La mise en correspondance de ces deux termes, signifie en effet que D est (def def) et que E est (def D). Si A, B et C sont trois termes, que B est mis en correspondance avec A, C peut être mise en correspondance avec B aussi. Mais la mise en correspondance peut échouer, aussi bien entre B et A que entre C et B. Elle pourrait aussi pouvoir se faire entre B et C mais pas entre B et A.

La partition entre relations et constructeurs est une conséquence des deux précédentes notions, et surtout de la première. C’est une conséquence, mais pas une conséquence subie, elle est nécessaire. Comme le point de départ de la construction d’un terme est toujours une constante ou que tout le terme est une constante seule, une variable seule ne peut jamais être à elle seule un terme complet. Donc, la mise en correspondance décrite plus haut, ne pourra jamais mettre en correspondance cette constante initiale avec une variable. Pour comprendre pourquoi c’est impossible, il peut être plus simple de voir ce qui serait nécessaire pour que ce soit possible. Pour que le abc de (abc D E F) puisse être mise en correspondance avec une variable, il faudrait qu’on puisse avoir (X D E F), mais ce n’est pas permis par la syntaxe comme le terme ne commence pas par une constante. Pour que la constante seule abc, puisse être mise en correspondance avec une variable X, il faudrait que la variable X seule puisse être un terme tout entier, mais ça n’est pas permis par le syntaxe, pour la même raison. Cependant, une variable peut capter une constante autre que cette constante initiale, comme une constante apparaissant dans un terme plus interne. Un example avec la mise en correspondance de ces deux termes : (abc X) et (abc def). Si la variable X apparaît ailleurs, elle peut même signifier que cette constante def se trouve par là ailleurs aussi, mais seulement dans un terme interne, comme c’est le seul endroit où une variable peut apparaître. Par contre, une variable ne pourra jamais capter la constante de départ abc. On peut en comprendre que les constantes de départ d’un terme complet, dont l’exemple est toujours abc pour faciliter la lecture, restent toujours des constantes de départ d’un terme complet, ne sont jamais virtuellement injectées dans des termes internes par des variables, parce que les variables ne peuvent jamais les capter par mise en correspondance. Il y a mécaniquement une partition entre ces constantes initiales des termes entiers et les constantes initiales des termes internes. Les premières sont des relations, les secondes sont des constructeurs. Par extension, ce qui a été appelé plus haut, un terme complet, est aussi appelé une relation (comme on appel « bureau », le meuble mais aussi la pièce dans laquelle se trouve ce meuble). Les relations sont parfois appelées des prédicats, mais ce mot est plutôt à laisser à d’autres domaines. Ce qui a été appelé précédemment un terme interne, est appelé un terme tout‑court. Les constructeurs sont appelés ainsi parce qu’ils permettent de construire des termes (internes) par composition, récursivement. Les constructeurs sont parfois appelés des fonctions, mais ce mot devrait lui aussi être laissé à d’autres domaines. Cette partition est une conséquence de l’unification et de la syntaxe, mais plus encore de la syntaxe, comme la syntaxe précède l’unification. Cette distinction qui de fait sépare deux niveaux de langage dans les termes, est une conséquence syntaxique.

Note en marge de ce long paragraphe : même quand une constante de relation et une constante de constructeur ont le même nom, elles restent sémantiquement distinctes, mécaniquement, elles n’appartiennent pas au même niveau de langage. C’était le but de ce long paragraphe, que d’expliquer pourquoi et de le souligner.

Le signifiant et le signifié sont deux concepts assez connus dans la culture populaire linguistique et philosophique, ce qui montre leur importance. Dans le présent formalisme, cette notion passe par une construction réalisée par deux opérateurs syntaxiques, que sont la conjonction et la disjonction et un autre opérateur syntaxique pour distinguer un terme comme signifiant. Chaque terme peut signifier un signifié, s’il peut être mis en correspondance avec un terme signifiant. Schématiquement et pour aider à comprendre, en utilisant des lettres majuscules pour représenter des termes quelconques d’une manière abstraites, voici un exemple. Soit « H : C1 & C2 & C3 … ». Le tout s’appel une règle. Le « H » est conventionnellement appelé la tête de la règle et le « C1 & C2 & C3 … » est conventionnellement appelé le corps de le règle. Le « H » est le terme signifiant, distingué par l’opérateur syntaxique noté ici « : » , mais noté « : - » dans la notation classique. Le « C1 & C2 & C3  » est le signifié, c’est une conjonction où les Cn sont eux‑même des termes. La conjonction notée ici « & » est plus classiquement notée par une virgule. La disjonction est soit implicite soit explicite. Ici, elle est toujours implicite, elle correspond à plusieurs règles dont les signifiants sont similaires. Elle peut être explicite avec une notation de la forme H : (C1 & C2 …) ; (C3 & C4 …) où le « ; » est un opérateur syntaxique signifiant la disjonction et à comprendre au sens de « ou au choix ». Certaines notations semblables dans le principe, utilisent une bar verticale, « | » au lieu de « ; ». Les termes C1 et C2 …, peuvent chacun signifier une règle à leur tour s’ils peuvent être mis en correspondance avec le signifiant de la règle en question. Par exemple si on a H1 : C1 & C2 et qu’on a aussi H2 : C3 & C4, si C3 par exemple, est en correspondance avec H1, alors a C3 peut être substitué C1 & C2. Le corps d’une règle peut être vide ou ne contenir qu’un seul terme, pas nécessairement plusieurs. Il est nécessaire que le corps de certaines définitions puissent être vide, sinon l’idée qu’un terme est défini par une suite de termes chacun à leur tour définis par une suite de termes, etc … ne s’arrêterait jamais. L’existence de définition dont le corps est vide, permet au concept de ne pas finir en récursion infinie.

Note en marge du précédent paragraphe : quand plusieurs règles peuvent être signifiées par un même signifiant, qu’il y a donc plusieurs alternatives pour le signifié d’un signifiant, l’ensemble est souvent appelé une clause, et chaque alternative, une règle. Mais il semble que parfois, les mots règle et clause sont utilisés comme s’ils étaient synonymes. Quand ces deux mots ne sont pas pris comme des synonymes, si on a par exemple « H : C1 et H : C2 », il y a deux règles et une clause, ce qui parfois serait noté d’une manière semblable à « H : C1 ; C2 ».

Le contexte de la signification est le contexte sous lequel un signifié est valide. Ce que signifie un signifiant, dépend du contexte. C’est pour cette raison que les définitions dans les dictionnaires, se déclinent en plusieurs options contextualisées. De même avec ce formalisme, mais en posant explicitement que si la contextualisation n’est pas possible, alors rien n’est signifié. Dire qu’une signification n’est pas valide, on peut le comprendre comme dire qu’elle ne signifie rien. Un terme est dans un contexte et peut signifier quelque chose s’il correspond à un signifiant. Ce terme place le signifiant en contexte et le signifiant place à son tour le signifié en contexte. Si la contextualisation échoue, le terme ne signifie rien, et par là, toute la définition (conjonction) dans laquelle il se trouve lui‑même (le concept et récursif). Par exemple, si on a H1 : C1 & C2 et H2 : C3 & C4, implicitement C3 est dans un contexte, si d’après son contexte, C3 est correspondant à H1, de même, « C1 & C3 » est mis dans le contexte transmis par H1 qui est lui même en contexte d’après C1. Si C3 dans son contexte, ne correspond pas à H1, C3 ne peut pas signifier C1 & C2, et s’il n’existe pas d’autre règle alternative, C3 ne signifie rien du tout, et si c’est le cas C3 & C4 ne signifie rien non‑plus. C’est ainsi, récursivement. C3 tient lui‑même son contexte de H2 de la même manière. Le contexte tout initial, le tout point de départ, est celui d’une requête qui est‑elle même un terme ou une conjonction de termes, mais comme son contexte, à cette requête, est posé à priori, il n’y a donc pas de récursion sans fin dans cette notion, il y a heureusement un point de départ. Le contexte tout initial, celui d’une requête, est souvent un contexte vide, mais pas nécessairement, il peut être un contexte laissée par une requête précédente ou même un contexte défini arbitrairement.

Une analogie. Si ce que signifie la bonne mesure des choses en diplomatie par exemple, peut être variable selon les contextes et les climats (un mot qui a lui même un sens dépendant fortement du contexte), ça ne change rien à ce que signifie la bonne mesure des choses en physique ou en chimie par exemple. La bonne mesure des choses en diplomatie, ne signifie pas la même chose quand on est dans des relations commerciales paisibles ou en situation sociale tendue faite de griefs réciproques, mais ça n’a aucune influence sur ce que signifie la bonne mesure des choses en chimie, qui elle, variera selon qu’on est dans l’industrie du vinaigre ou des composés azotés. Si la bonne mesure des choses dépend de ces deux contextes, ça ne signifie pas que ces signification n’ont rien en commun, on ne parle pas de mesure dans les deux cas (ou de climat par exemple encore), par hasard, mais reste que la signification dépend du contexte et sinon n’en a pas concrètement.  Le sens peut même dépendre d’un contexte dans le contexte. Le sens de certaines choses abstraites est applicable dans une large gamme de contextes, comme par exemple la notion d’équivalence entre deux choses, tandis que d’autres n’ont de sens que dans un petit nombre de contextes, comme la notion salinité par exemple. Il faut bien distinguer la signification en contexte de l’homonymie. Il ne s’agit pas là d’homonymie. Comme une comparaison a été faite avec un dictionnaire, il sera peut‑être utile de se remettre les choses dans leur contexte, justement, en revenant au fait que c’est une analogie pertinente, juste que dans ce formalisme on ne parle pas de mots, mais de termes dont la forme est beaucoup plus composée et décomposable que des mots et dont les sens renvoient moins facilement à des notions innées. Ces termes qui sont moins innés que des mots, sont composés de parties variables, ce sont elles qui portent le contexte ou sur elles que portent le contexte (c’est pareil). La bonne mesure des choses, c’est une notion abstraite, si cette définition doit être posée, ça ne peut être qu’avec des parties variables.

L’instantiation et le contexte sont deux concepts donnant sens aux variables, qui elles, donnent son sens à la notion de mise en correspondance de deux termes. Quand une définition, c’est à dire le corps d’une règle, est mise en contexte, ça ne concrétise le sens que dans ce contexte, la définition d’origine n’est pas changée. Ça semble trivial pour le sens commun, mais ça l’est moins avec un langage formel qu’on peut avoir tendance à aborder comme des bouts de texte qu’on manipule ; c’est assez ça, c’est vrai, et c’est justement pour cette raison qu’il faut préciser que quand on insère le contenu d’une définition dans un contexte, ses parties variables désignent des choses dans ce contexte, mais ces parties variables, restent variables dans la source de la définition. Si on a une règle triviale disant que X = X, et que quelque part on en conclut que b = b, la règle X = X, reste et on pourra toujours conclure que c = c, parce que X ne sera pas devenu b partout. En plus pour les règles, d’avoir des variables propres à chacune de leurs instantiations, ces variables ont leur sens concret défini par le contexte ou complète ce contexte, selon le cas et c’est en fait la même chose. Selon le cas, parce que la mise en correspondance de deux termes, qui est à l’origine de l’association entre une variable et ce qu’elle désigne, se fait aussi bien dans un sens que dans l’autre. si (abc Def) mis en correspondance avec (abc def) signifie que la variable Def désigne la constante def, la réciproque est vraie aussi, si (abc def) est posée comme en correspondance avec (abc Def). Si on a H1 : C1 et H2 : C2, que C2 a une variable X qui dans le contexte de C2, désigne, disons zzz, que cette variable X est mise en correspondance avec une variable Y dans H1, que cette variable Y apparaît dans C1, alors la variable Y de C1 désignera zzz. Réciproquement, si la variable X dans C2 ne désigne rien, qu’elle n’a pas de valeur, qu’elle est mise en correspondance avec un Y dans H1, que C1 correspond une règle faisant que Y désigne zzz, alors le X de C2 désignera zzz. On peut avoir les deux en même temps, X et Y étant en accord et désignant la même chose. Si X et Y ne désignent pas la même chose et ne peuvent pas désigner la même chose, les contextes sont incompatibles ou elles forment des contextes incompatibles, ce qui est la même chose. Si seulement l’une de X ou de Y désigne quelque chose, l’autre pourra désigner la même chose et ce sera justifié par la liaison entre les deux, un fait qui sera une des associations du contexte.

La petite parenthèse avant la suite qui tarde parce que des choses me tracassent à son sujet.

Le précédent message a définit les choses en se reposant sur le sens dans le langage naturel, parce qu’il est le représentant le plus accessible du sens inné. Certaines des choses décrites ne collent pourtant pas directement au langage naturel. C’est ce que cette parenthèse essaie d’aborder pas trop longuement, parce que même si c’est sémantiquement important d’en parler, ça n’est pas le sujet. Ça n’est pas sans rapport non‑plus, comme le sens, formel ou pas, finira toujours par être compris en termes de sens inné ou ne le sera pas. On peut appeler ce sens inné, l’intuition et remarquer que le langage naturel ne le représente que partiellement, mais comment faire mieux ?

L’idée de variable peut assez correspondre à celle de pronoms et déterminants. L’idée d’instantiation correspond au sens commun que dans deux phrases différentes, à moins qu’elles ne soient liées, les pronoms et déterminants ne désignent pas la même chose. L’idée de constructeur renvoi à la structure des mots, même si les langues naturelles sont très inconstantes à ce sujet et restreignent beaucoup les libertés.

L’idée de relation est plus trompeuse. Un raisonnement courant est la généralisation et l’abstraction sur la base d’attributs communs. Ça ne correspondrait bien qu’à la relation à un seul argument, c’est à dire à un type. Un autre raisonnement courant est l’association, qui ne correspond pas à la relation et correspondrait plutôt à l’implication. Associer B à A correspondrait à A ==> B qui correspondrait à « B : A. », c’est à dire que associer B à A correspondrait plutôt à dire qu’on définit (ou parfois, réduit) B comme au moins entre autres, A, ce qui n’est pas une relation. Je suis incertain de à quoi la relation en général pourrait correspondre dans le sens commun. Peut‑être à un type de complément, complément au sens grammatical ? Ça restera en suspend.

Ce qui a été décrit comme une définition se lit parfois mieux comme une condition et la notion de condition n’est pas une notion du langage naturel où elle n’est éventuellement qu’un objet comme un autre. La différence de lecture dépend de la forme des termes apparaissant dans ce qui a été appelé la tête de la règle. Quand la tête de la règle dit déjà quelque chose de la forme d’un terme, le corps de la règle se lit mieux comme une condition. Mais on peut toujours écrire la règle en ayant que des variables comme termes dans la tête de la règle et en exprimant la forme des termes associés à ces variables, dans le corps de la règle. C’est une question de style, c’est logiquement équivalent. On peut aussi toujours voir une définition comme posant une condition sur le contexte d’interprétation et considérer que alors une définition est quand‑même toujours implicitement une condition quelque part.

La séparation en deux niveaux de langage ne doit pas être vue comme une limitation mais comme garantissant que les relations sont des relations et que les constructeurs sont des constructeurs. Traiter les constantes des relations comme les constantes des constructeurs, pourrait être comparable à perdre le sens de mots en les confondant : on ne gagne alors rien en liberté à les traiter ainsi, mais on perd en capacité à exprimer le sens des choses. Ça se dit brièvement, mais c’est à souligner, c’est important.

Important à souligner aussi, est la caractéristique que les définitions ne peuvent pas être invoquées dans un contexte où elles n’ont pas de sens. Cette caractéristique est une perle. De même pour la conjonction émanante ; la conjonction n’a pas besoin d’être définie, elle émane.

Concernant le sens de ces choses en termes informatiques, il faut faire attention à ne pas confondre relation et fonction : une fonction peut être décrite par une relation, mais une relation ne peut pas être décrite par une fonction (ou pas en général et puis dans le fond ça n’aurait même pas vraiment de sens … relire la phrase pour comprendre pourquoi). Comme avec le langage naturel, la relation à un argument correspond bien à un type. Ces types peuvent être vus comme pouvant être génériques.

Une dernière, une colle. Aucune idée de ce à quoi peut correspondre une relation sans argument. Quel sens peut bien avoir une relation sans argument ? Permettre d’invalider tout un ensemble de règles par le fait d’une règle représentant une sorte de condition d’intégrité de l’ensemble ? Cette question aussi restera en suspend. Aux constructeurs sans argument, correspondent au moins les concepts totalement abstraits pour le sens commun et les constantes élémentaires (mais qu’on peut toujours introduire) en informatique.

Dans ce message qui sera le dernier avant longtemps, il n’y aura que des questions, aucune réponse.

Pour résumer ce qui va suivre, vont être introduits les idées de univers de Herbrand, base de Herbrand, interprétation, modèle et modèle minimal. Chacun de ces concepts repose sur celui le précédant.

On part d’un ensemble de règles, avec leurs relations et leurs constructeurs, quelques soient leurs arités. On pose l’ensemble des constructeurs. Si cet ensemble est vide, un constructeur arbitraire est posé pour que l’ensemble initial ne soit pas vide, même si ce constructeur n’apparaît pas dans l’ensemble des règles. L’introduction arbitraire de cette constante est partout posée, mais jamais expliquée, alors suit une tentative d’explication.

Il s’agit plus tard d’instancier des relations à partir de termes de l’univers de Herbrand dont la définition est poursuivie un peu après. Cet univers de Herbrand ne contient que de termes tout entier constants, sans aucune variable. On peut imaginer un ensemble de règles sans constructeurs, seulement avec des variables. Dans ce cas, l’introduction d’une constante arbitraire peut se comprendre, comme il faudra bien donner des arguments à ces relations et que ces arguments doivent provenir de l’univers de Herbrand, qui ne contient pas de variables.

La raison des termes entièrement constitués seulement de constantes serait d’après au moins un document, d’éliminer les quantificateurs pour ramener des démonstrations sur des prédicats à des démonstrations sur un ensemble infini de propositions. On est donc pas au bout de l’infini, en voilà encore un autre. Ceci dit, les quantificateurs sont déjà éliminés autrement en Prolog, la notion de contexte leur étant substitué. En Prolog, au lieu d’être liée à un quantificateur, une variable est liée un contexte. Dans A : B, une variable apparaissant dans A peut être vue comme universellement quantifié et une variable apparaissant dans B, comme existentiellement quantifiée (sauf erreur). Soit, mais ce n’est pas nécessairement étrange pour autant. Si pour les prédicats une variable est toujours sous un quantificateur, éliminer les quantificateurs équivaut à éliminer les variables, ce qui est autant applicable aux termes en Prolog. Il semble cohérent de comprendre l’intention ainsi, comme l’univers de Herbrand ne contient que des termes constitués de constantes. Je me demande si le fait d’éliminer les variables n’aurait pas comme effet de rendre plus accessible à l’analyse, les relations entre les règles. Mais ce n’est qu’une intuition, et puis, cet ensemble est infini, ce qui poserait un problème en amenant une solution.

Le passage d’un ensemble fini de prédicats à un ensemble possiblement infini de propositions, permettrait un démonstration à l’aide d’un certain théorème, le théorème de Herbrand.

Voici donc jusqu’ici pour la constante éventuellement introduite arbitrairement (conventionnellement souvent nommée « a »), l’élimination des quantificateurs ou peut‑être plutôt des variables et le passage d’un ensemble de prédicats à des propositions en nombre infini. On reprend avec la définition de l’univers de Herbrand.

Donc, l’univers de Herbrand est constitué initialement de toutes les constantes de constructeurs apparaissant dans un ensemble de règles posées et si l’ensemble de règles ne fait apparaître aucun constructeur, une constante est arbitrairement posée. C’est le niveau zéro de l’univers de Herbrand. Le niveau suivant prend les constantes du niveau précédent et leurs applique les arguments de ce niveau précédent, pour former de nouvelles valeurs constantes, selon les arités des constructeurs, puis à ce qui vient d’être obtenu, est ajouté ce qui l’avait été niveau précédent. C’est le niveau n°1 de l’univers de Herbrand. Les niveaux suivants se construisent de la même manière, chaque fois à partir du niveau précédent, ceci jusqu’à l’infini. On imagine alors que c’est une construction en intention et pas en extension, même si dans quelques cas cet univers est fini.

Cette définition qui est donnée presque à l’identique partout, est étrange. Comment l’arité d’un constructeur est‑elle déterminée ? On peut imaginer que l’arité est inférée du texte des règles, en notant qu’un constructeur peut avoir plusieurs arités. Étrange que ce ne soit jamais précisé, mais ce serait raisonnable, je ne crois pas que les constructeurs soient déclarés comme on déclarerait des fonctions dans un langage typé par exemple (même si un système d’édition de règles peut le prévoir pour éviter les erreurs d’écriture, ça ne ferait pas partie du formalisme pour autant). La définition varie cependant parfois, l’arité d’un constructeur étant supposément toutes les arités possibles, de zéro à l’infini. On est plus à ça près, l’univers de Herbrand étant de toutes manières typiquement infini (et cet infini ne serait pas pire, ce serait le même, le cardinal des entiers naturels … mais ça n’aide pas non‑plus de le remarquer). On peut s’interroger sur l’intérêt de considérer qu’un constructeur existe toujours avec toutes les arités possibles. Une source dit d’ailleurs explicitement, que dans le premier niveau de l’univers de Herbrand, les constantes du niveau zéro sont toutes appliquées à elles‑mêmes. Donc une constante comme … z, par exemple, qui est d’arité zéro, serait appliquée à elle‑même. Difficile d’y voir du sens. Mais peut‑être qu’on peut se débarrasser de cette épine en notant avec de l’avance, que ces termes de l’univers de Herbrand sont destinés à être appliqués à des relations et que plus loin, on s’intéressera surtout aux cas où les relations sont vérifiées, ce qui exclut implicitement ces arguments qui n’ont pas de sens. Peut‑être serait‑il possible d’exclure certaines de ces termes constants par anticipations sachant qu’ils n’auront jamais d’utilité ? Mieux vaut je crois en rester à l’idée de l’arité inférée d’après le texte des règles. Ce n’est pas tout, il n’y a pas que l’arité, il y a ce qui est appliqué à quoi. Quel est le sens d’appliquer n’importe quelle constante à n’importe quelle constante ? Quel est le sens d’appliquer z à z, sans même s’arrêter à son arité ? Ceci dit, vrai que les variables peuvent faire qu’on ne peut pas inférer directement du texte, quelles constantes peuvent être appliquées à quelles constantes. Mais il n’est pas exclus que même sans tout inférer, il reste possible d’inférer que certains cas ne peuvent pas se produire ; c’est sous réserve qu’une méthode (fiable) soit définie à cette fin. Mais cela changerait‑il quelque‑chose ? Réduire un ensemble infini pour avoir un sous‑ensemble tout aussi infini ?

Il semble, mais c’est assez incertain, qu’il peut suffire de poser l’univers de Herbrand jusqu’à un certains niveau, pas nécessairement jusqu’à l’infini ? Un document m’a donné cette impression, mais un seul.

L’univers pas clair et infini de Herbrand est posé.

Une base de Herbrand est constituée de toutes les clauses instanciées par tous les termes de l’univers de Herbrand, un univers qui est typiquement infini. Là aussi, l’ensemble ne peut alors pas être posé en extension, seulement en intention, reste à savoir comment. Même remarque que précédemment concernant la question de ce qui est appliqué à quoi, mais les variables font qu’on ne peut pas facilement l’inférer à partir du texte des règles, alors acceptons l’idée que tous les termes de l’univers de Herbrand peuvent être un argument de n’importe quelle clause de la base de Herbrand, quoique là aussi, peut‑être que certaines choses peuvent quand‑même être inférée sous la même réserve.

Dans le contexte de Prolog, il semble que les clauses doivent être comprises comme les relations, c’est à dire les termes qui sont des relations, ceux des têtes des règles et ceux des corps des règles. C’est assez explicitement confirmé par au moins un document.

L’univers étant posé autant que possible, la base à partir de l’univers, autant que possible aussi, on peut essayer de poser l’interprétation à partir de le base.

Une définition de l’interprétation est que à chaque instances de relations de le base, est associé le jugement Vrai ou Faux. Une variante courante et qui vient naturellement aussi, est de « poser » un sous‑ensemble de la base dont toutes les instances de relations sont jugée Vraies, les autres étant implicitement jugées Fausses. En « posant », parce que la base étant infinie, et un sous ensemble d’un ensemble infini étant plus facilement infini que fini, cet ensemble et qui est l’interprétation, ne pourra lui aussi que être posé en intention. Là aussi, reste à savoir comment.

Il y a quand‑même encore une bizarrerie. Au moins un document pose une interprétation de constructeurs en guise d’exemple, ce que je n’ai vu dans aucun autre document. Quel sens cela a‑t‑il ?

À partir de l’interprétation, est vérifié un modèle. Vérifié, parce que un modèle est en fait une interprétation ayant cette propriété : toutes les instance de tête de règle apparaissant comme vraies dans l’interprétation sont vraiment vraies, si leurs termes, qui sont des instances de termes, apparaissent comme vrais dans cette interprétation, et si touts les instances de tête de règles sont ainsi vraiment vraies, alors cette interprétation est un modèle de l’ensemble de règles posées au départ. Un modèle parmi d’autres possibles, un modèle n’étant pas nécessairement unique.

La notion de modèle minimal, suit, mais ne semble pas incontournable ou au moins potentiellement implicite. Plusieurs interprétations peuvent être définies. Un ensemble infini aussi ou pas ? En oubliant cette question, dans le cas où plusieurs interprétations sont définies, qu’on ne s’intéresse qu’à celles qui sont des modèles vérifiés, il existe entre tout ces modèles, une intersection, et cette intersection, est le modèle minimal, parfois appelé, la sémantique déclarative du programme, le programme devant être compris au sens de l’ensemble de règles posées. Dans le cas où une seule interprétation est définie, elle est le modèle minimal ?

Pourquoi poser plusieurs interprétations ? Je crois qu’il est illusoire de répondre à cette question, vu les questions que soulèvent déjà les définitions plus haut et dont cette notion dépend.

Non seulement ces définitions ont quelques aspects surprenantes, restent finalement vagues et suggèrent de traiter avec des ensembles infinis de propositions, mais en plus, elles sous‑entendent la mise en œuvre de formes de déclarations qui ne sont pas précisées. Je ne vois en effet pas comment définir les ensemble précédent si ce n’est en intention, mais avec quel langage, quel formalisme ? Le formalisme lui‑même ? Ces ensembles seraient eux‑mêmes définis par des relations et des termes ? Ce n’est pas tout, ces définitions suggèrent des calculs assez spécifiques, au moins pour la vérification d’un ensemble infini de propositions. Certaines interprétations des récursions infinies, quelques fois évoquées, seraient‑elles des pistes ? Faut‑il un système de déduction had‑oc ? Mais alors les termes sans variables seraient représentés par des termes avec des variables ? Et une méthode spécifique aussi pour le calcul du modèle minimal.

Ce n’est pas du tout clair et n’a pourtant encore même pas été posée une question me semblant importante : vérifier qu’une chose est parfois vraie, toujours vraies, parfois fausse ou toujours fausse. Peut‑être que justement ces concepts difficiles à aborder le permettent‑ils ? Impossible à dire à moins de les comprendre assez clairement.

La suite, je ne sais pas quand (tout ce temps a été pris sur d’autres choses qui ont pris un énorme retard, et ça ne peut pas durer).

Pour bien laisser sur sa faim, voici trois documents sur la question, qui me semblent représentatifs de la manière d’exposer ces concepts, mais dont l’imprécision me semble tout autant représentative, juste pas les pires :

• Semantic Aspects of Prolog Programs (ocw.ui.ac.id) [PDF].
• Méthode de Herbrand (liris.cnrs.fr) [PDF], il n’est pas en Anglais, ça fait bizarre.
• Herbrand Method (cse.unsw.edu.au) [PDF].

Une note en marge pour la fin, avant vraiment pas tout de suite, c’est sûr. Le calcul des prédicats dont Prolog est une variante, est sound et complete. Ça peut sembler une bonne nouvelle, mais peut‑être pas : ça peut signifier qu’il manque d’expressivité. Mais peut‑être qu’il ne faut pas s’en préoccuper avant d’en avoir une raison concrète. Et puis peut‑être que l’idée de superposer des langages pourrait y remédier, mais je n’en sais rien et inutile de penser à la solution à un problème sans savoir si, ni comment, il va se présenter, s’il se présente.

Pour ne pas terminer sur un message trop déprimant. C’est pas encore Noël, mais comme le paquet sera long à ouvrir, il ne sera peut‑être pas ouvert avant Noël.

Une inférence, c’est l’application d’un modèle réduit (hihi).

On est dans un monde ou B : A, mais on vient d’un monde où A ⊢ B (formulé en termes contemporains).

Dans « l’abstraction » (λx • … x …), x est une abstraction.

Brouillon : n.m. plur. brouillons. Feuille de papier sur laquelle sont écrites une ou des formules dans lesquelles ont été griffonnés des quantificateurs. Voir aussi : cul‑de‑sac.

Fill‑in the blanks: Un ensemble [ ] de termes récursifs [ ]s est une [ ]e et cet ensemble a un terme [ ] [ ].

En présence de variables, la définition d’un ensemble de termes tous uniques, est à priori problématique. On ne peut pas définir de tels ensembles de n’importe quoi. Ça suggère qu’il est à priori difficile de définir des ensembles non‑typés (par analogie, en tenant une relation comme un type, le principe de base de Prolog n’étant pas typé).

Des relations pouvant n’être vérifiées que pour des termes sans variables, c’est possible et même courant. C’est à ne pas confondre avec une recherche de solutions vérifiant une relation, il s’agit bien de termes vérifiant une relation, pas d’une recherche de ces termes. Reste que vérifier une relation ne suffit pas, comme il reste possible que des relations puissent être vérifiées pour des termes contenant des variables.

En faisant comme si la précédente question était résolue, il en reste une autre. S’il n’est pas possible de définir des ensembles sans typer (toujours l’analogie) leur éléments, alors il n’est pas possible de définir une idée des ensembles en général ?

Le précédent message inspire une catégorisation des règles.

Il faut distinguer les règles qui se vérifient en ne laissant pas de variables libres, de celles qui se vérifient en laissant possiblement des variables libres.

Les règles de la seconde catégorie, sont potentiellement problématiques, mais à priori, je ne crois pas qu’elles le soient toujours.

Plus haut, par variables non‑libres, il faut comprendre liées à autre chose que Any, et récursivement, finalement liées à un terme qui peut se développer comme un terme fait seulement de constantes.