Les logiques : notes en vrac

L’autre option précédemment envisagée, ne se lirait pas mieux :

(r1 A) : ⟦(nat N)⟧ & (r2 A N) & ︙(nat N).
vs
(r1 A) : ⟦(nat N)⟧ & (r2 A N) & …(nat N)?.

Il faut trouver une autre idée pour la notation, ça ne va pas.

En abandonnant l’idée de choisir des symboles évocateurs, noter ⟅(nat N)⟆ pour la vérification de l’hypothèse, ne serait pas trop désagréable à la lecture.

Le précédent exemple ressemblerait à :

(r1 A) : ⟦(nat N)⟧ & (r2 A N) & ⟅(nat N)⟆.


C’est à voir, ce n’est pas l’essentiel, qui est pour le moment le sens, mais c’est nécessaire, parce que sans notation, rien n’est possible en pratique. Heureusement qu’il n’y aura pas d’autre distinction de terme à apporter à ce niveau de langage.

On vérifie des hypothèse ensemble, mais on peut au moins parfois, partitioner cet ensemble, d’après les dépendances des hypothèses entre elles. Dans le cas des hypothèse portant sur une variable spéciale, c’est possible. Mais ce n’est à priori pas possible en général avec des hypothèses portant sur des variables ordinaires (une hypothèse portant sur les deux types de variables, est traitée comme si elle portait sur des variables ordinaires, pour ce qui est du moment auquel sa vérification peut être posée), comme on ne peut pas prédire d’après l’écriture, si ces hypothèses sont liées ou pas du fait d’une variable. Les hypothèses portant sur des variables normales, qui ne peuvent être vérifiées qu’après la vérification de toute la requête, doivent être considérées comme toutes interdépendantes à priori, car étant donné deux variables normales, A et B, et deux hypothèses ⟦(h1 A)⟧ et ⟦(h2 B)⟧, la seul lecture du texte, ne permet pas de savoir si A et B sont liées entre elles indirectement. Il n’en va pas de même avec les variables spéciales. Étant données deux variables spéciales A et B, ⟦(h1 A)⟧ et ⟦(h2 B)⟧ peuvent être vérifiées séparément, car A et B, ne peuvent pas être interdépendantes (les valeurs des variables), l’unification ne le permet pas, comme elles sont liées chacune à une constante spéciale. On pourrait vérifier ⟦(h1 A)⟧ et ⟦(h2 B)⟧ séparément, mais comme on peut aussi avoir une seule variable spéciale A, et deux hypothèses ⟦(h1 A)⟧ et ⟦(h2 A)⟧, dans ce cas il est nécessaire de vérifier la conjonction des deux. Cette interdépendance qui cette fois ne doit rien aux valeurs des variables, mais à leurs occurrences, peut se déterminer syntaxiquement. Mais pour rester simple, il est préférable de considérer que un ensemble de vérification d’hypothèses est toujours vérifié comme une conjonction. Il faut tout de même pouvoir déterminer l’interdépendance dans ce cas, au moins pour que poser la vérification de ⟦(h1 A)⟧ sans poser la vérification de ⟦(h2 A)⟧, soit rejeté. Ce n’est pas un problème, comme c’est syntaxiquement déterministe, il n’y a même pas besoin d’évaluer quoique ce soit, juste analyser le texte de la règle.


Étant donné qu’une variable spéciale est définie comme n’importe quelle valeur vérifiant une hypothèse, une variable ordinaire liée à une variable spéciale, devrait être vérifiée en choisissant une valeur avec laquelle la vérifier.

Par exemple si A est une variable spéciale, définie par l’hypothèse ⟦(h1 A)⟧ et que B est une variable ordinaire, que après la résolution de la requête il s’avère qu’elle est liée à A, que la requête ⟦(h2 B)⟧ doit être vérifiée, il faut choisir un B parmi les valeurs possibles de A, et vérifier ⟦(h2 B)⟧ avec cette valeur. Ou encore, on peut vérifier la conjonction (h1 A) & (h2 A). On pourrait penser que ça signifie que A est re-posée à nouveau, cette fois comme un A vérifiant (h1 A) & (h2 A) au lieu d’un A vérifiant (h1 A). Ça n’est pas le cas, parce que A reste définie comme n’importe quelle valeur vérifiant (h1 A), et c’est seulement la vérification de (h2 B) qui s’avère devoir être une vérification de (h1 A) & (h2 A). On pourrait aussi se dire qu’il est inutile de démontrer séparément que (h1 A) est vérifiable, si on doit au final démontrer (h1 A) & (h2 A). Mais ⟦(h1 A)⟧ aura put être posée et vérifiée dans la règle même où elle a été posée, comme vu précédemment.

Concernant le dernier paragraphe du précédent message, il est quand‑même plus simple de considérer que toutes les hypothèses restantes dans le contexte après la vérification d’une requête, doivent être vérifiées comme une conjonction. Ce qui est discuté dans le précédent paragraphe n’est pas strictement nécessaire, mais donne un sens aux choses discuter. Reste que formellement, la vérification des hypothèses devra se faire en les vérifiant toutes, sinon, il y a échec général et le résultat de la requête n’est pas interprétable. Il ne faut pas confondre les deux niveaux de préoccupation.

L’alpha‑équivalence n’existe pas dans le formalisme du Prolog de base qui est la base du langage objet discuté ici. Elle serait pourtant utile pour quelque chose qui sera dit un peu plus tard. Mais on peut introduire l’alpha‑conversion en restant assez dans les termes de ce langage objet.

Ça devrait être démontré, mais cette description devrait être assez convaincante :

Soit deux termes tout juste instanciés, toutes leurs variables liées à Any et liées à aucune variable. Si les deux termes sont unifiables, si après cette unification, chaque variables est toujours liées à Any et que chaque variables est liée à exactement une et une seule autre variable, alors les deux termes sont alpha‑équivalents.

La condition que les deux termes soient unifiables est évidente. La conditions que les variables soient toujours liées à Any, signifie que en face de chaque variable dans un des deux termes, il y a aussi une variable dans l’autre terme. La condition que les variables ne soient liées qu’à exactement une autre variable, signifie qu’elles sont liées deux à deux et qu’a une variable dans un des deux termes, correspond exactement une variable de l’autre terme.

Tester l’alpha‑équivalence directement serait plus efficace, mais il est intéressant de noter qu’elle peut se définir avec l’unification aussi. Ça présente l’avantage de le faire en termes de la sémantique du langage objet.

Dans le courant du mois d’Octobre, avait été péniblement abordée la question des modèles et des interprétations. La définition de l’univers de Herbrand avait donné des frayeurs et laissé que des questions, de même la définition de l’interprétation, qui en dépend directement. Il avait été noté que comme ces ensembles sont typiquement infinis, ils ne peuvent pas être posés en extension, seulement en intention. S’était alors naturellement posé la question du langage qui permettrait de les représenter.

Il y a un lien à faire entre cette question et ce qui a été dit depuis quelque jours. En fait, cette question sur les modèles est maintenant au moins en bonne partie résolue.

Pour rappeler ce qui a été maintes fois répété ces derniers jours, l’hypothèse ⟦(nat N)⟧ (mon exemple préféré, tant il aura ouvert la voie vers les hypothèses), définie un N tel que (nat N) est vérifié, un N quelconque, c’est à dire un ensemble de valeurs possibles. Il se trouve que pour la relation nat, cet ensemble est infini, ce qui correspond exactement au problème de la représentation d’une interprétation défini par un ensemble infini. Ceci, en oubliant pas qu’une variable spéciale de ce type, peut être définie par une conjonction d’hypothèses, ce qui permet une certaine expressivité.

Ce qui est chouette, c’est que ce langage pour poser une interprétation, c’est le langage objet lui‑même, qui peut donc définir ses propres interprétations. Il n’y a même pas besoin d’un niveau de langage supplémentaire ou d’un langage dédié à part, comme je l’avais supposé sans le dire explicitement.

Les hypothèses portant sur les variables spéciales, permettent alors au moins quatre choses : faire des vérifications qui seraient impossibles autrement (ex. vérifier que étant donné N tel que (nat N), on a toujours (nat-lt N (s N)), définir des interprétations (l’ensemble des valeurs possibles de N, est finalement une interprétation), faire de la vérification de modèle (une autre manière de dire le premier point), introduire naturellement la notion d’hypothèses omniprésente en logique. Tout ça, en restant dans le langage objet lui‑même.

C’est plutôt bon signe pour la suite, même si le chemin sera encore long et qu’il est plutôt stressant d’y penser.

En marge, quand le résultat d’une requête contient des liaisons à Any, ces liaisons peuvent à priori être remplacées par n’importe quel terme, et doivent même l’être par un terme constant, pour une interprétation. C’est peut‑être là que serait un sens plus compréhensible, de la constante arbitraire mentionnée dans tous les documents sur les interprétations et modèles. Une constante arbitraire à cette fin, remplacer Any et produire des termes constants, a en effet déjà plus de sens qu’une constante arbitraire décrite comme pouvant être appliquée à n’importe quel constructeur n’importe comment. Plus encore, comme ces liaisons à Any peuvent être remplacées par n’importe quel terme constant, pas seulement cette constante arbitraire, c’est encore une autre représentation d’un ensemble infini de termes constants, et par là, un autre élément permettant de formuler des modèles.

La question de la conjonction des hypothèses, devrait être posée aussi dans le cas des hypothèses vérifiant le corps des règles. Il n’a été question que de leur conjonction quand elles sont posées (ce qui ne pose pas de problème) et quand elles sont vérifiées, mais pas quand elles apparaissent dans le corps d’une règle ou n’a été traité et testé, que le cas d’hypothèses uniques, c’est à dire un seul terme portant sur une variable spéciale, et non–plus plusieurs termes portant sur plusieurs occurrences de cette variable spéciale ou même plusieurs de telles variables.

Quelques messages en arrière, était posée la question pratique de trouver une notation pour représenter la vérification d’une hypothèse. Cette question peut être oubliée, il semble qu’une meilleure solution se présente.

Il a été dit que les hypothèses portant sur des variables spéciales, au contraire des hypothèses portant sur des variables ordinaires, peuvent être vérifiées à n’importe quel moment, et même avant de poser l’hypothèse, comme il s’agit de démontrer que le terme en question, a au moins une solution.

Plutôt que poser la vérification du terme dans la règle, il serait peut‑être plus intéressant encore d’avoir une liste d’hypothèses démontrées, en plus de la liste des règles. L’écriture serait assez semblable à celle d’une règle. Au lieu d’avoir un terme, la tête de la règle serait une hypothèse et même pourrait être une conjonction d’hypothèses. Au lieu du corps de la règle, serait écrite une conjonction de termes constants, vérifiant la conjonction posée en hypothèse. Il serait vérifié que la conjonction de termes constants vérifie effectivement la conjonction posée en hypothèse. Il pourrait y avoir plusieurs de telles conjonctions de termes constants vérifiant l’hypothèse, même si une seule suffirait, comme présenter plusieurs solutions pourraient être utile à fin d’example. Cette possibilité n’est pas formellement nécessaire, mais présente un intérêt pratique, pour aider à communiquer le sens.

Il resterait toujours utile de poser des hypothèses dans les règles, car comme vu précédemment, les hypothèse permettent de vérifier des choses qui ne peuvent pas toujours l’être autrement. Une hypothèse introduit les variables spéciales dont il a été question, qui sont à l’origine de cette propriété. La démonstration d’une liste hypothèses aux côtés des règles, aurait l’avantage de simplifier l’écriture et la vérification des règles. Ceci d’autant plus, que deux hypothèses de la même forme mais portant sur deux variables spéciales différentes, comme ⟦(r A)⟧ et ⟦(r B)⟧, pourraient avoir la même preuve qui n’aurait besoin d’être posée qu’une seule fois, et prouverait toutes les hypothèses correspondantes.

Il ne serait pas obligatoire, pour une hypothèse, d’être ainsi démontrée par avance, si elle ne l’était pas, elle serait alors à démontrée avec les hypothèses portant sur des variables normales, après la vérification de la requête.

Un exemple fictif de ce à quoi ça pourrait ressembler :

⟦(nat N)⟧ : (nat z) ; (nat (s z)).

⟦(nat N)⟧ & ⟦(nat-lt N (s N))⟧ : (nat z) & (nat-lt z (s z)) ; (nat z) & (nat-lt z (s (s z))).

Ici, le point virgule signifie une alternative, une disjonction.

L’idée de la vérification d’une hypothèse comme étape de la vérification d’une règle, serait oubliée.

La recherche d’une correspondance pour une hypothèse sous forme d’une conjonction, c’est à dire comprenant plus d’un seul terme, doit être posée. Cette question est liée à la précédente.

À la suite du précédent message.

Il a été proposé qu’on pose une liste de vérifications d’hypothèses, en plus d’une liste des règles. Cet exemple avait été donné :

⟦(nat N)⟧ : (nat z) ; (nat (s z)).

Implicitement étant donné ces deux règles :

(nat z).
(nat (s N)) : (nat N).

Ici, la notation ne signifie pas que ⟦(nat N)⟧ est posé en hypothèse, mais qu’on propose que toutes hypothèses de la forme ⟦(nat N)⟧, est vérifiable, en donnant des exemple de solution vérifiant (nat N). La même notation est utilisée, faute d’en avoir introduite une autre, mais il y a un rapport entre les deux. Par ailleurs, quand il fait mention de la preuve d’une hypothèse, il faut le comprendre comme une preuve que le terme est réalisable, mais c’est plus long à dire.

Jusque là, il n’a pas été dit comment on s’assure qu’une solution proposée est effectivement une preuve qu’une hypothèse ⟦(nat N)⟧ correspond à un terme réalisable.

Une preuve de ⟦(nat N)⟧ est une preuve que (nat N) posée comme une requête, a au moins une solution. Si (nat N) a une solution, la variable N est alors liée à une valeur vérifiant (nat N). Le développement du terme (nat N), N étant liée à un terme, est lui même un terme, et ce terme développé est unifiable avec (nat N) (le développement forme un terme unifiable avec le terme d’origine).

On note que la solution est un terme développé, c’est à dire entièrement constant. Si une variable est liée à Any, on peut développer Any par une constante arbitraire, qu’on peut d’ailleurs appeler “ any ”, à ne pas confondre avec “ Any ”, qui représente « pas de valeur » et qui est un nom interdit, autant pour une variable que pour une constante. Comme les constantes commencent par une minuscule, la question ne se pose pas, mais c’est plus une conclusion pratique qu’une conclusion formelle. Par exemple, une preuve que ⟦(eq A A)⟧ est réalisable, pourrait être (eq any any), mais aussi bien n’importe quelle autre constante, comme dans (eq abc abc) ; c’est seulement que la constante any pourrait être une convention plus parlante.

Donc dans cet exemple :

⟦(nat N)⟧ : (nat z) ; (nat (s z)).

On sait déjà que les solutions données comme preuves, doivent être unifiables avec le terme qu’elles prouvent. Mais on sait aussi que (nat N) doit être vérifiable par une règle. Seulement, on va devoir aller à rebours. Si on cherchait directement une règle vérifiant (nat N), on ferait une recherche de solutions et non‑pas la vérification d’une solution proposée (en fait, si, on pourrait aller dans ce sens là, si on aime faire compliquer quand on peut faire simple ; je laisse imaginer comment). On va d’abord unifier le terme avec la solution proposée et seulement ensuite chercher une règle vérifiant le terme après unification avec sa solution proposée. Ainsi, on prouve que le terme est conforme à la règle et que la solution proposée est bien une preuve que le terme posé en hypothèse est réalisable.

On commence par tenir l’hypothèse pour un terme ordinaire. On tient ⟦(nat N)⟧ pour (nat N). On choisit une solution proposée. On vérifie que ce (nat N) s’unifie bien avec la solution proposée. Ça colle pour (nat z) où on a N = z. C’est seulement maintenant, qu’on s’assure que étant donné cette association de variables, il existe une règle vérifiant ce (nat N) avec ses variables liées. En fait, la vérification de (nat N), se fait alors exactement comme si le terme apparaissait dans une règle et ce que ses variables étaient liées du fait des exigences des autres termes de cette règle. On cherche dans toutes les règles, s’il en existe une vérifiant (nat N) avec sa variable liée. La règle qui vérifie ce (nat N), permet de conclure que ⟦(nat N)⟧ est prouvé par (nat z). On peut faire de même avec (nat (s z)), une autre preuve proposée pour ⟦(nat N)⟧. Dans ce cas, on a N = (s z), et la règle vérifie ce (nat N) est la seconde règle, «  (nat (s N)) : (nat N). »

Note : les termes prouvant les hypothèses, sont entièrement constants, mais on a vu il y a quelques semaines, que la vérification d’un terme entièrement constant peut aussi se terminer en récursion infinie. Ça peut se produire quand une ou des règles ne sont jamais vérifiables. On y reviendra plus tard. Il faut juste noter jusque maintenant, que ce n’est pas parce que les preuves données pour les hypothèses, sont sous forme de termes constants, que la vérification est assurée de se terminer. De toutes manières, la vérification est susceptible d’échouer, aussi.

Si l’hypothèse est une conjonction, on doit s’assurer de la même chose, mais sur plusieurs termes ensemble. Vérifier une conjonction, on a l’habitude. Unifier une conjonction avec une conjonction, c’est nouveau, ce n’est pas exactement comme unifier un terme avec un terme. Le problème de l’ordre des termes va encore montrer le bout de ses moustaches.

On a vu que l’ordre des termes dans une hypothèse, est toujours sans importance (parce que la vérification par une hypothèse, ne vérifie pas des règles), mais que l’ordre des termes dans une règle, peut avoir une importance ou pas, selon les conditions qu’on exige (voir les précédents messages, sur la recherche des hypothèses dans le contexte de la résolution vs dans le contexte syntaxique). On sait donc déjà que si l’ordre des termes d’une hypothèse est sans importance, l’ordre de la vérification des termes prouvant que l’hypothèse est réalisable, pourra pourtant éventuellement avoir une importance.

Si on a une hypothèse ⟦H1⟧ & ⟦H2⟧ et qu’une preuve proposée pour l’hypothèse, est T1 & T2, on va par exemple unifier H1 et T1, puis H2 et T2 (dans le contexte de l’unification de H1 et T1) et vérifier la conjonction H1 & H2 comme si elle apparaissait dans une règle. Mais si H1 est unifiable avec T2 et H2 unifiable avec T1 (dans le contexte de l’unification de H1 et T2), va‑t‑on devoir vérifier H1 & H2 ou H2 & H1 ?

On a vu que l’ordre des termes peut être important, depuis qu’on a introduit la possibilité pour les règles de poser des hypothèses. On a vu qu’une option peut représenter un choix entre deux interprétations possibles (voir les messages sur la recherches des hypothèses dans le contexte de la résolution vs dans le contexte syntaxique). Dans un cas, l’ordre des termes reste sans importance malgré les hypothèses, dans l’autre cas, il est important à cause des hypothèses. Quand l’ordre est important, je ne vois pas d’autres solutions que considérer que l’ordre des termes de l’hypothèse est le même que l’ordre des termes vérifiant l’hypothèse, on ne cherchera alors qu’à unifier H1 avec T1 et H2 avec T2 et à vérifier H1 & T2, seulement. Si l’ordre des termes n’est pas important, on peut unifier dans l’ordre qu’on veut et vérifier dans l’ordre qu’on veut. Si on peut unifier dans l’ordre qu’on veut, il faut quand‑même qu’à un Hn corresponde un Tn, et ne pas oublier que l’interdépendance des termes entre eux, n’impliquera pas que si un Hn est individuellement unifiable avec un Tn individuellement, ça n’impliquera pas qu’il en sera de même dans la conjonction (une unification se faisant dans les contexte des précédentes unifications, en commençant par un contexte vide de toutes unifications). Il faudra éventuellement tester plusieurs permutation possibles. Mais que penser du cas om plusieurs permutations peuvent être vérifiées ? Formellement, ça signifie qu’une vérification est possible est que l’hypothèse est réalisable. Ce que ça signifie sémantiquement, est une question restant en suspend. Ça pourrait en tous signifier que certaines termes sont équivalents et qu’il y a une redondance. Mais peut‑être que ça pourrait signifier autre chose. Cette question est importante, mais temps qu’il n’y a pas d’incohérence, il n’y a pas de raison de s’en alarmer, même s’il ne faut pas l’oublier.

Une question n’a pas encore été abordée : on vérifie que des hypothèses sont satisfiables, étant donné une assignation de leurs variables à des termes constants et un ensemble de règles. Mais qu’en est‑il si les règles avec lesquelles sont vérifiées ces preuves, posent aussi des hypothèses ? Ce sera l’objet d’un prochain message.

La question de la réalisabilité d’une hypothèse, peut évoquer celle d’une règle.

On pourrait penser que poser la tête d’une règle en hypothèse et démontrer que cette hypothèse est réalisable, est une preuve que la règle en question est satisfiable. Mais ce terme pourrait correspondre à plusieurs règles, et dans ce cas, ce ne serait pas une preuve qu’une règle en particulier est satisfiable.

Exemple :

(r1 a).
(r1 X) : (r2 X).

On voit que r2 n’est pas définie, que donc la seconde règle n’est pas satisfiable. Pourtant, on pourrait démontrer que le terme (r1 X) admet au moins une solution, que l’hypothèse ⟦(r1 X)⟧ a donc un sens. Mais elle serait vérifiée par la première règle, pas par la seconde.

On peut avoir au moins la certitude qu’une règle dont le corps est vide, est satisfiable. Mais on ne peut pas récursivement supposer que toute règle dont le corps est constitué de termes individuellement satisfiable, sera effectivement satisfiable, comme la conjonction est plus exigeante que les termes individuels. Cependant, on sait que si un seul de ses termes n’est pas satisfiable, alors elle n’est pas satisfiable. On peut donc récursivement au moins déterminer quelles sont les règles dont il est certain qu’elles ne sont pas satisfiables. Je ne le mentionne que comme une possibilité. Personnellement, je n’en ferai pas de mise en œuvre, parce que cette solution est partielle et que les solutions à moitié, ne m’intéressent pas dans ce contexte.

Quoiqu’il en soit, une solution montrant qu’une règle est satisfiable, est comparable à une solution montrant qu’une hypothèse est satisifiable. Mais l’hypothèse peut désigner n’importe quelle règle dont la tête correspond. Pour démontrer qu’une règle est satisfiable, on doit pouvoir désigner une règle en particulier. L’idée avait été émise de le faire avec les preuves des hypothèses, mais c’était parler trop vite, ça n’est pas possible. Ça aurait put permettre de simplifier la définition de l’écriture. Le problème n’est pas tant formel que pratique, en pratique, il est préférable de réduire au minimum les règles d’écriture et les symboles spéciaux (comprendre, hors constantes et variables) utilisés pour cette écriture. Le problème de cette notation, reste en suspend.

Peut‑être désigner la règle par son nom serait une idée. Mais ça imposerait de nommer toutes les règles. Ça dépend de la taille des systèmes de règles, envisagés. L’idée de le faire avec le texte de la règle n’est pas mauvaise, mais ça risquerait d’alourdir le texte des règles, en plus de nécessiter au moins un nouveau symbole pour séparer le corps d’une règle d’un exemple de solution prouvant qu’elle est satisfiable.

Retour sur une question de sens, avec la non‑importance de l’ordre des termes dans une hypothèse et les termes isolés, de cette hypothèse.

Il a été dit que l’ordre des termes n’est jamais important dans une hypothèse, même dans les cas où l’ordre des termes est important dans une règle, et que alors l’ordre des termes est important aussi dans la preuve d’une hypothèse.

Il a été dit que l’ordre n’est pas important, parce que les hypothèses sont comme constitués de termes désignant des règles dont les corps seraient vides, qu’elles sont donc indépendantes entre elles, si ce n’est pour les liaisons des variables sur lesquelles elles portent, et justement en ça, l’ordre n’est pas important.

C’est l’explication, logique, formelle, mais qu’est‑ce que ça peut bien signifier ?

Un exemple peut l’illustrer. Soit deux procédures P1 et P2. Disons que P1 alloue une zone de mémoire et lie une référence mémoire à cette zone allouée. Disons que P2 écrit une valeur dans cette zone de mémoire, via cette référence mémoire. L’ordre ne peut être que P1 puis P2, pas l’inverse. On peut dire que P2 est sous l’hypothèse produite par P1. C’est pour la réalisation. Mais quand on est sous l’hypothèse P1 & P2, on est sous l’hypothèse, implicitement, que P1 & P2 a été vérifiée et à ce moment là, l’ordre n’a plus d’importance.

Mais reste autre chose. L’hypothèse P1 & P2 est‑elle aussi une hypothèse de P1 et une hypothèse de P2, individuellement ? Oui, comme P1 & P2 implique P1 et implique P2. Logiquement, formellement, ça se comprend facilement, mais quel sens cela peut‑il bien avoir ?

Un autre exemple. Disons que P1 calcul une valeur et que P2 affiche cette valeur. P1 & P2 signifie « une valeur valeur a été calculée, et cette valeur a été affichée ». On peut être sous l’hypothèse de P1 seulement, qui se comprendrait comme « une valeur a été calculée ». On peut être sous l’hypothèse de P2 seulement, qui se comprendrait comme « une valeur a été affichée ». Il faut bien lire, cette fois c’est « une valeur » et non‑pas « cette valeur ». Mais peut‑on toujours être sous l’hypothèse P1 et P2, « une valeur valeur a été calculée, et cette valeur a été affichée » ? Oui, mais à condition que les deux hypothèses soient liées, par exemple par une variable (même liées indirectement, comme via un terme portant sur une variable). Mais on peut aussi être sous l’hypothèse seulement de P1 ou seulement de P2, avec le sens un peu différent mentionné.