Les logiques : notes en vrac

Une instance n’est pas nécessairement produite par application d’une règle, la production et le constat que c’est une instance de la règle, sont séparés. Les constantes récemment introduites, sont reformulées, elles ont surtout une représentation écrite locale associée à une identité globale.

Il n’y a pas besoin (et ça poserait même des problèmes, comme expliqué précédemment) que les termes d’un discours sont instanciés par des règles. Ce qui est nécessaire, c’est que ces termes du discours, vérifient ces règles (ou soit vérifiés par ces règles), qui sont alors les règles du discours. Il est possible de parler d’un terme vérifié par une règle, comme d’une instance de cette règle, ça a du sens, mais il n’est pas produit par la règle, il lui suffit d’être écrit pour être. S’il ne vérifie pas une règle qu’il devrait vérifier, un terme n’est seulement pas une instance de cette règle. On retrouve la question de pouvoir formuler des choses non‑correctes, sous la seule condition qu’elles soient syntaxiquement correctes, pour ensuite faire une appréciation de leur validité.

Comme il était question d’instanciation de règles parce qu’il y avait instanciation de constantes dans les termes de ces règles, ce qui impliquait l’instanciation de ces règles qui en étaient littéralement des schémas de règles, il faut remettre en question l’idée de constates instanciées aussi, ou plutôt, la reformuler.

Les constantes automatiquement générées ou instanciées, avaient été vues comme nécessaires, pour répondre au besoin d’un nombre variable d’identité, et en plus, un nombre potentiellement important en pratique. Sans le dire, il avait été considéré comme inenvisageable de créer un grand nombre de symboles globalement tous unique. Mais la solution à ce problème existe presque déjà dans certains domaines : plutôt qu’avoir des symboles de porté syntaxique globale, on peut avoir des symboles de porté syntaxique locale. Ici, ils ont pourtant une porté sémantique globale, comme ils représentent des faits qui sont tous globaux et doivent alors faire usage de constantes globalement uniques. C’est en ça qu’il serait éventuellement quand‑même possible de parler d’instanciation. Pour un symbole c locale, un symbol globale c_1 serait par exemple produit et c est en fait un alias local de c_1. Pour ne pas confondre ces constantes qui ne sont écrites que localement mais qui se distinguent globalement, il est préférable de continuer à les distinguer à l’écrit quand‑même et de garder alors une annotation, comme @c, le iota à l’envers qui aurait été préféré, ne s’affichant pas.

Il serait possible de se passer cette notion, mais ça poserait des problèmes pratiques à l’écriture, qu’elle soit manuelle ou automatiquement générée, par un processus de traduction automatique par exemple.

C’est à ne pas confondre avec les objets locaux dans les langages de programmation, qui apparaissent en entrant dans la portée et disparaissent en sortant de la portée. À la limite, ce serait à comparer à des objets locaux statiques, c’est à dire persistants dans le contexte globale, même si on ne peut pas les désigner depuis l’extérieur de leur portée lexical, excepté indirectement par des références transportées par des variables. De même ici, ces constantes peuvent être transportées par des variables, même si on ne peut pas les désigner directement depuis une autre portée. Pour des raisons pratiques, il devrait quand‑même être possible de désigner globalement, ces constantes locales, en associant leur nom local à un nom global unique, soit explicitement, soit implicitement.

Pourquoi doivent‑elles malgré tout avoir une identité globale unique, ces constantes locales ? Parce qu’elles apparaissent dans des faits et que les faits doivent avoir une portée globale. Pourquoi les faits doivent‑ils avoir une portée globale ? Parce que sinon les règles ignoreraient des faits et ne serait alors plus pertinentes (et pourraient peut‑être même ouvrir la porte à des incohérences, mais c’est à voir). Ou plus exactement, les faits doivent avoir la même portée que les règles. Des faits pourraient être locaux, si exclusivement des règles locales s’y appliquaient.

Sans savoir si ça aurait une utilité, il n’y aurait pas d’incohérence à ce que des constantes de portée locale, puissent aussi être écrites dans des règles, où elles seraient aussi des alias locaux de constantes globales, comme expliqué précédemment, et il ne s’agirait pas alors de devoir instancier une règle par nécessité d’instancier une constante.

Jusque là, la seule différence syntaxique entre une règle et une conjonction de termes comme un fait, est dans le premier terme avant les deux points verticaux. Pour les règles, il y a une tête de règle qui peut être un terme composé avec souvent des variables, pour les faits, ce n’est pour le moment qu’une constante servant à désigner la conjonction. Désigner un fait par un terme composé entièrement constant, ne pas serait pas insensé, un terme entièrement constant pouvant remplir le même rôle d’identification, qu’une constante autant unique que ce terme. Il faudrait se demander si ça a un sens, pour un fait, de contenir des variables liées par un terme semblable à une tête de règle. La question reste en suspend pour le moment. En attendant une réponse à cette question, la syntaxe des faits est la même que celle des règles, à la différence que le premier terme avant les deux points verticaux, ne peut pas contenir de variables ou en tous cas, c’est incertain jusque maintenant.

Avant une piste de réponse à la question laissée en suspend, quelques corrections.

Quand il a été dit que les règles ne sont pas pertinentes si elles ignorent des faits, l’intention était de dire que l’application des règles n’est pas pertinente si elle se fait en ignorant des faits. Les règles et l’application des règles, sont deux objets différents même s’ils sont en rapport.

Il a été question d’instanciation de règles de deux manières, ce qui à de quoi égarer. Quand il a été dit que l’idée de l’instanciation était abandonnée, c’est seulement l’idée d’instancié des faits pendant une vérification de règle. L’instantiation qui a toujours existé, pendant la vérification des règles, n’est pas du tout remise en question (ce serait une folie).

Remarque : en fait, si, une règle pourrait instancier un terme comme un fait, mais seulement un terme qu’elle a déjà vérifié. Ça pourrait avoir un usage, pour faire des économie de vérification, mais c’est de l’optimisation (dont le bénéfice peut être mis en doute), pas de la sémantique.

S’est dégagé une forme de stratification, qui sera un concept a intégrer au langage.

S’est posé la question de savoir si les faits sous forme de conjonction, doivent pouvoir avoir un terme semblable à une tête de règle, c’est à dire pouvant contenir des variables, pas seulement des constantes.

Il faut déjà se poser la question du statut des variables dans ces conjonctions. Quand est écrit cet exemple :

procedure-1 : (alloc M (size V)) & (write …) & ….

Quel est le status des variables y apparaissant ? On peut revenir en arrière en se reposant la question du status des variables dans les termes vus jusque maintenant. Ces variables étaient le plus souvent sensées être résolues, et dans le cas où la sémantique est une vérification de termes constants, seulement, les variables non‑liées sont indéterminée (et ce status peut se transmettre sous condition).

Dans l’exemple précédent, on comprend bien intuitivement qu’on écrit des variables là où on veut signifier qu’on a des parties variables, mais ça ne dit pas si elles sont dans le même cas que les variables de termes qu’on vérifie. Aussi, comme il s’agit de termes posés comme des faits, l’idée de résolution semble surprenante ; un fait, c’est un fait, ça ne se résous pas. Pourtant ça ne peut apparemment pas être autrement.

Par exemple dans le terme « (alloc M (size V)) », il est compréhensible que la variable M est contrainte ou partiellement déterminée par la règle correspondante, alloc. C’est bien ce qu’on veut dire, on espère bien dire que M est fixée ou partiellement fixée par l’allocation. Mais ce n’est pas le cas de V, que rien ne contraint et qui dans l’intention, est un argument à ce qui a été étiqueté « procedure-1 ». À priori, rien ne permet de résoudre V. Mais ce n’est un problème, on a vu qu’une résolution peut laisser des variables libres, ce qui nécessite seulement de définir leur interprétation.

Si la résolution de termes posés comme des faits surprend, il faut se rappeler que ces faits posés, sont en fait les termes d’un discours, qui n’est d’ailleurs pas nécessairement correcte ou au moins pas temps qu’il n’a pas été vérifié qu’il est correcte (et éventuellement ensuite, on peut vouloir vérifier d’autres choses à son sujet). Dans un texte en langue naturelle, il y a une part de résolution ; ça peut ne pas plus surprendre.

Les variables apparaissant dans ces termes peuvent donc être résolues, ou partiellement déterminées ou laissées libres. Mais on peut remarquer que l’exemple donné contient un terme inclus, (size V) (*) et ce terme ne représente rien de concret si V est libre. Ça qui va être proposé peut laisser un doute comme ça semble trop directement sauter à l’idée de passage de paramètres comme on en aurait dans un langage de programmation, mais il semble qu’il ne peut pas en être autrement : la variable V doit être déterminé autrement, et donc lié de la même manière que dans une règle, par la tête de la règle.

(*) En fait, il ne devrait pas se trouver là, mais plutôt à côté, comme ce terme est sensé être une interprétation. L’exemple devrait plutôt ressemblé à ceci : « procedure-1 : (size V Size-V) & (alloc M Size-V) & (write …) & …. »

L’exemple pourrait alors être réécrit ainsi :

(procedure-1 V) : (alloc M (size V)) & (write …) & ….

S’il semble douteux de passer si vite à un principe ressemblant tellement à un passage de paramètres, on peut penser aux pronoms dans un texte en langage naturel. Hors contexte, ils ne renvoient à rien de concret. Ce qu’ils désignent est précisé par le contexte, et dans le langage défini ici, la tête de la règle permet de passer un certain terme choisi dans le contexte, à une autre règle. Cette transmission passe par la tête de la règle. Il semble que c’est incontournable avec ces conjonctions posées comme des faits, elles doivent pouvoir avoir une tête contenant des variables, comme les règles.

Syntaxiquement, rien ne semble distinguer ces faits, des règles.

Si syntaxiquement, il n’y a pas de différence en entre un fait et une règle (**), on peut se demander s’il est possible de poser des règles comme des faits et réciproquement, s’il est possible de poser des faits comme des règles.

(**) Pendant longtemps, les règles ont mêmes été considérées comme la représentation des faits, la seule possible.

Un exemple de faits utilisés comme des règles. Disons qu’on a deux fait « proc-2 : op1 & op2. » et « proc-3 : op1 & op2. ». La conjonction est la même, c’est volontaire. Si quelque part on a « proc-3 », on sait qu’on a op1 & op2, puisque la sémantique le dit. Mais la sémantique dit aussi que si on a op1 & op2 on peut vérifier proc‑2. On peut donc à partir de ces faits, dire que si on a proc‑3, on a aussi proc‑2. Les faits ont été utilisés comme des règles. La réciproque est encore plus simple : si les faits sont des règles, alors les règles sont des faits. C’est rassurant, car les règles et les faits avaient été jusque maintenant été tenues pour la même chose.

Pourtant on attend que les termes de ce qui a été appelé le discours, soient vérifiés par des règles après avoir été posés. D’abord, ce n’est pas tellement nouveau, il existait déjà la notion de satisfiabilité des règles, ce qui n’en était pas loin et les termes des règles ont toujours fait références à d’autres règles, ces termes, font seulement référence à des règles appartenant à un autre ensemble.

On pourrait même mélanger les deux, les règles et le discours, ensemble. Si on ne le fait pas, c’est intuitivement parce que les règles qui vérifient les termes du discours seront toujours les mêmes, tandis que le discours constitués de terme, ne sera pas toujours le même. C’est une raison pratique, mais il y en a une autre qui éclaire enfin ce qui s’est laborieusement dessiné intuitivement : une stratification.

Une couche est posée sur une couche sous-jacente. Ce qui a été appelé le discours dans les précédents messages, est avant tout une seconde couche se reposant sur une première. Cette couche pourrait elle‑même être la couche de base d’une troisième couche.

Cette stratification n’est pas seulement pratique, elle peut être une nécessité. Dans les exemples précédents, figuraient ces deux règles : « (alloc M) : (free M). » et « (free M) : (alloc M). » Il avait été expliqué que ce ne sont pas des opérations, mais des conditions, qu’un terme correspondant à une allocation, attend qu’existe un terme correspondant à la libération de ce M et réciproquement. La réciprocité pourrait sembler impossible à vérifier : les deux règles sont mutuellement une condition l’une de l’autre … boum, récursion infinie. Oui, mais pas si on stratifie. Si on stratifie, on pose d’abord ces règles, puis on pose des faits écrits tels‑quels, sans avoir besoin de les vérifier pour pouvoir les écrire, puis ensuite, on les vérifie. Si les faits contiennent les deux termes correspondant, les deux règles sont vérifiées sans récursion infinies, si l’un des deux termes manque, par exemple le discours a un terme (alloc M) mais pas de terme correspondant (free M), alors la condition du terme (alloc M) n’est pas vérifiée et le discours est invalide, sans récursion infinie. En notant au passage, qu’on a une justification à la possibilité de poser des faits avant des les vérifier correctes ; s’il fallait les vérifier en les posant, la même récursion infinie réapparaîtrait. Se pose quand‑même la question de savoir comment les deux règles pourraient être prouvées satisfiables sans discours sur lequel les vérifier. Peut‑être qu’il faut envisager que la satisfiabilité puissent être prouvée avec un exemple de discours et par seulement avec un exemple de terme.

En résumé. Ce qui s’est péniblement dessiné, c’est une stratification en des règles et un discours dont les termes, après avoir été écrits (pas pendant leur écriture), doivent être vérifiés par des règles. La syntaxe des règles et du discours ou énoncé de faits, est exactement la même. L’énoncé de faits peut être interprété comme un ensemble de règles, sous condition que ces termes ait été validés après avoir été écrits, autant que des règles peuvent peuvent être vues comme un énoncé de faits. Tout rassembler en une strate ou organiser en plusieurs strates, peut être un choix libre d’après l’usage ou la praticité ou la lisibilité, mais peut parfois être une nécessité si on a affaires avec des dépendances réciproques.

La notion informelle d’application du langage, mentionnée plusieurs fois, a maintenant une définition formelle : c’est la seconde couche, telle que définie dans le précédent message. La définition d’un langage, est alors la première couche. Comme l’une peut se trouver dans le rôle de l’autre, une application d’un langage peut être la définition d’un langage, ce qui peut s’appliquer même là où on ne le dirait pas comme ça.

Serait‑ce aussi une piste à une méthode de vérification du langage par lui‑même ? La première couche et la seconde couche, auraient alors littéralement le même contenu, pour éviter une régression infinie.

Même si les règles et le discours, peuvent être dans le rôle du discours et des règles, respectivement, ce n’est pas en même temps. Quand le discours a le rôle d’un discours, il n’a pas le rôle d’un ensemble de règles et réciproquement.

L’explication est dans l’exemple de dépendance mutuelle. Les deux règles mutuellement dépendantes étaient :

(alloc M) : (free M).
(free M) : (alloc M).

Un exemple de discours conforme à ces règles :

procedure-1: (alloc This-M) & (free This-M).

Si les deux termes peuvent être validés par les deux règles, sans que la vérification ne tombe dans une récursion infinie, c’est parce que la première règle (validant le terme (alloc This-M) ) va vérifier sa condition avec le fait posé (free This-M) et la seconde règle (validant le terme (free This-M) ) va vérifier sa condition avec le fait posé (alloc This-M). Il n’y aura pas de récursion infinie, parce que la vérification s’arrêtera aux faits posés. Pour la première couche, celle des règles, procedure-1 est un fait posé et appartient à la couche des faits posés, même si procedure-1 peut être utilisé comme une règle par une couche au dessus, par exemple une troisième couche. Pour une couche donnée, toutes les couches en dessous sont des couches de règles, elles ne peuvent pas être des couches de faits et réciproquement, toutes les couches au dessus, sont des faits posés. Par rapport à elle‑même, une couche est une couche de règles.

En résumé : une règle peut être un fait, un fait peut être une règle, mais le status est fixé par la position d’une couche par rapport à l’autre, il n’est pas fixé arbitrairement. En particulier, les deux couches ne peuvent pas avoir le même status l’une par rapport à l’autre. Mais rien n’interdit à deux couches d’avoir littéralement le même contenu.

Sous réserve de futures corrections …

Il serait possible de dire qu’une règle ne fait pas de récursion dans un fait, qu’elle ne peut le voir que sous sa forme en surface.

Il reste des points à éclaircir pour s’assurer que le point de vu des messages précédents est sensé et correcte. Les termes des conjonctions posés comme des faits, sont utilisables par les règles comme des faits vérifiant des termes de ces règles. Mais quel est le status de la tête des faits pour ces règles ? Par exemple dans « (procedure-1 V) : … & … », quel est le statut de (procedure-1 V) pour une règle ? Quel est la status de ce même terme pour les autres faits ? Quand une règle vérifie un terme (r X) par un fait (r Y), elle peut lier la variable Y. Que faut‑il en penser ?

En attendant des réponses aux questions difficiles du message précédent, une colle à propos de l’égalité d’une constante avec elle‑même, puis un retour sur les constantes de la forme @c, temporairement abandonnées.

En revenant aux seules règles et en oubliant un instant la distinction introduite entre faits posés et règles. Un même symbole, une constante, peut apparaître à plusieurs endroits d’un ensemble de règles. Une constante est toujours égale à elle‑même. On a précédemment envisagé que deux choses non‑comparables ne peuvent pas être égales. Voici la colle : si pour un ensemble de règles données, un certain symbole représentant une constante apparaît à deux endroits différents, faisant que ces deux occurrences ne peuvent jamais se trouver en situation d’être unifiées, s’agit‑il toujours bien d’une même constante égale à elle‑même ou finalement de deux constantes différentes, seulement représentées par un même symbole ?

D’un côté, le symbole est la représentation d’une constante et alors la constante est la même quelque soit l’endroit où elle apparaît, ses occurrences. D’un autre côté, ces deux occurrences ne peuvent pas être comparées et alors elles ne peuvent pas être dites égales.

Cette question avait déjà été suggérée, en remarquant que les constantes n’ont pas toujours la même signification partout où elles apparaissent. La question plus haut, est une est une manière de poser la question, formellement. Il sera peut‑être nécessaire de distinguer les constantes et les symboles les représentant.

En parlant de constantes distinctes du symbole les représentant, un retour sur les constantes de la forme @symbole, qui avaient été introduites puis reformulées. Elles ont été reformulées,mais finalement sans rien changer à la définition initiale. La seule chose qui a changé, est qu’elles ne sont plus instanciées par des règles comme initialement, mais par des faits écrits directement. Initialement, les faits été sensés être posés au cours de vérification de règles et ces constantes en même temps. Il a été vu que les faits doivent être d’abord écrits puis seulement ensuite validés par des règles. Mais le nouveau type de constante qui accompagnait cette mauvaise idée initial, est resté. Un symbole @c apparaissant dans un fait posé, génère toujours une constante globale comme par exemple c_1. Ça fait échos à la question plus haut : il y a là une différence explicite entre le symbole représentant une constante et la constante en temps qu’identité.

Ceci dit, cette idée sera temporairement abandonnée. Il faut expliquer pourquoi ce n’est pas un problème de l’abandonner temporairement, et pourquoi malgré cet abandon temporaire, une réintroduction ultérieure est déjà certaine.

Ce que permettait ces constantes, c’était de donner des identités à des choses nombreuses, pour lesquelles il était considéré comme peu envisageable, d’associer une constante pour chaque. Par exemple dans le cas où l’identité correspond à une position dans une séquence d’opération, donner un nom différent à chacune de ces opérations, n’était pas considéré comme crédible (et dans l’idée initiale de règles produisant des faits, c’était même impossible). Par exemple avoir des choses comme (t123456789 alloc M), n’était pas vu comme une bonne idée, d’où l’idée d’avoir plutôt (@t alloc M), où à la place de @t, est générée une constante globalement unique. Quand a été abandonnée l’idée problématique de faire générer les faits par des règles, les symboles comme @t, ont été revus comme plutôt des symboles ayant une portée locale. Par exemple si on a « proc-1 : (@t alloc M) & …. » et « proc-2 : … & (@t free M). », alors les deux @t sont un même symbole, mais de portée limitée à la conjonction dans laquelle ils apparaissent, générant chacun une constante globale différente. En ça, ces constante n’ont pas changé de nature, elles sont toujours instanciées, c’est seulement les conditions dans lesquelles elles le sont, qui a changé.

C’est pratique, mais justement parce que la seule justification est une raison pratique et pas une nécessité sémantique, l’idée sera abandonnée, mais comme il y a une raison pratique facilitant la lecture et l’écriture, elle sera réintroduite. La raison de l’abandonner est de garder la définition de base du langage, la plus simple possible, sans artifice pratique, avec seulement les définitions nécessaires à la sémantique. Pour le moment, ce ne sont des constantes littéralement globales qui seront écrites et non‑pas des symboles de portée locale générant des constantes globalement unique ; au moins pendant un temps.

Il sera peut‑être nécessaire de revenir à l’idée qu’une règle peut générer des faits. Il y a été vu un problème, mais en connaissant la raison du problème (*) : une règle ne peut pas générer comme fait, un terme qu’elle doit vérifier. Si l’idée est réintroduite, ce sera sans ce problème. Au passage, la remarque qu’une règle ne peut pas générer comme fait un terme qu’elle doit vérifier, fait échos à la remarque que pendant la vérification d’un terme, le terme n’est pas encore vérifié, ce qui était la solution à une contradiction rencontrée en définissant la double‑négation pendant une résolution. Ça peut même être dit encore plus généralement : de ce point de vue, depuis l’intérieur d’un terme, le terme englobant n’existe pas. Cette reformulation suggère qu’il faudra correctement définir la sémantique des termes récursifs en conséquence.

(*) Ce qui dit l’utilité, quand une erreur est faite, de ne pas l’effacer, de plutôt conserver son occurrence et de comprendre comment on en est arrivé à la faire et pourquoi elle est une erreur et ce qu’il faudrait pour qu’elle n’en soit plus une. Les erreurs peuvent être autant importantes que les solutions correctes.

Il y a une différence, même si pas techniquement, entre valider et donner du sens, quoique la différence n’est pas toujours si importante. Ce qui a été précédemment appelé des faits, est plutôt un propos. Q’une règle d’une couche en dessous lie une variable du propos, a du sens.




Dans « (procedure-1 V) : … & … », quel est le statut du terme (procedure-1 V) pour un fait :

On peut comprendre qu’il peut être utilisé comme un terme d’une conjonction. Il a été remarqué que parler d’une tête de règle comme d’un terme défini et du corps de la règle comme d’une définition du terme, n’est pas toujours approprié, en prenant entre autre l’exemple d’une règle sans condition dont le terme censé être défini, n’aurait alors pas de définition. Dans le cas présent, l’analogie de la définition correspondrait au contraire, parfaitement. Si on a posé un fait « proc-1 : op1 & op2 », on peut vouloir écrire proc-1 au lieu des deux termes ensemble op1 et op2. C’est compatible avec l’idée qu’une couche, du point de vu d’elle‑même, est une couche de règles. Si maintenant on a « proc-2. », l’équivalent d’une règle sans condition, alors ajouter proc-2 dans une conjonction, équivaut à ajouter rien à la conjonction. L’analogie de la définition, correspond cette fois même dans ce cas. Ça peut surprendre : après avoir dit qu’une couche représentant des faits, est un ensemble de règles de son propre point de vue, on note une différence d’interprétation, en remarquant que l’analogie de la définition qui ne convient pas parfaitement avec les règles, convient parfaitement cette fois‑ci. Ça peu faire se demander si alors les faits sont vraiment des règles de leur propre point de vu. La réponse est oui, parce que quand on parle d’écrire proc-2 au lieu d’une conjonction de termes ou d’écrire proc-3 pour ajouter comme du rien, on ne parle pas d’application de règle, mais d’écriture. C’est quand on écrit les faits, qu’une tête de fait est comme un terme défini dont le corps est la définition, et ce « on », n’est pas une règle en train d’être appliqué. La différence d’appréciation ne doit donc pas surprendre. On est ici dans un le même cas que celui où un terme est substitué par ses conditions pendant une vérification, une réécriture (mais ce n’est pas ainsi qu’on lit une règle, raison pour laquelle l’analogie de la définition ne convient pas tout à fait bien avec les règles, mais convient parfaitement quand on parle d’écriture).

Dans « (procedure-1 V) : … & … », quel est le statut du terme (procedure-1 V) pour une règle :

En supposant que le paragraphe précédent est correcte, on peut noter que le terme peut apparaître, pas seulement comme tête d’une conjonction représentant des faits, mais aussi comme terme dans une telle conjonction. Jusqu’ici, il a été supposé que les termes constituant le discours, sont validé par des règles. Avec ce cas, il y a une question à se poser : faut‑il qu’il existe une règle pour (procedure-1 V) alors que ce terme est déjà défini dans le discours représentant les faits ? Cette question est laissée en suspend pour le moment. En dehors de ce cas, comme les règles ne font pas de récursion dans les faits, quand le terme (procedure-1 V) n’est pas posé dans une conjonction, seulement comme tête d’une conjonction, ce terme est normalement inconnu pour les règles, le cas où il apparaît dans une conjonction étant une question laissée en suspend jusqu’à plus loin.

Quand une règle vérifie un terme (r X) par un fait (r Y), elle peut lier la variable Y ; que faut‑il en penser :

Il y a une seconde question masquée dans la question. En supposant que c’est normal, alors que penser du cas où la solution pour Y n’est pas unique ? Toujours en supposant que c’est normal, dans le cas où il n’y a pas de solution pour Y, le terme n’est pas validé. Dans le cas où il y a une solution exactement, alors considérer que le fait est validé avec une liaison pour Y, n’est pas une problème. Reste à savoir quel sens ça peut avoir. Dans le cas de (alloc M) par exemple, la liaison peut être une adresse mémoire ou un terme permettant de déterminer une adresse mémoire, si elle ne peut pas être déterminée statiquement. Dans le premier cas, la signification est déterminée, dans le second cas, elle n’est que partiellement déterminée. On a une porte ouverte sur le non‑déterminisme, ce qui était inévitable, il ne fallait pas rêver, parce que c’est conforme à la réalité : on ne peut pas prédire si l’allocation sera un succès ou un échec, c’est ce à quoi est lié M qui le déterminera le moment venu seulement. Il faudrait savoir à quoi ça pourrait corresponde en terme de language naturelle. Ceci étant dit, le cas où la variable a plusieurs solutions pourrait faire penser à un cas indéterminé mal formulé, le cas indéterminé devant se formuler avec une solution unique partiellement déterminée. Ou alors, ça peut signifier que le terme a plusieurs sens. La raison de finir ce paragraphe sur ces mots est expliquée juste après.

Retour le status du terme (procedure-1 V) pour une règle :

Il a été noté que (procedure-1 V) peut apparaître comme un terme dans le discours et s’est posé la question de savoir si alors il doit dans ce cas, exister une règle pour valider ce terme du discours. L’existence d’une telle règle peut surprendre, comme ce terme est lui‑même la tête d’une conjonction représentant, une règle dans les faits. À moins qu’il n’y ait une raison d’exclure qu’une règle de validation puisse être définie pour ce terme quand il apparaît dans une conjonction, disons que cette possibilité n’est pas exclue. Mais comme ce terme est déjà un terme défini, on peut au moins aussi vouloir ne pas l’exiger. Alors on se trouve dans le cas où des termes du discours n’aurait pas de règle de validation. On pourrait se dire que ce n’est pas insensé, puisque ce terme est définis dans les faits. Mais imaginons que ce terme apparaissent dans une conjonction, n’ait pas de règle de validation correspondante et ne soit pas une définition dans les faits. Que ce passe‑t‑il ? Ce terme du discours n’est pas validé est donc invalide ? Excepté qu’il n’est pas validé non‑plus, si on exige pas qu’il existe une règle correspondante quand ce terme est défini dans les faits, et que ça ne rend pas le discours insensé, puisque le terme est défini. La clé est peut‑être là, justement : validation vs définition ou plutôt, validation vs sens. Et si les règles ne validaient pas les termes du discours, mais plutôt leur donnait leur sens ?

L’idée qu’il s’agit de donner du sens plus que de valider, doit être justifiée, mais même sans justification, il faut savoir que pour ce qui est d’une mise en œuvre du langage, ça ne fait pas de différence, que la distinction est sans risque pour cet aspect, mais fait une différence pour la compréhension.

Une première justification est une relecture de ce qui a été dit à propos de ce qu’il faut penser d’une variable liée pendant la validation d’un terme. Des exemples ont été donnés en expliquant le sens que ça pourrait avoir, de lier une variable pendant la validation. Mais voilà, ça se comprend plus spontanément si c’est dit ainsi : la variable est liée pendant le processus qui donne du sens au terme. Et on comprend alors que la liaison de la variable fait partie de ce sens, surtout que la justification de cette liaison a été donné en terme de sens. On peut aussi revenir sur le cas où la variable a plusieurs solutions, plus difficile à expliquer comme suite d’un processus de validation, dont on ne sait pas dire s’il a alors échoué ou pas à valider le terme. C’est plus clair dit ainsi : le terme a plusieurs sens possibles, il est ambiguë. Et on peut finir avec une relecture des conclusions sur le status du terme « (procedure-1 V) » pour une règle : il n’a pas besoin d’une règle pour lui donner du sens, puisqu’un sens lui est donné sous forme d’une définition dans les faits. Dans le cas où le terme n’a pas de définition dans les faits, aucun sens ne peut lui être attribué, un cas qui se distingue moins bien du status invalide. Un second cas qui s’en distingue peu, est aussi celui de donner du sens à un terme constant, sans variables. Faute de variable, rien n’est fourni en plus pour lui donner du sens, il est soit sensé tout‑court, soit n’a pas de sens, ce qui est un second cas où donner du sens et valider, se comprend de la même manière.

Pour illustrer l’essentiel du paragraphe précédent, deux exemples . Un convive est invitée à une réunion secrète accessible sur lettre d’invitation seulement. Un taquin arrive et présente le texte d’un discours à la place. Le discours a peut‑être du sens, mais est incorrecte ou invalide comme permission d’entrée. Une équation est posée. Une formule mathématique est donnée en l’avançant comme une solution. La formule peut avoir du sens, mais ne pas être une réponse correcte ou valide à l’équation. Dans l’idée de validation, il y a l’idée d’adéquation et l’adéquation est étrangère au langage, même si on peut la formuler en terme de propriétés devant être vérifiée pour une chose, elle restera toujours étrangère au langage.

Un propos ne pouvant pas être dit vrai ou faux sans poser une question à son sujet, il n’y a pas de raison de donner un status invalide à un propos pour la raison qu’un de ces terme n’aurait pas de sens attribué, même si en pratique il serait utile de le signaler comme une erreur probable. Même sans le signaler, on peut imaginer que ce terme se fera remarquer d’une manière ou d’une autre en posant divers problèmes et qu’il est préférable de le signaler tôt, pour ne pas avoir à remonter à la source de ces problèmes. Formellement, quelle raison y aurait‑il à donner un status invalide à un énoncé syntaxiquement correcte, si ce n’est pas en vérifiant une propriété de cet énoncé, qui elle pourra se conclure par un jugement ?

Il faut aussi revoir ce qui a été présenté comme un discours présentant des faits. Des faits ne peuvent que avoir un sens, alors d’où viendrait la nécessité de règles pour leur donner un sens (hors réinterprétation ou reformulation) ? Ce n’est peut‑être pas un discours posant des faits, plutôt un propos en des termes. Ce qui justifie cette dénomination, c’est que ce qui a été présenté comme un discours sur des faits, était dans les exemples pris, ceux des instructions élémentaires dans un exemple fictif de bout de programme, n’était pas des faits posés, mais une réalisation, plus proche du propos que d’un exposé de faits. Quels faits représentent ces exemples ? Aucun, il sont posés pour eux‑même, avec une finalité quelconque en imaginant que ce soient des extraits d’un logiciel réel. Les faits que pose ces exemples, ne sont rien d’autre qu’eux‑même ; sans avoir été posés, ils n’existeraient simplement pas. Il ne s’agit pas de faits, mais de propos.

Un propos peut exposer des faits, mais un propos n’est pas toujours une exposé de faits. Faits ou propos tout‑court, c’est l’interprétation externe qui le dit, cette distinction est étrangère au langage.

Pour résumer. La seconde couche n’est pas un discours sur des faits, mais un propos, qui peut éventuellement être un exposé de faits. Les règles de la première couche, ne valident par les termes de ce propos, mais leur donne un sens. Ce faisant, des variables peuvent être liées. Si des variables n’ont pas de solution, alors le sens n’a pas put être établit pour diverses raisons, comme une contradiction ou une condition manquante. Si des variables ont plusieurs solutions, plusieurs sens sont possibles pour le terme concerné, il est ambiguë. Si la variable a une seule solution, le sens est fixé, mais si la variable est seulement partiellement déterminée, alors le sens est non‑déterministe pour l’interprétation externe, ce qui est différent de ambiguë. Un terme peut recevoir son sens d’une définition posée dans le propos, mais il n’est pas exclu à priori, qu’une règle de la première couche s’applique aussi, sans savoir encore si ça peut être pertinent ou si ça ne l’est jamais. Il est possible qu’aucun sens ne soit attribué à un terme du propos. Dans ce cas, on peut imaginer que ce terme laissé sans avoir de sens, empêche de vérifier des propriétés du propos ou pas, sans certitude. Que ce terme n’ait pas de sens attribué peut être important ou pas, selon l’interprétation externe, ce qui est étranger au langage. La tête d’une conjonction dans un propos, n’existe pas pour les règles des couche en dessous, parce qu’elles prennent les termes du propos tels qu’ils sont, tel qu’il a été prévu que les règles s’y appliquent, sans appliquer les définition posées dans le propos.

Maintenant il faut aussi distinguer propos et construction, cette distinction est encore plus importante que celle entre propos et faits.

Les propos sont ne sont pas des constructions, ce sont des conjonctions. Les termes restent les seules constructions. Il est quand‑même possible d’imaginer une traduction de l’un vers l’autre, mais elle ne sera probablement pas unique. Les propos sur une construction, peuvent être multiple et si un propos est vu comme la description suffisante d’une construction, l’ordre des termes d’une conjonction n’étant pas important, il est possible que cette description suffisante puisse être concrétisée par plus d’une construction possible.