Les logiques : notes en vrac

Mais il devrait être orienté dans l’autre sens, du coup, ce ：- est une idée malvenue (je ne sais pas qui l’a eu), ou alors il aurait dut être -：. Je donnerai une autre idée de symbole juste après, mais sans l’utiliser ici.

C’est à dire que dans B ：- A, le A serait une preuve de B. En Prolog, la tête d’une règle, le B, est d’ailleurs souvent appelée un but, le mot goal qui est souvent utilisé dans les démonstrations.

Mais dans B ：- A, le A n’est une preuve de B, que quand le A (et donc le B aussi) a été instancié et mis en correspondance comme décrit précédemment, et que aucune mise en correspondance n’a échoué. Il ne suffit pas de l’écrire, il faut que le schéma de la preuve soit réalisable — selon le processus précédemment décrit — et selon les éventuelles autres règles que A désigne (récursivement).

Ce qui est écrit, n’est que le schéma de ce qui pourrait être, ce qui est, c’est l’application du schéma de correspondances qui est écrit, et une preuve, doit être.

Une autre lecture de A ==> B, peut être de se demander ce que signifie B. Il peut signifier des choses concrètes, mais d’un point de vue abstrait, on sait que étant donné A ==> B, une occurrence de B, peut signifier une occurrence de A, ce qui est une manière légèrement différente de redire que A est une possibilité dans B.

Cette manière légèrement différente de le lire, équivaut à dire que A donne une signification à B ou que A est une définition de B. Si on a une seule règle de la forme A ==> B, alors A est l’unique définition de B. Mais c’est à condition qu’on soit dans une démarche constructiviste, c’est à dire qu’on ne fait pas l’hypothèse qu’il puisse exister un B qu’on ne saurait pas créer ou dont on ne saurait pas démontrer l’existence réelle. Cette démarche est compatible avec celle de poser une chose par définition. Si on dit que B est défini comme A, on suppose qu’il n’existe pas de B pour lequel la définition serait inconnue.

Quand on lit A ==> B comme « B est défini comme A », on peut autant avoir A1 ==> B et A2 ==> B pour dire dire que A1 et A2 sont deux définitions possibles de B, la définition n’a pas besoin d’être unique.

A ==> B se pose comme B ：- A en notation Prolog. Si on le lit comme « A est une définition de B », on peut se demander ce que vient faire le tiret, comme les deux points verticaux tout‑seuls sont une convention courante pour introduire une définition. « B : A » se lirait bien comme B est défini comme A.

C’est à cette notation que j’ai d’abord pensé, utiliser « : » tout‑court au lieu de « ：-  » . J’y reviendrai pour moi‑même, je n’en fais ici que la suggestion et ne l’utiliserai pas ici où je resterai à « ：-  ». L’avantage que j’y vois, c’est que ça ne ressemble pas à un turnstile (⊢) à la direction opposée de ce qu’elle devrait être. B ：- A correspondrait à A ⊢ B (permutées !), ce qui fait de B ：- A une notation que je juge trompeuse, raison pour laquelle j’aurais préféré que les gens qui ont opté pour B ：- A optent plutôt pour B : A. Mais il n’a malheureusement pas été ainsi …

En marge, voir A ==> B comme implicitement une définition de B, est peut‑être une justification du bien‑fondé de la sémantique de Herbrand qui est non‑dénotationnelle. Je suis personnellement à priori méfiant envers une sémantiques qui ne dénote rien de concret, mais là, il y a bien une dénotation au sens propre, même si c’est du domaine vers le domaine lui‑même. Après, rien n’empêche d’ajouter à ça une autre dénotation en parallèle et de prévoir des moyens de s’assurer qu’elle est correcte.

Il y a deux autres avantages à lire « A ==> B » ou « B ：- A » comme « A est une (ou la) définition de B » ou « B est entre autre (ou est tout‑court) défini comme A  ». Le premier avantage est sémantique, le second avantage est pédagogique.

Le premier avantage, sémantique. Une lecture parfois faite de B ：- A est de dire que A est la condition de B, ce qui avait d’ailleurs aussi été suggéré ici, comme une possible lecture de A ==> B. Mais il est sémantiquement moins trompeur de parler de définition que de condition. Parler de condition, laisses croire que les choses sont ainsi, point à la ligne. Parler de définition, reconnait implicitement que c’est ainsi qu’on se représente les choses, ni moins, ni plus, et que les choses sont peut‑être différentes en réalité. La différence est probablement ténue quand le domaine des choses réelles dont parle une logique, est lui‑même un domaine abstrait ou formelle, mais ça fait une différence importante quand le domaine est probablement largement inconnu, ce qui est le cas quand on parle des choses de l’univers dans lequel on vit, qui n’est pas un univers de Herbrand. Si B est une particule, que A est un assemblage de particules élémentaires, dire que A est une condition de B, me semble trop laisser croire à la certitude qu’on connait tout de B (et même de A). Tandis que dire qu’on définit la particule B comme un assemblage A de particules élémentaires, laisses moins oublier que c’est une tentative de représentation qu’on se fait. C’est une illustration avec la physique, ça serait encore plus flagrant avec la biologie (ou autres).

Le second avantage, pédagogique. En lisant B ：- A comme « B est défini comme A », la lecture d’un des précédents messages expliquant longuement ce qu’il se passe pendant l’évaluation d’une règle, est plus facile à comprendre. Il est plus facile de comprendre que ça correspond à remplacer un mot, par sa définition, tout en remplaçant chaque mot lui même de la définition elle‑même, pas sa propre définition, récursivement. C’est évidemment difficilement praticable quand on lit un texte en langage naturel, mais ça a plus de pertinence quand on lit un texte en langage formel. Si malgré leur volonté d’y arriver, des gens n’ont pas put suivre le message sur le processus d’application des règles, je suggère de le relire avec cette image à l’esprit, qu’il s’agit de remplacer un mot par sa définition, et récursivement de même avec les mots apparaissant dans la définition. Normalement, ça devrait être plus compréhensible ainsi, modulo quand‑même la notion d’instantiations et de variables que je ne vois pas comment expliquer autrement que comme ça l’a été. Mais peut‑être que des gens n’auront pas de mal à imaginer un dictionnaire dont les mots auraient des parties variables. Le processus et la signification d’une démonstration, pourrait aussi être plus clairs avec cette image.

Comme B ：- A peut se lire A ⊢ B, ça signifie que A ⊢ B peut se lire comme « B est démontré par A », ce qui ne surprend pas, mais avec à l’esprit des remarques similaires à celle du précédent message, si on peut lire A ⊢ B comme « B est logiquement démontré par A », ça devrait aussi se lire comme « B est sémantiquement, (seulement) justifié, par A ».

En lisant un document, je constate une autre convention. Je ne l’aime pas, pour les raisons que je vais donner, mais je la rapporte quand‑même, parce que c’est toujours utile de savoir quand des mots sont ambiguës et de savoir quels différents sens ils peuvent alors avoir.

Il semble quand‑même exister un mot pour désigner à fois les constantes de fonctions et les constantes de relations, ce mot a déjà été utilisé ici, c’est « foncteur ». Mais parler de foncteur par opposition à variable, ça va contre le sens courant des mots. Dans le sens courant, on oppose variable et constant(e). Je préfère encore parler de relation tout‑court pour les constantes de relation et parler de constante tout‑court pour les constantes de fonction, et quand‑même parfois utiliser le mot « constante » tout‑court pour parler des constantes en général, que de parler de foncteur.

Le mot « atome » est parfois utilisé pour désigner des constantes en général. Mais pourquoi ne pas les appeler constantes, alors ? Parce que dans ce document, il est fait une distinction entre les nombres et les constantes. Je trouve cette distinction sans intérêt, jugeant qu’il est plus appropriée de dire que 123 est une constante comme les autres. Il faut quand‑même savoir que si parfois un terme comme (relation a b …) est appelé un atome, parfois ce n’est que la constante relation, qui est appelé un atome, et que une constante fonction serait aussi appelée un atome. Comme dit juste un peu avant, ce que je n’aime pas dans cette convention, c’est qu’elle est conçue pour distinguer les nombres des autres constantes, alors que je juge cette distinction sans intérêt, les nombres étant je crois, des constantes (si on les représente comme des polynômes, c’est autre chose, mais là il s’agit bien de traiter le token « 123 » comme à part des autres constantes).

Je n’aime pas du tout ces deux conventions, que je trouve encore plus problématiques que celles que j’avais remarqué dans d’autres documents, je ne les utiliserai pas ici, mais il faut savoir qu’elles existent. Souvent, il faut lire en essayant de deviner quel sens est donné à quel mot, ça peut changer d’un document à l’autre.

Le même document utilise une autre convention, est qui de parler de structure pour parler d’un terme comme (fonction a b c). Mais le mot « structure » a un sens très fort dans plusieurs autres domaines et de plus, ce sens qu’il a dans plusieurs autres domaines, est le même, c’est un sens unanime. Ce sens, c’est celui qui lui est donné dans la théorie des catégories. Je préférerais encore parler de terme structurel, ou plus simple, de schéma (ou pattern), plutôt que de structure. Un autre mot qui conviendrait bien, serait « constructeur . Le mot « constructeur » a déjà été introduit et il sera justifié plus tard. Au passage, le mot « foncteur » a lui aussi un sens dans ces domaines, raison de plus pour éviter de l’utiliser à légère pour signifier une constante accompagnée d’arguments. Dans le sens de la théorie des catégories, un foncteur permet de passer d’une structure à une autre. Et dans ce document, le terme foncteur est utilisé pour parler des constantes en générale, celles désignant des relations et celles désignant des fonctions. C’est peut‑être parfois justifié, mais je préfère éviter ces deux mots au sens trop fort, pour parler de termes en Prolog ou dans la sémantique de Herbrand.

Des exemples simples mais essentiels à poser, pour aider à comprendre et donner un sens à ce qui a été expliqué sur la résolution des règles en Prolog ou Prolog‑like.

Juste d’abord un petit changement : à partir de maintenant, j’abandonne le symbole ：- et utilise le symbole : . Il n’est pas conventionnel, il pourra surprendre, mais il a été justifié. Les « -- » suivit de texte, sont des commentaires. Quand un terme ou une conjonction apparaît suivit d’un point d’interrogation, ça signifie une requête, c’est à dire le point de départ d’une résolution, tel que expliqué précédemment. Les lettres en majuscule sont des variables, les mots en minuscules, sont des constantes.

Un exemple simple pour commencer, pour s’assurer que le principe de l’unification, c’est à dire de la mise en correspondance a bien été compris. Mais pas d’inquiétude, ces exemples vont répéter les détails, pour aider à les percevoir.

(peu-importe a). -- Une relation simple avec une constante.

(peu-importe X) ? -- Une requête avec une variable.

Normalement, si tout à été compris, il se ra possible de deviner que la requête sera satisfaite et que la solution sera …

X = a

Une autre requête, en gardant la même règle :

(peu-importe b) ? -- Hou, t’es sûr ?

Cette requête là n’aboutit pas.

Moins simple, mais toujours simple et plus intéressant. On oublie la règle précédente, et on pose celle‑ci :

(eq A A). -- Définition de l’égalité.

Ce n’est pas parce que cette règle a une constante de relation nommée eq pour equal, qu’elle est une définition de l’égalité. Le constante identifiant la relation pourrait bien s’appeler comme on veut, la règle serait toujours une définition de l’égalité. Ce qui en fait une définition de l’égalité, c’est son schéma, et surtout qu’elle ne contient que deux occurrences de variables et que ce sont deux occurrences de la même variable. Le nom de la constante ou de la variable, pourrait être ce qu’on veut, tant que le schéma serait le même, ce serait la même définition, ou plus formellement, une définition équivalente.

Oops, pendant que j’ai le dos tourné, quelqu’un a écrit ça :

(eq c c) ?

Quelle est la solution de cette requête ? Une règle va être cherché, et il n’y en a qu’une et elle va correspondre. D’abord (eq A A) sera copiée avec de nouvelles variables comme expliqué précédemment. L’unique variable qui a deux occurrences, sera nommée A_1, par pure convention et elle n’aura pas de valeur. Puis eq va être mis en correspondance avec eq. Ça colle. Puis A_1 va être mise en correspondance avec c, comme elle n’a pas de valeur, A_1 va être associée à c et ça ne changera plus. Puis la deuxième occurrence de A_1 va aussi être mise en correspondance avec c, et ça colle, comme A_1 vient justement d’être associé à c.

La solution est simplement :

A_1 = c

On pourrait même oublier ce A_1 en fait, mais il fait parti du contexte qui est la solution de la requête.

Maintenant, on oublie ce contexte et on teste une autre requête :

(eq X b) ?

Idem, une copie de la règle est créé, la A_1 est mise en correspondance avec X, on a alors A_1 = X, qui n’ont pas de valeur, puis A_1 est mise en correspondance avec b, on a donc A_1 = b, mais on avait déjà aussi A_1 = X, la solution est donc :

A_1 = X = b

On pourrait toujours oublier A_1, mais on peut remarquer que X est à priori plus intéressant à garder, comme il apparaissait dans notre requête.

Cette fois, on oublie pas le contexte précédent, on le garde, on reste dedans, et on teste encore la même requête « (eq X b) ? ». Que va‑t‑il se passer ? A_1 existe déjà dans le contexte, donc la copie de la règle (eq A A) aura une variable d’un autre nom, disons A_2, par pure convention. Il se passera la même chose que précédemment, mais cette fois, X a une valeur. En effet, ne pas oublier qu’on a choisi de garder le contexte, cette‑fois. On aura d’abord A_2 = X, et comme on a déjà X = A_1 = b, on aura en fait A_2 = X = A_1 = b. Puis A_2 est mise en correspondance avec b, ce qui colle, comme A_2 = b, après mise en correspondance avec X.

La solution est donc :

A_1 = A_2 = X = b

J’ai dit « on a choisi de garder le contexte cette fois ». Ça ne signifie pas qu’en appliquant une règle, on peut choisir de garder ou pas le contexte précédent, c’est seulement possible parce que « (eq X b) ? » est une requête.

Mais ça signifie quoi, de garder ou pas le contexte ? Si on ne garde pas le contexte, ça signifie qu’on refait une requête à partir de zéro, aucune association entre variable et valeur. Si on garde le contexte, ça signifie que la seconde requête « (eq X b) ? » est faite dans le contexte résultant de la première requête « (eq X b) ? », c’est à dire avec comme contexte, les associations entre variable et valeur qu’elle a produite. Ça rappel quelque chose ? Un contexte inclus dans un autre contexte … Ça doit normalement rappeler que c’est la même chose que quand dans une règle, on invoque une autre règle.

En fait, faire la seconde requête dans le contexte de la première, équivaut à une conjonction, c’est comme si la requête avait été :

(eq X b) & (eq X b) ? -- Le symbol & signifie une conjonction.

Dans une conjonction, un élément à droite est dans le contexte généré par la vérification des éléments à gauche. C’est en fait presqu’à comprendre à rebours : c’est à parce que dans P1 & P2, il sera vérifié P2 dans un contexte qui vérifie P1, qu’on a une conjonction. C’est à dire que après P1 & P2, on a un contexte qui vérifie à la fois P1 et P2 … ou pas, et si pas, alors la règle n’a pas été vérifiée. Un contexte qui vérifie à la fois P1 et à la fois P2 et à la fois P3 …, c’est ça, la conjonction de P1 et P2 et P3 … Un prochain message reviendra sur une subtilité pratique.

Si on oublie le précédent contexte, et qu’on teste cette requête contenant une conjonction, on obtient la même solution que quand on fait la seconde requête séparément mais dans le contexte du résultat de la première requête, à savoir, le même :

A_1 = A_2 = X = b

On oubli encore le contexte, et disons que quelqu’un taquin a encore écrit une autre requête pendant que j’écrivais ailleurs :

(eq X Y) ?

Solution …

A_1 = X = Y = Any

Quoi ? Mais il est bogué ce truc ? X, c’est pas Y. Mais si, X et Y sont deux variables, elles n’ont pas le même nom, mais peuvent avoir la même valeur. A_1 est créé, mise en correspondance avec X, on a A_1 = X, puis la seconde A_1 est mise en correspondance avec Y. A_1 = X, et X n’a pas de valeur, et il se trouve que Y non‑plus, n’a pas de valeur, donc pas de problème pour avoir A_1 = Y, et on a donc finalement A_1 = X = Y, et comme ni Y ni X n’ont de valeur, on A_1 = X = Y = pas de valeur, noté Any ici, ce qui est une convention courante. À noter : Any n’est pas une variable, c’est une représentation de « pas de valeur ». Pour que cette convention soit cohérente, il faut évidemment interdire d’avoir une variable de ce nom là, pour ne pas se retrouver avec Any = 123 quelque part, et ailleurs, avec X = Any pour dire que X n’a pas de valeur. Pour la même raison, il ne faut pas qu’une constante puisse s’appeler Any, non‑plus. Cette longue remarque est plus importante qu’il ne semble, ce n’est pas qu’une remarque à propos d’une convention ou d’un système en particulier, c’est une remarque à propos d’un type d’incohérence, qui s’appel Pollack inconsistency.

Maintenant, on oublie encore le contexte, et on teste ceci :

(eq X 3) & (eq X Y) ?

Sans détailler cette‑fois, voici la solution qui doit permettre de s’assurer qu’on a bien compris :

A_1 = A_2 = X = Y = 3

C’est tout pour les exemples simples mais essentiels, pour que le message ne soit pas trop long, il est arrêté ici. Le prochain donnera d’autres exemples, mais ne répétera plus tous les détails qui auront été répétés dans celui‑ci et qui seront supposés implicitement compris.

En mettant les pieds dans le plat directement, sans transition ni introduction, l’exemple autant classique que fondamental en logique, celui des entiers représentés comme dans l’arithmétique de Peano.

Ils pourraient être représentés ainsi :

(nat z). -- z, c’est zéro.
(nat (s N)) : (nat N). -- s, c’est la fonction « successeur ».

Une remarque : il ne serait pas correcte d’écrire (nat (s (nat N))) à la place de la deuxième règle. Si l’intention d’écrire (nat (s (nat N))) serait de dire qu’un nat peut être le successeur d’un autre nat, le terme interne (nat N), ne signifierait pas un N vérifiant la première ou la deuxième règle, il signifierait une valeur ayant le schéma (nat N), ce qui n’est pas la même chose. Il faut faire attention à ne pas confondre les termes les plus externes, qui désignent des règles, et les termes les plus internes, qui ne peuvent jamais désigner des règles, même s’ils participent évidemment au succès ou à l’échec de l’unification avec la tête d’une règle. C’est pour cette raison que la constante au début des termes les plus englobants, a un statut à part et n’est pas comparable à la constante qui se trouve au début des termes internes. C’est la raison pour laquelle sont distinguées deux catégories de constantes. Elles peuvent être parfois homonymes si on le veut, mais si on craint d’induire en confusion ou de s’auto‑induire en confusion, c’est à éviter.

Revenons aux deux règles introduites :

(nat z).
(nat (s N)) : (nat N).

On peut tester ces règles avec une requête :

(nat N) ?

Elle présentera à la suite, ces solutions, qui seraient en nombre infini si on ne s’en lassait pas :

N = z
N = (s z)
N = (s (s z))
N = (s (s (s z)))
N = (s (s (s (s z))))
N = (s (s (s (s (s z)))))
N = (s (s (s (s (s (s z))))))
N = (s (s (s (s (s (s (s z)))))))
N = (s (s (s (s (s (s (s (s z))))))))
…

La première règle est la première essayée, d’où la première réponse. Ensuite, la seconde règle est essayée. Elle nécessite que N ait le forme de (s X), et que ce X, vérifie lui‑même une règle nat. Donc pour ce X, la première règle sera tentée à nouveau, dans le contexte de la deuxième règle, trouvant une nouvelle solution, (s z). Puis le seconde règle sera à nouveau essayée, mais en restant toujours dans le contexte de la première instance de la deuxième règle, ce qui aboutira à trouver la solution (s (s z)), à partir de là, la suite sera à l’identique et une liste infinie de solutions pourrait être produite.

Ces deux règles auraient put être formulées ainsi, en SML :

datatype nat = Z | S of nat

À comparer à :

(nat z).
(nat (s N)) : (nat N).

Le nom du type devient le nom de la relation, les noms des constructeurs, deviennent les noms des constantes des fonctions. En SML, l’argument de S n’est pas explicitement nommé, il est implicite. Ici, il est explicitement nommé N. C’est la seule différence importante finalement, le reste n’étant qu’une question de forme. On peut quand‑même noter que la forme du terme a été exprimé dans la tête de la règle et le type de son argument, dans une condition de la règle. Mais exprimer la forme dans le corps de la règle, aurait été possible :

(eq A A).
(nat z).
(nat M) : (eq M (s N)) & (nat N).

Ce n’est pas seulement possible dans ce cas en particulier, c’est possible en général. Note : la plupart des interpréteurs Prolog ont une notation spéciale au lieu de la règle (eq A A), généralement quelque chose comme X = …, mais cette différence n’a aucune importance logique, et utiliser une règle (eq A A), souligne que le principe de Prolog est assez expressif en lui‑même pour ne pas avoir besoin de cet ajout, qu’il peut permettre de formuler dans ses propres termes.

Si on avait écrit ce qui suit à la place, les choses seraient‑elles différentes ?

(nat (s N)) : (nat N).
(nat z).

Elles seraient différentes, oui et non. Elles seraient logiquement identiques, mais en pratique différentes.

Avec ces règles, si on tente la requête « (nat N) ? », rien ne se passe, la recherche de solution part dans une récursion infinie ou s’arrête avec une indication d’erreur si l’interpréteur pose des limites. La première règle est rencontrée d’abord, elle fait référence à une règle (nat X), avec laquelle la première règle est en correspondance, et ainsi de suite, cette règle boucle empêchant d’atteindre la seconde règle.

Mais c’est seulement parce que la manière standard de chercher une solution est de tenter les règles dans leur ordre d’apparition. On peut imaginer d’autres manières de faire, mais elles seraient non–standard et ce ne sera pas vraiment abordé ici, juste rapidement suggéré à la fin.

Ce qui est plus intéressant et parfaitement standard, c’est qu’une règle peut être vérifiée, sans recherche de solution. C’est le cas quand il n’y a pas de variables dans les termes de la requête.

Même sans changer l’ordre des deux règles plus haut, cette requête ne part pas dans une récursion infinie :

(nat (s (s z)) ?

Elle ne donne pas de solution au sens stricte, puisqu’il n’y a pas de variables auxquelles donner une valeur (la vérification en produit quand‑même), mais la requête s’arrête en disant d’une manière qui dépend des interpréteurs, qu’elle s’est soldé par un succès.

Il ne faut pas voir les systèmes à la Prolog que comme des calculatrices pour la recherche automatique de solutions à certains problèmes, mais autant, ou même plus, comme des systèmes qui peuvent vérifier qu’un terme ou une conjonction de termes, sont vérifiés par un ensemble de règles. C’est même à ça que ces systèmes sont les meilleurs. La recherche de solutions et la vérifications de solutions, sont deux choses différentes, bien qu’elles soient menées selon les deux mêmes principes de base que sont l’unification et l’insertion d’instances de règles. Il y a toutes une gamme entre les deux, une requête pouvant contenir plus ou moins de parties variables.

S’il doit y avoir recherche de solutions, l’ordre des règles peut avoir une importance, mais leur signification logique reste la même, quelque soit leur ordre d’apparition, et que quelque soit l’ordre des règles, on pourra le plus souvent « toujours » vérifier qu’un terme constant, est vérifié ou pas par les règles. S’il doit y avoir recherche de solution et que l’ordre des règles est important, il faut pour une relation donnée, d’abord poser ses règles non–récursives, puis ses règles récursives seulement à leur suite.

Attention quand‑même, même avec un simple vérification sans recherche de solutions, la récursion infinie peut toujours se produire.

Pour second exemple, une représentation des nombres plus conforme à celle à laquelle on est habitué, même si elle en est encore plutôt éloignée.

(digit 0).
(digit 1).
(digit 2). -- Arrêtons‑nous là, ce sera de la base 3.
(poly (p1 N)) : (digit N).
(poly (p2 M N)) : (poly M) & (digit N).

L’idée est d’avoir une représentation polynomiale des nombres, d’où le nom de la relation (ou du type, selon les points de vue), poly. Comme on ne peut plus se contenter d’une seule constante élémentaire, comme avec le z du nat précédent, une relation est aussi ajoutée pour définir ce qu’est un digit. Les p1 et p2, sont deux constructeurs, comme précédemment. Une définition de types correspondante en SML, pourrait être celle‑ci :

datatype digit = Zero | One | Two
datatype poly = P1 of digit | P2 of poly * digit

Notez les similitudes en remarquant aussi que à la définition de poly en SML, correspondent deux règles en notation à la Prolog.

On ne peut pas donner le même nom aux deux constructeurs en SML, mais avec une formulation à la Prolog, c’est possible :

(digit 0).
(digit 1).
(digit 2).
(poly (p N)) : (digit N).
(poly (p M N)) : (poly M) & (digit N).

Les deux constructeurs se distinguent par leur « signature » : l’un a un seul argument, l’autre en a deux.

Si ça a l’air correcte, on peut tester une recherche de termes correspondants à ces règles, avec cette requête :

(poly P) ?

Les solutions suivantes seront présentées :

P = (p 0)
P = (p 1)
P = (p 2)
P = (p (p 0) 0)
P = (p (p 0) 1)
P = (p (p 0) 2)
P = (p (p 1) 0)
P = (p (p 1) 1)
P = (p (p 1) 2)
P = (p (p 2) 0)
P = (p (p 2) 1)
…

Ça s’énumère bien comme les nombres qu’on à l’habitude d’écrire, même si la notation est différente.

On peut toujours, là aussi, vérifier un terme sans variables et donc sans recherche de solutions :

(poly (p (p (p (p 2 ) 2) 0) 1)) ?

La requête se termine sans échec, le terme est vérifié.

La même remarque que précédemment, sur l’ordre des règles, s’appliquerait, mais ce serait sans intérêt d’en refaire un exemple. Il y a un autre ordre, qui est important maintenant. Dans la dernière règle, on a un conjonction de deux termes. Que ce passe‑t‑il si on les permute ? Logiquement, ça ne peut que être la même chose, mais en pratique, on aura une mauvaise surprise, qui là encore, se constatera si on est dans une recherche d’exemples de solutions vérifiant les règles.

Si au lieu de :

(poly (p M N)) : (poly M) & (digit N).

La dernière règle est :

(poly (p M N)) : (digit N) & (poly M).

Et qu’on veuille lister des solutions :

(poly P) ?

P = (p 0)
P = (p 1)
P = (p 2)
P = (p (p 0) 0)
P = (p (p 1) 0)
P = (p (p 2) 0)
P = (p (p (p 0) 0) 0)
P = (p (p (p 1) 0) 0)
P = (p (p (p 2) 0) 0)
P = (p (p (p (p 0) 0) 0) 0)
P = (p (p (p (p 1) 0) 0) 0)
P = (p (p (p (p 2) 0) 0) 0)
P = (p (p (p (p (p 0) 0) 0) 0) 0)
P = (p (p (p (p (p 1) 0) 0) 0) 0)
…

C’est « pas beau » parce que ce n’est pas très représentatif. Si on espérait une énumération, cette fois c’est raté. Seule un digit semble varier et tous les autres sont toujours zéro.

Ce qu’il se passe, c’est que pour trouver une solution à (digit N) & (poly M), une solution est d’abord cherchée pour (digit N), et la première qui est trouvée, c’est « 0 ». Une solution ayant été trouvée pour ce terme, la recherche de solutions passe au terme suivant, et arrive à (poly M). Pour résoudre ce terme, la première règle correspondante, sera « (poly (p N)) : (digit N). », elle permettra de trouver trois solutions. Quand ces trois solutions auront été épuisées, la recherche de solutions passera à la seconde règle correspondante, qui est la dernière et qui est récursive. La recherche va une fois de plus résoudre (digit N) & (poly M), en commençant par (digit N), qui aura encore zéro comme première solution, puis repartira à nouveau dans le même cycle, en cherchant une solution à (poly M). Sans fin, la recherche de solution continuera une récursion à travers (poly M), allongeant le polynôme, mais ne faisant jamais varier la solution au premier terme, (digit N), parce que la recherche de solutions à (poly M), récursive, ne s’arrêtera jamais.

Si pour l’ordre des règles, il peut être utile de préférer poser ce qui est non‑récursif d’abord, pour l’ordre des termes d’une conjonction, c’est le contraire, il peut être utile de préférer poser ce qui est récursif d’abord, et ce qui a un nombre de résultats possibles limités, à la fin de la conjonction. De cette manière, les solutions pour ce qui est à droite de la conjonction, finissent par être épuisées après avoir toutes été trouvées, et la seule option restante et de faire varier ce qui est à gauche de la conjonction. Mais attention, si un des termes à droite dans la conjonction est impossible à résoudre et que ce qui est à gauche est récursif, il y aura récursion infinie, parce qu’il y aura tentative de faire varier ce qui est à gauche, en échouant toujours avec ce qui est à droite, sans jamais trouver de solution, puisqu’il y aura toujours échec de la vérification de tous les termes.

Ce qu’il faut retenir. Le principe de base de Prolog n’est pas une solution universelle à la résolution de problèmes, mais il est une solution expressive pour formuler des règles et vérifier si des termes correspondent ou pas à ces règles. Entre la requête sur un terme tout entier constant (qui s’appel un ground term) et la requête ne contenant que des variables, il peut y avoir toute une gamme. Même avec une vérification sur un terme tout entier constant, même sans recherche de solutions, la récursion infinie peut toujours se produire, mais ce sera moins probable.

Cette apparente limitation du principe de base de Prolog, est dut au fait qu’il n’y a pas de méthode de recherche universelle des solutions possibles à un ensemble de règles, et que la solution standard d’explorer les possibilités des règles dans leur ordre d’apparition puis les termes des règles dans leur ordre d’apparition aussi, cette solution, même si elle est un « langage » commun, n’est pas une méthode de recherche de solutions, universelle.

Mais cette manière de rechercher des solutions, n’est pas imposée par la logique sous-jacente, qui n’interdit pas de chercher des solutions en suivant d’autres stratégies de choix des règles et d’ordre de traitement des termes des conjonctions. Un exemple pourrait même être qu’un humain décide à chaque étape, d’opter pour telle ou telle règle, puis dans une règle de commencer par vérifier tel terme, puis de s’occuper de vérifier tel autre terme, etc.

L’ordre des termes n’a logiquement pas d’importance. Il faut se rappeler qu’une solution à une conjonction, c’est un contexte vérifiant tous les termes de la conjonction. Hors, un contexte est un ensemble d’associations entre les variables et leur valeur, et si les termes de la conjonction sont satisfaits par ce contexte ou pas, ne dépend pas de l’ordre des termes, seulement de leurs variables (les noms des variables créées par les instantiations, ne seront cependant pas les mêmes dans tous les cas, mais ce sera équivalent). Comme l’ordre des règles, l’ordre des termes n’a pas d’importance logique mais il a une importance pratique. Ceci dit, il ne faut pas appliquer cette remarque à toutes les logiques, certaines logiques distinguant l’ordre des termes dans les conjonctions.

Le prochain message, plus court, sera à propos de la récursivité dans les règles, mais plus pour donner une idée de pistes d’investigation que pour expliquer quelque chose.

Avant le message qui avait été annoncé, sur la récursion, un exemple en supplément des deux du message précédent. En parlant de message annoncé, celui concernant la sémantique n’est pas oublié, c’est juste que plusieurs messages sont venu s’intercaler entre temps.

Posons ces règles :

#1 (nat z). -- Les #n sont seulement pour numéroter les règles.
#2 (nat (s N)) : (nat N).
#3 (nat-lt N (s N)) : (nat N). -- lt, pour dire lower than.
#4 (nat-lt M (s N)) : (nat-lt M N).

On reconnait les deux premières, les deux les suivantes, sont nouvelles.

L’idée est de définir ce qu’est un nombre plus petit qu’une autre. D’abord on pense à dire que un nombre est plus petit que son successeur. Mais ça ne couvre pas tous les cas, parce que M peut être plus petit que N, mais N être trop grand pour être son successeur. L’astuce consiste à le formuler ainsi : A est plus petit que B si B est le successeur de A, ou si un B2 est le successeur d’un B1 et que A est plus petit que ce B1 et récursivement sur tous les Bn. Récursivement, parce qu’on peut remarquer que la règle #4 peut s’appliquer récursivement avec tous les successeurs de N mais toujours avec le même M.

Avant de tester cet ensemble de règles, même si elles on été expliquées, on va les étudier un peu sur quelques aspects, mais seulement les règles #3 et #4, les #1 et #2 ayant été vue.

On peut remarquer que la règle #3 pourrait avoir du sens même sans sa condition (nat N). Seulement, elle permettrait alors de vérifier quelque chose comme (nat-lt abc (s abc)), ce qui n’est pas ce qui est attendu. Pour cette raison, la condition ou la précision sur la définition, (nat N), est ajoutée. (nat N) ne reconnait pas comme participant à la relation, tout N qui ne vérifierait pas les règles #1 ou #2.

La règle #3, toujours, a deux termes. Pourtant, seulement (nat N) est vérifié. Il ne serait pas insensé de l’écrire ainsi à la place :

(nat-lt N (s N)) : (nat N) & (nat (s N)).

Ce ne serait pas faux, mais ce serait redondant, et comme chaque terme dans une condition est un problème potentiel pour la stratégie classique de recherche de solutions, il peut être une bonne habitude d’éviter les termes inutiles. On doit quand‑même s’assurer qu’il est bien inutile, ce second terme de la conjonction. On remarque d’abord qu’il correspond au schéma de la tête de la règle #2, qui précise que le N de (s N) doit être conforme à (nat N). Hors, cette condition apparaît comme premier terme dans la règles #3. Le second terme est donc redondant.

Au cas où ça surprendrait : oui, les deux N des deux règles ne sont pas la même variable, mais quand la règle est appliquée, elle finissent par désigner la même chose, après unification, d’où la simplification d’en parler comme si les deux N étaient la même variable.

Après cette parenthèse, on pourrait faire des remarques similaires pour la règles #4, mais le raisonnement est différent, alors il est abordé. On pourrait écrire la règle #4 ainsi :

(nat-lt M (s N)) : (nat M) & (nat N) & (nat-lt M N).

On pourrait se dire deux choses. D’abord remarquer que si le troisième terme est vérifié par la règle #3, les deux premiers termes sont redondants. En effet, on a vu que la règle #3 pose déjà une condition suffisante pour vérifier que ses deux termes sont bien conformes à nat. Mais on pourrait aussi se dire que c’est supposer trop vite qu’on va passer par cette règle, et que la règle #4 elle‑même, peut correspondre à son propre troisième terme. Mais si on ne finissait jamais par passer par le règle #3, ce serait alors une récursion infinie. On peut donc oublier les deux premiers termes, en fondant ce choix sur l’existence de la règle #3, par laquelle il sera de toutes manières nécessaire de passer, sans quoi c’est la récursion infinie et qu’on ne sait pas comment choisir entre n’importe quoi et n’importe quoi.

Après les avoir inspecté et mis leurs formulations en question, revenons à ces règles pour les revoir avant de les tester :

#1 (nat z).
#2 (nat (s N)) : (nat N).
#3 (nat-lt N (s N)) : (nat N).
#4 (nat-lt M (s N)) : (nat-lt M N).

On les teste :

(nat-lt M N) ?

M = z
N = (s z)

M = (s z)
N = (s (s z))

M = (s (s z))
N = (s (s (s z)))

M = (s (s (s z)))
N = (s (s (s (s z))))

M = (s (s (s (s z))))
N = (s (s (s (s (s z)))))

M = (s (s (s (s (s z)))))
N = (s (s (s (s (s (s z))))))

…

C’est un peu décevant, c’est souvent le cas avec la stratégie standard de recherche de solutions vérifiant des règles. Ce qui est décevant ici, c’est que les seules solutions trouvées par cette méthode, sont un nat et son successeur, on ne voit pas apparaître de M = z et N = (s (s (s z))) par exemple.

Pas grave, si on sait que ça doit pouvoir être vérifié, on peut le tester :

(nat-lt z (s (s (s z)))) ?

La vérification se termine sans échec, la relation est bien vérifiée par les règles.

On peut tester la permutation des deux termes de la relation :

(nat-lt (s (s (s z))) z) ?

C’est un échec … c’est rassurant.

On pourrait le tester avec des termes variables …

(nat-lt (s N) N) ?

… mais récursion infinie, ni échec, ni succès, rien.

Mais pourquoi cette récursion infinie ? Ben parce que la méthode de résolution ne cherche pas un démenti comme nous, elle cherche une solution ! Mais elle n’y arrive jamais, on se doutait qu’il est impossible qu’une solution existe, on voulait même s’en assurer. Malheureusement, comme il y a deux opportunités de récursion, et que la méthode s’entête à trouver une solution, elle plonge dedans et n’en sortirait jamais. Reste qu’on a put vérifier l’échec de cette relation avec un terme tout entier constant. Mais est‑ce assez qu’on ait put le vérifier (cet échec) avec un seul exemple ? C’est que nous verrons dans un prochain message, qui abordera la sémantique.

On pourrait aussi vouloir définir une relation lower than pour les nombres poly du précédent message, mais ça ne sera pas fait ici. Il y a tellement de choses qui pourraient être essayées, si elles ne le sont pas ici, ça veut dire qu’il faut les essayer soi‑même.

Si la règle #3 est écrite sans la condition équivalente à un type, c’est à dire juste :

(nat-lt N (s N)).

 … alors une chose intéressante peut être remarqué avec la requête citée :

(nat-lt (s N) N) ?

N = (s (s (s N_1)))
N = (s (s (s (s N_1))))
N = (s (s (s (s (s N_1)))))
N = (s (s (s (s (s (s N_1))))))
N = (s (s (s (s (s (s (s N_1)))))))
…

La condition équivalente à une exigence de type, n’est pas qu’une sécurité commode, elle est formellement nécessaire pour le sens de la relation. Si ce type (exprimé comme une relation) n’est pas vérifié, la relation n’a pas le sens entendu. Wink … (hihi).