Les logiques : notes en vrac

Quand il a été dit que quand un terme d’un propos n’a pas de sens attribué, ça n’invalide pas le propos, pourvu qu’il soit syntaxiquement correcte, ça peut être comparé à la possibilité d’avoir des règles non‑satisfiables.

La satisfiabilité des règles n’a pas été introduite par nécessité sémantique, mais pour raison de pertinence et raison pratique. Pour un ensemble de règles donnés, la vérification d’un terme quelconque, reste définie même si une ou des règles ne sont pas satisfiables. Là, il faut comprendre que la vérification n’est pas nécessairement automatique.

C’est de la même manière qu’il est proposé qu’un terme d’un propos, puisse ne pas avoir de sens attribué, sans que le propos n’en soit invalidé, même si éventuellement rien de pertinent ne pourra en être retiré. Une règle non‑satisfiable peut se trouver n’avoir aucune importance pour la vérification d’un terme. De même, un terme d’un propos sans sens attribué, peut se trouver n’avoir aucune importance pour par exemple vérifier une propriété de ce propos ou le traduire en une construction.

L’idée de la stratification, même si elle laisse encore quelques questions sans réponses certaines, s’accepte bien, correspond bien à la manière qu’on peut avoir de comprendre des choses. Mais cette idée correspond‑t‑elle à une réalité ou seulement à une manière qu’on a d’aborder la réalité, qui ne correspond peut‑être pas à la réalité ?

À quoi correspondrait cette stratification dans des phénomènes physiques par exemple ? Par exemple, les phénomènes physiques à petite échelle et les phénomènes physiques à grande échelle, sont‑ils dans une relation de stratification semblable à celle décrite ?

Une réponse positive serait une indication que cette idée est bonne. Dans le cas contraire, elle laissera toujours un doute sur sa pertinence, quelque soit sa praticité (assez certaine) et sa cohérence (dont il faut encore s’assurer).

Une réponse positive pourrait être informellement justifiée ainsi : le tout ne peut pas exister avant les parties. Mais comment savoir si la réalité est bien ainsi …

À quelle réalité physique correspondrait la dépendance réciproque entre deux règles, qui ne peut être vérifiée que par des termes posés dans une couche au dessus, des termes dans lesquels les règles en question ne font pas de récursion ? C’est cet unique cas qui jusque maintenant, justifie que la stratification, en plus d’être pratique, est nécessaire. Mais existe‑t‑il des phénomènes physiques correspondant à ce cas ?

Concernant la stratification encore, même si l’introduction semble à propos d’autre chose.

Précédemment, il a été proposé de permettre de distinguer des règles comme ne définissant pas des termes, mais vérifiant des propriétés de certaines règles, d’une manière un peu comparable à une vérification de type.

L’exemple était pris d’un fragment d’une possible définition du langage de base. Cette définition inclus la définition de ce qu’est une constante puis définit ce qu’est l’égalité et la non‑égalité de deux constantes :

(const ()).
(const (C)) : (const C).

(eq () ()).
(eq (C1) (C2)) : (eq C1 C2).

(neq (C) ()).
(neq () (C)).
(neq (C1) (C2)) : (neq C1 C2).

Note : neq n’est ici pas la même chose que not eq, mais ce n’est pas important pour le propos.

En précisant que la règle const n’est jamais utilisée, que la seule chose utilisée est la règle eq et la règle neq. D’ailleurs, la règle const n’est même pas utilisée dans les règles eq et neq non‑plus. Dans ces conditions, on peut se demander si la règle const est vraiment nécessaire. En effet, elle ne l’est pas, elle est seulement écrite pour faciliter la compréhension et la description. En fait, elle décrit les arguments de eq et neq, sans que ce ne soit nécessaire. Mais pour s’assurer de la pertinence des règles eq et neq, on voudrait quand‑même s’assurer que le domaine du premier argument de eq, couvre bien le domaine défini par const, et idem pour le second argument (indépendamment, pas simultanément) et idem pour neq. Dans le cas de cet exemple simple, la réponse est évidente, c’est avec des exemples plus longs et plus nombreux qu’il est rassurant de pouvoir le vérifier.

Il avait été proposé que cette vérification non‑formellement nécessaire, mais dont l’utilité est justifiée en pratique, que cette vérification soit posée par des règles à part des règles ordinaires. Il s’agissait de distinguer les règles ordinaires et des règles devant être vérifiées sur les règles ordinaires, un peu à la manière d’un contrôle de typage

Cela peut‑il être reformulé avec la stratification ? Si oui, alors ce serait un bon indicateur qu’elle est bien utile, parce qu’elle correspondrait à un nouveau concept plus général qu’un précédent qu’elle couvrirait. Un concept serait ajouté, mais en faisant l’économie d’un autre.

Solutions multiples tout‑court et solutions multiples comme solution unique. La question se pose après que soit ressortie la question de l’ambiguïté.

La simple négation d’un terme, pose que ce terme n’est pas vérifiable, que toutes ses solutions possibles sont exclues. L’exclusion de ces solutions représente la solution de cette négation, qu’on peut comprendre comme une conjonction d’exclusions. La double‑négation est la négation de la simple négation. Elle pose qu’au moins une solution parmi plusieurs, est possible, ce qui peut être compris comme une disjonctions de solutions possibles.

Dans les deux cas, une solution est définie à partir d’un ensemble de solutions, c’est à dire qu’un ensemble de solutions, « se cache » dans une solution unique.

À moins que ce ne soit à corriger, il a été proposé que quand une règle attribut un sens à un terme d’un propos en liant ses variables, s’il existe plusieurs solution, alors le terme a plus d’un sens possible, il est ambiguë. Mais résoudre une négation ou une double‑négation produit ce qui apparaît comme une solution unique, qui se définit pourtant par un ensemble de solutions. Faut‑il y voir une ambiguïté aussi, quand ce type de solution est produite en attribuant un sens à un terme ?

Pour la simple négation, non, il n’y a pas d’ambiguïté, toutes les solutions sont exclues, il n’existe pas de choix indéterminé. Pour la double‑négation, il semble y avoir ambiguïté, puisque d’abord, s’il existe au moins une solution au choix parmi plusieurs, ce choix n’est pas déterminé. Plus encore, le sens de la double‑négation n’exclus pas que toutes les options soient possibles, c’est alors encore plus clairement une solution ambiguë.

Même si cette réponse s’avérait ne pas être la bonne, la question est à poser : en pensant à l’ambiguïté, il faut en plus de considérer les cas à plusieurs solutions, aussi les cas à solution unique en apparence, qui sont en fait des cas à plusieurs solutions. Cette question est sous réserve de remise en cause de l’idée d’ambiguïté dans le sens attribué à un terme d’un propos.

Parfois la pertinence est distinguée du sens, dans le même registre il est parfois question de cohérence. Il faudrait ajouter à ces trois, le caractère pour une chose, d’être définissable ou définie. La définissabilité ou la définitude ?

C’est ressorti implicitement dans un précédent message, en notant que par exemple même en présence de règles non‑satisfiables, la vérification d’un terme est malgré tout définie, même si la conclusion ou même la possibilité d’arriver à une conclusion, varie.

Une règle ne contenant aucune variable, est‑elle une règle pertinente ?

C’est le cas typique des règles inconditionnelles, c’est pertinent au moins dans ce cas. Mais une règle contenant des conditions et aucune variable, est‑elle pertinente ? Elle pourrait être comprise comme une règle facilement tenue pour pertinente, c’est à dire contenant des variables, mais dont toutes les variables seraient fixées, ce qui arrive pendant une résolution sans faire se demander si c’est pertinent ou pas, tellement c’est normal pour la résolution. Justement, elle pourrait être vu comme une règle avec éventuellement des variables, mais dans un contexte implicitement fixé. Imaginer définir un ensemble de règles tout en définissant un contexte initial non‑vide, ne semble pas insensé et pourrait faire penser à une paramétrisation.

Cette question est venue en essayant d’imaginer ce que pourrait inspirer l’idée d’un propos écrit avec seulement des termes constants, dans l’espoir que ça puisse donner des pistes de réponses aux questions que pose encore l’idée de la stratification. Ça n’aboutit à rien, excepté à la remarque plus haut qui n’est pas sans intérêt.

Une tentative de répondre à une question précédemment posée, celle de la pertinence de deux règles mutuellement dépendantes, la stratification n’ayant eu comme seule justification par la nécessité, ce cas, qui n’a encore qu’une justification dans un exemple tiré de l’informatique, et il manque un exemple tiré d’une chose concrète en dehors de ce domaine, de la préférence un exemple en physique. La tentative est un échec, mais amène à prendfre des notes qui ne sont pas sans intérêts.

On peut imaginer deux astres pas trop éloignés l’un de l’autre, peu importe où dans l’Univers. Le mouvement de l’un dépend de celui de l’autre et réciproquement. Ça se représenterait peut‑être assez bien par deux règles mutuellement dépendantes, comme le sont alloc et free dans des exemples précédents. Mais il y a une différence. Alloc et free, sans stratification, entrent dans une récursion infinie n’aboutissant à rien. Dans le cas de la définition du mouvement de ces deux astres, on peut imaginer intuitivement qu’on aurait bien une récursion, mais qui sera une suite convergente, qui donnera pour un certain instant, le mouvement d’un des deux astres, selon son propre mouvement instantané et celui de l’autre. La suite ne sera peut‑être pas finie, mais plus on la poursuivra plus le résultat sera précis. Je ne fais qu’imaginer que ça peut se poser ainsi, mais je crois assez que oui.

C’est à la fois proche et différent du cas de alloc et free. C’est proche, parce qu’on a bien une récursion infinie, mais c’est différent parce que dans le cas des astres, elle tend vers quelque chose, tandis que rien n’évolue durant la récursion entre alloc et free. Cette différence peut être vue comme un non‑problème, le domaine n’étant pas le même et la similitude assez importante.

Il y a un autre point commun, sans différence cette fois. En imaginant cette suite qui donne le mouvement d’un astre selon son propre mouvement instantané et celui de l’autre, on va devoir poser simultanément deux paramètres, celui du mouvement du premier astre et celui du mouvement de l’autre. Ces deux paramètres sont posés simultanément, l’un n’est pas une fonction de l’autre. Il en va exactement de même avec alloc et free utilisés avec une stratification, alloc étant vérifié par un terme free posé dans le propos et free étant vérifié par un terme alloc posé dans le propos, les deux termes étant perçus comme posés simultanément, même si techniquement, on écrit l’un après l’autre, ils sont tous les deux là en même temps quand le propos a fini d’être écrit. C’est justement des les poser simultanément, ne produisant pas l’un à partir de l’autre, qui permet de ne pas entrer dans une récursion infinie.

La stratification permet de poser comme simultanée, des choses qui avec des règles, devraient se dériver l’une de l’autre, tout en permettant quand‑même de vérifier que ces choses interdépendantes, sont comme le disent ces règles.

Mais l’exemple n’est pas si bon. Dans le cas de la série que j’imagine infinie et convergente, donnant le mouvement d’un astre à partir du sien et celui d’un autre, les deux paramètres pourraient être posés simultanément, aussi comme arguments d’une interprétation, ce qui n’est pas le cas de alloc et free, avec lesquels ça poserait problème, leurs arguments étant nettement plus contextualisés.

Avec ces deux derniers, utiliser un argument serait au minimum, peu fiable. Imaginons qu’on passe à alloc, un argument représentant un terme free et réciproquement pour free. On exprimerait pas le fait que les deux arguments doivent exister conjointement, on pourrait vérifier alloc en passant un terme free sans jamais vérifier free avec un terme alloc, et même si on le faisait, ces termes pourraient être dissociés, provenir de deux mondes différents, sans que les règles ne puissent l’invalider. Si on représente la paire, par une interprétation attendant deux arguments, se pose deux autres problèmes. On ne peut plus aborder la validité de l’un seul, même si en terme de l’autre, alors que c’est pertinent de pouvoir le faire, pour une opération. Les deux arguments peuvent venir de nul part, être dissocié de tout et si on veut les associer à quelque chose, il faut compliquer leur formulation. Dans le cas du propos comme une couche au dessus des règles, les termes alloc et free font partie d’un tout auquel ils sont implicitement associés. En théorie, il ne doit pas être impossible de faire sans, mais il faudrait définir un terme représentant ce tout qu’est le propos, extraire certains de ces termes, tout en représentant un lien entre les termes extraits et le tout, et l’interprétation validant une paire alloc et free, devrait vérifier la validité de ce lien et vérifier que les deux termes en argument en font bien partie. Ce serait reformuler le même concept sans vouloir l’utiliser, avec des complications dans les termes et les règles, sans aucun avantage. Pour comprendre ces lamentations, il faut se souvenir que ces termes sont par exemple associés à une identité représentant leur position dans une séquence d’opérations, ce qui rend délicat leur disassociation d’avec le tout d’où ils proviennent.

En résumé. L’analogie dans le domaine de la physique, qui était bien pressentie, n’est pas une réponse à la question, même si c’est un cas intéressant. On peut conclure que la stratification a bien un important intérêt pratique, du moins, que s’en passer peut être plus lourd que de faire avec, mais ça ne fait toujours pas la justification sémantique concrète attendue.

Une reformulation d’une tracasserie restant à aborder et la raison pour laquelle trouver une bonne justification à la stratification, serait rassurant.

Une tracasserie restante a déjà été décrite, mais mal imagée. Ce qui suit un exemple d’extrait de propos, assez court.

proc-1 : op1 & op2.
proc-2 : op1 & proc-1.

op1 et op2 sont sensés avoir un sens donné par des règles sur lesquelles se reposent le props (la couche du dessous). proc-1, quand il apparaît dans la première ligne, n’est pas sensé avoir un sens donné par une telle règle, parce que ce n’est pas un terme du propos, mais une définition ou une règle du propos. Mais quand le proc-1 apparaît dans la seconde ligne, en temps que terme cette fois, il pourrait en principe recevoir une signification d’une règle de la couche du dessous. Le problème est que le proc-1 de la seconde ligne, a une signification qui lui est donné par la première ligne. Avoir les deux, à la fois qu’un terme du propos ait un sens d’après une règle de la couche du dessous parce qu’il est un terme, et à la fois que son sens n’ait qu’une origine, ce qui est une attente raisonnable pour ne pas avoir à arbitrer (bricolage très douteux), semble un problème non-résoluble. De quoi se demander si ce type de construction est vraiment une bonne idée. Une solution proposée a été qu’un terme, peut, mais n’est pas pour autant obligé d’avoir un sens donné par une règle de la couche du dessous. Ça a été justifié par le fait qu’une règle non‑satisfiable dans un système de règles, n’empêche pas d’utiliser ce système de règles. Mais le cas n’est que vaguement similaire, du moins pour servir cette justification, comme la possibilité pour un terme du propos de ne pas être associé à une règle, doit être en effet conservé.

Cette tracasserie est celle qui laisse le plus de doute sur cette construction qu’est la stratification qui en semble bancale. C’est la raison pour laquelle il lui faudrait une justification indiscutable, qui en plus donnerait peut‑être une piste de réponse à la tracasserie plus haut. Aussi, comme cette construction a surtout des justifications pratiques, c’est même comme ça qu’elle est progressivement venue, en s’arrêtant dessus, il y a un risque de passer à côté d’une éventuelle meilleure construction, plus justifiée sémantiquement et répondant aux mêmes attentes pratiques.

Une réponse à la question non‑résolue du message précédent et une justification sémantique et non‑plus seulement pratique, à l’idée de stratification.

La réponse à la tracasserie du précédent message, est trouvée en oubliant un instant la stratification, ce qui peut sembler inattendu ; pourtant c’est la description qui a été faite de la stratification, qui le justifie.

Rappel du cas discuté dans le précédent message :

proc-1 : op1 & op2.
proc-2 : op1 & proc-1.

Où op1 et op2 sont correspondaient à des règles de la couche du dessous. Comme on oubli un instant la stratification, on ramène tout à une seule couche et pour cela, on ajoute ce qui était sensé être défini dans la première couche :

op1: ….
op2: ….
proc-1 : op1 & op2.
proc-2 : op1 & proc-1.

Rien ne semble étrange. Mais la tracasserie n’était pas là, elle était dans l’apparente ambivalence possible de proc-1. De quoi a l’air cette couche unique, si on imagine que la construction a deux couches définissait proc-1 à la fois dans le première et dans la seconde couche :

op1: ….
op2: ….
proc-1 : ….
proc-1 : op1 & op2.
proc-2 : op1 & proc-1.

C’est étrange, il n’y a plus rien de bizarre, rien qui tracasse. Mais que s’est‑il donc passé ? On vient de remarquer que proc-1 est simplement une règle à deux clauses comme il en a été vu plusieurs exemples. À trop se concentrer sur la distinction entre les couches, à trop se concentrer sur le status particulier qu’elles peuvent avoir, on peut trop les isoler. La stratification se dérive du seul modèle connu jusqu’à il y a peu, celui d’un unique système de règles. En introduisant la stratification par ses justifications pratiques (une justification sémantique vient plus loin), il a été dit que dans certains cas, on peut décider librement de stratifier ou pas, qu’on peut toujours si rien ne l’empêche, mettre ensemble un propos et les règles sur lesquelles il se repose. C’est ce que fait la reformulation plus haut. Maintenant on revient au modèle stratifié, mais cette fois en montrant les deux couches :

op1: ….
op2: ….
proc-1 : ….

proc-1 : op1 & op2.
proc-2 : op1 & proc-1.

proc-1 est définie dans la deuxième couche et dans le première, mais ça ne devrait plus faire s’alarmer après ce qui a été dit : proc-1 est défini par deux clauses différentes. Il ne faut pas trop insister sur la séparation des deux couches, pour le percevoir. Disons alors que le terme dans la deuxième ligne, est ambiguë, une question sur laquelle il faudra revenir plus tard, mais plus rien de bancal en tout cas.

Pourtant, que la seconde couche puisse se comprendre en partie en la plaçant au même niveau que la première, si la stratification s’est introduite avec autant d’insistance, il doit y avoir une raison et des différences entre les deux couches ont été soulignées. C’est justement là que se cachait la justification sémantique.

Il a été dit que les termes de la couche du dessus, les termes du propos ou de l’exposé de faits selon les cas, sont des faits pour la couche du dessous. C’est à dire qu’un terme est vérifié par la couche du dessous, par le fait qu’il est présent dans la couche du dessus, sous réserve qu’il corresponde bien, ce qui illustré dans un prochain message.

Dans le modèle précédent, celui sans couches, une règle était vérifiée en produisant des solutions pour ses termes de manière à vérifier ses conditions, étant données des liaison de variables passées par la tête de la règle, ce qui a été appelé la résolution. On entrait dans la règle par la tête, pour ensuite suivre ses conditions. Avec la stratification, les termes de la couche du dessus, entrent dans le corps de la règle pour la vérifier et vont éventuellement lier des variables dans la tête de la règle, c’est le chemin inverse. Une analogie avec la physique va permettre de comprendre la pertinence de ce chemin inverse.

Un système physique quelconque, est décrit par des lois de la physique. Ces lois sont pressenties et posées d’après des observations de phénomènes. Puis elles sont vérifiées sur grand nombre d’instances diverses et variées de ces mêmes phénomènes, c’est à dire que cette fois on observe le phénomène pour voir s’il correspond bien aux règles définies.

Comment peut‑on suivre la même démarche avec l’ancien modèle sans couches ? Réponse cinglante : on ne le peut pas. Tout ce qu’on peut faire avec, c’est générer quelque chose qui vérifie les règles, produire des solutions aux règles, pas vérifier que quelque chose qui n’a pas été généré par les règles, vérifient bien les règles, est bien une solution aux règles, puisque qu’on ne passe pas ses termes à une règle, que au lieu de ça elle les solutionne. C’est même incorrecte pour vérifier qu’une chose correspond à des règles, puisque la règle ne peut que générer ce qui la confirme, et pour la démarche qui nous intéresse en ce moment, il devrait être possible d’infirmer.

Pourtant, on a bien utilisé l’ancien modèle pour vérifier par exemple que des termes correspondent à des règles. Oui, mais des termes isolés seulement, pas des conjonction de termes (la différence sera expliquée dans un prochain message) et pas des termes du corps de la règle. Pour preuve que cette démarche n’était pas possible, un exemple simple :

(r A) : (x A) & (y A).

Étant donnée cette règle, on aurait put faire une requête comme par exemple « (r abcd) ? », pour vérifier si le terme peut permettre de vérifier les conditions de la règle, mais on avait aucun moyen de vérifier directement qu’une conjonction « (x abcd) & (y abcd) », vérifie la règle et produise un (r abcd) en conséquence (c’est le cas de le dire). En vérifiant (r abcd), on vérifiait qu’il existe une ou plusieurs solutions pour la condition « (x A) & (y A) », on avait aucun moyen de vérifier qu’une certaine conjonction, comme « (x abcd) & (y abcd) » est une telle solution à la condition de la règle.

L’exemple pris précédemment, celui du mouvement de deux astres, correspondait plutôt à l’application d’une règle pour faire un calcul, pas à la vérification qu’un mouvement observé correspond bien à la règle qu’il est sensé vérifié.

On a une application à la physique, ce qui est un bon signe de pertinence et on constate le caractère général de ce qu’apporte la stratification, qui s’en trouve solidement justifiée, normalement.

D’autres commentaires viendront, pour compléter.

Une requête comme « (x abcd) & (y abcd) ? » était possible aussi, mais ne faisait que vérifier que la conjonction, ne vérifiant toujours pas qu’elle remplit les conditions de (r A).

Ce problème avait déjà été rencontré pendant les expériences de petites démonstrations. Étant donné une règle comme « C : A & B », ne pouvant pas faire de vérification automatique que A & B vérifie C, il avait parfois été tenté de faire une vérification automatique de la conjonction A & B & C, en supposant que C était vérifié sous le contexte A & B, mais ce n’est pas idéal, si on note que l’ordre des termes d’une conjonction est sensé être sans importante : dans cette conjonction, B est autant sous le contexte A & C que C est sous le contexte A & B.

Cependant, dans le brouillon de langage de démonstration qui avait été esquissé, il était possible de vérifier C à partir de la conjonction A & B, A et B étant vérifiés dans un même contexte.