Les logiques : notes en vrac

Il faudra revenir en arrière avant d’aller à nouveau en avant, par un autre chemin. Certaines choses dites dans ce message, ressembleront à des répétitions de choses dites il y a un an, mais avec des compléments et plus dans le même contexte.

Le problème avec la sémantique de Herbrand, avait déjà souligné, c’est celui de l’univers, un ensemble infini, parfois même décrit d’une manière étrange, en produisant toutes les combinaisons de constantes possibles, même insensées. Un second problème, est qu’il ne suppose pas d’interprétation, pas d’univers extérieure.

Le problème avec la sémantique de Tarski, est qu’elle est trop générale, elle traite de langages avec un certain nombre d’axiomes, pose que le méta‑langage doit être plus capable que le langage objet, suppose une théorie des ensembles incluse dans le méta‑langage et des ensembles infinis de phrases. C’est trop complexe et suppose trop de concepts ayant un status fondamental (trop risqué). Le langage défini ici, n’est pas quelconque et la suite se fera en excluant les ensembles comme notion fondamentale, pour une raison qui sera donnée plus tard. Si les ensembles à proprement parler, sont exclus, encore plus les ensembles infinis, qui ne peuvent pas être produits. Tarski est réputé avoir trouver des solutions à des paradoxes sémantiques comme le paradoxe du menteur. Ce type de paradoxe n’est possible qu’avec la notion de négation, qui n’existe pas dans le langage défini ici.

La raison de voir un problème dans l’absence d’interprétation ou d’univers extérieur, n’est pas seulement dans l’intention du langage, elle est formelle : l’égalité n’a pas de définition formelle, elle n’a qu’une définition pour une interprétation, même s’il est possible d’avoir une interprétation de l’égalité qui soit toujours la même et sur laquelle les interprétations devraient se baser, elle serait commune à toutes les interprétations, mais n’en appartiendrait pas moins au domaine de l’interprétation.

Les paradoxes comme le paradox du menteur, ne peuvent se produire que quand le langage peut se contredire lui‑même, ce qu’on appel la négation. Le langage défini ici ne le peu pas, la négation n’existe pas, seul existe le constat de l’impossibilité d’une vérification. Il n’est pas possible de définir une règle empêchant une autre règle de vérifier ce qu’elle vérifiait déjà.

Les ensembles infinis, la question qui a resurgit et qui fait peur, cette question peut être mise de côté avec une justification sémantique : le langage ne parle que ce qui est, qui est parce que écrit comme posé ou qui est parce que produit. Il n’est pas assez utile de parler de ce qu’on ne peut pas produire ou de ce qui n’est pas.

Ça peut sembler contradictoire avec l’idée que les hypothèses représentent des ensembles infinis. Justement, les mots étaient trompeurs, elles ne représentent pas des ensembles infinis, une hypothèse représente la réduction d’un ensemble infini à une chose fini, un fait. De l’ensemble infini des entiers naturels, l’hypothèse {(nat N)} ne retient qu’une chose finie : N vérifie (nat N). Ceci permet de traiter avec les récursions potentiellement infinies, mais qui seront toujours finie en pratique.

Pour résumer les points les plus importants de la sémantique : aucune règle ne peut en contredire une autre, la négation n’existe pas, seul existe le constat d’une impossibilité, on ne parle que ce qui est, que ce soit une chose posée ou produite, en tout cas, qui existe (quand on ne parle que pour dire des faits produits, on ne ment pas, d’où l’impossibilité du paradoxe du menteur). Il faudrait ajouter une dernière règle à cette sémantique : une absence de conclusion, ne conclut rien, même pas un échec, rien, elle n’est pas interprétable, donc l’aboutissement d’une récursion infinie n’est pas dans son domaine, même si le langage peut parler des étapes finies d’une récursion éventuellement infinie.

Il faudra revenir en arrière. La notion d’équivalence va être mise en suspend, le langage de base datant d’avant les hypothèses sera repris, mais en y ajoutant la notion de composition horizontale, essentielle. Les règles de l’unification ne seront plus les mêmes. L’idée de relaxer la règle qu’un terme commence toujours par une constante, serait appliquée à ce nouveau langage de base. Les autres idées émises ultérieurement, sont repoussées à plus tard, même celle des hypothèses qui avait connue une mise en œuvre,.

Dès l’ancien langage de base, une occasion a été perdue de d’abord tenter de définir la syntaxe du langage lui‑même, dans ses propres termes. C’est la base, on ne peut pas dire ce qu’est une construction correcte, sans d’abord que sa description ne soit syntaxiquement correcte. Cette tentative aurait d’ailleurs put être une bonne illustration, après les exemples expliquant en détail, l’unification et la résolution. Définir cette syntaxe dans les termes du langage lui‑même, pose déjà une colle qui sera rapportée plus loin. La syntaxe serait simplifiée, mais seulement pour la définition, la syntaxe utilisée en pratique resterait la même, elle aurait un statut de sucre syntaxique. Cette syntaxe simplifiée sera rapportée plus tard.

Pour ce nouveau langage de base, la syntaxe étant posée, la sémantique serait qu’il vérifie un terme qui est vérifié par les règles, et qu’il ne le vérifie pas sinon, sans se soucier de la génération des solutions possibles, à définir ensuite. Rien que cela, pose la problème d’une possible récursion infinie. Il a été vu que la vérification d’un terme constant, se termine toujours, même en présence de règles suspectes. Se limiter à la vérification de termes constants pourrait être une première étape. Après avoir formuler ce qu’est cette vérification, il serait possible d’ajouter à nouveau la preuve de satisfiabilité des règles, mais avec un terme constant quelconque, pas sous une forme générale avec des hypothèses, qui ne serait pas encore introduite. Ce serait un ajout à la syntaxe. Cet ajout fait, il n’y aurait plus de risques de récursion infinie avant de trouver la moindre solution, et la vérification d’un terme ne porterait plus seulement sur des termes constants. La génération de plusieurs solutions, serait encore remise à plus tard.

La définition de ce qu’est une vérification d’une règle, nécessiterait de définir ce qu’est une instantiation de règle. Là, se poserait une colle, qui se poserait même avant, avec la définition de la syntaxe : ces définitions nécessitent une non‑égalité.

Même en fixant les symboles spéciaux de la syntaxe (ce qui n’est pas une nécessité, mais une possibilité quand‑même), il faudrait pouvoir formuler le fait que les nomes des constantes et des variables ne peuvent être égales à aucun de ces symboles spéciaux. Pour définir ce qu’est l’instantiation d’une règle (ce qu’elle est, et non‑pas comment elle est réalisée), il faudrait pouvoir poser que les variables de la règle instanciée, n’ont pas les mêmes noms que des variables précédentes. Dans les deux cas, en plus d’une notion fondamentale d’égalité, il faut une notion de non‑égalité. Même en imaginant qu’une astuce permette de s’en passer pour définir ce qu’est l’instantiation, cette notion de non‑égalité resterait nécessaire pour la syntaxe. Si elle est défini comme l’échec de l’égalité, il faut introduire la notion explicite d’échec d’une règle et interprétation de cette notion par le langage, ce qui n’a pas une fois été abordée jusque maintenant, l’échec d’une règle n’a même pas de représentation définie. La question de l’introduction de la non‑égalité ou de l’échec d’une règle, n’a pas encore de réponse.

Une note suivante en dira plus sur la raison du statut donné à l’égalité (notion fondamentale, définie par l’interprétation) et aux ensembles (exclus du statut de notion fondamentale, mais pas exclus du statut de notion dérivée).

Sur l’égalité et les ensembles. Une partie du message s’aventure sur un terrain délicat, celui de donner à une partie de la sémantique, une interprétation dans le monde ordinaire.

L’égalité n’est pas moins délicates que les ensembles, mais elle est nécessaire à la définition du langage, contrairement aux ensembles et est plus simple à introduire, parce qu’elle ne nécessite pas de représentation, seulement une règle.

Un ensemble, en plus d’un concept, est un objet, comme tel, il lui faudrait une représentation, mais un même ensemble pourrait avoir plusieurs représentations. Définir une représentation canonique, suppose de se reposer sur des propriétés des éléments, en plus de celle de l’égalité qui pourrait définir une notion de base des ensembles.

L’égalité, n’est pas un objet, seulement un concept. Comme telle, elle ne nécessite pas de représentation. Comme concept, elle peut se définir comme un règle, même si cette règle pose le problème de ne pas avoir de preuve de satisfiabilité générale.

L’égalité, nécessaire à la définition même du langage, et qui pose moins de problème que les ensembles, reste quand‑même un mystère.

L’égalité est une règle, mais à quelle règle correspond‑t‑elle dans le monde dont on a l’expérience quotidiennement ? En pratique, on parle plus facilement de ses effets ou des phénomènes qu’elle peut produire, qu’on en parlerait comme d’une règle. Les compositions horizontale et verticale récemment introduites, sont des choses autant dans la syntaxe que dans le monde et leur représentation dans la syntaxe est même quasiment une représentation physique proche de la réalité. Rien de tel avec l’égalité qui n’a pas de représentation et qui comme règle ne peut même pas se poser d’une manière qui permettrait de prouver sa symétrie, qui doit être supposée.

Dans le langage, l’égalité est utilisée pour l’unification. L’unification, au contraire de l’égalité, elle, peut correspondre à des réalités, même si abstraites, partout où des choses réagissent entre elles par mise en correspondance. Cette mise en correspondance ne se fait pas sur la base d’une quelconque égalité, mais sur la base de chose comme des dimensions, une charge électrique (même si elles doivent être opposée), des phases synchrones, des suites d’événements ayant les mêmes conséquences, etc. Rien de tel dans le langage, où toutes les propriétés des choses mises en correspondance, le sont sur la base d’une seule propriété, qui est l’égalité ou pas des constantes, comme si l’égalité était dans ce cas là, une abstraction de la diversité des choses qui dans le monde, peuvent être à l’origine de, ou faire voir des, correspondances.

Même en dehors du rôle qu’elle a dans l’unification, la notion d’égalité est abstraite, elle ne se mesure que rarement et quand elle se mesure, c’est toujours avec une marge d’erreur, mais ce n’est pas important. Ce qui est important, c’est que le plus souvent elle ne se mesure pas, elle se constate, à travers un effet. Par exemple deux formes découpées dans du carton, superposées, se cachent l’une l’autre si elles sont égale ; c’est un effet. On peut verser le volume d’un seau plein dans un autre seau de même volume ; c’est un effet. Et encore, on y verrait plus facilement une forme de correspondance plus qu’une égalité, qui est généralement modulo quelque chose. Le monde du quotidien, connait plus les équivalences que l’égalité, au point que deux choses vraiment égales ou identiques, sont vu comme une surprise, une coïncidence improbable. L’égalité dont le langage à besoin pour sa définition, qui ne semble définissable que par une interprétation en dehors du langage, semble pourtant n’avoir vraiment d’existence que dans le langage.

Pour résumer, l’égalité n’a pas de définition formelle qui ne suppose pas sur sa supposition, elle n’est définie que par une interprétation qui peut être variable, même s’il est possible de lui donner une interprétation unique dans le domaine des constantes du langage, mais même là encore, elle ne peut pas avoir de définition formelle, ne semble justifiée que par une interprétation.

Heureusement que son introduction comme concept explicite dans le langage pose moins de problème qu’elle n’est un mystère insondable. L’unification semble tellement plus naturelle qu’il a été crut que l’égalité pouvait être vu comme une manifestation de l’unification. À moins que ce ne soit en effet le cas … Une solution au problème que pose la preuve de sa satisfiabilité, sera décrite plus tard.

L’idée de simplification de la syntaxe du langage, serait comme suit : le symbole de la conjonction disparaîtrait de la syntaxe formelle, la suite de termes terminée par un point, suffisant à faire des termes, ceux d’une conjonctions. Les deux points verticaux pourrait être omis aussi, une règle commençant toujours par un terme, le premier est toujours la tête de la règle, les termes suivants jusqu’au point final, sont ceux du corps de la règle, la conjonction.

Les deux points verticaux et le symbole de la conjonction, resteraient utilisés dans la syntaxe en pratique, pour raison de lisibilité.

En même temps, conserver ces symboles même dans la syntaxe formelle, ne poserait pas de problème pour sa définition tout aussi formelle.

Une formulation moins confuse de l’égalité clarifiant, sa nature, son rôle et expliquant pourquoi elle est indéfinissable dans le langage, bien qu’elle doive être posée.

Dans l’interprétation, c’est l’équivalence qui existe le plus souvent, l’égalité étant rare ou plutôt spécifique à certains domaines d’interprétation. Quand c’est l’équivalence qui existe, l’égalité est une conclusion de l’équivalence ou de la correspondance, une notion proche. Le langage ne connait pas ces équivalences, même s’il est prévu de lui ajouter la possibilité de traiter avec, il n’en inclura pas de définitions, celle‑ci n’existant que dans les interprétations. L’égalité est la conclusion d’une équivalence, l’équivalence peut éventuellement être définie par une fonction, concluant ou pas par une égalité. Le langage n’ayant pas de définition des équivalences possibles, il ne l’interprète que comme une égalité mais en établissant une relation entre les deux, comme il y en a une. Cette relation étant posée, il peut dériver une équivalence en particulier et unique, à partir de l’égalité, tandis que l’interprétation, à l’inverse, dérive une égalité d’une équivalence.

D’un point de vue logique ou sémantique, la dernière phrase est la plus importante : l’interprétation dérive l’égalité des équivalences que le langage ne défini pas, et le langage dérive une équivalence minimale de l’égalité. Il faut noter l’inversion de la direction. Cette inversion de direction n’est pas surprenante, si on oublie pas que l’égalité est une conclusion de l’équivalence ou une traduction de l’équivalence dans le langage.

C’est la raison pour laquelle l’égalité semble indéfinissable et même ne pas exister en réalité, alors qu’elle est une notion évidente pour la plupart des gens. L’égalité est une notion nécessaire pour traiter avec les équivalences, qui la justifie, c’est une réduction à une abstraction d’une interprétation dont les détails disparaissent avec cette abstraction.

Reste deux notes.

Il est dit que la langage ne connait pas les équivalences et il est aussi dit qu’il est prévu de lui permettre de traiter avec. Pour traiter avec, il n’y a pas besoin de les connaitre, il ne connaîtra que les inférences possibles à partir d’une équivalence posée. Et pour s’assurer à la fois de la cohérence de l’équivalence dans l’interprétation et de la cohérence de la représentation des choses sur lesquelles portent les équivalence, il pose et pour lui‑même, et suppose pour l’interprétation, la règle « A = B ==> A == B ». Si une interprétation ne vérifie pas cette règle, le langage ne peut pas le savoir, mais alors l’interprétation de ses conclusions pourront ne pas être possible ou ne pas avoir le sens qu’on croit.

On se dire que l’égalité n’est pas si abstraite, puisque même si elle n’existe pas dans la plupart des domaines d’interprétation, excepté ceux abstraits, elle est partout, par exemple dans l’informatique. Justement, dans l’informatique, ce qui permet de conclure à une égalité, c’est une équivalence, un phénomène physique ou électronique, avec lequel l’égalité stricte est improbable, où il n’existe que des égalités modulo quelque chose. On retrouve bien l’égalité comme conclusion ou interprétation d’une équivalence.

Comme dit précédemment, heureusement que l’égalité pose moins de problème à intégrer, qu’elle n’est mystérieuse.

Ce qui a été dit ici, n’a pas beaucoup d’importance pour la définition du langage, la relation d’inférence entre égalité et équivalence ayant été déjà posée plusieurs fois. Ce qui est dit dans ce message est plutôt pour assurer que l’égalité ne cache pas un problème logique ou sémantique derrière ce qu’elle a de mystérieux et il est explique pourquoi elle est mystérieuse d’un certain point de vue et non‑définissable en elle‑même dans tous les cas.

Sans répéter le précédent message, comme sa conclusion est sémantiquement importante, deux autres exemples pour illustrer cette conclusion.

Imaginons qu’on veuille vérifier une unification, non‑pas par logiciel, mais à l’écrit sur du papier. Disons qu’on veuille vérifier l’unification de deux constantes. Elles sont écrites, par leurs noms, l’une à côté de l’autre. On conclut par exemple qu’elles sont les mêmes, donc à l’égalité et donc au succès de l’unification. Pourtant il est très improbable que les deux noms écrits soit vraiment identiques, une lettre ici ou là n’aura pas exactement une forme superposable à la lettre correspondante sur l’autre nom, etc. Plus encore, les deux noms sont deux objets nécessairement non‑identiques, parce qu’ils ne peuvent pas se trouver au même endroit sur la feuille de papier, ce qui suffit à en faire deux objets distincts. Pourtant on conclut à leur égalité, une égalité qui n’existe pas autrement que comme une abstraction, une interprétation d’une équivalence.

Un second exemple, justement en parlant de deux choses au même endroit, mais cette illustration est aventureuse et faite en espérant ne pas dire une bêtise. Quand au zéro « absolu », deux particules se trouvent dans le même état au même endroit, elles ne font qu’un et on a même plus d’égalité puisqu’on a plus deux choses distinctes, excepté l’égalité d’une chose avec elle‑même, qui n’est encore qu’une interprétation par rapport à l’état précédent, celui où il existait encore deux particules distinctes.

Justement peut‑être qu’il manquait juste à poser l’égalité d’une chose avec elle‑même, mais cette règle n’a pas beaucoup d’intérêt en pratique, elle est plutôt une conséquence de l’égalité comme interprétation de l’équivalence. Elle pourrait quand‑même être posée, pour la même raison qu’il faut poser « A = B ==> A == B », comme prérequis (supposé, non‑vérifié par le lanage) pour la validité de l’interprétation, en plus pour cette règle là en particulier, de permettre des inférences cohérentes avec l’interprétation.

L’importance de cette définition sémantique de l’égalité est aussi une justification à l’objection faite à la sémantique de Herbrand, qui suppose qu’il n’y a pas d’autre univers et donc pas d’interprétation dans un autre univers que celui qu’il défini (sans compter l’horreur impraticable qu’est l’ensemble infini que cette sémantique suppose, mais c’est une autre question).

Il a été noté que la définition de la syntaxe du langage dans le langage lui‑même, nécessite que le langage puisse vérifier la non‑égalité de deux constantes et que la définition de ce qu’est l’instantiation d’une règle, nécessite de la vérification de la non‑égalité de noms de variables, ce qui pose la question d’introduire la « négation » ou plutôt pour ce langage, la conclusion de l’impossibilité, avant même l’introduction des hypothèses, qui avaient été pressenties comme une notion permettant justement la preuve de l’impossibilité en général, dans tous les cas, sans tomber dans des récursions infinies.

Un problème que pose la vérification de l’impossibilité, est illustré par cette conjonction : « (r A) & non (s A) » qui en principe, peut être réécrite « non (s A) & (r A) ». En marge, il faudrait trouver un opération autre que « non », qui dénote la négation, exclue du langage, mais ce sera pour plus tard. Le problème est celui‑ci : comment vérifier l’impossibilité à un moment ou la variable A n’est peut‑être pas encore fixée par la résolution, si encore elle finie par l’être ? Une possibilité serait de s’en tenir à poser l’impossibilité à la fin. Le corps d’une règle ne serait plus une conjonction, mais une paire de deux conjonctions, une conjonction positive et une conjonction négative, la conjonction négative étant vérifiée après la conjonction positive. Il serait possible d’être insensible à cet ordre avec une unification qui lierait des variables à des exclusions. Par exemple si on a « non (eq A a) & (eq A b) », la première unification lierait A à une représentation de l’exclusion de « a » et le second terme serait vérifié, comme « b » n’est pas « a ». Si le second terme était (eq A a), alors il ne serait pas vérifié, « a » étant noté comme exclu. C’est une option, mais elle compliquerait la définition de l’unification et serait moins générale que la notion d’impossibilité de la vérification, comme elle ne s’appliquerait qu’à l’impossibilité de l’égalité. L’option de toujours vérifier les impossibilités à la fin, est préférable.

Il a été vu que vérifier une impossibilité peut se terminer en récursion infinie, comme la vérification d’une règle est une recherche d’au moins une solution, il peut arriver que la recherche de solution s’entête dans une récursion infinie à chercher une solution qui justement n’existe pas, sans pouvoir le conclure, à cause de la récursion infinie. Il a aussi été vu que la vérification d’un terme entièrement constant, ne se termine jamais en récursion infinie, qu’elle réussit ou pas, mais produit toujours une conclusion. Il pourrait être posé que la vérification de l’impossibilité, en plus de se faire après une vérification positive, ne serai définie que sur des termes constants, c’est à dire que sur des termes dont toutes les variables son liées. Mais une résolution peut se terminer avec des variables non‑liées. Pourtant, on peut définir la non‑égalité même sur des variables non‑liées : Any n’est non‑égale à rien. Any n’est pas non‑égale à Any, ça n’aurait pas de sens, mais Any n’est jamais non‑égale à quelque constante que ce soit, puisque l’interprétation de Any, est justement de pouvoir lui substituer n’importe quel terme. C’est une justification de conclure la non‑égalité même en présence de variables non‑fixées, mais ça n’exclus toujours pas le cas de la possible recherche infinie d’une solution positive pour conclure à son impossibilité, ce qui nécessite toujours que l’impossibilité ne soit vérifiée que sur des termes constants, sans variables non‑fixées. On peut noter pourtant que cette récursion infinie, ne peut jamais se produire avec la seule vérification de la non‑égalité, qui ne peut pas se terminer en récursion infinie et c’est de cette vérification là, que le langage a besoin immédiatement.

Le nouveau langage de base, est donc modifié ainsi : le corps d’une règle est une paire de deux conjonctions, la règle est vérifiée si la première conjonction a une solution et si dans le contexte de cette solution, la seconde conjonction n’a de solution pour aucun de ses termes. L’une ou l’autre conjonction peut être vide, ou même les deux.

Il faut préciser que vu comme une conjonction, le second ensemble de termes est une conjonction d’impossibilités et que vu comme impossibilité en lui‑même, le second ensemble de termes est une disjonction (non A & non B == non (A ou B)).

Dans le cas où un terme du second ensemble se termine en récursion infinie, il n’y a pas de conclusion. Comme souligné plus haut, ce cas ne se produit pas avec la vérification ou la conclusion de l’impossibilité de la vérification de l’égalité, qui est ce dont le langage a besoin pour définir sa propre syntaxe et sa propre sémantique, ce qui justifie de ne pas y voir un problème, au moins pas pour le moment.

Sous réserve d’éventuels futurs commentaires ou révisions.

Peut‑être une occasion de revoir la question des termes récursifs.

Ce qui a justifié l’exclusion des termes récursifs, n’est pas seulement que c’est un comportement standard des Prolog‑like, c’est que l’interprétation d’une solution est son développement en un terme constant, un développement qui ne se termine jamais dans le cas d’un terme récursif.

Savoir si un terme est récursif ou pas, peut se faire sans récursion infinie (mais pour une mise en œuvre de l’unification, il y a un risque de récursion infinie dont il faut se prémunir).

Exclure les termes récursifs pour une raison d’interprétation, équivaut à imposer quelque chose à l’interprétation, arbitrairement, puisque la nécessité de cette exclusion n’a pas de justification dans le langage lui‑même. Si une interprétation ne reconnait pas les termes récursifs, elle peut le dire ou s’assurer de ne poser que des règles ne produisant pas de termes récursifs.

Avec la possibilité de poser la non‑vérification d’une chose, et comme il est possible de vérifier si un terme est récursif ou pas, comme cette vérification est réalisable (preuve qu’elle est satisfiable) d’une manière qui se termine toujours, il est possible de définir la non‑vérification (ou même la vérification) de la récursivité d’un terme et de laisser cette option libre à l’interprétation plutôt que lui imposer. Il y aurait un double‑gain d’expressivité : non seulement les termes récursif seraient ouvert à l’interprétation, mais il serait aussi possible de poser qu’une solution doit être un terme récursif.

Resterait à définir une représentation d’un terme récursif. Comme un terme récursif a un point d’entrée et un point de « sortie », liés entre eux, une idée pourrait être d’avoir un symbole représentant ces deux points spéciaux.

Imaginons un terme (x (y V)) et a une unification de ce terme avec (x V). La solution pour V est un terme récursif, et (x (y V)) est alors lui‑même un terme récursif. Disons que le symbole E (il faudrait en trouver un autre) représente le point d’entrée et le symbole S (même remarque) représente le point de « sortie » par lequel on revient au point d’entrée, alors ce terme pourrait avoir cette représentation finie : (x E(y S)). Le symbole E désignerait le terme (y S) ; une notation englobante serait plus lisible et moins ambiguë, par exemple, mais un mauvais exemple, (x [(y S)]), les crochets carrés désignant le terme d’entrée, en imaginant trouver autre chose que les crochets carrés qu’il est préférable de réserver à d’autres choses.

Il faudrait envisager la possibilité de cycles dans des cycles.

Deux caractères intéressants dans Unicode, issus du script Hangul.

U+53EF, nommé, may, can, -able; possibly.
U+1F251, nommé CIRCLED IDEOGRAPH ACCEPT.

Le second est censé être le même que le premier, englobé dans un cercle. Comme prévisible, ils ne s’affichent et ne peuvent même pas être posté (message d’erreur du forum), mais l’existence d’un symbole pour cette signification, peut être notée.

Toujours issus du script Hangul :

U+6B63, nommé right, proper, correct.
U+32A3, nommé CIRCLED IDEOGRAPH CORRECT.

Là aussi, le second est censé être le premier, englobé dans un cercle.

C’est intéressant de découvrir ces symboles (plus haut et précédent message) portant un sens utile ici, qui proviennent d’un script à idéogrammes, justement après qu’un rapprochement ait été fait entre les termes du langage et les idéogrammes.

Le Hangul est un script de Corée du Sud. Il est décrit comme un alphabet, mais contient apparemment des idéogrammes aussi. Il pourrait être intéressant de se pencher sur ce script …

— Édit —

Toujours dans le script Hangul :

U+9042, nommé comply with, follow along; thereupon.
U+3785, nommé not straight, improper.
U+38FE, nommé do not care; unmindful of.
U+3A8E, nommé uncertain; not yet settled, […], to complete; to finish, all; entirely; totally; completely.
U+3AD8, nommé disappeared, not supported by, to avoid, unable to see.
U+64EF, nommé exclude, expel, reject; usher.

Probablement d’autres …

Mais sans connaitre la langue, difficile de savoir s’ils sont vraiment appropriés. Une sélection d’un nombre réduit pourrait être facilement reconnus avec l’habitude et utilisés pour les notations, moyennant une police de caractères had‑oc pouvant les afficher.

Ce que j’aurais aimé trouvé, est un symbole pour dire « ne doit pas être tel que », peut‑être U+64EF, comme représentation de la pseudo‑négation signifiant qu’une chose n’est jamais vérifié, et un symbole pour dire « entrée » et un autre pour dire « sortie », pour la représentation des termes cycliques.

Les termes négatifs seraient vérifiés dans le contexte vérifiant les termes positifs, et pour cette raison, la vérification des termes négatif ne devrait pas modifier le contexte.

La vérification d’un terme repose sur l’unification. La non vérification d’un terme, se définirait peut‑être mieux avec une anti‑unification, qui ne lierait pas les variables et vérifierait qu’elles ne peuvent pas être liées de la manière dont elles ne voient pas l’être.

C’est proche de l’idée de lier une variable à une exclusion, le choix entre les deux devrait avoir de bon fondements, au moins pratiques, si ce n’est pas sémantiques, parce que sémantiquement, il n’y a apparemment pas de différence entre les deux, la différence n’était que dans la formulation et les étapes de l’interprétation, les deux aboutissant toujours à la même conclusion (ce qui est supposé jusqu’ici, en tout cas).

En se restreignant un instant à la vérification de la non‑égalité, les deux possibilités se résument ainsi :

Une seule unification, qui en plus de pouvoir traiter avec des termes et des variables, peut traiter avec des exclusions. L’ordre des termes négatifs et positifs n’est pas important.

Deux unifications, chacune traitant avec des termes et des variables seulement, le but de l’une et de vérifier l’unification le but de l’autre et de ne pas la vérifier. L’une lie les variables, l’autre pas. L’ordre des termes négatifs et positifs est important, les termes négatifs sont toujours vérifiés tout en dernier.

La première possibilité est plus tentante, même si elle semble compliquer la définition de l’unification, l’interprétation est dans l’ensemble plus directe qu’avec la seconde possibilité, le tout est plus simple. Reste à savoir si elle peut représenter entièrement le concept de « négation par l’échec ». À voir …