Les logiques : notes en vrac

Ce n’est pas très important, mais juste pour le dire. Le mieux dans le cas de l’exemple, est d’avoir une règle démontrant la symétrie de eq, une règle « (eq B A) : {(eq A B)}. », d’utiliser cette règle pour prouver « (const B) : {(eq A B)}. » à partir de « (const A) : {(eq A B)}. ». Au moins, même si on écrit une preuve supplémentaire pour réduire une autre au minimum, c’est en ajoutant une preuve assez évidemment utile.

Par exemple :



Le nombre de règles, est de toutes manières difficilement réductible, il ne faut pas tellement y voir un problème. Avec deux ensembles, pour démontrer une relation et sa réciproque entre ces deux ensembles, il faut deux règles, à multiplier par les relations entres arguments, ici deux pour une règles et un pour l’autre règle, donc à multiplier par deux. Moins, ce n’est simplement pas possible et alors il ne faut rien y voir de pathologique.

Une autre solution serait de considérer la question au moment de la création de la règle. La règle eq par exemple, est écrite en ayant à l’esprit que le domaine de ces arguments est défini par const et est écrite en conséquence. Mais ça n’apparaît pas explicitement, raison pour laquelle ça doit être démontré. On peut imaginer d’en faire un fait explicite, que la règle soit définie à partir des cas des paires de consts, ce qui serait plutôt une formule décrivant la règle, à partir de laquelle pourrait être produite automatiquement la règle et la preuve de la couverture. Ça ne pourrait pas faire partie du langage de base, ça en serait une extension assez conséquente.

Ce qui est décrit plus haut, peu faire penser à l’écriture d’une fonction conformément à un type, pour prouver ensuite qu’elle a ce type. Ça peut sembler être un gaspillage si on pense en terme de langage informatique ordinaire, mais ici, c’est un langage sémantique, et la fonction en question pourrait en principe avoir plusieurs types ou même, en supposant l’extension décrite plus haut, être écrite pour correspondre à plusieurs types en même temps, les règles produites étant vérifiées équivalentes ensuite, pour n’en conserver qu’une les représentant toutes et pour laquelle seraient disponibles toutes les preuves en rapport.

Il faut peut‑être aussi ajouter « T : {T}. ». Ce qui suit est sous réserve d’erreurs.

Cette règle peut sembler inutile, pourtant elle explique pourquoi et comment un terme en hypothèse, attend que son hypothèse soit confirmée avant que les conclusions qui en dépendent soient réalisées.

Si on est sous une hypothèse {H2}, qu’on peut en dérive un A, c’est parce que ce A est dérivable d’un H1 concret. Quand un H3 concret arrive plus tard, voici le sens de ce qu’il se passe : H3 est mis en correspondance avec {H2} qui peut effectivement laisser la place à H1 dérivée de H3.

La chaîne est ainsi : H3 -> {H2} -> H1. C’est parce que {H2} est substitué par H1, que ce qui en dépendait à travers sa promesse {H2}, peut se réaliser. Cette étape est représentée par le règle « T : {T}. », qui peut être considéré comme une véritable règle, telle qu’elle est écrite, mais elle n’a pas de démonstration, elle est, c’est tout.

Mais par quelle règle serait représentée l’étape H3 -> {H2} ? En tous cas, pas par une règle du genre « {T} : T », parce que dans cette étape, {H2} existe déjà, comme H3 est mis en correspondance avec {H2}, ce qui ensuite permet à {H2} de laisser la place à H1. Au contraire de ce que dirait « {T} : T », {H2} peut préexiste à H3, ce qui est même souvent le cas.

Il faudrait aussi une règle représentant le passage d’une hypothèse à travers une hypothèse au lieu du passage d’un terme à travers une hypothèse. Dans le message précédent, la démonstration de §eq-swapped en contient un exemple, dans le cas §eq-s et ça semble incontournable.

Idée de formulation : une hypothèse peut prendre la place d’un terme mais ne peut pas rester à la place d’un terme ; un terme peut prendre la place d’une hypothèse ou d’un autre terme et y rester ; quand une hypothèse prend la place d’une hypothèse, c’est en prenant la place d’un terme.

La question proche, est l’idée de permettre d’interpréter les relations entre termes, en dehors de leurs interprétations au sens courant. Le problème avec l’idée initiale, était de l’appliquer à une tête de règle en temps que telle, il est plus pertinent de l’appliquer à des termes résolus ou partiellement résolus. Les relations interprétables comme des constats ou des jugements seraient : T1 plus spécifique que T2, T1 sans relation de spécificité avec T2, T1 et T2 sont égaux (sans résolution), T1 et T2 sont possiblement unifiables, T correspond à aucune/une/plusieurs règles candidates, T est entièrement déterminé. Les relations de spécificité, seraient la formulation des relation entre ensembles précédemment envisagées, mais pas seulement et en notant que des relations entre ensembles peuvent être formulées par des règles ordinaires.

Ce serait des constats, sans résolutions. L’égalité existe comme résoluble, elle serait là, un constat sans chercher à la résoudre. Quelque part, les relations de spécificité pourraient être résolubles, on pourrait résoudre un terme T1 de manière à ce qu’il soit plus spécifique qu’un terme T2, mais ça ne pourrait se faire que d’une manière arbitraire, ce sont les résolutions par les règles qui rendent les termes plus spécifiques, avec du sens. Par contre, connaitre la relation de spécificité entre deux termes, n’est pas arbitraire, chaque terme ayant un sens, elle dit qu’un terme peut être vu comme dérivé d’un autre, donc qu’un sens peut être vu comme dérivé d’un autre ou qu’un terme en couvre un autre ou plusieurs autres, en plus de la relation ensembliste qu’on peut y voir. Résoudre l’unification de manière à rendre deux termes unifiable, n’aurait pas de sens et de manière à les rendre non‑unifiable, se ferait d’une manière arbitraire (au contraire de not (eq A B) qui a un sens) avec les mêmes remarques que pour les relations de spécificité.

La raison pour laquelle ces relations seraient sans résolution, peut collectivement se résumer ainsi : ces relations ne sont pas définies par des règles et alors les résolutions ne seraient pas associées à un sens. La définition de ces relations n’est elle‑même pas arbitraire, il s’agit de relations existant implicitement dans la sémantique du langage, qui les rendrait accessibles.

Le cas d’une démonstration où l’hypothèse n’est pas suffisante pour donner une solution avec liaison unique, pour une variable, doit être considéré comme un échec de la démonstration. En plus de l’arbitraire qui ne peut pas rester dans le langage, il semble que ce problème trahit une erreur.

Il avait été dit que les couvertures devraient pouvoir être vérifiées, pas tellement en pensant à ce cas simple qui avait été dit évident, mais en pensant à d’autres cas plus compliqués.

Voici peut‑être une piste de réponse au problème rencontré et une illustration qu’on peut toujours faire une bourde inexcusable, même sur un cas simple. La règle neq est incorrecte et c’est peut‑être ce que trahit cet arbitraire dans une démonstration l’impliquant.

Il y a une erreur dans les règles ci‑dessous, sauras‑tu la trouver ?

§neq-b1 (neq () (C)).
§neq-b2 (neq (C) ()).
§neq-s (neq (C1) (C2)) : (neq C1 C2).

L’erreur est dans les deux cas de base, ils sont vérifiées par un variable indéterminée. Ils devraient avoir une condition est être réécrits ainsi :

§neq-b1 (neq () (C)) : (const C).
§neq-b2 (neq (C) ()) : (const C).
§neq-s (neq (C1) (C2)) : (neq C1 C2).

Parce que cette condition manquait, le domaine des arguments de neq, était plus vaste que celui défini par const et alors il ne pouvait que se passer quelque chose de perturbant en essayant de démontrer qu’ils sont égaux. C’est probablement cette erreur que trahis la solution arbitraire qui a dut être posé dans une démonstration.

Le message concerné contient peut‑être d’autres erreurs, il est à revoir entièrement.

Ce serait mieux dit ainsi : la sémantique ne connait pas ce qui est textuellement. Si deux variables dans deux règles différentes ont le même nom, ça n’a aucune conséquence pour la sémantique des règles, idem si elles n’ont pas le même nom. Deux variables du même nom dans deux règles différentes, sont textuellement les mêmes, mais pas littéralement les mêmes. Deux variables du même nom dans une même règle, sont textuellement et littéralement les mêmes, mais la seule chose qui importe, est qu’elles le soient littéralement, parce que après tout, il n’est même pas garanti qu’elles le soient textuellement, comme on peut imaginer une notation disant quelque chose comme « la même variable que précédemment », qui serait textuellement différent de la variable précédente, mais serait littéralement la même chose.

Un langage de démonstration est nécessaire dans le langage de base, mais celui utilisé jusqu’ici, est encore trop élaboré pour être élémentaire, même s’il ne l’est pas assez en pratique (et en pratique, il y a probablement toujours quelque chose à redire, comme une démonstration peut être compliquée).

Il faudra revenir sur ce langage, pour distinguer ce qui est nécessaire de ce qui est optionnel. Une démonstration est celle d’une règle, il faudrait une formulation des démonstrations, qui s’approche au plus près possible de la formulation des règles les plus courantes que sont les définitions.

Avec un doute que c’est peut‑être en partie une répétition, autant que c’est peut‑être une idée pas encore écrite.

Il pourrait être intéressant d’envisager de remplacer l’indétermination d’une variable, par une hypothèse, en notant qu’un terme partiellement déterminé, contient toujours au moins une variable entièrement indéterminée (c’est le cas de base).

Quand une variable est indéterminée, dans une résolution ayant plusieurs solutions pour cette variable, la solution de la variable pourrait être une hypothèse sur la variable, à moins que la solution ne soit unique et alors la solution de la variable est cette solution unique. La solution unique serait un terme unique, possiblement partiellement déterminé et c’est alors la solution à ces parties indéterminées, qui serait décrite par une hypothèse, de la même manière, sauf solution unique. Pour savoir qu’il existe plus d’une solution, il suffirait à la résolution d’en vérifier au moins deux, il n’y a pas besoin de toutes les trouver.

Mais dire que la solution à une variable est une hypothèse, nécessite de poser une hypothèse sur cette variable et poser une hypothèse sur une variable, gèle la variable et bloquerait la suite de la résolution, empêchant de trouver des solutions ; des exemples de cette situation ont déjà été vus.

Une vague idée de solution à ce blocage pourrait être ainsi : l’hypothèse est une solution dans un contexte où la variable a plusieurs solutions, si le contexte change, les solutions de la variable changent peut‑être aussi, il est alors tenté de résoudre le terme de l’hypothèse. Si le nouveau contexte fait que la variable n’a qu’une solution, la variable est liée à cette solution et l’hypothèse est abandonnée, sinon la solution de la variable est une nouvelle hypothèse remplaçant la précédente qui est abandonnée. Dans les deux cas, l’ancienne hypothèse est abandonnée, elle est remplacée soit par une solution unique soit par une nouvelle hypothèse.

Quand le contexte change, tous les termes liés à ce contexte changent implicitement, un terme qui devient déterminé sous un nouveau contexte, le devient implicitement. Contrairement à un terme, une hypothèse doit être réévaluée pour devenir un terme déterminé, elle ne se transforme pas implicitement en un terme déterminé, d’où la nécessité de la procédure vaguement décrite.

Il y aurait une condition : la méthode ne devrait pas faire prendre le risque de croire à une absence de solution quand il y en a pourtant au moins une.

— Édit : cette idée conviendrait peut‑être mieux pour la double et la simple négation, ou alors si on considère que les solutions sont toujours présentées ainsi, alors il n’y a plus de différence entre la double négation et l’absence de négation. Mais là encore, ce n’est qu’une vague idée. —

L’alpha‑équivalence (égalité modulo les noms des variables) n’existe pas pour les termes, seulement pour les règles et encore, sous réserve.

Précédemment, a été souligné que deux termes différents peuvent désigner la même chose. Ce n’était rien de nouveau, mais c’était auparavant une curiosité théorique et cette relation a eu pour la première fois une application pratique importante.

Il a été précisé que la conclusion de cette comparaison entre deux termes, vaut pour un contexte donné. On peut alors imaginer cette comparaison pour le contexte global, vide, et en allant trop vite, penser à l’alpha‑équivalence (termes identiques modulo un renommage des variables) entre deux termes. Mais si on pense que l’équivalence entre deux choses, implique qu’on peut substituer l’une par l’autre, en essayant d’imaginer qu’on substitue un terme par un autre qui lui est alpha‑équivalent, après quelques secondes, on peut pressentir que quelque chose cloche. En effet, l’alpha équivalence entre deux termes, ne signifie pas qu’on peut remplacer l’un par l’autre et elle devrait alors être considérée comme non‑définie pour les termes. Si on imagine le cas de la conjonction (r1 A) & (r2 A) et de la conjonction (r1 A) & (r2 B), alors (r2 A) est alpha équivalent à (r2 B) et pourtant on ne peut pas substituer l’un par l’autre, à cause de la situation de la variable à l’extérieur du terme. Si on comparait ces deux termes à la manière décrite en parlant d’un type de récursion, dans le contexte globale, comparés de cette manière, les deux termes seraient différents.

Il ne faut pas voir l’alpha‑équivalence comme un cas de l’équivalence sur des termes, dont il a été question. L’alpha‑équivalence ne vaut même pas pour une conjonction, comme les variables d’une conjonction peuvent apparaître dans la tête d’une règle et alors avoir une situation externe à la conjonction. Cette équivalence ne vaut justement que pour les règles, et c’est encore seulement si on exclut la possibilité de variables globales pour des raisons pratiques.

Plus brièvement, l’alpha‑équivalence n’est valable que si on la vérifie pour l’ensemble de la portée la plus large de toutes les variables concernées.

Sur les constats, alias les jugements, qui posent des problèmes difficiles. À moins que ces problèmes ne finissent par être tous résolus, cette idée des constats en supplément des standards false et true, sera abandonnée.

Il a été dit qu’ils se font sans chercher à les résoudre. La raison a été expliquée précédemment. En résumé, la résolution est définie par les règles, les constats ne sont pas des règles et ne peuvent justement pas l’être, raison de les exposer de cette manière. Ce point n’est pas remis en cause jusqu’ici.

Il a été dit qu’ils sont testés après la résolution. La raison déjà donnée est qu’une règle n’est pas toujours vérifiée en résolvant ses termes, elle peut l’être à partir de termes fournis, qui peuvent devoir être en parti résolu, mais qui peuvent aussi déjà l’être entièrement. Si les constats se faisaient avant la résolution, ils ne seraient pas applicable dans ces cas. Une double‑confirmation pourrait être que de toutes manières, un terme sans aucune résolution n’a pas beaucoup de sens, comme dans « A & not A », et un constat sur un terme qui n’a pas de sens, n’en aurait pas non‑plus ; les termes d’une règle se comprennent dans un contexte où ils sont vérifiés, sans quoi ils sont oubliés. Le problème est que la résolution d’un terme évolue au fil de contextes successifs, ce qui va poser le plus gros des problèmes décrits plus loin, sans compter que d’autres viendront encore plus tard.

D’abord un problème déjà en partie mentionné. Disons qu’on a la conjonction A false & B, si A & B est résolu puis que le constat A false est testé ensuite, en imaginant pas plus d’une seconde (vraiment pas plus) que ce constant est avéré, alors B qui a été résolu pour être en accord avec A, n’est pas cohérent, puisque pas en accord avec A false. De toutes manières, A false ne peut jamais être constaté, comme l’échec de A provoque l’échec de la conjonction et son abandon.

Note en marge : si on tente d’imaginer un instant que A false explicite, est comme un A true s’il est testé sur un A false implicite, alors A false false est A true et alors false n’est pas un constat rapportant l’échec, mais une interprétation du constat d’échec en faisant la négation.

Mais c’est le constat false, qui n’est pas quelconque. C’est peut‑être plutôt la confirmation que A false ne peut pas être un synonyme de not A, y compris en l’absence de résolution. Ce constat n’est peut‑être pas à exclure pour autant. Ici, il accompagne une condition de l’abandon de ce sur quoi il est sensé être constaté, ce serait différent avec une chose pouvant être non‑vérifiée sans pour autant être abandonnée. Par exemple et même si le sujet est les constats sur des termes, une règle « A : {B}. » pourrait avoir été démontrée impossible (un type de démonstration par encore prévu, mais imaginons), ça ne provoquerait pas pour autant l’abandon de l’ensemble des règles, ça empêcherait seulement d’appliquer cette règle et on pourrait même imaginer qu’on ait justement voulu s’assurer que cette règle est une contradiction.

Note : que le paragraphe précédent dit que le constat false pour une règle, signifierait qu’elle est impossible, contradictoire, ne doit pas surprendre, il ne faut pas oublier que c’est ainsi pour les termes, un terme en échec, est un terme impossible, en contradiction avec son contexte.

Le constat A false pourrait malgré‑tout être posé dans une règle, ce ne serait pas une erreur de l’y écrire, mais il ne pourrait jamais être vérifié, son hypothétique vérification serait une auto‑contradiction du langage, la présence de ce constat rend nécessairement une règle non‑satisfiable.

Un exemple de constat autre que false et true, comme c’est tout de même le but. Disons qu’on a un constat nommé const, qui teste si un terme est constant. Si on a une conjonction A const & B, A & B est résolu, si A n’est pas constant, la conjonction est en échec malgré‑tout. Ça ne peut pas faire mentir l’accord entre les termes, puisqu’ils sont tous oubliés dans le même temps. Ça n’introduit pas non‑plus d’incohérence dans le langage, faire échouer une règle qui était initialement vérifiée, n’est pas la même chose que de poser une règle négative, ce qui est exclus pour les raisons déjà expliqués. Il n’y a pas de moyen de transformer une règle « A : C. » en une sorte de « not A : B. » en présence de « A : B. », en faisant échouer « A : C. », même inconditionnellement, parce que ça ne permet pas de vérifier à la fois A et not A, ça ne fait qu’empêcher de vérifier « A : C. » qui en serait non‑satisfiable.

La conjonction prise en exemple plus haut, même résolue et retenue, n’est typiquement pas à la fin de toute résolution, si la conjonction est celle d’une règle mentionnée par une autre règle. Le problème est que si dans A const & B, A n’est pas constant après la résolution de cette seule conjonction, il le sera peut‑être par la suite. De plus, même s’il n’y a pas de dépendance à l’ordre des termes dans la conjonction, il peut y avoir une dépendance à l’ordre des termes dans une conjonction « englobante ». Les constats ne pourraient alors être testés qu’en toute fin de résolution, à moins qu’ils ne portent sur des termes entièrement déterminés, dont il est certain qu’il n’évolueront plus, ça ne peut pas être le cas général. Les termes sujet à un constat devraient donc être conservés et les constats testés à la toute‑fin de la résolution.

Se pose aussi un problème d’intégration avec la négation. Si on a « A : B const. » et quelque part ailleurs, not A, B est résolu en négatif, mais comment est sensée être interprété le constat const dans ce cas ? Cette question est à noter, mais elle n’est pas discutée pour le moment.

Pourquoi les constats implicites false et true ne posent pas temps de problème ? Une piste pourrait être dans cette question : qu’ont‑ils de prévisible faisant qu’ils n’ont pas besoin d’être testés seulement à la toute fin de la résolution ? Quand un terme échoue dans une conjonction, on sait qu’il échouera dans un contexte plus spécifique. Le constat true est l’absence de constat false, comme le constat false (celui implicite) ne pose pas de problème, celui de true non‑plus. Le constat false est un point d’arrêt et true se vérifie temps qu’il n’est pas arrêté par false ; ce n’est pas formel, mais c’est plus facile à imager. Ou une autre manière de le voir : quand le constat est false, ça ne change pas, true est true jusqu’à ce qu’il devienne false, et à partir de là, ça ne change plus.

Peut‑être que ça suggère d’aborder la question ainsi : il faut penser à comment les constats évoluent dans un contexte plus spécifique. Considérer qu’un constat est l’absence d’un certain constat négatif et que le constat négatif, s’il est vérifié dans un contexte, ne pourra que l’être aussi dans un contexte plus spécifique. Si le constat const est l’absence du constat var, alors peut‑être que le problème se comprend mieux, comme le constat var, s’il est vérifié dans un contexte, n’est pas dans le cas de ne pouvoir que être vérifié dans un contexte plus spécifique. Le constat const serait par contre, un bon candidat de constat négatif. Si const est vérifié dans un contexte, il ne peut que l’être dans un contexte plus spécifique. Alors un constat var, défini comme l’absence du constat const, serait‑il autant exempt de problème que le constat true ? Comme A true qui est tenu pour constaté jusqu’à preuve du contraire, var pourrait être tenu pour constaté jusqu’à preuve du contraire, suivant alors la même évolution que les constats implicites : const vérifié dans un contexte, ne peut que l’être dans un contexte dérivé, tout‑comme false, et var vérifié dans un contexte, peut être remis en cause dans un contexte dérivé, tout‑comme true (le constat true devient false, similairement, le constat var devient const), et ça ne change plus dans les contextes dérivés.

Ce n’est qu’une idée vague sur un problème malheureusement compliqué. S’il n’a pas de solution, l’idée des constats supplémentaires en plus des true et false implicites, sera abandonnée. Après avoir repris à la suite du paragraphe précédent, il faudra se poser la question des constats sur des relations entre deux termes, comme T1 plus spécifique que T2.