Les logiques : notes en vrac

Il existe un cas particulier de l’implication, sans savoir s’il est important de le distinguer. Ce cas particulier, c’est le cas particulier .

Si on a une proposition (P1 A) et une proposition (P2 A) tel que (P2 A) implique (P1 A) mais pas la réciproque, ont peut dire que (P2 A) est un strict sous‑type de (P1 A), mais en langage courant, on l’appellerait plutôt un cas particulier (du moins si le cardinal de l’ensemble défini par (P2 A) est assez petit par rapport à celui de l’ensemble défini par (P1 A) ).

Cette définition du cas particulier est bien un cas particulier de l’implication, parce que quand on écrit (P2 A) ==> (P1 A), l’objet ou le sujet des deux propositions, est le même, A.

Trois autres exemples sur ce que les types ne permettent pas d’exprimer alors que ce serait parfois nécessaire. Les deux premiers exemples sont deux autres illustrations pratiques intéressantes, le troisième pose un problème plus délicat, au point de remettre en question le langage.

Les deux premiers exemples d’abord ; le troisième sera décrit dans un message suivant. Ce message‑ci n’est pas d’une grande importance, il complète seulement ce qui a déjà été dit par deux illustrations assez concrètes.

Le premier est celui des nombres avec des dimensions. Avec les types, il est pénibles de traiter correctement des nombres avec unités, comme des vitesses, surfaces ou plus complexes. Il faut contourner le système de typage, ce qui n’est pas toujours permis ou alors abandonner l’idée de typer les valeurs selon leurs dimensions ou compliquer les choses en redéfinissant toutes les opérations mathématiques sur autant de types différents qu’il y a de combinaisons de dimensions. C’est une des illustrations les plus parlante des limites des types. Dans certains domaines, c’est un problème.

Le second exemple nécessite d’exposer un peu plus des circonstances. Posons qu’on a deux domaines. Pour être concret, disons que le propos de ces deux domaines sont des mots, au sens de ceux d’un texte. Le premier domaine définit des mots qu’il distingue en particulier et il se trouve que tout ces mots commencent par une majuscule. Il les distingue par des constantes les désignant, mais pas plus, il ne leur donne pas un type plus particulier qu’aux autres mots. Posons un second domaine dépendant du premier, et pour celui‑ci, les mots commençant par une majuscule sont tellement différents des autres, qu’ils n’ont pas le même type. Le problème peut se poser ainsi : des fonctions du premiers domaines devraient être utilisées dans le second domaine, mais elles sont définies dans le premier domaine, elles ne distinguent pas des types que le second domaine distingue. Soit, on peut contourner le problème en dupliquant toutes ces fonctions dans le second domaine. Devoir le faire est un mauvais signe, mais ce n’est pas impraticable. Ça devient plus impraticable si vient un troisième domaine, dépendant des deux premier et qui doit utiliser les mêmes fonctions : il ne peut pas faire cohabiter celles des deux domaines, à moins de cette fois créé un domaine de toutes pièces, qui sera une duplication des deux autres domaines, mais aussi en les redéfinissant en partie pour leur permettre de communiquer, ce qui est plus pesant et encore plus mauvais signe que dans le premier cas.

Une solution plus convenable est que le type ne soit pas soudé aux choses, mais qualifie les choses. Par exemple, au lieu d’avoir un type pour les mots commençant par une majuscule dans le second domaine, posant problème parce que les mots du premier domaine commençant par une majuscule ont le même type que tous les autres mots, la solution vraiment convenable, est de pouvoir qualifier certains mots du premier domaine, comme étant du type défini par le seconde domaine. Et justement, les types ne le permettent pas. C’est un cas particulier de l’impossibilité de la duplicité avec les types, dont il a été question précédemment.

Le troisième exemple, plus délicat, est important et sera décrit un peu plus tard.

La troisième chose que les types ne permettent pas d’exprimer, est de cette forme : on a une fonction f et une fonction g, la fonction g prend en argument une valeur produite par f, avec des précisions qui seront ajoutées plus loin. Jusque là, il suffit de créer un type pour la valeur produit par f et poser que l’argument de g est de ce même type. Mais si vient une autre précision, ça se complique : g ne peut être appliquée qu’à une seule valeur produite par f, une valeur quelconque, mais une seule.

C’est encore abstrait, alors le poser et donner une interprétation, sera plus compréhensible.

type a = …
type b = …
type t = …
f: a -> t = …
g: t -> b = …

x = f (a1)
y = f (a2)
z = g (x)

Disons que l’exemple ci‑dessus serait correcte, mais pas celui‑ci :

x = f (a1)
y = f (a2)
z1 = g (x)
z2 = g (y)

Cet exemple serait incorrecte, parce que g est appliquée à x, puis à y, alors qu’elle ne devrait être appliquée qu’à un des deux, n’importe lequel des deux, mais un seul des deux.

Dans un langage comme SML et peut‑être d’autres, on pourrait le mimer par masquage, en écrivant par exemple ceci :

x = f (a1)
x = f (a2)
z = g (x)

Dans ce cas, le second x masque le premier et g ne s’applique qu’à x.

Une autre variante qu’il est autant impossible d’exprimer avec les types, c’est le cas où g ne doit être appliqué qu’une seule fois à x. Cet exemple serait correcte :

x = f (a)
z = g (x)

Cet exemple serait incorrecte :

z = f (a)
z = g (x)
z = g (x)

C’est encore trop abstrait, alors peut‑être que ce sera plus compréhensible en disant qu’il s’agit d’une formulation des effets de bords. Dans un langage fonctionnel, les effets de bord n’ont normalement pas lieu d’être, mais on peut vouloir des effets de bord, non‑pas pour des raisons techniques ou pratiques, mais pour des raisons de sens, pour des raisons d’accord avec la réalité : on ne peut pas commencer une même chose deux fois ou la finir deux fois.

Même en terme de relation et de résolution, ça ne semble pas pouvoir être exprimé, et pire, il semble même se poser une contradiction : g s’applique à un x qui vérifie quelque chose, ce x peut avoir plusieurs solutions, et g peut s’appliquer à chacune de ces solutions, mais dès que g est appliqué à une solution de x, alors x ne devrait avoir plus qu’une seule solution. C’est simplement insensé pour le langage tel que discuté jusqu’ici.

Ça peut pourtant du sens, parce que dans la réalité, quand on est arrivé en bas d’un escalier, on ne peut pas en redescendre une seconde fois sans le remonter d’abord. Ça a même un sens en physique, le paragraphe précédent évoquant facilement le comportement d’une particule dans — réellement ou virtuellement, je ne sais pas — plusieurs états superposés, tout ces états étant tous possibles, se trouvant subitement ne plus avoir qu’une seul état possible si elle « s’effondre » dans l’un de ces états sous l’effet d’une action externe à elle‑même.

Mais comment justifier qu’un terme ayant plusieurs solutions possibles, n’ait plus qu’une solution possible dès que ce terme est utilisé dans la solution d’un autre terme, sachant que ce second terme, pourrait aussi bien avoir été résolu avec le premier terme ayant n’importe laquelle de ses solutions possibles.

Il y a deux moyens de rendre impossible ce qui était possible ou de réduire un ensemble de solution : la suppression de règles, mais aussi, comme vu précédemment, l’introduction de règles ! La première solution ne serait pas facilement acceptable, la seconde le serait plus facilement, mais resterait difficile à justifier.

Pourtant, même sans justification, la seconde solution aurait une certaine harmonie, ce qui n’est au moins pas un mauvais signe. En effet, elle pourrait signifier que la résolution du second terme en utilisant le premier, libère une règle dans le contexte courant (et les contextes qui en dérivent), cette règle ajoutée dans le contexte, faisant que les autres solutions qui étaient possibles avant pour le premier terme, ne le sont plus. Ce serait harmonieux, parce que les contextes de résolutions, pouvant contenir des règles, n’auraient plus rien de différent du contexte globale, qui n’aurait rien de plus particulier que d’être un contexte initial. Reste que ça ne fait pas une raison d’ajouter cette possibilité au langage, sans compter que cette idée est vague en l’état, ne donne pas d’exemple concret de terme et de règle ajoutée au contexte, faisant que ce terme ayant plusieurs solutions n’en aurait plus exactement qu’une seule après l’ajout de cette règle. Un exemple trivial serait une règle qui contraindrait directement le terme à sa solution au moment de son utilisation, mais personnellement, cette idée me semble douteuse, être difficilement justifiable par un sens quelconque.

Même si ça pose plus de questions que ça ne résous le problème, le côté harmonieux de la solution peut inviter à ne pas l’abandonner trop vite. Ce qui inviterait encore plus à s’y intéresser, serait d’avoir en plus, une répondre à cette question : cela a‑t‑il du sens d’ajouter une règle dans un contexte, et si ça en a un, quel serait ce sens ? Il faudrait illustrer avec un exemple ancré dans le réel.

Dans les contextes, il a déjà été évoqué la possibilité de pouvoir ajouter depuis un contexte quelconque, des hypothèses, dont la satisfiabilité est à démontré à posteriori au moins. Mais une hypothèse n’est pas comme une règle. Ça ne correspond pas, parce qu’il n’y a pas à démontrer ultérieurement l’existence d’un fait constaté immédiatement. Seule une règle peut représenter un fait.

Un autre cas doit aussi pouvoir être exprimé :

x = f (a)
x = f (a)

Où les deux x ont une valeur quelconque et ne sont pas les mêmes, tout en vérifiant quand‑même l’égalité avec eux‑mêmes.

Dire qu’une fonction renvoi une valeur fixée mais non‑déterminé, ça devrait être possible, mais dire qu’elle ne s’évalue pas à la même chose avec pourtant le même argument, c’est impossible à exprimer dans le sémantique décrite jusque maintenant. Ce qui serait plus crédible, ce serait que après avoir été évaluée, la première fonction disparaît et est remplacée par une autre ayant exactement les mêmes propriété, mais pas la même. Dans ce cas, que les deux x ne soient pas les mêmes, passerait mieux.

En fait, c’est le propos de la logique linéaire, qui porte bien son nom. Dans les cas d’un message précédent, on peut parler d’objets qui suivent une ligne ou une trajectoire, qui n’a qu’une origine et ne bifurque jamais ; c’est ce qu’on veut quand on traite avec des effets de bord, et pas seulement. Mais cette fois, le cas est différent.

Il n’est peut‑être nécessaire de reformuler la logique linéaire qui me semble compliquée, il serait suffisant de pouvoir formuler les cas présentés, pourvu que ce soit d’une manière qui fait sens.

L’idée précédente que la vérification d’un terme libère une règle dans le contexte, n’est pas dans la possibilité de libérer une règle dans le contexte, ça ne présente pas de risque d’incohérence, même si ça complique les démonstrations de généralités. Le problème est de savoir quel sens ça a. Surtout qu’il n’est pas certain que cette idée de déposer une règle dans le contexte, soit vraiment une bonne approche. Un problème similaire allant finir par se poser avec la modularité, il devrait être résolu quand‑même, mais il aura une justification pratique, pas sémantique, ce qui n’est pas assez pour introduire la même idée dans le cas présent. De plus, ces règles devraient bien être écrites quelque part, mais serait cachées pour ne devenir visible que dans certaines circonstances. Difficile de ne pas être mal à l’aise avec cette idée.

Peut‑être qu’une autre piste, est de faire des instances des règles, une chose à part entière et de permettre à des termes, d’être liés, pas seulement à d’autres termes, mais aussi à quelque chose identifiant une instance d’une règle.

Si A et B sont deux termes, que A peut avoir plusieurs solutions, que A est nécessaire pour résoudre B, mais que A se trouve subitement ne plus avoir qu’une seule solution possible quand il est utilisé pour résoudre B, ce pourrait être parce A et B sont aussi ensemble liés à une instance d’une règle, une instanciation d’une règle ne pouvant être égale qu’à elle‑même (parce que chaque position dans une chaîne d’inférence, est une position unique). B n’aurait pas seulement besoin de A ou encore l’identité de l’instance de la règle qui l’a produite, serait intégré à A et B étant lié à A, B serait aussi lié à cette identité.

La même intrication pourrait permettre de poser que dans le nouvel exemple de ce message, le second x n’est pas le même que le premier, parc qu’il n’est pas produit dans la même instance de la règle qui le produit. Et de même, x et f serait lié à l’identité de cette instance, comme ils pourraient l’être à un terme quelconque.

En tout cas au moins, donner une identité aux instanciations des règles, ça fait sens plus facilement.

C’est au moins autant justifié que l’interprétation qui a été faite des constantes, vues comme des identités définies par des positions dans un espace quelconque.

Intuitivement, ça se comprend assez bien comme l’identification d’un instant dans une chaîne d’événements, même s’il faudrait faire attention à ne pas interpréter les chaînes d’inférence comme des représentations du temps exclusivement, parce que faut de pouvoir justifier cette limite à l’interprétation, elles peuvent à priori être un chemin dans n’importe quel autre type d’espace.

C’est en accord avec la sémantique du langage jusqu’ici et ça se comprend bien intuitivement, alors peut‑être que c’est la bonne représentation avec les propriétés qu’il faut.

Plus précisément, la résolution d’un terme serait attaché au point de la chaîne où il est entièrement résolu. C’est important à préciser, comme la résolution d’un terme implique généralement tout un segment de chaîne. Les termes vérifiables sans condition, seraient considérés comme attachés au contexte initial. En reprenant l’exemple précédent des deux termes A et B, on pourrait avoir deux cas. Soit c’est A qui est attaché à une position quand il est résolu, soit c’est B qui est attaché à une position quand il est résolu avec A. Le second cas correspondrait le mieux aux exemples posés précédemment.

Reste deux problèmes pratiques, un concernant la notation, un autre concernant la lecture.

Avec quelle notation écrire qu’un terme doit être lié à une position dans la chaîne d’inférence ?

Il serait peut‑être difficile, pendant une démonstration par exemple, de lire une formule en voyant deux termes semblant identiques, mais étant pourtant différents parce que ayant été résolus chacun à une position différente de la chaîne d’inférences.

À la suite du message précédent.

Étant donné (eq A A), dans la conjonction (eq x x) & (eq x x), les instances de A ne sont pas les mêmes. Elles avaient été notées A_1 et A_2, sous la condition que ces noms ne puissent pas être écrits dans le texte d’une règle, seulement produits par le processus de vérification des règles. Les instantiations de ces constantes, pourraient avoir une représentation reprenant le même principe, on aurait pour @c, les instances @c_1 et @c_2, par exemple.

De la même manière, une constante pourrait être instanciée, chaque instantiation produisant une constante unique. Les variables et les constantes habituelles, sont distinguées par la première lettre, si la première lettre est une majuscule, c’est une variable, sinon, c’est une constante. Pour distinguer le nouveau type de constante introduit, le symbole @ pourrait être utilisé, comme il se lit “at”, ce qui fait bien écho au fait que sa valeur, abstraite, représente une position dans la chaîne d’inférence.

Il faut maintenant vérifier que cette notion permet d’exprimer les exemples de cas posés.

En posant que (f X Y) est une représentation de y = f(x). Cette notation est utilisée ici, plutôt que celle du langage, pour aider à se mettre dans l’ambiance des langages classiques, qui sont le domaine où se pose les problèmes auxquels il est tenté d’apporter une solution : la description des effets de bord.

-------------------------
Le cas :

y = f (x)
y = f (x)

Où les deux y ont une valeur quelconque et ne sont pas les mêmes.

Si y est un terme contenant une constante spéciale, alors le second y est différent du premier. Par exemple si on a « (f X Y) : (eq Y (e @c X)) », alors les deux y sont différents, comme ils sont liés chacun à une instance différente de @c. L’ordre des terme n’a pas d’importance.

-------------------------
Le cas :

x = f (a1)
y = f (a2)
z1 = g (x)
z2 = g (y)

Cet exemple serait incorrecte, g étant appliquée à x, puis à y, alors qu’elle ne devrait être appliquée qu’à un des deux, n’importe lequel des deux, mais un seul des deux.

Il ne faut pas comprendre incorrecte dans le sens de ne pas pouvoir l’écrire, mais dans le sens que la conjonction de termes n’auraient pas de solution. Les deux g pourraient ne pas être les mêmes, la première occurrence de g serait une résolution de g, pas seulement de z1, de même pour la seconde occurrence de g. Pour que les deux occurrence de g soit les mêmes, il faudrait que g ait déjà été résolu avant ces deux occurrences. Pour que g ne puisse être appliqué que à x ou que à y, il faudrait que g soit déjà liée d’une certaine manière à x ou y et donc ait été résolu avant. L’application de g à x ou à y au choix, serait une autre résolution. Disons que ça nécessiterait une reformulation, par exemple celle‑ci :

(g, x) = f (a1)
(g, y) = f (a2)
z1 = g (x)
z2 = g (y)

La première occurrence de g étant résolu, la seconde qui serait différente, ne peut pas aboutir et alors la résolution échoue directement ici :

(g, x) = f (a1)
(g, y) = f (a2)

On arrive même pas au point de tenter de résoudre z1 = … ou z2 = …. L’équivalent du terme « (g, x) = f (a1) » fixerait g d’une telle manière que l’équivalent du terme « (g, y) = f (a2) » n’ait pas de solution, même en imaginant que a2 = a1. Ça ne contredirait pas l’égalité, le premier g n’étant pas le même que le second, ce qui ne contredirait pas l’égalité non‑plus, si f résous g avec une constante spéciale, qui n’apparaît pas dans l’écriture plus haut, mais dont il faut imaginer qu’elle fait partie du terme g. La constante spéciale est nécessaire, justement pour que la formulation corresponde à l’intention, même dans le cas où a1 = a2. Dans ce cas, g ne représente pas une constante, mais un terme et on pourrait illustrer plus clairement ainsi : (G, x) = f (a1).

L’ordre des termes n’a pas d’importance, la conjonction de « (g, x) = f (a1) » et de « (g, y) = f (a2) », ne peut pas être résolue, quelque soit l’ordre de ces deux termes, pour la même raison que (eq a b) n’est pas plus résoluble que (eq b a).

-------------------------
Le cas :

x = f (a)
y = g (x)
y = g (x)

Cet exemple serait incorrecte, g ne devant être appliquée qu’une seule fois à x.

On peut imaginer que x a un état, que après la première application de g à x, x change d’état et que cet état ne permet pas la seconde application de g à x dans son nouvel état. Il faudrait donc que g résolve un x qui ne serait pas entièrement résolu. Mais la seconde occurrence de g recevrait un x déjà résolu et le terme serait résolu par avance, comme une vérification redondante. Ça ne convient pas. Il faut donc que le premier g ne soit pas le même que le second, et là encore, reformuler ainsi :

(G, x) = f (a)
y = G (x)
y = G (x)

Le terme (G, x) ne serait résoluble que si x est en suspend, c’est à dire que G n’a pas encore été appliqué à x. Quand G est appliqué à x, le x est fixé dans un état faisant que G n’est plus applicable, G ne pouvant être résolu qu’avec un x en suspend. Donc x devrait plutôt s’écrire X. Dans « (G, X) = f (a) », G pourrait être lié à une constante spéciale, mais pas X, puis dans « y = G (X) », G lierait X à cette constante spéciale. Resterait à formuler que G ne peut être appliqué qu’à un X en suspend.

Ici aussi, l’ordre des termes n’aurait pas d’importance. Le terme correspondant à « y = G (x) » ne serait pas entièrement résoluble tout seul, mais seulement parce que « (G, x) = f (a) » n’aurait pas déterminé une partie de la résolution nécessaire de x. La conjonction des deux pose une relation entre les deux, pas un ordre entre les deux. Le terme « y = G (x) » tout seul, dirait que G a été appliqué à x, mais sans encore avoir résolut la condition de la relation entre G et x. La vérification ultérieure de « (G, x) = f (a) » confirmerait cette relation ou échouerait, si x devrait aussi être lié à un autre G, que ce soit précédemment ou ultérieurement. Pour le même raison, quelque soit l’ordre des termes, le conjonction de deux « y = G (x) », comme x devrait être dans deux états en même temps, ce qui n’est pas possible (à moins de le prévoir ainsi).

Il faudrait pouvoir interpréter différemment, un X non‑résolu et un X résolu. Les règles de l’interprétation jusque maintenant, ne le permettent pas, une interprétation représentant autant une vérification potentielle qu’une résolution potentielle, jusque maintenant, une résolution de X serait tentée si X n’est pas résolu et si X est fixé, une vérification serait effectué. Peut‑être faudrait‑il permettre de distinguer un terme non‑résolu et un terme résolu, de la même manière que la négation permet de distinguer un terme vérifié et un terme non‑vérifié. En parlant de négation, justement, ce concept pourrait être vu comme une négation de l’état résolu. Tout comme on peut avoir « non T » pour dire que T ne doit pas être vérifié, on pourrait avoir « unresolved V » pour dire que V n’est pas résolue, ce qui est différent de non‑résoluble, c’est à dire que « (r unresolved V) » ne serait pas un synonyme de « non (r V) ».

Mais un terme peut être entièrement ou partiellement résolu et justement dans les formulations précédentes, il est question de différent niveau de résolution. Il faudrait pouvoir distinguer non‑résolu en quoi et non‑résolu en quoi. L’application de l’opérateur suffirait à le distinguer : « (r unresolved A B) » ne serait pas la même chose que « (r A unresolved B) », A ou B pouvant être une variable où un terme. Si on voulait pouvoir distinguer l’état d’un terme d’après l’état d’une variable interne, il serait possible d’utiliser une interprétation.

Par exemple :

(u1 A) : (eq A (r unresolved B C)).
(u2 A) : (eq A (r B unresolved C)).

Il serait alors possible d’écrire (u1 X) sans nécessairement avoir à développer tout le terme X. Les interprétation u1 et u2, distingueraient deux aspects de l’état du terme en question.


Sous réserve de futures réflexions après décantation.

Déjà une énormité à corriger :


Cette partie doit être oubliée, l’ordre des termes deviendrait important. Une autre solution et de distinguer les différentes résolution, par autant de constantes spéciales qu’il y a de relations différentes.

L’exemple était celui‑ci :

(G, x) = f (a)
y = G (x)

Où G est lié à x, c’est à dire que G ne peut être appliqué que à x, cette relation étant posée par l’instantiation d’une constante spéciale, G et x étant partiellement résolus par la même règle, ensemble. Le fait que G ait été appliqué à x, peut être représenté par un autre état, qui peut être un état de G ou de x, au choix, l’état étant finalement celui des deux ensemble, conséquence que les deux sont liés ensemble. Cet état est résolu lui aussi par l’instanciation d’une constante spéciale, une seconde constante. Dans ce cas, le conjonction d’un « y = G (x) » et d’une autre « y = G (x) », n’est pas vérifiable, comme prévu, la constante n’étant pas la même pour les deux termes correspondants.

Pour aller plus loin, cet exemple :

(g, x) = f (a)
y = g (x)


Pourrait être formulé autrement :

x = f (a)
g = h (x)
y = g (x)

Au lieu que f produise g et x, f ne produit qu’un x et g est produite séparément, h liant g à x de la même manière que l’aurait fait f.

Une autre alternative encore :

x = f (a)
g = h (g, x)
y = g (x)

Ici h ne produit pas g, mais lie g à x, seulement, g étant supposée produite autrement.

Il existe peut‑être d’autres possibilités encore, il s’agit surtout de montrer que ça peut se formuler de plusieurs manières, l’une pouvant être plus praticable que les autres selon les usages.

Ces constantes spéciales semblent ce qui convient. Les constantes spéciales instanciées avec les règles comme le sont les variables, avaient déjà été imaginées sans le dire, mais abandonnées comme elles ne présentaient pas d’intérêt autre que théorique. Comme leur possibilité est venue tôt et naturellement et qu’elle s’avère maintenant répondre à une nécessité pour l’expressivité, il est peu probable qu’elles soient abandonnées.

La mauvaise piste des règles déposées dans le contexte pendant la vérification de règles, était mal venue, mais est venue dut à une précédente remarque, qu’un ajout de règles peut réduire l’ensemble des solutions d’un terme ou même le réduire à être impossible, ce qui semblait proche d’une solution à ce qui était recherché. Cette idée présentait le problème que ces règles auraient bien dut être écrites quelque part, mais cachées pour ne devenir visible qu’en certaines circonstances, ce qui au feeling, ne laissait pas une bonne impression. Il y a une raison plus formelle d’abandonner cette initiale mauvaise idée : ce qui était recherché, c’était la réduction d’un ensemble de solutions possibles, à une et exactement une seule solution possible. L’ajout de règles dans le contexte, en plus d’être une idée douteuse, aurait présenté un autre problème : la vérification préalable qu’elles réduisent bien l’ensemble des solutions à une solution unique exactement.

La solution des constantes pourrait se résumer ainsi : une solution unique est une identité et une identité est une solution unique. L’identité, c’est justement ce que représente ces constantes. Cette identité est produite automatiquement sous une forme abstraite, plutôt que produite concrètement par des termes dont ils faudrait prouver qu’ils auront au final au moins une et au plus une solution. La contrepartie de la production automatique de ces identités, est que ce sont des identités abstraites. Cela pourrait‑il devenir un problème ?

L’instanciation suivant la même logique que celle des variables, plusieurs occurrence d’une de ces constantes dans une règle, serait la même constante.

Pourrait se poser la question de savoir si les variables doivent pouvoir être liée à ces constantes ou pas ou s’il est nécessaire d’introduire un type de variable spéciale pour ces constantes spéciales.

Ces constantes se comportant comme des constantes ordinaires en tout excepté pour leur origine, qu’une variable ordinaire puisse être liée à une de ces constantes, ne se serait pas plus un problème que de la lier à une constante ordinaire. Mais il pourrait tout de même être utile d’introduire un type de variable ne pouvant être liée qu’à ces constantes.

D’abord un exemple avec seulement les variables ordinaires.

Ce cas avait été utilisé :

x = f (a)
g = h (g, x)
y = g (x)

f renvoi un x, h lie x et g dans le sens où g ne peut être appliquée qu’à x, y est le résultat de cette application.

Mais si on supprime la seconde ligne ?

x1 = f (a1)
x2 = f (a2)
y2 = g (x2)

Dans ce cas, g n’est plus lié à un x en particulier. Pourtant g, qui est en réalité un terme, a une place pour une constante représentant l’identité de ce à quoi elle peut être appliquée. Cette variable est liée automatiquement selon que g est appliquée à x1 ou à x2. On pourrait même imaginer que les x1 et x2 produit par f, aient une variable laissée libre au lieu d’être liée à une identité et alors g peut être appliquée à x1 puis à x2, deux variables libres pouvant toujours être liées.

Cette souplesse ne serait pas possible en ne permettant que les constantes spéciales ne puissent être propagées que par des variables spéciales. Ce ne serait pas incohérent, mais ce serait une sur‑contrainte facilement dommageable.

Sans devoir être imposé, ce type de variable spéciale pourrait avoir une utilité. Comment formuler qu’un terme doit être liée à une chose qui est une identité seulement, sans fixer cette identité par résolution ? Une solution serait un type de variable ou une proposition spéciale du langage. Au choix, soit quelque chose comme @V soit quelque chose comme (is-id V), qui serait un terme vérifié seulement si V est liée à une constante représentant une identité. Contrairement à la mauvaise idée précédent, celle d’un prédicat qui serait vrai selon qu’une variable est résolue ou pas, cette fois la non‑importance de l’ordre des termes d’une conjonction serait préservée. Dire d’abord que V est liée à une identité puis ensuite la liée à une identité en particulier ou l’inverse, n’aurait pas plus d’importante que de poser l’égalité entre deux variables avant ou après qu’elles ne soient déterminées.

Une variable comme @A serait plus spécifique qu’une variable comme B :

@A = B serait possible si B est libre et ferait de B une variable ne pouvant être liée qu’à une identité, variable ou constante, comme si @B avait été écrit.

B = @c serait autant possible que B = c, mais seulement @A = @c serait possible, pas @A = c.

Serait‑il utile de pouvoir poser qu’une variable ne doit pas être liée à une identité, c’est à dire qu’elle ne doit être liée qu’à un terme concret ou rester libre ? Ça ne semble en tout cas pas une nécessite, au contraire de pouvoir poser qu’une variable doit être liée à une identité sinon rien.

Comme la non‑importance de l’ordre des termes est préservée, ces constantes ne sont pas ordonnées, elles ne sont que des identités et alors l’utilisation de @ pour les distinguer, qui évoque un adressage, n’est pas idéal. Peut‑être que le symbol, « ℩ » conviendrait mieux. C’est le caractère U+2129, nommé “ turned Greek small letter iota ”, décrit comme ayant cette signification : “ unique element fulfilling a description (logic) ”. Ce symbole ressemble à un i, comme son nom l’indique, et i est la première lettre du mot “ identity ”. Il est petit, mais une police de caractère sur mesure pourrait y remédier.

L’introduction de ce type de constante, peut‑il compliquer la vérification, la résolution automatique ou les preuves ? Sans certitude, mais à priori, plutôt non. Comme souligné précédemment, excepté pour leur origine, ces constantes ne sont que des constantes et pour l’unification, elles sont autant simples que n’importe quelle constantes. La seule différence serait que le nombre de constantes présentes dans un contexte et donc encore plus en fin de résolution ou en fin de démonstration, serait plus important qu’avec les constantes ordinaires, mais ce n’est rien en comparaison des termes qui peuvent se composer récursivement, qui sont plus complexes que des constantes.

Il a été prévu que la langage serait repris en partant d’une définition dans laquelle seule la vérification de termes constants serait défini. Ce langage de base devrait‑il ou pas inclure ces constantes ? — La question se pose aussi à propos des termes récursifs. — Le problème qui se poserait, est que ces identités n’ont pas de représentation, comme elles sont produites, elles peuvent sembler n’avoir de place qu’à un niveau du langage supportant la résolution. Pourtant, il n’est pas difficile de les imaginer associée à des termes constants. Il ne serait pas étrange d’imaginer qu’elles puissent être produites même en l’absence de résolution, comme il n’y a pas besoin de résolution pour les produire.

Les exemples présentés jusque maintenant, ne couvrent pas un cas pourtant important, qui sera décrit un peu plus tard.

Une propriété à noter, est qu’un terme non‑prévu pour être lié à une identité, peut quand‑même être lié à une identité, mais pas la réciproque, un terme prévu pour être lié à une identité, ne peut pas devenir un terme non‑lié à une identité.

Un exemple du premier cas : (eq (A B) (@c B)). Le terme de gauche dans eq, est un terme ordinaire, mais il finit lié à un @c. Ce n’est pas possible avec tous les termes ordinaires : (eq (a b) (@c b)) n’est pas vérifiable. Il faut retenir que (@A B), ne peut jamais devenir un terme comme (A B), mais (A B) peut devenir un terme comme (@A B), ce qui reste sous condition qu’il existe une interprétation prévue pour ce terme, sans quoi il n’est plus pertinent.