Hello!

Inspiré(e) de prendre part à la discussion ? Ou de poser une question ou demander de l’aide ?

Alors bienvenues dans les grands sujets des forums de La Bulle : m’inscrire.

Cette partie du forum n’est pas compatible avec les bloqueurs publicitaires

Félicitations à vous, de préférer les accès payants plutôt que la gratuité par la publicité, c’est honnorable et cohérent de votre part. Malheureusement, l’accès payant par micropaiement (qui serait d’environ 1 cent pour 20 pages consultées) n’est pour l’instant pas encore mis en place, et l’accès gratuit sans publicité, est réservé aux membres actif(ve)s du forum. En attendant, si vous souhaitez poursuivre votre visite chez nous, vous pouvez ajouter le site à votre liste blanche, ou encore mieux, désactiver le bloqueur partout. Pour ajouter le site à votre liste blanche, pour Firefox (similaire pour les autres navigateurs), rendez‑vous en bas à gauche de la fenêtre de votre navigateur, et cliquez sur le menu comme dans l’exemple de l’image ci‑dessous, puis rechargez la page, en appuyant sur F5.

Les logiques : notes en vrac
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 19342
Mar 24 Nov 2020 23:13
Message Re: Les logiques : notes en vrac
Suite du précédent message, avec une réponse à la seconde question du paragraphe cité.

Ce qui est dit dans ce message est susceptible de devoir être complété et est sous réserve.

Hibou a écrit : 
[…] Et si le terme posé en hypothèse, B, est unifiable avec la tête d’une règle mais contredit la règle ? On sait en effet, que l’unification d’un terme avec la tête d’une règle, ne garantit pas que la règle sera vérifiée, à moins que le corps de la règle ne soit vide. Et si l’hypothèse est une conjonction au lieu d’un unique terme ? […]

Jusqu’ici, unifier un terme A et un terme B, était la même chose qu’unifier le terme B et le terme A. Sans le dire, une distinction est apparue. L’unification n’est plus toujours symétrique, depuis qu’a été introduite la notion de couverture des cas.

Quand à partir de l’hypothèse ⟦(nat N)⟧ est créé le cas (nat (s N_2)) avec N lié à (s N_2), la règle été supposée vérifiée. Mais pourquoi ? À cette question il sera répondu un peu plus loin. Dans le précédent exemple, le terme en hypothèse a la même forme que l’unique terme du corps de la règle représentant un cas. Ça peut être perturbant et c’est un cas particulier, ce qui peut être dangereux, alors pour la suite, un autre exemple va être choisi. On va reprendre avec l’exemple de la relation poly, qui était :

§d0 (digit 0).
§d1 (digit 1).
§d2 (digit 2).
§poly-b (poly (p N)) : (digit N).
§poly-s (poly (p M N)) : (poly M) & (digit N).

Disons que maintenant, on va envisager les cas possibles de l’hypothèse ⟦(poly P)⟧ ; il y en a deux. On va s’intéresser au premier, celui de la règle §poly-b. Le P de l’hypothèse va être lié à (p N) et l’hypothèse ⟦(digit N)⟧ sera produite.

La liaison de P à (p N) vérifie‑t‑elle la règle §poly-b ? La réponse pourrait être que oui, puisqu’on a l’hypothèse ⟦(poly P)⟧, mais poly peut être vérifiée par l’autre règle, pas nécessairement celle‑ci et on sait qu’il ne suffit pas d’unifier un terme avec la tête d’une règle pour que la règle soit vérifiée. Pourtant, si on veut représenter ce cas, il faut que l’hypothèse ⟦(poly P)⟧ puisse le représenter.

La question devrait alors être reformulée autrement : l’hypothèse ⟦(poly P)⟧ est‑elle en accord avec la liaison de P à (p N) et l’hypothèse produite, ⟦(digit N)⟧ ? La règle dit que pour vérifier (poly (p N)), il faut vérifier (digit N), et (digit N) est posé en hypothèse. Ors, P est lié à (p N), donc l’hypothèse ⟦(poly P)⟧ correspond à (poly (p N)), même si ce terme n’est pas une hypothèse (pour une règle représentant un cas, le corps de le règle est posé en hypothèse, pas la tête de la règle). L’hypothèse est bien unifiée avec la tête de la règle et l’hypothèse produite vérifie la règle.

Oui, mais si on lie par exemple P à (p (abc def)), l’hypothèse pourrait toujours être unifiée avec la tête de la règle, mais la règle ne serait plus vérifiée, n’est‑ce pas ? Alors ça ne marche pas toujours, ça se voit. Oui, c’est justement pour cette raison qu’on ne liera pas P à n’importe quoi.

On sait qu’un terme peut être vérifié par une hypothèse correspondante. Un cas particulier n’a pas été souligné, c’est celui où au lieu de certains termes seulement, tous les termes du corps d’une règle, sont vérifiés par une hypothèse. Depuis que les hypothèses ont été introduites, le langage a implicitement une inférence de la forme ⟦A⟧ ==> B, où A reprend les termes du corps d’une règle en les posant tous en hypothèse, et B, est la tête de la règle correspondante. Note : pour simplifier, les hypothèses prises en exemple ici sont toujours des termes seuls, mais elles peuvent être des conjonctions de termes. Si une règle est réalisable, c’est que son corps est réalisable. Le corps de la règle, quand il est posé en hypothèse, représente une solution générale de la règle (à ne pas interpréter trop hâtivement non‑plus, c’est une représentation, pas une méthode de résolution). On ne peut cependant pas poser la tête de la règle en hypothèse pour la seule raison d’avoir le corps de la règle en hypothèse, parce que la tête de la règle, peut correspondre à d’autres règles aussi. Par exemple si on a B : A1 et B : A2, même si avec l’hypothèse ⟦A1⟧ on peut vérifier un B, on ne peut pas poser B en hypothèse, parce qu’il existe une autre règle pour B. Le terme B vérifié par ⟦A1⟧, aurait ses variables liées comme dans le terme A1 de l’hypothèse, c’est à dire typiquement liées à des généralités. Mais même si le terme B porte sur des variables représentant toutes des généralités, on ne peut pas pour autant le prendre pour une hypothèse.

Donc avec ⟦A1⟧, on peut vérifier un terme B tel qu’il apparaît comme tête de la règle B : A1. Mais c’est cohérent seulement si les variables de ce B, sont liées en vertu de ⟦A1⟧. Si les variables de ce B ne sont pas modifiée, on a la certitude que la règle est vérifiée. On peut unifier un terme avec ce B, si on ne modifie pas la moindre de ses variables, même indirectement.

On reprend la question d’avant le précédent paragraphe. On a voulu poser un cas de ⟦(poly P)⟧. Ce cas est celui de la règle (poly (p N)) : (digit N), nommée §poly-b. Après avoir posé ⟦(digit N)⟧ en hypothèse, qui est le corps de la règle §poly-b, on a put vérifier un terme (poly (p N)), qui est la tête de la règle §poly-b. Quand on a unifié le terme de l’hypothèse ⟦(poly P)⟧, avec (poly (p N)), on a lié la variable P de l’hypothèse à (p N). Aucune variable du terme (poly (p N)), n’a été modifiée. Si on liait P à (p (abc def)) et qu’on unifiait ensuite (poly P) à (poly (p N)), il faudrait lier N à (abc def). On modifierait la variable N du terme (poly (p N)). C’est justement cette liaison qui ne doit pas être permise, parce que ce N doit rester inchangé, pour que (poly (p N)) soit tenu pour vérifié par ⟦(digit N)⟧.

Dit d’une manière plus concise et plus formelle, si on a une hypothèse ⟦H⟧, pouvant correspondre à plusieurs règles et qu’on veuille couvrir chacun de ces cas, pour chaque cas représenté par une règle A : B, le corps B est posé en hypothèse, se faisant, les variables de A sont liées d’après B, puis le terme H est unifié avec le terme A, avec A constant, c’est à dire que aucune de ses variables ne peut être changée. L’hypothèse ⟦B⟧ est un cas du ⟦H⟧ d’origine, et ce cas, en plus d’être représenté ⟦B⟧, est aussi représenté par l’hypothèse ⟦H⟧ dérivée, où H est lié après unification avec A. Ce n’est pas la même chose que poser A en hypothèse, même si ça semble l’être ; un prochain message expliquera pourquoi. Le nouveau ⟦H⟧ remplace le précédent, dans la branche représentant le cas.

La dernière phrase du précédent paragraphe, corrige une erreur que j’ai dite précédemment en parlant de conserver l’hypothèse d’origine dans la branche représentant le cas. C’était intuitivement assez correcte, mais formellement inexacte. C’est une hypothèse lui correspondant qui lui est substitué. Conserver l’hypothèse d’origine ne serait même pas possible, comme toutes les références à cette hypothèse seraient avec les variables apparaissant dans cette hypothèse, et ces variables seraient liés comme décrit plus haut, dans toute la branche représentant le cas.

Ce n’est pas encore tout à fait tout. On entre dans une branche pour vérifier quelque chose dans ce cas, et on doit le vérifier pour plusieurs cas. Si la vérification échoue pour cette branche, elle échoue tout‑court et il n’est pas tenté de vérifier les autres cas, puisque la généralité ne serait pas vérifiée. Si la branche est vérifiée, les autres branches le sont de la même manière. À ce moment là, l’hypothèse d’origine est reprise pour entrer dans une nouvelle branche, en lui substituant à nouveau une hypothèse correspondante, pour cette branche. L’hypothèse d’origine peut être oubliée ou pas, c’est un détail technique, ça dépend de si les cas sont tous produits avant de les vérifier ou pas. L’important est que pour chaque branche, ce n’est pas l’hypothèse d’origine qui est visible, mais celle qui lui est substituée, une par branche.

Reste encore une question en suspend. Comment est déterminée la liste des cas devant être couvert. Pour savoir si une règle est applicable à un terme, on unifie le terme avec la tête de la règle et ensuite on vérifie le corps de la règle. Avec les branches représentant les cas, selon la méthode décrite dans ce message, c’est différent. Le corps de le règle est posé en hypothèse, puis l’hypothèse est unifiée avec la tête de la règle maintenue constante (la tête de la règle). Si par exemple une hypothèse est ⟦(nat (s (s N)))⟧, quels sont les cas devant être couverts pour s’assurer de faire une vérification en général, pour la généralité que représente cette hypothèse ?

En oubliant ce qui a été dit dans ce message et en revenant à l’unification ordinaire, (nat (s (s N))) serait unifiable avec (nat (s N_2)) ou N_2 serait lié à (s N), mais alors on modifierait la variable de la tête de la règle. Il faudrait ensuite s’assurer que N_2 vérifie (nat N_2). Ce terme est vérifiable, mais l’unification qui l’a produite, n’est pas permise dans la méthode de ce message, pour garantir que la règle est respectée. C’est une question en suspend. La méthode décrite dans ce message semble correcte dans les limites de sont applicabilité, mais elle ne s’applique à pas tout. Exactement, elle n’est applicable que quand la forme du terme posé en hypothèse est autant ou plus générale que la forme des têtes de règle représentant les cas. C’est déjà un pas quand‑même. La solution pour la compléter devrait normalement être une réponse à la question de savoir comment à l’appliquer à une hypothèse de plusieurs termes en conjonction et à la question de justifier l’éventuelle exclusion de certains cas.


Pour rappel, la mise en œuvre de plusieurs choses décrites ces derniers jours, n’a toujours pas été réalisée, des choses étant en court de réécriture avant de pouvoir les réaliser, tout en devant concevoir des solutions aux questions qui se posent. Les message de ces derniers jours, sont seulement des investigations, ils ne sont pas confirmés par des formulations réels et fonctionnels.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 19342
Mer 25 Nov 2020 12:20
Message Re: Les logiques : notes en vrac
Le problème à résoudre peut être reformulé d’une manière plus générale que dans le précédent message. Cette formulation plus générale se comprend facilement, mais ne laisse pas voir de solution immédiate.

Avant, la description d’une piste à ne pas prendre. Elle ne ferait que poser un nouveau problème, intéressant, mais sans intérêt pour le moment et dont la solution semblerait même encore plus lointaine.

Quand en unifiant une hypothèse avec la tête d’une règle, et que l’unification lierait une variable de la tête de la règle (seulement, ce n’est pas à propos des autres cas), il serait possible de considérer que le terme de l’hypothèse restreint la règle. Une restriction, ça peut faire penser à un terme supplémentaire ajouté au corps de la règle. Une idée semblerait alors de faire comme dans le précédent message, de poser le corps de la règle en hypothèse, puis d’unifier l’hypothèse initial à la tête de cette règle, mais en liant les variables de l’hypothèse aux termes de la tête de la règle au lieu de dans l’autre sens, et seulement ensuite, en ajoutant un terme à l’hypothèse représentant le cas, pour ajouter la contrainte de cette autre manière. Un exemple sera plus clair. Précédemment, cet exemple de cas problématique avait été pris : l’hypothèse ⟦(nat (s (s N)))⟧ pour laquelle on souhaiterais la branche de cas correspondant à la règle (nat (s N)) : (nat N). Il a été dit que l’hypothèse ne peut pas être unifiée avec la tête de la règle, parce qu’il faudrait lier le N de l’instance de la règle, N_2, avec le terme interne (s N) de l’hypothèse. Mais il serait possible de ne pas modifier les termes existant de la règle par cette liaison et de plutôt ajouter un terme à l’hypothèse représentant le cas. Le résultat serait alors l’hypothèse ⟦(nat N_2)⟧ & ⟦(eq N_2 (s N))⟧, pour représenter ce cas de l’hypothèse d’origine. Ça ramènerait à résoudre le problème de savoir si étant donné un terme ajouté au corps d’une règle, l’ajout est neutre, restreint seulement la règle mais en la laissant satisfiable ou la rend insatisfiable. La réponse serait nécessaire pour savoir si c’est une branche à effectivement couvrir. Si la réponse est que ça rend la conjonction insatisfiable, alors ce n’est pas une branche à couvrir. La question pourrait éventuellement avoir une utilité, mais elle n’en a aucune maintenant et surtout, c’est trop pour seulement ensuite pouvoir espérer résoudre la question initiale. De plus, le seule terme ajouté porterait toujours sur la relation eq, ce qui au feeling me semble être un mauvais signe, mais je ne vais pas essayer de plus décrire cette impression.

L’autre piste, passe par une reformulation. Elle n’apporte pas plus de solution, mais au moins, ne s’égare pas, contrairement à la mauvaise idée du précédent paragraphe.

Dans le message précédent, la solution n’est pas toujours applicable, mais elle est parfois applicable quand‑même. En fait, elle correspond à un cas particulier mais peut‑être pas sans intérêt en pratique, celui où l’hypothèse représente un ensemble de règles, plutôt qu’un terme ou une conjonction quelconque. Les justifications de cette solution ont beaucoup insisté sur la validité du corps de la règle posée en hypothèse représentant un cas d’une hypothèse d’origine. Cette validité repose sur la supposition que la règle dont est tirée un cas, est‑elle même satisfiable. C’est pour préserver son caractère satisfiable, que les variables de la tête de la règle ne doivent pas être liées autrement qu’elles ne le sont par le corps de la règle posé en hypothèse.

La satisifiabilité est à la base de la reformulation mentionné au début du message, mais cette satisfiabilité doit être contextualisée. C’est aussi une réponse théorique (car sans solution pour le moment) à la génération de la liste de cas à couvrir.

La reformulation. Si une hypothèse est unifiable avec la tête d’une règle et que le corps de la règle tel qu’il est après l’unification de la tête, est satisfiable, alors le corps de la règle représente un cas à couvrir. Chaque règle doit être ainsi testée pour l’hypothèse d’origine dont on veut couvrir les cas. C’est aussi simple que ça, en théorie au moins. En pratique, ça pose le problème de pouvoir vérifier la satisfiabilité de n’importe quel corps de règle, dans la foulée de la génération de la liste des cas à couvrir.

Dans le message précédent et avant, les hypothèses désignaient toujours des règles telles‑quelles : l’hypothèse contenant toujours un seul terme dont la forme est autant ou plus générale que la forme des têtes de règle pouvant lui correspondre. Il était alors supposé qu’il suffit de sélectionner les règles dont la tête correspond, étant supposé que toutes les règles du système de règles, sont satisfiables. La condition de correspondance avec la tête, élimine les cas à ne pas couvrir, et la garantie que les règles ont toutes été vérifiées satisfiables, garantie que les cas sélectionnés comme à couvrir, sont bien des cas valides. Aucun cas valide n’est omis (préservation de la généralité), et aucun cas sélectionné n’est invalide (pas de risque de faux échecs).

Mais ça ne fonctionne plus avec une hypothèse dont le terme peut être quelconque (et encore moins avec une conjonction comme hypothèse), par exemple être plus spécifique que la tête d’une règle. On pourrait se dire qu’il suffirait de se reposer sur la preuve à priori que l’hypothèse est satisfiable et utiliser la règle utilisée pour prouver l’hypothèse, pour produire un cas unique. Mais justement, le problème est que le cas n’est pas nécessairement unique. En fait, il y a une différence entre prouver la satisfiabilité d’une règle et prouver la satisfiabilité d’une hypothèse. Le processus est le même, mais les conclusions qu’on peut ou devrait pouvoir en faire, ne sont pas les mêmes.

On peut prouver que les deux règles de la relation nat sont satisifiables, en associant à chacune un exemple de satisfaction. Mais donner un exemple de satisfaction à une hypothèse, garanti seulement que l’hypothèse est satisfiable, sans dire exhaustivement par quelles règles elle peut l’être. Ors, ce serait nécessaire pour avoir la certitude de couvrir tous les cas, sans quoi la couverture des cas n’est pas cohérente, car ne préserve pas la généralité que représente l’hypothèse. Ors, on pourrait par exemple prouver que ⟦(nat N)⟧ est satisfiable, avec la première règle nat, sans pouvoir savoir qu’elle peut être satisfaite par la seconde règle aussi. La preuve de la satisfiabilité d’une hypothèse, ne dit rien sur l’ensemble des règles pouvant la satisfaire. C’est justement le problème qui se pose avec une hypothèse comme ⟦(nat (s (s N))⟧, qui ne désigne pas une ou des règles telles‑quelles.

Pour résoudre ce problème, il faudrait que la preuve d’une hypothèse se fasse en prouvant que telles règles peuvent satisfaire l’hypothèse et que toutes les autres règles ne le peuvent pas, ce qui devrait être prouvé aussi. Il faudrait apparemment résoudre le problème de la négation, qui justement nécessite que soit résolu le présent problème d’abord.

Ceci dit, la solution du précédent message reste valide quand‑même, même si elle ne couvre pas toutes les possibilités et ne permet la couverture des cas qu’avec les hypothèses ayant une forme adéquate. Mais comme elle ne couvre pas tous les cas, elle ne peut pas permettre de prouver tout ce qui devrait pouvoir l’être et par là, de ne pas prouver toutes les négations non‑plus, comme prouver une négation nécessite une couverture des cas.

Ou peut‑être la solution du précédent message est‑elle un cas de base qui permettrait d’avancer ensuite ?

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 19342
Mer 25 Nov 2020 20:10
Message Re: Les logiques : notes en vrac
« Normalement », la réponse ne peut être que négative. Si la réponse était autre, le problème des récursions infinies ne se poserait pas.

La solution de l’avant dernier message pourrait être conservée, avec juste une petite modification : l’unification avec la tête de la règle se ferait normalement, c’est à dire sans tenir la tête de règle pour constante. Si aucune variable de la règles n’est liée par cette unification, la suite se passe comme dans l’avant dernier message. S’il est détecté qu’elle modifie des variables apparaissant dans la règle, à priori, la couverture des cas est considérée comme non‑réalisable, à moins que la satisfiabilité de la règle ne soit vérifiée avec ses variables ainsi liées, mais seulement s’il est garanti que cette vérification se termine. Ce peut être le cas si le corps de la règle ne contient que des termes faisant référence à des règles dont le corps est vide.

La dernière condition permet d’éviter les échecs de couverture de cas dans des situations où ce serait difficilement acceptable, tant ce serait humainement incompréhensible. Un exemple serait le cas où au lieu d’écrire « (r c). », il serait écrit « (r V) : (eq V c). ». Les deux sont équivalentes, mais sans la petite touche de la fin du précédent paragraphe, la seconde règle ferait systématiquement échouer le génération de la couverture de cas. Comme dans l’avant dernier message, si la règle est vérifiée satisfiable, le corps de la règle est posé comme une hypothèse, avec toutes les variables représentant des généralités. La seule différence, serait dans cette vérification sous condition qu’il soit garanti qu’elle se termine et dans un temps raisonnable. Il est possible d’aller plus loin, mais ce ne sera pas décrit ici, pour rester un minimum accessible, alors que ça ne me semble déjà pas l’être autant que ça le devrait. C’est au minimum censé permettre d’avoir conscience et un minimum de compréhension, de ce que signifie concrètement, faire des vérifications portant sur des généralités, c’est à dire faire des démonstrations.

La couverture des cas pour une conjonction, pourrait se faire en générant une combinaison des couvertures possibles pour chaque terme. Mais fait de cette manière automatique, le nombre cas à couvrir pourrait vite augmenter. Par exemple avec seulement trois termes, si le premier a quatre cas possibles, le second cinq et le troisième, six, la couverture est déjà composée de 120 cas possibles, sous chacun desquels doit être vérifiée une requête ou le corps d’une règle, pour conclure à sa vérification avec des généralités. C’est encore sans compter l’éventuel découpage en cas de chacun de ces cas eux‑mêmes. La vérification automatique dans ces conditions, devrait se faire avec des limites, par exemple une limite du nombre de cas générés automatiquement, au delà de quoi, une intervention humaine serait requise pour faire les bons choix nécessaires à la démonstrations. Sans ça, une vérification automatique pourrait vite avoir à faire des couvertures avec des nombres de cas à plusieurs zéros, pour une seule vérification d’un terme avec une hypothèse non‑triviale.

Il faut espérer que la méthode de base décrite dans l’avant dernier message et affinée dans celui‑ci, soit suffisante pour des vérifications intéressantes et utiles, au moins pour que le système de base ne soit pas trop excessivement compliqué à démontrer.

Il apparaît que la couverture des cas, est une source de difficultés plus importante qu’attendue. Je m’y attendais, mais quand‑même pas à ce point.

La négation, qui est liée à cette question, pose encore plus de problèmes. Pas seulement parce que prouver la négation nécessite assez rapidement une couverture des cas, mais aussi parce que son cas de base, qui se constate pendant l’unification, n’est pas évident à propager. Un exemple pour que ce soit plus clair : soit une règle A : B & C & D. Disons que le terme C est vérifié et que la tentative d’unification échoue avec toutes les têtes de toutes règles. Dans ce cas, la contradiction est avérée. Mais jusqu’où remonter cette contradiction ? Si la cause de l’échec est une liaison de variable par la vérification du terme B, peut‑être qu’une autre solution pour B résoudra le problème et dans ce cas, il ne faut pas conclure à l’échec inconditionnel de cette instance de règle avec ses liaisons initiales. Si au contraire, la liaison à l’origine de l’échec systématique, est extérieur à cette instance de cette règle, alors on peut conclure à la négation de cette instance de cette règle, dans tous les cas. Ce n’est pas trivial à première vue (peut‑être une idée s’énonçant bien, mais sans certitude et qui ne sera pas réalisée avant un certain temps), et ça vient s’ajouter à la difficulté venant avec la couverture des cas, une couverture que nécessiterait souvent aussi la négation.

Pour la couverture des cas, même si une solution plus complète est conçue (peut‑être déjà une idée, mais sans certitude), ce ne sera pas rapporté ici, parce que ce serait probablement trop compliqué à exposer dans ce sujet au point de le rendre trop difficile à lire. Normalement, il n’y aura pas de retour sur cette question. Il y aura peut‑être un retour sur la question de la preuve de la négation, si est trouvée une solution assez intéressante et pas trop complexe, même si elle ne s’applique pas toujours (à la manière de la solution incomplète mais assez intéressante, proposée pour la génération des cas à couvrir). Un retour sur cette question, n’est pas exclus, mais pas garanti non‑plus.

Une petite note sur une question de vocabulaire. Je me souviens avoir assez souvent lu l’expression “ cases split ”, peut‑être surtout dans la littérature à propos de l’assistant de démonstration, Coq. Cette expression est compréhensible, mais je la trouve trompeuse. D’abord, il n’y a pas nécessairement plusieurs cas, il peut autant bien n’y en avoir qu’un seul. Ensuite, la raison pour laquelle cette notion a été introduite, était surtout pour résoudre le problème de l’opacité des hypothèses, elles‑mêmes initialement introduite pour représenter les généralités. La raison initiale était de les rendre plus transparentes quand ça peut être nécessaire, la notion de couverture des cas étant plus le moyen que l’intention. Pour ces deux raisons, je me demande si parler d’ouvrir une hypothèse, comme on ouvre une boite, plus proche de l’intention, ne serait pas plus évocateur et moins trompeur.

Cette fois, je crois qu’il sera vraiment pris congé de ce sujet pendant un temps, parce que la petite montagne de difficultés qui s’est élevé avec les deux dernières questions, suggère de prendre du recul et de n’y revenir qu’après avoir laissé décanter et à tête reposée.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 19342
Jeu 26 Nov 2020 22:31
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Cette fois, je crois qu’il sera vraiment pris congé de ce sujet pendant un temps, […]

Après ce message, ce sera vraiment‑vraiment.

C’est avec le langage naturel qu’on comprend le mieux les choses, mais seul un langage formel peut rendre les choses vérifiables selon un procédé tout aussi formellement établit.

Voici un exemple de compléments au langage qui a été défini jusqu’ici. C’est seulement une ébauche, une base, il n’a pas encore été mis en œuvre. Les exemples ci‑dessous ajoute au langage, la possibilité de prouver qu’une règle est satisfiable, de justifier une hypothèse, de lister ses cas et de faire des démonstrations d’après une hypothèse opaque ou d’après une hypothèse après son ouverture.

L’exemple est découpé en parties, chacune étant commentée.

Code : 

§nat-z      (nat z).
§h-nat-z ⟦(nat N)⟧ : §nat-z.
§nat-s (nat (s N)) : (nat N) =| §h-nat-z.
§h-nat ⟦(nat N)⟧ : §nat-z | §nat-s.
§nat-lt-b (nat-lt N (s N)) : (nat N) =| §h-nat..
§h-nat-lt-b ⟦nat-lt N1 N2⟧ : §nat-lt-b.
§nat-lt-s (nat-lt N1 (s N2)) : (nat-lt N1 N2) =| §h-nat-lt-b.
§h-nat-lt ⟦nat-lt N1 N2⟧ : §nat-lt-b | §nat-lt-s.
§d0 (digit 0).
§d1 (digit 1).
§d2 (digit 2).
§h-digit ⟦(digit D)⟧ : §d0 | §d1 | §d2.
§poly-b (poly (p D)) : (digit D) =| §h-digit.
§h-poly-b ⟦(poly P)⟧ : §poly-b.
§poly-p (poly (p P D)) : (poly P) & (digit D) =| §h-poly-b & §h-digit.
§h-poly ⟦(poly P)⟧ : §poly-b | §poly-p.
§int (int (i N1 N2)) : (nat N1) & (nat N2) =| §h-nat.
§h-int ⟦(int I)⟧ : §int.
§int-z (int-z (i N N)) : (nat N) =| §h-nat.
§h-int-z ⟦(int-z Z)⟧ : §int-z.

C’est la reprise des règles qui ont servi d’exemple (il manque juste la règle eq, qui pose une petite colle). Comme avant, les §n servent à donner des noms aux règles, mais ici, aussi aux hypothèse. Le symbole =| est le |= orienté dans l’autre sens. On peut lire A =| B comme B est une solution de A ou B satisfait A. C’est une notation pour la satisfiabilité dont il a été souvent question. La satisfiabilité pourrait se faire avec des termes constants, mais comme les hypothèses représentent des généralités qui sont comme des ensembles de constantes, elles sont utilisés à la place comme une preuve de satisfiabilité plus général. En gros, A : B =| §h peut se lire l’existence de §h prouve que A : B est satisfiable. La satisfiabilité des hypothèses aussi, doit être montrée. Mais le symbole =| n’est pas utilisé. La raison est que c’est plutôt le terme de l’hypothèse qui est satisfiable. Aussi, comme une hypothèse peut avoir plusieurs justifications et qu’une liste exhaustive de ses justifications peut correspondre à la liste de ces cas possible, il est considéré qu’on peut dire par abus de langage, que la liste des cas d’une hypothèse est un peu sa définition. Pour cette raison, la justification des hypothèse est noté avec le même symbole que les règles qui sont prises pour des définitions. Par exemple ⟦H⟧ : §r1 | §r2, signifie que l’hypothèse a deux cas possibles, qui sont les règles §r1 et §r2 et la liste de ces cas fait en même temps office de preuve que le terme de l’hypothèse est satisfiable ; deux en un.

Plus haut, on peut remarquer que les preuve de satisfiabilité des règles, se font en désignant des hypothèses, et que à l’inverse, les preuves de satisfiabilité des hypothèse qui est aussi la liste de leurs cas, se font en désignant des règles. Cette notation rend visible la relation réciproque entre les deux.

Certaines hypothèses peuvent être justifiées plusieurs fois, c’est normal, dans ce cas, elles sont complétés par de nouveaux cas et reçoivent un nouveau nom. Elles pourraient avoir le même nom dans tous les cas, mais donner un nom différent rend plus clair qu’elles sont complétées avec l’introduction de règles pouvant leur correspondre. Chaque ligne ne dépend que des précédentes, que ce soit pour les hypothèse ou les règles, c’est ce qui explique que la règle §poly-p n’est pas justifiée par elle‑même, même si elle pourrait l’être si elle était posée une seconde fois.

Code : 

VERIFY (int Z) : ⟦(int-z Z)⟧.
OPEN HYPS.
CASE §int-z OF ⟦(int-z Z)⟧ IS (int-z (i N N)) : (nat N).
YIELDS §1 Z = (i N N), §2 ⟦(nat N)⟧, ⟦(int-z Z)⟧.
§3 (int (i N N)) : (nat N) & (nat N) -| §int.
§4 (int (i N N)) -| §3 IN §2.
(int Z) -| §4 IN §1.
END CASE.
(int Z).
CLOSE HYPS.
QED.

C’est un exemple de preuve, la vérification qu’un Z qui vérifie int-z vérifie toujours int ; l’exemple sur lequel la vérification automatique avait séchée et qui a nécessité une réécriture pour être vérifié. Ce cas est celui qui avait fait conclure que l’opacité des hypothèse empêche certaines vérifications, ce qui a amené à introduire la notion d’ouverture de l’hypothèse et de cas représentant l’hypothèse. Les mots en majuscules sont censées être des mots clés. La ligne commençant par YIELDS, correspond à l’unification de la l’hypothèse avec la tête d’une règle correspondant à un cas. Ici, il n’y qu’un cas. Comme expliqué précédemment, la variable Z est lié, le corps de la règle est posée en hypothèse et une hypothèse dérivée remplace l’hypothèse d’origine. Le symbole -| est le symbole |- orienté dans l’autre sens. On peut lire A -| B comme A est justifié ou produit par B. Le B peut être l’instanciation d’une règle, la vérification d’une règle, la liste n’étant pas exhaustive. Le IN signifie dans le contexte de. Par exemple §3 IN §2 signifie la règle rapportée en §3 vérifiée dans un contexte où on a l’hypothèse rapportée en §2. Ces explications sont déjà un peu longues à lire, alors pas plus de détails ne sont donnés, mais ils peuvent se deviner en essayant de suivre.

La preuve plus haut n’avait pas put être faite avec la simple requête « ⟦(int-z Z)⟧ & (int Z) ? », parce que la vérification nécessite d’ouvrir l’hypothèse, qui autrement ne vérifie rien d’utile à la démonstration. La requête s’était achevé sans résultat. Mais cette variante, c’était achevé avec une solution : ⟦(nat N)⟧ & (int-z (i N N)) & (int (i N N)) ? », où on peut reconnaître dans la requête, l’hypothèse utilisée dans la démonstration plus haut.

Code : 

VERIFY (nat-lt N (s (s N))) : ⟦(nat N)⟧.
OPEN HYPS.
CASE §nat-z OF ⟦(nat N)⟧ IS (nat z).
YIELDS §1 N = z, §2 ⟦(nat N)⟧.
§3 N2 = (s N).
§4 (nat N2) : (nat N) -| §nat-s.
§5 (nat N2) -| §4 IN §2.
§6 (nat-lt N N2) : (nat N) -| §nat-lt-b.
§7 (nat-lt N N2) -| §6 IN §2.
§8 (nat-lt N (s N2)) : (nat-lt N N2) -| §nat-lt-s.
§9 (nat-lt N (s N2)) -| §8 IN §7.
(nat-lt N (s (s N))) -| §9 IN §3.
END CASE.
CASE §nat-s OF ⟦(nat N)⟧ IS (nat (s N_1)) : (nat N_1).
YIELDS §1 N = (s N_1), §2 ⟦(nat N)⟧.
§3 N2 = (s N).
§4 (nat N2) : (nat N) -| §nat-s.
§5 (nat N2) -| §4 IN §2.
§6 (nat-lt N N2) : (nat N) -| §nat-lt-b.
§7 (nat-lt N N2) -| §6 IN §2.
§8 (nat-lt N (s N2)) : (nat-lt N N2) -| §nat-lt-s.
§9 (nat-lt N (s N2)) -| §8 IN §7.
(nat-lt N (s (s N))) -| §9 IN §3.
END CASE.
(nat-lt N (s (s N))).
CLOSE HYPS.
(nat-lt N (s (s N))).
QED.

C’est un exemple avec deux branches. Il se trouve que les deux branches sont identiques, parce que le point de départ de chacun des cas ne change rien au raisonnement qui est le même dans les deux branches. En fait, ce raisonnement peut se faire sans ouvrir l’hypothèse, ce qui rend moins étonnant que les deux branches soient identiques.

Code : 

VERIFY (nat-lt N (s (s N))) : §1 ⟦(nat N)⟧.
§2 N2 = (s N).
§3 (nat N2) : (nat N) -| §nat-s.
§4 (nat N2) -| §3 IN §1.
§5 (nat-lt N N2) : (nat N) -| §nat-lt-b.
§6 (nat-lt N N2) -| §5 IN §1.
§7 (nat-lt N (s N2)) : (nat-lt N N2) -| §nat-lt-s.
§8 (nat-lt N (s N2)) -| §7 IN §6.
(nat-lt N (s (s N))) -| §8 IN §2.
QED.

La même chose, mais sans ouvrir l’hypothèse, en raisonnant avec l’hypothèse sous sa forme opaque ou abstraite, directement. Que l’hypothèse n’ait pas besoin d’être ouverte, explique que cette vérification avait put être faite avec une requête ordinaire : « ⟦(nat N)⟧ & (nat-lt N (s (s N))) ? », qui avait renvoyé une unique solution, correspondant en fait à la preuve plus haut.

Image
Hibou57

« La perversion de la cité commence par la fraude des mots » [Platon]
Profil Site Internet