Les logiques : notes en vrac

Mieux vaut préférer à ces mots trompeurs, d’autres moins ambiguës, par là, en distinguant deux genres de status positifs, deux genres de status négatifs, et pour être complet, un cinquième status encore incertain mais semblant nécessaire :

Réalisé
Non‑réalisé
Réalisable
Non‑réalisable
Indéterminé

Le dernier n’est pas encore certain et est à ne pas confondre avec les variables indéterminées, même s’il y a un rapport entre les deux. Il faut le comprendre comme « le status du terme n’est pas déterminé » (status d’un terme vs status d’une variable).

On peut y distinguer trois groupes : le premier avec le second, le troisième avec le quatrième et le cinquième, seul dans son propre groupe. Le premier groupe correspondrait intuitivement au passé ou au réalisé (positif ou négatif) ou le contexte, le second à l’avenir ou au réalisable (positif ou négatif) ou les bifurcations possibles à partir du contexte, et le troisième, … à un groupe indéterminé (rigolo).

Le choix de mots du précédent message ne convient encore pas, par exemple la notion d’impossibilité fixée, ne se dit pas clairement avec ces mots. En plus, il reste encore à trouver des mots moins trompeurs que vrai et faux et à trouver des mots moins connotés que positif et négatif.

Pour le langage, les règles d’une application du langage, sont des termes, mais évidemment, sans connaître ces termes qui ne sont vus que comme des généralités, peut‑être à la manière dont les hypothèses le sont, mais sans certitude que la comparaison doive être faite. En tous cas, ces termes que sont les règles d’une application du langage, sont du point de vu du langage, une chose avec une partie inaccessible, ce qui évoque une abstraction.

Mais telles qu’elles ont été quelques fois aperçues, les abstractions proviennent plutôt de l’amont, et là, l’abstraction serait en aval.

En même temps, une abstraction peut bien être vue en amont. Du point de vue de l’application du langage, les termes définissant le langage, sont inaccessibles et n’existent que comme des effets. Là aussi, on retrouve une chose avec une partie inaccessible, qui évoque aussi une abstraction.

Il faudrait clarifier ce point. Il y a peut‑être deux notions d’abstraction à distinguer, celles en amont et celles en aval. À moins qu’il ne soit pas correcte de parler d’abstraction dans ces cas là. À moins encore que l’abstraction définie par une équivalence ne soit un troisième genre d’abstraction ou participe à l’une ou aux deux aperçues plus haut. Il faudrait justement étudier les paragraphes précédents en cherchant à savoir s’il s’y trouvent des notions d’équivalence implicites quelque part. Il semble bien y en avoir une quelque part au moins, mais ce sera pour plus tard.

Peut‑être que l’idée vague et intuitive de traduction ou de correspondance, pourrait se décrire comme un auxiliaire de l’équivalence. Quand une règle d’équivalence dit que deux choses sont équivalentes, il manque quelque chose …, cette équivalence suggère l’existence d’une chose existante, mais qui n’a pas de représentation et qui par là, en est virtuelle. Jusque maintenant, l’équivalence est une interprétation définissant une chose, mais cette chose n’a pas de représentation. Ça suggère peut‑être même plus encore, qu’une interprétation, en général, pas seulement l’équivalence, devrait avoir une représentation (plus à ce sujet, plus tard) et que l’équivalence en particulier, le suggère le plus. La production de cette représentation, est peut‑être ce qui se cache derrière l’idée intuitive de traduction. Comme déjà suggéré, une règle que devrait avoir la traduction, est qu’elle est devrait toujours être de un vers un, la traduction ne devant pas confondre ce qui est distinct dans ce qui est traduit.

Le plus important est : une équivalence devrait pouvoir (permettre, pas exiger) produire une représentation, pas seulement autoriser une substitution et la production de cette représentation, serait appelée une traduction. Excepté pour la substitution, peut‑être qu’il devrait en être de même avec les interprétations en général, pour une raison qui sera exposée plus tard.

Une chose me tracasse personnellement, c’est que le langage ne produit pas de représentation du status des vérifications ou des résolutions, et il me semble que ça manque.

Dans le lambda calcul, un résultat a une représentation sous forme d’un terme ayant la même syntaxe (celle du lambda calcul) que le terme qu’on veut calculer. On écrit un terme avec une syntaxe, et en appliquant des règles de ré‑écriture (c’est la vraie nature du lambda calcul), on fini par obtenir un nouveau terme sur lequel plus aucune application de fonction, ni aucune réduction, ne s’applique, on ne peut plus aller plus loin, ce qui signifie qu’on est au bout du calcul, qu’on a le résultat. Ce résultat est lui‑même un terme.

Le langage dont il est question ici, et c’est le cas des autres langages voisins ou de la même famille, n’est pas un système de ré‑écriture. Ça se démontre informellement. Il a été fait remarquer que la substitution qui a lieu pendant la vérification d’une règle, n’est pas une substitution sémantique, au lieu de ça, elle est une substitution par des conditions. La tête d’une règle porte une partie du sens et les conditions de la règle, une autre partie du sens. Alors quand on substitue un terme par ses conditions, on le substitue par seulement une partie de son sens, qui se réduit de plus en plus, jusqu’à qu’il ne reste plus aucune terme à vérifier. Le sens disparaît progressivement pour se retrouver progressivement transféré dans le contexte ou en une seule fois, réduit à un status.

Non seulement il n’y a pas de production d’un terme représentant un résultat, en plus ni le contexte ni le status, n’ont de représentation, alors qu’ils sont le résultat (l’un ou l’autre ou un seulement le second, selon qu’on est dans une résolution ou une vérification).

Il y a bien la notation P true pour dire que P est vérifié, mais c’est une représentation d’un jugement l’on veut vérifier, pas une représentation du status, qui peut être un échec.

On peut se dire que c’est de la responsabilité de l’interprétation externe que de mettre en œuvre la récupération de ce status, sa représentation et son interprétation. C’est possible (et ça souligne encore l’importance des suppositions sur l’interprétation externe), mais avoir une représentation pour ce qui est interprétable, ne peut que être utile et quand c’est possible les définitions sont préférable au vague. Supposer que l’interprétation externe sait s’arranger pour reconnaître un succès ou un échec, suppose aussi que le status ne peut être que Oui ou Non, ou autres status binaires, ce qui semble insuffisant depuis quelques temps.

Il serait utile de pouvoir distinguer au moins un autre status à côté de succès ou échec, le status indéterminé. Il pourrait être utile non‑seulement pour le cas d’une définition du langage n’interprétant pas les variables indéterminé, mais aussi pour une définition du langage pouvant éventuellement répondre à certaines question, seulement dans certains cas et pas dans d’autres. Dans ces conditions, une réponse Oui ou Non est fausse, elle n’est pas correcte, une réponse correcte devrait bien distinguer, Indéterminé, parce que indéterminé, ce n’est ni un succès ni un échec, à moins qu’on ne décide de comparer la status à succès ou échec.

Un autre exemple avait été donné avec l’idée de non‑seulement vérifier si un terme constant est vérifié par des règles, mais de distinguer le cas où il est vérifiée par une seule chaîne d’inférence ou plusieurs, distinguer ce cas où un terme à plusieurs vérifications, par un status spécfcique.

La représentation du status, devrait permettre une distinction parmi plusieurs status possibles. C’est l’idée de constantes dédiées, qui vient le plus facilement.

Des questions se posent. Ce résultat devrait‑il pouvoir être interprétable comme un terme ? Quelles seraient les règles de sa production ?

Une réponse à la première question, pourrait être Oui, à condition qu’il ne soit pas confondus avec les autres termes. La réponse Oui pourrait être justifiée en supposant d’abord une réponse à la seconde question : par substitution dans l’écriture. Dans P true, P serait substitué à un status, qui serait lui‑même un terme, faisant que la notation P true aurait bien un sens et cette notation signifierait qu’on interprète le status pour savoir s’il est true (et seulement true, pas autre chose), ce qui produirait un nouveau status qui se substituerait à P true. Cela signifierait que la notion de conjonction devrait être définie pour ces status, elle le serait par des règles, des règles appartenant à la définition du langage, pas au domaine d’application du langage. L’interprétation de ces status dans une conjonction, devrait être cohérente avec la sémantique. Le status d’après une conjonction de status, serait le status de la règle.

Ces status pourraient faire plus qu’être le status d’une règle, ils pourraient être le status d’un ensemble de règles tentées, comme il y a une notion d’alternatives dans le langage, pas seulement une notion de conjonction. Il faudrait en plus d’une interprétation de ces status dans une conjonction, définir une interprétation dans une disjonction.

L’idée du précédent message pose un problème à résoudre. Comme ce sera abordé plus tard, les représentations internes de la définition du langage, sont inaccessibles à une application du langage. Comment des constates de la définition du langage pourraient‑elles être transmises à une application du langage ? Peut‑être comme des constantes qui auraient un status syntaxique … dans le sens où elles ne seraient pas des constantes ordinaires, mais plutôt des symboles syntaxiquement interprétés. La syntaxe est le seul véhicule par lequel peut passer un échange entre la définition du langage et une application du langage. Ça ne laisse pas beaucoup d’autres options : zéro, oops.

Des constantes avec une interprétation syntaxique, seraient en fait plus des symboles que des constantes. Là encore, se pose une question de vocabulaire, peut‑être que parler de symbole n’est pas très lisible pour exprimer cette distinction.

La conversion entre syntaxe et représentations internes à la définition du langage, se ferait alors dans les deux sens, mais sans être applicable aux mêmes choses pour un sens et pour l’autre (avec le lambda calcul, les deux sens seraient applicables aux mêmes choses).

L’idée d’une interprétation des règles par une substitution d’un terme par son status, a été justifiée par l’utilité de distinguer d’autres status que le simple succès/échec. Même en l’absence de status au delà de cette dichotomie, cette substitution rend la définition de l’interprétation des règles, plus claire. Sans cette substitution, l’échec c’est l’absence de quelque chose et le succès, c’est l’existence de quelque chose. Cette idée que sans correspondance, rien n’existe a été utilisée pour mettre la définition de la syntaxe de côté, en disant qu’il n’y a pas d’erreur de syntaxe, parce que si quelque chose n’a pas de correspondance avec la syntaxe, alors il n’y a juste rien, rien n’est produit et alors il n’y a pas d’interprétation de quoique ce soit. Avec la syntaxe, ça ne pose pas de problème, parce que l’interprétation ne va pas plus loin, il n’y a pas d’interprétation nécessaire d’une erreur de syntaxe, en dehors de « on obtient rien ». Avec l’interprétation des règles, réduire l’échec à une absence de validation, ne marche pas aussi bien. On peut supposer que l’interprétation externe se débrouille pour reconnaître et reformuler cette absence de quelque chose quand il s’agit du status d’une requête, d’une manière qui lui convient, mais cette interprétation existe aussi dans la sémantique du langage, pour chaque condition d’une règle. Pour cette raison, rendre l’échec explicite, peut faciliter sa définition, même en l’absence de status non‑standards.

Dans ISO Prolog, il existe une constante true. Je ne sais pas s’il existe une constante false. Qu’il existe une constante true en ISO Prolog, devrait aider à ne pas s’étonner de l’idée de substituer un terme à son status. Cette constante true d’ISO Prolog, pour représenter une condition unique d’une règle (une seule condition avec succès inconditionnel), avait été mentionnée il y a un peu plus d’un an, mais pas retenue car jugée sans intérêt pour l’écriture des règles, un corps vide signifiant aussi bien le succès inconditionnel d’une règle. Ça reste vraie pour l’écriture des règles, mais ce type de constante est finalement utile pour la définition de l’interprétation, pour donner une existence à l’interprétation, même en cas d’échec.

L’idée que la constante soit produite par substitution d’un terme à une constante représentant son status, ne pose pas de problème quand l’ordre des termes n’est pas important et rend même plus évidente la non‑pertinence de l’ordre des termes dans une conjonction. À condition justement que l’ordre des termes soit toujours non‑pertinent … cette non‑pertinence ne serait alors plus seulement un constat, mais aussi une condition.

Représenter des relations où l’ordre des choses est important, devrait se faire autrement que par l’ordre des termes. Ce ne serait pas une mauvaise chose, comme ça faciliterait la lecture des règles. L’ordre des termes n’est généralement pas important, une règle où l’ordre des termes serait important, pourrait être facilement mal lue. Représenter l’idée qu’une chose vient après une autre, pourrait se faire avec une relation, une imbrication ou une interprétation (plutôt les deux premières).

Dans ce message il est question de constantes, mais comme dit précédemment, ces constantes doivent être distinctes des autres, ne pas pouvoir être confondues avec. Il a été proposé qu’elles auraient un status syntaxique à part, mais il serait aussi possible d’imaginer une syntaxe pour un type de terme à part, à la place. Les constantes seraient interprétées différemment, dans ce type de terme, sans nécessiter qu’elles aient par elles‑mêmes un status syntaxique à part. Ça pourrait être utile pour permettre à une application du langage, de représenter ses propres interprétations des status, mais est‑ce vraiment utile ? Cela ne risquerait‑il pas d’introduire des risques d’incohérences ?

Une colle qui n’a peut‑être pas de réponse possible.

Étant donnée une définition du langage, existe‑il une requête à lui formuler, prouvant qu’elle est bien une définition d’elle‑même ?

Ce n’est peut‑être pas clair, alors il faut un exemple concret. Disons qu’une définition du langage est posée et qu’elle est réalisée. Cette réalisation doit pouvoir reconnaître comme valides, les propres termes de sa définition. Mais ça ne prouve pas qu’elle est une réalisation de sa propre définition, parce que les termes de sa définition ne sont que des termes parmi d’autres. Cette idée naïve est loin d’être une condition suffisante.

Est‑il possible de définir une requête et une réponse attendue à cette requête, prouvant que la réalisation de la définition, est bien une réalisation de la définition ? Est‑ce possible ?

L’idée du précédent message est probablement une folie à oublier. On ne peut pas reconnaître une chose en lui posant une seule question, ce n’est pas crédible.

L’idée de démontrer ultérieurement des propriétés du langage à un moment ou sa définition le rendra assez expressif pour ça, est plus crédible.

L’idée de réduire un terme à son status ne suffit pas à permettre de formuler que l’ordre des termes dans le corps d’une règle, n’est pas pertinent.

La source de la difficulté est peut‑être là : la validation du corps d’une règle nécessite que un terme soit vérifié après un autre, à cause de la possible interdépendance des termes entre eux (l’idée de vérification en parallèle, ne serait applicable qu’avec des conjonctions de termes indépendants entre eux), mais à posteriori, l’ordre des termes n’est pas important pour le status final.

Il n’y a peut‑être pas d’autre solution que de définir la vérification d’une règle avec l’ordre arbitraire des termes d’après leur écriture et de prouver, dès une définition du langage assez expressive, que finalement cet ordre n’est pas important, qu’un ordre est nécessaire, mais qu’il peut être quelconque. C’est spécial comme notion, quand‑même. À quel phénomène réel peut‑elle correspondre ? Dans la réalité, qu’est‑ce qui se construit par étapes nécessairement successives, mais dont l’ordre des étapes n’est au final pas important ? Ou ce phénomène est‑il spécifique à ce type de langage ?

Quoiqu’il en soit, la définition de la conjonction des status, devrait permettre le court‑circuit, c’est à dire qu’elle se réduirait dès le premier status qui le permettrait. Ce point est normalement certain. Même chose avec la disjonction. Le status permettant le court‑circuit, dépendrait des status possibles et il ne serait pas le même pour la disjonction et pour la conjonction.