Les logiques : notes en vrac

Il s’avère que telles que définies jusqu’ici, la non‑égalité et la « négation » de l’égalité par l’échec, ne sont pas équivalentes. L’une des deux doit‑elle être rendue équivalente à l’autre ? Faut‑il abandonner la première ? Il n’est au moins pas envisageable d’abandonner la seconde. Faut‑il ne pas y voir un problème et clarifier la relation et les différences entre les deux ?

Ce qui suit est en se restreignant, pour le moment au moins, à une non‑égalité avec seulement une constante, pas avec un terme plus complexe.

En définissant la non‑égalité par un concept d’exclusions interprétés par l’unification, se poserait plusieurs problèmes pendant qu’un avantage se présenterait.

La règle spéciale de la non‑égalité, lierait une variable non‑liée à une exclusion ou vérifierait qu’une variable liée ne contredit pas une exclusion ou validerait le remplacement d’une liaison à une exclusion par la liaison à une constante non‑exclue. Elle aurait l’apparence d’une règle ordinaire, alors qu’elle n’en est pas tout à faite une (voir plus loin), même si elle serait une forme de résolution, juste nouvelle. Elle nécessiterait peut‑être d’introduire une notion d’ensemble, mais ce problème n’est pas certain comme n’importe quel terme interprétable comme listant les liaisons exclues, suffirait, surtout qu’il n’y a pas de nécessité d’ensemble potentiellement infini. Elle aurait l’avantage de permettre de formuler une chose impossible actuellement : « n’importe quelle constante exceptés celles‑ci », ce qui avec des airs de rien, est encore une manière de se passer de certains ensembles infinis.

Le dernier point nécessite de revoir ce qu’est une solution et explique pourquoi plus haut il est dit que ce n’est pas une règle ordinaire. Disons que la non‑égalité soit une règle (neq A B) et qu’on pose une simple requête comme (neq A b), A étant libre. Cette requête ne pourrait pas avoir une solution semblable à celles jusque maintenant, elle ne pourrait ni être un terme ni être Any, elle serait un exclusion, « peu importe, excepté b ». Savoir si c’est acceptable ou pas, est discuté plus loin.

Qu’en serait‑il d’une formulation de la même chose, avec la « négation » par l’échec ? La requête pourrait ressembler à « non (eq A b). » Comme vu précédemment, une négation par l’échec n’est pas une résolution, est censée être vérifiée dans un contexte qu’elle ne modifie pas après que les résolutions positives ont abouti. Si A est liée à une constante la conclusion, qui est soit Oui soit Non, est facilement interprétable et ne déçoit pas. Si A est liée à Any, la vérification de « (eq A b) » échoue, parce que Any peut être b est donc A ne peut pas être dit non‑b, mais A étant Any, A pourrait aussi bien ne pas être b. Il avait été envisagé que la négation par l’échec ne serait définie que pour des termes sans variables libres ; cet exemple semble plaider en faveur de cette option. Mais comment interpréter la négation par l’échec dans les cas où elle n’est pas définie ? Ici, « non (eq A b) » signifie seulement qu’on ne peut pas dire que étant donné A libre, qu’on a « (eq A b) », justifiant de conclure « non (eq A b) », elle ne signifie pas que A étant libre, quelque soit A, qu’on a jamais (eq A b). C’est compréhensible, mais c’est décevant et c’est surtout facile à mal lire.

Plus haut se posait la question de savoir s’il est acceptable ou pas, qu’une requête renvoi comme solution, quelque chose comme « n’importe quelle valeur, excepté celles‑ci ». On pourrait se dire que c’est une équation à résoudre, pas une véritable solution. Mais ce n’est pas comme si le résultat était décrit par n’importe quelle propriété, il s’agit d’une non‑égalité, l’égalité étant déjà une notion fondamentale. Pour l’interprétation, une constante peut d’ailleurs déjà désigner plusieurs objets équivalents, sans que ça ne pose problème, même si ça n’est typiquement pas le cas si le domaine d’interprétation est l’informatique. Cette réponse n’est pas pertinente pour toutes les interprétations, mais elle est au moins une justification qui fait ne pas plus y voir un problème qu’avec le renvoi d’une constante, qui peut aussi être vu comme une équation à résoudre, mais simple, autant que l’est d’ailleurs une réponse comme « n’importe quelle valeur, exceptés celles‑ci ».

Ce n’est pas un gros problème, mais cette possibilité a‑t‑elle vraiment un intérêt ou n’aurait‑elle d’intérêt qu’à l’étape où la définition du langage a besoin de poser que certaines constantes sont distinctes ? Cette possibilité serait‑elle utile dans d’autres cas, autres que celui de la définition du langage ? De cette possibilité, serait‑il possible d’en dériver d’autres, plus fréquemment utiles ? Serait‑il possible de définir la négation par l’échec avec la non‑égalité ?

De la réponse à ces questions, dépend la réponse à cette question : pour le besoin de la formulation du langage dans ses propres termes, il est nécessaire de poser que certains noms de variables et de constantes, sont distincts d’autres ; est‑il préférable de le faire en définissant une non‑égalité ou en introduisant plus tôt que prévu, la « négation » par l’échec ?

Pour ce qui est de poser qu’une constante n’est pas égale à d’autres ou qu’un nom de variable n’est pas égales à d’autres, ça ne fait pas de différence, les deux option produiraient le même résultat, Oui ou Non, comme les règles de l’interprétation du langage, seraient toujours vérifiées avec des termes constants ; c’est à côté, ailleurs, que ces deux options deviennent différentes et font se demander ce que ça signifie.

Concernant la négation par l’échec, cette question posée plus haut est à rappeler : en supposant qu’elle n’est définie que sur des termes sans variables libres, comment interpréter la négation par l’échec dans les cas où elle n’est pas définie ?

Un test imaginaire sur l’égalité, avec des simples et doubles négation. D’abord avec deux constantes, égales puis non‑égales. Ces deux cas ne posent pas de problèmes, les requêtes portant sur des constantes. Puis le cas d’une variable libre avec une constante. Ce cas pose problème et est envisagé de deux manières. Il semble se confirmer que la négation par l’échec, doit être testée dans un contexte où la résolution des termes positifs est achevée, les variables ayant été fixées, même si elles restent libres.

Avec deux constantes égales :

(eq a a) ? -- Oui.
(neq a a) ? -- Non, pas de solution.
non (eq a a) ? -- Non, (eq a a) étant vérifiée.
non (neq a a) ? -- Oui, (neq a a) n’étant pas vérifiée.
non non (eq a a) ? -- Oui, « non (eq a a) » n’étant pas vérifiée.

Avec deux constantes non‑égales :

(eq a b) ? -- Non.
(neq a b) ? -- Oui et pas besoin de solution.
non (eq a b) ? -- Oui, (eq a b) n’étant pas vérifiée.
non (neq a b) ? -- Non, (neq a b) étant vérifiée.
non non (eq a b) ? -- Non, « non (eq a b) » étant vérifiée.

En supposant que A est une variable libre et que sous la négation « non », une variable non‑liée est traitée comme une constante différente de toutes les autres, une manière de formuler qu’elle ne garantit pas l’égalité avec quelque constante que ce soit :

(eq A b) ? -- Oui, A = b.
(neq A b) ? -- Oui, A = n’importe quelle constante sauf b.
non (eq A b) ? -- Oui, (eq A b) n’étant pas vérifiée.
non (neq A b) ? -- Non, (neq A b) étant vérifiée.
non non (eq A b) ? -- Non, « non (eq A b) » étant vérifiée.

En considérant virtuellement que neq est une négation de eq, les simple‑négations et les doubles‑négations, sont en accord, mais les simples négations renvoient un statut positif, comme eq, au lieu d’un statut opposé à eq. Pour eq vs neq, ça ne surprend pas, neq cherchant une solution et en trouvant une, de même que eq. De manière amusante, l’intrus semblerait être eq, mais c’est juste pour blaguer, parce que rien n’y est anormal.

En supposant que A est une variable libre et que sous la négation « non », avec une variable non‑liée, le status est renvoyé d’après sa capacité à être liée mais sans être effectivement liée, une manière d’être plus en accord avec le sens qu’aurait le terme en dehors de la négation « non » :

(eq A b) ? -- Oui, A = b.
(neq A b) ? -- Oui, A = n’importe quelle constante sauf b.
non (eq A b) ? -- Non, (eq A b) pourrait être vérifiée.
non (neq A b) ? -- Non, (neq A b) pourrait être vérifiée.
non non (eq A b) ? -- Oui, « non (eq A b) » n’étant pas vérifiée.

Les simple‑négations renvoient un status opposé l’un de l’autre, et les double‑négations, de mêmes. Ces résultats ne sont pas satisfaisant et confirme que la négation « non » doit se comprendre dans un contexte ou les variables sont fixées. Si la négation par l’échec est évaluée dans un contexte considéré comme fixé et non‑pas seulement en ne modifiant pas le contexte, alors elle est dans ces exemples au moins, en accord avec la non‑égalité, bien qu’elle fonctionne différemment.

Reste quand‑même que dans ce meilleur cas (celui d’avant le précédent) « non (eq A b) » renvoi un status positif qui peut être trompeur, mais même un statut négatif, cette négation est facile à mal lire de toutes manières. La non‑égalité est au moins plus claire, s’il est compris qu’elle cherche à une solution à une non‑égalité à moins qu’elle ne la vérifie ou l’objecte. Elle ne semble pas créer d’incohérence à la lecture, avec la négation par l’échec qui ne peut pas s’y substituer. La négation par l’échec est trompeuse à la lecture, autant appliquée à eq qu’appliquée à neq.

Par le seul fait que la négation par l’échec suppose une résolution achevée, des variables fixées, la double‑négation « non non A » ne peut pas être interprétée comme A.

Avec neq, la double‑négation n’est pas possible, la négation étant dans la règle, n’étant pas une négation appliquée à un terme. Mais « non neq » reste possible, même si ce n’est pas à proprement parler un doublement de la négation de neq, les deux négations n’étant pas de la même nature.

Pour la négation par l’échec, le message précédent semble indiquer qu’il n’est pas impossible d’interpréter une variable libre même après résolution, mais ça reste moins lisible et la cohérence est moins évidente que quand cette négation s’applique à un terme constant. Ça nécessite encore des investigations.

Comme une partie du problème est de savoir comment interpréter une négation non‑définie, peut‑être faudrait‑il une notion de « non‑défini » en plus des notions de « vérifié » et « impossible », la notion de « non‑vérifié » se comprendrait alors comme « non‑défini » ou « impossible ».

Concernant neq, cette idée nécessite encore des investigations pour les cas plus complexes qu’une constante et une constante ou une variable et une constante.

Pour facilité une vision d’ensemble, un résumé de l’évolution du status de la négation par l’échec et de sa relation avec la non‑égalité comme règle spécifique.

Il a d’abord été noté que vérifier par l’échec une chose qu’on sait impossible, n’est pas toujours possible, à cause des récursions infinies. L’idée a alors été posée qu’elle n’est peut‑être définie que sur des termes constants, comme ils ne sont pas sujets aux récursions infinies. Ça n’avait pas été écrit, mais une idée avait été que comme c’est en fin de résolution que tous les termes potentiellement constants sont effectivement constants, que alors c’est en fin de résolution qu’elle devrait être vérifiée. Plus tard encore et en parallèle de l’idée que la vérification de l’équivalence devrait se faire sans modifier le contexte, pour ne pas introduire d’incohérences, a été posée l’idée que la négation par l’échec devrait elle aussi se faire sans modifier le contexte, pour qu’elle n’introduise pas d’incohérences, elle non‑plus, et le moment le plus approprié pour figer un contexte sans que ça ne pose problème, est en fin de résolution. Ce sont en résumés, toutes les raisons qui ont aboutit à ces conditions pour l’application de la négation par l’échec.

Le règle spécifique de la non‑égalité est intéressante dans le sens où elle permet des solutions à des choses qui pourraient être formulées, mais sans qu’une solution ne puisse être représentée. En supposant, ce qui n’est pas encore certains, que la négation par l’échec soit définie même avec des variables libres, il est par exemple possible de formuler la requête « non (eq A b) & non (eq A c) », une chose qui pourrait être formulée, mais dont la solution n’aurait aucune représentation. Sous la forme « (neq A b) & (neq A c) », cette formulation a une solution représentée comme un « ensemble » d’exclusion, contenant b et c.

Pourtant, le fait que la même chose puisse être formulée de deux manières différentes, l’une renvoyant un résultat et pas l’autre, n’est pas satisfaisant. Le fait que les deux notions se recouvrent partiellement, n’est pas satisfaisant non‑plus et est même un mauvais signe. Pourtant, il ne semble pas possible de dériver l’une de l’autre. Si la requête « non (eq A b) & non (eq A c) » n’est pas permise ou non‑définie, alors elle n’a pas une double‑formulation, mais une seule, qui est « (neq A b) & (neq A c) ». Les deux notions se recouvriraient toujours quand‑même, dans le cas où elles portent toutes les deux sur des termes constants et ce recouvrement partiel n’en serait pas moins un possible mauvais signe.

Une solution à la superposition des deux notions de négation et un retour en amont concernant l’interprétation.

Une solution au fait suspect de la superposition des deux idées de la négation, pourrait être d’intégrer celle de la règle spécifique neq dans la négation par l’échec. L’unification sous une vérification négative, ne se comporterait pas en tous points comme sous une vérification positive.

Une condition de l’application de vérification négative, un nom plus approprié que « négation par l’échec », doit être revue. Il a été dit qu’elle ne doit pas modifier le contexte, pour ne pas introduire d’incohérence. Mais c’est justement cette condition qui pourrait être incohérente, en voulant résoudre un risque d’incohérence qui n’existe pas.

Dans une vérification, même négative, les règles doivent être testées et pour cela, être instanciées. La nécessité de l’instantiation des règles, fait qu’il n’est pas possible pour la vérification négative de ne pas modifier le contexte, ou alors ça signifierait qu’elle ne teste pas les règles comme elle le devrait, ce qui serait incohérent. La condition qu’elle doit vérifier et plutôt de ne pas contredire le contexte déjà produit. Contredire un contexte, serait par exemple couper la liaison d’une variable ou la lier à un terme incompatible. Ce n’est pas possible, quoiqu’il en soit, l’unification ne contredisant jamais les précédentes unifications. Il n’y a pas à poser de notion de non‑modification contradictoire du contexte, pour les vérifications négatives, parce que aucune modification contradictoire n’est possible. Inutile d’exclure une chose impossible.

La règle que les vérifications négatives ont lieu après les vérifications positives, reste maintenue. Les vérifications positives que doit faire la vérification négative, ne sont pas concernées. Ce qui justifie cette règle, est que la vérification négative est définie sur des termes sans variables libres et que ceux qui peuvent exister, existent à la fin de la vérification positives, alors qu’ils peuvent ne pas encore exister avant son achèvement, même s’ils le peuvent parfois.

Pourtant, une vérification négative peut avoir du sens, même avec des variables libres. Soit une requête « non (x A) ? », A étant libre, aucun terme ne correspondant à (x …). Cette vérification négative peut se conclure par Oui, comme rien ne permet de vérifier (x A), même avec A libre.

Il est assuré qu’une vérification négative est définie pour une requête sans variables libres, mais elle peut l’être aussi pour certaines requêtes avec variables libres.

La présence de variables libres peut faire que certains certains termes ne correspondent pas mais pourrait correspondre. C’est en présence de tels cas seulement, que la vérification négative n’est pas définie. Dans un tel cas, elle pourrait poser une condition sur la variable libre, garantissant qu’il n’y aurait pas de correspondance et garantissant la vérification négative. Elle pourrait le faire sans contredire les unifications précédentes, si elle ne le fait que sur des variables libres en définissant des exclusions finie. C’est justement ce qui est dans l’idée de la règle spécifique neq.

Mais cette possibilité intéressante n’est pas une nécessité, pour une raison d’interprétation sur laquelle il est revenu plus loin. Bien que intéressante, cette idée complique la définition et comme ce n’est pas une nécessité, elle est reportée à plus tardivement. Mais une partie de son interprétation peut être posée, pour ne pas considérer comme indéfinie des vérifications négatives qui pourraient pourtant être définies. L’unification de deux termes dans un contexte, peut se terminer de deux manières : soit l’unification est possible et elle renvoi un nouveau contexte vérifiant la correspondance des deux, soit elle échoue en se réduisant à un échec. Pour une vérification positive, toutes les unifications doivent être vérifiées. Pour une vérification négative, il suffit qu’une seule unification soit garantie non‑réalisable, mais elle doit quand‑même reconnaître les correspondances vérifiées.

Dans le cas précédent de « non (x A) ? » avec A libre et aucune tête de règle de la forme (x …), aucune tentative d’unification ne réussit. C’est le cas aussi avec « (eq a b) ? ». Avec « (eq A b) ? », une solution pourrait être trouvée, l’unification normale la produirait. Cette même unification sous une négation, en cas de possible solution, conclue à une solution et donc à l’échec de la vérification négative. En fait, elle n’a même pas besoin de produire cette solution, elle pourrait simplement renvoyé un status « une solution serait possible » et ce status serait suffisant pour conclure à l’échec de la vérification négative. C’est précisément la situation ambiguë qui pose problème. C’est ici que deux options se présentent et qu’une seule sera retenue, la seconde, offrant plus de possibilités, étant reportée. La première solution est que la vérification négative renvoi un status « non‑défini », qui n’est pas interprétable comme un status « Oui » ou « vérifié », ce qui est assez pour la cohérence de l’interprétation. Une solution intéressante mais reportée à plus tard, serait que l’unification sous une vérification négative, renvoi une solution résolvant l’ambiguïté, cette solution, ne peut que avoir la forme d’une exclusion. Cette solution ne contredirait pas la résolution positive, puisqu’elle s’appliquerait aux variables libres. Si la vérification positive a conclut qu’une chose est vraie avec une certaines variables pouvant avoir quelque valeur que ce soit, aucune incohérence n’est introduite en ajoutant « n’importe quelles valeurs, excepté celles‑ci », comme l’exclusion de certaines possibilité ne change rien à la conclusion positive pour les autres valeurs restant possibles.

C’est ici qu’une interprétation faite dans l’idée de la règle spécifique neq pourrait être incorporée à la vérification négative en générale. Cette règle spécifique n’existerait plus, et la vérification négative, en présence de variable libres faisant qu’une vérification positive resterait possible, serait une recherche de contrainte sur ces variables libres, garantissant que la vérification positive ne serait pas possible, garantissant par là, la vérification négative.

Pour le moment, seule la condition produisant une ambiguïté est retenue, renvoyant un status spécifique, distinct de « Oui » ou « vérifié ».

Ce qui justifie de remettre à plus l’idée d’une recherche de contraintes assurant une vérification négative, est que l’interprétation n’en a pas besoin.

Certes, les requêtes peuvent être faites sur des variables, mais ce n’est pas l’interprétation des règles définie par la sémantique, c’est seulement un effet secondaire utile en pratique. Ceci dit, il serait possible de définir l’interprétation d’une requête portant sur des variables, mais strictement, elle n’a besoin d’être définie que sur des termes constants. C’est là un retour en amont encore plus lointain que celui qui a déjà eu lieu.

Prenons le cas du langage défini ici, et imaginons que ses règles aient été posées dans ses propres termes. Ces règles ne disent pas comment l’interprétation est faite, elles disent ce qu’elle est. La question de savoir comment elle est faite est à résoudre à côté, de quelque manière que ce soit, mais quelque soit la manière dont elle le fait, elle doit vérifier les règles posées.

Que signifierait une requête portant sur une variable dans ce contexte ? Réponse : rien de concret. Ça peut surprendre, mais ça se comprend avec un exemple. Les règles de la syntaxe étant posée, on veut vérifier qu’un terme est conforme à la syntaxe définie, c’est à dire qu’on a un terme représentant une formule et qu’on vérifie si ce termes est conforme aux règles de la syntaxe. Eh bien une variable libre dans ce termes n’a pas de sens pour l’interprétation qui nous intéresse, elle signifierait qu’on se demande si une formule non‑fixée est valide ou pas. On peut lui donner un sens, mais ce sens n’est pas nécessaire pour savoir si une formule concrètement écrite est valide ou pas. Il en va de même pour toutes les inférences, supposées concrètes et non‑pas partiellement indéfinie, ce que signifierait la présence d’une variable libre.

Ceci justifie de reporter à plus tard la possibilité de recherche de contraintes dans une résolution négative, comme elle est supposée se faire sur des termes constants de toutes manières.

La vérification négative sous une requête ne portant sur aucune variable libre, n’est plus sensible à l’ordre des termes. Il serait alors possible de permettre aux termes négatifs, d’apparaître au milieu des termes positifs, le tout dans n’importe quel ordre. Mais cette idée n’est pas retenue, parce que même si revenant en amont, on ne se préoccupe que de l’interprétation des termes sans variables libres, on sait que en présence de variable libres, cet ordre est important et comme poser que les termes négatifs se vérifient à la fin, n’a pas de coût en terme de complexité de la définition et ne fait rien perdre à l’interprétation, cette idée est conservée, même si pas nécessaire pour le moment, en prévision de l’avenir.

Un complément au message précédent, pour le clarifier avec des exemples plus concrets.

Imaginons qu’un ensemble de règles, définisse les opérations arithmétiques élémentaires et nécessairement aussi, une syntaxe pour les représenter.

Les règles valideraient par exemple ceci : « (égale (plus 1 2) 3) ». Elles ne validerait pas ce terme : « (égale (bidule 1 2) 3) ». Ce terme ne serait pas validé non‑plus : « (égale (plus 1 2) 4) ».

Que signifierait vouloir vérifier un terme comme par exemple celui‑ci : « (égale (X 1 2) 3) » ? Ça ne signifierait rien de concrètement interprétable avec une conclusion Oui ou Non. La raison est que le terme n’étant pas entièrement déterminé, la variable X étant ce qui le rend indéterminé.

C’est du moins le cas pour l’interprétation à laquelle il est nécessaire de revenir avant de à nouveau aller plus loin. Parce que une interprétation de « (égale (X 1 2) 3) » pourrait être par exemple Possible tandis qu’une interprétation de « (truc (X 1 2) 3) » ou même « (truc (plus 1 2) 3) », serait Impossible. Allant plus loin, le principe de la résolution pourrait être réintroduit en posant que Possible s’accompagne d’un exemple de solution. Dans le cas de « (égale (X 1 2) 3) », Possible s’accompagnerait de X = plus. Cette possibilité ne serait pas encore une recherche exhaustive de solutions., qui n’a peut‑être en fait même pas besoin d’être posée par la définition du langage.

La conclusion Possible aurait un coût faible, tout en permettant une conclusion utilement interprétable, comme cas bien distinct de Impossible. Possible et Impossible ne serait pas interprétables comme Oui, qui serait un synonyme de Vérifié, mais pourraient tous les deux être interprétables comme Non‑Vérifié, le Non tout‑court étant un synonyme de Impossible. Mais la possibilité de ces interprétations n’est même pas nécessaire au point en amont où il est utile de revenir. Comme illustrer plus haut, la possibilité de vérifier des termes entièrement déterminés, sans variables libres, est suffisante.

Même si elles ne sont pas une nécessité, ces interprétations peuvent être étudiées et être envisagées dans le contexte d’une vérification négative, la définition ayant posée problème. Il a été vu que « (eq A b) ? » pourrait être interprété comme Possible. À première vu, « non (eq A b) ? » pourrait aussi être interprété comme possible. Mais ce serait plutôt une possible contradiction. En effet, « (eq A b) & non (eq A b) ? » est évidemment impossible, alors si les deux termes se concluaient par Possible et qu’on en concluait Possible, on aurait une contradiction. Cette contradiction disparaît si sous une vérification négative, une possibilité s’interprète comme Indéfini. Dans ce cas, « (eq A b) & non (eq A b) ? », se conclut par Indéfini. Ça devrait être le cas pour « non (eq A b) & (eq A b) ? » également et alors Possible & Indéfini devrait se conclure par Indéfini (ou Incertain ?). Possible ne pourrait se conclure que de Possible & Possible & etc. Cependant, « (eq a b) ? » ayant l’interprétation Impossible, « non (eq a b) ? » pourrait avoir l’interprétation Vérifié et « (eq a b) & non (eq a b) ? » pourrait avoir l’interprétation Impossible. Impossible & Confirmé se conclurait par Impossible.

Cette possibilité ultérieure de plusieurs interprétations et des interprétations de leurs conjonctions, en plus des seules interprétations Oui ou Non, serait à étudier. Mais pour le moment, il est décidé de s’en tenir à l’interprétation de termes entièrement déterminés, sans variable libres. La prochaine mise en œuvre se limitera d’ailleurs à cette interprétation, ce qui peut surprendre après avoir eu une mise en œuvre plus élaborée, mais c’est préférable.

Comme dit précédemment, certaines idées qui ont été étudiées, n’étaient pas sans intérêts, mais ces idées ont été introduites trop tôt. La question de définir le langage dans ses propres termes, est venue à un moment où le langage était déjà trop élaboré, compliquant l’étude de cette question. Revenir à un langage plus simple, devrait faciliter sa définition dans ses propres termes. Seulement ensuite, les idées étudiées seront progressivement réintégrées. Elles seront même probablement réintégrées en les définissant alors mieux, comme une possibilité en est illustrée par l’exemple plus haut, des interprétations comme Possible, Impossible, Confirmé, Indéterminé, et peut‑être d’autres qui se montreront nécessaires.

Après l’égalité mystérieuse venue d’un univers parallèle (il faut imaginer la musique d’un teaser d’Harry Potter ou quelque chose comme ça), voici le hasard magique qui peut réaliser des choses avant même de savoir comment les réaliser (chimes and cowbells …).

Sans la résolution renvoyant des résultats à une requête, on peut croire avoir perdu la possibilité d’un exemple de solution accompagnant une conclusion Possible. Pourtant non, en théorie, il est toujours possible de générer des termes aléatoire à associer aux variables et pour chaque terme déterminé ainsi généré, de tester s’il est vérifié ou non. Quand un terme déterminé produit, est interprété comme Vérifié, il est retenu, par exemple en l’affichant. Il est aussi possible d’appliquer cette idée aux termes tout‑court, sans variables libres, générant des termes vérifiés par les règles, sans aucune procédure certaine de production de ces termes.

Le hasard est aussi une réponse sans incohérences, à une précédente remarque de l’étrangeté apparente qu’il y a à valider la définition d’un langage écrit dans ses propres termes, avant même que ce langage n’ait été défini. En théorie, une probabilité même extrêmement très faible, n’étant pas une impossibilité, il est possible d’imaginer quelque chose comme suit : le hasard produit matériellement quelque chose qui soit lisible d’une manière ou d’une autre, comme des règles interprétables par quelque chose, un quelque chose qui serait lui même matériellement produit par hasard. L’interprète produit par hasard validerait des vérifierait des règles produites par hasard, ces règles correspondant à ses propres règles d’interprétation. Quand il a été dit qu’une mise en œuvre de l’interprétation d’un langage peut être créée avant même que la définition du langage n’ait été posée, disons que en pratique, le hasard peut être beaucoup aidé, ce qui en soit, reste un sacré mystère quand‑même.

La possibilité de générer des termes aux hasard pour tester si oui ou non ils vérifient des règles, en lieu et place de la résolution, sera intégré à la mise en œuvre du nouveau langage de base. Les termes produits seront tous déterminés, il n’y aura donc jamais de récursion infinie pendant leur vérification. La probabilité que la génération d’un terme aléatoire ne se termine pas étant extrêmement faible et étant possible de la limiter arbitrairement, pourvu qu’on puisse attendre des secondes ou des minutes voir quelques heures dans le pire des cas, on pourrait toujours avoir des exemples de solutions aux règles définies ou avoir des exemples de solutions pour les variables de termes indéterminés. Cette possibilité serait même plus intéressante que la procédure de résolution dont il a été question, dont a a vu qu’elle produit parfois des listes décevantes, car peu illustratives de ce que les règles vérifient. Le hasard pourrait produire des résultats plus intéressants et plus illustratifs qu’une procédure de résolution.

Le moment venu, des exemples de telles solutions produites seront présentés.

Remarque : ici, l’ensemble infini de l’interprétation de Herbrand, est remplacé par le hasard. Encore un ensemble infini dont on se débarrasse. Une réalisation par la magie du hasard est préférable au problème sans solution d’une réalisation impossible.

Commentaires et compléments sur des points variés précédemment abordés.

En introduisant les compositions horizontales et verticales, cette interprétation avait été proposée : la composition horizontale est comme un axe, les compositions verticales sont comme des dimensions, chacune ayant un axe. Puis il avait été dit que ces dimensions ont une relation d’ordre entre elles. Ce n’est peut‑être ce qu’elles sont le plus. Elle sont surtout imbriquées, l’une étant dans le contexte d’une autre plus englobante et y voir une relation d’ordre, ne serait qu’y voir une représentation possible des relations d’ordre. Voir la composition verticale comme une imbrication, résous le problème de l’interprétation de la liste. On peut voir une représentation d’un espace à plusieurs dimension dans un arbre, mais moins dans une liste et la représentation de la liste possiblement vue comme un arbre dégénéré, semblait étrange. Cette bizarrerie n’est plus, si on pense surtout à une imbrication. C’est finalement ce qui était suggéré en disant que pour arriver à un élément d’une liste, il faut passer par tous ses précédents, c’est à dire qu’arrivé à un élément, on est dans un contexte où on est passé par tous les précédents. C’est ce qui explique pourquoi essayer d’imaginer une représentation autre que la liste pour représenter les cas où une couverture exhaustive est requise, cette recherche d’une autre représentation se conclu par une absence d’autres idées. Ça ne change rien au fait que même si on peut avoir une représentation équivalente de la composition horizontale avec une liste, ça n’en est qu’une représentation qui ne la remplace, car comme remarqué, sans la composition horizontale, pas de liste. On peut l’interpréter comme telle, mais elle ne peut pas la remplacer.

Il a été envisagé que même pour le nouveau langage de base, les termes négatifs seraient toujours écrits et testés, après les termes positifs. Cette idée est abandonnée, il pourront apparaître à n’importe quelle position de la conjonction, comme les termes positifs. Ce qui le justifie, est la remise en cause de la précédente justification de les mettre à la fin : c’était parce que la négation par l’échec n’est convenablement définie qu’avec des termes constants, qu’on a le plus probablement en fin de résolution. Mais une autre négation a été envisagée, la négation par la résolution d’exclusions, qui elle, ne nécessite plus de vérifier les termes positifs en fin de résolution.

Même si elle est plus complexe, la négation par la résolution d’exclusions sera probablement privilégiée à la négation par l’échec, dans une future définition plus complète du langage. La raison est que la négation par l’échec dans un contexte de résolution (ce n’est pas le cas dans un contexte de vérification seulement), fait que les termes négatifs se comportent trop différemment des termes positifs. Les termes positifs, dans une résolution, participent à fixer les variables, mais pas les termes négatifs. Le problème avait été illustré en imaginant une requête ne contenant qu’un terme négatif, renvoyant un status positif, mais ne fixant par la variable contenu dans le terme, contrairement à ce qu’aurait fait une requête sur un terme positif. C’est trop dissonant. Pour cette raison, la négation sera une négation par l’échec seulement dans le nouveau langage de base qui ne vérifiera que des termes constants. Puis quand la résolution sera réintroduite, les termes négatifs participeront à la résolution, comme les termes positifs, même si la mise en œuvre s’en trouvera compliquée.

L’idée envisagée de représenter les termes cycliques, n’avait même pas été mise en œuvre dans la précédente version du langage qui appliquait même le test d’occurrence (occur check) pour s’assurer d’exclure les termes cycliques. Alors pourquoi introduire les termes cycliques, dès la définition initiale du nouveau langage de base ? La raison de l’exclusion des termes cycliques produits, était : ce qui est interprété, est le développement d’un résultat sous une forme constante, entièrement déterminé, et avec un terme cyclique, ce développement ne se termine jamais. Mais une formulation de la situation en prenant la question par l’autre bout, aurait donné ceci : il n’y a pas de représentation pour les termes cycliques, alors il ne peuvent pas être posé pour vérification, de toutes manières. Cette autre manière de voir la question avait été manquée. Les règles pouvant vérifier des termes cycliques, il est étonnant qu’ils ne puissent pas être vérifiés, pour la raison que étonnamment, ils ne peuvent pas être écrits. C’est une bizarrerie, puisque les règles sont censées permettre de vérifier si un terme écrit est conforme aux règles ou pas. Que les règles permettent décrire des choses qui ne peuvent pas être écrites, est dissonant. Même en l’absence de possibilité de les écrire directement, les exclure des résultats quand ils sont produits, est déjà assez étrange aussi. Les termes cycliques sont souvent présentés comme une aberration, dans la littérature, alors qu’ils ne sont pas incohérents. L’aberration ne serait‑elle pas plutôt d’écrire des règles produisant des termes cycliques et de s’étonner qu’ils puissent alors être produits par les résolutions ? Pour cette raison au moins, filtrer les termes cycliques au moment où ils se produisent, ne me semble même pas avoir l’intérêt pédagogique parfois avancé, même au contraire. Dire que l’on peut écrire des règles permettant de produire des choses que la résolution se chargera de filtrer aussitôt qu’elle les produira, c’est laisser prendre une mauvaise habitude, celle de poser comme correctes des choses qu’on considère comme incorrectes. C’est plutôt là que serait l’aberration. Il y a en plus au moins une bonne raison pratique de les permettre. Les termes cycliques ne sont pas toujours qu’une curiosité juste non‑incohérente, ils peuvent être une nécessité. Il a été prouvé par des mathématiciens, que la partie non‑entière des nombres rationnels écrit dans une base quelconque (pas sous forme d’une fraction), se terminent toujours par une partie cyclique se répétant à l’infini, cette partie pouvant être un zéro. Sans représentation des termes cycliques, il ne peut donc pas y avoir de représentation exacte des nombre rationnels dans une base quelconque. Le seul fait que les termes cycliques soient nécessaires pour une certaine forme de représentation des rationnels, justifient de ne pas y voir qu’une curiosité, mais une nécessité dans certains domaines.

Précédemment, a été à nouveau abordée l’idée d’affiner les status des requêtes pour les interpréter. Une occasion de ce genre a été manquée, en sautant directement à l’étape d’un langage de résolution sans passer par l’étape d’un langage de vérification seulement. Pendant une résolution, plusieurs solutions peuvent être trouvées. Mais aussi, une solution peut avoir plusieurs vérifications. Ça avait été évoqué, mais ça ne ressortait pas, comme pour vérifier si une solution avait plusieurs vérifications, il aurait fallut bien inspecter la liste des solutions pour y chercher des doublons, sans encore de garanti qu’un doublon ait bien été produit pour une solution ayant plusieurs vérifications. Pour la définition du nouveau langage de base, il sera prévu que même après avoir trouvé une vérification d’un terme, il continue à en rechercher d’autres possibles. Le status Vérifié serait précisé en deux status, Vérification Unique et Vérifications Multiple.

Précédemment, il a été dit que la convention de toujours commencer un terme par une constante, peut éviter la confusion entre des constantes désignant des choses différentes et ayant pourtant le même nom. Il a été dit que cela peut être évité en s’assurant de toujours donner un nom différent à des choses différentes. Mais cette convention ne met même pas à l’abris de tous les mélanges de significations, il n’est pas possible de toujours s’en prémunir, en seulement nommant différemment les choses différentes. Il n’y a pas que le nom qui distingue une chose, sa position dans un terme, autant, et si deux choses à deux positions différentes dans un terme peuvent être les mêmes tout en ayant un sens différent, rien n’empêche ce mélange, à moins de toujours associer une position dans un terme à une constante unique, unique non‑pas seulement à travers toutes les positions dans un terme, unique aussi à travers toutes les positions dans tous les autres termes écrits dans les règles. Sans vouloir dire que ça doit être fait, il s’agit seulement de souligner que ce mélange de signification pourrait se produire de cette manière aussi.

Même avec la négation vu comme une forme de résolution, « non non P » ne signifie pas P, la différence importante pour certaines logiques, déjà abordée.

En posant qu’une exclusion pour A, un ensemble infini de termes possibles, réduit à un ensemble fini de termes exclus, est autant une solution pour A qu’une liaison de A à un terme, « non (r A) » signifie « il existe une solution pour A, tel que (r A) est garanti impossible ». Alors « non non (r A) » signifie « il n’existe pas de solution pour A, tel que (r A) est garanti impossible », ou plus brièvement, « non (r A) n’a pas de solution », ce qui n’est pas la production d’une solution pour A tel que (r A) ; au contraire d’une solution, la conclusion est que aucune solution ne peut être produite (non‑pas pour (r A), mais pour « non non (r A) », (r A) pouvant quand‑même éventuellement avoir une solution. »).

La logique définie ici est donc une de ces logiques pour lesquelles « non non P » n’est pas équivalent à P.

Avec une vérification de termes constants, l’instantiation d’une règle n’a plus besoin d’instantiations de variables, comme les variables d’une règle, sont immédiatement substituées par des termes (transmis par la tête de la règle). Avec cette restriction du nouveau langage de base, les variables n’existent que dans l’écriture des règles. Les règles sont quand‑même toujours instanciées, d’une certaine manière.