Les logiques : notes en vrac

Le document dans lequel en 1956, Noam Chomsky a commencé à définir les catégories de grammaires qui sont encore utilisées de nos jours en logiques, linguistique, psychologie et « acquisition » d’une langue : Three models for the description of languages (chomsky.info) [PDF], Noam Chomsky, Septembre 1956.

Le vocabulaire n’est pas encore exactement celui qui a été finalisé plus tard, il ne parle pas encore de grammaires génératives, mais déjà de grammaires transformationnelles. Il n’y parle pas encore non‑plus de la hiérarchie regular ⊂ context‑free ⊂ context‑sensitive ⊂ unrestricted.

Avant de se préoccuper des propriétés d’une grammaire ou d’une logique, il faut se préoccuper de son expressivité, tester ce qu’il est possible de représenter avec et avec quelles facilité et difficulté ; ensuite, si ça semble prometteur, on peut se poser la question de la démontrabilité des propriétés escomptées.

Le vrai implique la validité, la validité est une conséquence implicite du
vrai.

Ça peut sembler sans intérêt de le souligner, pourtant ça signifie que du vrai ont peut dériver le validité, et pouvoir dériver quelque chose, ça peut permettre de démontrer quelque chose.

J’aime bien cette superposition de deux schémas à la page 5 de ce document : What can sequent calculus do for functional programs ? (irif.fr) [PDF], Leverhulme Grant, 2009.

À garder : Notes for the Proof Theory Course (univ-paris13.fr) [PDF].

Le document aborde des choses compliquées, mais la première partie, sur la déduction naturelle, est abordable. En particulier, il est intéressant de comparer ses deux formulations, en comparant les formules de la page  № 3 et de la page № 6 (les numéros en bas des pages, pas ceux des liseuses PDF). On y lit implicitement que la décharge des hypothèses dans la déduction naturelle sans séquents, correspond à la présence puis à l’absence de ces hypothèses dans le contexte (la partie gauche des séquents) dans la déduction naturelle avec séquents.

À garder : Natural Deduction (ualberta.ca) [PDF], Francis Jeffry Pelletier, Allen P. Hazen, 2014.

C’est à propos de la confusion que peut créer le nombre de variantes de logiques qui sont toutes qualifiées de déduction naturelle. Je constate aussi, à mes dépends, que ça n’aide pas à s’y retrouver. Je crois qu’il faut choisir en fonction de l’adéquation avec le domaine d’application ; pour ça, bien penser au sens et au non‑sens (selon le domaine d’application) que peuvent avoir les règle d’inférences. Il y a aussi le problèmes des notations, mais c’est moins important, même si ça aussi, ça n’aide pas à s’y retrouver.

C’est malheureusement long, mais lire l’introduction en dit déjà assez.

Sur la déduction naturelle vs le calcul des séquents, surtout sur le vocabulaire, la notation et les détails concrets me semblant les plus importants.

Ces deux systèmes appartiennent plus au domaine de la théorie des preuves qu’au domaine de la logique, au sens de langage objet. Mais il arrive que les deux niveaux de langage suivent la même logique.

On parle presq’autant de séquents dans la déduction naturelle que dans le calcul des séquents. Le nom de chacun des deux systèmes, est trompeur, en ce qu’il suggère que les séquents sont spécifiques au second. Ce qui est spécifique au second, c’est d’avoir été défini après la première, pour la seule raison d’une démonstration d’une chose mathématique (quelque chose à voir avec faire une preuve en particulier, sans faire usage de la règle de la coupure).

Dans la déduction naturelle sans séquents, on parle de décharge de la preuve ou de décharge de l’hypothèse (la seconde expression me semble plus adaptée) ; cette décharge de l’hypothèse est notée avec deux crochets autour de l’hypothèse et trois petits points descendant vers le bas. Cette notation (et les quelques nuances qui l’accompagnent) est tout ce qui distingue la déduction naturelle sans séquents de la déduction naturelle avec séquents. Modulo quelques nuances sémantiques sans consensus, c’est bien seulement une différence de notation, cette décharge existe aussi avec les séquents, mais n’est jamais désignée comme telle en mots, elle ne se lit que dans la notation. Notée sous forme de séquent, cette décharge, pour une hypothèse P, correspond à P apparaissant à gauche d’un séquent dans la condition et n’apparaissant plus, ni même à droite du séquent, dans la conclusion.

Les séquents sont souvent associés aux termes antecedents ou context et succedents ou consequent (en Anglais). Quand il n’est pas question de séquent, le terme antecedents est souvent employé aussi, mais le terme consequent est préféré au terme succedents. Ça ne semble pas porter de différence de signification, juste que s’il n’y a qu’un séquent dans la conclusion, au moins une source parle de consequent et ne parle de succedents que si la conclusion est constituée de plusieurs séquents. Quand le domaine est la logique appliquée à l’informatique, le terme context est toujours (ou presque ?) préféré au terme antecedents. J’ai bien plus souvent lu parler de context que de antecedents.

Un séquent est parfois aussi appelé hypothetical judgment, tandis que dans le domaine de la logique, on lis souvent l’expression hypothetical proposition. La différence entre les deux semble mince et j’ai lu explicitement qu’il n’y a pas de consensus sur la différence entre judgment et proposition. Une différence assez admise, pourrait quand‑même être que le terme proposition est connoté moins formel que le terme judgment, qui typiquement est plus accompagné de l’exigence de fonder l’antécédents. Disons alors qu’une proposition hypothétique doit le plus souvent se lire comme « Supposons que A, alors on a B », tandis qu’un jugement hypothétique, doit le plus souvent se lire comme « Si A est établit, alors on a B », qui est de plus, souvent associé à une notion de contexte, c’est à dire que dans « si A est établit », le A se comprend comme dans un contexte dans lequel doit se comprendre ce qui est à droite du séquent.

J’ai personnellement une préférence pour la notation avec les séquents, plus précise car plus explicite et aussi parce qu’elle souligne la similitude qu’il y a entre la dérivation dans un langage objet et la dérivation dans un méta‑langage, bien qu’il faille aussi faire attention à ne pas confondre les deux, malgré parfois (selon le domaine d’application) de grandes similitudes.

Dans les notations avec les séquents, l’ordre des séquents est important, c’est parfois dit seulement en mots, mais ça se constate concrètement dans les définitions formelles du langage SML (dans la section № 6, “Dynamic Semantics for the Core”).

Je m’avance un peu plus en disant que le contexte à gauche des séquents, est un (ou plusieurs) objet avec un type bien précis, sur lequel on peut faire des requêtes dans les termes de ce qui se trouve à droite du séquent. Là aussi, ça se constate concrètement dans les définitions formelles du langage SML (surtout dans la section № 4, “ Static Semantics for the Core”). Les termes à droite des séquents, sont dans une notation précise, définie domaine par un domaine.

Les termes à gauche d’un séquent sont liés par une conjonction, tandis que ceux à à droite du séquent, sont liés par une disjonction (bien lire et s’en souvenir : une disjonction).

Dans la conclusion d’une inférence, il n’y a typiquement qu’un séquent (c’est même obligatoire pour les variantes intuitionnistes de ces deux systèmes). Dans la condition, c’est typiquement l’inverse, il y a le plus souvent plusieurs séquents. Même chose pour les séquents composant les règles d’inférence : les séquents intuitionnistes ont toujours exactement un succedent.

Quand je dis plus haut que dans la condition d’une inférence, l’ordre des séquents est important, c’est en général, pas toujours en particulier, mais la notation semble avoir été posée pour être valable en général.

C’est valable en particulier pour la définition de SML (encore, oui) ou la définition de la sémantique dynamique, tantôt implicitement, tantôt explicitement, accompagne les séquents d’un état. Quand les séquents représentent des opérations ayant des effets, l’ordre des séquents ne peut que être important. Quand il n’est pas important, je crois qu’il faut le préciser et le justifier (ça dépend de la nature des contextes et de la logique du langage objet).

L’ordre des contextes à gauche des séquents, est en général sans importance, mais il n’est pas impossible qu’il le soit dans certains domaines. La déduction naturelle dans ses formes les plus courantes, a des règles d’inférence dites structurelles. L’une d’elle porte sur la contraction des contextes listés à gauche des séquents, et une autre sur la permutation de l’ordre de ces contextes, ceci n’étant significatif que quand il y en a plusieurs, et le plus souvent il n’y en a qu’un seul. Mais les logiques dont on peut parler en général, peuvent être sujettes à des variantes. Il n’est pas interdit dans un document formel, de poser qu’on utilise la déduction naturelle avec les séquents mais sans certaines règles d’inférence (ce qui ne présente pas de risque d’introduction d’incohérences).

Quand je parle plus haut, de possibles effets de bord liés à l’évaluation des séquents qui est à l’origine de la significativité de l’ordre dans lequel il apparaisse, ça évoque le comportement d’un logiciel, et je crois que le rapprochement est correcte. Ça peut surprendre si on associe la logique et les preuves, entre autres aux langages fonctionnels sans effets de bord. Ça n’est pas contradictoire, comme même dans un langage fonctionnel, l’ordre des définitions est important et que pendant l’élaboration d’un programme à partir de sa source, il y a bien des effets de bords, et même des effets de bords encore, même si transparents pour la logique du programme, pendant l’execution du programme. Que l’évaluation d’une preuve soit ici comparée à un programme avec effets de bord, n’est pas en contradiction avec l’affinité qu’il y a entre les langages fonctionnels et les démonstrations auxquels ils se prêtent bien.

Quand je dis plus haut que le plus souvent, il n’y a qu’un seul contexte à gauche d’un séquent, il ne faut pas oublier que le contexte n’en est pas moins un objet avec sa logique propre, représentation des élaborations du langage objet, et qu’il peut être composé. Par exemple, un contexte peut être constitué de plusieurs ensembles, de listes ou autres, ceci devant être défini préalablement. Il ne faut pas confondre un contexte et ses constituant, qui ne sont pas des contextes (ne sont peut‑être pas suffisants pour ça, ou alors sont regroupés par commodité).

À ce propos, il y a un manque de précision, je me pose une question à laquelle pour l’instant je ne trouve pas de réponse (excepté ce que je crois deviner). Ces contextes doivent bien pouvoir suivre le fil des inférences : comment le font‑ils ? Sont‑il mis à jours ? Est‑ce implicite ? Est‑ce‑explicite ? Quelles versions des contextes se propagent comment ? Ou sont‑ils statiques (pas mis à jours) ? Dans ce cas là, leur contenu statique est dérivé ou posé comment ? C’est important d’avoir une réponse à ces questions, pour une raison que dont je parlerai plus tard.