Les logiques : notes en vrac

Sur l’idée du diagnostique des causes d’échec de vérification impliquant des hypothèses.

Le problème des hypothèses jusque maintenant, est qu’elles occasionnent des faux désaccords par ignorance de certains faits. Ces faux négatifs ne sont pourtant pas une catastrophe, ils restent absolument moins graves que s’ils étaient des faux positifs, qui seraient des incohérences. On ne peut pas vérifier tout ce qui devrait pouvoir l’être ; cette lacune est dut à ces possibles faux désaccords, faisant manquer des solutions qui ne seraient peut‑être pas contradictoires avec des variables ordinaires. Même si un précédent message essayait d’équilibrer la perception de cette lacune des hypothèses avec la perception d’une lacune assez équivalente avec les variables ordinaires, cette lacune avec les hypothèses, est plus embêtante qu’avec les variables ordinaires. Plus embêtante, parce qu’avec les variables ordinaires, cette lacune s’exprime par une vérification qui ne se terminerait jamais, ce qui a l’avantage d’être perceptible, d’être facile à distinguer des cas où la requête se termine. Avec les hypothèses, la lacune correspondante, ne se distingue pas, la requête se termine même quand elle n’a pas vérifié ce qui aurait put l’être pour une certaine interprétation.

Pour une certaine interprétation, c’est important à souligner. Ce message va ébaucher une idée de diagnostique qui pourrait être une piste de réflexion, autant pour cette réinterprétation que pour l’ajout d’un éventuel nouveau concept au langage. Ce qui devrait être réinterprété, n’est pas tant les hypothèses que les conclusions négatives faites à partir de ces hypothèses. Ce serait une bonne idée de ne pas envisager un ajout sans avoir d’abord fait ce qui est possible sans. Ce qui est possible sans, c’est de reformuler l’interprétation des hypothèses, d’une manière rendant leurs limites moins inattendues. Un ajout pour répondre à un problème dont les termes seraient formulés ou mal compris, ne serait de toutes manières pas une bonne idée, ce serait le poser sur de mauvaises fondations.

Au moins une formulation de leurs limites a déjà été formulée, mais la formuler n’aide pas à s’en satisfaire : une conclusion sous une hypothèse, n’est pas une conclusion sous la cause de l’hypothèse. Dit autrement, si A implique B, que B est posé en hypothèse, on a pas le fait A avec l’hypothèse B, on a que l’hypothèse B et rien d’autre. C’est facilement problématique, il est difficile de faire avec B sans supposer sa cause. Mais le rendre possible amène un autre problème : il faudrait pouvoir peut‑être en faire autant avec les causes de B, elles‑mêmes. Intuitivement, ça évoque l’idée de pouvoir appliquer les règles à rebours. Mais avec les chaînes d’inférences, qui notent ce qui est appliqué pendant la vérification des règles, on en a au moins une trace. Oops, ces idées sont sorties trop spontanément, il faut maintenant les oublier, au moins pour un temps.

Avant d’ébaucher l’idée d’un diagnostique de cette limite, un diagnostique qui pourrait être affiché avec le résultat d’une requête pour aider à l’interpréter, on peut justifier l’idée de ce diagnostique.

Précédemment il a été dit qu’on pose une exemple de résolution d’une hypothèse pour la prouver, que si on ne craint pas de faire une bêtise, on peut aussi prétendre la preuve de cette hypothèse sans la faire, en la tenant pour un axiome. Comme les axiomes sont dangereux, les conclusions impliquant un axiome, peuvent devoir être marquées comme telles. C’est une sorte de traçabilité permettant d’interpréter une conclusion en connaissance. Ce principe est appliqué par exemple dans l’assistant de démonstration HOL4, mais d’autres incluent probablement la même option.

Noter que la conclusion positive d’une requête n’a pas put se faire sans utiliser un certain axiome, se comprend facilement. L’idée serait la même, excepté que le diagnostique porterait sur les requêtes dont la conclusion est négative, les requêtes ne renvoyant pas de résultat. Ce diagnostique, s’il est assez pertinent (ce qui n’est pas gagné), pourrait aider à interpréter le résultat, par exemple savoir s’il n’y a pas de solution parce qu’une solution serait vraiment contradictoire ou parce qu’un faux désaccord a fait passer pour contradictoire ce qui ne l’est pas vraiment.

Comme rappelé précédemment, quand deux termes sont unifiés, si au moins l’un des deux est une variable liée à Any, il n’y a jamais de désaccord, même si l’un des deux termes est une constante spéciale. Ce n’est que quand deux termes sont unifiés, qu’il peut y avoir désaccord. Que les termes, soient posés directement tel‑quel dans le texte du terme ou soient posés indirectement par la liaison d’une variable, n’y change rien. Pour noter un détail, les constantes spéciales ne peuvent être posées que par une variable, ces constantes ne pouvant pas être écrites ; c’est une nécessité, qu’elles ne puissent pas l’être.

On pourrait déjà distinguer deux catégories de termes : les termes ordinaires et les constantes spéciales. Si un terme ordinaire se trouve contenir une constante spéciale via une variable, la récursion qui a lieu pendant l’unification, fera de toute manière prendre ce cas en compte. Le cas du désaccord entre deux termes ordinaires, ne laisse pas de doutes. Le désaccord ne peut laisser un doute que si au moins un des deux termes est une constante spéciale. On peut distinguer alors deux cas, le cas de l’accord entre un terme ordinaire et une constante spéciale et le cas de l’accord entre deux constantes spéciales.

Le cas entre un terme ordinaire et une constante spéciale, échoue toujours, parce qu’on ne peut unifier que deux constantes identiques. Mais ce cas présente des possibilités de faux désaccords, comme on ne sait pas à quel collection de termes pourrait correspondre la constante spéciale. Au moins un cas de désaccord peut pourtant être certain. Une variable ne peut pas être liée à un terme désignant cette variable (directement ou indirectement), c’est pour cette raison que si une unification produirait un terme cyclique, il y a échec de l’unification. Si un tel cas est détecté, mais avec les constantes spéciales, le désaccord peut être tenu pour certain. Un problème, est qu’une variable n’est définitivement fixée, que quand une tentative de solution a été entièrement traitée. Il reste alors peut‑être encore un doute, faisant que ce cas de désaccord certain pourrait passer pour incertain. Sinon, pour le détecter, il faudrait vérifier si le terme qui ne peut pas être unifié avec la constante, désigne ou pas la constante elle‑même (via une variable, impossible autrement). Si oui, le désaccord est certain, il est incertain dans le cas contraire.

Reste le cas entre deux constantes spéciales. Si les constantes proviennent de la même hypothèse (pas de la même instance d’hypothèse posée, mais de la même hypothèse) et que les deux constantes correspondent à la même variable, l’unification échouera si elles ne sont pas de la même instance, mais il est compréhensible de suspecter que ces deux constantes pourraient désigner la même chose. Ce cas pourrait être noté comme suspicion de faux désaccord. Un exemple rendra le cas plus clair. Soit l’hypothèse prouvée ⟦(r A)⟧ , soit deux instances posées pour cette hypothèse, ⟦(r B)⟧ et ⟦(r C)⟧ . Ces deux hypothèses posées, sont deux instances de la même hypothèse. Il est assez envisageable, même si sans certitude, que B et C pourraient désigner le même terme, même si étant représentée par deux constantes différentes, leur unification échouera. Ceci justifie la suspicion de faux désaccord.

Les autres cas serait considérés comme sans certitude mais aussi pas sans doute. Une échelle de certitude devrait être posée, et la suspicion ou la certitude la plus élevée, serait retenue, si plusieurs sont notées.

Ça fait peu de chose. Un cas permettant de confirmer un désaccord, mais encore sous réserve qu’il ne soit pas manqué, et un cas de suspicion de faux désaccord avec une justification raisonnable. Le reste serait entre les deux.

Heureusement qu’il ne s’agit que d’un diagnostique, pas d’une règle de calcul, parce que ça laisserait à désirer. Quoiqu’il en soit, ça pourrait être intéressant à mettre en œuvre.La mise en œuvre devrait tester tous les termes d’une règle, même quand l’évaluation normale s’arrêterait avant. Un exemple fera comprendre pourquoi. Soit la règle A : B & C & D. Si C provoque un échec suspecté d’être un faux échec, le reste de le règle n’est pas testé, parce qu’il y a un échec tout‑court, le diagnostique n’y changeant rien. Mais il se peut que D aurait produit un échec certain et c’est cette certitude, qui devrait être noté. Pour ne pas la manquer, devant l’échec de C, il faudrait revenir au contexte précédent, ignorer C et tenter D. Comme C a échoué, la règle doit échouer même si D n’échoue pas et que C a été ignoré. Ça complique les choses, pour un diagnostique incertain, alors il n’est justement pas certain qu’il sera mis en œuvre et réellement testé (surtout que d’autres choses sont toujours en attente).

Ce diagnostique ne pourra pas être une solution, il faudra en trouver une à proprement parler. Il y a au moins deux pistes et les deux sont peut‑être liées. L’une serait d’attacher plus d’informations aux hypothèses, quoique ça peut déjà se faire en utilisant une hypothèse plus appropriée qu’une autre. Comme dit plus haut, la chaîne d’inférences, pourraient être utile en ça (celle de la preuve de l’hypothèse, mais il peut y en avoir plusieurs, de ces preuves). Pour rappel, le problème est que quand une hypothèse n’est pas approprié, elle peut faire à tord croire qu’on a conclut à l’impossibilité d’une chose, sans dire que c’était surtout que l’hypothèse ne permettait pas de remarquer une possibilité qui pourrait bien exister. Une autre piste, comme le problème se pose avec les faux désaccords, serait d’exiger que quand il s’agit de généralité, les échecs doivent être explicitement prouvés en prouvant une contradiction, et que l’échec d’une requête qui pourtant se termine, n’est pas une preuve d’une impossibilité. Cette piste aurait le mérite de ne pas laisser de doute. Il n’y a pas de doutes sur les réponses positives, il n’y en a que sur les réponses négatives, négative par l’échec, alors prouver explicitement les impossibilités, est une solution tentante. Reste à savoir comment ces preuves pourraient être faites.

La deuxième piste fait revenir la question de la négation. Cette définition de la négation par la preuve de la contradiction et non‑pas par l’échec d’une requête, est autant tentante que la piste qui l’introduit. Sous réserve qu’une méthode de preuve adéquate soit trouvée. Elle devrait en tous cas, découler naturellement de la notion de contradiction présente dans le langage, c’est à dire l’impossibilité d’unifier deux termes et la contradiction entre deux termes, voulant chacun réaliser une unification contredisant une unification voulue par l’autre terme ; excepté que cette fois, il faudrait l’appliquer aux variables représentant des généralités.

Je crois que la meilleure piste, est celle de la preuve explicite de la contradiction, mais une idée vague n’est pas une formulation.

Ça s’annonce difficile …

Surtout que ça devra pouvoir s’expliquer clairement.

Une omission dans le précédent message. Ça a été dit, mais pas très explicitement. Il y a un mois, avait été suspecté que à moins que des règles n’aient pas de sens (non‑satisfiables), une requête ne portant que sur des constantes, doit toujours se terminer. C’est une conviction, sans preuve.

Les requêtes sur des généralités sont comme des requêtes sur des constantes, alors des requêtes qui ne portant que sur des généralités et/ou des constantes, devraient toujours se terminer, aussi.

Sans rapport directe, peut‑être une interprétation intuitive des constantes dans le langage de base, serait justement de les voir elles aussi, comme des généralités.

Encore sur les constantes, cette fois, avec les variables. Il avait été dit que les variables ne peuvent jamais capter les constantes représentant les relations. Dans le langage de base décrit, une constante ne peut pas non‑plus apparaître à la place d’une constante représentant un constructeur, mais sans à proprement parler pouvoir capter la constante d’un constructeur, elle est peut représenter l’application d’un constructeur, quand‑même. Si une variable V est liée quelque part à un terme, disons (c A), la variable A peut être liée ailleurs, comme si elle était une déclaration d’argument, et la variable V, pourra propager ailleurs le choix de ce constructeur, par liaison de variables aussi. Même si une variable ne peut pas désigner un constructeur, parce qu’elle ne peut pas apparaître à la place d’un constructeur, elle peut quand‑même désigner l’application d’un constructeur de choix variable (sous réserve de cohérence).

Si la négation est l’interprétation de l’impossibilité, la seule définition certaine de la négation jusque là, est celle de la négation de la négation. Si on a une preuve de A, alors on a une preuve de « non non A ». Ça ne doit pas être confondu avec la démonstration par l’absurde, « A implique non non A », n’est pas la même chose que « non non A implique A ». Plus encore, si la seule démonstration possible de non non A est une preuve de A, ce serait tourner en rond.

Ceci implique aussi que pour prouver non A, il faut prouver que aucune preuve de A n’est possible. Cette remarque sembler revenir au point de départ, mais on peut la voir comme la nécessité de vérifier tous les cas possibles, ce qui en dit un peu plus. C’est le problème de cette couverture, qui me semble pour le moment insoluble. En tous cas, la nécessité de cette couverture, signifie que faire une preuve négative est plus difficile que faire une preuve positive, que ça nécessite plus de certitude.

Note à propos de la notation. Dans ce qui suit, les conjonctions seront noté sans « & », ça vient plus naturellement ainsi, comme des mots se suivant dans une phrase. Je crois que la syntaxe sera modifiée dans ce sens. Quand plusieurs connecteurs binaires (arité 2), sont présents, noter la conjonction est utile, mais pas quand elle est le seul connecteur binaire qui peut donc être implicite. Le symbole « & » garde sont intérêt en présence d’autres connecteurs.

Note à propos du vocabulaire. Souvent, il été fait mention de requête sous une hypothèse. Le mot me semble trompeur, il serait plus approprié de parler de requête avec une hypothèse. Parler de requête sous une hypothèse, évoque plutôt quelque chose comme ⟦H⟧ ==> T, alors que les requêtes sont plutôt ⟦H⟧ & T. J’essaierai d’y faire attention à partir de maintenant.

Disons qu’on veut démontrer non A. On sait que si une seule preuve de A est possible, on a non non A et que non A est alors impossible, puisque la négation est ici, l’impossibilité. Si par exemple le terme A peut correspondre à deux règles, soit B : C D et E : F G. Il ne suffit pas de constater que A ne peu pas être vérifié par la première règle, parce qu’il suffit que A puisse être vérifié par la seconde règle, pour que conclure la négation de A sur la base de l’impossibilité de la première règle, soit incohérent. On ne peut conclure non A que d’après le constat que les deux règles sont non‑applicables.

Note : ici, par l’échec des règles, ils ne faut pas comprendre cela comme des règles non‑satisfiables en général, il faut le comprendre comme non‑satisfiables étant donné les liaisons des variables dans le terme A. Une règle non‑satisfiable est quand‑même un exemple de négation.

Pour prouver non A, il faut alors connaitre toutes les règles qui pourraient éventuellement prouver A est s’assurer qu’aucune ne correspond finalement. Jusque là, ça ressemble à une requête ne renvoyant simplement pas de résultat. Où est le problème alors ? On a vu que l’absence de résultat à une requête, ne peut pas toujours s’interpréter comme la négation. Contradiction ? Non, les faux négatifs se produisent seulement avec des requêtes avec hypothèses. Ça ne doit pas faire oublier que si une requête ne dépend pas d’hypothèses, la négation peut être conclue, si la requête se termine sans solution (mais si elle ne se termine pas ou est stoppée arbitrairement pour cause de récursion trop profonde, on ne peut rien conclure). C’est déjà ça, une définition de la double négation et une définition de la négation, hors hypothèse. Ça ne fait pas avancer non‑plus, c’est juste une mise au clair, le problème initial n’est toujours pas résolu.

Le problème n’est toujours pas résolu, mais ce précède, inspire de reformuler deux choses.

La première, est l’idée de diagnostique, précédemment proposée. Le diagnostique décrit, laissait à désirer. Il serait plus simple et peut‑être presqu’aussi précis, de réduire le diagnostique à l’utilisation d’hypothèses ou non. Une requête peut se terminer par Yes (avec ou sans variables à afficher) ou par No. En cas d’absence de solution et si des hypothèses ont été impliquées pendant la tentative de recherche de solution, Unsure serait affiché au lieu de No. Ce serait plus simple, mieux défini et autant satisfaisant pour la plupart des cas. Ceci, sous réserve qu’aucune solution ne soit trouvée. Même si une solution était trouvée, cette idée pourrait s’appliquer au langage tel que décrit jusqu’ici, c’est à dire sans l’éventuel futur ajout qui viendra.

La seconde est que précédemment, le problème avait été formulé en terme de manque d’information permettant de conclure avec certitude. C’est le manque d’information qui peut faire échouer une requête avec une hypothèse et renvoyer un status négatif, pouvant être pris à tord pour une négation (corrigé par le précédent paragraphe). Mais d’après un paragraphe plus haut, une autre formulation du problème, est l’impossibilité d’explorer toutes les possibilités pendant la vérification. C’est ce qui est fait pendant une recherche de solutions n’impliquant pas d’hypothèse, et c’est ce qu’empêche les hypothèses, comme sont elles sont vérifiées sans vérifier de règle qu’elles désigneraient.

Cette reformulation, même si elle est plus simple et plus compréhensible qu’une absence d’information difficile à définir, n’est pourtant pas encore une solution.

Ça pourrait quand‑même faire s’interroger sur une possible piste : serait‑il possible, malgré qu’une hypothèse ⟦H⟧ soit considérée comme vérifiée à priori, de quand‑même tenter de vérifier les règles qu’elle désignerait ? Après la reformulation précédente, du problème, c’est une idée qui peut venir. Mais comment se déroulerait cette vérification ? Comment se passerait l’unification avec les têtes de règle si l’hypothèse n’y correspond pas directement. Par exemple, comment le terme de l’hypothèse ⟦(nat N)⟧ pourrait‑il être unifié avec les têtes de règle (nat z) et (nat (s N)) ? Existe‑t‑il une réponse cohérente à cette question ou sa formulation est‑elle le signe que cette idée est une impasse ? Ou devrait‑on pouvoir, à partir de l’hypothèse ⟦(nat N)⟧, obtenir deux autres hypothèses, ⟦(nat z)⟧ et ⟦(nat (s N))⟧ ? Mais par quelles justifications ? Et si l’hypothèse ⟦(nat N)⟧ n’a été prouvé que par le règle (nat z) et pas par la règle pour (nat (s N)) ? (avec des cas moins triviaux, ça peut devoir être envisagé) Cela signifie‑t‑il que la preuve d’une hypothèse doit couvrir toutes les règles avec lesquelles sa tête serait unifiable si elle était constituée de variables ordinaires ? Faut‑il distinguer les hypothèse prouvées par un seul cas, des hypothèse prouvées pour toutes les règles pouvant correspondre ? Ou est‑il finalement incorrecte de se satisfaire d’un cas pour prouver une hypothèse ? (dans ce cas, la preuve d’une hypothèse, serait plus que la seule preuve de la satisfiabilité d’un terme).

En oubliant pas que la variable spéciale N, est en fait une variable ordinaire, liée à une constante spéciale, mais en oubliant temporairement la constante spéciale.

Unifier ⟦(nat N)⟧ avec l’un ou l’autre de (nat z) ou (nat (s N_2)), peut au moins être imaginé, mais N aurait un caractère moins général. Unifier ⟦(nat N)⟧ avec (nat z), équivaudrait à supposer que N est seulement z. Ce serait une restriction de la généralité, mais une généralité quand‑même, réduite à la seule valeur possible, ce qui n’est pas un choix arbitraire parmi un ensemble de valeurs possibles.

Mais que pourrait être le résultat d’unifier ⟦(nat N)⟧ avec (nat (s N_2)) ? Avec une unification ordinaire, N ne représenterait plus une généralité, on aurait à faire une recherche de solution pour N_2, avec un ou des choix arbitraires parmi plusieurs possibles, le sens de N serait contredit. Imaginons, si une hypothèse ⟦(nat (s N_2))⟧ était produite, la variable serait liée à une généralité et serait donc toujours une généralité, d’une nouvelle forme (l’application d’un constructeur à une constante spéciale au lieu d’une constante spéciale), mais une généralité quand‑même. L’idée de N serait préservée, N serait toujours une généralité, mais une généralité plus restreinte. Cela poserait‑il un risque d’incohérence ?

En tous cas, on ne peut pas lier (s N_2) à une généralité N, ça n’a pas de sens pour le langage, on ne peut à la rigueur, que lier N à une généralité (s N_2) où N_2 serait définie comme une valeur quelconque vérifiant (nat (s N_2)), comme avec n’importe quelle hypothèse. Mais N_2 n’apparait pas que dans la tête de la règle, dans le corps aussi. Le corps de la règle est (nat N_2) : faudrait‑il automatiquement poser ⟦(nat N_2)⟧ en hypothèse aussi ? Au lieu de vérifier le corps d’une règle pour vérifier un terme, on partirait d’un terme en hypothèse pour arriver au corps d’une règle, en hypothèse.

Ce qui justifierait de poser ⟦(nat N_2)⟧ en hypothèse, automatiquement, serait qu’une éventuelle conclusion serait en réalité avec cette hypothèse. Mais N_2 est déjà définie par l’hypothèse ⟦(nat (s N_2))⟧. Peut‑il y avoir deux hypothèses définissant cette variable ? Le cas serait nouveau, mais il ne serait pas incohérent, ce serait sémantiquement cohérent. Faudrait‑il oublier l’hypothèse d’origine, ⟦(nat N)⟧ ? Elle a été restreinte, alors peut‑être doit‑elle être oubliée, pour ne conserver que les hypothèses qu’elle a généré.

Si l’idée de lier une variable liée à une constante spéciale, à un autre terme représentant une généralité, surprend : ça n’est pas plus surprenant que de lier une variable initialement liée à Any, à un autre terme. Ici, la constante spéciale serait comme un Any, mais propre à chaque variable. Il serait plus limité aussi. Si on peut lier une variable liée à Any à n’importe quel terme, on ne pourrait pas lier une variable liée à une constante spéciale, à n’importe quel terme représentant une généralité. Ceci, parce que la variable est définie comme une valeur quelconque vérifiant une certaine relation et alors la liaison ne devrait se faire que par l’unification avec une tête de règle vérifiant cette relation. Ce n’est aussi, pas une liaison avec n’importe quel terme vérifiant cette relation, mais aussi un terme lié à l’hypothèse d’origine. C’est à dire que si on a une hypothèse ⟦(nat N)⟧, que ce N se trouve par liaison dans un autre terme et qu’au court d’une unification, ce N est mise en face d’un (s X), la liaison ne se fera pas et l’unification échouera, parce qu’il n’y a pas de rapport entre ce (s X) et ce N, ceci, même si ce (s X) est éventuellement aussi une généralité vérifiant la même relation. Dans cette idée, le (s N_2) auquel est lié ce N, a été créé pour lui, c’est celui de la tête de la règle tout juste instanciée. Dit autrement, ce N ne serait lié qu’à une restriction de la généralité qu’il représente, plus encore, seulement de la généralité qu’il représente, lui.

Les deux idées caractérisant les variables spéciales, seraient préservées. Le résultat préserve bien l’idée d’une variable représentant une valeur quelconque vérifiant une certaine relation, mais ici, une restriction à une seule des règles vérifiant la relation. L’idée de valeur quelconque se satisfait‑elle ou pas d’une restriction ? La généralité inclue ce cas, mais ne correspond pas à un choix arbitraire parmi les cas. Difficile de répondre à cette question, mais elle s’avère liée à une autre qui sera l’objet d’un prochain message. La variable est toujours liée à une généralité. Certes, c’est un constructeur appliqué à une constante spéciale, plutôt qu’une constante spéciale tout‑court, mais le terme représente bien une généralité, autant qu’un terme posé en hypothèse représente aussi une généralité. Si les mots ne sont pas incorrectes, cette généralité à laquelle il est lié, est un élément de la partition représentant une généralité parente.

Petite pensée qui vient. Il faut envisager le cas piège noté précédemment, celui de variables logiquement liées par une relation, sans liaison de variable à variable.

L’exemple était :

(r b c)
(r c b).

L’hypothèse ⟦(r X Y)⟧ ne doit pas pouvoir permettre d’arriver à une paire X et Y tel qu’elles sont toutes les deux b ou toutes les deux c. Le risque ne se présente pas, parce qu’une hypothèse ⟦(r b c)⟧ ou ⟦(r c b)⟧ serait produite, pas les deux en même temps. Fin de cette petite vérification par sécurité.

Quel serait l’intérêt de tout ça ? Ce serait une interprétation supplémentaire pour les variables apparaissant dans des hypothèses, permettant de faire parler les hypothèses sur leurs causes possibles, posées comme des hypothèses aussi, c’est à dire comme des généralités. Ça permettrait de résoudre des problèmes tel que A ==> B, A ==> C, puis B posé en hypothèse, mais de quoi on ne peut pas conclure B ==> C, comme on a pas A. Cette implication n’est d’ailleurs valide que sous une condition, qui sera l’objet d’un prochain message. Cette condition se trouve aussi être la principale condition permettant de faire une preuve négative. Ce sera aussi une réponse à la question de savoir s’il est correcte ou pas, de restreindre une généralité à un élément de sa partition.

Ça demande encore réflexion et surtout à être mieux justifié. Pour l’instant, ça ne ressemble encore qu’à une idée.

La réponse est qu’il n’est raisonnable de l’attendre, que si A est la seule cause possible de B ou dit autrement, si B ne peut que signifier A. Si A est la seule signification de B, si de A on peut conclure C, alors de B on peut conclure C, puisque B étant posé, on peut dire A ; même si A n’est pas posé, il est au moins virtuellement là. Seulement, comme on fait des conclusions à partir d’applications de règles, on a quand‑même besoin de A pour déduire C de A, d’où l’idée, que si A n’est pas posé, mais que B l’est, de pouvoir poser A en le justifiant par le fait qu’on a B, ce qui encore une fois, n’est valide que si A est la seule signification de B.

Rappel : A ==> B peut se lire comme A est une cause de B ou A est une signification de B, B : A et A ==> B, représentent la même chose. S’il n’y a qu’une seule règle ou définition, B : A, alors A est la seule signification de B, ou encore, sa seule cause possible. Toujours pour rappeler un message d’il y a plusieurs semaines, la notion de cause est plus sujette à caution que celle de définition, même si les deux sont quelque part synonymes. On peut se dire que affirmer connaitre toutes les causes, équivaut à affirmer tout connaitre d’un phénomène, ce qui avec les choses pratiques, est souvent faux, mais typiquement vrai si ces choses pratiques, sont des choses formelles. C’est la raison pour laquelle le langage note des règles en les interprétant plus comme des définitions que comme des causes, ce qui signifie qu’il note ce qu’on connait. Quand les termes désignent des choses concrètes imparfaitement connues, cette différence vaut, mais on ne peut faire qu’avec ce qu’on sait ; quand les termes désignent des choses formelles, alors A est une signification de B ou A implique B, sont généralement synonymes (généralement, parce qu’on ne peut pas exclure des systèmes formels pour lesquels ce ne serait éventuellement pas le cas). En tous cas, dans ce langage, cause et signification sont synonymes ; il n’y a pas de moyen initialement prévu pour dire qu’on ne sait pas tout, cependant, ce serait possible juste un tout petit peu indirectement, mais ce sera pour plus tard.

Après ce rappel, retour à ce qui nous intéressait en premier lieu.

On a besoin de A pour dériver C, parce qu’on accepte que les conclusions par application de règle. Mais pourtant on poserait A étant donné B, arbitrairement ? Non, justement, on le dériverait d’une règle aussi, mais à rebours. On peut poser A étant donné B, parce qu’on a une règle B : A. Une règle est appliquée, mais « à rebours ».

Ça peut faire tiquer, parce qu’il peut y avoir plusieurs règles pour B. On y vient un peu après. Il faut retenir que rien ne sera posé arbitrairement, mais toujours justifié par les règles disponibles, que ce soit dans un sens ou dans l’autre.

Jusque là, étant donné B, on peut poser A pour la raison que A est sa seule signification, et de A, dériver C, et ainsi on peut dériver C à partir de B. À partir de A ==> C, et A ==> B, on aura fait le raisonnement B ==> A, puis A ==> C, pour arriver à B ==> C. Ne pas oublier : jusque là, on suppose que A est la seule signification ou cause possible de B.

Mais si B peut signifier plusieurs choses ? Dans ce cas, il faut un A qui représente toutes ces significations. Mais alors, ce A ne peut pas être le corps d’une règle. La solution à ce problème, demande d’accepter un saut vers un autre principe dont l’ébauche commence juste après et de lui accorder de la considération pour la raison qu’on va constater qu’il pourrait résoudre le problème.

Maintenant, on imagines que B peut signifier plusieurs choses ou avoir plusieurs causes possibles, disons deux, qu’on va nommer A1 et A2, disons qu’on a les deux règles B : A1 et B : A2. Que signifierait le raisonnement précédent, dans cette situation ? Disons qu’on a là aussi, l’intuition ou la certitude que de B on peut conclure C. Si on peut le faire directement à partir de l’hypothèse B, pas de problème (ce qui est le cas si on a par exemple une règle C : B), mais si on ne le peut pas et que pourtant la conviction est toujours autant présente ? Il peut y avoir deux cas : on peut en avoir l’intuition, mais cette intuition peut être bonne ou mauvaise, ou alors on peut en avoir la conviction parce qu’on l’a constaté par ailleurs. Comment pourrait‑on l’avoir constaté par ailleurs ? Eh bien par exemple si on sait (ou qu’on a l’intuition) qu’on peut prouver A1 ==> C et A2 ==> C. L’intuition, elle est mystérieuse, on ne sait pas comment elle sait, parfois elle se trompe, alors on pourra ou pas la vérifier. En tous cas, si on avait la conviction que de B on peut conclure C, par intuition, on sait qu’on peut prouver que l’intuition est bonne si on peut prouver A1 ==> C et A2 ==> C. Mais si on ne peut pas, disons, prouver A1 ==> C et qu’on a quand‑même toujours la conviction qu’on peut conclure C de B ? Dans ce cas, peut‑être que que A1 a lui‑aussi plusieurs significations ou causes possibles et qu’il faut prouver A11 ==> C et A12 ==> et A13 ==> C. Si ça ne marche pas, il faudrait essayer autre chose, et si ça ne marche toujours pas, peut‑être que l’intuition est mauvaise, et si on ne peut pas croire que l’intuition n’est pas bonne, ben ça ne changera rien pour la démonstration, ça restera non‑démontré, et on ne gardera que l’intuition, qu’on abandonnera ou pas, selon qu’on y tiendra beaucoup ou pas, et si on y tient, il faudra faire attention à ne pas trop se torturer avec, ce qui serait dommage si elle s’avère être mauvaise, tout autant qu’il peut être dommage de l’abandonner si elle s’avère bonne.

Ça a l’air censé, mais on a l’impression de s’éloigner de notre langage formel. Pour poser les choses plus brièvement et plus formellement, si on ne peut pas directement prouver C à partir de B, mais que B a une ou plusieurs significations possibles, et qu’on peut prouver C à partir de chacune de ces significations possibles, on peut conclure qu’on prouve C pour toutes les signification de B et donc qu’on prouve C pour B en général. Le principe est récursif : une signification de B peut devoir elle‑même être re‑posée comme ses significations possibles, si on ne peut pas directement prouver C à partir de cette signification.

Plus brièvement, si pour prouver B ==> C, on a besoin de A ==> B où A est l’ensemble des significations possibles de B, alors on peut remplacer B par l’ensemble de ses significations possibles et essayer de prouver C à partir de cet ensemble, tout cet ensemble. On le fait en prouvant C avec, posée en hypothèse tout à tour, chacune des significations ou causes possibles (toutes) ; tour à tour, pas en même temps.

Par exemple, si on ne peut pas vérifier ⟦H⟧ & T, on pourra peut‑être vérifier ⟦H1⟧ & T puis ⟦H2⟧ & T, si on a H : H1 et H : H2.

Quand on a voulu vérifier ⟦(int-z I)⟧ & (int I), on échoué, la généralité I n’était pas unifiable avec le terme (int N1 N2), de la tête de règle (int (int N1 N2)). Mais on a put prouver ⟦(nat N)⟧ & (int-z (int N N)) & (int (int N N)). Il se trouve que (nat N) est le corps de la règle dont la tête est (int-z (int N N)). D’une manière détournée, c’est le principe décrit dans ce message, qui a été appliqué. Juste que comme on a dut réécrire la requête en introduisant l’hypothèse ⟦(nat N)⟧, on a dut poser l’hypothèse d’origine comme un terme ordinaire, (int-z (int N N)), pour garder le relation entre l’hypothèse qu’on a introduit et l’hypothèse qu’on avait voulu à l’origine. C’est proche de ce que ferait l’unification décrite dans le message précédent. À partir de l’hypothèse ⟦(int-z I)⟧, aurait été produite l’hypothèse ⟦(nat N)⟧ avec I lié au terme (int N N), lui aussi une généralité. Le terme (int N N) avec l’hypothèse ⟦(nat N)⟧, aurait put vérifier la relation (int (int N1 N2)), dont le corps est (nat N1) & (nat N2). Ces deux derniers termes auraient été vérifiés par l’hypothèse ⟦(nat N)⟧, N1 et N2 étant tous deux liés à N.

D’autres questions peuvent se poser, mais avant ça, une réponse à chacune de deux questions posées précédemment.


On a vu que les preuves négatives d’un terme, nécessitent de couvrir tous les cas possibles, c’est à dire toutes les significations possibles de ce terme. Pour prouver non A, si A peut signifier A1 ou A2, il faut prouver non A1 et non A2. On ne doit pas en manquer un seul, car s’il existe ne serait‑ce qu’une solution à A, on a non non A et on ne doit alors surtout pas avoir non A. On a toujours pas de formulation complète du calcul de la négation, mais on sait qu’on a déjà un moyen de remplir un condition nécessaire à son calcul : la couverture de tous les cas.

Pour ce qui est de la validité de restreindre une généralité à un sous‑ensemble de ses valeurs possibles, même si ce sous‑ensemble est lui‑même représenté par une généralité, la réponse semblait ambivalente. D’un côté, la généralité représente bien entre autre ce sous‑ensemble, mais d’un autre côté, elle ne permet pas un choix arbitraire, sinon elle n’est plus la généralité posée. Ce qui a été introduit, résous ce problème. Si on restreint une généralité à un sous‑ensemble de ses valeurs possibles, c’est à moitié correcte, mais à moitié incorrecte aussi, c’est donc incorrecte tout‑court. Mais si on pose plusieurs restrictions et que cet ensemble de restrictions couvre toutes les valeurs possibles, alors on revient bien à la généralité qui avait été posée à l’origine, mais ce faisant, on a de l’information supplémentaire, sous forme d’une distinctions de cas. D’abord on perd la généralité, puis on la retrouve en la recomposant. C’est le fameux saut mentionné précédemment. Si on applique pas toutes les étapes, on ne préserve pas la généralité, mais si on applique toutes les étapes, on la retrouve. Démonter pour remonter après, ce n’est pas toujours rassurant, on peut ouvrir des yeux écarquillés sur ce qui est démonté en y voyant plus qu’une chose démontée, déliée. Mais si on sait que ce sera remonté, on peut se rassurer … à condition que ça finisse par être effectivement remonté.

Ce message soulève des questions. Et si B peut signifier A1 ou A2 ou A3 et qu’on ne peut conclure C qu’à partir de A1 et à partir de A2 et pas à partir de A3 ? Et si le terme posé en hypothèse, B, est unifiable avec la tête d’une règle mais contredit la règle ? On sait en effet, que l’unification d’un terme avec la tête d’une règle, ne garantit pas que la règle sera vérifiée, à moins que le corps de la règle ne soit vide. Et si l’hypothèse est une conjonction au lieu d’un unique terme ? Ces questions seront abordées plus tard.

Deux ajouts au précédent message.

Après avoir vérifié qu’on peut conclure C de B, comment pourrait‑on conserver cette démonstration ? Conclure C de B, B ==> C, peut déjà se noter C : B. Une bonne option serait peut‑être de le conserver comme une règle.

Si une hypothèse est posée comme un axiome, on ne peut pas lui connaitre de causes. Dans le message précédent, si B était un axiome, on ne pourrait pas le substituer à une collection de cas ; au moins pas pour le moment.

Après avoir généré les hypothèses représentant un élément de la partition d’une hypothèse d’origine, je crois que garder l’hypothèse d’origine disponible, ne serait pas incohérent et serait utile pour deux raisons.

Ce ne serait pas incohérent, parce que même dans une branche représentant une portion des cas possibles pour les variables de l’hypothèse, l’hypothèse d’origine ne peut que toujours être valable. Si à partir de ⟦(nat N)⟧ a été générée une hypothèse ⟦(nat (s N_2))⟧ avec N liée à (s N_2), l’hypothèse d’origine, ⟦(nat N)⟧, vaut toujours et si ce n’était pas le cas, alors ça signifierait que l’hypothèse ⟦(nat (s N_2))⟧ n’est pas un cas possible de pour ⟦(nat N)⟧.

En plus d’être cohérent, ce serait utile pour deux raisons.

La première est que ce qui n’a pas put être démontré avec ⟦(nat N)⟧ seule, mais pourrait être démontré avec ⟦(nat (s N_2))⟧ (et N liée à (s N_2)), pourrait éventuellement nécessiter les deux ou être plus facilement démontrable avec les deux. Je n’en vois pas d’exemple immédiatement, mais ce n’est pas incohérent et ça me semble pouvoir ouvrir des possibilités.

Mais surtout, il y a une seconde raison. Dans le cadre d’une vérification automatique, comme implicite depuis le début (mais ça ne va pas durer, c’est à craindre), se poserait la question de savoir jusqu’à quel niveau interne, développer une hypothèse pour la représenter par un ensemble de cas possible. Il faudra bien poser une limite, parce que rien qu’avec une hypothèse comme ⟦(nat N)⟧, les cas possibles forment un ensemble infini. Même en posant une limite à la profondeur du développement, se présenterait un problème combinatoire : il pourrait falloir par exemple développer tel terme d’une hypothèse dérivée jusqu’à tel niveau et développer tel autre terme jusqu’à tel autre niveau. En gardant disponible l’hypothèse générant un cas, et ceci récursivement, ce problème combinatoire disparaît, comme pour un niveau de développement donné, les hypothèses de tous les niveaux de développement jusqu’à ce niveau, sont disponibles.

Cela fait trois bonnes justifications pour garder les hypothèses d’origine, disponibles dans les branches qu’elles génèrent. Par disponible, il faut comprendre disponible pour vérifier un éventuel terme, pas disponible pour génération de cas possibles, qui n’est faite qu’à un endroit, celui où l’hypothèse est posée (en fait, plusieurs endroits, comme cet endroit dans une règle, peut avoir plusieurs instances, autant que la règle ou l’hypothèse apparaît).

Avant de donner des réponses aux questions laissées en suspend dans un précédent message, un bref retour sur le message qui résumait l’histoire de l’évolution de l’expressivité du langage jusqu’ici.

Cette histoire n’a pas mentionné l’ajout de la possibilité de faire choisir les étapes d’une vérification par un humain (ou même éventuellement non‑human, en fait). Cette étape s’explique ainsi : le langage de base a été défini sans prendre la méthode de résolution standard comme incontournable, en ne tenant pour nécessaire, que la conformité aux règles.

En parlant de méthode de résolution, un autre point omis, qui a été souvent sous‑entendu mais pas souligné dans le message en question, a été que le langage de base est pris pour un langage avec lequel on fait plus des vérifications que des recherches de solutions. S’il avait été vu comme un langage permettant surtout des recherches de solutions, l’idée de conserver les chaînes d’inférences, n’aurait pas été introduite, et peut‑être même pas non‑plus l’idée des variables représentant des généralités.

Le choix plus ou moins conscient de l’aborder comme permettant surtout des vérifications, aura eu assez de conséquences qu’il faille considérer que ce choix fait partie de la définition du langage.

La vérification et la recherche de solution, ne se sont pourtant pas trop distinguées, jusque maintenant, mais on va voir qu’une distinction entre les deux, est apparue sans se faire remarquer, dans les précédents messages.

Dans ce cas, on ne conclut pas C à partir de B ou pas à partir de B en général. C’est la réponse, elle est simple, mais soulève maintenant une nouvelle question, qui n’a pas de réponse satisfaisante pour le moment : que faire dans ce cas, si on veut pouvoir déduire C de A1 et A2, en général, si on ne peut pas le faire de à partir de B ?

Une solution pourrait être de reposer B autrement, par exemple

B-particulier : A1.
B-particulier : A2.
B : B-particulier.
B : A3.

Et on dériverait C de B-particulier en général. Notez que B-particulier et B, se distingueraient par le nom de la relation.

Ou aussi pourquoi pas :

B1 : A1.
B1 : A2.
B2 : A3. -- Distinction de A3 au même niveau que celle de A1 et A2.
B : B1.
B : B2. -- Au lieu de A3, pour mettre la distinction au même niveau.

Et on dériverait C de B1 en général. Ici encore, B1, B2 et B, se distingueraient nécessairement par le nom de le relation.

Mais on peut vouloir ne pas réécrire B a posteriori, si on a découvert tout autant à posteriori, la nécessité de dériver C d’une généralité.

Peut‑être qu’une autre idée pourrait se trouver dans une précédente, celle de pouvoir noter plusieurs corps de règle pour une seule tête. Pour rappel, on peut écrire ceci :

B : A1 ; A2 ; A3.

Qui est équivalent à :

B : A1.
B : A2.
B : A3.

Peut‑être une idée serait‑elle de permettre aussi, d’avoir plusieurs tête pour un seul corps de règle ? Ça pourrait ressembler à ceci :

D ; B : A1.
D ; B : A2.
B : A3.

Qui serait équivalent à :

B : A1.
B : A2.
B : A3.
D : A1.
D : A2.

Et on dériverait C à partir de D en général, sans avoir réécrit B, seulement en ayant ajouté des têtes de règles au cas qu’on veut distinguer et regrouper sous une généralité plus restreinte.

L’avantage de cette option, et qu’elle ne nécessiterait pas de réécrire B, mais au pris de règles supplémentaire, quoique implicites.

Si ça devrait se produire, les deux notations pourraient se retrouver combinées, sans que ça ne devienne un problème :

A ; B : C ; D.

Serait équivalent à :

A : C.
A : D.
B : C.
B : D.

Les points virgules ont été précédés d’un espace, pour les rendre plus visibles, mais ils s’écrivent plutôt sans espace avant et avec un espace après.

Dans les deux solutions, un nouveau nom de relation doit être introduit, sinon il n’y a pas de distinction. La nécessité de créer une relation pour distinguer un sous‑ensemble de cas, pourrait peut‑être avoir une autre solution, mais ce serait au pris d’une complication du langage, alors ce ne sera pas envisagé pour le moment.

La première solution a l’avantage de ne pas dupliquer les corps de règles. Elle a aussi l’avantage de diviser la généralité d’origine plutôt que d’en introduire une nouvelle. Mais elle a l’inconvénient de modifier les définitions, ce qui peut poser des problèmes si des preuves, solutions ou des chaînes d’inférences, ont été déjà produites à partir de ces règles, et que pour une raison ou une autre, il est problématique de les remettre en question.

La seconde solution a l’avantage de ne pas présenter le problème qu’a la première solution. Mais la nouvelle relation est dissociée de la première pour laquelle elle distingue des cas.

Aucune des deux solutions n’est assez satisfaisante. La seule bonne solution, serait de ne pas avoir à solutionner ce problème à posteriori, et que B ait été posé du premier coup comme dans la première solution. En ce sens, la première solution est la meilleure, mais elle ne répond encore pas à tout les cas.

Et si on veut pouvoir tenir A1 et A2 comme une généralité, tout autant qu’on veut tenir A2 et A3 comme une autre généralité ? Dans ce cas, seule la seconde solution fonctionne encore, aux prix de la dissociation, qui est l’inconvénient de la seconde solution.

Répondre à la question aura été simple, mais la question que soulève la réponse, n’a pas de réponse pour le moment. Il faudrait donc pouvoir exprimer n’importe quel sous ensemble d’un ensemble de règles, sans créer de nouvelles relations et sans modifier les corps de règle déjà posés. Ça semble nécessité l’introduction d’un nouveau concept dédié à ça. Mais comme dit précédemment, c’est trop tôt, d’autres choses appelant des réponses avec plus de priorité.

Une autre question apparaissait dans le paragraphe cité partiellement au début de ce message. Il lui sera donné une réponse plus tard.