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 : 22173
Dim 8 Nov 2020 19:51
Message Re: Les logiques : notes en vrac
— Édit — Ce message est sur une mauvaise piste, il est quand‑même conservé pour ne pas oublier une intuition tentante mais menant à une impasse.

Le principe de collecter les origines des termes liés aux variables, se formule bien, au moins, même si la formulation réelle avec tous les détails, est longue.

On peut le voir de deux manières équivalentes : la localisation des termes dont dépend le schéma d’une variable ou la localisation des termes que vérifie le schéma d’une variable. Ceci inclut les variables rendues équivalentes par liaisons, il est ainsi possible de savoir où dans les termes des règles, se trouvent les variables avec lesquelles une variable a été liée. Par « terme », il faut comprendre les termes inclus, pas les termes les plus englobants.

Cette localisation de ce qui fait la valeur d’une variable, ne distingue pas les instantiations, comme le principe a été introduit initialement comme une étape vers la possibilité de poser une variable en général, c’est à dire quelque soit sa valeur quand elle vérifie une règle.

La localisation a la forme d’un chemin, semblable à un chemin d’accès à un fichier et dont la racine serait un terme convenablement identifié. Chaque terme doit avoir sa propre identité d’une manière ou d’une autre, ce qui peut être l’indexe de la règle dans laquelle il se trouve accompagné de l’indexe représentant sa position dans cette règle. Plusieurs solutions sont possibles, ce n’est pas la seule, mais il faut au moins prévoir de pouvoir distinguer aussi les termes que sont les têtes de règle et les terme de la requête, de la même manière.

Un chemin est une liste d’indexes, avec un élément pour chaque niveau d’imbrication de tuple, la valeur de chaque indexe étant une position dans un tuple.

Par exemple, soit le terme (r (f a b c)), si le terme est identifié comme disons « règle 1, terme 2 », alors la localisation de c serait (1,2)/0/1/3, ou pour prendre un autre exemple encore, la localisation de (f a b c) serait (1,2)/0/1. Un ensemble de tels chemins accompagne chaque liaison entre une variable et un terme, dans le contexte.

Ça a l’air trivial, formulé en mots, mais ça implique beaucoup de choses en pratique, dans l’unification, l’instantiation et l’application des règles. Pourtant, malgré l’importance des réécritures que ça aura nécessité, il semble y avoir dans ce principe, quelque chose de naturel. Je ne saurais pas trop décrire mon impression en mots, mais disons au moins que c’était comme si c’était déjà implicitement présent, caché, et que ça n’attendait que d’être mis en évidence, tout en disant quelque chose. Pour ce bon pressentiment et comme ces données dérivées peuvent avoir un intérêt pour l’analyse, je crois que ce principe est à retenir, même s’il s’avère que ce qui l’a fait introduire en premier lieu, l’idée des variables spéciales précédemment décrites, n’est finalement pas réalisable (il est encore trop tôt pour le dire).

En marge, à cette occasion, il m’a semblé que les termes récursifs sont peut‑être plus problématiques qu’ils n’en ont l’air. Mais comme cette possibilité reste toujours exclue pour le moment, cette dissonance peut être oublié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 : 22173
Dim 8 Nov 2020 22:33
Message Re: Les logiques : notes en vrac
— Édit — Ce message est en partie sur une mauvaise piste, il est quand‑même conservé pour ne pas oublier une intuition tentante mais menant à une impasse.

Hibou a écrit : 
[…] Ceci inclut les variables rendues équivalentes par liaisons, […]

Un chemin est une liste d’indexes, avec un élément pour chaque niveau d’imbrication de tuple, la valeur de chaque indexe étant une position dans un tuple.

Par exemple, soit le terme (r (f a b c)), si le terme est identifié comme disons « règle 1, terme 2 », alors la localisation de c serait (1,2)/0/1/3, ou pour prendre un autre exemple encore, la localisation de (f a b c) serait (1,2)/0/1. Un ensemble de tels chemins accompagne chaque liaison entre une variable et un terme, dans le contexte.

[…]

Mais je crois qu’il ne faut pas qu’une variable puisse être associée à un chemin vers une de ses propres occurrences. Sans ça, une variable est toujours sa propre solution, ce qui n’est pas souhaitable.

En marge, peut‑être qu’un exemple aiderait à mieux percevoir l’idée de cet hypothétique type de variable (sans même savoir s’il existe ou pas). En reprenant l’exemple précédent de la relation nat-lt, où X serait un tel type de variable, la requête (nat-lt X (s X)) & (nat X), ne devrait avoir qu’une seule solution (une solution constituée de deux chemins) et la requête (nat-lt (s X) X) & (nat X) ne devrait avoir aucune solution, au lieu de partir dans une infinie et vaine recherche de solutions. Mais c’est encore vague et sans même de certitude que ce soit réalisable, même si je pressens que ça l’est.

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 : 22173
Lun 9 Nov 2020 04:56
Message Re: Les logiques : notes en vrac
Malheureusement, non, il n’est pas possible d’évaluer les règles avec un type de variable dont la valeur serait une valeur en générale, ce serait incohérent.

Un contre‑exemple est tellement évident que je m’en veux de ne pas y avoir pensé plus tôt. Imaginons ces deux règles et une requête :

(r a b).
(r b a).
(r X Y) ?

La valeur générale de X équivaudrait finalement à « a ou b », et de même pour Y, mais X ne peut pourtant pas être b quand Y est b et de même pour a.

L’idée de variable ayant une valeur en général n’est pas du tout une piste pour poser un terme en hypothèse.

Finalement, la solution est bien la toute première idée naïve et mauvaise, qui était d’ajouter l’hypothèse comme une règle au corps vide, mais avec une différence qui la rend moins naïve : cette règle n’aurait qu’une instance et elle se vérifierait par correspondance, mais sans unification.

Dans ce cas, poser (r X Y) en hypothèse, ne présente par le risque de permettre de conclure (r A B), à moins que par ailleurs X ne soit liée à A et Y liée à B.

Un terme posée en hypothèse serait donc une règle au corps vide et à instance unique et vérifiée par correspondance sans unification. L’hypothèse est une règle non‑instantiable. Cette approche sera testée prochainement. Au moins, elle s’énonce simplement et clairement, et semble immédiatement cohérente.

Reste la question du statut des variables apparaissant dans cette hypothèse. Ce qui est au moins sûr à ce point, c’est qu’elles ne sont pas liées à travers l’hypothèse. Par exemple s’il existe une règle (r c), faire l’hypothèse (r X), ne lie pas X à c, mais fait seulement que si ce même (r X) correspond à un terme dans le corps d’une règle, alors il est considéré comme vérifié sans le remplacer par sa définition.

Par exemple, soit ces deux règles :

(r a).
(s B) : (r B).

Si (r X) est posé en hypothèse, alors (s X) est vérifiée, parce que (s B) correspond à (s X) après unification et alors (r B) correspond à (r X), par la liaison entre X et B, comme (r X) est vérifié sans aller plus loin, (s X) est vérifiée sous cette hypothèse. Si la règle (r a) n’existe pas, le résultat est le même, puisque (r X) ne sera pas du tout vérifié et donc (r a), même pas recherchée. Cette remarque est importante, elle fait prendre conscience de ce que signifie « posé en hypothèse ». Cette remarque ramène aussi encore la question de la réalisabilité de l’hypothèse, mais c’est une chose qui ne peut pas se confirmer ou s’infirmer avec le seul langage objet. Justement, en parlant de ça, ce qui est intéressant dans cette notion de terme posé en hypothèse, et que ça s’interprète directement dans le langage objet, en utilisant ses seuls mécanismes, modulo une petite adaptation quand‑même, mais c’est encore quasiment le langage objet.

Quelle notation pour distinguer un terme comme étant hypothétique ? Pas d’idée pour le moment.

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 : 22173
Lun 9 Nov 2020 15:27
Message Re: Les logiques : notes en vrac
Plusieurs messages précédent le dernier ont été annotés en gras, comme sur une mauvaise piste. Il ne sont cependant pas supprimés, pour ne pas oublier la mauvaise intuition qui aura mené à une impasse.

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 : 22173
Lun 9 Nov 2020 17:19
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]
Reste la question du statut des variables apparaissant dans cette hypothèse. Ce qui est au moins sûr à ce point, c’est qu’elles ne sont pas liées à travers l’hypothèse. […]

C’est la même question qui avait été précédemment posée et dont une solution pressentie s’est avéré mener à une impasse. C’est la question.

Cette variable en plus de ne pas être liée à une valeur via l’hypothèse, ne doit pas être liée à une valeur par ailleurs non‑plus, sinon ce pourrait être incohérent. Par exemple si l’hypothèse (nat N) est posée et que ailleurs apparaît le terme (eq N abc), N ne doit pas être liée à abc, pour ne pas pouvoir être en contradiction avec l’hypothèse (nat N), quelque soit sa vérifiabilité.

Le meilleur moyen de l’exprimer, est par la liaison à une constante spéciale et unique (pas par la valeur spéciale précédemment décrite en plusieurs messages, qui est une impasse parce que ouvrant la porte à l’incohérence).

Que la variable puisse être liée à cette constante spéciale, empêche de la lier à une autre valeur mais n’empêche pas de la lier à d’autres variables, qui sont alors aussi liées à cette constante spéciale et unique.

Cette constante est spéciale dans le sens où elle ne doit pas pouvoir être posée dans l’écriture des règles (c’est à dire ne doit pas pouvoir être écrite dans les règles), pour ne pas permettre de lui faire dire autre chose que ce qu’elle dit. Elle appartient à un autre ensemble de constantes, en plus des deux ensembles de constantes déjà existants, celui des constantes de relation et celui des constantes de constructeur.

Donc, retour à l’idée initiale, celle des constantes spéciales et uniques, comme valeur de ces variables.

En marge, pourrait aussi se poser la question de la possible contradiction entre un terme posé en hypothèse et un autre terme. Cette question est plutôt laissée en suspend pour le moment. En tous les cas, la question ne se pose pas pour un terme qui n’est lié en rien au terme posé en hypothèse, et cette éventuelle liaison, passe pas les variables et la solution vient alors peut‑être d’elle‑même avec la solution qui doit être trouvée pour ces variables.

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 : 22173
Lun 9 Nov 2020 22:03
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Finalement, la solution est bien la toute première idée naïve et mauvaise, qui était d’ajouter l’hypothèse comme une règle au corps vide, mais avec une différence qui la rend moins naïve : cette règle n’aurait qu’une instance […]

Pour ne pas risquer que ce soit mal compris, il faut préciser que si le terme posé en hypothèse apparaît dans le corps d’une règle plutôt que dans une requête, cette hypothèse doit tout de même être instanciée chaque fois que la règle l’est. La raison est que l’hypothèse porte sur des instances de variables, comme les autres termes, pour que cette sémantique soit préservée, les termes qui ont un status d’hypothèse, doivent être instanciée en même temps que les termes de la règle dans laquelle ils apparaissent.

Ce qu’il faut surtout comprendre par instance unique, est ceci : comme déjà vu, au moment de vérifier une règle, la règle est d’abord instanciée, il y a donc une instantiation à chaque invocation de la règle par un terme, tandis que la vérification d’une hypothèse, ne s’accompagne pas d’une instanciation à chaque invocation de l’hypothèse, c’est une instance déjà existante qui est vérifiée (ou pas), possiblement plusieurs fois. C’est seulement qu’une hypothèse n’est pas instanciée au moment de sa vérification, mais avec la requête ou la règle qui la contient, seulement.

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 : 22173
Lun 9 Nov 2020 22:10
Message Re: Les logiques : notes en vrac
Il faut qu’une hypothèse soit connue au moment où un terme susceptible d’en dépendre, est rencontré. Syntaxiquement, l’hypothèse pourrait être écrite après le terme en dépendant, pourvu que les termes posés comme hypothèse soient collectés d’abord à fin d’avoir connaissance de tous, avant d’être en situation de rencontrer un terme en dépendant. Mais il me semble plus pédagogique et lisible je crois, de faire en sorte que la syntaxe nécessite d’écrire les termes en hypothèse avant les autres termes.

Comme la tête d’une règle ne peut pas être un terme posé en hypothèse, ce qui n’aurait pas de sens, les termes en hypothèse pourraient être écrits après la tête de la règle mais avant les termes du corps de la règle. Syntaxiquement, les hypothèses se situeraient mieux dans la moitié du côté du corps de la règle que dans la moitié du côté de la tête de la règle.

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 : 22173
Lun 9 Nov 2020 23:37
Message Re: Les logiques : notes en vrac
Ce que signifie poser une hypothèse, dépend de quoi on parle, de quel langage. Il n’y a probablement pas de définition effective et générale de cette notion ; elle est initialement abstraite.

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 : 22173
Mar 10 Nov 2020 20:17
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Il faut qu’une hypothèse soit connue au moment où un terme susceptible d’en dépendre, est rencontré. Syntaxiquement, l’hypothèse pourrait être écrite après le terme en dépendant, pourvu que les termes posés comme hypothèse soient collectés d’abord à fin d’avoir connaissance de tous, avant d’être en situation de rencontrer un terme en dépendant. […]

Ce n’est pas seulement qu’il faille avoir connaissance d’un terme posé en hypothèse avant de rencontrer un terme pour lequel il faudra éventuellement juger qu’il y correspond, c’est aussi qu’il faut, quand une variable est rencontrée dans un terme, savoir si elle apparaît aussi ou pas, dans un terme posé en hypothèse. C’est important, comme les variables apparaissant dans une hypothèses sont spéciales (comme déjà un peu expliqué ; ce le sera peut‑être mieux à une prochaine occasion).

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 : 22173
Mer 11 Nov 2020 00:03
Message Re: Les logiques : notes en vrac
Précédemment a été donné un exemple de séquence d’interactions, pendant laquelle il était possible de choisir quelle règle sera tentée pour résoudre un terme en cours.

Quand le terme est vérifiable par une hypothèse, faut‑il donner le choix de l’hypothèse ou même donner le choix de le vérifier une par une règle plutôt que par une hypothèse ?

Je crains que laisser le choix de vérifier par une règle, un terme vérifiable par une hypothèse, ne soit une possible ouverture à l’incohérence et qu’alors si un terme est vérifiable par une hypothèse, le choix ne doit pas être pas laissé, de le vérifier par une règle. En oubliant un petit détail un instant, laisser le choix de vérifier un terme par une règle quand il est vérifiable par une hypothèse, ne correspondrait pas à ce qui est attendu en écrivant l’hypothèse et serait même plutôt inattendu si on note que les variables apparaissant dans les hypothèses sont des sortes de généralité. Le petit détail omis juste avant : en fait, il pourrait même être vain de laisser le choix d’une règle, comme les variables spéciales apparaissant dans les hypothèses, sont liées à une constante spéciale, ce qui empêche les unifier à autre chose qu’à une variable liée à Any ou qu’à une variable liée à la même constante spéciale. Ce sont de bonnes justifications pour d’abord toujours tester si un terme est vérifiable par une hypothèse, et s’il l’est, de ne jamais tenter de le vérifier par une règle.

Concernant le choix de l’hypothèse, si plusieurs hypothèses vérifient un terme, alors le choix de l’hypothèse est sans importance, comme la vérification d’un terme par une hypothèse ne s’accompagne pas d’une unification (contrairement à l’unification qui a lieu avec la tête d’une règle, il n’y a pas d’unification entre un terme et le terme posé en hypothèse lui correspondant). Cependant, il n’y aurait pas de problème à restreindre le choix aux hypothèses correspondantes et à proposer d’en choisir une parmi celle‑ci, pour des questions d’expressivité des démonstrations, si on juge que dans une circonstance donnée, une hypothèse fait plus intuitivement sens qu’une autre.

Pour résumer : si un terme est vérifiable par une hypothèse, il doit être vérifié par une hypothèse, jamais par une règle, et le choix de l’hypothèse est sans importance, pourvu qu’elle soit parmi celles correspondantes.

Image
Hibou57

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