Les logiques : notes en vrac

Une distinction précédemment faite, à noter à part : il y a deux genres d’abstraction, que sont les abstractions en aval et les abstraction en amont. Ce sont les abstractions en amont, qui peuvent être source de difficultés.

Jusqu’ici, une règle peut être dans trois cas possibles, par rapport à un terme.

Conditionnée par le terme. C’est le cas où une règle doit vérifier une base de faits, pour que la règle soit considérée comme correcte. Ce cas n’est pas nécessaire, il l’est ou pas selon l’approche du domaine.

Justifiée par le terme. C’est le cas dans la preuve de satisfiabilité. Ce cas peut être explicite ou implicite (preuve générée automatiquement) mais est toujours nécessaire pour garantir que la règle a du sens. La preuve qu’un règle admet au moins un terme ne la vérifiant pas, pourrait être considérée de la même manière.

Conditionnant le terme. C’est le cas où un terme est vérifié par une règle. C’est le cas de loin le plus fréquent. Ce cas se distingue des deux précédents, en ce qu’une non‑vérification n’est pas nécessairement une erreur.

Pour le premier et le troisième cas, la relation entre la règle et le terme, est inversée par rapport à l’autre cas (conditionnée vs conditionnante).

Le cas où une règle est considérée comme un terme, est à part, ce n’est pas une relation entre règle et terme. Il est à noter à côté des trois précédents cas quand‑même.

Dans cas, il faut peut‑être plus parler de notation, que de langage.


Parler de catégorisation, pourrait convenir parfois aussi.

C’est l’interprétation, qui fait une variable.

Il a été dit que le langage de base initial, ne vérifiera que des termes constants. Ça peut sembler étrange : si le langage de base peut interpréter sa propre définition, qui utilise des variables, comme cela peut‑être être possible avec un langage qui né vérifie que des termes constants ?

La représentation interne précédemment décrite pour les variable, un terme de la forme (var N) ou N est l’identité de la variable, est un terme constant. En fait, toute écriture est toujours un terme constant. Il n’y a plus de mystère quand on sait que (var N) est sujet à une interprétation spécifique, et que c’est cette interprétation qui en fait une variable. Ceci dit, les requêtes ne pourront pas contenir de ces termes représentant une variable ou pas sans renvoyer une status « indéterminé ».

À noter : une écriture est toujours en elle‑même un terme constant.

Cette vision de l’interprétation par rapport à une relation, semble suggérer que l’équivalence est une forme d’interprétation. Il y aurait alors deux genres d’interprétation. L’équivalence telle qu’elle a été grossièrement définie, se réfère elle‑même à une interprétation, alors peut‑être serait‑elle une interprétation d’une interprétation. Dans ce cas, peut‑être un lien est‑il à chercher entre application d’une règle à une règle et équivalence. À moins que l’équivalence ne soit plutôt à définir sur les relations plutôt sur sur les interprétations … ou sur les deux ?

Ça fait beaucoup de questions, donc à clarifier.

Une petite correction au message précédent, mais qui n’y change finalement rien.

L’équivalence avait été introduite sur les relations, pas sur les interprétations. Cet exemple pratique avait été posé :



L’équivalence serait alors plus une forme d’interprétation, directement. Pourtant, sans raison pour le moment, de penser que l’équivalence ne s’applique jamais à une interprétation, les interrogations plus générales du message précédent (pas celui cité), restent les questions à se poser.

Ni les règles de eq ni les règles de neq, ne mentionnent une condition du genre (name N). Les règles de name y sont implicites. Elles sont implicites dans les décompositions que font eq et neq. On pourrait alors se demander à quoi servent les deux règles de name. L’interprétation name peut être vue comme descriptive, par exemple s’il est dit quelque part, que le terme auquel s’applique eq ou neq, est un terme interprétable comme un name. Pourtant ce n’est pas dit explicitement, et même si ça l’était par une note ou un commentaire, ça resterait informelle. C’est une des raisons pour lesquelles pouvoir vérifier que des règles correspondent à des règles, pourrait être utile. Par exemple ici, une vérification serait que tout terme interprétable comme name, est unifiable à une des têtes des règles de eq et neq, c’est à dire que si (name T1) et (name T2) est vérifié, alors il doit exister une unification avec une tête de règle, pour (eq T1 T2) et (neq T1 T2), mais sans garantie de vérification. C’est cette idée qui a précédemment fait comparer certaines interprétations à des types. Ici, l’interprétation name est comme un type et autant eq que neq sont censées s’appliquer à ce type. On peut remarquer que cette notion distingue nettement interprétation et terme interne (ici aussi appelée relation), comme le terme T est comme extrait de name ou être placé dans eq ou neq.

Ça ne permet pas de rendre les choses plus vraies, mais ça peut les rendre plus dignes de confiance, une sorte de test de salubrité. Ce qui est sûr quand‑même, c’est que ça rend les choses plus lisibles, d’où l’idée de dire que name est descriptive.

Correction d’une erreur dans le précédent message.

Si on a (name N1) et (name N2), l’unification de (eq N1 N2) n’est pas nécessairement possible, c’est celle de (eq N1 N2) ou de (neq N1 N2), qui l’est. Ce qui aurait dut être dit, serait plutôt que si on a (name N), alors (eq N ?) et (eq ? N) et (neq N ?) et (neq ? N), sont unifiables, le point d’interrogation représentant quelque chose dont on ne se préoccupe pas.

Le type ne peut pas porter sur le produit des deux arguments, comme l’unification participe à la vérification, qui peut ne pas être possible. Cela fait une différence importante avec la notion la plus courante des types, qui étant donné le type d’un argument, permettrait d’avoir un type pour le produit des deux. Ce que dit intuitivement le paragraphe précédent, c’est que ce pseudo type, s’appliquerait à chacun des deux arguments, individuellement.

Comme ça ne correspond pas tout à fait à la notion de type la plus couramment utilisée, mieux vaudrait ne pas utiliser ce mot. Parler de couverture serait approprié et moins trompeur.

Une notation fictive pour poser cette couverture à vérifier, pourrait être :

(coverage (eq name name))
(coverage (neq name name))

Ce serait un exemple de règles appliqués à des règles. Cette notation nécessiterait que la constante caractérisant une interprétation soit toujours la première constante d’un terme, sinon la notation n’a pas de sens. Elle se lirait ainsi : l’interprétation eq a un premier argument couvrant name et un second argument couvrant name, idem pour neq.

La couverture ne peut pas porter sur le produit des deux arguments, parce que l’unification est une partie de la vérification de la règle. Mais les deux interprétations eq et neq, ensemble, couvrent bien le produit des deux arguments, et d’ailleurs elles partitionnent ces produits. Par rapport au produit des deux arguments, chacune des deux interprétations couvre moins que le produit et plus qu’elle ne vérifie.

Si ce message ne semble pas totalement clair, c’est normal, mais intuitivement, il peut se comprendre et c’est suffisant pour ce qu’il veut dire.

Comme dit précédemment, cette notation ne participerait pas à la définition des interprétations, seulement à leur description. Elle dirait à quoi s’applique une interprétation, d’une manière immédiatement lisible et la vérification de cette couverture serait aussi un test de salubrité, dans le sens où si elle n’est pas vérifiée, alors il y une erreur dans les règles définissant l’interprétation ou dans l’idée qu’on s’en fait. Ce qui justifie cette notation, c’est que certaines conditions qui pourraient apparaître dans les règles, mais y étant redondantes, elles n’y sont pas écrite et par là, peuvent manquer, mais seulement pour la lecture, pas pour la définition. D’où l’idée de permettre d’écrire ces conditions dans une description d’une interprétation, plutôt que dans sa définition où elle n’a pas une bonne place.

Ce concept ne ferait pas partie du langage de base.

Une autre notation serait plus appropriée :

(coverage (eq N1 N2)) : (name N1) & (name N2).
(coverage (neq N1 N2)) : (name N1) & (name N2).

Elle aurait ces avantages :

Elle représente directement l’intention, qui est de rapporter dans une description, une condition qui n’est pas écrite dans les règles. C’est moins concis, mais ça reste lisible et en tous cas autant lisible que n’importe quelles autres règles.

Dans le cas où la condition implicite porte sur plusieurs termes, cette notation permet de le dire, la notation précédemment proposée ne le permettait pas.

Cette notation n’est pas plus sensible à la position de la constante caractérisant une interprétation, que ne l’est une règle ordinaire, même s’il reste préférable de toujours l’écrire au début du terme.

Cette notation ressemble simplement plus à une règle, qui faciliterait la définition de sa sémantique.

Note : la constante coverage pourrait peut‑être aussi s’appeler dom, pour domain, ce qui serait plus concis est évoquerait la même chose, surtout avec la nouvelle notation :

(dom (eq N1 N2)) : (name N1) & (name N2).
(dom (neq N1 N2)) : (name N1) & (name N2).

Ce serait même plus clair, l’idée de domaine évoquant mieux l’idée de couverture exacte, tandis que coverage pourrait être mal compris comme signifiant une couverture minimale, c’est à dire pouvant être plus large. C’est probablement la notation qui sera retenue ; en rappelant que ce concept ne ferait pas parti du langage de base, seulement d’une définition ultérieure.

Il a été dit que ces cas de règles sur des règles ne participeraient pas aux définitions, seraient des descriptions et des tests de salubrité. Pourtant, elles pourraient servir dans des démonstrations. En effet, cette description, si vérifiée, pourrait permettre de conclure que si N ne vérifie pas (name N), alors N ne peut pas vérifier (eq N ?).

Il faudrait une notation pour ça. Le point d’interrogation a déjà un usage pour les requête et son usage courant le place mal au milieu d’un terme. ISO Prolog utilise le blanc souligné, mais cette notation n’est pas naturelle et peu lisible.