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
Mer 18 Nov 2020 03:25
Message Re: Les logiques : notes en vrac
Précédemment, une hypothèse ⟦(int-z I)⟧ a été posée en espérant prouver sous cette hypothèse, que I vérifie (int I), mais la requête a échoué et cet échec était un faux échec. Il y a plus longtemps, avait été posé une hypothèse ⟦(nat N)⟧ pour s’assurer de l’échec de (nat-lt (s N) N), et c’était un vrai échec, pas un faux échec.

Pourquoi l’un était un faux échec et l’autre un vrai échec ? Qu’est‑ce qui les distingue ?

Précédemment, il avait été noté que l’erreur avait été de poser ⟦(int-z I)⟧, ce qui pose I comme une généralité non‑décomposable. Mais il y a une explication plus générale et plus facile à comprendre.

En posant l’hypothèse ⟦(nat N)⟧ pour vérifier l’échec de (nat-lt (s N) N), on a en fait posé le corps de la règle en hypothèse. En posant ⟦(int-z I)⟧ pour vérifier (int I), on a posé la tête de la règle en hypothèse. Le corps en hypothèse, vs la tête en hypothèse. Hors, on ne peut pas conclure une chose découlant d’une définition, si on ne pose pas le corps de la règle. Poser la tête d’une règle en hypothèse équivaut à oublier le corps de la règle correspondante, au moins pour la variable concernée. Quand on pose un terme en hypothèse, il faut se demander si on veut vraiment raisonner à partir de la tête de la règle, en barrant l’accès au corps de la règle. Si oui, alors c’est correcte, si non, alors on se trompe. Si on espère raisonner sur une règle en pensant au corps de la règle, c’est la conjonction du corps de la règle qu’il faut poser. La limitation est qu’on ne peut pas (ou pas encore) le faire pour le corps de plusieurs règles en même temps. Avec une hypothèse portant sur une généralité, on court le risque de se tromper sur ce qu’on croit formuler. Il faut penser à ce qui vient d’être dit plus haut, à ce que représente et ce que ne représente pas, une hypothèse représentant une généralité.

C’est une reformulation peut‑être plus claire est plus complète, de ce qui avait déjà été dit à propos de cet erreur.

Il y a une autre manière de le comprendre, elle aussi vaguement esquissée précédemment.

Il a été répété, que les accords et désaccords entre les termes, passent par les variables. Une variable portant sur une généralité, peut produire un désaccord qui n’aurait pas lieu avec une variable ordinaire. Mais il faut noter, c’est important, qu’une variable portant sur une généralité, ne peut pas produire un accord qui n’aurait pas du avoir lieu (possibilité de faux négatifs, mais les faux positifs ne sont pas à craindre). Il a été question il y a plusieurs semaines, de la différence entre logique complete et logique incomplete. Les hypothèse portant sur des généralité, semblent rendre la logique incomplete, en l’empêchant de voir l’accord là où il devrait y en avoir un. Mais ce serait une appréciation incorrecte, car elle permette par contre, des vérifications finies, alors qu’elles seraient infinie avec des variables ordinaires.

Soit A et B, deux variables. Si aucune n’est liée à quoique que ce soit, elles peuvent toujours être liées entre elles. Si l’une n’est liée à rien, que l’autre est liée à quelque chose, celle qui n’est liée à rien, est alors liée à cette chose. Si les deux variables sont liées chacune à un terme, les deux termes sont unifiés. Il y a désaccord si l’unification échoue. Si A est liée à une généralité, que B est liée à un terme, même si la généralité que représente A, pourrait être le terme liée à B, il y a désaccord, parce que A pourrait être autre chose. Mais on pourrait aussi vérifier si oui ou non, l’accord serait éventuellement possible. S’il s’avère que A ne pourrait jamais être unifiable avec le terme liée à B, alors le désaccord est finalement un vrai désaccord. Si au contraire A pourrait, même si pas toujours, être unifiée avec le terme lié à B, alors le désaccord est en partie vrai et en partie faux, selon les cas. S’il s’avère que la généralité représentée par A devrait être toujours unifiable avec le terme représenté par B, alors le désaccord est clairement un faux désaccord. Si A et B sont deux généralités, il serait intéressant de distinguer les cas où la généralité est du même genre, c’est à dire représentée par une hypothèse du même schéma ou pas. Un cas particulier aussi est à noter. Deux variables normales A et B, peuvent être égale, même si elles n’ont pas le même nom. Deux variables A et B représentant une généralité, ne peuvent jamais être égales, parce qu’elles n’ont pas le même nom. Ça se comprend, comme A et B pouvant être une valeur quelconque vérifiant une hypothèse, on ne peut pas affirmer qu’elles sont égales … mais on ne peut pas affirmer qu’elles sont différentes, non‑plus, pourtant l’échec de l’unification entre ces deux constantes différentes, semblent prendre le partie du premier cas, sans plus de raison.

Parenthèse : cette dernière remarque aurait put être ajoutée à un des précédents paragraphes : en plus d’être sous l’hypothèse soit du corps d’une règle, soit de la tête d’une règle, ce qui fait une différence, on est finalement aussi sous l’hypothèse que deux généralités de noms différents, sont toujours différentes, jamais égales. Fin de la parenthèse.

Une requête se termine soit par un échec, soit par une ou des solutions. Il serait peut‑être intéressant de lui faire afficher des diagnostiques d’après les idées plus haut, concernant les possibles faux désaccords ou même les certitudes de faux désaccords, sans toutes‑fois interférer avec le status renvoyé par la requête. Il serait au moins utile d’afficher un message en cas de suspicion qu’une hypothèse ne correspond pas à ce à quoi on croit peut‑être qu’elle correspond. Même sans mettre en œuvre ces diagnostiques, il y a là au moins une piste de réflexion pour avoir un type d’hypothèses plus satisfaisantes. À nouveau, l’idée qui s’était avérée être une impasse, l’idée d’associer la généralité à un ensemble d’application de constructeurs possibles, serait tentante, mais le même écueil se présenterait toujours : la relation avec les autres variables. Pour rappel, cet exemple avait été donné :

(r a b).
(r b a).

Si on représente chacun des deux arguments par une généralité représentée par l’ensemble des valeurs possibles, sous une forme ou une autre pourvu qu’elle soit finie, on aura le même ensemble de valeurs possibles pour les deux, soit {a, b} , qui ne reflète pas que les deux arguments ne peuvent pas avoir la même valeur en même temps. Cette piste encore une fois tentante, finirait par s’échouer de la même manière : elle casse la relation entre les variables et ouvre donc la porte à l’incohérence (des faux positifs, au lieu de faux négatifs).

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 18:40
Message Re: Les logiques : notes en vrac
Les généralités peuvent être vu comme des types abstraits ou des types distingués par leurs noms, comme ceux des langages de la famille des Pascal. On y retrouve les mêmes limitations.

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 18:49
Message Re: Les logiques : notes en vrac
Il a été dit que si les hypothèses doivent être prouvées, c’est pour que leur vérification à priori dans les règles, ait un sens vis à vis de la sémantique du langage. Il y a une autre raison plus directement compréhensible mais moins généralisable : les hypothèses doivent être prouvées pour que les solutions aux requêtes, soient bien des solutions.

Si dans une solution trouvée à une requête, figure une variable caractérisée par une hypothèse, est que cette hypothèse n’est pas réalisable, c’est comme si la variable ne représentait rien au lieu de représenter un ensemble de valeurs au choix. Dans ce cas, on peut dire que la solution trouvée n’en est pas une.

Mais cette vision est moins généralisable, parce que un terme dans une règle, peut participer à la sélection d’une solution sans prendre part au terme solution. Par exemple, un terme « eq » peut dire que deux variables doivent être liées, ce qui filtrera les valeurs possibles comme solution, mais ce terme n’apparaîtra pas directement dans la solution elle‑même. Il en va de même avec les hypothèses. Dans ce cas, les solutions trouvées à une requête sembleront être de véritables solutions, mais elles seront des solutions potentiellement incohérentes. C’est encore plus méchant, car non‑directement perceptible.

Le point important à retenir est qu’on peut dire que prouver les requêtes est une nécessité pour que les solutions soient des vraies solutions, ça se comprend bien, mais il est plus correcte de dire que les hypothèses doivent être prouvées pour les applications des règles aient un sens, mais ça se comprend moins immédiatement.

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 19:10
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]
Mais cette vision est moins généralisable, parce que un terme dans une règle, peut participer à la sélection d’une solution sans prendre part au terme solution. Par exemple, un terme « eq » peut dire que deux variables doivent être liées, ce qui filtrera les valeurs possibles comme solution, mais ce terme n’apparaîtra pas directement dans la solution elle‑même. […]

Cet exemple souligne l’utilité de la distinction entre relations et constructeurs. Sans relations, il serait toujours possible de créer une paire d’entiers naturels tel que le premier est plus petit que le second, mais on ne pourrait le faire que dans un constructeur, le relation ne pourrait pas exister en dehors de ce constructeur. Ça signifie que par exemple les deux entiers ne pourraient pas avoir deux origines quelconques ou que cette propriété n’existerait plus pour ces deux entiers naturels, si on les extrayait du constructeur.

Sans relations, le langage n’a plus que des constructeurs. Ça permettrait sûrement d’exprimer un bon nombre de choses, mais ça deviendrait vite limité ou abusivement complexe.

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

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).

[…]

Ce n’est pas assez convaincant, parce que j’avais oublié un exemple à ce moment là (en y ayant pourtant pensé avant). Il faut lire ce qui suit comme un ajout après le paragraphe cité.

L’explication reposait beaucoup sur les termes ordinaires, mais il s’agit de termes posés en hypothèses, alors manque un exemple concernant directement la crainte de leurs éventuels désaccords. Pour commencer en répétant un peu, si l’hypothèse ⟦(r1 A)⟧ & ⟦(r2 A)⟧ est posée, qu’une règle contient un terme (r1 X) pouvant être prouvée par ⟦(r1 A)⟧, il sera naturellement vérifié par l’hypothèse qui implique cette vérification. La règle n’a pas besoin de dépendre de toute la conjonction en hypothèse, pour la respecter. Mais la règle pourrait ne pas respecter l’hypothèse si elle en demandait plus que l’hypothèse n’apporte. Bien la règle peut vérifier (r1 X) & (r2 X), elle ne peut pas vérifier un éventuel (r3 X), parce que ce terme n’est pas en hypothèse. Elle ne peut pas vérifier cet éventuel (r3 X) par une quelconque règle normale, si elle a vérifié (r1 X) ou (r2 X) par l’hypothèse, car ça implique que le X est lié au A de l’hypothèse. Ors, ces hypothèses créent des constantes spéciales qui ne peuvent pas être produites autrement qu’en posant une hypothèse, et ne peuvent donc pas non‑plus vérifier des termes autres que posés en hypothèse. Donc, une règle ne peut pas contraindre une conjonction en hypothèse. Il ne faut pas s’inquiéter qu’elle ne dépendent pas nécessairement de toute la conjonction en hypothèse ou se repose sur ces termes plusieurs fois ou dans le désordre, ça ne lui permettra jamais de contredire l’hypothèse sans faire échouer la règle, ce qui autrement, serait une 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
Mer 18 Nov 2020 20:24
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…] Un cas particulier aussi est à noter. Deux variables normales A et B, peuvent être égale, même si elles n’ont pas le même nom. Deux variables A et B représentant une généralité, ne peuvent jamais être égales, parce qu’elles n’ont pas le même nom. Ça se comprend, comme A et B pouvant être une valeur quelconque vérifiant une hypothèse, on ne peut pas affirmer qu’elles sont égales … mais on ne peut pas affirmer qu’elles sont différentes, non‑plus, pourtant l’échec de l’unification entre ces deux constantes différentes, semblent prendre le partie du premier cas, sans plus de raison.

[…]

Plus généralement, une particularité importante ou intéressante, des variables représentant des généralités, est que les liaisons qu’elles représentent, sont toujours explicites, jamais implicites. On sait que dans un terme ordinaire, comme (r A B), A et B peuvent être liées. Mais si on a une hypothèse ⟦(r A B)⟧ où A et B représentent une généralité vérifiant la relation, alors A n’est pas lié à B et réciproquement, c’est une « certitude ». La raison des guillemets, est donnée plus loin, cette certitude dépend du niveau de l’interprétation.

Plus haut, je disais « particularité importante ou intéressante ». Ça rend peut‑être ces hypothèses analysables, comme ne pourraient pas l’être des termes ordinaires. Mais il faudrait un exemple le montrant et ça me semble incertain.

Reste quand‑même la difficile question de la signification qu’il y a à considérer que A et B sont différentes dans le cas où elles pourraient pourtant être égales, si elles étaient des variables ordinaires. Quel sens y‑a‑t‑il à conclure que si on ne peut pas vérifier l’égalité, alors on considère qu’il n’y a pas égalité ? Il y a peut‑être là un problème d’interprétation à corriger. Faut‑il considérer ou pas qu’on est sous une hypothèse implicite que les deux variables sont différentes ? Je ne crois pas, ça pourrait même être incohérent. Si, disons, A et B peuvent être abc ou def, alors peut‑être que rien n’interdit, que A et B soit toutes les deux abc ou tous les deux, def, mais peut‑être aussi que quelque chose l’empêche. C’est encore plus perturbant si on pense à une hypothèse comme ⟦(eq A B)⟧, qui est réalisable. Que signifie affirmer l’échec quand la conclusion devrait plutôt être l’incertitude ? Peut‑il y avoir un moyen d’affirmer l’échec seulement dans le cas où les deux variables ne peuvent en effet pas être égales ? Peut‑être qu’une solution est de préciser quelque chose dans l’interprétation des hypothèses ? Le cas d’une hypothèse comme ⟦(eq A B)⟧, semble l’indiquer.

En attendant d’avoir une réponse à cette question je ne sais pas quand, un prochain message donnera une justification à une précédente idée, celle d’un diagnostique sur l’usage des hypothèses, avec une ébauche de formulation de ce diagnostique.

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

Pour information quand‑même :

  • Le caractère Unicode U+22A7, qui s’affiche comme ⊧ , c’est à dire |=, est utilisé pour dire « A  ⊧ B », « A est un modèle de B ».
  • Le caractère Unicode U+2AE4, qui s’affiche ou pas comme ⫤ , c’est à dire =|, pourrait être utilisé pour dire « A ⫤ B », « B est un modèle de A ».

Mais il y a un moyen détourné, les caractères dits “ box drawing ”, qui servaient avant, à dessiner des interfaces utilisateur en mode texte. Certains de ces caractères pourraient être utilisés d’une manière détournée, comme leur forme s’y prête bien. Ça ne respecterait pas la sémantique des caractères, mais mieux vaut des symboles qui s’affichent même si ce ne sont pas ceux qu’il faudrait, plutôt que les caractères qu’il faudrait et qui ne s’affichent pas.

Le caractère U+2561, ╡ pourrait convenir comme substitut à celui qui ne s’affiche pas. Mais pour raison de cohérence dans le style graphique, il faudrait alors aussi utiliser U+255E,╞ à la place de U+22A7, ⊧. Je leur trouve même l’avantage d’être plus lisibles, parce que plus gros. Toujours pour raison de cohérence dans le style graphique, les deux turnstiles, devraient être remplacés aussi, par U+251C,├ et U+2524 ┤.

Pour la saisie au clavier, il serait toujours possible d’utiliser le barre verticale | et les deux = et -.

Je crois que la syntaxe va être en partie redéfinie, c’est pourquoi je mentionne ces caractères.

Pour les gens que ça intéresse, voici la liste des caractères qui servaient à dessiner des fenêtres et menus en mode texte : Box Drawing (jrgraphix.net). Pour annecdote, ils n’étaient pas encodés comme en Unicode actuellement, ils étaient encodés comme des octets de 128 à 255, ce qui parfois posait problème, mais ce n’est pas le sujet ici.

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
Jeu 19 Nov 2020 14:21
Message Re: Les logiques : notes en vrac
Il y a donc un problème de faux négatifs avec les variables représentant des généralités, certains cas négatifs étant possiblement plus des incertitudes que des désaccords indiscutablement constatées. Ce problème n’existe pas avec les variables ordinaires, mais elles présentent le problème qu’on a pas la certitude de toujours avoir toutes les solutions. On sait que la méthode de résolution standard peut facilement en manquer, mais même la résolution dirigée par des choix à chaque étape, on et toujours pas sûr toutes les lister. De toutes manières, c’est au moins impossible de finir de toutes les lister, quand l’ensemble des solutions est infini. Les généralités, elles, représentent toutes les solutions pour un terme ou une conjonction de termes, même si ces solutions forment un ensemble infini, mais seulement pour ça.

Les variables représentant des généralités, ne sont pas entièrement insatisfaisantes, mais les variables ordinaires, non‑plus. Ça dépend de ce qu’on en attend.

Cependant, si les généralités représentent toutes les solutions pour un terme, même quand elles forment un ensemble infini, ces mêmes généralités, peuvent empêcher de trouver des solutions qui sont représentées par autre chose que l’hypothèse posée qui les introduite, puisqu’elles présentent le problème de pouvoir produire des faux cas négatifs ou plutôt des cas de désaccords incertains, par ignorance.

Même si les variables ordinaires ne sont pas entièrement satisfaisantes, elles ne laissent pas de doutes, si ce n’est qu’elles manquent des solutions. Les généralités ne manquent pas des solutions, mais seulement pour certaines variables (celles représentant les généralités sur lesquelles portent l’hypothèse posée), tandis qu’elles peuvent en faire manquer ailleurs.

Peut‑être qu’il faut trouver un moyen d’avoir de la glace liquide ou de l’eau chaude solide.

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
Jeu 19 Nov 2020 14:24
Message Re: Les logiques : notes en vrac
Les faux négatifs avec les généralités, me font penser à la principale limitation des types classiques à la Pascal.

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
Jeu 19 Nov 2020 17:30
Message Re: Les logiques : notes en vrac
Encore un retour sur un message d’il y a plusieurs semaines, en le mettant en rapport avec deux messages plus récents. C’est à propos de l’interprétation intuitive des variables et des définitions.

Il a été dit récemment, que les variables se comprennent mieux comme des liens. Il a été dit il y a un mois, que la notation « A : B » se lit le mieux comme « A est défini comme B », tout en remarquant que cette lecture est moins évidente quand B est vide. Cette idée de la définition est abstraite, elle se comprend mieux, car plus concrètement, si on considère que A : B définit les valeurs (par liaisons, pas par remplissage de cases individuelles) des variables qui y apparaissent. Si A : B est invoquée depuis un terme qui lui même est dans un règle, ainsi de suite jusqu’à la requête, la définition définitive des variables y apparaissant, n’est connue avec certitude qu’après la vérification complète de la requête, ce qui à l’origine de la distinction entre hypothèse vérifiable à priori et hypothèse vérifiable seulement à posteriori.

L’important est que lire A : B comme une définition, se comprend peut‑être plus facilement si on pense aux variables, juste que cette compréhension n’est pas entièrement généralisable, même si elle couvre la plupart des cas.

Image
Hibou57

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