Les logiques : notes en vrac

Un petit miracle s’est produit , un aboutissement.

Avant un résumé ultérieurement, voici un aperçu de ce que permet la capacité de poser des termes en hypothèse. Une nouvelle notation est introduite : les deux symboles ⟦ et ⟧, entourent les termes en hypothèse pour les distinguer des autres termes.

Pour les exemples qui suivent juste après, ces règles déjà vues, sont reprises :

§nat-b (nat z).
§nat-s (nat (s N)): (nat N).
§nat-lt-b (nat-lt N (s N)) : (nat N).
§nat-lt-s (nat-lt M (s N)) : (nat-lt M N).

Un exemple trivial pour commencer :

⟦(nat N)⟧ & (nat N) ?

La réponse, et il n’y en a qu’une, est celle‑ci :

H#1
N = Abs#1

Avant que d’autres exemples ne puissent être compris, il faut d’abord expliquer comment lire celui‑ci. La notation ⟦(nat N)⟧ signifie que (nat N) est posé comme hypothèse. Pour l’écriture, ce ⟦(nat N)⟧ est considéré comme un terme et est donc séparé du suivant par le symbole de la conjonction. Comme expliqué précédemment, les hypothèses sont notées avant les termes ordinaires, excepté pour les têtes de règle, qui sont toujours écrites en premier.

La ligne affichant « H#1 » est celle affichant la chaîne d’inférences, un principe expliqué précédemment. Son unique élément est H#1, qui signifie que la seule inférence utilisée était l’hypothèse #1. Les hypothèses sont instanciées automatiquement et existent à part de la liste des règles. Si une règle ou une requête échoue, les hypothèses générées par cette règle ou cette requête, ne sont pas conservées.

La ligne affichant « N = Abs#1 » est celle affichant les valeurs des variables de la requête. Le Abs#1 signifie en gros « constante abstraite #1 », il s’agit des constantes spéciales précédemment suggérées. Ici, il n’y en a qu’une seule, comme il n’existe qu’une seule variable apparaissant dans l’unique hypothèse de cet exemple.

Il est important de noter que la requête « ⟦(nat N)⟧ & (nat N) ? » ne renvoi qu’une seule réponse, tandis que la requête (nat N) en reverrait une liste, qui serait infinie si on la laissait se poursuivre. Comme (nat N) est posé en hypothèse, (nat N) est vérifié sans énumérer des valeurs de N vérifiant (nat N).

Cet exemple était un exemple trivial, de présentation. En voici d’un peu plus intéressants, dont un particulièrement intéressant qui viendra en dernier.

⟦(nat N)⟧ & (nat (s N)) ?

§nat-s H#1
N = Abs#1

Cette exemple confirme que l’hypothèse peut être utilisée indirectement. Ici, l’hypothèse a permis de vérifier un terme dans la règle §nat-s, alors que l’hypothèse est pourtant posée dans la requête.


⟦(nat N)⟧ & (nat z) ?

§nat-b
N = Abs#1

Ici, l’hypothèse n’est pas utilisée, mais on peut voir que le N de la requête a malgré tout été instancié.


⟦(nat N)⟧ & (nat-lt N (s N)) ?

§nat-lt-b H#1
N = Abs#1

La relation est vérifiée sans énumérer des valeurs de N.


⟦(nat N)⟧ & (nat-lt N (s (s N))) ?

§nat-lt-s §nat-lt-b H#1
N = Abs#1

Une variante de la précédente requête.


⟦(nat N)⟧ & (nat-lt (s N) N) ?

Cette requête qui ne renvoi pas de solution, ne rappel pas quelque chose ? C’est la méchante requête qui restait coincée dans une boucle infinie, parce qu’elle essayait de chercher un successeur de N qui soit plus petit que N, alors que c’est impossible. Ici, la requête échoue directement. C’est cet exemple, qui est particulièrement intéressant. Si la requête « (nat-lt (s N) N) ? » se termine en récursion infinie, ce n’est pas une erreur, c’est parce qu’elle cherche des solutions à quelque chose qui n’en a pas. La requête « ⟦(nat N)⟧ & (nat-lt (s N) N) ? » , elle, ne cherche pas de solution pour N, elle ne tient N que pour la variable qui vérifie (nat N) et partant de là, échoue à vérifier (nat-lt (s N) N), sans entrer dans une recherche vaine et infinie, ce qui est un résultat plus satisfaisant.

Ça ne va pas paraître très clair encore pour le moment, cette distinction pourtant déjà faite sera éclaircie à une prochaine occasion, mais il est important de souligner encore que ces exemples sont tous évalués au niveau du langage objet seul, sans même nécessiter de niveau de langage supplémentaire. Certes, ce langage objet n’est pas le Prolog standard, mais c’en est une extension me semblant naturelle et surtout bien utile à fin de vérifications et de démonstrations.

Se demander si une hypothèse peut contenir une variable normale, revient à se demander si cette hypothèse peut être posée dans un contexte où cette variable existe déjà, ce qui peut se produire au moins avec une requête faite dans le contexte résultant d’une précédente requête.

Les exemples précédents ne posaient une hypothèse que dans la requête, il n’y a pas eu de test de règles contenant des hypothèses. Pourtant même en limitant les hypothèse aux requêtes (ce qui était d’ailleurs l’idée initiale), se pose la question de savoir si une variable apparaissant dans une hypothèse peut être une variable normale, comme le cas peut se présenter.

Example d’un tel cas :

§eq (eq A A).
#2 (r X) : (s X).
(eq Y b) ?

Y = b

⟦(s Y)⟧ & (r X) ?

…

Si le contexte de la première requête a été conservé, le Y de la seconde requête est fixé. L’instantiation des hypothèses telle qu’elle a été définie jusqu’ici, lie chaque variable apparaissant dans une hypothèse, à une constante spéciale et unique. Dans ce cas, l’hypothèse ⟦(s Y)⟧ ne peut pas être instanciée. Je ne vois pas de contre exemple prouvant qu’il serait incohérent de quand‑même instancier la requête. C’est au moins assez inattendu que cette instantiation échoue, parce que ça fait échouer la requête avant même d’avoir tenté de vérifié ses termes. Si au contraire, l’instantiation de la requête n’instancie pas une nouvelle variable, l’hypothèse porte alors sur le Y déjà fixé par la requête précédente. En fait, ça ne pose sémantiquement pas de problème, l’hypothèse ne serait alors vérifiée que pour (s b) ou pour toutes variables liées à b.

Ça resterait cohérent et ce serait un gain d’expressivité. Mais il se pose alors une autre question, celle de l’ordre des termes. Des questionnements concernant les cas possibles, vont être posés.

On considère d’abord comme à part, d’un côté les hypothèses et d’un autre côté, les termes ordinaires. On a vu précédemment que les l’ordre des termes dans une règle est sans importance (les justifications de cette affirmation ont été données précédemment). On peut comprendre facilement que l’ordre des hypothèses est sans importance, lui aussi, justement parce que ce sont des hypothèses, c’est à dire des termes déjà tenus pour vérifiés ; leur ordre ne peut alors que être sans importance. On considère maintenant les hypothèses et les termes ordinaires, ensemble et non‑plus séparément. Cette fois et si on considère qu’une hypothèse peut porter sur une variable ordinaire, l’ordre a une importance. Non‑pas l’ordre des termes entre eux ni l’ordre des hypothèses entre elles, cet ordre là reste sans importance, mais l’ordre des hypothèse par rapport aux termes et réciproquement (c’est la même chose).

Examples :

peu-importe : ⟦(r A)⟧ & ⟦(s B)⟧ & (t A) & (u B).
peu-importe : (t A) & (u B) & ⟦(r A)⟧ & ⟦(s B)⟧.

Dans les deux cas, l’ordre des hypothèse n’a pas d’importance, de même que l’ordre des termes, mais le status des variables ne serait pas les mêmes dans les deux cas. Dans le premier cas, les variables sont liées à une constante spéciale, une pour A et une pour B. Dans le second cas, les variables seraient des variables ordinaires, c’est à dire qu’il pourrait y avoir une recherche de solution pour A et B, et les hypothèses correspondantes seraient instanciées, pour ces valeurs de A et B. Il faut souligner le point de le dernière phrase, il est important : pour les A et B qui seront trouvés, autant d’hypothèses seront instanciées.

L’effet variable et implicite d’un ordre variable, pourrait rendre difficile la lecture des règles. Un exemple avec une écriture fictive où les lettres désignent des termes quelconques :

A : B C ⟦D⟧ E.

À premier vue, c’est à dire sans lecture approfondie (ce qui est toujours le cas le plus fréquent), l’hypothèse D est‑elle censée être après B et C ou seulement après B ou seulement après C ? Ce n’est qu’un exemple simple, en pratique, des situations encore plus illisibles pourraient se présenter.

En résumé jusque maintenant. L’ordre n’a pas d’importance entre les termes, ni entre les hypothèse, mais il en a un entre les termes et les hypothèses et réciproquement. Pour chaque hypothèse, il y a possiblement une relation d’ordre avec chaque terme, et réciproquement. Il serait préférable de poser une convention et de reformuler autrement les règles pour lesquelles l’ordre souhaité n’est pas celui de la convention. Par exemple si on pose que les hypothèse viennent toujours après la tête de la règle mais avant les termes ordinaires du corps de la règle, et qu’on souhaite « A : B & ⟦C⟧ » au lieu de « A : ⟦C⟧ & B », il resterait possible d’écrire une règle B2 pour avoir « A : B2 » et « B2 : ⟦C⟧ ». Ça nécessite de créer d’éventuelles nouvelles relations, mais il est probablement préférable de rendre ainsi lisibles les cas où l’ordre est important. L’avantage serait en fait surtout de ne pas devoir introduire une construction ou une notation spécifique, pour raisonner sur l’ordre des hypothèses par rapport aux termes. Cette préoccupation anticipe le niveau de langage supplémentaire qui finira par être introduit et qui permettra de raisonner sur ce langage objet. Cette préoccupation rejoint celle de la lisibilité immédiate d’une règle.

Ceci clos une justification de la volonté de poser un ordre fixe entre les hypothèses et les termes, en renvoyant vers l’introduction de nouvelles règles dans les cas où cet ordre fixe ne convient pas. Il n’est pas dit pour autant, que ce choix ne pourra pas être remis en question, mais il faudra une bonne raison pour cela.

Reste maintenant à définir ce que doit être cet ordre fixe, lequel serait le plus susceptible de correspondre à ce qui est le plus souvent souhaité, à fin de limiter la nécessité d’écriture de relation ad‑hoc.

On peut réfléchir sur ces trois cas, dont la notation en partie fictive, reflète l’ordre d’instantiation :

⟦(hyp A)⟧ & (head A) : (term A).
(head A) : ⟦(hyp A)⟧ & (term A).
(head A) : (term A) & ⟦(hyp A)⟧.

Dans le premier cas, l’ensemble de la règle est sous hypothèse. Dans le second cas, le corps de la règle est sous hypothèse. Dans le troisième cas, la règle génère seulement, l’hypothèse.

Le troisième cas peut sembler étrange, mais il est censé. Ça n’a pas encore été dit, mais les hypothèses instanciées, sont conservées dans le contexte, aux côtés des liaisons des variables. Donc dans le troisième cas (et les autres aussi), une hypothèse est ajoutée au contexte, si le corps de la règle est vérifié. Cette hypothèse peut vérifier des termes dans d’autres règles. Ce n’est pas insensé, mais ce n’est pas ainsi qu’on comprend le plus immédiatement une hypothèse.

Le premier cas est plutôt encore plus étrange que le troisième, et il est même problématique : si l’hypothèse et la tête de la règle ont une variable en commun, il empêche que cette variable puisse être une variable ordinaire, ce qui est n’est pas une limitation souhaitable, comme expliqué précédemment. Ce cas implique aussi que l’unification avec la tête de la règle, n’est décidable que si les hypothèses sont instanciées en même temps, ce qui est un gâchis, comme le plus souvent cette unification échoue ; cette remarque est plus technique que sémantique. Cette option semble être la plus à exclure des trois.

Dans le second cas, le corps de la règle est sous hypothèse. C’est le cas ressemblant le plus l’utilisation typique d’une hypothèse. Comme le troisième cas est étrange même si pas insensé, comme le premier cas est encore plus étrange que le troisième, le second cas semble être celui à préférer. Il correspond à placer le corps de la règle sous les hypothèses. C’est le cas qui avait d’ailleurs spontanément choisi, avant même d’y réfléchir, tellement il vient naturellement. Ce choix a aussi l’avantage de permettre de facilement fixer une variable pour vérifier une relation sans énumérer ses solutions ou d’échouer immédiatement si ce n’est pas possible, plutôt que de chercher une solution impossible. C’est d’ailleurs cet objectif qui a aboutit à l’introduction d’un type de terme particulier, permettant de représenter des valeurs en général, et qui s’est avéré ressembler beaucoup à la notion courante d’hypothèse. Cela fait assez de bonnes raisons pour préférer cette option plutôt que l’une des deux autres.

Même si un ordre fixe semble avoir été choisi avec une bonne certitude, il peut être intéressant de se demander si le choix d’une option quelconque parmi ces trois, laisse toujours la possibilité d’exprimer les deux autres cas par l’écriture d’une règle ad‑hoc. Cette question devra recevoir une réponse plus tard.

Dans le fragment cité, les conventions désignent l’emplacement permis pour les hypothèses, mais n’imposent pas que des hypothèse se trouvent à ces emplacements. L’ordre des instantiations est celui de l’écriture représentant la convention.

1) À partir de la convention « ⟦(hyp A)⟧ & (head A) : (term A). » :

1.1) On ne peut pas exprimer l’équivalent de « (head A) : ⟦(hyp A)⟧ & (term A). » : A peut être une variable ordinaire, mais la convention fait que la variable d’une hypothèse est toujours liée à une constante spéciale.

1.2) On ne peut pas exprimer l’équivalent de « (head A) : (term A) & ⟦(hyp A)⟧. » : même raison que pour 1.1

2) À partir de la convention « (head A) : ⟦(hyp A)⟧ & (term A). » :

2.1) On peut exprimer l’équivalent de « ⟦(hyp A)⟧ & (head A) : (term A). », par cette réécriture :

(head A) : ⟦(hyp B)⟧ & (eq A B) & (term B). -- B liée à une constante spéciale, au moment de l’instanciation, indépendamment de A.

2.2) On peut exprimer l’équivalent de « (head A) : (term A) & ⟦(hyp A)⟧. », par cette réécriture :

(head A) : (term A) & (term2 A). -- Pas sous l’hypothèse.
(term2 A) : ⟦(hyp A)⟧. -- Mais dépend finalement de l’ordre de vérification.

3) À partir de la convention « (head A) : (term A) & ⟦(hyp A)⟧. » :

3.1) On ne peut pas exprimer l’équivalent de « ⟦(hyp A)⟧ & (head A) : (term A). » : une hypothèse ne peut être générée qu’après la vérification de tous les termes d’une règle, alors aucun terme ne peut contraindre sa variable à être une constante spéciale et si une hypothèse se réfère à une variable, c’est toujours une variable ordinaire.

3.2) On peut exprimer l’équivalent de « (head A) : ⟦(hyp A)⟧ & (term A). », par cette réécriture :

(head A) : (term2 A) & (term A). -- Mais dépend de l’ordre de vérification.
(term2 A) : ⟦(hyp A)⟧. -- Sera sous cette hypothèse.

Contrairement à ce qu’il pouvait sembler à première vue, seul le seconde cas, posé comme convention, permet d’exprimer aussi la même chose que les deux autres cas. Le premier cas ne permet d’exprimer que des hypothèse portant sur des variables liées à une constante spéciale, le troisième cas présente la propriété inverse, les hypothèses ne peuvent en pratique porter que sur des variables ordinaires.

Il serait peut‑être possible de pousser la réécriture plus loin, mais s’il faut passer par des règles servant de point d’entrée, dont la tête n’est pas celle de la règle qu’on veut réécrire, langage n’en serait que illisible.

La seconde option est non‑seulement la plus intuitive, elle est aussi la seule qui n’empêche pas d’exprimer tous les cas : les hypothèses sont instanciées après la tête de la règle et peuvent porter sur les variables de la tête de la règle, les termes ordinaires du corps de la règle sont vérifiés sous ces hypothèses (si applicables) et peuvent porter sur des variables instanciées pour les hypothèses. Les hypothèses peuvent autant porter sur des variables normales que des des variables liées à une constante spéciale, de même pour les termes ordinaires. Si la tête de la règle est censée porter sur des variables liées à des constantes spéciales, il faut ajouter un terme pour l’exprimer indirectement.

Une nouvelle question est apparue, celle de l’importance que peut avoir l’ordre de la vérification des termes, quand ils peuvent générer des hypothèses. Cette remarque amène à reconsidérer la persistance des hypothèses. Ce sera pour le prochain message.

Le résumé prévu devra attendre, comme des choses doivent encore être éclaircies ou corrigées, selon le cas.

Bien que la mise en œuvre des hypothèses telle que testée, est telle que attendue, deux questions se posent. La première est sur la possibilité que les hypothèses portent sur des variables ordinaires, la seconde est sur l’effet de l’évaluation des termes en présence de génération d’hypothèses par des termes.

Dans les exemples donnés précédemment, les variables apparaissant dans les hypothèses sont liées à des constantes spéciales. Ces variables n’ont pas de valeur interprétable par elle‑même. La seule interprétation possible de ces variables est de la forme « n’importe quelle variable V vérifiant le terme (r V) ».

Plus tard est venue une raison de s’interroger sur la pertinence qu’il y a limiter ces variables à être liées à ces constantes spéciales, faisant envisager la possibilité que les hypothèses puissent porter aussi sur des variables ordinaires. La question est initialement venue en constatant que sans cela, certaines instantiations de requêtes peuvent échouer avant même d’avoir évalué le moindre de leurs termes.

D’un côté, on peut se dire que si on peut poser l’hypothèse (r V) où V est une variable ayant une valeur quelconque mais seulement égale à elle‑même, alors il est étonnant de ne pas pouvoir poser la même hypothèse pour une valeur en particulier d’une variable ordinaire. D’un autre côté, si on a une valeur en particulier d’un variable, on peut tester la relation sans hypothèse. Cette question n’est toujours pas décidée.

Notant que l’ordre des hypothèse par rapport à l’ordre des termes peut avoir une importance si on considère que les hypothèses peuvent porter soit sur des variables spéciales soit sur des variables ordinaires, est venue la question de se limiter à un certain positionnement fixe des hypothèses par rapport aux termes, par soucis d’en faciliter la lecture et l’analyse. S’est alors posé la question du meilleur choix pour cet ordre fixe, le bon choix devant permettre d’exprimer les autres cas, même si indirectement. À cette occasion, a été remarqué que les réécritures permettant ces formulations indirectes, sont sensibles à l’ordre de vérification des termes.

Comme les variables liées à une constante spéciale ne sont pas interprétables sans connaitre les hypothèses qu’elles vérifient, il a été spontanément choisit que les hypothèses générées sont liées au contexte, aux côtés des variables liées. Ça semblait naturel et ne pas poser de problème. Mais il s’avère que ça peut en poser un. Soit la séquence de termes A B, si A génère une hypothèse indirectement (par une règle qu’elle désigne), que cette hypothèse est notée dans le contexte, cette hypothèse est alors accessible pendant la vérification de B. Mais ça signifie alors que la vérification de B peut dépendre de la vérification de A, et que alors l’ordre des termes devient important en présence d’hypothèses générées par les termes.

Noter les hypothèse dans le contexte, avec les variables, peut sembler étrange, on pourrait penser à ne laisser persister les hypothèses apparaissant dans une règle que pendant la durée de vérification de la règle, mais ce serait oublier trop vite que ces hypothèses, représentent indirectement la valeur liée à certaines variables, d’où l’idée de les garder dans le contexte.

Soit la requête « ⟦(r A)⟧ & (s A) ?  » : quel est le sens de A si l’hypothèse ⟦(r A)⟧ disparaît avec la fin de la vérification de la requête ? Ou si on considère que l’hypothèse ne doit pas persister au delà de la vérification de la requête et que A n’a pas de sens sans l’hypothèse qu’elle vérifie, alors on peut imaginer que la variable disparaît en même temps que l’hypothèse. Mais qu’en‑est‑il si si une autre variable a été liée à cette variable ? Doit‑elle être oublier aussi ? Mais faire disparaître une variable d’un contexte a‑t‑il seulement du sens ? Garder dans un contexte, une variable que rien permet d’interpréter, est‑il acceptable ?

Peut‑être une solution est‑elle de conserver deux ensembles de ces hypothèses. Un ensemble persistant, aux côtés des variables du contexte et un ensemble non‑persistant pour les hypothèses actives, seulement le temps de la vérification d’une règle. Peut‑être une solution est‑elle aussi d’accepter que l’ordre des termes ait une importance et de ne simplement pas y voir un problème, mais reste à comprendre ce que signifie alors l’ordre des termes, qui serait donc maintenant significatif.

Cette question est encore plus importante que celle de savoir si les hypothèses doivent ou pas pouvoir porter sur des variables ordinaires, bien qu’il faudra aussi répondre à cette question.

Cette question a deux réponses. Une justifiée par une longue raison informelle et une justifiée par une courte raison assez formelle.

Oui, si un terme portant sur une variable ordinaire est vérifiable, alors il n’y a pas besoin d’hypothèse pour le vérifier (ce n’est pas le même cas qu’une variable liée à une constante spéciale). Mais ce n’est pas une raison suffisante pour exclure que les hypothèses puissent porter sur des variables ordinaires. Une hypothèse, pour avoir un sens, doit être ultérieurement démontrée vérifiable, comme ce sera abordé plus tard. Vérifiable ultérieurement, n’implique pas que ça le soit immédiatement. L’hypothèse peut devenir vérifiable après l’ajout d’une règle et avant l’ajout de cette règle, un terme portant sur une variable, peut ne pas être vérifiable autrement que par une hypothèse. L’ajout d’une règle, n’est pas une manière correcte de démontrer qu’une hypothèse est vérifiable, après cet ajout, il faudrait plus tout revérifier que vérifier seulement l’hypothèse, mais ça peut avoir une utilité si on pose des hypothèses pendant une ébauche. Il a aussi été vu que l’absence de cette possibilité, peut aboutir à des comportements non‑souhaitables avec les requêtes, pouvant empêcher leur instantiation. Que l’instantiation n’échoue jamais (pas l’unification, la réalisation d’une copie, avant l’unification), est une propriété appréciable, il est tentant de la préserver. Cette justification a plus des raisons pratiques que formelles.

Mais il y a aussi une raison assez formelle, moins longue à expliquer. Les cas envisagés étaient des hypothèses portant soit sur une variable spéciale soit sur une variable ordinaire, mais il manque le cas des hypothèses portant sur les deux types de variables en même temps. La variable ordinaire peut être sujette à recherche de solutions et autant d’hypothèses être générées, une pour chaque cas de la variable ordinaire avec à chaque fois, la variable spéciale liée à une nouvelle constante distinguant ce cas. Exclure cette possibilité est difficilement justifiable, même si on peut s’inquiéter d’avance du cas où l’ensemble des solutions pour la variable ordinaire, est infini.

Cette question a maintenant une réponse justifiée plus haut : il est décidé que les hypothèses peuvent porter sur des variables ordinaires, pas seulement sur des variables liées à une constante spéciale. En notant qu’il serait possible de ne pas le permettre, mais qu’il semble assez sûr que cette décision finirait pas être regrettée.

Une réponse est apparue ou plutôt un choix entre deux options. La réponse ne sera donnée qu’après sa justification. Cette justification sera plus claire en répétant des choses déjà dites. Une distinction pas encore faite jusque maintenant, doit être introduite.

Jusque maintenant, quand il était question de contexte, c’était en pensant à l’ensemble des liaisons entre les variables et leur terme ou autre variable associé(e). Ce contexte sera appelé le contexte de la vérification, dans le reste de ce message. Il existe un autre contexte, que j’appelles le contexte syntaxique, ne voyant pas une autre expression plus appropriée. Ce contexte syntaxique, c’est celui des règles et de l’expansion des termes, en les substituant par les règles qu’ils désignent. Par exemple soit la règle « A : B C », et les deux règles « B : D E » et « C : F G », quand « D E » et « F G » sont insérées dans la règle A parce que B et C s’y réfèrent, elles sont dites ici, dans le contexte syntaxique de la règle A. Ce contexte est différent de celui notant les associations des variables. Si le terme D implique une liaison, disons entre une variable X et une variable Y, cette liaison fait partie du contexte résultant de la vérification de B (comme « D E » résulte de B) et cette liaison fera donc aussi partie du contexte dans lequel sera vérifiée C et donc aussi F et G. Il en va autrement du contexte syntaxique, la formulation ou le texte, qui a impliqué la liaison entre X et Y, ne se trouve pas dans le contexte syntaxique de F ou G, seulement dans celui de D et de B et de A et de l’éventuelle règle se référant à A.

Si on se replace dans la situation d’avant l’introduction des hypothèses, dans la règle « A : B C », l’ordre pourrait être « C B » aussi bien que « B C », ça ne fait pas de différence logique (c’est à dire pour la vérifiabilité) même si ça fait une différence pratique. Ça ne fait pas de différence logique, parce que le contexte de vérification qui vérifie C, vérifie aussi B et réciproquement. L’ordre ne change que les étapes avec lesquelles il est construit, mais le résultat est le même, les deux chemins convergent vers la confirmation des deux ou l’échec de la vérification simultanée des deux.

Si B implique ou nécessite (c’est la même chose, ici) une liaison entre X et Y, et que C implique aussi une liaison entre X et Y, chacun à leur manière, l’ordre dans lequel on le vérifie ne change rien à cette nécessité. La nécessité de cette liaison peut être posée dans le contexte par B via le terme D, le terme C se satisfera de cette exigence ou pas. La même chose dans l’autres sens, de C vers B, C peut d’abord poser cette nécessité dans le contexte, via F par exemple, et B s’en satisfaire ou pas. Dans les deux cas, le résultat est le même.

F n’est pas dans le contexte syntaxique de D, et réciproquement, mais les deux termes disent la même chose concernant la liaison entre X et Y. Le contexte de la vérification note les deux et confirme la satisfaction simultané des deux (ou pas).

Le point important est « disent la même chose », en étant pourtant séparé.

Si on ne parle maintenant plus d’une liaison entre X et Y, mais d’une hypothèse sur une variable, disons Z. Imaginons que la relation qui est affirmée, n’est pas vérifiable autrement que par cette hypothèse. Cette fois, D et F ne peuvent pas toujours dire la même chose. Si l’hypothèse porte sur une variable ordinaire, D et F peuvent poser la même hypothèse, mais si l’hypothèse porte sur une variable liée à une constante spéciale, la constante spéciale ne pourra pas être la même dans les deux cas : le texte de l’hypothèse pourra bien être le même dans D et F, l’hypothèse instanciée par D ne pourra pas correspondre à celle instanciée par F et réciproquement, ce qui signifie que les deux hypothèse ne pourront pas vérifier les mêmes termes. On peut au passage noter que le problème ne se pose qu’avec les variables liées à une constante spéciale, que D et F peuvent quand‑même dire la même chose même s’ils posent indépendamment une hypothèse, à condition que cette hypothèse ne porte que sur des variables ordinaires.

Donc, D et F ne peuvent pas poser la même hypothèse portant sur une variable liée à une constante spéciale. Pourtant, F peut accéder à l’hypothèse produite pas D, comme elle est laissée dans le contexte (un retour sur ce point, sera fait plus loin), mais seulement si F est vérifiée après D. S’il est tenté de vérifier F avant D, et que F ne peut pas vérifier un certain terme sans cette hypothèse, la vérification de F puis de D, échouera, alors que la vérification de D puis de F, pourrait être faite avec succès.

Ce n’est pas sans solution, F et D peuvent avoir accès à la même hypothèse portant sur une variable spéciale, sans qu’elle ne soit produite par aucun des deux. Si cette hypothèse est produite dans le contexte syntaxique de A, la même instance est disponible pour D et pour F, quelque soit l’ordre dans lequel on les vérifie. Ceci, sous réserve que rien n’empêche de formuler la même hypothèse que celle qui était formulée dans le contexte syntaxique de D, mais dans le contexte syntaxique de A. Je ne vois pas de cas où ce ne serait pas possible, mais il faut noter cette question.

De cette manière, l’ordre des termes dans une règle reste sans importance. La seule condition est que D ou F ne soit pas vérifiée avant que A ne soit instanciée ; cette question ne se pose même pas, ça n’aurait pas de sens.

Cependant, le cas où l’hypothèse est posée par D n’est pas incorrecte (retour sur ce point, plus loin), c’est seulement qu’il rend la règle A, sensible à l’ordre des termes. Comme il est supposé (jusqu’à preuve du contraire, et je ne crois pas à une preuve du contraire à priori) que cette hypothèse peut aussi bien être formulé dans A, l’idée est d’exiger qu’elle soit formulée dans A. C’est l’objet de ce qui vient maintenant.

Comment exiger que l’hypothèse dont dépend à la fois D et F, ne soit formulée que de manière à être accessible au deux quelque soit l’ordre ? Une réponse a déjà été donnée implicitement, elle est rappelée explicitement ici. Jusque maintenant, les hypothèses générées étaient notées dans le contexte de la vérification, puis quand un terme doit être vérifiée, avant de chercher une règle correspondante, les hypothèses présentes dans le contexte de la vérification, étaient d’abord testées. Cette manière de faire est à l’origine de la dépendance à l’ordre, comme vu plus haut. Mais, comme on le verra plus loin, il est nécessaire de continuer à conserver les hypothèses dans le contexte de la vérification, mais ça n’implique pas que les hypothèses correspondantes soient obligatoirement recherchées dans le contexte de la vérification. Il est possible de noter les hypothèses, dans le contexte syntaxique, aussi, elles sont alors oubliées par ce contexte quand il se termine. Par exemple, quand la règle A discutée plusieurs fois plus haut est vérifiée, les hypothèses éventuellement définies dans cette règle, sont oubliées par le contexte syntaxique (mais toujours conservées par le contexte de la vérification). Les hypothèses sont notées dans le contexte de la vérification et dans le contexte syntaxique, et la recherche d’une hypothèse correspondante à un terme, ne se fait qu’en consultant les hypothèses présentes dans le contexte syntaxique.

De cette manière, si l’hypothèse est définie dans A, elle est accessible à la fois à D et à F. Si elle est définie dans D, elle n’est pas accessible à F, qu’il soit tenté de vérifier F, avant ou après D. On constante que l’ordre n’a plus d’importance : soit il y a échec de la vérification des deux ensemble, quelque soit leur ordre, soit les deux peuvent être vérifiés ensemble, quelque soit leur ordre. En oubliant pas encore une fois, que ceci est sous réserve que l’hypothèse formulée dans D, puisse être formulée dans A. J’en suis convaincu, mais comme la question ne doit pas être oubliée, je vais opter pour une solution permettant d’avoir les deux comportements, d’après une option. Ainsi, il sera toujours possible de faire des comparaisons, au cas où.

En parlant de cette option, une petite astuce peut être intéressante, mais elle n’a « qu’une » importance pratique, pas une importance logique : l’hypothèse peut être cherchée dans le contexte de la vérification, puis ensuite vérifier si elle est présente dans le contexte syntaxique. Si elle n’est pas présente dans le contexte de la vérification, elle n’est mécaniquement pas présente dans le contexte syntaxique et alors aucune hypothèse correspondante n’est trouvée. Si une hypothèse correspondante est trouvée dans le contexte de la vérification, mais pas dans le contexte syntaxique, il est considéré que aucune hypothèse correspondante n’a été trouvée, mais un message peut être affiché pour dire qu’une certaine hypothèse, en la désignant, a été trouvée, et qu’elle devrait être placée dans un contexte syntaxique plus englobant. La logique de la vérification serait la même, mais avec l’avantage pratique d’un diagnostique pouvant être utile.

Le message suivant, reviendra sur la question de la nécessité de conserver les hypothèses dans le contexte de la vérification, et pourquoi il ne serait pas incorrecte de les chercher là, malgré que ça rende les règles sensibles à l’ordre de leurs termes. Il ne faut en effet pas oublier que c’est une raison pratique, qui a fait ici opter pour une variante préservant la non‑importance de l’ordre des termes. Ce choix est justifiée par trois choses : il est espéré que la non‑importance de l’ordre facilite la lecture des règles et aussi la formulation de leur analyse, et il est supposé avec une bonne conviction, qu’il est toujours (ou presque ?) possible de déplacer les hypothèses dont l’emplacement ne serait pas conforme (pour permettre que les règles ne soient pas sensibles à l’ordre des termes), ce qui fait supposer que ce choix ne limite pas ce qui peut être exprimé.

Des exemples seront plus parlant.

Soit ces deux ensembles de règles, où la notation ⟦T⟧ signifie que le terme T est introduit comme hypothèse :

#1 (eq A A).
#2 (r1 A) : ⟦(h B)⟧ & (eq A B) & (h A).
#3 (r2 A) : (h A).
#4 (r3 A) : (r1 A) & (r2 A).

et

#1 (eq A A).
#2 (r1 A) : ⟦(h B)⟧ & (eq A B) & (h A).
#3 (r2 A) : (h A).
#4 (r3 A) : (r2 A) & (r1 A).

La seule différence entre les deux, est que dans la règle #4, le deux termes r1 et r2, sont permutés.

Cette requête est testée pour chacun des deux cas de règles :

(r3 A) ?

Si les hypothèses sont recherchées dans le contexte de la résolution, le résultat avec le premier ensemble de règle, est :

#4 #2 #1 H#1 #3 H#1
A = Abs#1

Avec le second ensemble de règles, la résolution échoue. Comme expliqué précédemment, mais maintenant illustré avec ces exemples. La raison est que dans le second ensemble de règles, r2 est vérifié avant r1, l’hypothèse h n’existe donc pas pour r1, comme elle est générée par r2.

On constate comme précédemment décrit, que si les deux termes r1 et r2 de la règle #4, sont permutés, la résolution échoue. Cette règle est sensible à l’ordre des termes, pour les raison précédemment expliqué est illustrées ici. Cette dépendance à l’ordre des termes est vue comme un problème, un problème pratique, pas un problème logique, mais considéré comme assez sérieux (ça nuit à la lecture des règles, au moins) pour vouloir ne pas l’accepter.

Si les hypothèses sont recherchées seulement dans ce qui a été appelé le contexte syntaxique, la résolution échoue dans les deux cas, même dans le premier. Même dans le premier, mais avec un message (qui n’est pas formellement nécessaire), indiquant qu’une hypothèse existe dans le contexte (sous entendu, le contexte de la résolution), mais qu’elle est hors de portée.

Cette fois donc, il n’y a plus de dépendance à l’ordre des termes, les deux cas échouent. Ça peut sembler étrange de préférer que les deux cas échouent, mais ça ne l’est pas, parce que les règles vont être réécrites de manière à qu’elles n’échouent pas, même en permutant r1 et r2. Il est supposé qu’il doit toujours être possible de re‑écrire les règles de manière à ce qu’elles ne soient pas dépendantes de l’ordre des termes ; ceci, en faisant remonter les hypothèses à un niveau syntaxique plus englobant (désolé pour l’expression utilisée, si elle n’est pas appropriée).

Les deux ensembles de règles peuvent être réécrits de cette manière :

#1 (eq A A).
#2 (r1 A) : (h A).
#3 (r2 A) : (h A).
#4 (r3 A) : ⟦(h B)⟧ & (eq A B) & (r1 A) & (r2 A).

et

#1 (eq A A).
#2 (r1 A) : (h A).
#3 (r2 A) : (h A).
#4 (r3 A) : ⟦(h B)⟧ & (eq A B) & (r2 A) & (r1 A).

La différence avec les deux premiers ensembles de règles, est que l’hypothèse h, qui se trouvait dans la règle r1, a été remontée au niveau de la règle r3. Comme juste précédemment, pour le second ensemble de règles, les termes r1 et r2 de la règle #4, sont permutés.

Pour le premier cas, la requête « (r3 A) ? » renvoi cette résolution :

#4 #1 #2 H#1 #3 H#1
A = Abs#1

Pour le second cas, elle renvoi cette résolution :

#4 #1 #3 H#1 #2 H#1
A = Abs#1

La seule différence est dans la chaîne d’inférences, comme deux termes ont été permutés.

Ce qui est important, c’est que la permutation des deux termes ne fait plus échouer la règle r3. Pour cela, l’hypothèse a été remonté. Si l’hypothèse existe mais n’est pas accessible, la règle échoue quelque soit l’ordre des termes, comme vu plus haut.

S’il est toujours possible de remonter les hypothèses de la même manière que dans cet exemple simple, alors il n’y a pas de problème à exiger par choix, que les règles soient écrites de manière à ne pas devenir dépendantes de l’ordre des termes à cause des hypothèses.

Deux messages annoncés sont toujours en attente. L’un, qui devait revenir sur la raison de conserver les hypothèses dans le contexte de la résolution, est mis en attente en attendant d’éclaircir une question restante à propos des hypothèses portant sur les variables normales. L’autre message qui devait résumer la genèse de l’introduction des hypothèses, ici, ne viendra qu’après.

Les deux messages en attente, sont toujours en attente, mais ce message annonce la venu prochaine de l’un des deux, autant que quelque gouttes, annonce souvent la pluie. Le nuage en question, est une brume : encore une difficile question de notation à introduire, par nécessité.

Ce n’est pas pour faire la peinture avant d’avoir maçonné les murs, parce qu’ils le sont en cachette sans rien dire ; sans rien dire, parce qu’ils ne sont pas encore finis.

D’abord, il n’avait pas encore été expliqué pourquoi la notation ⟦H⟧ a été choisie pour dire que le terme H est posé comme hypothèse. La raison vient d’une notation dans la déduction naturelle, qui utilise les crochets [ et ] pour noter les hypothèse, mais ces crochets sont déjà utilisés pour une notation qui ne sera pas présentée ici (ça n’a pas d’intérêt général pour le sujet). La déduction naturelle note aussi trois points de suspensions verticaux en dessous, pour signifier « la décharge de la preuve », ce qui est une manière que dire que le raisonnement est purement hypothétique. Ici, on ne se décharge pas de la preuve, ce sujet est biaisé depuis le début, il a un biais constructiviste : tout ce qui est tenu pour vrai doit être réalisable et si ça ne l’est pas, réalisable, alors ça n’est pas vrai, non‑plus.

Reste donc maintenant à poser une notation pour dire qu’on s’assure qu’un terme posé en hypothèse est effectivement réalisable.

Comme la notation des hypothèses a été inspirée de la déduction naturelle, on pourrait penser à garder cette source d’inspiration et utiliser les points verticaux. Mais comme on écrit les formules comme du texte, en lignes horizontales et non‑pas verticalement, peut‑être qu’on pourrait aussi voir de quoi ont l’air les trois points horizontaux. Il existe plusieurs variantes de ces caractères dans le standard Unicode.

Par exemple pour dire qu’on s’assure que (nat N) est un terme effectivement vérifiable, après l’avoir posé en hypothèse, on pourrait éventuellement écrire, au choix :

• ⋮(nat N)
• ︙(nat N)
• ...(nat N)
• …(nat N)
• ⋯(nat N)
• (nat N)∎

Le dernier est un intrus. Il existe dan Unicode, un caractère nommé QED, signifiant « ce qu’il fallait démontrer », mais je le trouve problématique ici, parce qu’il est une marque de toute‑fin alors que les vérifications de termes peuvent devoir être en nombre.

Les points verticaux ne sont pas jolis, probablement parce que le reste de l’écriture est horizontale. Il reste les points horizontaux. Ceux s’affichant sur le milieux de la hauteur de la ligne, ont un air trop dur, c’est subjectif, mais il faut faire un choix. Reste les deux autres options. L’une est simplement trois points normaux à la suite, l’autre est un caractère Unicode appelé ellipsis. Les points normaux à la suite pourraient être une notation synonyme, par commodité, quand le caractère ellipsis ne peut pas facilement être écrit au clavier. En marge, au lieu de ⟦H⟧, il serait possible d’écrire aussi [|H|] comme synonyme plus facile à entrer au clavier (ça lasse, les copier‑coller de caractères), ce qui n’empêche pas une conversion automatique vers les caractères préférés, à l’occasion de l’affichage.

Pour revenir aux vérifications de réalisibilité des hypothèses, il y aurait une autre option, ce serait celle de les noter comme une requête. Par exemple noter « (nat N)? » pour dire qu’on s’assure que (nat N) est effectivement réalisable. Cette notation est tentante, elle est évocatrice (dans le contexte de ce sujet et même en dehors) et la vérification qu’une hypothèse est réalisable est effectivement la même chose qu’une requête de cette forme. Reste que c’est trompeur, comme le point d’interrogation est déjà utilisé pour les requêtes.

C’est moins trompeur si on associe cette idée avec celle plus haut, pour avoir cette notation : « …(nat N)? ». On retrouve bien les trois points de la décharge de la preuve, à gauche, parce que la preuve a été omise jusqu’au point mentionné et on retrouve le symbole de la requête qui signifie qu’on vérifie quelque chose, mais avec tout de même le symbole ellipsis qui aide à éviter que le point d’interrogation n’ai l’air trop ambiguë à la lecture. Pour précision : il est prévu qu’il n’y ait pas d’espaces entre « … » et la parenthèse ouvrante ni entre le point d’interrogation et la parenthèse fermante. C’est comme si les deux caractères étaient assemblés pour former un seul symbole. Du coup, la notation pour les requêtes nécessite que le point d’interrogation soit précédé d’un espace s’il suit une parenthèse, ce qui est souvent le cas ; ça ne devrait pas poser un problème.

La notation « …(nat N)?  » se lirait intuitivement comme « on a supposé que (nat N) … mais attend, (nat N)? », pour dire qu’on voudrait quand‑même bien s’en assurer.

Tout ça pour dire qu’une nouvelle notation est introduite : là où ⟦H⟧ signifie que H est posé comme une hypothèse, …(H)? signifiera qu’on s’assure que H est effectivement réalisable. Pourquoi et comment, … ce sera l’objet d’un prochain message.

À moins que mieux ne soit trouvé … mais il faut bien avancer.

Une précision le sens des hypothèses posées dans une règle, avant, dans le même message, d’aborder la question de la vérification des hypothèses.

Dans la règle «  (r A) : ⟦(h A)⟧ & (r2 A). », la variable A n’est pas liée à une constante spéciale, elle est une variable ordinaire. Dans la règle
«  (r B) : ⟦(h A)⟧ & (r2 A B). », A est une variable spéciale. La différence est que dans le premier cas, la variable sur laquelle porte l’hypothèse, apparaît dans la tête de la règle, alors que dans le second cas, elle n’apparaît pas dans la tête de la règle et est donc une variable posée dans la règle. Cette variable est immédiatement liée à une constante spéciale quand elle est créée. Dans la règle, «  (r A) : ⟦(h A)⟧ & (r2 A). », si la variable A est liée à rien, c’est à dire à Any, il serait en principe possible aussi de lier A à une constante spéciale créée pour l’hypothèse, comme on peut toujours lier une variable « libre » à n’importe quelle valeur. Mais cette option est exclue, parce que le sens de l’hypothèse changerait selon les cas. Par exemple, selon que la règle en question est invoquée avant ou après un terme fixant A, le sens ne serait pas le même. Ce serait une cause de dépendance à l’ordre des termes, et par choix, ces cas sont exclus. Pour cette raison, si la variable sur laquelle porte une hypothèse apparaît dans la tête de la règle, l’hypothèse porte toujours sur une variable normale, elle porte sur une variable spéciale créée par la règle, dans le cas contraire.

Pour comprendre ce qui est dit dans le paragraphe précédent, il faut se souvenir que les hypothèses sont toujours posées après la tête de la règle et avant les autres termes du corps de la règle. C’est ainsi par choix, pour des raisons qui ont été expliquées. C’est en tous cas pour cette raison que les explications du précédent paragraphe, ne mentionnent que les variables apparaissant dans la tête de la règle, qui sont les seules importante à cet égard.

Comme vu plus haut, dans l’hypothèse ⟦(nat N)⟧, N peut être une variable spéciale ou une variable ordinaire. Dans le premier cas, ⟦(nat N)⟧ pose un N tel que (nat N) tout‑court, est vérifié. Cette affirmation n’a de sens que s’il existe au moins un tel N. Dans le second cas, ⟦(nat N)⟧ affirme que (nat N) est vérifiée pour la variable N, sans rien dire de ce qu’elle désigne. Cette affirmation n’a de sens que si (nat N) tout‑court est vérifiable, pour le N donné. Quel est ce N donné ? Ce qui vient aborde cette question.

À la vu du terme (r A), quel est la valeur de A ? Si le terme est vérifié, c’est un A vérifiant (r A). Si le terme n’est pas vérifié, la question ne se pose pas, A n’existe pas ailleurs que dans le texte du terme. Mais (r A) ne dit peut‑être pas tout de la valeur de A. Si dans une règle on a (r1 A) & (r2 A), la variable A est telle qu’elle vérifie les deux termes en même temps. Mais si ces deux termes apparaissent dans une règle qui est elle‑même invoquée par un terme d’une règle dont un des termes porte sur A directement ou indirectement, alors c’est cette règle qui en invoque une autre, qui en dit plus sur A, et ainsi de suite, jusqu’à finalement l’origine, qui est la requête actuellement vérifiée.

Il est possible que A soit déterminée seulement par un seul terme d’une certaine règle, par exemple, mais on ne peut pas le savoir à priori. La seule chose certaine est que toute variable normale apparaissant dans quelque règle que ce soit, n’a une valeur qui peut être considérée comme fixée, que quand la requête a été vérifiée en totalité.

Ça peut sembler étrange dit comme ça, mais quand on voit (r A), la terme peut être vérifié alors que la valeur de A n’est pas connue ou pas totalement connue. C’est moins mystérieux si on se souvient comme dit précédemment, que le terme (r A) participe à la définition de la valeur de A, comme les autres termes, est qu’une règle ou une requête échoue si jamais ce que dit un terme d’une variable ne peut pas être en accord avec ce qu’en disent les autres termes.

Donc, la valeur d’une variable est considérée comme inconnue ou seulement partiellement connue, jusqu’à la fin de la vérification de la requête, si encore la requête est vérifiée.

Ça a une importante pour la vérification de certaines hypothèses. Si une hypothèse porte sur A, l’hypothèse ne peut pas être démontrée avant que la vérification de la requête n’ait été achevée, car pendant tous le temps de la vérification de la requête, sa valeur n’est pas encore connue ou pas entièrement.

Si une hypothèse porte sur une variable spéciale, c’est différent. La variable spéciale est immédiatement liée à une constante et comme toute variable liée à une constante, si un autre terme en dit autre chose, ils sont en contradiction, l’ensemble pas vérifié, par là toute la règle dans laquelle ils apparaissent, en cascade jusqu’à peut‑être la requête elle‑même, s’il n’y a pas de règle alternative pouvant être vérifiée. Un terme qui le contredit, n’est pas vérifié.

Donc la valeur d’une variable spéciale peut être considérée comme connue dès sa création ou comme n’existant pas, car si la règle dans laquelle elle est posée, n’est pas vérifiée, la variable disparaît.

Ça fait une différence importante pour la vérification des hypothèses portant sur une variable spéciale : à priori, l’hypothèse pourrait être vérifiée aussi tôt après avoir été posée. C’est à l’opposé de ce qu’il en est avec les hypothèses portant sur des variables ordinaires. Mais un autre choix est fait, qui sera expliquée.

On voit déjà à quel point une hypothèse portant sur une variable ordinaire, ne peut pas être abordée comme une hypothèse portant sur une variable spéciale.

Il y a une autre différence si on se remémore ce qui a été dit juste précédemment, sur la nature de la vérification en elle‑même.

Pour vérifier une hypothèse sur une variable ordinaire, on vérifie l’hypothèse en temps que terme tout‑court, avec la variable dont la valeur est connue. Pour vérifier une hypothèse sur une variable spéciale, on chercher au moins une solution à l’hypothèse en temps que terme tout‑court.

Respirez quelques secondes avant de lire la suite, prenez un peu le temps d’imaginer ce que peut signifier, pour en prendre conscience par vous‑mêmes.

Une chose intrigante : pendant qu’on vérifie l’hypothèse sur la variable ordinaire, ce qui était une variable, est à ce moment là, comme une constante, et pendant qu’on vérifie l’hypothèse sur la variable spéciale liée à une constante, elle devient à ce moment là, une variable ordinaire. C’est mystérieux et intriguant … il doit y avoir un sens caché là dessous. Pourtant c’est ainsi, il ne peut pas en être autrement ou je ne vois pas.

Note : une variable peut toujours être liée à Any, même après la vérification d’une requête, ou elle peut être liée à un terme contenant des variables liées à Any. Dans ce cas, la variable n’est pas vraiment comme une constante, mais disons que sa valeur est fixée. Est‑il nécessaire de fixer ces liaisons à Any par une constante au moment de la vérification de l’hypothèse ? Je ne crois pas, comme quoiqu’il en soit, la vérification de l’hypothèse, si elle est en contradiction avec ce que les termes de la requête ont dit de la valeur de la variable, alors cette vérification de l’hypothèse échouera. Ça signifie quand‑même que à priori, la vérification de l’hypothèse pourrait lier ces points liés à Any, à autre chose. On peut tout de même se poser la question de ce que ça pourrait impliquer. Une réponse vient immédiatement si on considère la vérification de l’ensemble des hypothèses devant être vérifiées, comme une séquence de termes, alors on peut dire que l’ensemble de ces termes doivent être en accord sur la valeur de cette variable et que dans le cas contraire, la vérification des hypothèses échoue.

La dernière phrase du précédent paragraphe implique que si la vérification d’une hypothèse d’un ensemble d’hypothèses, échoue, alors la vérification de l’ensemble des hypothèses, échoue. Cette sémantique est encore accord avec celle du langage objet sur lequel on se base.

Si on ne peut pas vérifier une hypothèse portant sur une variable ordinaire avant la fin de la requête, alors certaines réponses renvoyées par le langage objet défini ici, ne sont pas interprétables, et pour être interprétables, le résultat de la requête doit passer par un autre traitement, ce qui commence à nous faire entrer dans un autre niveau de langage. On peut vouloir ne pas l’accepter. Pour cette raison, il peut être utile de prévoir une option spécifiant que les hypothèses portant sur des variables ordinaires, ne sont pas acceptées. Ça peut se déterminer syntaxiquement, comme expliqué plus haut.

On peut vérifier une hypothèse portant sur une variable spéciale, à n’importe quel moment à priori. En fait, on pourrait même la démontrer avant même de la poser, mais ce serait des complications inutiles pour la formulation du langage. On peut en tous cas la démontrer aussi tôt après l’avoir posé, plus tard après l’avoir posé ou après la vérification de la requête, comme avec les hypothèses portant sur les variables ordinaires. La même remarque sur l’interprétation du résultat d’une requête, s’applique avec ces hypothèses, mais au lieu de n’avoir comme seul option que de les rejeter, on peut aussi exiger qu’elles soit vérifiées. Pour une telle option, un moyen d’exiger qu’elles soient vérifiée, est d’exiger que ce soit fait dans la règle même où l’hypothèse est posée. Les autres manière de l’exiger ne serait pas syntaxiquement déterministe. Comme on a vu plus haut, qu’au moment de la vérification d’une telle requête, sa variable qui est comme une constante, devient une variable ordinaire, il peut être préférable de le faire à la fin du corps de la règle, pour que la lecture de la règle n’en devienne pas étrange. En effet, si l’hypothèse est déclarée, d’abord avec une variable spéciale, puis démontrer, avec une variable ordinaire, voir cette variable apparaître dans le corps de la règle, de nouveau avec un status de variable spéciale, pourrait une sensation d’inconstance, à la lecture.

Si une option exige que les hypothèse portant sur des variables spéciales, soient vérifiées, on peut vérifier syntaxiquement que le texte d’une règle le formule effectivement. En reprenant la notation proposée précédemment, on aurait par exemple « (r1 A) : ⟦(nat N)⟧ & (r2 A N) & …(nat N)? ». Le moyen le plus simple de s’assurer qu’une vérification d’hypothèse correspond bien à une hypothèse posée, est d’exiger que le terme soit le même. Par exemple ici, cette écriture considéré comme non‑valide, parce que le N est remplacé par un X : « (r1 A) : ⟦(nat N)⟧ & (r2 A N) & …(nat X)? ».

En marge, je ne suis pas satisfait de la notation « …(nat N)? », il faudrait trouver autre chose .

S’il est important de conserver les hypothèses dans le contexte, ce n’est pas seulement pour savoir à quoi correspondent certaines variables, et d’ailleurs ça ne s’appliquerait qu’aux variables spéciales, c’est aussi pour avoir la liste des hypothèses devant être vérifiées, pour que le résultat de la requête ait un sens. Dans le cas des hypothèses portant sur des variables spéciales qui seraient vérifiées dans le corps même de la règle, les hypothèses devraient quand‑même être conservées pour savoir à quoi correspondent les variables qui leur correspondent, mais ces hypothèses seraient marquées comme vérifiées.

Quand après avoir posé l’hypothèse ⟦(nat N)⟧, on vérifie l’hypothèse en vérifiant que le terme (nat N) a bien au moins une solution, ça ne peut se faire qu’en re‑instanciant le terme, pour que le N du terme vérifiant l’hypothèse, soit une nouvelle variable. Aucun terme ordinaire ne doit pouvoir se référer à cette variable.

Quand une hypothèse porte à la fois sur des variables spéciales et sur des variables ordinaires, elle ne peut que être traitée comme une hypothèse portant sur des variables ordinaires, surtout parce que les variables ordinaires font que l’hypothèse ne peut pas être vérifiée avant que la requête n’ait été vérifiée. Dans ce cas, pour la vérification, les variables spéciales deviennent des variables ordinaires, comme expliqué précédemment : il faut qu’il existe au moins une valeur pour la variable spéciale, qui vérifie le terme, étant donné la variable ordinaire, à ce moment là fixée, qui l’accompagne.

Quand une variable ordinaire apparaît dans plusieurs hypothèses, rien de spécial, toutes les hypothèses seront vérifiées avec la définition finale de la variable.

Quand une variable spéciale apparaît dans plusieurs hypothèses, c’est plusieurs occurrences de la même variable. Les hypothèses concernées doivent être vérifiées ensemble comme une conjonction, il n’y a pas d’autres solutions. Après une précédente remarque, ça souligne encore qu’on vérifie un ensemble d’hypothèses, plus qu’une hypothèse. Dans le cas d’une variable spéciale ayant plusieurs occurrences à travers plusieurs hypothèses, ces hypothèses ne peuvent que être déclarées dans la même règles, l’ensemble des hypothèses à vérifier est connu.

Le cas des variables ordinaires liés à une variable elle‑même liée à une constante spéciale, est une question encore en suspend.