Les logiques : notes en vrac

Sans résumer tout ce qui a été dit récemment, trois points importants à retenir des précédents messages :

Les constats ont été introduits pour exposer des faits sémantiques qui ne peuvent pas être dit avec des règles. Ces constats portaient initialement sur des termes, seulement.

Les constats sur les contextes ont été introduits, pour répondre à la nécessité de dire qu’on constate qu’une chose n’est pas possible dans un contexte, ce qui implique qu’on a besoin de pouvoir le faire en l’absence d’un terme résolu qui pourrait être le sujet du constat.

Même si par abus de langage, il est souvent fait mention de résolution d’un terme, il faut formellement comprendre qu’il s’agit de la résolution d’un contexte en vu d’y rendre un terme possible. La distinction est importante, comme la résolution d’un contexte peut avoir d’autres finalités, et que pour ces autres finalités, voir la résolution comme sur un terme, peut empêcher de facilement comprendre le sens de la résolution en question, qui se comprend en général mieux comme une résolution d’un contexte. Un terme est toujours impliqué quand‑même, comme le seul accès au contexte est à travers un terme ou une conjonction de termes.

Ça n’aurait pas du être dit. Les constats se font sans résolution. Le passage disant « alors not (A true) résous aussi le contexte tel que A true n’y soit pas vérifiable », doit être oublié, il est trompeur.

Dans une démonstration, les dérivations proviennent des règles. Les constats n’étant pas définis par des règles, dans une démonstration, ils ne peuvent être vérifiés que par résolution. Le constat interprète le résultat d’une résolution pour le besoin d’une démonstration.

Par exemple si une requête n’aboutit à rien, on ne constate aucun résultat. On peut, soi‑même, interpréter cette absence de résultat, par exemple constater que c’est conforme à ce qu’on attendait, ou au contraire, non–conforme et se poser des questions sur la cause de cette surprise. Dans une démonstration, il n’y a pas quelqu’un pour interpréter le résultat, il faut dire quel résultat est attendu, ce qui signifie dans le même temps, l’interprétation qui en est faite dans la démonstration.

Ce n’est qu’une idée encore vague, mais ça semble être une piste crédible.

Si vraiment des choses ne peuvent être démontrées que par constat, que cela signifie‑t‑il ? Est‑ce une vérification plus faible qu’avec une démonstration par dérivation ? Peut‑être est‑ce simplement incontournable. Si par exemple il n’existe qu’une seule règle pouvant vérifier un terme, comment cela pourrait‑il être prouvé par dérivation ? Il semble que la vérification par le constat soit la seule option possible. S’il n’existe qu’une seule règle, c’est parce qu’une seule a été écrite et si une seule a été écrite, ça n’est pas une conséquence d’autres règles (à moins que les règles ne soient des interprétations de termes produits par d’autres règles), s’il y a une raison, c’est une raison qui échappe à celle du langage, la raison de qui a écrit les règles (à moins que sa pensée à ce moment là ne puisse être représentée par d’hypothétiques règles, mais encore faut‑il qu’elles aient elles aussi été écrites). Comment alors espérer pouvoir vérifier cet exemple de fait, autrement que par un constat ?

Quand une vérification par dérivation est possible, elle est quand‑même préférable, parce qu’elle est au moins une explication d’après les règles, ce qui fait plus sens qu’un constat. Un constat peu aussi ne jamais se terminer, s’il est une vérification par résolution, c’est à dire par exploration, et dans ce cas, une preuve par dérivation a un avantage technique ou pratique, comme chaque étape est garantie se terminer. Même si ça fait deux raisons de préférer la dérivation au constat, reste qu’il semble inévitable que le constat soit parfois la seule possibilité.

En résumé, il existe deux type d’étapes dans une preuve : dérivation et constatation.

Étant une nouveauté, ça pourrait être qualifié de sous réserve, mais ça semble assez certain.

Pour raison de lisibilité, le constat true explicitement écrit, pourrait être rendu nécessaire pour ce qui est vérifié par constat dans une démonstration. Si A est vérifié par dérivation, la même notation qu’auparavant, de la forme « A |- justification. » resterait utilisée. Dans le cas d’une vérification par constat, au lieu d’écrire « A. » tout‑court, il serait nécessaire d’écrire « A true. », ce qui distinguerait bien les constatations des dérivations. La forme « A. » tout‑court, ne serait possible que dans le bilan de ce qui est vérifié après une couverture de cas.

Un problème qui se pose, est comment poursuivre avec une dérivation à partir d’un constat autre que A true ? Avec A true, le A peut prendre la place du terme d’une hypothèse pour appliquer une règle sous hypothèse. %ais à partir d’un constat comme A false par exemple, comment poursuivre avec une dérivation ? Les termes négatifs dans les hypothèses n’ont jamais été envisagés, et les autres constats, encore moins. Mais ça ne résoudrait encore par le problème, ça ne ferait que le repousser. En imaginant une règle comme « A : {B false} », à quoi pourrait ressembler une démonstration d’une règle sous une telle hypothèse ?

Les relations entre not et false restent à définir en détails, mais il semble assez certain que not A ne serait qu’une manière parmi d’autres, de vérifier A false. Par exemple si la constante c ne correspond à aucune tête de règle, c false est constaté. Seulement si A a éventuellement des solutions dans un contexte, il est nécessaire d’avoir un contexte dérivé via not A, pour pouvoir y vérifier A false. Étant donné « R : A & B. », si A et B sont mutuellement exclusifs, R false devrait pouvoir se démontrer, autant que être vérifié dans un contexte dérivé par not R, un contexte dérivé qui serait alors le même que celui à son origine.

Des choses à noter.

Comme déjà vu il y a longtemps, ne pas parvenir à vérifier une chose, n’est pas équivalent à prouver que cette chose n’existe pas. Mais c’est seulement dans le cas général, pas dans tous les cas. Avec une hypothèse comme {(nat N)}, une tentative d’unification à (nat (s N)) ne peut que échouer, se concluant par un false (ou le constat devrait‑il être autre chose que false ?), sans que ce ne soit une preuve que ce N n’a pas de prédécesseur. Mais si N est une variable ordinaire, l’échec de l’unification au même terme, est bien une preuve que ce N n’a pas de prédécesseur. L’absence de preuve n’est pas la preuve de l’absence, mais parfois, si. Le cas où cette conclusion est valable, c’est celui où une exploration exhaustive est faite, sachant qu’elle peut ne rien conclure de ne jamais revenir de son exploration.

Comme déjà vu, les variables des hypothèses étant gelées, il ne peut pas y avoir de résolution sur ces variables. Ça une conséquence implicite sur les démonstrations sous hypothèse, qui n’avait pas été soulignée : une démonstration sous hypothèse, se fait sans modifier le contexte, le contexte n’est que celui posé par l’hypothèse et ne change pas. Les branches des cas des hypothèses pourraient éventuellement être vu comme dérivant un nouveau contexte, mais il s’agit toujours d’un contexte exclusivement posé par l’hypothèse d’origine. Cette non‑modification du contexte doit être respectée, il faut veilleur à ce qu’une vérification par résolution dans une démonstration, abandonne le contexte de sa résolution pour ne conserver que son constat. Ainsi, à partir de l’hypothèse {(nat N)}, on peut vérifier par résolution que N a un successeur, mais il faut abandonner la variable intermédiaire produite par l’instantiation de la règle correspondante, pour ne retenir que le constat true

Avec une vérification par résolution dans une démonstration, vient le risque d’une résolution qui ne se termine jamais. C’est moins acceptable dans une démonstration que dans une requête. Mais il avait été pressentie qu’une vérification faite sur un terme constant, se termine plus sûrement, comme elle ne créé rien, ne fait que décomposer le terme d’origine de la requête. Ce n’est pas tout à fait vrai, mais pas loin.

Il existait pourtant au moins une possibilité de récursion infinie même avec une vérification sur un terme constant, mais ce type de récursion infinie a récemment reçu une solution. Est‑il possible de se limiter à ce type de vérification, c’est à dire sur des termes constants seulement, dans des démonstration, sans s’empêcher de faire certaines preuves ? En tous cas, on peut noter que les variables des hypothèses sont comme des termes constants et que alors il faudrait peut‑être plutôt se demander si dans une démonstration, une vérification sur autre chose que des termes constants, est pertinent.

Une vérification sur un terme constant peut se terminer en résolution malgré‑tout, si des règles contiennent des variables non‑liées par la tête de la règle, mais il est possible de définir une interprétation tenant ces variables pour non‑résolubles, et concluant la vérification par un constat indéterminé. Ce serait probablement trop limité en général, mais cette idée qui avait été envisagée pour une version de base du langage sans résolution (une idée qui sera probablement abandonnée sous cette forme), pourrait avoir un intérêt pour la vérification par constat dans les démonstrations, quand s’y restreindre est suffisant.

Sans que ce ne soit encore certain, il faut peut‑être envisager des pseudos axiomes. Pseudo dans le sens où ce serait des règles posées comme des axiomes, non‑prouvées par d’autres règles, mais dont il serait prouvé qu’une mise en œuvre du langage les vérifie. Ce qui le fait suspecter, c’est que pour poursuivre par des dérivation à partir de constat, il faut bien des règles qui le permettent. Mais ces règles de dérivation à partir de constats, ne peuvent pas être prouvées à partir d’autres règles, comme les constats ne peuvent pas être défini par des règles. Pourtant, ces règles de dérivation devrait pouvoir être prouvée pour une mise en œuvre du langage. Ces règles auraient donc l’apparence d’axiomes, sans en être vraiment, puisqu’elles seraient démontrées.

La relation entre constat et résolution peut parfois sembler confuse, comme les deux mots apparaissent souvent ensemble tout en étant dit indépendant. Pour clarifier, il faut distinguer deux choses : un mode de résolution ne se fait pas dans le but d’un constat attendu après la résolution, un constat attendu ne décide pas du mode de résolution. Il y a une relation entre les deux, mais sans influence de l’un sur l’autre.

En marge, les deux constats internes au langage, succès et échec, devraient plutôt être vérifié et non‑vérifié ou confirmé et non‑confirmé. Les mots succès et échec sont trop connotés au point de pouvoir être trompeurs.

Dire qu’il y a deux types de constat, les constats sur des termes et les constats sur des contextes, quand un contexte ne peut être vu qu’à travers un terme, n’est peut‑être pas clair. Peut‑être dire qu’il y a des constats sur des termes généraux et des constats sur des interprétations, serait plus clair. True et false seraient des constats sur des interprétations, var et const seraient des constats sur des termes généraux. Reste que les termes en question ont été distingués par leur relation au contexte, par exemple var et const ont été supposés définis seulement sur des termes vérifiés, tandis que true et false rapportent si un terme est vérifié ou pas. Var et const pourrait se concevoir sans nécessiter que les termes soient vérifiés, mais se poserait alors le question de leur interprétation sous une négation, où ils ont été vu comme abandonnés parce qu’il n’existe pas de terme sur lesquels ils pourraient porter.

Même si les constats se comprennent bien intuitivement, dans le détail ils sont pour le moment confus. Il faut espérer qu’il existe une solution autant simple est claire que celle qui a fini par être trouvée pour un type de récursion infinie ; en espérant qu’une telle solution existe. Contrairement à ce qui a été dit, cette idée ne pourra pas être abandonnée si elle n’a pas de solution, il s’avère que l’idée ne peut pas être abandonnée (la raison pour laquelle les constats sont incontournables, a été donnée précédemment) et doit trouver une solution, sinon le langage sera trop limité.

Il y a une bonne raison de poser que les constats sont tous applicables sur des termes possiblement non‑vérifiés et pas seulement certains et d’autres pas : le contraire signifie une supposition sur la conclusion, et cette conclusion n’a pas de place dans une sémantique générale des constats.

Quand il a été dit que A var s’applique à un A résolu, tandis que A false ne nécessite pas que A soit résolu, une supposition est faite sur var qui n’est pas faite sur false et alors dans la sémantique des constats en général, sont mêlés des détails spécifiques certains constats. C’est difficilement défendable.

Pour la question de savoir si oui ou non il faut distinguer constats sur des contextes et constants sur des termes, et si c’est une bonne idée de poser que les constats sont vu à travers des termes, quelque soit leur status, il y a un constat sur un contexte qui par exemple ne pourrait pas être fait, c’est celui de savoir si un contexte est vide ou pas. Mais est‑ce pertinent. On peut imaginer qu’un contexte initiales contiennent des liaisons de variables, que ces variables ont des noms qui n’apparaissent dans aucune règle. Dans ce cas, n’importe quelle résolution sous ce contexte non‑vide, aboutira aux mêmes conclusions qu’avec ces mêmes résolution dans un contexte vide. Ça montre que par exemple le notion de contexte vide, n’est même pas pertinente, que effectivement seul compte le rapport des termes à un contexte. Ce qui n’a pas d’effet sur une résolution, est non‑pertinent pour cette résolution. Poser que même les constats sur des contextes se font à travers des termes, semble être fondé.

Reste la question de la distinction entre termes généraux et termes représentant une interprétation. Mais un terme interne peut correspondre à une interprétation, que ce soit entièrement ou en partie, alors un constat qu’on comprend facilement comme portant sur une interprétation, par exemple false, peut aussi s’appliquer à un terme interne. C’est la définition du constat qui dit comme le terme est vu par ce constat. Aussi, la même remarque que précédemment sur une distinction à ne pas faire entre constats, s’appliquerait. Ce serait une autre distinction sur les types de termes auxquels s’appliquent certains constats et d’autres pas, ce mélange de niveau de définition à ne pas faire.

À moins que ce ne soit encore contesté, les constats s’appliquent toujours à des termes et à n’importe quels termes sans distinction, vérifiés ou pas.

Quand une règle « A : {H}. » est appliqué sur un terme H2 pour obtenir un A2, le terme A2 est produit directement à partir de H2, même si la démonstration de la règle distingue plusieurs cas.

C’est important à noter : le terme produit ne l’est pas via un chemin distinct selon le cas, le chemin passe par dessus les cas ou les court‑circuite. Ça doit avoir une signification, mais laquelle …

Note : c’est en pensant à une règle où les variables de la conclusion sont toutes liées par l’hypothèse. Les récents cas contraires sont à revoir.

Les variables apparaissant dans les hypothèses, ont été décrites comme des sortes de constantes. C’est assez correcte d’un certain point de vue et ça a l’avantage de facilement faire comprendre ce qu’on ne peut pas en faire, mais elles sont plus formellement des variables non‑résolubles, typiquement indéterminées non‑résolubles et dans le cas où elles sont liées à un terme, c’est ce terme qui est non‑résoluble (en oubliant pas que la liaison d’une variable ne peut pas être défaite).

La différence est importante, parce que des variables non‑résolubles sont possibles aussi en dehors des hypothèses, pourtant elles n’y ont pas été comparées à des constantes, mais simplement dites non‑résolubles. Les variables dans les hypothèses sont exactement de la même nature. Comparer les unes à des constantes et pas les autres, suggère qu’elles ne sont pas de la même nature, ce qui est incorrecte.