Les logiques : notes en vrac

Si par une option, on n’accepte que les hypothèses portant sur des variables spéciales et que ces hypothèses sont toutes prouvées, alors le résultat d’une requête est toujours interprétable. En ça, prouver les hypothèses, peut sembler plus important que prouver que les règles sont réalisables, puisqu’après tout, on va les vérifier et éventuellement juste échouer à les vérifier. C’est le côté formel.

Mais d’un autre côté, un côté plus sémantique ou intentionnel, il est plus incompréhensible encore de poser des règles non‑réalisables que de poser des hypothèses non‑réalisables. Parce qu’une hypothèse, peut être véritablement une hypothèse, pas seulement introduire une variable représentant une généralité.

Les deux sont autant une priorité. Entre des règles qui n’ont pas de sens et des résultats qui ne sont pas interprétables, difficile de choisir et plus facile de préférer éviter les deux.

Précédemment a été rapidement évoqué une notion au nom pompeux, l’alpha‑équivalence, sans expliquer pourquoi elle a été introduite.

Ce qui suit est implicitement à propos des hypothèses portant sur des variables spéciales, seulement, les variables liées à une constante.

Imaginons qu’on ait cette règle :

(r1 A) : ⟦(r2 B)⟧ & ⟦(r2 C)⟧ & (r3 A B C).

Disons qu’on a préféré prouver que ⟦(r2 B)⟧ est réalisable et que c’est fait. Doit‑on refaire une preuve de ⟦(r2 C)⟧ ? La preuve serait exactement la même. Ne serait‑il pas plus commode de considérer que la preuve de ⟦(r2 B)⟧ et aussi une preuve de ⟦(r2 C)⟧ ? De plus, si on a prouvé par avance, disons ⟦(r2 D)⟧, il faut bien que cette preuve soit miss en correspondance avec ⟦(r2 B)⟧ et ⟦(r2 C)⟧, pour qu’avoir fait la preuve de ⟦(r2 D)⟧ ait un intérêt.

C’est justement le propos de l’alpha‑équivalence. Les trois hypothèses, ⟦(r2 B)⟧, ⟦(r2 C)⟧ et ⟦(r2 D)⟧, sont les mêmes, elles ne diffèrent que par le nom de leurs variables. Les tenir pour équivalentes malgré cette différence ne devrait pas être une surprise. En effet, avant d’appliquer une règle, on l’instancie, c’est à dire qu’on en fait une copie avec de nouvelles variables mais en respectant le même schéma. C’est finalement la même chose, on peut dire qu’on en fait une copie alpha‑équivalente.

L’alpha‑équivalence, c’est l’égalité modulo le nom des variables (peut‑être parfois modulo le nom des constantes, mais pas ici). Ce n’est pas formellement une égalité, c’est pourquoi on parle d’équivalence et pas d’égalité, même si on peut informellement penser à une égalité.

Par exemple, les deux termes (a B C) et (a D E), sont équivalents, mais les deux termes (a B B) et (a D E), ne le sont pas. On a équivalence quand pour passer de l’un à l’autre, on change chaque variable en particulier, par une variable en particulier. À une variable, doit correspondre une et une seule variable, quelque soit le nombre d’occurrences de la variable. L’important est que les variables qui étaient les mêmes, restent les mêmes, et que celles qui étaient différentes, restent différentes. Pour le reste, le schéma doit être le même, mais ça ne fonctionne pas comme avec l’unification. Par exemple (a B C) serait éventuellement unifiable avec (a (b x) (b y)), mais n’est pas équivalent à (a (b x) (b y)). Unifiables et équivalents, sont deux notions différentes, même si on peut établir un lien entre les deux (comme définir l’équivalence à partir de l’unification).

Une colle : (a B C) est‑il équivalent à (a C D) ? Hé bien ça dépend. Si on prend les deux termes isolément, oui, dans le terme de gauche, on change B en C, puis C en D (mais seulement le C qui était déjà là), et on arrive à (a C D). Mais si on a une conjonction, c’est différent. Cette différence aurait put se poser dans le paragraphe précédent, elle s’exposait juste plus facilement avec cette colle.

Si on a une conjonction, l’équivalence doit s’appliquer sur l’ensemble de la conjonction, pas sur les termes pris individuellement. Là encore, peut se poser la question de l’ordre des termes. Comme pour une hypothèse, l’ordre n’est pas important, si on trouve une équivalence pour une certaine permutation des termes, alors il y a équivalence. Ceci, même quand l’ordre des termes est important dans les règles, comme il n’est jamais important dans les hypothèses, même dans ce cas. Une explication sensée a été donnée plus haut à cette apparente étrangeté. Comme pour la vérification d’une preuve d’une hypothèse, il pourrait être nécessaire de tester les permutations possibles.

On pourrait exiger que l’ordre des termes soit partout le même, mais on peut poser en particulier une preuve de ⟦(r A B)⟧ & ⟦(r B C)⟧ et en y pensant autrement, dans une règle, se référer à la conjonction d’hypothèses ⟦(r E F)⟧ & ⟦(r D E)⟧, pour une raison quelconque, par exemple en jaugeant que c’est quelque part plus lisible ainsi.

Imposer le même ordre partout, est une option défendable, mais j’y suis personnellement opposé, ce serait incompréhensible, l’ordre n’étant pas important. Il y a déjà bien assez d’opportunités de faire face à des erreurs en faisant des démonstrations, inutile d’en rajouter avec des erreurs inutiles qui n’en sont pas vraiment, ce serait du mal pour rien.

Dans une conjonction d’hypothèses, les termes peuvent être liés ou pas.

Ce qui suit est implicitement à propos des hypothèses portant sur des variables spéciales, seulement, les variables liées à une constante.

Par exemple la conjonction ⟦(r1 A)⟧ & ⟦(r2 B)⟧, les deux termes ne sont pas liés, mais dans ⟦(r1 A B)⟧ & ⟦(r2 B C)⟧, ils le sont par B.

Il est serait utile est compréhensible d’exiger de ne pas poser de preuve de conjonctions dont les termes ne sont pas tous liés entre eux. Il serait toujours possible de poser dans une règle, qu’on suppose l’hypothèse ⟦(r1 A)⟧ & ⟦(r2 B)⟧, mais poser la preuve de ⟦(r1 A)⟧ & ⟦(r2 B)⟧ ne serait pas permis, il serait au lieu de ça, attendu que ⟦(r1 A)⟧ et ⟦(r2 B)⟧ soit prouvées séparément.

La raison est que ça peut faciliter la recherche de preuves d’hypothèses et ça rendrait aussi les preuves plus facile à lire.

Cette question inspire qu’il pourrait être utile d’avoir une syntaxe permettant de regrouper entre eux, les termes liés, que ce soit dans les hypothèses le reste du corps des règles. Par exemple au lieu de ⟦(r1 A B)⟧ & ⟦(r2 B C)⟧, il pourrait être écrit ⟦(r1 A B) & (r2 B C)⟧. Reste à savoir quelle notation pourrait exprimer le regroupement de termes ordinaires dans le corps des règles et des requêtes.

Étant donné une conjonction, il faut pouvoir en extraire les groupes de termes liés. Étant donné deux conjonctions, il faut pouvoir déterminer si elles sont alpha‑équivalentes. Étant donné deux conjonctions, il faut pouvoir les unifier.

Même quand l’ordre des termes est important, il ne l’est qu’entre termes liés. En effet, ce qui peut rendre l’ordre des termes important, ce sont les hypothèses. Ors, un terme ne peut pas dépendre d’une hypothèse produite par un autre terme, s’il n’est pas lié aux variables créées pour l’hypothèse, ce qui implique que les deux termes sont liés par au moins une variable.

Des termes ne semblant pas syntaxiquement liés, peuvent l’être à travers les liaisons entre variables.

Précédemment, a été justifiée une option permettant de choisir si les hypothèses auxquelles se réfèrent les règles, sont recherchées dans le contexte de la résolution ou dans le contexte syntaxique. La justification était que dans le premier cas, l’ordre des termes devient significatif et que ça peut rendre la lecture et l’analyse des règles, moins commode.

Il en a été fait une option pour ne pas exclure la sémantique rendant les termes sensibles à l’ordre, « au cas où ».

Quand la dépendance à l’ordre à cause des hypothèses, n’est pas acceptée, une solution proposée pour ne pas limiter ce qui peut être exprimé, était de déplacer les hypothèses en cause, vers un contexte syntaxique plus englobant.

Ceci fait penser à la différence entre les langages dits impératifs avec effets de bord et les langages dits fonctionnels sans effets de bord. Ça pourrait bien être une raison de plus pour ne pas exclure le cas et en garder la possibilité en option.

Certes, la lecture des règles est moins commode quand leur sens dépend de l’ordre des termes, mais si le langage objet décrit ici est utilisé comme langage dans lequel est écrite la sémantique d’un autre langage, ce langage serait défini comme des règles dans le langage défini ici, et un programme dans cet autre langage, serait une collection de règles faisant référence aux règles définissant cet autre langage. Dans ce cas, les règles sont le résultat d’un processus de traduction, automatique, et elles ne sont pas destinées à être lues par un humain, surtout si elles sont en grand nombre.

Si on considère qu’on peut vouloir vérifier seulement des propriétés, elles‑même exprimées sous forme de règles, alors on a pas nécessairement besoin d’aller jusqu’à l’analyse des règles, leurs vérifications étant suffisante.

Les deux problèmes que sont la lisibilité et l’analyse éventuellement moins commode, ont moins d’importance dans ce cas. Par contre, la réécriture des règles pour répondre à la nécessité de la non‑pertinence de l’ordre des termes, pourrait être un problème.

Il y a de bonnes raisons de conserver la possibilité des deux cas, comme deux options aussi importantes l’une que l’autre, sans se limiter à une seule.

Comme dit précédemment, quand une hypothèse comme ⟦(r1 A B)⟧ & ⟦(r2 B C)⟧ est posée, on ne peut pas chercher une preuve de ⟦(r1 A B)⟧ et une preuve de ⟦(r2 B C)⟧, qui serait la même d’ailleurs, il faut chercher une preuve de ⟦(r2 A B)⟧ & ⟦(r2 B C)⟧, parce que les variables caractérisées ici, le sont par une conjonction et qu’elles ne le seraient plus de la même manière, par deux preuves séparées de chacun des éléments de la conjonction. C’est pour cette raison qu’il faut pouvoir extraire les groupes de termes liées par des variables, dans les termes posés en hypothèses.

Mais pour les termes pouvant être démontrés par cette hypothèse, il n’est plus nécessaire de rechercher une conjonction. Si le terme (r1 A B) est rencontré, il est prouvé par l’hypothèse ⟦(r1 A B)⟧ & ⟦(r2 B C)⟧, sans qu’il ne soit nécessaire de s’assurer qu’il est accompagné d’un terme (r2 B C). C’est ainsi, parce que les variables sont déjà caractérisées par l’hypothèse et que les variables liées y font seulement référence, ne les caractérisent pas.

Une hypothèse est posée avec tous ses termes ensemble, sinon elle n’a plus le même sens ; on repose sur une hypothèse, en se reposant sur ses termes individuellement, ça ne change pas son sens.

Retour sur une notation.

Jusqu’ici, la preuve qu’une hypothèse est réalisable, a été écrite comme dans cet exemple :

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

Il a été remarqué que cette notation n’est pas idéale, parce qu’elle utilise la même notation que pour les règles, « A : B » qui se lit « A est défini comme B ». Les symboles ⟦ ⟧ avant les deux points, lèvent quand‑même l’ambiguïté.

Formellement, ça devrait se lire comme « (nat z) ; (nat (s z)) est un modèle de (nat N) ». Il existe une notation pour ça : « A ⊧ B  » qui se lit comme « A est un modèle de B ». Mais on l’écrit ici dans l’autre sens, le modèle à droite. Il existe un symbole Unicode correspondant à un ⊧ tourné dans l’autre direction, mais au moins en ce qui me concerne, il s’affiche comme un caractère inconnu sans motif : ⫤. Si des gens voient quelque chose, tant‑mieux, mais ce symbole n’est visible pas supporté par toutes les polices de caractères.

La notation restera donc encore la même que jusqu’à maintenant.

Pour information quand‑même :

• Le caractère Unicode U+22A7, qui s’affiche comme ⊧ , c’est à dire |=, est utilisé pour dire « A  ⊧ B », « A est un modèle de B ».
• Le caractère Unicode U+2AE4, qui s’affiche ou pas comme ⫤ , c’est à dire =|, pourrait être utilisé pour dire « A ⫤ B », « B est un modèle de A ».

Dans ce message, un résumé de l’histoire jusqu’ici, juste après une note.

Dans plusieurs messages précédents, quand il était question d’hypothèses, c’était implicitement à comprendre comme des hypothèses portant sur des variables liées à une constante spéciale représentant une généralité, appelée les variables spéciales, pour le dire plus brièvement.

Deux de ces messages ont été modifiés pour ajouter une note le rappelant, mais la remarque peut s’appliquer à d’autres. Sans cette supposition implicite, plusieurs messages sont autrement faux. La différence est que si A et B sont deux variables spéciales, elles ne peuvent pas être liées indirectement, alors qu’elles peuvent l’être si elles sont des variables normales. La différence est importante et implicite dans plusieurs précédents messages.

C’est l’occasion de faire une note. Je crois que ce qui est appelé ici, les variables spéciales, correspond à ce qui est appelé ailleurs, les variables de Skolem. Sans certitude, ce serait à vérifier, mais ce ne sera fait que bien plus tard. Dans l’assistant de preuve Isabelle/HOL précédemment mentionné, apparaissait ce type de variable. Mais il y avait deux différences : elles ne s’accompagnaient pas d’une notation distinguant des hypothèses et il était parfois fait mention d’un processus nommé skolémisation, qui n’a pas d’équivalent ici. Si ce qui est appelé les variables spéciales, ici, correspond bien aux variables de Skolem, peut‑être alors, ce qui est appelé la skolémisation, est‑il un processus au cours d’une traduction d’une logique vers une autre.

S’il ne sera pas vérifié maintenant si oui ou non il s’agit bien de ce type de variable, c’est pour rester dans le fil naturel de ce sujet, et ne pas risquer une influence extérieur qui pourrait le rendre dissonant, un risque qui ne sera pas pris.

En parlant de fil, il avait annoncé un petit résumé, qui vient maintenant. Le fil de l’histoire est intéressant quand il est réduit à ses grandes lignes.

D’abord a été introduit le Prolog de base, sur la base d’une ancienne intuition. En le décrivant, il a été noté qu’il s’explique assez naturellement en terme de langage naturel écrit, malgré des différences. Ce qui est important, c’est que malgré qu’il soit un langage formel, il est abordable, il a une sémantique assez communément intuitive.

Puis des expériences simples ont été faites avec ce langage, des formulations et requêtes simples. À cette occasion, des limites se sont montré. Ces limites étaient surtout liées au fait qu’on ne pouvait pas faire de vérification sur des ensembles infinis de valeurs, parce que la vérification ne se terminerait jamais. Par exemple, on pouvait vérifier qu’un entier naturel en particulier est plus petit que son successeur, mais on ne pouvait pas vérifier que n’importe quel entier naturel est plus petit que son successeur, alors que ça semble évident ; mais ce qui semble évident, il est préférable que ce soit verifiable.

En voulant remédier à ce problème, a été posée l’idée intuitive, d’une variable quelconque vérifiant un terme et de raisonner sur cette variable en se basant sur le fait qu’elle vérifie ce terme. Il était pressenti que cette variable pourrait être associée à une sorte de constante, afin de préserver sa valeur quelconque, d’interdire de la considérer liée à autre chose qu’à sa valeur quelconque. Restait à définir cette constante.

Il y a eu un égarement en imaginant trop vite que la variable était au centre, que le terme qu’elle vérifie pouvait être oublié pour peu qu’on considère qu’elle a n’importe laquelle des valeurs possibles permises par ce terme et que cet ensemble de valeurs pouvait être représenté par un ensemble de constantes, l’ensemble de constantes étant tenu pour être une constante. Mais c’était oublier que cette variable pouvait être définie par rapport à une autre variable et que définir la valeur de la variable toute‑seule, cassait cette relation et était donc une porte ouverte à l’incohérence.

Une marche arrière a été faite, pour revenir à l’idée de départ, en associant cette fois la variable à une constante et au terme qu’elle vérifie (la variable). De cette manière, si le terme contient deux variables, la relation entre les deux variables n’est pas cassée, le sens est préservé.

Il s’est avéré que la seule interprétation possible de cette variable, était qu’elle est une variable qui vérifie un terme, ce qui revient à supposer ce terme, mais seulement quand il apparaît avec cette variable, la distinction avec les autres variables étant faite par la constante à laquelle elle est liée et qui lui est unique, ce qu’interprète naturellement la sémantique du langage de base, qui est préservée.

Il a été remarqué que ça ressemble beaucoup à la notion de poser une hypothèse, mais par là, en définissant précisément ce que signifie poser une hypothèse, ce qui est autre chose que l’idée intuitive qu’on peut en avoir.

Plus tard encore, s’est posé une autre question, évoquant le précédent écueil de casser des relations entre des variables : des hypothèses apparaissant ensemble dans une conjonction, ne doivent pas être tenues pour séparées, sous peine de casser la relation entre des variables et donc d’ouvrir la porte à l’incohérence. Cette fois, il ne s’agissait plus de variables liée ensemble dans un terme, mais de variables liées ensemble dans plusieurs termes.

Entre temps, comme la création d’hypothèse passait par la création de variables immédiatement liées à une constante spéciale propre à chacune, s’est posé la question de la création d’hypothèses portant sur une variable existant déjà, ce qui peut se produire avec une requête faite dans le contexte d’une requête précédente. C’est ainsi qu’à été posée la notion d’hypothèse portant sur des variables ordinaires, c’est à dire sur une valeur en particulier d’une variable, telle que définie par la résolution d’une requête.

Puis a été relevé la nécessité de démontrer qu’une hypothèse est réalisable, ce qui a été appelé une preuve de l’hypothèse. La raison était que si un terme d’une règle, est prouvé par une hypothèse, dans la sémantique du langage d’origine, ça signifie qu’il existe une règle vérifiant ce terme et qu’on a fait comme si, mais sans le vérifier et que ça n’a un sens que s’il existe effectivement une règle pouvant vérifier un tel terme avec ses variables.

Il a été remarqué qu’il suffit pour cela de montrer que le terme admet au moins une solution, une notion qui je crois, mais sans en être certain, correspond à la question dite des « types habités ».

Concernant la démonstration des hypothèses, il a été remarqué que les hypothèses portant seulement sur des variables spéciales, peuvent toujours être prouvées à priori, en posant un exemple de solution quelconque à ce terme ou conjonction de termes, ou même plusieurs solutions si on veut illustrer par plusieurs exemples. Il a été remarqué que, au contraire, les hypothèses portant sur ne serait‑ce qu’une variable ordinaire, ne peuvent être démontrées que à posteriori, la valeur de la variable n’étant définitivement définie, qu’à la toute fin de la résolution de la requête. Je ne sais pas à quoi correspond cette distinction qui s’avère pourtant essentielle et au sujet de laquelle je n’ai jamais vu le moindre mot ailleurs.

C’est en gros les grandes lignes de l’histoire jusque maintenant.

Deux choses en très résumé sont intéressantes à relever. D’abord, la notion d’hypothèse et de variable spéciale qui s’est avéré fructueuse, à été initialement introduite pour résoudre un problème de vérification sur les entiers naturels. Précédemment avait été dit à l’occasion d’un exemple, que les entiers naturels sont importants en logique. Le fil de cette histoire en est une illustration. La deuxième choses intéressantes, est qu’on été introduit des concepts qui sont probablement déjà connus, beaucoup ont sûrement été réinventés, mais des concepts qui sont soient souvent mal expliquées ou même pas distingués. Ce qui est intéressant, c’est qu’ils ont été introduits et définis naturellement, au fil des nécessités et des analyses de cas possibles. Ces choses se comprennent mieux et s’expliquent mieux quand on sait comment et pourquoi elles apparaissent, quand elles sont placées dans un fil.

Ceci dit, ce n’est que le début de l’histoire, le chemin sera encore long. De plus, tout ne sera pas dit. Deux autres types de variables spéciales sont envisagés mais ne seront pas décrits ici. L’un d’eux, est encore une fois inspiré par un problème de vérification sur les entiers naturels, mais sans même encore savoir si cette idée d’un autre type de variable est vraiment nécessaire ou pas. L’autre type encore, a une utilité même moins certaines. S’ils ne seront pas décris ici, c’est parce qu’ils seront encore plus aventureux que ce qui a été tenté jusque maintenant, et qui a été déjà long à formuler en mots. Mieux vaut en rester à l’essentiel, plutôt que risquer de noyer cet essentiel dans l’histoire d’autres idées peut‑être moins essentielles, sans compter les risque d’erreurs perturbantes qui peuvent être temporairement dites en chemin, même si elles finissent pas être corrigées (ex. l’initial égarement sur une mauvaise piste avec les variables spéciales avant de revenir en arrière et enfin passer par un chemin plus prometteur).

Si ce qui est appelé ici, les hypothèses vérifiables à priori, correspondait aux types, alors peut‑être que ce qui est appelé ici les hypothèses vérifiables seulement à posteriori, correspond aux types dépendants ? Ça se tiendrait peut‑être, comme des variables normales sont impliquées ; mais ça reste sans certitude. Quoiqu’il en soit, même si c’est le cas, c’est alors mieux expliqué par le fil de l’histoire jusqu’ici que par tout ce que j’en ai lu n’importe où ailleurs ; et je préfère malgré tout encore parler d’hypothèses vérifiables à priori et d’hypothèses vérifiables seulement à posteriori, ça me semble plus compréhensible, parce que mieux dire ce que c’est. Aussi, si ça correspond bien à ces notions, alors elles ont été introduites ici sans aucune complication telle que des niveaux de langage séparés.

Cette démarche peut sembler étrange ou arbitraire.

Si une règle peut renvoyer plusieurs solutions, il peut sembler arbitraire qu’il soit exigé de poser un exemple de solution comme ça et de se satisfaire de dire que ce terme peut avoir cette solution sans se soucier de toutes les autres solutions possibles. Pourquoi cette solution et pas une autre ? Surtout qu’on peut choisir n’importe laquelle ? Est‑ce que ça a du sens ? Du sens, non, ça n’en a pas vraiment, en effet (sans être insensé non‑plus), mais c’est une nécessité, pour qu’une autre chose puisse en avoir, du sens.

C’est étrange et arbitraire seulement si on confond la fin et les moyens. Proposer une solution, n’est pas la finalité, la finalité, c’est de montrer que le terme est vérifiable, pour la raison donnée dans ce qui est cité. Poser une solution parmi d’autre, ce qui peut sembler arbitraire, n’est que le moyen qui vient le plus simplement, pour répondre à cette nécessité, même si ça peut sembler étrange à cause de l’arbitraire du choix de la solution.

Il y a bien une différence entre la fin et le moyen. On peut poser plusieurs solutions, et non–pas seulement une, parce que la finalité n’est pas de donner un exemple de solution, mais de montrer que le terme est réalisable, ce qui peut se faire en proposant une solution, autant qu’en proposant plusieurs solutions. On voit déjà que le moyen varie un peu, mais que la finalité reste la même.

Une autre illustration de la différence, mais une illustration dangereuse, est que le terme peut être tenu pour vérifiable, d’autorité, sans même proposer de solution au terme. C’est un autre moyen pour la même finalité. Ce moyen, ça s’appel poser comme axiome, et c’est dangereux, parce que entre ce qu’on croit être à 100 % et ce qui est vraiment, il y a trop souvent une différence, même avec ce qui semble évident. C’est la raison pour laquelle a été imaginé une sémantique permettant de vérifier que n’importe quel entier naturel est plus petit que son successeur, plutôt que de se contenter de le croire, même avec une conviction inébranlable.