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 : 20298
Mar 5 Oct 2021 17:11
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Comme déjà rapidement suggérée l’année précédente, cette constante pourrait même se trouver ailleurs que en première position du terme. Toujours pour prendre une exemple pour le moment syntaxiquement incorrecte, au lieu d’être (eq A A), le terme pourrait être (A eq A). Là encore, s’il existe par ailleurs une règle (r A B) dont A = eq et B = r serait une solution, alors (r eq r) serait une solution aux deux règles.

[…]

Cet exemple illustre une conséquence de deux choses. La première est un mélange de conventions, avec la constante de la relation, en seconde position dans un cas et en première position dans l’autre cas. D’ailleurs, plus que de convention, il conviendrait mieux de parler d’une syntaxe, mais pas au niveau de la définition du langage, au niveau de son utilisation. La seconde, est le double usage de la constante eq (et même de la constante r), mais ça dépend aussi de ce que serait censée signifier cette hypothétique règle (r A B).

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 : 20298
Mar 5 Oct 2021 17:51
Message Re: Les logiques : notes en vrac
Il y a un peu moins d’un an, la notion suivante avait été décidée, pour représenter une hypothèse :

Citation : 
⟦H⟧


Cette notation avait été choisie, parce qu’elle reprend une sorte de crochet carré, déjà utilisé dans la déduction naturelle pour représenter certaines hypothèses. Les crochets carrés n’avaient pas été utilisés, parce que la notation de la déduction naturelle est moins répandue qu’une autre notation, répandue dès le collège, elle : la représentation d’un interval ou d’une séquence, utilisant ces mêmes crochets carrés, comme dans [0, infini [ ou [1; 2; 3].

Un autre problème, est qu’il semble que dans la déduction naturelle, les hypothèses notées entre crochets, sont des hypothèses disponibles, mais non‑utilisées.

De plus, ces crochets carrés à double‑bar ne s’affichent pas toujours bien. Ils s’affichent normalement bien plus haut, mais pas ici : ⟦H⟧ (mais ça dépend des navigateurs et de la gestion des polices de caractères, et ça peut changer au fil des mises à jours, en bien comme en mal).

Comme une hypothèse représente ici, une généralité, c’est à dire l’ensemble de tous les cas possibles d’un terme, peut‑être que les crochets utilisés pour les ensembles, seraient une meilleure idée : {H} au lieu de ⟦H⟧. Pour ne pas risquer d’introduire des erreurs d’écriture, les messages qui ont été écrits avec l’ancienne notation, ne seront pas ré‑édités.

Comme dit plusieurs fois, trouver une bonne notation, c’est toujours compliqué, mais c’est nécessaire avec ce qui est récurrent et doit avoir une représentation autant concise que possible.

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 : 20298
Mar 5 Oct 2021 19:35
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Une possible compréhension des choses, peut être à corriger, mais ça doit être à peu près ça.

Tout comme le « vrai » ne peut désigner autre chose que lui‑même, entre autres pas le « faux », tout comme le « faux » ne peut désigner que lui‑même, entre autres pas le « vrai », une expression ne doit avoir qu’un seul sens désigné (même s’il peut être désigné de plus d’une manière). On peut tirer des conclusions du sens désigné ; dans le langage courant on parlerait aussi bien de signification dans le premier cas que dans le second cas, mais ce n’est pas la même chose, sinon le sens, plus explicitement, le sens désigné, ne serait pas fiable, c’est à dire que le sens (celui de la sémantique) serait vain. C’est au moins le cas de la sémantique qui intéresse la logique (dans d’autres domaines, soit c’est à nuancer, soit c’est plus confus ou joueur ou manipulateur). C’est là qu’est la principale utilité de la notion de type, qui est un moyen de restreindre l’écriture d’une manière qu’elle ne puisse pas utiliser un sens en lieu et place d’un autre, ce que la syntaxe seule permettrait, à moins qu’elle ne soit déjà restreinte d’une manière qui ne lui permet pas de formuler à propos de tous les concepts eux‑mêmes, de sa propre sémantique, ce qui est quand‑même parfois le cas. Dans ce cas, le type est implicitement garanti par la syntaxe, mais une syntaxe dont l’expressivité a alors des limites.

Ça sous‑entendait une restriction à posteriori, c’est à dire que le type valide ou invalide une écriture. La restriction à priori, qui ne nécessite pas de validation à posteriori, produit un résultat équivalent à d’abord écrire puis filtrer ce qui n’aurait pas dut l’être ou filtrer des solutions non‑acceptables. Contrairement à ce qui a été suggéré à la fin du message cité, cette restriction à priori ne se fait peut‑être pas toujours mécaniquement au détriment de l’expressivité.

La raison de ce qui est dit plus haut, sera expliquée dans un message prochain.

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 : 20298
Mer 20 Oct 2021 21:38
Message Re: Les logiques : notes en vrac
Je ne sais plus si ça avait déjà été dit, alors ce sera peut‑être une répétition ou une reformulation.

Il avait été fait mention d’une règle de certaines logiques, disant que du faux ont peut tout conclure. Il avait été dit que bien que logiquement compréhensible, ça inspire la suspicion.

Un cas où ce serait moins suspect, est quand il faut montrer qu’une hypothèse représentant un cas d’une hypothèse qu’on vient d’ouvrir, n’est pas possible. Si en ouvrant {H} on y trouve {H1}, {H2}, {H3}, si on ne peut pas vérifier X directement à partir de {H}, on doit vérifier X à partir des {Hn}. Mais si disons, {H3} n’est pas possible, c’est un cas à ne pas couvrir. Seulement, il faudrait le démontrer. On se retrouverait alors à démontrer que {H3} est impossible. On pourrait le voir comme une manière de conclure X à partir de l’impossibilité de {H3}, mais on peut aussi le voir comme l’exclusion du cas {H3}, ce qui est encore moins suspect.

Le paragraphe précédent est en oubliant que jusque maintenant, les d’une hypothèses, sont générés automatiquement, même si une difficulté avait été rencontrée (pas encore étudiée depuis).

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 : 20298
Mer 20 Oct 2021 21:41
Message Re: Les logiques : notes en vrac
Il avait été souligné qu’une spécification n’est pas un programme, même une spécification à l’apparence executable, comme celle dans un langage à la Prolog. Il n’avait pas été dit ce qui les distingue : c’est qu’un programme est un choix de chaînes d’inférence en particulier, alors qu’une spécification n’en impose aucune en particulier, dit seulement lesquelles sont possibles.

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 : 20298
Mer 20 Oct 2021 22:04
Message Re: Les logiques : notes en vrac
Parfois il est plus concis de formuler des règles en supposant qu’elles sont ordonnées, que la première qui correspond, s’applique, et que les autres sont ignorées. Mais ici, l’ordre des règles n’a pas d’importance (excepté pour démontrer leur satisfiabilité), l’ordre des termes non‑plus (sémantiquement, pas en pratique).

Il est quand‑même possible de mimer une relation d’ordre entre des règles, mais c’est plus inutilement verbeux. Un exemple abstrait :

A.
B : not A.
C : not B & not A.
D : not & C and not …

Plus le numéro d’ordre augmente, plus il y a de négations. C’est déjà un problème, mais ça nécessite aussi d’introduire la négation qui ne l’a pas encore été jusque maintenant.

Le langage décrit ici, pourrait donner l’impression d’avoir une notion de relation d’ordre avec l’ordre des termes internes à un terme englobant. Mais il a été dit que à condition que la permutation soit faite partout (ce qui n’est pas trivial à faire automatiquement), cet ordre est permutable, alors ce n’est pas vraiment un ordre.

Serait‑il utile d’introduire une notion d’ordre dans la sémantique du langage ? Ou est‑il possible de s’en passer ? Peut‑être y‑a‑t‑il un choix à faire entre introduire la notion de négation ou introduire la notion d’ordre.

Plus haut, il est montré que la notion d’ordre peut se formuler à partir de celle de la négation, mais l’inverse est aussi possible. Si on suppose que ces deux règles sont ordonnées :

A : …
B : ….

En B, on a non A et montrer qu’on a toujours B, serait équivalent à montrer qu’on a toujours non A.

Ce n’est qu’une ébauche d’idée, mais ça semble être une question à poser. Aussi, en supposant qu’un choix est à faire entre les deux parce que l’un des concepts est exprimable à partir de l’autre et qu’on ne veut pas de redondance, laquelle des deux options s’avérerait la plus souvent pratique ? La notion de négation me semble assez innée, mais formuler des règles en les ordonnant par priorité, permet des formulations concises dans des cas qui ne sont pas si rares. En le disant, je me demande quand‑même si la notion de priorité ne serait pas plus innée que la notion de négation.

Il faudrait distinguer les règles ordonnées des autres, en groupant d’un côté celles qui n’ont pas de relation d’ordre entre elles, et d’un autre, celles qui en ont une et pour celles‑ci, il y aurait même plusieurs groupes.

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 : 20298
Mer 20 Oct 2021 23:33
Message Re: Les logiques : notes en vrac
Une autre question semblant en rapport avec la précédente, mais qui ne l’est pas ; en parlant des termes et non‑plus des règles, cette fois.

Dans le monde de la logique, une séquence d’éléments, comme des constantes ou d’autres termes, est quasiment toujours représentée de cette manière : 

(a (b (c (d ())))) ou (cons a (cons b (cons c (cons d nil))))

Typiquement, il existe une notation plus concise :

[a b c d]

Mais cette notation n’est qu’une apparence donnée à la représentation sous‑jacente, dans le genre des deux précédentes.

Deux choses me chiffonnent avec cette manière de représenter une séquence. D’abord, c’est un arbre dégénéré, alors qu’une séquence et un arbre, ne sont pas la même chose. Ensuite, elle ne peut se prendre que par un bout, avant de pouvoir la prendre par l’autre bout, il faut l’inverser ; la relation entre une liste et son sens inversé, peut être représentée par une règle.

J’ignore si la question de pouvoir la prendre un bout ou par l’autre, indistinctement, est vraiment pertinente. Ce n’est peut‑être qu’une mauvaise idée donnée par le fait de vivre dans un monde spatial, et celui des formules écrites, n’est pas le même.

Pour la question de l’arbre dégénéré, il existe une autre représentation, en apparence similaire, mais qui n’en fait plus un arbre. Cette représentation est constituée de deux listes, liée par une relation pouvant être représentée par une règle aussi.

Des exemples seront plus clairs q’une description. Ci‑dessous, chaque ligne est dérivée de la précédente.

(a (b (c (d ())))) () -- Deux listes, celle de droite et vide
(a (b (c ()))) (d ()) -- Le d est passé dans la liste de droite.
(a (b ())) (c (d ())) -- Le c est passé dans la liste de droite.

() (c (d (b (a ())))) -- La liste de gauche est vide, celle de droite est l’ancienne de gauche, inversée.
(() c) (d (b (a ()))) -- Le c est passé à gauche.


Cette représentation d’une séquence à partir de deux listes, permet de représenter une position dans une séquence, ce qui semble intéressant, pour une séquence et n’est plus un arbre dégénéré, un arbre n’ayant qu’un seul tronc, mais la représentation utilise toujours deux arbres dégénérés.

On avance vers la droite ou la gauche en repoussant à chaque fois, un élément de la liste de un des côtés dans la liste de l’autre côté. On a toujours l’avant et l’après, qui rime bien avec l’idée d’une séquence. La représentation classique, n’a pas des propriétés autant intéressantes.

Je ne sais plus où j’avais vu ce type de structure, alors je ne peux pas donner de référence ni donner son nom.

Une autre idée, pourrait être d’avoir une notion de séquence dans les termes, un peu à la manière dont il serait peut‑être possible d’avoir une notion de relation d’ordre dans les règles.

Le terme (a b c d) ne serait plus vu comme permutable pourvu que les permutations correspondantes soient appliquées ailleurs, il serait vu comme b après a, c après b, etc. Il serait nécessaire de différencier ces termes des autres, pour la cause de l’unification, comme décrit plus loin.

Ça nécessiterait de redéfinir l’unification. Jusqu’ici, l’unification de deux termes n’a qu’une solution ou n’en a aucune. Avec l’exemple plus haut, il serait facile d’imaginer unifier (a b c d) avec (A), mais l’unification avec (A B) (A et B sont des variables), pourrait avoir plusieurs solutions : A = a et B = b c d ou A = a b et B = c d, etc. De même l’unification avec (A B C), pourrait aussi avoir plusieurs solutions. Pour cette raison, il serait nécessaire de distinguer ces termes des autres, pour ne pas altérer le reste de la sémantique du langage.

Avec la représentation précédente, celle de la double‑liste, on trouverait plutôt plusieurs solution vérifiant une règle, pour des variables A et B, mais sans nécessiter de redéfinir l’unification. Le cas a trois variables ou plus, ne serait pas possible.

L’idée d’une notion de relation d’ordre dans les termes (différente de la même idée avec les règles), présente aussi le problème de la décomposition. Comment décomposer le terme (a b c d), si l’unification peut avoir plusieurs solutions ? S’il n’est pas décomposable, il n’est pas utilisable : bien qu’il donne l’impression de pouvoir être pris par n’importe lequel des deux bouts, il ne peut en fait, l’être par aucun.

La première solution qui ne nécessite que de définir des règles sans introduire de nouveau concept sémantique, est peut‑être la meilleure. Mais peut‑être quelque chose d’intéressant se cache‑t‑il dans la seconde solution.

Là aussi, ce ne sont que des ébauches d’idé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 : 20298
Jeu 21 Oct 2021 09:29
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Plus haut, il est montré que la notion d’ordre peut se formuler à partir de celle de la négation, mais l’inverse est aussi possible. Si on suppose que ces deux règles sont ordonnées :

A : …
B : ….

En B, on a non A et montrer qu’on a toujours B, serait équivalent à montrer qu’on a toujours non A.

Ce n’est qu’une ébauche d’idée, […]

Mais comment montrer qu’on a toujours B, sans montrer qu’on a jamais A ? C’est la négation qui semble plus essentielle et l’ordre des règles qui serait une notion dérivée. Surtout qu’il y a déjà une notion implicite de la négation avec l’échec de la vérification d’une règle et qu’une piste pour définir la négation avait été proposée, avec les hypothèses : montrer que A est toujours faux nécessite de le montrer en général et donc sous des hypothèses (à moins que les termes de la requête n’aient aucune variable libre, directement et indirectement).

Cette idée est abandonnée. Définir des règles en les supposant ordonnées par priorité, ce ferait avec un sucre syntaxique qui produirait automatiquement les négations nécessaires.

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 : 20298
Jeu 21 Oct 2021 11:12
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Une autre idée, pourrait être d’avoir une notion de séquence dans les termes, […]

Ça nécessiterait de redéfinir l’unification. Jusqu’ici, l’unification de deux termes n’a qu’une solution ou n’en a aucune. Avec l’exemple plus haut, il serait facile d’imaginer unifier (a b c d) avec (A), mais l’unification avec (A B) (A et B sont des variables), pourrait avoir plusieurs solutions : A = a et B = b c d ou A = a b et B = c d, etc. De même l’unification avec (A B C), pourrait aussi avoir plusieurs solutions. Pour cette raison, il serait nécessaire de distinguer ces termes des autres, pour ne pas altérer le reste de la sémantique du langage.

[…]

Sémantiquement, elle n’a qu’une solution, même si techniquement, elle peut en avoir plusieurs. Même si techniquement elle peut en avoir plusieurs, le sens reste le même, comme le sens d’une variable liée, c’est son développement complet, récursivement.

Pour revenir à la question, dans l’exemple plus haut, l’erreur est de tenir A et B pour des variables ordinaires, alors que le terme (a b c d) n’est pas tenu pour un terme ordinaire, mais pour une séquence qui n’est pas un arbre dégénéré. Dans ce cas, l’unification de (a b c d) et de (A B) doit se faire en considérant (A B) comme une séquence, ce qui implique finalement de ne pas traité A et B comme des variables ordinaires, mais comme éléments variables d’une séquence. Une solution serait que la séquence (A B) soit liée à la séquence (a b c d), sans séparer A et B. Dans ce cas, l’unification n’a qu’une solution, et de même en unifiant (a b c d) à (A B C). L’unification par la suite, de (a b c d e) et de (A B C) échouerait, l’unification de (a b c d e) et de (A B C D) aurait une solution et l’unification de (a b c d e) et de (D A B C) échouerait. Il faudrait évidemment une autre notation que celle‑ci, pour distinguer ce type de terme.

Un problème que posait cette idée vient d’avoir une solution ; reste celui de la décomposition par l’unification.

Image
Hibou57

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