Les logiques : notes en vrac

— Édit : l’idée de ce message est une mauvaise piste —

Le problème du message précédent, pourrait trouver une solution avec ces deux suppositions. La première : pour vérifier une condition, le terme doit correspondre exactement à l’hypothèse. La seconde : pour vérifier simultanément le terme et l’hypothèse, le terme peut être plus spécifique que l’hypothèse.

La première supposition est plutôt confirmée, elle est rappelée pour relever la différence avec la seconde, qui elle, nécessite une justification.

Même sans justification, la supposition semble assez propre. Une justification faible, pourrait être que d’une hypothèse, on dérive typiquement un terme plus spécifique que celui annoncé. Mais on le fait en faisant correspondre à l’hypothèse, un terme plus spécifique que l’hypothèse. Mais (une seconde fois), ce terme qu’on fait correspondre à l’hypothèse, pour produire le terme, est justement le même, qui est plus spécifique. Aussi, on peut prouver qu’une hypothèse est réalisable, avec un terme plus spécifique, comme déjà vu avec la preuve de la satisfiabilité des règles (*). Ce dernier argument est facile à accepter si on oublie pas que ici, l’hypothèse n’est pas une abstraction représentant tous les cas possibles d’un terme.

Ce qui reste difficile à accepter, c’est que pour la vérification d’une condition, il doit y avoir correspondance exacte, tandis que l’hypothèse peut être vérifiée par un terme plus spécifique. Ça pourrait présenter le risque de vérifier l’hypothèse avec un autre terme que celui qu’elle est sensée représenter. Pourtant, non, il est impossible que ce risque se produise, parce que l’hypothèse et le terme sont vérifiés simultanément, que alors l’hypothèse ne peut être vérifié que par ce terme qu’elle représente, pour peur qu’on pose comme condition, que ça ait lieu à l’instant de quitter l’instance de la règle.

Ça a l’air convaincant, mais mieux vaut ne pas se précipiter avant de se décider, surtout que la question est à manier avec précaution, pour le risque d’incohérence que présente une mauvaise solution. Même si le risque d’incohérence semble justement écarté, mieux vaut laisser décanter un peu.


(*) Il avait été proposé qu’on ne peut faire une hypothèse correspondant à une règle, que s’il est vérifié que la règle est satisfiable, ce qui prouve que l’hypothèse est réalisable et donc pertinente et pour faire cette preuve, une solution quelconque à la règle, est suffisante. Cette solution quelconque, est plus spécifique que le terme de l’hypothèse. La limitation, est qu’on a pas de couverture des cas, que l’hypothèse ne peut pas être ouverte, même si elle se décline en plusieurs cas possibles. Cette proposition a récemment été exclue de la sémantique du langage tout‑court, pour être considérée comme une possible extension à la condition que cette preuve ne soit pas obligatoire.

Complément sur la non‑importance de l’ordre des termes d’une conjonction.

La non‑importance de l’ordre des termes a été prise comme justification à une interprétation identique de deux règles récursives ne variant que par l’ordre des termes. La non‑importance de l’ordre des termes a déjà été justifiée, mais cette justification était incomplète, il lui manquait une précision.

La justification donnée jusque maintenant, était ainsi : si la conjonction T1 & T2 est vérifiée, les deux termes sont en accord dans le même contexte, ils sont individuellement d’accord avec le même contexte indépendamment de l’autre, et alors l’ordre des termes n’a pas d’importance.

Mais … ça parle des termes T1 et T2 quand ils sont résolus, ça ne parle pas des deux termes dans leur état littéral, et quand on dit que l’ordre des termes n’a pas d’importance, on le comprend spontanément comme ceci : devant le texte d’une règle, on lit la règle en supposant que l’ordre des termes n’a pas d’importance. Quand on lit une règle, ses termes sont sous leur forme littérale, pas sous la forme d’une solution. Ce qu’il faut justifier, c’est que l’ordre des termes dans une règle avant résolution, n’est pas pertinent pour la solution de la règle. Si les termes sont constants, leur solution et leur forme littérale peuvent être confondues ; disons alors que la justification donnée était suffisante au moins dans le cas de termes littéralement constants. Il faut maintenant le justifier dans le cas de termes littéraux non‑constants.

La solution d’un terme est soit le terme constant lui‑même, soit une liaison de ces variables. Intuitivement, pour que l’ordre des deux termes puisse être important, il faut qu’un des deux termes puisse décider des conditions que posera l’autre. Si T1 peut décider de la condition que T2 attendra, alors T1 & T2 n’est plus même chose que T2 & T1. Mais comment un terme peut‑il décider de la condition qu’un autre terme attendra de vérifier. On peut penser à la possibilité pour une variable, de représenter une interprétation. Un exemple immédiat serait quelque chose comme (r1 R2) & R2. Ici, le premier terme décide entièrement de la condition qui le suit et alors on peut difficilement croire que la conjonction est équivalente à R2 & (r1 R2). Pourtant si, mais sous réserve d’une précision qui nécessite d’en dire plus avant de comprendre ce qu’elle est.

On pourrait penser que si une variable ne peut pas poter sur une interprétation, alors cette possibilité disparaît. Pourtant si, même avec l’ancienne restriction initiale qu’une variable ne peut pas être liée à une interprétation, le cas peut se produire aussi. Si on (r1 A) & (r2 A B) et si on imagine que r2 a plusieurs clauses, on peut imaginer que la clause applicable dépend de A qui est choisie par le premier terme.

Mais alors l’ordre des termes est important et on l’a toujours considéré comme non‑important à tord ? Houlala, la grosse bourde … En fait non, mais la justification plus complète faisant que ce n’est pas une bourde, attend encore plus loin, elle nécessite encore d’exposer autre chose.

On reprend avec l’exemple (r1 A) & (r2 A B). L’exigence sur le contexte qu’à le second terme est décidée par le premier. On prend un instant les termes individuellement. Imaginons que quand il est seul, le (r2 A B) a plusieurs solutions, de même pour (r1 A). Que se passe‑t‑il si on énumère toutes les solutions de (r1 A) ? On énumère alors toutes les conditions qu’il peut décider que (r2 A B) aura. Il ne décide plus d’une exigence, mais de plusieurs possible. Oui, mais il décide toujours de la condition du second terme, non ? Oui, mais on peut aussi dire qu’il sélectionne toutes les conditions que le second peut poser, qui sont en accord avec les siennes. Que se passe‑t‑il maintenant si on inverse l’ordre des termes. On énumère toutes les solutions de (r2 A B) et on ne retient que celles qui sont en accord avec les conditions que (r1 A) peut poser. Cette fois, c’est comme si (r2 A B) décidait des conditions que (r1 A) va pouvoir poser. Pourtant il y a bien quelque chose qui reste et ne change pas : c’est l’ensemble des solutions faisant que les deux termes sont accord. Ce paragraphe reste valable même quand une variable peut porter sur une interprétation.

Ce qui a été omis à propos de la non‑pertinence de l’ordre des termes, est que cet ordre est en effet non‑pertinent, que sous la conditions où on considère toutes les solutions d’une conjonction, c’est à dire d’une règle.

Il y a une relation entre la multiplicité des solutions et la non‑pertinence de l’ordre des termes. Il faudrait, d’une certaine manière, voir l’ensemble des solutions à une conjonction, comme la solution à cette conjonction. Sous cette condition seulement, l’ordre des termes est en effet sans importance.

Ce cas est à distinguer de celui d’un terme partiellement déterminé, c’est à dire contenant au moins une variable indéterminée. On suppose qu’une variable laissée indéterminée par une résolution, est une constante indéterminée, même si ce pas le cas pour l’interprétation externe.

À propos du principe des deux couches, avec des règles dans une couche #1 et des faits dans une couche #2, on peut dire que la couche #2 est un modèle de la couche #1 (ou sensée l’être), l’idée de modèle étant à comprendre dans le même sens que la preuve de la satisfiabilité d’une règle en donnant un exemple de solution la vérifiant, l’exemple de solution étant un modèle de la règle. Mais ici, c’est un modèle avec une capacité supplémentaire (et une seconde plus loin) : il peut être partiellement indéterminé dans sa forme littérale pour être déterminé par les règles, simultanément à la vérification qu’il est un modèle des règles, ce qui a été appelé l’attribution du sens. Cette détermination peut avoir plusieurs solutions, ce qui pose un problème qui est laissé à plus bien tard. Ce modèle peut être littéralement constant et dans ce cas il n’est pas déterminé avec sa vérification, comme il l’est déjà, déterminé ; dans ce cas au moins, il ne peut y avoir de problème de solutions multiples. Une autre capacité supplémentaire, est que le modèle est lui‑même posé avec des formules pouvant être interprétées comme des règles, même si ce n’est pas obligatoire (on peut considérer que malgré la syntaxe, qu’il n’y a pas de règles dans la couche #2, quand il n’y a aucune application de ses règles).

Du coup, parler de modèle à deux couches n’est pas une bonne idée, comme le mot « modèle » est alors utilisé avec deux sens différents, ce qui peut embrouiller. Peut‑être est‑il préférable de parler de construction ou d’organisation à deux couches (ou même à plus de deux couches, au moins en théorie, les intérêts pratiques d’en avoir plus de deux restant à voir).

Plus clairement, un terme qui n’est pas une interprétation, n’a qu’une interprétation constante, ces variables libres, s’il y en a, étant des constantes indéterminées. Même si un terme imbriqué n’a pas de vu sur le terme l’englobant, de son point de vu, il est certain que le terme englobant existe, sinon il ne serait pas un terme imbriqué et il est certain que ce terme englobant n’a qu’une interprétation constante, même si elle est inconnue.

Quand une interprétation est imbriquée dans une autre interprétation, c’est différent, elle ne sait même pas si l’interprétation qui se réfère à elle, est au moins satisfiable. Ceci est en ne comptant pas les termes hypothétiques qui sont une question encore en suspend, ces termes étant une vue sur une interprétation englobante.

Mais cette condition n’est pas définissable sans définir les solutions individuelles, les solutions individuelles ne peuvent que être considérées. Disons qu’à un premier niveau, il y a une énumération de solutions individuelles et qu’à un second niveau, il y a un ensemble de telles solutions. Ceci étant posé, il possible de dire ensuite qu’un élément d’un ensemble de solutions peut lui aussi être un ensemble de solutions.

L’ensemble de solutions ne peut que être le même que celui qui serait produit par une double négation. Pour la double négation, l’ordre des termes est donc sans aucune importance, sous réserves que l’ensemble de solutions soit produit. De même pour la simple négation qui peut se définir à partir de la double négation, si on le souhaite. L’ordre des termes reste cependant sans importance pour une solution individuelle, pour la raison déjà donnée (l’ordre des termes n’est pas important pour le constat de l’accord avec le contexte). L’ordre des termes n’est important que pour l’ordre dans lequel les solutions individuelles sont produites, sous réserve qu’elles soient toutes produites. Cette conclusion avait déjà été faite, mais sa nouvelle version est plus générale et plus précise.

Faut‑il considérer que l’ordre dans lequel les solutions individuelles sont produites, peut avoir une interprétation ? Ça peut être pertinent, comme il est possible de par exemple poser la règle des entiers naturels représentés comme des polynômes, de manière à ce qu’ils soient énumérés par la règle comme on les énumérait naturellement. L’ordre de ces solutions peut avoir une interprétation externe, même s’il n’a pas d’interprétation interne. Peut‑être alors faut‑il envisager que l’interprétation des règles doit se faire sans modifier l’ordre des termes, même si l’ordre des termes n’est pas important pour un ensemble de solutions, et de prévoir comme extension possible, un mode d’interprétation pour lequel l’ordre des solutions n’est pas pertinent, quand c’est l’intention. C’est tentant, mais sous réserve que poser que les règles sont interprétées en respectant l’ordre de leurs termes, ne pose pas un quelconque problème et il a été vu un cas de récursion qui se résous difficilement autrement. Sous réserve, il est envisagé que la sémantique pose que l’ordre des termes est important, pour respecter l’ordre dans lequel les solutions individuelles sont énumérées, cet ordre pouvant avoir une interprétation externe.

En résumé, une distinction est faite entre un ensemble de solutions et une énumération de solutions. Cette distinction a deux justifications. L’une est le respect d’une possible interprétation externe, l’autre est que sans l’énumération, l’ensemble être peut‑être plus difficilement définissable.

C’est trop bancal. L’idée de vérifier l’hypothèse d’un terme avec un terme plus spécifique est le point suspect et sans solution. Une autre piste est tentée, à partir du sens des termes, en abandonnant la piste de poser des hypothèses.

Une première idée venue avant, sans l’avoir dite, était de noter que A & A est réductible à A et de voir dans ce type de récursion, un cas similaire. La liste des buts à résoudre est bien une conjonction simplifiable, mais le problème est qu’avec ce type de récursion, la conjonction n’est jamais sous une forme simplifiable. Dans « A : A. », à partir d’une « conjonction » A, le A est substitué à A qui est substitué à A, etc, indéfiniment, la liste des buts ne contient jamais rien d’autre que ce seul A, et alors jamais de conjonction réductible.

Une autre idée est dans une reformulation de l’instanciation des règles. Étant donnée la règle « (eq A A). », il avait été expliqué qu’on peut poser (eq b b) & (eq c c) et le vérifier sans y voir une contradiction, parce que les A ne sont pas les mêmes dans les deux termes, qu’on a une instance (eq A_1 A_1) et une instance (eq A_2 A_2) et qu’il en serait de même avec la conjonction (eq b b) & (eq b b). Voici justement : dans ce dernier cas, les deux instances seraient les mêmes, parce que les deux termes ont la même signification et que alors une seconde instance n’est pas justifiée pour la raison que A & A est réductible à A. Mais on a vu plus haut que ça n’est jamais applicable, comme la liste des buts n’est jamais sous une forme réductible. Ce n’est pas qu’un détail d’une mise en œuvre, une description concrète de la sémantique ne peut elle‑même pas se passer de cette liste des buts à résoudre. Mais il y a un détail : quand il est dit qu’on ne ré‑instancie pas (eq b b) parce qu’il existe déjà, ça implique qu’on sait que ce terme existe déjà. Ça change quelque chose pour la récursion. Étant donné « A : A. » et la « conjonction » A, on instancie A, puis dans la liste des buts, on s’apprête à lui substituer A, mais une instance de A non‑achevée existe déjà, son sens est donc déjà posé, inutile de le dupliquer, et alors on substitue la condition A par rien. On retrouve bien que « (r A) : (r A). » est équivalente à « (r A). ». C’est comme si on réduisait A & A, ou le premier A est celui en cours et le second sa condition, comme si on le réduisait au A en cours.

Dans une mise en œuvre, on ne peut que avoir une forme de pile des opérations en cours, mais ce qui est dit ne signifie pas qu’on a une pile, même si techniquement c’est la même chose, ce qui est dit qu’on se réfère explicitement au fait qu’on sait qu’on a un A en cours.

Mais un A en cours et un A à résoudre plus loin, ce n’est pas la même chose, qu’est‑ce qui permet de les traiter de la même manière ? Ce qui permet de les traiter de la même manière, c’est qu’ils signifient la même chose, autant que (eq b b) signifient la même chose que (eq b b), parce que les deux termes sont identiques, c’est à dire que la justification, c’est le sens des termes, ce qui fait une justification plus solide que celles données avec la mauvaise piste des hypothèse. Dire deux fois la même chose, pose la même signification que le dire une seule fois. Parler de terme hypothétique pourrait toujours être approprié, comme on à un A dont la vérification est en cours, mais il n’est plus question de poser des hypothèses et de les confirmer en confirmant un terme dans le même temps.

Une question à traiter avec prudence maintenant est, ce que signifie pour deux termes, signifier la même chose. Quand les deux termes sont littéralement constants, c’est trivial, mais quand les deux termes contiennent des variables ? Il faut peut‑être se méfier de l’idée que le développement des termes est suffisant, surtout si après développement, ils contiennent encore des variables libres, en oubliant pas qu’il s’agit de désigner deux termes comme identiques, même avant l’achèvement de leur résolution.

Par exemple, étant donnée « (r A) : (eq A b) & (r A). », quand le terme (r A) est instancié (ou plutôt la règle est instanciée), le terme est désigné par (r indéterminé) où le indéterminé a sa propre identité, mais après la vérification de la première condition, le sens du terme en question, est‑il désigné par (r b) ou toujours par le même (r indéterminé) ? Ou est‑il avant et après, toujours désigné par (r A) quelque soit la liaison de A ? C’est à cette question qu’il faut répondre avec prudence.

Suite.

Il a été question de terme littéralement, il faut distinguer aussi, textuellement et littéralement. Quand une variable du même nom apparaît dans deux conjonctions différentes, c’est textuellement la même variable, mais ce sont littéralement deux variables différentes, c’est une conséquence de la syntaxe, pas de la sémantique, la sémantique ne connait que ce qui est littéralement.

Qu’est‑ce qui désigne le sens de (r A) ? Si A est inconnue ou indéterminée, il est désigné par (r A), si un deuxième terme (r A) apparaît ailleurs, on sait qu’il a le même sens, quelque soit la liaison de A, parce que c’est littéralement le même terme. Mais si A est liée à b, qu’on le sait ou s’en préoccupe ? Alors le sens de (r A) est (r b), désigné par (r b) mais aussi par (r A). On peut faire de même avec des variables liées entre elles, si A est liée à B qui est liée à b, alors le sens de (r A) et de (r B) et de (r b) est (r b), désigné par (r A) ou (r B) ou (r b). C’est tellement simple que ça semble trop beau pour être vrai.

Y‑a‑t‑il un piège quelque part ? Il semble que non. On se propose de simplifier A & B en A ou en B si les deux sont vérifiés et A & B en A si A est en cours de vérification et B à vérifier plus tard, si on a la certitude que A et B ont le même sens et pour avoir la certitude que leurs sens sont les mêmes, on a pas besoin de connaître leurs solutions (dans le cas d’une résolution) et alors il n’y a pas de risque d’être incorrecte à appliquer ce principe même sur des termes en cours de résolution. On ne le fait pas si on en a pas la certitude. Les remarques du paragraphe précédent sont suffisantes pour avoir cette certitude. Ça reste une certitude même si les termes évoluent, comme à travers les étapes d’une vérification ou d’une résolution, une constante ne change jamais et les liaisons des variables ne peuvent jamais être défaites.

Il semble que pour éviter ce type récursion infinie avec la garantie que ce soit sémantiquement correcte, il suffit de conserver les termes en cours de résolution sans avoir besoin d’en faire une copie développée, de les comparer constante pour constante, identité de variable pour identité de variable, liaison de variable pour liaison de variable, et récursivement via terme lié à une variable pour terme lié à une variable. Il n’y pas de faux positif possible, seulement d’éventuels « faux négatif » qui auraient put être des cas positifs pour un certain ordre de vérification des termes. Implicitement, deux termes sont supposés comparés dans un même contexte.

Dans le cas de « (r A) : (eq A b) & (r A). », il n’y a aucune seconde entrée dans la règle comme c’était le cas précédemment avec la mauvaise piste des hypothèses et dans le cas de « (r A) : (r A) & (eq A b). » il n’y a plus de situation douteuse comme avec la même mauvaise piste des hypothèses, le cas est exactement le même que dans la première version de la règle, ce qui est conforme à la non‑pertinence de l’ordre des termes. Si par malheur c’était incorrecte, ce serait avec un air irréprochable.

Trop simple pour être correcte ? Mais qu’est‑ce qui pourrait avoir été manqué ?

Sauf cas sémantiquement incorrecte imaginé ultérieurement, ce sont les justifications de ce message et du précédent, qui fonderont l’élimination des entrées dans des récursions infinies du type de celle de l’exemple plus haut. Ces récursions sont parfois nécessaires, comme dans le cas de la paire alloc / free de certains précédents messages, les exemples utilisés récemment ne sont que des exemples sans prétention d’utilité pratique.


Quelques messages précédents sont marqués comme mauvaise piste.

Une conclusion justifiée par le message précédent, utile à noter séparément.

On peut toujours avoir la certitude que deux termes ont le même sens, mais à moins qu’ils ne diffèrent par des constantes ou que toutes vérifications ou résolutions ne soient achevées, on ne peut jamais avoir la certitude que deux termes n’ont pas le même sens.


Note en marge : il faudrait un mot pour dire « vérification ou résolution ».

Ce message est sujets à remises en questions, peut‑être en partie ou peut‑être entièrement.

Retour sur les ensembles.

Aucun nom alternatifs n’ont été décidés pour domain, range, codomain, corange. Cette question est remise à plus tard et n’est pas abordée maintenant.

Étant données les règles ci‑dessous, il avait été prévu de s’assurer qu’on peut prouver que les les arguments de eq et neq ont le même domaine que const :



Comme précisé précédemment, ces règles ne prétendent pas être des exemples de choses à écrire, elles sont seulement des exemples intéressants à étudier. Dans un cas réel, une formulation plus simple aurait été préférée à moins de vouloir explicitement souligner des choses et d’autres.

L’idée initiale de vérifier que le premier argument de la tête de eq est toujours unifiable avec un terme vérifiant const, est abandonnée et reformulée, mais une autre question assez proche reviendra un jour.

Il y a deux raisons à cet abandon. Faire une preuve sur une tête de règle en la tenant pour un terme isolé de ses conditions, trouve difficilement du sens ou je n’en ai pas trouvé. La tête de la règle a une forme explicite autant qu’une forme implicite, comme expliqué avec l’idée reléguée à un détail interne, de définir une normalisation des têtes de règle, ce qui rappel qu’elle peut difficilement garder son éventuel sens quand elle est isolée de ses conditions.

L’ancienne idée de vérifier la couverture de l’unification à la tête de la règle pour toutes ses clauses, est remplacée par la vérification de la couverture de ce qui est vérifié par la règle. En d’autres mots, au lieu de s’assurer que tout terme vérifiant const est unifiable au premier argument de eq, il est vérifié que le premier argument de tout terme vérifiant eq, vérifie toujours const.

Il s’agit de dire que ceci est toujours vrai : (eq A B) => (const A) et de même pour le second argument. On ne peut pas écrire cette formule dans le présent langage, mais « A : B. » peut se comprendre comme B => A et on peut écrire « (const A) : (eq A B). » À la lecture, ça fait sens, mais ce serait une définition redondante de (const A) et non‑seulement on ne veut pas répéter une définition existante au risque de la répéter inexactement, en plus, au lieu d’une définition, on veut une vérification que que c’est toujours vrai, d’après les définitions posées. On peut l’écrire « (const A) : {(eq A B)}. » qui n’est plus une définition même si c’est toujours une règle. La règle se lit « si on a (eq A B) alors on a (const A). », ou encore, étant donné (const C) et (eq A B), l’ensemble des A est inclus dans l’ensemble des C.

En reprenant la même syntaxe qu’avec le brouillon de langage de démonstrations dans Re: Les logiques : notes en vrac, la démonstration que le premier argument des termes eq et neq, supposés vérifiés, est toujours un const, pourrait être ainsi :



Une notation moins verbeuse est possible, mais celle‑ci rend presque tout explicite ce qui permet de la comprendre plus facilement.

La seule nouveauté par rapport à fin‑Novembre 2020, est que la démonstration est récursive, elle se réfère à la règle qu’elle prouve, étiquetée §r. Ça semble sensé, mais il faudra justifier de se le permettre.

Si on veut prouver « (const A) : {eq A B). » et « (const B) : {(eq A B)}. », on doit répéter deux fois une preuve quasiment identique. Il n’y a pas raison de se précipiter à y remédier, si les preuves sont identiques, c’est parce que les deux arguments sont de la même nature, ce qui est un cas particulier.

On pourrait préférer pouvoir dire « (const A) & (const B) : {(eq A B)} », mais ce n’est pas possible directement. Ça l’est quand‑même indirectement. Il serait possible de poser cette règle qui serait d’une utilité assez générale :

(conj A B) : A & B.

Puis d’avoir une démonstration de « (conj (const A) (const B)) : {(eq A B)} ». L’intérêt pour les variables, de pouvoir capturer une interprétation, vient d’avoir son premier exemple d’utilité pratique (cette utilité ne faisait pas vraiment de doute, c’est seulement que le premier exemple a tardé à avoir une occasion d’être introduit).

Quand on prouve « (const A) : {(eq A B)}. », on prouve seulement que le domaine du premier argument de eq est inclus dans celui de l’argument de const, on ne prouve pas qu’il couvre tout ce domaine. Pour cela, il faut prouver que réciproquement, le domaine de l’argument de const est inclus dans celui du premier argument de eq, en d’autres mots, qu’on peut toujours vérifier un terme (eq A B) pour tout A vérifiant (const A), c’est à dire (const A) => (eq A B), B étant libre, c’est à dire « (eq A B) : {(const A)}. ». La nouveauté, est qu’une variable de la conclusion, n’est pas liée par l’hypothèse et est donc libre à priori. Note : la réciprocité de l’inclusion, signifie finalement que les deux domaines sont les égaux, les mêmes.

La démonstration nécessite une règle préalable qui est démontrée d’abord et ensuite celle souhaitée. Cette démonstration préalable, est récursive, mais pas la seconde, qui n’en a plus besoin.


La nouveauté est le LET. La conclusion a une variable B qui n’est pas liée par l’hypothèse, il faut donc lui trouver une solution, ce que fait LET, qui lui en donne une. Dans le cas présent, la solution est unique.

La démonstration correspondante, pour neq :



Ici on a une surprise, une nouveauté et un problème. La surprise est qu’on a pas besoin de démonstration récursive, alors que la définition de neq, l’est. Cette surprise est lié au problème décrit plus loin. La nouveauté est qu’on a un LET qui pose un C en le laissant indéterminé. Même si ce C indéterminé est utilisé par B, il reste indéterminé et B ne l’est alors que partiellement. Le problème est dans la preuve dans le cas §const-s. La variable B reçoit comme solution, (), ce qui est une solution correcte, mais B pourrait avoir d’autres solutions, n’importe quelle solution différente de A, d’après §neq-s, qui n’est même pas mentionné dans la démonstration. La règle ne précise pas qu’elle produit une solution plus restrictive que nécessaire, et c’est un problème, surtout que c’est une solution arbitraire et que l’arbitraire ne devrait pas avoir sa place dans le langage, du moins pas en dehors de la syntaxe. Et en plus, cette arbitraire est caché.

Ici, comme précédemment, les mêmes preuves peuvent être faites pour le second argument, en plus de pour le premier. Quand on a prouvé que le domaine du premier argument de eq couvre celui de const et que celui de const couvre celui du premier argument de eq, on a prouvé que les deux domaines sont les mêmes.

On peut vérifier huit règles. Les quatre premières :

(const A) : {(eq A B)}.
(const B) : {(eq A B)}.
(const A) : {(neq A B)}.
(const B) : {(neq A B)}.

La première règle signifie que le domaine de const inclus celui du premier argument de eq, et l’équivalent pour les trois autres règles.

On peut abréger, si on préfère :

(conj (const A) (const B)) : {(eq A B)}.
(conj (const A) (const B)) : {(neq A B)}.

Les quatre règles suivantes :

(eq A B) : {(const A)}.
(eq A B) : {(const B)}.
(neq A B) : {(const A)}.
(neq A B) : {(const B)}.

La première règle signifie que le domaine du premier argument de eq inclus celui du domaine de const. Comme on peut prouver la réciproque, on peut prouver que le domaine du premier argument de eq et le domaine de const, sont les mêmes.

On peut abréger là aussi si on préfère, toujours moyennant des ajouts ou réécritures ailleurs :

(conj (eq A B) (eq B A)) : {(const A)}.
(conj (neq A B) (neq B A)) : {(const A)}.

Les points essentiels du précédent message :

Des preuves récursives ont été utilisées, mais il reste à justifier de se le permettre.

La vérification de la couverture du domaines des arguments des deux règles à deux arguments, nécessite huit règles démonstrations, ce qui peut sembler encombrant, même s’il est possible d‘interfacer ces huit règles, pour arriver à diviser le nombre par deux, n’en laissant plus que quatre.

Quand une variable apparaissant dans une conclusion n’est pas posée dans l’hypothèse, il peut se poser un problème de solution arbitraire. Poser une solution ne serait pas un problème sous certaines conditions. La solution devrait être unique même si elle est partiellement déterminée. Il devrait être prouvé qu’elle est unique et qu’elle est donnée sous sa forme la plus générale. Le cas où la solution est une variable indéterminée et non‑liée, ne pose pas de problème. Ou alors, il faudrait prouver qu’on donne toutes les solutions possibles, de quelques manières que ce soit. Ou alors le concept introduit avec le mot clé LET, doit être abandonné et il faut préférer que les variables de la conclusion apparaissent toutes dans les hypothèses, même s’ils faut pour cela ajouter des hypothèses.