Les logiques : notes en vrac

Même chose pour les genres d’interprétation d’un terme, quatre avaient été relevés, mais un cinquième manquait ; le plus simple, c’est pour ça qu’il n’avait pas été relevé. Comme précédemment, un résumé suivit du cas manquant.

L’interprétation comme une solution quelconque le vérifiant.

L’interprétation comme toutes les solutions pouvant le vérifier.

L’interprétation comme la solution assurant de ne pas le vérifier.

L’interprétation comme une hypothèse.

Le cinquième manquant, l’interprétation du terme tel‑quel, sous sa forme indéterminée (à moins qu’il ne soit entièrement constant).

Correction d’une précédent tournure malheureuse, en parlant de la cohérences des contextes.

Il avait été dit que ce qui est vérifié impossible dans un contexte, ne peut que rester impossible dans un contexte dérivé. Puis il avait été dit que cependant, des choses possibles dans un contexte, peuvent devenir impossible dans un contexte dérivé.

Ce n’est pas faux, mais c’est ambiguë. C’est vrai dans le sens où avant de poser qu’une chose est impossible, elle était éventuellement possible et une fois que les conditions de son impossibilité mise en place, elle n’est plus possible. Mais c’est trompeur dans le sens ou plutôt que parler de possible, il aurait fallut parler de potentiellement possible, une possibilité éventuelle mais dont les conditions n’ont pas été mise en place.

Une possibilité vérifiée, c’est à dire un fait avéré, le reste dans les contextes dérivé.

Ne pas confondre éventuelle possibilité et possibilité établie.

Comme dans le message précédent, mais concernant une petite blague par omission. Le blague ne doit pas être laissée telle‑quelle.

Il a été dit que le hasard peut réaliser des choses avant même de savoir comment les réaliser.

Il n’y a pas de contradiction, c’est juste que des mots manquaient, pour s’amuser. Sans blague cette fois, le hasard peut produire des choses, d’une manière hasardeuse (mais correctes si elles sont vérifiées correctes), avant même de connaitre une méthode certaine et prévisible de les produire. En pratique, une différence est aussi dans l’exhaustivité (quoi qu’une méthode prévisible n’en est pas automatiquement exhaustives).

Deux visions de la tête d’une règle, une pratique mais moins formelle, une formelle mais moins pratique.

La première vision est celle habituelle, avec des variables, une même variable apparaissant plusieurs fois, signifiant des termes égaux.

(r (c A) (d A)) : …

Une autre vision est de considérer comme la tête de la règle a des variables chacune de nom différent, une par point variable, et que l’égalité est rapportée dans le corps de la règle.

(r (c A1) (d A2)) : (eq A1 A2) & …

La première vue est naturelle parce que pratique et fait écho à la possibilité qu’une variable puisse apparaître plusieurs fois dans un terme du corps de la règle, comme dans « (r …) : (s A A). »

La seconde vue sépare mieux deux notions, celle de la collecte de termes d’après un schéma et celle de l’égalité. Elle met sur un même plan l’égalité et la non‑égalité. Avec la première vue, si deux variables différentes doivent être différente, ça doit être posé dans le corps de la règle mais ça ne peut pas apparaître explicitement dans la tête de la règle, l’égalité et la différence ont un status différent. Avec la seconde vue, l’égalité et la différence ont le même status, les deux doivent être posés dans le corps de la règle.

La première vue est humainement plus naturelle, la première vue est plus formelle. Une conversion de la première vue vers la seconde est possible automatiquement.

Techniquement, la première vue fait échouer plus tôt une tentative de vérification de règle qui ne peut pas aboutir, parce que l’échec de la vérification d’une égalité dans la tête de la règle, fait échouer dès ce moment là, l’unification d’une tête de règle et d’un terme. Avec la seconde vue, si les schémas correspondent, l’unification peut être vérifiée mais la vérification de la règle échoué plus tard, faute de vérifier l’égalité. Mais cette aspect technique n’est pas un aspect formel, il ne fait pas une bonne raison de choisir cette option, même si elle peut être préférée dans une mise en œuvre, après avoir démontré son équivalence.

Il a été dit que la première vue semble naturelle, comme elle fait écho à la possibilité pour une variable, d’apparaître plusieurs fois dans un terme du corps d’une règle. Mais la seconde vue, elle, semble plus naturelle par rapport à la notation qui a été proposée pour les termes récursif : les points d’entrées et de sorties des cycles, seraient énuméré à la suite, au lieu d’être nommée, ceci afin d’avoir une représentation autant canonique que possible. La seconde vue fait plus écho à cette notation, dans le sens où elle énumère des points d’entrée dans la tête de la règle.

Mais il y a surtout une autre différence entre la première est la seconde vue. Cette différence est incertaine, mais pourrait être fondée : la seconde vue pose explicitement l’égalité dans le corps de la règle, ce qui pourrait éventuellement avoir une conséquence sur la faisabilité de certaines démonstrations ou la formulation des propriétés de certaines règles. Avec la première vue, l’égalité de deux variables dans la tête de la règle, peut apparaître de deux manières, tandis qu’elle n’apparaît que d’une seule manière dans le seconde.

Pour une définition formelle, la seconde vue semble préférable, même si elle semble moins naturelle. Comme dit précédemment, définir la tête d’une règle avec la seconde vue, formelle, n’empêche pas de définir la tête d’une règle dans la syntaxe, avec la seconde vue, pratique.

Question probabilité, le cas de variables posant implicitement une égalité dans la tête de la règle, n’arrive pas souvent, ce qui fait que la seconde vision, un cas certes peu naturelle ou peu pratique, mais faisant peu souvent une différence en pratique.

L’idée du précédent message, ne serait cependant plus directement compatible avec l’idée d’avoir des têtes de règles à plusieurs termes, pour poser des conditions supplémentaires à des conjonctions de termes, en plus des conditions de leurs termes individuels. Parce que alors, il faudrait poser des conditions (au moins de possibles égalité de variables) à la nécessité de la vérification de ces conditions supplémentaires … quoique ça ne serait pas insensé, et alors ce serait la seconde vue du précédent message qui l’aurait révélé, possible sign que c’est effectivement la meilleure option pour une définition formelle.

Cette seconde vue a surtout l’avantage de bien séparer deux choses : la connexion établie par la tête de la règle, entre un terme et un corps de règle et les égalités de certaines variables, qui ne concerne finalement pas cette connexion, mais est une condition de la vérification de la règle. Distinguer ce qui est différent, ça peut aider.

Mais cet avantage supposé qu’il y aurait à donner le même statut à la différence et à l’égalité, est peut‑être inutile, parce que la mise en correspondance met l’accent sur des égalités. Un masque et posé sur un terme, les ouvertures du masque sont les variables, le reste du masque doit être en correspondance avec ce qu’il recouvre sur le terme, il y a là aussi une égalité implicite avec un status particulier par rapport à la différence (il n’y a pas de notion de différence requise, avec ce masque) et peut‑être alors que l’égalité implicite de certaines variables dans la tête de la règle, ne présente pas de risque de poser de problèmes à ne pas être distinguée d’une égalité posée explicitement dans le corps de la règle.

Sur l’égalité dans le langage.

L’idée de déplacer l’égalité des variables dans une tête de règle vers le corps de la règle, n’est pas tellement justifiée, même si l’idée n’est pas folle est équivalente, son intérêt théorique est faible et est cause d’une petite complication pratique, mais ultérieurement, pas au moment même de la définition du langage, où cette idée permet même une simplification.

Il n ’y a pas à remettre l’égalité à sa place, elle est quasiment partout, elle a une omniprésence que n’a pas la différence, c’est ainsi. Même si la différence existe et qu’elle peut devoir être posée comme condition, l’égalité a un status particulier, il n’y a pas de symétrie complète avec la différence. Elle est dans la correspondance et l’équivalence, elle est en pratique bien plus fréquente que la différence, autant que les termes positifs sont bien plus fréquents que les termes négatifs. Cette sur‑représentation d’une face par rapport à l’autre, doit signifier quelque chose, mais quoi …

L’égalité, eq, définie explicitement à partir de l’unification (oui, c’est possible sans régression infinie, comme expliqué plus loin), est nécessaire, pour au moins pouvoir définir la différence, neq, à partir de l’unification aussi (les conditions permettant de définir eq, sont les mêmes que celles permettant de définir neq). C’est la raison pour laquelle l’idée de l’égalité entre deux choses entièrement abstraites, a été abandonnée elle pose des problèmes sans solution, alors la petite simplification qu’elle permet, n’a plus d’intérêt.

Sans définition explicite de l’égalité, la différence ne peut se définir que comme la négation de l’égalité et nécessite d’introduire la négation même avant qu’elle ne soit nécessaire par ailleurs.

Pouvoir poser une définition explicite de la différence, en plus de permettre d’utiliser la différence avant même l’introduction de la négation, peut se faire en prouvant ultérieurement qu’elle est la négation de l’égalité, c’est à dire que quand neq est vérifiée, eq ne l’est pas et réciproquement. Seulement après l’avoir prouvé, neq pourrait être considérée comme la négation de eq. Cette preuve serait nécessaire pour la cohérence, il n’est pas envisageable de poser que la négation de eq est neq, par définition, il faut le prouver. Aucune telle preuve ne serait nécessaire en définissant la différence comme la négation d’une égalité sur des choses abstraites, mais comme expliquée plus haut, cette égalité là a dut être abandonnée.

L’égalité d’une chose concrète avec elle‑même, peut se démontrer d’après cette définition explicite de l’égalité, mais reste à savoir si ça peut être démontré en général.

Comment cette définition explicite de l’égalité peut‑elle être possible.

La règle de base de l’égalité, est formulée dans une définition du langage, qui suppose une interprétation de ce langage, d’après sa propre définition. C’est équivalent à un raisonnement sous une hypothèse, où la preuve de l’hypothèse est faite à posteriori. L’existence de l’égalité est comme une hypothèse implicite, à partir de laquelle une définition de l’égalité est possible à partir de l’unification, qui est une expression de cette hypothèse de l’existence de l’égalité. Une réalisation de la définition du langage, prouve implicitement cette hypothèse, même si d’une manière qui échappe au langage lui‑même. C’est ce qui explique que autant étrange que ça puisse paraître, l’égalité peut être explicitement définie et sans régression infinie.

En fait, ce n’est pas le cas qu’avec l’égalité, toutes la sémantique du langage de base est comme posée en hypothèse qui sera ultérieurement démontrée.

En plus de ne pas vérifier les termes avec une variable indéterminée, le langage de base n’aura pas de négation, ne supportera pas les termes cycliques, ni les les variables avec une arité autre que 1. Aucune de ces deux notions n’est nécessaire si tôt. Comme le langage ne fait pas de résolution, il ne peut pas produire des choses qui ne peuvent pas être écrites ; au contraire, il ne peut vérifier que ce qui peut être écrit et l’écriture de ce type de terme n’est pas nécessaire pour cette graine de langage.

Il y a effectivement une dysmétrie entre égalité et différence mais la différence n’est pas si absente, elle est implicite. La dysmétrie entre les deux, provient de leurs interprétations.

Il a été dit qu’un terme peut avoir plusieurs interprétations. Il a été dit que la définition d’une équivalence, définit implicitement une abstraction. Dans une égalité, il y a un implicite aussi : tout ce qui ne vérifie pas cette égalité. La différence, est une autre interprétation d’une égalité posée.

C’est ce qui explique la dysmétrie et explique aussi pourquoi l’égalité est beaucoup plus présente. Une chose est à égale seulement à elle‑même (même quand l’égalité est définie par une équivalence, mais oublions cet autre sujet). L’interprétation d’une égalité posée comme une différence, défini un nombre potentiellement infini d’entités différentes. C’est ce qui explique la dysmétrie. La différence est aussi généralement indéterminée, justement parce que, sauf conditions supplémentaires, on a pas à priori de définition réelle ou exhaustive de l’ensemble qu’elle défini. Au contraire, l’interprétation de l’égalité, est beaucoup plus déterminante. C’est la raison pour laquelle elle est bien plus fréquente. L’intention des règles, étant généralement de déterminer, d’où leur plus grand usage de l’égalité, tellement fréquente qu’elle est même par nécessité, implicite (dans l’unification surtout).

L’interprétation de la différence est moins précisément déterminée, et souvent quasiment pas (qu’est‑ce que soustraire un élément à un ensemble potentiellement infini …). La différence est la non‑égalité et les interprétations de la négation ou de la double‑négation de termes, sont des solutions généralement seulement partiellement déterminées. C’est normal, il existe un lien quasiment directe entre les deux. C’est pour la même raison que les termes négatifs sont moins fréquents : ils déterminent moins.

La différence est autant déterminante que l’égalité, dans un seul cas : quand le domaine n’a que deux éléments.

L’égalité, est une autre justification à traiter les variables non‑liées, comme indéterminées.

L’égalité, l’air de rien, a deux interprétations : sous une résolution et sous une vérification. Sous une résolution, l’égalité entre deux variables non‑liées, lie ces variables entre elles. Sous une vérification, l’égalité entre deux variables non‑liées, n’est pas définie, à moins qu’on ne compare leurs identités, ce qui n’est jamais formulé et n’apparaît que dans la définition de la sémantique du langage, pas dans son application.

Considérer que le sens des variables non‑liées, en elles‑mêmes, est celui qu’elles auraient dans la vérification, ne devrait pas surprendre.

Une condition de salubrité, informelle, pour la négation par l’échec dans une vérification.

Pour la vérification, la négation ne peut être que la négation par l’échec. L’échec d’un terme, signifie qu’il n’est pas correcte d’après les règles. Dit comme ça, c’est perturbant, parce que intuitivement, la négation n’est pas une non‑pertinence. Ça peut se clarifier ainsi : la négation d’un terme constant est probablement suspecte, elle devrait plutôt s’appliquer à un terme contenant des variables (supposées déterminées à l’instantiation de la règles), qui pourraient éventuellement être correctes. C’est à dire qu’il devrait exister une substitution à ces variables, pouvant en faire un terme correcte, en dehors de la négation.

Une idée pourrait être d’apporter une preuve de satisfiabilité du terme mis en négation. Mais il n’y a pas de nécessité, ni sémantique ni technique, à le faire. C’est juste pour dire qu’un terme en négation, n’a vraiment de sens que si le terme peut avoir un sens sans la négation.

Après tout, on pourrait en dire autant des termes positifs. Un terme positif qui n’est jamais vérifiable, c’est autant suspect aussi, même si dans le cas de la négation, la question se pose plus facilement.