Les logiques : notes en vrac

Faire finir un certain type de récursion infinie.

Un terme T, sous entendu une interprétation, est vérifié par une règle récursive. Quelle est la solution de T ? Trois réponses sont proposées, toutes les trois me semblant acceptables, mais la troisième est la seule formellement justifiée dans le contexte du langage défini ici.

La récursion est vue comme une suite convergente. Si à une récursion, le terme T est le même qu’à la précédente récursion, alors on a le T vers lequel converge la série et alors sa solution. Attention : T est le terme vérifié, pas une variable de ce terme ou un terme interne, sinon ça n’est pas valable.

Si le terme T est le même à une récursion qu’à la précédente récursion, alors il n’existe pas de T plus spécifique et alors si la solution n’est pas T, il ne peut pas exister de solution. Au choix, le résultat est soit T soit pas de solution.

La résolution est vue comme sous l’hypothèse {T} à prouver ultérieurement. Si on se trouve à devoir résoudre T à nouveau, comme on est sous l’hypothèse {T}, on peut omettre cette résolution, T étant vérifié par l’hypothèse. La récursion s’arrête alors, achevant la résolution de T, prouvant par là l’hypothèse {T}. Attention : ça ressemble à la permission de court-circuiter une vérification, mais ça ne l’est pas, parce que ça n’est valable que exactement comme décrit, en particulier le terme T doit parfaitement correspondre à {T}, ne pas être un T' dérivé d’un précédent T, sinon ça n’est pas valable.

Note : dans chacune de ces trois réponses, on se préoccupe pas de savoir si le contexte à changé ou pas entre la récursion actuelle et la précédente, on ne se préoccupe que de T. Si le contexte n’a pas changé, T n’a évidemment pas changé, mais T peut ne pas avoir changé alors que le contexte a changé.

À la suite du message précédent.

Ça signifie que par exemple « (r A) : (r A). » peut être tenue pour équivalente à la règle inconditionnel « (r A). ». Peut, parce qu’il ne serait pas incohérent de considérer que c’est une récursion infinie. Comme dans le second cas du message précédent, on pourrait avoir le choix entre une solution et pas de solution.

Justement, c’est un choix fait pour la sémantique : si un terme et éventuellement vérifiable par une règle et certainement vérifiable par une hypothèse, il doit obligatoirement être vérifié par l’hypothèse sans tenter de le vérifier par la règle. Une hypothèse a la priorité sur une règle correspondante. Ce choix qui avait déjà été envisagé et est maintenant confirmé, n’est pas formellement nécessaire, mais il est posé parce que pas incohérent et utile au point d’en être nécessaire en pratique. Si la sémantique dit qu’une vérification ne doit pas passer outre une vérification par une hypothèse quand elle est possible, ça signifie qu’elle pose que la possibilité que la vérification d’un terme se fait implicitement sous l’hypothèse de ce terme, doit obligatoirement être considérée.

C’est ça, l’état hypothétique d’un terme. Cet état est distinct du type d’interprétation, mais pas indépendant, parce que ça n’est pas applicable à un terme en temps qu’hypothèse, comme il est déjà une hypothèse.

Le message précédent et le premier paragraphe de ce message, clarifient la signification des l’exemple de alloc et free dans une couche #1, appliquées à des termes dans une couche #2.

Même si les règles de la couche #1, mentionnées depuis la couche #2, par les termes posés dans cette couche #2, sont à la recherche de confirmations par ces termes, elles peuvent devoir faire des résolutions. En effet, ces règles de la forme « A : B. » ne peuvent pas être appliquées directement comme des règles de la forme « A : {B}. », les termes de la couche #2 n’étant pas vérifiés à priori. Quand un terme n’est pas dans un état vérifié, il doit être résolu pour être vérifié, même si le terme lui‑même n’est pas produit par la règle par résolution. C’est différent avec les termes dans un état vérifiés, avec lesquels les règles de la couche #1 peuvent être appliquées comme si elles étaient de la forme « A : {B}. ».

Une règle qui est de la forme « A : {B}. » dans la couche #1, ne peut pas être appliquée sur des termes de la couche #2 qui ne sont pas dans un état vérifié. C’est seulement pour les termes vérifiés, que les règles de la couche #1 qui sont de la forme « A : B. » et celles qui sont de la forme « A : {B}. », se confondent. Sinon elles ne se confondent pas, et alors elles ne se confondent pas dans le cas général. Les règles qui sont de la forme « A : {B}. » dans la couche #1, ne peuvent être appliquées qu’après les règles qui y sont de la forme « A : B. »


C’est différent pour un terme qui n’est pas une interprétation mais une construction. La remarque serait pertinente pendante l’imaginaire construction d’un terme, mais ils sont tenus pour posés tout entier d’un coup. Si on considère qu’un terme est construit par une résolution, alors on est dans le cas d’une résolution.

Mais toujours en donnant la priorité à la confirmation, il ne s’agit pas d’une résolution ordinaire. Il a été dit que une règle peut nécessiter un terme A, qui n’existe pas, mais est dérivable d’un terme B qui existe, que dans ce cas elle dérive A de B, pour avoir la confirmation A. Mais elle peut avoir le terme A dans un état non‑vérifié avec B qui existe en même temps. Dans ce cas, elle ne peut pas résoudre A en ignorant B, elle doit vérifier A avec B.

Reste le cas ou A est vérifiable à la fois avec un B1 et avec un B2, ou même le cas où un A est manquant et dérivable d’un B1 ou d’un B2. C’est un cas d’ambiguïté dans les faits au lieu de par les règles.

Peut‑être faut‑il envisager aussi le cas où A est le même, qu’il soit vérifié ou dérivé avec B1 ou B2 et dans ce cas, il n’y a pas d’ambiguïté, seulement une double‑confirmation.

À côté du choix sémantique justifié par une raison pratique, on pourrait en allant trop vite, voir une justification plus directement sémantique. Si un terme a deux règles candidates et qu’il est vérifiable par une des deux règles mais pas par l’autre, il est vérifié, il n’est pas permis d’ignorer la règle qui le vérifie. On pourrait considérer qu’on est dans le même cas. Mais ça ne l’est pas, parce qu’une réponse négative alors qu’il existe une réponse positive, n’est pas la même chose qu’une absence de réponse quand une réponse positive pourrait exister. On est au minimum à la limite entre la capacité d’une mise en œuvre et la sémantique. Surtout qu’il existe un autre cas de récursion infinie pouvant être traitée d’une manière autant formellement justifiée, mais qui ne sera pas exposé ici et il n’est pas impossible qu’il en existe d’autres encore. Disons que ce cas méritait d’être souligné, au moins parce qu’un exemple l’impliquant, a été mentionné.

Définition sémantique ou capacité d’une mise en œuvre, … peut‑être est‑il préférable de considérer que ça ne fait pas partie de la sémantique, seulement d’une capacité, sinon la sémantique en deviendrait compliquée et même sujette à révision au grès des capacités d’une mise en œuvre. Une mise en œuvre ultérieure à une première, ayant de meilleures capacités, serait considéré comme conforme à la même sémantique, mais avec de meilleures capacités, c’est à dire pouvant fournir une réponse là où une autre n’en fournirait pas et une absence de réponse et à ne pas confondre avec une réponse négative.

Révision : ce n’est pas un choix sémantique, c’est un choix technique, conforme à la sémantique et il en existe d’autres. Les cas où un choix technique a comme conséquence qu’une réponse peut être fournie quand il pourrait y avoir absence de réponse, devrait cependant être décrits.

À la suite du message précédent, avant d’autres précisions encore manquantes.

Ce serait plus clair de le dire ainsi : la sémantique du langage ne dit pas exhaustivement ce que les choses sont, elle ne permet que d’écrire des formules qu’elles doivent vérifier et ce que signifie d’être vérifiée pour une formule. Dire ce que sont les choses exhaustivement, équivaudrait à définir aussi comment ces propriétés sont vérifiés et cela avec la garantie que si elle ne dit pas comment vérifier une chose alors c’est qu’elle n’est pas vérifiable. Ça supposerait de pouvoir résoudre toutes les formules pouvant être écrites et c’est ça qui est trop et justifie en pratique, de séparer deux niveaux de la sémantique : le second est comment les choses sont vérifiées et donc dans quels cas on peut parvenir à les vérifier. Ce second niveau peut être considéré comme une extension du premier et doit être en accord avec. Le second niveau peut être considéré comme une solution à un problème pour lequel il existe plusieurs solutions, probablement partielles, avec des capacités plus ou moins étendues.

En marge à ce propos, l’obligation que si un terme est vérifiable à la fois par une hypothèse et par une règle, il est vérifié par l’hypothèse, est considéré comme faisant partie du second niveau, pas du premier. Idem pour la preuve de satisfiabilité des règles, qui de plus, comme elle ne fait pas partie du premier niveau, ne peut pas être une exigence du second niveau, pour rester conforme au premier, même si on peut imaginer un comportement optionnel et non‑conforme par restriction, en faisant une exigence.

La sémantique définie, est celle du premier niveau, appelée la sémantique tout‑court, ce qui est du second niveau est considéré comme des détails d’une mise en œuvre envisagée. Ainsi, l’idée de la normalisation des têtes de règles, précédemment envisagé, est aussi considérée comme du second niveau, un détail interne à une mise en œuvre qui n’est pas la seule possible.

Sur les termes posées en hypothèses, des précisions plus générales que celles plus limitées qui avaient été déterminées quand les hypothèses avaient été initialement discutées. Ce qui est dit dans ce message, est possiblement sujet à des remises en question ultérieures.


Une preuve de {H} et une preuve de « C : {H}. », ne sont pas de la même nature. Le premier cas est abordé dans ce message, le second cas le sera dans le suivant. Le premier cas est le plus délicat après l’utilisation qui en a été faite précédemment pour sortir d’une récursion infinie, un cas qui nécessite de poser des précisions qui n’avaient pas été nécessaires quand les hypothèses ont été abordées fin‑Novembre 2020. Ces nouvelles précisions rendent plus générale la description des termes en hypothèses, en couvrant des cas particuliers, et expliquent mieux leur utilisation et leur sens que ça ne l’avait été.

Prouver une hypothèse, c’est prouver qu’un terme supposé vérifié, l’est effectivement. Un terme peut être supposé vérifié pour poursuivre en tenant ce terme pour vérifié et ne valider la conclusion ainsi produite, que que quand la supposition est vérifié, c’est à dire que le terme est effectivement vérifié, ce qui peut parfois se faire antérieurement ou ultérieurement, au choix, parfois seulement ultérieurement. Dire qu’une hypothèse doit être prouvée pour valider les conclusions réalisées avec cette hypothèse, a l’air cohérent et suffisant pour rassurer, mais les cas pratiques peuvent rester perturbants ou laisser des doutes tellement prégnants que cette explication ne suffira plus à les dissiper. Pour cette raison, il faut re‑expliquer le principe dans le contexte où il interroge le plus, celui de sa récente utilisation dans une récursion à priori infinie, et c’est aussi nécessaire pour apporter des précisions sans lesquelles on peut se demander si la sémantique décrite est au moins réalisable.

D’abord un retour sur l’utilisation d’une hypothèse, en général. Quand l’hypothèse est utilisée, on ne sait pas comment le terme est vérifié, on « sait » (guillemets, car sous réserve de preuve de l’hypothèse) seulement qu’il est vérifié, c’est tout. Le terme contient des parties constantes, ces parties constantes sont connues, mais si le terme contient des parties variables, alors ces parties variables sont inconnues, même pas connues comme non‑liées, totalement inconnues et sur lesquelles aucune résolution ne peut être appliquée, c’est à dire opaques et gelées. Comment prouve‑t‑on l’hypothèse ? En prouvant que le terme est vérifié, soit antérieurement, soit ultérieurement à l’utilisation de l’hypothèse. Une preuve de {H}, c’est une preuve de H. On peut alors se demander quel en est l’utilité, si une preuve de {H} c’est une preuve de H, autant juste prouver H, non ? Une première utilité, qui ne répond pas encore vraiment à la question, avait été vue où un {H} prouvé est un témoignage que H est vérifiable. Cette utilité était informative et ce fait pouvait éventuellement servir pendant la résolution de termes. Mais la récente séparation de la sémantique en deux niveaux en fait un détail du second niveau, c’est à dire ne faisant par partie de la sémantique définie tout‑court. Une seconde utilité, qui répond à la question est celle vue précédemment, de pouvoir vérifier des règles récursives (et ce type de terme est permis par le premier niveau de la sémantique), y compris indirectement récursives. Dans ce cas, il peut être impossible d’utiliser une preuve de H, si H est justement en train d’être vérifié, d’où l’utilisation de l’hypothèse {H} au lieu de H lui‑même, parce qu’il n’est pas possible de faire autrement.

Si une chose perturbe en y pensant, c’est peut‑être celle‑ci : mais on a pourtant vu que pendant la vérification d’un terme, ce terme n’est pas vérifié et ça semblait convaincant, alors cette idée que {H} dit que H est vérifiée, est douteuse, non ? Ce n’est pas douteux pour deux raisons. La première, avant la plus parlante qui suit, est que l’hypothèse doit être prouvée, que ce soit avant ou après son usage et si elle n’est pas prouvée, la conclusion faite à partir de l’hypothèse est irrecevable. La seconde, plus parlante, est que l’hypothèse est une abstraction, elle ne dit pas exactement quelle est la solution du terme à moins qu’il ne soit entièrement constant, elle dit seulement que le terme est résolu. Ne pas oublier cette abstraction peut aider à ne pas être trop mal à l’aise avec cette idée de supposer {H}. Il est possible que ce ne soit pas assez pour être rassurant, alors voici une reformulation de la même chose : après la résolution d’un terme, on obtient une certaine valeur pour ce terme, c’est ce qu’on obtient à la fin de sa résolution, mais quand on utilise l’hypothèse qui lui correspond, on ne connait justement pas cette valeur finale, qu’on utilise pas, et alors on utilise pas cette valeur avant de l’avoir produite, puisqu’on ne l’utilise simplement pas. L’hypothèse de {H} est une abstraction de H, réduit à son statut vérifié. Mais il y a tout de même un terme dans {H}, avec lequel il doit y avoir une correspondance, pour qu’on ne puisse pas supposer n’importe quoi avec ce {H}. Par exemple on ne peut pas utiliser {c1} pour supposer qu’on a c2, {c1} ne permet que de supposer qu’on a c1, ne permet rien d’autre, et c’est ce qu’on veut.

Qu’est que la correspondance au terme de l’hypothèse ? C’est une correspondance entre deux termes où une constante correspond à la même constante et où chaque variable est réduite à (plutôt abstraite à) une identité et ne correspond qu’à cette identité. Conformément à ce qui a été dit plus haut, les parties constantes sont connues, les parties variables sont inconnues, mais sont tout de même égales à elles‑mêmes et une variable libre peut s’y lier.

Un terme (r a) peut être mis en correspondance avec l’hypothèse {(r a)}, mais un terme (r V) ne peut pas être mis en correspondance avec un terme {(r X)}, si V est une variable ordinaire, puisque X est réduite à une identité et n’est égale qu’à cette identité et que V est une variable qui n’est pas dans cet état. Poser un terme (r V) en hypothèse, nécessite donc de lui substituer un autre terme (r V) où les variables libres sont liées à des identités. Pour être plus précis, si le terme est noté (r V) mais que au moment de poser l’hypothèse correspondante, V est liée à par exemple (abc D) où D est libre, alors (r V) est en réalité (r (abc D)) et alors c’est l’hypothèse {(r (abc D)}, qui est posée où D est réduite à une identité qui lui est propre. Quand (r V) est posée en hypothèse, V est lie à (abc D) où D est une identité au lieu d’être un variable libre. Ainsi, le terme (r V) pourra être mis en correspondance avec le terme de l’hypothèse {(r V)} qui est concrètement {(r (abc D)}, la variable V ne pourra plus changer de valeur, ces parties variables étant réduites à des identités, elles ne peuvent pas être liées à autre chose qu’à leur identité. Donc, en plus de correspondre à, et de pouvoir alors être supposé par, son hypothèse, le terme (r V) ne pourra pas lui jouer un mauvais tour en changeant de valeur, ce qui fait que son hypothèse est assurée lui correspondre.

Mais se pose un problème : on aura alors vérifié le terme dans l’hypothèse, par le terme d’origine à partir duquel l’hypothèse a été posée.

D’abord, comment retrouver ce terme d’origine ? La solution est dans une nécessité. Le terme d’origine se trouve gelé et opaque, pour que son hypothèse soit cohérente. Cela signifie que si on veut retrouver le terme d’origine, on ne doit plus utiliser l’hypothèse. On pourrait considérer comme invalide toute référence à l’hypothèse après restauration du terme dans son état d’origine, mais cela poserait des problèmes d’interprétation de cet usage invalide. Il serait plus simple d’abandonner l’hypothèse, cet abandon de l’hypothèse rendant le terme d’origine. De cette manière, plus besoin de se soucier d’ultérieures références invalides à l’hypothèse et est défini en même temps un moyen de restaurer le terme d’origine. Reste à définir la construction à utiliser. Une idée ne nécessitant pas de construction spécifique, serait que l’hypothèse est abandonnée automatiquement quand on quitte l’instance de la règle qui a introduit l’hypothèse. L’abandon de l’hypothèse et la restauration du terme d’origine, se ferait automatiquement.

Mais si on a abandonné l’hypothèse, comment fait‑on pour valider la vérification du terme sous cette hypothèse qui n’existe plus, comme on doit démontrer cette hypothèse pour valider le terme ? La solution est implicitement dans la précédente, pour le cas de la récursion : quand on sort de l’instance de la règle parce que sa vérification est achevée, le terme est alors vérifié et donc son hypothèse aussi. D’autres justifications et mécanismes seraient peut‑être nécessaires dans d’autres cas d’utilisation.

Ces explication ne décrivent pas la sémantique du premier niveau, elles font parties de la sémantique du second niveau, pour lequel d’autres solutions sont possibles, dont une autre évoquée, celle d’avoir une opération explicite de récupération du terme d’origine et une interprétation restant à définir, des cas de référence invalide à l’hypothèse. Ce que la sémantique du premier niveau exige, c’est seulement que le terme posé en hypothèse, ne change pas le temps que l’hypothèse correspondante est active, ceci pour que l’hypothèse ait le sens qu’elle doit avoir. Ce qui est décrit, est juste une manière d’y parvenir, exposé surtout pour convaincre que cette sémantique est réalisable d’une manière qui la rende utilisable.

Quand les hypothèse avaient été discutées, il ne s’était jamais présenté de cas où on devait récupérer un terme sous sa forme d’origine après l’avoir posé en hypothèse, raison pour laquelle ces explications sont introduites seulement maintenant, par nécessité, comme on a récemment utilisé un terme posé en hypothèse, pour prouver le terme lui‑même tel qu’il est et il n’est pas un terme gelé.

Même si on y pense peut‑être pas immédiatement, on peut tôt ou tard se poser deux questions en repensant à ce qui précède. La première : la solution finale d’un terme partiellement déterminé, peut être plus déterminé, c’est à dire plus spécifique, que le terme sous sa forme moins déterminée, c’est à dire plus générale, mais alors on s’interdit dans le cas présent que le terme final soit plus spécifique ? La seconde : après avoir récupéré le terme sous sa forme d’origine, s’il contient des variables libres, il peut encore évoluer par la suite, est–ce normal ? Les réponses sont respectivement Partiellement et Oui et les deux remarques sont liée. Il est normal et pas incohérent que le terme puisse changé après sa sortie d’hibernation, parce qu’on a vérifié le terme avec ses variables libres tenues pour inconnues et donc sous une forme générale et cette forme générale, vaut pour les formes plus spécifiques (*). Ceci justifie encore de parler d’une hypothèse comme d’une généralité. Donc, il est normal que le terme évolue, parce que s’il évolue, il ne le pourra que vers une forme plus spécifique, comme conséquence de la sémantique de l’unification, ce qui répond au deux remarques en même temps. Mais la première question a besoin d’une précision : la solution ne peut devenir plus spécifique que après l’abandon de l’hypothèse.

Reste une question en suspend : devrait‑il être possible, pour un terme posé en hypothèse, de devenir plus spécifique que le terme d’origine ? Dans ce cas, le terme posé en hypothèse ne serait plus gelé. Un argument en faveur de l’idée, est que l’hypothèse étant plus générale que le terme, ce qu’on peut en conclure ne peut que s’appliquer à un terme plus spécifique et c’est même posé dans le paragraphe précédent. Un argument en défaveur et que justement, est‑il vraiment certain que ce qui peut se vérifier sur un terme général, se vérifie aussi sur un terme plus spécifique ? Normalement oui, sinon le paragraphe précédent est erroné, si le terme plus spécifique est effectivement vérifié, il ne peut que être en accord avec le contexte du terme plus général, sinon le terme plus spécifique est en contradiction et ne peut pas être tenu pour vérifié. Malgré ces arguments, un argument en défaveur peut toujours persister : l’idée de variables liées à une identité, c’est à dire de termes gelés, était une bonne garantie et alors s’en passer demande réflexion.


(*) Ceci implique qu’une variable libre ne peut pas être tenue pour être une valeur particulière, mais seulement pour une valeur indéterminé, le cas le plus général possible qu’elle puisse connaître. C’est la raison pour laquelle deux variables libres peuvent être liées entre elles, cependant que indéterminé ne peut pas être égale à indéterminé. En fait, la question ne se pose même pas, comme aucune valeur correspondant à l’indéterminé n’est accessible. Mais ça souligne encore qu’il faut bien prendre garde à ne pas confondre le Any évoqué il y a un an et demi, quand il est utilisé pendant la résolution ou la vérification et ce même Any quand il est sujet à une interprétation externe. On peut imaginer que les variables libres sont liées à un Any représentant une valeur indéterminée, mais Any n’a vraiment de sens que comme représentation externe d’une valeur indéterminée (et encore, en faisant à attention à ne pas mélanger des Any qui ne sont pas liés entre eux), comme représentation externe seulement. La caractère indéterminé plutôt que lié à Any, d’une variable libre, avait déjà été noté en discutant de la sémantique de la double et simple négation.

Le cas de « C : {H}. » avait été déjà abordé mais seulement à moitié. Sa preuve l’avait été, mais pas son utilisation. Une partie de ce qui avait été déjà abordé, est répété, pour en rappeler l’essentiel.

Contrairement au cas du paragraphe précédent, {H} n’est pas un terme concret posé en hypothèse, il est une hypothèse posée telle‑quelle, une complète abstraction de tout terme étant identique à H ou étant un cas particulier de H, c’est à dire plus spécifique que H. Comme ce n’est pas un terme concret posé en hypothèse, les variables ne peuvent que être posées directement comme des identités, ne peuvent correspondre à rien d’autres. L’hypothèse peut représenter plusieurs cas, accessibles après ouverture de l’hypothèse. Pour prouver qu’avoir {H} équivaut à dire qu’on a C, il faut prouver que c’est ainsi à partir de tous les cas de {H}. Parfois l’ouverture de l’hypothèse n’est pas nécessaire pour le vérifier. Quand l’hypothèse telle‑quelle n’est pas suffisante car pas assez précise, qu’il faut une preuve au cas par cas, les cas à couvrir sont eux‑mêmes représentés par des termes où les variables sont réduites à des identités. Le comment une démonstration d’une telle règle peut être réalisée, n’est pas rappelé, ce n’est pas utile pour les questions à éclaircir maintenant.

Contrairement au cas du message précédent, le cas des variables ne pose pas de questions, elles ne peuvent que être abstraites.

Après qu’elle a été prouvée (non‑valable sinon), la règle peut valoir pour elle‑même, témoignant qu’on a prouvé une chose dont on voulait s’assurer et on peut s’arrêter là. Quand les hypothèses ont été discutées, ça n’était en effet pas allé plus loin.

Mais on peut aussi utiliser cette formule pour dériver ou plutôt vérifier ou déterminer un terme à partir d’un autre (ce type de règle ne s’utilise pas en mode résolution). En marge, aucun mécanisme n’avait été prévu pour passer un terme comme solution à une condition d’une règle, jusqu’à récemment et comme effet collatéral, en répondant à d’autres besoins, avec le modèle en couches. La règle est d’abord instanciée. Quelque soit la manière dont il est passé pour application à la règle, on imagine qu’on a un terme T candidat. T doit vérifié et être autant ou plus spécifique que H, sinon l’application n’est pas valide. Si T peut être unifié à H (la copie instanciée de H), alors l’unification lie les variable de H, qui cette fois ne sont pas des identités, mais des variables libres. Les variables correspondante dans C, sont par là aussi liées. Le terme à vérifier ou à déterminer, est unifié avec C, pour lui transmettre le résultat. Le terme vérifié est égal ou plus spécifique que le terme d’origine. Le terme vérifié peut être à l’origine d’une contradiction pendant son unification à C, l’application de la règle pour vérifier un terme, n’est donc pas garantie réalisable, même si la règle est vérifiée et que T est bien un cas de son hypothèse.

T doit être vérifié (*), parce que la dérivation de C à partir de H, n’est définie que pour H supposé vérifié. De plus, T doit être autant ou plus spécifique que H, pour garantir que le T vérifié est bien un H vérifié. En particulier, H ne peut pas déterminer une variable de T, seule T peut déterminer une variable de H et par là, une variable de C et par là, du terme vérifié ou déterminé par application de la règle. Si T est par exemple un (X Y) vérifié, que H est (a Z), alors l’application de la règle n’est pas valable, comme X n’est pas nécessairement « a » alors que la dérivation n’est définie que à partir de (a Z). Pour cette raison, il n’est pas suffisant que T soit vérifié, il doit être aussi testé autant ou plus spécifique que H. Il peut être plus spécifique que H, comme H est prouvé pour tous les cas de H, c’est à dire y compris pour les cas particuliers ou plus spécifiques (c’est la même chose). Il est possible d’imaginer qu’on vérifie d’abord que T est autant ou plus spécifique que H puis qu’on pratique une unification ordinaire entre T et H, mais on peut aussi imaginer une unification qui vérifie que T est plus spécifique que H en même temps que de faire l’unification, ce qui serait une unification asymétrique, contrairement à l’unification ordinaire. Cette unification asymétrique avait déjà été envisagée quand s’était posée la question de comment déterminer les cas de {H2}, à partir des cas de {H1}, quand H2 est plus spécifique que H1. Mais cette question là n’avait été que rapidement survolée sans entrer dans tous les détails et reste encore en suspend.

(*) Il est aussi envisageable que T soit seulement supposé vérifié, plutôt que vérifié tout‑court, auquel cas, le résultat de l’application de la règle ne serait validé que quand cette supposition serait vérifiée. C’est à dire qu’on peut utiliser l’hypothèse d’un terme, aussi pour remplir les conditions d’une hypothèse, pas seulement pour vérifier un terme.

— Édit : une bonne partie de ce message est une mauvaise piste —

Dans le message précédent, la condition que T soit autant ou plus spécifique que le H d’origine, fait échos à la question laissée en suspend dans le message avant le précédent. Même si une règle « C : {H}. » n’est pas de la même nature que l’hypothèse d’un terme, {T}, on pourrait suspecter que la mise en correspondance d’un terme avec une hypothèse, devrait avoir les mêmes conditions dans les deux cas. Il est important de noter que ce qui est décrit dans le message avant le précédent, c’est à dire geler le terme posé en hypothèse, est un cas particulier de ce qui est décrit dans le précédent, c’est à dire la condition que le terme correspondant à l’hypothèse soit plus spécifique, mais il faut s’assurer que ce n’est pas plus restrictif que vraiment nécessaire. Une restriction non‑justifiée ne serait pas acceptable, les limites à l’expressivité étant à éviter. Plus qu’une limite à l’expressivité, ce pourrait même être une source d’incohérence, en permettant de vérifier une impossibilité là où il y a pourtant bien une possibilité. Une fausse réponse négative est en effet une incohérence, contrairement à une absence de réponse.

On peut noter que la condition posée dans le message précédent, n’est pas seulement que T soit autant ou plus spécifique que H, une autre condition est que T soit vérifié. Dans le cas du message avant le précédent, la vérification du terme et de l’hypothèse se confondent. Mais on a aussi vu que dans le message précédent, T puis lui‑même être supposé vérifié et le résultat de l’application de la règle, être valide seulement après que T ait été prouvé effectivement vérifié. Rien ne semble empêcher alors que les mêmes conditions soient applicables dans le message avant le précédent.

Deux exemples concrets pour aider à convaincre. On a vu que la règle « (r A) : (r A). » est équivalente à « (r A). » Ici, la variable A peut être gelée, ça ne pose ps de problème. Mais qu’en serait‑il avec cette variante : « (r A) : (eq A c) & (r A). » ? On ne pourrait même pas poser une nouvelle hypothèse pour la récursion, comme A est gelée, le terme (eq A) ne pourrait pas être vérifié. La conclusion serait que cette règle n’est jamais vérifiable. Mais est‑ce vraiment le cas ? Il y a de quoi en douter si on repense à la justification informelle mais plus intuitivement compréhensible, de la suite convergente. Dans ce cas, A serait liée à c, puis la récursion se poursuivrait avec une A qui resterait liée à c. On aboutit bien à une valeur stable de A. Si on considère que l’hypothèse {(r B)} ne gèle pas le terme d’origine (r A), mais qu’il doit être vérifié que (r A) est autant ou plus spécifique que (r B), alors (r c) qui devrait être vérifié par le second terme de la condition, est vérifié par hypothèse au lieu d’entrer dans la récursion, comme (r c) est plus spécifique que le (r B) de l’hypothèse. On conclut alors que la règle est vérifiable, et on pourrait même remarquer qu’elle est équivalente à « (r A) : (eq A c). »

Si dans le paragraphe précédent, le terme de l’hypothèse a été écrit (r B) au lieu de (r A), c’est pour souligner que le terme de l’hypothèse est supposé être une copie du terme d’origine. Mais comme la condition de vérification de l’hypothèse est que (r A) soit autant ou plus spécifique que (r B), si (r A) devient plus spécifique, on pourrait croire que l’hypothèse pourrait suivre et alors le terme de l’hypothèse pourrait rester lié au terme d’origine, c’est à dire rester le terme d’origine. Mais ça empêcherait alors de vérifier un éventuel autre terme, qui correspondrait aussi initialement à (r B), mais qui ne serait pas devenu plus spécifique, ce qui présenterait un risque d’incohérence par faux négatif.

Il semble donc que la réponse laissée en suspend dans le message avant le précédent, est que le terme posé en hypothèse ne doit pas être gelé, que l’hypothèse avec laquelle on vérifie une correspondance pour vérifier un terme, doit être une copie du terme d’origine. Une copie est à comprendre au sens de avec des nouvelles variables liées comme dans le terme d’origine mais non‑liées à celles du terme d’origine, et ainsi récursivement pour tout le terme. En moins de mots, le terme de l’hypothèse est une copie du terme d’origine, qui n’évolue pas si le terme d’origine évolue.

Ça demande encore réflexion.

— Édit : une bonne partie de ce message est une mauvaise piste —

Ce n’est pas encore une réponse aux questions, mais des remarques, avec quelques répétitions, qui disent quelles propriétés la réponse devra nécessairement avoir.

Si le terme est un terme à résoudre, il ne peut pas être gelé, comme dans cet état il ne peut pas être résolu.

Si dans le cas d’une hypothèse abstraite, on a des variables abstraites, c’est parce qu’on couvre tous les cas possibles d’un terme. Avec un terme en hypothèse (ou un terme hypothétique, comme le nom était venu naturellement précédemment), on a pas de couverture de cas, seulement la supposition que le terme sera vérifié. Ça exclus naturellement que l’hypothèse aient des variables abstraites. Ce paragraphe est aussi une confirmation du paragraphe précédent.

Avec un terme en hypothèse, l’hypothèse représente le terme vérifié avec éventuellement des liaisons de variables, alors le terme peut changer. Quand le terme change, c’est pour devenir plus spécifique. Si l’hypothèse est une copie du terme initial, elle devient par la suite plus générale que le terme et peut donc permettre de confirmer autre chose que le terme qu’elle est sensée représenter, ce qui ne respecte pas la sémantique de l’hypothèse. Ça exclus naturellement que l’hypothèse reste une copie du terme initial ou alors ça exclus que le terme puisse lui correspondre quand il devient plus spécifique. En mots plus claires, l’hypothèse doit suivre le terme, pour qu’il puisse lui correspondre quand il devient plus spécifique. On peut ici faire échos au paragraphe précédent : l’hypothèse n’a qu’un seul cas, qui est un terme en particulier.

Avant d’expliquer ce que pourrait signifier pour l’hypothèse, suivre le terme, il faut dire plus précisément, sous quelle condition poser un terme en hypothèse, ne permet pas de court‑circuiter sa vérification. L’hypothèse peut être posée de deux manières : avant d’entrer dans la règle ou après être entré dans la règle. Si l’hypothèse est posée avant d’entrer dans la règle, elle permet de vérifier le terme sans même entrer dans la règle et donc sans vérifier quelque conditions que ce soit, permettant en fait de vérifier n’importe quel terme. Poser un terme en hypothèse avant d’entrer dans la règle qui le vérifie, permet effectivement de court‑circuiter sa vérification tout‑court. Ceci explique pourquoi il est important que l’hypothèse du terme, soit posée après être entré dans la règle et implicitement avant de commencer à vérifier ses conditions.

Cette précision étant faite, si l’hypothèse suit le terme, elle ne peut le faire que d’une manière conforme à la condition posée dans le paragraphe précédent. Cette condition exclue la possibilité que l’hypothèse soit simplement lié au terme, c’est à dire soit finalement un alias du terme, sinon elle serait comme posée avant d’entrer récursivement dans la règle devant le vérifier.

En résumé pour le moment. Pour que le terme soit vérifié par l’hypothèse, il doit correspondre exactement au terme en hypothèse, sinon l’hypothèse peut permettre de vérifier un autre terme, ce qui n’est pas conforme au sens de l’hypothèse. Comme il doit y avoir correspondance exacte, quand le terme change, l’hypothèse doit suivre, mais seulement après l’entrée dans la règle devant vérifier le terme avec sa nouvelle valeur, sinon l’hypothèse permet de court‑circuiter la vérification du terme et par là, permet de vérifier n’importe quoi. L’hypothèse ne peut pas être une forme d’alias du terme, sinon la condition de la phrase précédente n’est pas vérifiée.

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

Il reste la vérification de l’hypothèse par la vérification du terme. Le message précédent ne répond pas à un possible problème à ce sujet. Le problème qui se pose peut être expliqué avec deux cas concrets.

(r A) : (eq A b) & (r A).

Disons que A est initialement indéterminée. On entre dans la règle et pose l’hypothèse correspondante, {(r indéterminé)}. À la première condition, A est liée à b. À la seconde condition, le terme (r b) ne correspond plus à l’hypothèse, la seconde condition n’est donc pas vérifiée par l’hypothèse. On ré‑entre dans la règle récursivement. Une nouvelle hypothèse, {(r b)} est produite. La première condition est vérifiée. La seconde condition est vérifiée par l’hypothèse, il n’y a plus de récursion, on quitte la seconde instance de la règle puis la première. Le terme est finalement (r b), le terme et l’hypothèse sont vérifiés simultanément.

(r A) : (r A) & (eq A b).

Là aussi, A est initialement indéterminée. On entre dans la règle et pose l’hypothèse correspondante. La première condition est vérifiée par l’hypothèse. La seconde condition est résolue en liant A à b. Le problème est que l’hypothèse est (r indéterminé) tandis que le terme est (r b).

Dans le premier cas, on peut facilement accepter la convergence vers (r b). Dans le second cas, c’est plus difficile, mais on peut au moins accepter que si une solution existe, elle ne peut être que celle‑ci, que sinon, la règle ne produit aucune réponse. L’ordre des termes d’une conjonction étant sensé ne pas être important, ça ne pose pas de problème. Mais le problème qui se pose, est de valider l’hypothèse (r indéterminé) par la vérification du terme (r b). L’hypothèse ne suppose pas la valeur finale du terme, ne fait que supposer qu’il sera vérifié, tout en devant le suivre. Mais cela permet‑il de vérifier l’hypothèse par la vérification d’un terme qui ne lui correspond plus ?

Peut‑être une solution serait‑elle d’arranger l’ordre des conditions en plaçant à la fin, les conditions pouvant aboutir à une récursion. Ou plutôt, il faudrait placer les conditions pouvant modifier le terme, avant les conditions récursives, pour se trouver dans la même situation qu’avec le premier cas. Mais le problème est que s’il existe plus d’une condition récursive et que chacune des deux conditions récursives peut modifier le terme, cette arrangement de l’ordre des conditions n’est plus pertinent.

Manque‑t‑il une précision à comment l’hypothèse doit suivre le terme ? Ou l’idée du message précédent est‑elle une impasse ?