Les logiques : notes en vrac

C’est de cette citation que partira ce message. Il est en deux parties, une courte qui douche une illusion, puis une plus longue plus intrigante.

Le résolution des requêtes Prolog ou Prolog‑like, peut facilement finir en boucle infinie et il a été dit peu après, que cet interpréteur sera le sujet d’une première tentative de démonstrations des propriétés d’un logiciel, des fonctions qui le constituent.

La fonction de recherche des solutions à partir de clauses partant dans de possibles récursions infinies, ça ne peut que décevoir l’espoir de faire une démonstration de bon fonctionnement en général, puisque des exemples du contraires sont triviaux à produire. Ça montre que parfois il est nécessaire de se contenter de moins. Avec ce cas, il ne pourra pas être possible de faire mieux que démontrer que les solutions de la liste de solutions renvoyées par cette fonction, sont des solutions répondant bien aux termes de la requête et en conformité avec les règles. Mais ça peut avoir une limite espiègle : on pourrait faire cette démonstration trivialement pour une fonction ne renvoyant jamais rien : si on doit montrer que quand la fonction renvoi quelque chose, ce qu’elle renvoi et valide, alors il suffit qu’elle ne renvoi jamais rien, et le tour est joué. Ça peut poser la question du raisonnable derrière ce type de démonstration. Le problème peut se poser de deux manières. La première est par la pratique, vérifier que la fonction ne se contente pas de ne jamais rien renvoyer, et ça c’est facile. La seconde, plus difficile, et de caractériser précisément et exhaustivement, les ensembles de règles et requêtes pour lesquels la fonction saura toujours donner une réponse. La première solution est la plus accessible, la seconde me semble beaucoup plus compliquée, mais si elle est accessible, elle est bien préférable.

Mais … cependant et ce problème mis de côté, il est possible d’éviter certaines de ces récursions, et ceci sans même réordonnancer les règles. Je pressens assez clairement deux solutions pour deux cas assez généraux, sans donner de détails que d’ailleurs je ne connais pas encore entièrement moi‑même.

L’importance de pouvoir démontrer qu’une fonction ne finit pas en récursion infinie, a été abordée plusieurs fois. Mais le cas qui se présente est différent. Il faudra démontrer que certaines tentatives de recherche de solution seront abandonnées par la fonction, parce que ces tentatives finiraient avec certitude en récursion infinie. C’est là qu’on va commencer à glisser dans un monde de doutes.

Non seulement il est utile de pouvoir démontrer la non‑récursion infinie, mais il semble maintenant autant utile, de pouvoir démontrer la récursion infinie. La récursion infinie ne serait plus une chose qu’on ne ferait qu’éviter, mais une chose avec laquelle on traiterait.

Comme on manie toujours des représentations (de choses réelles quand‑même), vient la question de représenter la conclusion d’une fonction partie dans une récursion infinie. Je penses à ⊤. Oui, ⊤, pas ⊥. Pourquoi ? Parce que ⊥ est une contradiction, mais bien que irritante, une récursion infinie n’est pas une contradiction. Dans certaines logique, de ⊥ on peut tout conclure, mais dans toutes les logiques mentionnées jusque maintenant, on ne peut rien conclure de ⊤, ce qui est justement le cas d’une récursion infinie qui ne renvoi jamais de résultat. De plus, comment une fonction qui ne renvoi jamais rien, pourrait‑elle aboutir à une contradiction ? La récursion en semble même une indiscutable négation de la contradiction. Donc ⊤ serait la négation de ⊥ ? Pourtant, dans les logiques présentées jusqu’ici, il n’y a pour ⊤, qu’une règle d’introduction et pas de règle d’élimination, et pour ⊥, qu’une règle d’élimination et pas de règle d’introduction, et là, on aurait une relation entre les deux. Sans certitude, mais la question est à se poser : ⊤ pourrait‑elle être la négation de ⊥ ?

Aussi, comment justifier d’introduire que ⊤ serait la conclusion d’une fonction ne renvoyant rien ? Peut‑être serait‑il possible de le faire ainsi : par défaut, toute fonction serait supposée renvoyer ⊤ à moins qu’il ne soit prouvée qu’elle renvoi autre chose. Ce n’est là aussi, qu’une idée, je ne me risque pas à affirmer. Reste à savoir comment pourrait être justifiée l’élimination de ⊤.

Est‑il correcte de seulement vouloir parler d’infini dans des démonstrations ? Probablement oui. Ici, une fonction partant dans une récursion infinie, est une représentation de l’infinie, un objet fini qui n’est infini que si on s’engage dans son tourbillon. Mais une représentation d’un infini bien réel quand‑même, comme le montre concrètement n’importe programme piégé dans une récursion infinie. Si on traite avec une représentation de l’infinie, on ne se laisse juste pas enfermer dedans. C’est un infini en intention, pas un infini en extension comme dans le déroulement d’un programme.

Comment pourrait se comporter ⊤ dans des conjonctions et des disjonctions ? Pour une conjonction, ça devrait normalement la réduire à ⊤. Si ⊤ peut être introduite par les récursions infinies, une conjonction de plusieurs fonctions dont une seule part dans une récursion infinie, c’est une récursion infinie tout‑court (en oubliant les questions du genre call‑by‑value vs call‑by‑need). Dans une disjonction, ⊤ ne resterait qu’un élément de la disjonction, mais resterait comme une épine quand il s’agirait de faire une conclusion valable sous tous les cas d’une disjonction, comme on ne peut rien conclure de ⊤. De là vient la nécessité de pouvoir éliminer ⊤ par une règle assez indiscutablement justifiée.

Je ne vois pas le lien, mais me demande s’il n’y aurait pas une lueur du côté de l’implication et ses raisonnement hypothétiques ; c’est justement qu’ils soient hypothétiques, qui me fait espérer de la voir comme une lueur dans cette brume.

Finalement l’autre chose se résume en peu de mots :

Ce qui a été dit s’applique aussi aux instructions conditionnelles, qui elles aussi ressemblent plus à des séquents. Un détail important qui a aussi été oublié, est que A ⊢ B ne signifie pas que les cas d’occurrences de A sont inclus dans les cas d’occurrences de B, ni même la réciproque (mais il devrait toujours être possible de trouver un contexte minimum vérifiant cette propriété dans l’autre sens), ce qui achève de montrer à quel point le séquent est différent de l’implication, et même que la dérivation est différente de l’implication.

Le concept derrière le séquent est finalement tellement fréquent, qu’on pourrait dire que l’implication est une exception et que c’est le séquent qui est la règle, ce qui fait aussi un jeux de mot qui aide à s’en souvenir.

La manière de lire une implication, qui avait été proposée, dans l’autre sens et sans hypothèse non‑fondée, c’était finalement la manière de lire un séquent. J’ai donc tourné en rond avec mes explications . Mais ça fait quand‑même penser à souligner que à droite d’un séquent, on pas une conséquence automatique, mais une possibilité, quoiqu’il est possible qu’une possibilité ait plus d’importance que ça dans certains cas (ex. une chose qui n’est pas possible quand existe une certaine possibilité).

Quand il a été dit que la logique n’interprète pas les connecteurs du langage objet, il aurait fallut ajouter que c’est aussi le cas de ses constantes. Par exemple le vrai et le faux des booléens d’un langage informatique, ne sont pas interprétés par la logique, et quand c’est le cas, c’est seulement indirectement pas association. Ces associations sont possibles avec n’importe quelles constantes.

Il a été suggéré que ⊤ pourrait convenir comme représentation de la seule chose pouvant être conclue d’une récursion infinie, le rien. Il y a un autre point commun. La règle d’introduction de ⊤, est sans aucune condition. On peut autant sans condition particulière, créer une récursion infinie (à moins qu’un langage ne dispose pas de la récursion). Peut‑être que ça pourrait confirmer que cette proposition convient.

Il y a une question qui pourrait donner une piste. Si on écrivait une fonction pour la division de deux nombres, et qu’on voulait ne jamais produire d’exception, on la définirait pour le diviseur zéro, comme renvoyant une constante spéciale, ne contenant pas de valeur et ne pouvant pas être utilisée comme argument d’opérations sur les nombres. C’est ce que font certains langages. Dans ce cas là, la proposition ⊤ serait attachée à la constante quand elle est renvoyée par cette fonction et représentant son résultat.

J’ai du mal à le fonder clairement, mais je me demande si en fait cette question ne serait pas plus une question de sémantique que de logique. Après‑tout, qu’est‑ce qu’une logique sait de la récursion infinie ? Rien, elle ne connait même pas la récursion, « que » des étapes, des transitions, et même le raisonnement par induction réduit une récursion à un nombre de cas de transition, que nous, nous interprétons comme la récursion. Cette proposition qui correspond bien à la récursion infinie, la logique n’en dit rien et n’en fait rien, elle ne fait que poser son existence (je me demande d’ailleurs ce qui a fondé l’idée de poser cette proposition, ça devrait être intéressant de le savoir). Si la logique n’en dit rien, c’est peut‑être à la sémantique de le faire. Que ses propriétés dans la logique correspondent bien aux propriétés réelles qu’elle représente (les comparaisons faites précédemment), c’est bon signe, mais ça ne fait pas encore avancer concrètement. Par exemple, ça ne dit encore pas comment avec cohérence, traiter ⊤ dans un disjonction représentant une couverture de cas.

Sinon, plus concrètement, il n’y a pas que la question de la récursion infinie ne pouvant qu’aboutir à rien, il y a aussi la question de la récursion infinie produisant une séquence infinie de résultats, mais qu’elle ne renvoi jamais, comme elle n’achève jamais cette séquence. Ce cas est différent, si on limite arbitrairement cette fonction, par exemple à un nombre de résultats maximum, elle renverra quelque chose, c’est seulement que si on ne la limite pas pas arbitrairement, elle ne renverra jamais rien.

Ce fait pourrait‑il suggérer une piste ? Il semble suggérer qu’on peut toujours délibérément ignorer ⊤ dans une disjonction (jusqu’au point d’éliminer toute une disjonction si elle ne contient rien d’autre que des ⊤ ?) et garder tout le reste de la disjonction, mais je ne suis pas à l’aise avec cette idée. Pourtant, ce ne serait pas incohérent : s’il est possible d’introduire ⊤ sans condition, ça signifie que chaque fois qu’on a A ⊢ B, en oubliant pas que à droite d’un séquent, on a une disjonction, on peut aussi le voir comme A ⊢ B, ⊤ comme on peut toujours avoir A ⊢ ⊤, et que alors sans le savoir, on voit toujours en fait un A ⊢ B, ⊤ comme un A ⊢ B en ignorant un ⊤ virtuel qui serait présent dans toutes les disjonctions. Ça pose quand‑même un possible problème, certaines logiques au moins n’acceptant pas les conclusions multiples à droite d’un séquent, sûrement pas sans raisons, mais c’est une question différente, la question ici étant surtout comment traiter ⊤ dans une disjonction, avec la certitude de ne pas prendre des risques avec la logique. Resterait à expliquer pourquoi il n’existe pas de règle d’élimination de ⊤, si ces idées sont vraiment correctes.

Il avait été dit qu’il y a plusieurs théories de choses dont on aurait put croire qu’il n’y en a qu’une seule, qu’il y aussi plusieurs logiques et non‑pas la logique au singulier.

Il en va de même avec Prolog. En me faisant des démonstrations informelles qu’il est possible de faire une interprétation censée de certains cas au moins de récursions infinies, j’ai voulu savoir si ces idées sont compatibles avec la sémantique formelle de Prolog,  que j’ai voulu consulter … pour découvrir qu’ils en existent plusieurs et non‑pas une seule.

Un cas de divergence qu’on peut introduire sans chercher loin, est avec l’unification de deux termes. Je savais déjà que le Prolog classique n’accepte pas les termes cycliques qu’il considère comme non‑unifiable, mais il semble que à propos de savoir si deux termes cycliques devraient être unifiables ou pas, les avis divergent. Personnellement, je ne suis pas d’accord avec l’idée que des termes cycliques signifient nécessairement une erreur, je crois plutôt qu’ils sont une formulation naturelle de certaines choses et d’ailleurs les graphes cycliques n’ont jamais été vu comme des aberrations en général. Mais c’est un avis personnel.

C’est pour l’unification des termes, seulement, pas difficile alors d’imaginer que des divergences encore plus délicates peuvent exister concernant certains types de circularité dans l’application des règles, mais je n’ai rien vu le mentionnant (je n’ai pas cherché des heures non‑plus).

Sans surprise d’après ça, il semble qu’il n’existe pas une mais plusieurs sémantiques pour Prolog, ce qui justifie de parler de Prolog‑like (je le faisais déjà sachant que mon interprétation n’est pas celle standard, mais je ne pensais pas qu’elle diverge autant) pour souligner les éventuelles divergences.

La logique ne peut pas être dissociée de la sémantique et la récursion infinie est une bonne colle.

Comme la question divise, je ne parlerai plus de cette récursion infinie, parce que j’allais le faire en prenant justement mon interprétation de la résolution en Prolog comme modèle (il y a récursion infinie et récursion infinie, en fait). Mais ça souligne qu’il serait intéressant d’aborder la question de savoir comment définir une sémantique et s’assurer que la logique qu’on utilise est cohérente avec cette sémantique. Ça serait moins osé et plus généralement util.

Je ne suis même pas sûr qu’il n’y aurait pas d’incohérences avec l’interprétation la moins expressive, de détecter les cycles, pas dans les unifications, mais dans l’application des règles, en les interprétant alors comme des échecs, en évitant au moins d’entrer dans ces récursions infinies.


En marge, c’est sûrement util, malgré les avis personnels, de considérer une interprétation de Prolog qui soit le plus petit dénominateur commun, qui n’unifie pas les termes qui sont des graphes cycliques, n’interprète en rien les cycles dans l’application des règles (même pas pour s’interdire d’y entrer), au moins pour voir si certaines choses restent démontrables avec. Si elles restent réalisables, ces démonstrations en seraient plus convaincantes. Il serait aussi intéressant de savoir si cette interprétation réduite au minimum, permettrait de démontrer au moins certaines propriétés significatives d’autres interprétations plus élaborées, mais ça restera personnelle, je voulais juste mentionner cette idée d’approche, sans même savoir si elle peut aboutir.

Cette question se résume à celle de la sémantique. Si celle du Prolog classique, c’est la logique du premier ordre, alors elle ne correspond pas au domaine d’ici, la formulation et la vérification des propriétés de logiciels, à moins qu’elle ne soit plus souvent suffisante que je ne le crois.

Pourtant, son principe de base, d’un point de vue abstrait, peut avoir un espace d’applications plus large et être facilement compris, au moins intuitivement et en surface.

Ses termes sont ce qu’on peut faire de plus élémentaire — constantes, variables et une composition récursive à travers des tuples. Pour les constantes, elle ne sont pas toujours nécessaires, les variables pouvant permettre plus d’abstraction, mais pas dans le Prolog classique où la tête des clauses commence toujours par une constante (on peut mimer des foncteurs non‑constants, mais ça devient vite lourd à l’écriture). Les termes en Prolog, ont des constituants aussi élémentaires que les termes en lambda calcul. Le lambda calcul est connu pour pouvoir se passer de constantes.

La mise en correspondance de deux termes aussi, est d’un intérêt tellement général qu’on peut considérer ce principe comme élémentaire. Je dit la mise en correspondance de deux termes, parce qu’il semble que les mots “ unified ” et “ matched ” ont des significations trop précises pour inclure l’idée de trouver une correspondance entre deux termes avec des relations cycliques, sans que je ne sache quel mot conviendrait mieux en général ou quel mot conviendrait mieux dans le cas particulier ou les termes cycliques sont des possibilités. Cette mise en correspondance de termes, c’est ce qui fait que le principe de base de Prolog est plus intuitivement expressif que la lambda calcul et il est aussi plus facilement logique (il doit y avoir un lien entre les deux).

Je crois que la sémantique du lambda calcul ne donne pas lieu à débat, contrairement à celle de Prolog.

La logique du Prolog classique est fixée, mais son principe de base présente un intérêt au delà. Je crois qu’il faut oublier les commentaires catégoriques disant que les termes cycliques sont des erreurs qui ne devraient pas exister, en tenant implicitement pour universelle et seule possible, une sémantique qui n’est qu’une parmi d’autres possibles. Il ne faut pas pour autant ignorer la sémantique classique, qui reste une base essentielle.

Inutile de faire coller une sémantique à une autre, ce serait une impasse. Mais il peut être intéressant de savoir dans quelle mesure deux sémantiques deux sont liées, ou comment une est éventuellement incluse dans une autre ou si cette inclusion n’est qu’une apparence parce qu’elle présenterait des contradictions.

En résumé, si le Prolog classique a une logique en particulier, sont principe abstrait, peut, lui, être appliqué dans d’autres domaines, avec des termes désignant d’autres réalités et sujets à une logique autre, bien que présentant deux similitudes importantes à travers le principe essentiel de la mise en correspondance de termes et le caractère abstrait de ces termes. Ça nécessite quand‑même de poser explicitement à quelle réalité on associe ces termes.

Ce qui semble être deux sémantiques de référence, la première pour la logique du premier ordre (sémantique de Tarski), la seconde pour le Prolog classique (sémantique de Herbrand).

• Tarskian semantics, or no notation without denotation! (wiley.com) [PDF], Drew McDermott, 1978.
• Herbrand Semantics (stanford.edu), Michael Genesereth, Eric Kao.

Le premier document est juste à propos de l’idée de dénotation, mais le deuxième revient sur la première sémantique aussi.

Les premiers risques d’incohérences dut aux termes cycliques, seraient par rapport à ces deux sémantiques. Reste à savoir si elles sont toujours pertinentes. Mais selon ce qu’on fait, on utilise peut‑être pas nécessairement toujours la même sémantique. On peut imaginer en utiliser une pour représenter le comportement ou les termes d’un programme et une autre pour parler de ce comportement ou de ces termes, même s’il y a des représentations en commun. Seulement, si certaines représentations n’ont pas de sens pour une sémantique, il faut une traduction qui me semble ne pouvoir passer que par une abstraction et du coup, la sémantique ou la logique associée, ne permet pas de parler de tout ce que sont les termes initiaux.

J’aime bien le titre du premier document.

L’unification avec occurs check, est possible en un temps polynomial (au pire et le pire cas est improbable), ce qui est déjà un peu mieux que le temps exponentiel que j’ai souvent vu mentionné. Ce n’est pas un tour de passe‑passe impossible dans la fonction de recherche d’occurrences de variables, c’est un détail de mon unification qui permet une simplification. Je ne sais pas si c’est vraiment un temps exponentiel pour les mise en œuvres courantes ou si c’était plutôt mal rapporté.

Que la fonction remplit bien son rôle, sera un exemple de chose à tenter de démontrer.

En Prolog, les termes cycliques posent aussi des problèmes avec la négation par l’échec, mais cette notion de négation n’est pas une nécessité.

En parlant de sémantique, je me demande si quand on parle par exemple de logique du premier ordre, l’expression ne serait pas inappropriée. Il me semble que la qualification s’appliquerait mieux au domaine ou aux termes qu’à la logique, qui plutôt en hériterait.

La distinction peut avoir une importance si on se souvient que pour des termes mêmes termes, on peut avoir plusieurs logiques. Parler de prédicats, de premier ordre, etc, c’est plus du domaine de la sémantique, de la nature des termes, que de la logique. Seulement ensuite, est définie ou s’y applique, une logique. Cette logique, c’est celle d’un langage objet, au passage, un exemple de cas où il ne faut pas confondre avec le système de déduction. Mais il y a quand‑même pas tout à fait une indépendance entre les deux, parce que certains aspects du langage objet peuvent devoir être traduit pour le système de déduction. C’est le cas au moins des quantificateurs (il a déjà été dit, que la preuve d’un quantificateur universel, c’est une preuve tout‑court sous un context en particulier).

Après avoir essayé de se faire une image des logiques, il faut essayer de se faire une image des types de sémantique. Ça se ressent, que c’est essentiel pour continuer.

Je crois que pour dire qu’un terme T a une certaine propriété p, cette simple représentation est courante : T p.

Je vois souvent noté “ P true ” pour dire qu’il a été vérifié que la proposition P est vraie, j’ai souvent vu noté “ S prop ” pour dire qu’il a été vérifié que la phrase S est une proposition. Ça ressemble a une notation en sens inverse de celle en usage pour l’application de fonction (on pourrait voir true et prop comme des fonctions), mais cette notation est courante. C’est aussi en sens inverse de la notation en Prolog classique, où ce serait plutôt “ prop(S) ” et “ true(P) ”.