Les logiques : notes en vrac

Cet exemple illustre une conséquence de deux choses. La première est un mélange de conventions, avec la constante de la relation, en seconde position dans un cas et en première position dans l’autre cas. D’ailleurs, plus que de convention, il conviendrait mieux de parler d’une syntaxe, mais pas au niveau de la définition du langage, au niveau de son utilisation. La seconde, est le double usage de la constante eq (et même de la constante r), mais ça dépend aussi de ce que serait censée signifier cette hypothétique règle (r A B).

Il y a un peu moins d’un an, la notation suivante avait été décidée, pour représenter une hypothèse :



Cette notation avait été choisie, parce qu’elle reprend une sorte de crochet carré, déjà utilisé dans la déduction naturelle pour représenter certaines hypothèses. Les crochets carrés n’avaient pas été utilisés, parce que la notation de la déduction naturelle est moins répandue qu’une autre notation, répandue dès le collège, elle : la représentation d’un interval ou d’une séquence, utilisant ces mêmes crochets carrés, comme dans [0, infini [ ou [1; 2; 3].

L’utilisation de crochets carrés, qu’ils soient à double ou simple bar, n’est peut‑être pas une bonne option, car il semble que dans la déduction naturelle, les hypothèses notées entre crochets carrés, sont des hypothèses disponibles mais non‑utilisées.

De plus, ces crochets carrés à double‑bar ne s’affichent pas toujours bien. Ils s’affichent normalement bien plus haut, mais pas ici : ⟦H⟧ (mais ça dépend des navigateurs et de la gestion des polices de caractères, et ça peut changer au fil des mises à jours, en bien comme en mal).

Comme une hypothèse représente ici, une généralité, c’est à dire l’ensemble de tous les cas possibles d’un terme, peut‑être que les crochets utilisés pour les ensembles, seraient une meilleure idée : {H} au lieu de ⟦H⟧. Pour ne pas risquer d’introduire des erreurs d’écriture, les messages écrits jusqu’ici avec l’ancienne notation, ne seront pas ré‑édités.

Comme dit plusieurs fois, trouver une bonne notation, c’est toujours compliqué, mais c’est nécessaire avec ce qui est récurrent et doit avoir une représentation autant concise que possible.

Ça sous‑entendait une restriction à posteriori, c’est à dire que le type valide ou invalide une écriture. La restriction à priori, qui ne nécessite pas de validation à posteriori, produit un résultat équivalent à d’abord écrire puis filtrer ce qui n’aurait pas dut l’être ou filtrer des solutions non‑acceptables. Contrairement à ce qui a été suggéré à la fin du message cité, cette restriction à priori ne se fait peut‑être pas toujours mécaniquement au détriment de l’expressivité.

La raison de ce qui est dit plus haut, sera expliquée dans un message prochain.

Je ne sais plus si ça avait déjà été dit, alors ce sera peut‑être une répétition ou une reformulation.

Il avait été fait mention d’une règle de certaines logiques, disant que du faux ont peut tout conclure. Il avait été dit que bien que logiquement compréhensible, ça inspire la suspicion.

Un cas où ce serait moins suspect, est quand il faut montrer qu’une hypothèse représentant un cas d’une hypothèse qu’on vient d’ouvrir, n’est pas possible. Si en ouvrant {H} on y trouve {H1}, {H2}, {H3}, si on ne peut pas vérifier X directement à partir de {H}, on doit vérifier X à partir des {Hn}. Mais si disons, {H3} n’est pas possible, c’est un cas à ne pas couvrir. Seulement, il faudrait le démontrer. On se retrouverait alors à démontrer que {H3} est impossible. On pourrait le voir comme une manière de conclure X à partir de l’impossibilité de {H3}, mais on peut aussi le voir comme l’exclusion du cas {H3}, ce qui est encore moins suspect.

Le paragraphe précédent est en oubliant que jusque maintenant, les cas d’une hypothèses, sont générés automatiquement, même si une difficulté concernant cette génération, avait été rencontrée et pas encore étudiée depuis.

Il avait été souligné qu’une spécification n’est pas un programme, même une spécification à l’apparence executable, comme celle dans un langage à la Prolog. Il n’avait pas été dit ce qui les distingue : c’est qu’un programme est un choix de chaînes d’inférence en particulier, alors qu’une spécification n’en impose aucune en particulier, dit seulement lesquelles sont possibles.

Parfois il est plus concis de formuler des règles en supposant qu’elles sont ordonnées, que la première qui correspond, s’applique, et que les autres sont ignorées. Mais ici, l’ordre des règles n’a pas d’importance (excepté pour démontrer leur satisfiabilité), l’ordre des termes non‑plus (sémantiquement, pas en pratique).

Il est quand‑même possible de mimer une relation d’ordre entre des règles, mais c’est plus inutilement verbeux. Un exemple abstrait :

A.
B : not A.
C : not B & not A.
D : not & C and not …

Plus le numéro d’ordre augmente, plus il y a de négations. C’est déjà un problème, mais ça nécessite aussi d’introduire la négation qui ne l’a pas encore été jusque maintenant.

Le langage décrit ici, pourrait donner l’impression d’avoir une notion de relation d’ordre avec l’ordre des termes internes à un terme englobant. Mais il a été dit que à condition que la permutation soit faite partout (ce qui n’est pas trivial à faire automatiquement), cet ordre est permutable, alors ce n’est pas vraiment un ordre.

Serait‑il utile d’introduire une notion d’ordre dans la sémantique du langage ? Ou est‑il possible de s’en passer ? Peut‑être y‑a‑t‑il un choix à faire entre introduire la notion de négation ou introduire la notion d’ordre.

Plus haut, il est montré que la notion d’ordre peut se formuler à partir de celle de la négation, mais l’inverse est aussi possible. Si on suppose que ces deux règles sont ordonnées :

A : …
B : ….

En B, on a non A et montrer qu’on a toujours B, serait équivalent à montrer qu’on a toujours non A.

Ce n’est qu’une ébauche d’idée, mais ça semble être une question à poser. Aussi, en supposant qu’un choix est à faire entre les deux parce que l’un des concepts est exprimable à partir de l’autre et qu’on ne veut pas de redondance, laquelle des deux options s’avérerait la plus souvent pratique ? La notion de négation me semble assez innée, mais formuler des règles en les ordonnant par priorité, permet des formulations concises dans des cas qui ne sont pas si rares. En le disant, je me demande quand‑même si la notion de priorité ne serait pas plus innée que la notion de négation.

Il faudrait distinguer les règles ordonnées des autres, en groupant d’un côté celles qui n’ont pas de relation d’ordre entre elles, et d’un autre, celles qui en ont une et pour celles‑ci, il y aurait même plusieurs groupes.

Une autre question semblant en rapport avec la précédente, mais qui ne l’est pas ; en parlant des termes et non‑plus des règles, cette fois.

Dans le monde de la logique, une séquence d’éléments, comme des constantes ou d’autres termes, est quasiment toujours représentée de cette manière : 

(a (b (c (d ())))) ou (cons a (cons b (cons c (cons d nil))))

Typiquement, il existe une notation plus concise :

[a b c d]

Mais cette notation n’est qu’une apparence donnée à la représentation sous‑jacente, dans le genre des deux précédentes.

Deux choses me chiffonnent avec cette manière de représenter une séquence. D’abord, c’est un arbre dégénéré, alors qu’une séquence et un arbre, ne sont pas la même chose. Ensuite, elle ne peut se prendre que par un bout, avant de pouvoir la prendre par l’autre bout, il faut l’inverser ; la relation entre une liste et son sens inversé, peut être représentée par une règle.

J’ignore si la question de pouvoir la prendre un bout ou par l’autre, indistinctement, est vraiment pertinente. Ce n’est peut‑être qu’une mauvaise idée donnée par le fait de vivre dans un monde spatial, et celui des formules écrites, n’est pas le même.

Pour la question de l’arbre dégénéré, il existe une autre représentation, en apparence similaire, mais qui n’en fait plus un arbre. Cette représentation est constituée de deux listes, liée par une relation pouvant être représentée par une règle aussi.

Des exemples seront plus clairs q’une description. Ci‑dessous, chaque ligne est dérivée de la précédente.

(a (b (c (d ())))) () -- Deux listes, celle de droite et vide
(a (b (c ()))) (d ()) -- Le d est passé dans la liste de droite.
(a (b ())) (c (d ())) -- Le c est passé dans la liste de droite.
…
() (a (b (c (d ())))) -- La liste de gauche est vide.
(() a) b (c (d ()))) -- Le a est passé à gauche.
…

Cette représentation d’une séquence à partir de deux listes, permet de représenter une position dans une séquence, ce qui semble intéressant, pour une séquence et n’est plus un arbre dégénéré, un arbre n’ayant qu’un seul tronc, mais la représentation utilise toujours deux arbres dégénérés.

On avance vers la droite ou la gauche en repoussant à chaque fois, un élément de la liste de un des côtés dans la liste de l’autre côté. On a toujours l’avant et l’après, qui rime bien avec l’idée d’une séquence. La représentation classique, n’a pas des propriétés autant intéressantes.

Je ne sais plus où j’avais vu ce type de structure, alors je ne peux pas donner de référence ni donner son nom.

Une autre idée, pourrait être d’avoir une notion de séquence dans les termes, un peu à la manière dont il serait peut‑être possible d’avoir une notion de relation d’ordre dans les règles.

Le terme (a b c d) ne serait plus vu comme permutable pourvu que les permutations correspondantes soient appliquées ailleurs, il serait vu comme b après a, c après b, etc. Il serait nécessaire de différencier ces termes des autres, pour la cause de l’unification, comme décrit plus loin.

Ça nécessiterait de redéfinir l’unification. Jusqu’ici, l’unification de deux termes n’a qu’une solution ou n’en a aucune. Avec l’exemple plus haut, il serait facile d’imaginer unifier (a b c d) avec (A), mais l’unification avec (A B) (A et B sont des variables), pourrait avoir plusieurs solutions : A = a et B = b c d ou A = a b et B = c d, etc. De même l’unification avec (A B C), pourrait aussi avoir plusieurs solutions. Pour cette raison, il serait nécessaire de distinguer ces termes des autres, pour ne pas altérer le reste de la sémantique du langage.

Avec la représentation précédente, celle de la double‑liste, on trouverait plutôt plusieurs solution vérifiant une règle, pour des variables A et B, mais sans nécessiter de redéfinir l’unification. Le cas a trois variables ou plus, ne serait pas possible.

L’idée d’une notion de relation d’ordre dans les termes (différente de la même idée avec les règles), présente aussi le problème de la décomposition. Comment décomposer le terme (a b c d), si l’unification peut avoir plusieurs solutions ? S’il n’est pas décomposable, il n’est pas utilisable : bien qu’il donne l’impression de pouvoir être pris par n’importe lequel des deux bouts, il ne peut en fait, l’être par aucun.

La première solution qui ne nécessite que de définir des règles sans introduire de nouveau concept sémantique, est peut‑être la meilleure. Mais peut‑être quelque chose d’intéressant se cache‑t‑il dans la seconde solution.

Là aussi, ce ne sont que des ébauches d’idées.

Mais comment montrer qu’on a toujours B, sans montrer qu’on a jamais A ? C’est la négation qui semble plus essentielle et l’ordre des règles qui serait une notion dérivée. Surtout qu’il y a déjà une notion implicite de la négation avec l’échec de la vérification d’une règle et qu’une piste pour définir la négation avait été proposée, avec les hypothèses : montrer que A est toujours faux nécessite de le montrer en général et donc sous des hypothèses (à moins que les termes de la requête n’aient aucune variable libre, directement et indirectement).

Cette idée est abandonnée. Définir des règles en les supposant ordonnées par priorité, ce fera avec un sucre syntaxique qui produira automatiquement les négations nécessaires.

Sémantiquement, elle n’a qu’une solution, même si techniquement, elle peut en avoir plusieurs. Même si techniquement elle peut en avoir plusieurs, le sens reste le même, comme le sens d’une variable liée, c’est son développement complet, récursivement.

Pour revenir à la question, dans l’exemple plus haut, l’erreur est de tenir A et B pour des variables ordinaires, alors que le terme (a b c d) n’est pas tenu pour un terme ordinaire, mais pour une séquence qui n’est pas un arbre dégénéré. Dans ce cas, l’unification de (a b c d) et de (A B) doit se faire en considérant (A B) comme une séquence, ce qui implique finalement de ne pas traité A et B comme des variables ordinaires, mais comme éléments variables d’une séquence. Une solution serait que la séquence (A B) soit liée à la séquence (a b c d), sans séparer A et B. Dans ce cas, l’unification n’a qu’une solution, et de même en unifiant (a b c d) à (A B C). L’unification par la suite, de (a b c d e) et de (A B C) échouerait, l’unification de (a b c d e) et de (A B C D) aurait une solution et l’unification de (a b c d e) et de (D A B C) échouerait. Il faudrait évidemment une autre notation que celle‑ci, pour distinguer ce type de terme.

Un problème que posait cette idée vient d’avoir une solution ; reste celui de la décomposition par l’unification.

Le mot « séquence » n’est pas approprié. La structure à deux listes présentées précédemment, est une séquence : à chaque position, correspond un avant et un après, l’ordre n’est pas arbitraire. Parler de conjonction non‑ordonnée mais non‑permutable est plus approprié. Faute de connaitre un mot pour ça, cette notion sera appelée X, dans le reste de ce message. X = conjonction non‑ordonnée mais non‑permutable en elle‑même ; en espérant trouver un mot à mettre à la place de ce X. Elle n’est pas ordonnée, parce que elle pourrait être permutée, à condition que la même permutation soit effectuée partout, raison pour laquelle elle n’est pas permutable en elle‑même.

Pourquoi voir un problème dans la représentation comme un arbre dégénéré ? Disons que si (a b c d) est un ensemble de constantes dans un ordre arbitraire, d n’est pas après c, b n’est pas avant c, d a seulement une position et b a aussi une position, etc. Dans le cas où d est après c et b avant c, alors la représentation à deux listes est celle qui convient.

Voir (a b c d) comme implicitement (a (b (c (d ()))) pose b sous a, c sous a et sous b, etc. C’est à dire qu’en écrivant (a b c d), pour écrire un ordre arbitraire mais fixé, on est contraint de dire en plus, une autre chose qu’on ne voulait pas dire. C’est le signe d’une grave lacune dans l’expressivité du langage (contraindre à dire une chose qu’on ne voulait pas dire pour pouvoir en dire une autre, oui, c’est grave). Une autre indication qu’il y a une lacune dans l’expressivité du langage jusqu’ici, est qu’il ne permet pas de parler des termes eux‑mêmes, justement pour la raison qu’il ne permet pas de représenter des X. Oui, on peut les représenter comme des listes de termes, c’est techniquement acceptable, mais ça ne l’est pas sémantiquement, pour les raisons données plus haut ; ça permet d’en dire des choses qu’il ne devrait pas être permis d’en dire. Important : il ne faut pas confondre la mise en œuvre et la sémantique et une mise en œuvre, ne doit pas prendre ses représentations internes, pour la sémantique. Par exemple, sémantiquement, l’ordre d’unification des éléments d’un terme, n’est pas pertinent, même si techniquement il peut éventuellement avoir une importance.

Un X pourrait être composé de terme ordinaires composés ou simples (simples constantes). Un terme ordinaire seul, serait un X unitaire. L‘unification du X (a b c) avec le X (A B C), permettrait donc d’unifier A, B et C, individuellement, aux constantes correspondantes. L’unification du X (a b c) avec le X (A B), ne permettrait pas d’unifier les variables indépendamment, elles seraient unifiées ensemble à (a b c), comme décrit dans un précédent message.

Reste le cas où un élément d’un X est un X. Ça peut signifier deux choses : un X sous un autre X, ce qui peut légitimement pouvoir être écrit (ex. un arbre où l’ordre des feuilles ou des branches n’est pas pertinent), ou un X ajouté à un autre X, ce qu’il serait nécessaire de pouvoir représenter pour pouvoir unifier deux X contenant chacun des variables et non‑pas un seul des deux, comme dans tous les exemples précédents, ou pour pouvoir étendre un X.

Comme un X dans un X est un X toujours pas moins plat, il n’y a pas de récursion (même s’il est possible de représenter un X sous un X, c’est à ne pas confondre avec un X dans un X), la syntaxe n’a donc pas besoin d’avoir des signes distincts pour l’ouverture et la fermeture d’un X. Peut‑être que la barre verticale serait une idée ? |a b c| pour représenter le X précédemment noté comme (a b c) ? Cette notation est déjà utilisée pour la valeur absolue, mais la notation [a b c] est, elle, déjà utilisée pour les listes, une notion plus importante à distinguer que la valeur absolue, qui appartient à un autre domaine.

La notation |a b c| ne serait pas un sucre syntaxique, elle correspondrait à une notion sémantique non‑dérivable.

Note : |a b b| ne serait pas la même chose que |a b|, l’absence d’ordre pertinent — mais fixé quand‑même, ne doit pas faire confondre cette notion avec celle des ensembles.

Attention : un texte vu comme une séquence de graphèmes, par exemple, ne pourrait pas être représenté ainsi, parce que c’est une liste ou une séquence, strictement ordonnée. Il est question ici, de conjonction de termes non‑ordonnés et non‑permutables.

En parlant de séquence comme du texte par exemple. La séquence navigable présentée précédemment, pourrait avoir un sucre syntaxique : l’utilisation de [ et ] comme pour les listes, mais avec en plus, un symbole signifiant la position courante. Peut‑être qu’une idée de symbole pourrait être •. Par exemple, [• a b c d] correspondrait à « () (a (b (c (d ())))) », [a b • c d] correspondrait à « ((() a) b) (c (d ())) » et [a b c d •] correspondrait à « ((((() a) b) c) d) () ». La seule présence du symbole • suffirait à distinguer ce type d’expression des autres listes.