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
Lun 16 Nov 2020 17:16
Message Re: Les logiques : notes en vrac
Une chose à souligner, qui ressort deux fois dans le précédent résumé de l’histoire jusqu’ici, c’est de toujours faire attention à la relation entre les variables : toujours se soucier que les ajouts sémantiques, ne permettent pas de briser la relation entre deux variables, parce que le sens ne serait plus respecté et ce serait alors une porte ouverte à l’incohérence.

Le langage de base qui a été présenté il y a plusieurs semaines, existe toujours, il est toujours présent, sa sémantique est toujours respectée. Le sens dans ce langage, repose beaucoup sur les liaisons des variables, la non‑contradiction des liaisons de variables. La contradiction d’une liaison est à la base de la définition de l’échec d’un terme. Et les variables peuvent être liées entre elles.

Pour cette raison, briser la liaison d’une variable, est une porte ouverte à la contradiction, la contradiction qui doit normalement signifier l’échec d’une vérification. Cette contradiction qu’on laisserait passer sans l’interpréter comme un échec, c’est l’incohérence.

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 16 Nov 2020 18:33
Message Re: Les logiques : notes en vrac
Pour prouver qu’une hypothèse est vérifiable, on peut donner un exemple de solution à ce terme ou conjonction de termes. Mais comme les variables spéciales comme elles sont appelées ici, représentent un ensemble de solutions à un ou des termes, il devrait être possible de poser comme exemple, des solutions générales, à base de telles variables. Ceci équivaudrait à prouver une hypothèse en utilisant une autre hypothèse, comme ces variables sont introduites par des hypothèses. Mais pour que ce soit une preuve que le terme est vérifiable, il faudrait que l’hypothèse en question ait déjà été démontrée. Ça rejoint la question précédemment posée, des propositions de solutions vérifiées par des règles pouvant éventuellement contenir des hypothèses. Là aussi, ces hypothèses devraient être déjà vérifiées.

On peut itérer l’ensemble des preuves d’hypothèses et ne pas considérer comme vérifiées, les preuves dépendant d’hypothèses non‑vérifiées, que ce soit dans la formulation de la solution ou dans les règles pouvant la vérifier. Si aucune preuves n’a put être vérifiée, on considère que c’est un échec. Si au moins une preuve a put être vérifiée, on recommence l’itération. Quand il ne reste plus aucune preuve non‑vérifiée, on a fini.

On sait qu’un terme peut être prouvé par plus d’une règle, mais qu’il suffit d’une seule preuve d’une hypothèse pour que l’hypothèse soit vérifiée. Il se peut donc qu’une preuve reposant sur une règle, soit vérifiable, tandis qu’une preuve reposant sur une autre règle, ne l’est pas, … ou pas encore, comme on itère plusieurs fois et qu’à une prochaine itération, les hypothèses dont dépend la preuve, seront peut‑être vérifiées.

En reprenant ce fidèle exemple des entiers naturels, soit ces deux preuves d’une hypothèse :

⟦(nat N)⟧ : (nat z).
⟦(nat N)⟧ : ⟦(nat N)⟧ & (nat (s N)).

Ça peut paraître incorrecte, la seconde preuve semblant reposer sur elle‑même. En fait, non. La première preuve peut être validée directement. La seconde preuve repose sur ⟦(nat N)⟧, dont une preuve vient d’être vérifiée, on s’assure alors que (nat (s N)) est vérifiable sous l’hypothèse ⟦(nat N)⟧, et c’est le cas (la règle correspondante étant « (nat (s N)) : (nat N). »).

Ça n’est circulaire qu’en apparence. Au moment de la vérification, l’hypothèse est prouvée par le première preuve, c’est comme si l’hypothèse désignait cette première preuve, la seconde n’étant pas encore vérifiée. C’est seulement après que la seconde preuve soit validée, que si on la vérifiait à nouveau, elle pourrait faire référence à elle‑même, ce qui est censé, puisque la définition des entiers naturels est récursive.

C’est intéressant à noter pour démontrer que non‑plus seulement des hypothèse, mais que des règles sont satisfiables. C’est aussi intéressant dans le sens où les preuves ne reposent plus sur des choix arbitraires de solution, mais sur des généralités.

L’idée est à noter.

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 16 Nov 2020 19:04
Message Re: Les logiques : notes en vrac
Si tous les termes d’une règle correspondent à des hypothèses prouvées, alors la règle peut être considérée comme démontrée satisfiable.

Note : attention aux termes liées par des variables ! Quand des variables lient plusieurs termes entre eux, l’hypothèse prouvée correspondante, doit avoir le même schéma que cette conjonction extraite. Si une règle contient les termes « (r A B) & (r B C) », sa satisfiabilité ne peut pas être prouvée par une hypothèse ⟦(r X Y)⟧, même prouvée, mais l’hypothèse ⟦(r X Y)⟧ & ⟦(r Y Z)⟧, si elle est prouvée, pourrait participer à la preuve de la satisfiabilité de la règle en question.

Plutôt que donner des solutions prouvant que chaque règle individuellement est satisfiable, ce qui pose le problème de notation précédemment posé, il serait possible de le faire indirectement, en prouvant toutes les hypothèses nécessaires à la preuve que toutes les règles sont satisfiables.

Pour chaque règle satisfiable, la tête pourrait être posée comme une hypothèse prouvée, si la tête contient une ou des variables. La preuve serait simplement le corps de la règle, qui aurait la forme d’une solution générale, dans l’esprit de ce qui a été décrit dans le précédent message. Le corps de la règle, doit se comprendre comme incluant aussi les hypothèses qui y apparaissent éventuellement. Pour cette raison, il serait plus simple de considérer qu’une règle satisfiable est aussi une hypothèse prouvée. Ça éviterait une duplication inutile.

Si une règle a un corps vide et une tête entièrement constante, à priori, une hypothèse pourrait être générée automatiquement, en remplaçant chaque argument de la relation par une variable, une pour chaque argument de la relation. Mais la création de variable automatique dont le nom ne serait pas délibérément choisi, n’est pas idéale, ces hypothèses auraient un air étrange et se poserait la question d’utiliser une même variable ou pas pour deux arguments égaux, un choix difficile à faire automatiquement. Par exemple l’hypothèse générée à partir de la règle « (nat z). », ressemblerait à ⟦(nat A)⟧ ou ⟦(nat X)⟧ plutôt que le ⟦(nat N)⟧ plus évocateur et moins surprenant. L’idée est intéressante pour un système partiellement automatisé, mais pour des raisons de lisibilité et des raisons pédagogiques (c’est lié), je crois qu’il est préférable d’attendre que les preuves de ces hypothèses soient écrites explicitement, même si elles sont évidentes et que ça peut sembler inutile (mais au moins, c’est facile).

On peut quand‑même remarquer que par exemple pour les règles des entiers naturels, une preuve d’une hypothèse ⟦(nat X)⟧ pourrait être générée automatiquement à partir de la règle « (nat z). », et par là, serait prouvée automatiquement la satisfiabilité de cette règle, puis ensuite, la satisfiabilité de la règle « (nat (s N)) : (nat N). », comme son unique terme (nat N), correspond au schéma de l’hypothèse ⟦(nat X)⟧.

Ne sera conservé pour le moment, que la satisfiabilité des règles, prouvée d’après les hypothèses prouvées et il n’y aura pas de génération automatique d’hypothèses prouvées, en dehors du cas implicite des règles prouvées satisfiables (si la tête de la règle contient au moins une variable).

En marge, cette idée n’a pas encore été mise en œuvre, ni plusieurs idées précédemment décrites. Ça va prendre du temps, alors aucun exemple vérifié ne sera donné avant quelques temps.

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 16 Nov 2020 22:33
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Une chose à souligner, qui ressort deux fois dans le précédent résumé de l’histoire jusqu’ici, c’est de toujours faire attention à la relation entre les variables : toujours se soucier que les ajouts sémantiques, ne permettent pas de briser la relation entre deux variables, parce que le sens ne serait plus respecté et ce serait alors une porte ouverte à l’incohérence.

[…]

Ça avait été oublié au début de la tentative d’introduction des hypothèse, parce que les exemples portait sur les nat, dont les termes ne portent que sur une variable.

Tout en restant fidèle au nat mais pour avoir une définition à deux variables, on peut s’intéresser à une définition des entiers relatifs.

Deux variables pour une définition des entiers relatifs, ça sonne étrange ? Et une représentation des entiers relatifs, sans signe, ça sonne étrange aussi ? Surprise : c’est une représentation des entiers relatifs sans signe et avec deux variables.

C’est une notation dont je ne connais pas le nom mais que j’ai parfois vu. Elle est basée sur les entiers naturels de Peano, en représentant un entier relatif par une paire d’entiers naturels, un pour la partie négative et un pour la partie positive, les deux tirant chacun de leur côté. Avec cette notation, un même entier naturel, peut avoir plusieurs représentations.

Par exemple, en notant les deux parties en décimal, (2, 3) représenterait en fait +1, tandis que (5, 1) et (6, 2), serait deux représentations possibles de -4 (moins quatre). La seule différence, est que les deux entiers sont représentés comme dans la relation nat, avec les deux constructeurs z et s.

§nat-b (nat z).
§nat-s (nat (s N)) : (nat N).
§int (int (int N P)) : (nat N) & (nat P).

Note : le int de (int N P) est un constructeur, le int le plus englobant, est la relation. Il faut se souvenir qu’il y a une différence entre constructeurs et relations. Ici, les deux sont homonymes, pour ne pas devoir inventer un second nom trop bizarre. Il est normalement préférable de ne pas utiliser des homonymes pour des constructeurs et des relations, mais disons que ça fera prendre l’habitude de lire des termes en faisant attention à distinguer les deux.

Par commodité, on peut ajouter une relation de l’entier zéro. Cette relation ne porte pas sur une constante, comme un entier relatif dans cette notation, peut avoir plusieurs représentations possibles.

§int-z (int-z (int N N)) : (nat N).

La définition de la relation int-z ne se réfère même pas à la relation int. On peut se demander si ce qui vérifie int-z vérifie bien toujours int.

(int-z I) & (int I) ?

Ce n’est pas un l, c’est un I majuscule. Il y a plusieurs solutions, et même une infinité. Encore un cas de vérification qui ne se terminerait jamais.

Mais on a notre baguette magique, les hypothèses, ça va le faire, c’est sûr :

⟦(int-z I)⟧ & (int I) ?

Bah, ça marche pas ? Pourquoi ça dit qu’il n’y a pas de solution ?

Ah, bing, bienvenu dans l’apparente dure réalité des variables représentant une généralité : elles sont non‑décomposables, même quand sémantiquement elles signifient des choses décomposables. Ce n’est pas une limitation de l’idée de les représenter par des constantes, cette idée leur correspond même parfaitement, c’est seulement qu’une telle variable se décomposerait comment, puisqu’elle représente toutes les valeurs possibles vérifiant un terme ou une conjonction ? Par exemple une généralité d’un nat, comme N, se décomposerait en une application du constructeur s ou en le constructeur z ? La variable pouvant aussi bien signifier z que (s z) que (s (s z)), etc, elle s’en trouve n’être décomposable en aucune manière.

On gagne en généralité, mais on perd les détails des cas en particulier. Comment cela pourrait‑il être autrement ? En fait, ce n’est pas seulement que les variables représentant des généralités ne sont produites que par des hypothèses, c’est aussi qu’on ne peut rien en dire sans ces hypothèses qui les introduisent.

Il faut relire à tête reposé pour bien réaliser. C’est important de le comprendre, sinon ouille les désillusions. Quand on a compris la limite, on peut passer à comprendre la solution à cette limite : si c’est trop général pour formuler ce qu’il faudrait, il faut explicitement aller dans les détails, mais il faut le faire de la bonne manière.

Donc, ces variables sont non‑décomposables et tout ce qu’on peut en dire, c’est ce qu’en disent les hypothèses qui les introduisent.

Soit, on va alors la poser explicitement en hypothèse, cette décomposition :

⟦(nat N)⟧ & ⟦(int-z (int N N))⟧ & (int (int N N)) ?

§int H#1 H#1
N = Abs#1

On a deux hypothèses dans le requête, mais vous ne remarquez pas une chose ? Dans la chaîne d’inférences, n’apparaît que la première hypothèse, utilisée deux fois, la seconde hypothèse n’a même pas été utilisée. En effet, il suffit de prouver que N est un nat pour prouver que (int N N) est un int. Mais on voulait vérifier que ce qui est int-z est toujours int …

Plus haut, on a voulu s’assurer que ce qui vérifie int-z, vérifie toujours int, mais on était encore partie pour une liste infinie de solutions, c’est à dire pour une vérification qui ne se termine jamais. Cette fois, après avoir calé sur une entité tellement abstraite qu’elle est non‑décomposable, on se retrouve avec une hypothèse que devait faire partie de la vérification, qui n’est même pas utilisée, ce qui est mauvais signe pour le sens qu’on croyait qu’avait la requête.

En fait, on avait calé sur la décomposition, mais ça n’implique pas qu’il fallait la poser entièrement dans l’hypothèse. Voici, avec la décomposition hors de l’hypothèse, mais avec une hypothèse sur le composant :

⟦(nat N)⟧ & (int-z (int N N)) & (int (int N N)) ?

§int-z H#1 §int H#1 H#1
N = Abs#1

Cette fois, la seule hypothèse utilisée est toujours la première, mais on ne s’en inquiète pas, elle est la seule. Surtout, on a bien vérifié la conjonction de int-z et int, par une vérification qui se termine : ce qui vérifie int-z, vérifie toujours int (même si c’est aller un peut vite de le lire comme ça).

Si on met l’échec avec « ⟦(int-z I)⟧ & (int I) ? » en face du succès de la requête plus haut, on peut s’interroger ; mais non, ce n’est pas une erreur, l’explication à été donné. L’échec précédent n’était pas une preuve que c’est impossible, une illustration que l’absence de preuve n’est pas la preuve de l’absence et on a fini par trouver une preuve, il aura seulement fallut formuler la requête autrement. Ça a une signification qui sera dite un peu plus tard, mais un autre message viendra avant.

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 16 Nov 2020 23:15
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]
⟦(nat N)⟧ & (int-z (int N N)) & (int (int N N)) ?

§int-z H#1 §int H#1 H#1
N = Abs#1

Cette fois, la seule hypothèse utilisée est toujours la première, mais on ne s’en inquiète pas, elle est la seule. Surtout, on a bien vérifié la conjonction de int-z et int, par une vérification qui se termine : ce qui vérifie int-z, vérifie toujours int (même si c’est aller un peut vite de le lire comme ça).

[…]

La parenthèse voulait dire qu’on a plutôt vérifié « une » conjonction des deux, pas que int-z implique int, même si c’est bien le cas ici.

Pour prouver que int-z implique int, il faudrait prouver que ce qui prouve int-z, prouve nécessairement int ; la réciproque n’est pas démontrable, on a au moins pas une équivalence entre les deux. Pour prouver l’implication, il faudrait prouver qu’il n’y a pas d’autres règles que int-z, autre que celle qui nécessite un int. Mais cette notion ne fait pas partie du langage défini.

On pourrait se dire que la définition de int-z pourrait produire une hypothèse sur son composant, comme celle qu’on a introduite. Mais cette hypothèse ne serait pas accessible en dehors de ce qui est sous la porté de la règle, en vertu d’une option décidée par choix (les justifications ont été exposées dans de précédents messages) (*). Ce choix fait que l’hypothèse doit être remontée, s’il le faut, en l’ajoutant explicitement dans une requête. On peut considérer qu’on ne doit raisonner que sur des choses qu’en les connaissant un minimum et que par exemple une documentation dirait qu’on peut vérifier int-z avec une preuve que son composant dédoublé est un nat. En fait, il n’y a même pas besoin de l’écrire dans une documentation, c’est dans le texte de la règle, qui est déjà une bonne documentation.

(*) l’hypothèse qu’elle pourrait produire, n’aiderait peut‑être même pas, si c’était une hypothèse sur une variable ordinaire.

On peut remarquer que l’hypothèse qu’on a ajouté, correspond au corps de la règle de int-z. Et justement, si on a la certitude qu’un int-z ne peut que être un int, d’où vient cette certitude si ce n’est de sa définition elle‑même ? (et qu’il n’y a qu’une définition) C’est une solution généralisable, qui est de poser le corps de cette règle, en hypothèse, pour prouver la conjonction de int-z et int. Cette stratégie est en théorie encore plus largement applicable, pas seulement dans ce cas.

On sait qu’une hypothèse doit être démontrée pour que le résultat de ce qui repose sur cette hypothèse, ait un sens. Cette hypothèse a été vérifiée plus d’une fois, on en a vu défiler, des entiers naturels.

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 17 Nov 2020 00:40
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Si on met l’échec avec « ⟦(int-z I)⟧ & (int I) ? » en face du succès de la requête plus haut, on peut s’interroger ; mais non, ce n’est pas une erreur, l’explication à été donné. L’échec précédent n’était pas une preuve que c’est impossible, une illustration que l’absence de preuve n’est pas la preuve de l’absence et on a fini par trouver une preuve, il aura seulement fallut formuler la requête autrement. Ça a une signification qui sera dite un peu plus tard, […].

La signification, c’est que la notion de négation par l’échec est à prendre avec méfiance. Ici, une négation par l’échec aurait fait à tord croire qu’on peut prouver que la conjonction de int-z et int n’est pas possible, alors qu’on a put prouver plus loin qu’elle est vérifiable.

Ma pensée personnelle est que la négation, à moins qu’elle n’ait une définition évidente et sans mauvaise surprise possible, mieux vaut s’en passer. J’ai déjà personnellement un mauvais à priori à son sujet, jugeant qu’il est généralement difficile de seulement lui trouver un sens.

Voici trois pensées personnelles à ce propos :

Si on a pas besoin de la négation, pourquoi la définir ? Je doute qu’elle soit nécessaire, qu’on ne puisse pas faire sans.

La négation qu’on connait, en tous cas dans l’informatique, c’est celle d’une condition, typiquement représentée par un booléen. La négation est donc celle d’un booléen : non‑vrai = faux et non‑faux = vrai. Mais qu’est‑ce qu’un booléen ? Vraiment, rien. Ce n’est pas un sentiment personnel, ce n’est véritablement rien de plus que d’autres constantes. Ce sont deux constantes sont plus des discriminants que les notions logiques que leurs noms laissent trompeusement croire. Un booléen fait une discrimination sur deux cas, on peut définir des discriminants sur plus de deux cas, comme trois cas avec la relation d’ordre : less, equal, greater, ils se valent autant. Dans le langage discuté ici, les booléens se représenteraient mieux comme des relations que comme l’échec ou le succès de la vérification d’une requête.

D’un point de vue logique, ici, la négation pourrait éventuellement correspondre à l’impossibilité de quelque chose. Mais on vient de voir que cette conclusion peut se faire à tord si on généralise trop. Avec des variables ordinaires, la vérification d’une chose impossible peut se terminer en recherche infinie, au lieu d’aboutir à un échec, autant d’ailleurs que la vérification d’une chose possible peut aussi se terminer en recherche infinie. Avec les variables représentant des généralités, la vérification d’une chose possible peut échouer parce que la généralisation ne dit pas ce qui permettrait de prouver une chose et par là, pourrait faire croire à tord à une négation par l’échec. On peut être sûr du succès d’une requête, on ne peut pas toujours être sûr de son échec. Ou alors, il faudrait pouvoir s’assurer de la négation de quoi on a vraiment eu une preuve.

Je crois plus à la négation comme l’échec de la couverture d’un ensemble par des sous‑ensembles : on pose un ensemble de choses par une définition, puis des zones couvertes par autant de définitions, et on vérifie qu’il ne reste pas de zones non‑couvertes. Dans le cas contraire, qui serait la négation de la couverture, on devrait pouvoir obtenir un exemple de zone non‑couverte. On pourrait appeler ça une négation par une preuve positive.

Un quatrième cas, pourrait être la négation par l’analyse des règles. La négation ne serait pas prouvée par le langage lui‑même, mais pas un niveau de langage permettant de raisonner sur les règles écrites dans le langage. La différence entre ce langage d’analyse et le langage objet, sera évoquée une prochaine fois.

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 17 Nov 2020 19:20
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Pour prouver que int-z implique int, il faudrait prouver que ce qui prouve int-z, prouve nécessairement int ; la réciproque n’est pas démontrable, on a au moins pas une équivalence entre les deux. Pour prouver l’implication, il faudrait prouver qu’il n’y a pas d’autres règles que int-z, autre que celle qui nécessite un int. Mais cette notion ne fait pas partie du langage défini.

[…]

C’est à dire qu’on est pas naturellement sous une hypothèse listant tous les cas vérifiant une règle. Quand on a repris le corps de la règle int-z pour faire une vérification sous cette hypothèse, c’est pourtant ce qu’on a fait, mais ça n’a été possible que parce qu’il n’y a qu’une seule règle correspondante, un cas qui peut se produire souvent, pas qui n’est pas généralisable. L’hypothèse représentant plusieurs règles ne peut généralement pas se poser de cette manière, elle se pose plutôt comme la tête de la règle (de l’ensemble de règles, en fait). Mais la tête de la règle posée en hypothèse, fait perdre les informations présentes dans les corps de l’ensemble des règles qu’elle représente, pourtant, elle a quand‑même l’avantage de représenter explicitement l’ensemble des règles alternatives possibles qu’on suppose, une information qui autrement n’a pas de représentation et à laquelle on ne peut donc pas se référer. En espérant juste que ce qui est dit là est au moins un peu compréhensible, comme je ne suis pas sûr que ce soit bien exposé. Le point important, est qu’il n’existe pas pour le moment, de représentation assez satisfaisante, de l’ensemble des règles vérifiant un terme. Soit on a une seule règle et alors on a une bonne représentation qui est le corps de la règle posé en hypothèse, soit on a plusieurs règles et alors on ne peut plus procéder de la même manière et ne reste que l’option de poser en hypothèse, un terme correspondant aux têtes des règles qu’on veut prendre en considération.

Ça rejoint une question qui sera abordée plus tard, mais sans lui donner de réponse pour le moment. Avant ça, un autre message reviendra sur trois notions concernant les hypothèses, pour éclaircir des choses qui peut‑être semblent déroutantes.


Un cas particulier en marge. Peut‑être qu’il serait possible, dans des cas particuliers, de poser en hypothèse, un ensemble de règles en posant le corps des règles comme une hypothèse, même si ce n’est pas faisable en général. Ce serait éventuellement possible si les règles ont toute le même nombre de termes et que les corps des règles peuvent être simultanément couverts par une conjonction de termes en hypothèse. Un exemple abstrait sera plus clair. Soit trois règles, R1 : A1 & B1, R2 : A2 & B2 et R3 : A3 & B3. Elles ont toutes les trois le même nombre de termes. Si en plus on peut poser une hypothèse A couvrant A1, A2 et A3, et de même, une hypothèse B couvrant B1, B2 et B3, alors on pourrait se placer sous une hypothèse A & B représentant une généralité « R1 ou R2 », avec peut‑être moins de perte d’information que si la généralisation ne représentait que « la tête de R1 ou la tête de R2 », comme dans le premier paragraphe de ce message. C’est un cas particulier, mais je le trouvais intéressant à relever, sans vouloir affirmer qu’il peut avoir ou souvent avoir un intérêt en pratique.

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 17 Nov 2020 21:54
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Le langage de base qui a été présenté il y a plusieurs semaines, existe toujours, il est toujours présent, sa sémantique est toujours respectée. Le sens dans ce langage, repose beaucoup sur les liaisons des variables, la non‑contradiction des liaisons de variables. La contradiction d’une liaison est à la base de la définition de l’échec d’un terme. Et les variables peuvent être liées entre elles.

[…]

Un retour sur des notions abordées vers le début de l’histoire.

Ce serait un ajout à faire à un précédent message d’il y a plusieurs semaines, où était résumé les éléments constituant le sens, dans le Prolog de base. Les variables ne semblaient pas s’introduire aussi naturellement que le reste, mais suit une autre formulation que celle qui avait été alors proposée.

Le langage permet de formuler des définitions en des termes renvoyant eux‑mêmes à des définitions (vide ou pas). Il avait été plus ou moins souligné que ces définitions ne peuvent être invoquées que dans un contexte pouvant les vérifier. Mais il n’avait pas encore été souligné que cette vérification se définie comme l’accord des termes entre eux, et l’accord ou le désaccord des termes entres eux, passe par les variables. Les variables s’expliquent mieux comme des liens que comme des places où on peut mettre quelque chose. Par ces liens, passent le fil de la cohérence, les termes communiquent leurs accords ou désaccords entre eux, par ce fil passant par les variables.

Le point important, est que les variables sont des liens et que la cohérence se définie comme le respect des liens.

Si on lit le premier paragraphe avec le sens commun, l’idée de désaccord peut évoquer un jugement comme « l’un a raison, l’autre a tort ». Mais ce jugement est parfois fait sans qu’il ne puisse l’être, deux parties en désaccord pouvant avoir tort en même temps. Si elles ont toutes les deux raison et sont pourtant en désaccord, c’est un problème qu’on ne va pas discuter. Ce qui est important ici, c’est que cette idée doit être oubliée : quand deux termes sont en désaccord, il n’est jamais cherché à savoir si l’un a raison et l’autre a tort, il est seulement noté qu’ils sont en désaccord et les situation de désaccord ne sont jamais retenues.

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 17 Nov 2020 22:02
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Si ce qui est appelé ici, les hypothèses vérifiables à priori, correspondait aux types, alors peut‑être que ce qui est appelé ici les hypothèses vérifiables seulement à posteriori, correspond aux types dépendants ? Ça se tiendrait peut‑être, comme des variables normales sont impliquées ; mais ça reste sans certitude. Quoiqu’il en soit, même si c’est le cas, c’est alors mieux expliqué par le fil de l’histoire jusqu’ici que par tout ce que j’en ai lu n’importe où ailleurs ; et je préfère malgré tout encore parler d’hypothèses vérifiables à priori et d’hypothèses vérifiables seulement à posteriori, ça me semble plus compréhensible, parce que mieux dire ce que c’est. Aussi, si ça correspond bien à ces notions, alors elles ont été introduites ici sans aucune complication telle que des niveaux de langage séparés.

En fait, si, un niveau de langage a bien été introduit et ça a même été évoqué avec les mêmes mots. Les hypothèses à prouver à posteriori, sont constatées comme des hypothèses notées dans le contexte et non‑marquées comme démontrées réalisables. Cette inspection du contexte pour y lister les hypothèses non‑prouvées, n’est pas une notion du langage, c’est une opération qui lui est extérieure. Les hypothèses ainsi relevées, peuvent être prouvée avec le langage lui‑même, en créant des requêtes leur correspondant. L’initiative de cette opération, aussi, ne fait pas partie du langage. Après la résolution d’une requête, si elle n’a pas échouée, on constate des hypothèses à démontrer à posteriori, on utilise le même langage pour les démontrer, mais, on y revient après en être sorti, après l’achèvement d’une requête. Ce qu’il se passe entre les deux, entre la sortie d’une requête et la vérification de nouvelles requêtes dérivées, ne peut que se placer à un niveau méta, méta‑jnsais‑pakoi, mais en tous cas extérieur au langage lui‑même. Il y a bien un autre niveau de langage, mais il est très simple, il se résume en deux opérations : listage d’hypothèses non‑prouvées, et génération d’une requête à vérifier pour chacune de ces hypothèses restant à prouver.

Chacune de ces requêtes doit être vérifiée dans le contexte résultant de la résolution de la requête précédente, la première hypothèse étant vérifiée dans le contexte résultant de la requête initiale. Les hypothèses à vérifier, doivent être extraites non‑pas terme par terme, mais par conjonction de termes d’après les liaisons des termes entre eux par leurs variables, en notant que pour les requêtes portant sur des variables ordinaires, il n’est pas suffisant pas de dériver ces liaisons d’après les noms des variables, les variables ordinaires pouvant être liées entre elles via les termes qu’elles désignent.

Ce n’est pas le sujet de ce message, mais au contraire des hypothèses portant sur des variables ordinaires, les hypothèses portant sur des variables spéciales, c’est à dire représentant des généralités, se vérifient à partir d’un contexte vide, elles sont des tautologies (si elles sont vérifiées).

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 18 Nov 2020 02:22
Message Re: Les logiques : notes en vrac
Sur les hypothèses portant sur des variables représentant des généralités, plusieurs choses ont été dites, pouvant sembler contradictoire. Ce messages les rassemble pour mieux appréhender le tout et comparer les situations. Dans ce message, les hypothèses portant sur des variables ordinaires, ne sont pas prises en compte.

Les hypothèses sont mentionnées dans trois circonstances dans lesquelles leur approche n’est pas comparable : quand elles sont prouvées, quand elles sont posées et quand elles sont utilisées. Il y a pour chacune de ces circonstances, une relation de un à plusieurs vers les cas de la circonstance suivante : la preuve d’une hypothèse peut vérifier plusieurs hypothèses posées, une hypothèse posée peut vérifier plusieurs termes.

Les choses pouvant sembler contradictoires.

Il a été dit qu’on ne peut pas séparer les termes d’une hypothèse quand ces termes sont liés par des variables, alors qu’il a aussi été dit qu’un terme peut être vérifié par un terme individuel d’une hypothèse. Par exemple, Par exemple, l’hypothèse ⟦(r1 A)⟧ & ⟦(r2 A)⟧ ne peut pas être divisé en deux hypothèses, alors que le terme (r1 B) apparaissant dans une règle peut éventuellement être vérifié par ⟦(r1 A)⟧ individuellement. La raison est que les termes dans une règle, sont vérifiés un par un, dans le contexte de la vérification des termes précédents, leur éventuels désaccords ne peuvent pas échapper (ce qui peut inclure une hypothèse manquant ou non‑correspondante). Mais quand l’hypothèse ⟦(r1 A)⟧ & ⟦(r2 A)⟧ est posé, ses termes ne sont pas vérifiés un par un comme dans une règle, aucun corps de règle n’étant appliqué, justement parce que c’est une hypothèse, le seul moyen de poser une généralité. Pour cette raison, la conjonction ⟦(r1 A)⟧ & ⟦(r2 A)⟧ doit avoir été prouvée toute entière, parce qu’il ne sera pas vérifié que ⟦(r2 A)⟧ est est accord avec ⟦(r1 A)⟧ d’après le contexte courant (l’accord est en fait posé dans le contexte courant).

Il a été dit qu’une preuve de ⟦(r A)⟧, peut vérifier les hypothèses ⟦(r1 A)⟧, ⟦(r1 B)⟧, ⟦(r1 C)⟧, etc. Pourtant elles ne portent pas sur la même variable. Ce qui l’explique, c’est que quand une hypothèse est posée, elle l’est sur une variable (ou des variables). Quand dans une règle apparaissent par exemple les termes (r X) & (r Y), les deux termes ne sont pas nécessairement les mêmes, parce que X et Y ne sont pas nécessairement liées. Mais si la relation r est vérifiable, et qu’on la vérifie dans une requête, elle sera vérifiable de la même manière, quelque soit le nom de la variable. La requête « (r X) ? » fournira la même solution que la requête « (r Y) ? ». Prouver une hypothèse, c’est assez comme la vérifier avec une requête. Poser une hypothèse, c’est assez comme poser des terme dans une règle.

Il a été dit qu’il suffit d’une preuve d’une hypothèse, pour que soient tenues pour vérifiées, toutes les hypothèses ayant le même schéma. Pourquoi alors poser des hypothèses ? N’est‑ce pas une répétition inutile ? La raison est assez la même que dans le précédent paragraphe, la différence est la même que entre vérifier par une requête, qu’un terme est réalisable et poser ce terme dans une règle. Quand on pose une hypothèse, ont dit sur quelle variable elle porte dans la règle. Quand on prouve une hypothèse, on ne la pose pas pour qu’elle s’applique à une variable dans une règle, on s’assure seulement qu’elle est vérifiable et que ça a donc un sens de la poser. On la prouve une fois, pour pouvoir la poser autant de fois qu’on veut, sur les variables qu’on veut.

En résumé, ne pas confondre : vérifier un terme par une hypothèse posée, poser une hypothèse préalablement prouvée et prouver une hypothèse. En parlant d’hypothèse, il faut toujours savoir dans laquelle de ces trois circonstances on se trouve.

Image
Hibou57

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