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
|
Dim 27 Sep 2020 20:08
Re: Les logiques : notes en vrac
Implicitement, je crois que ce qui est à droite du séquent dans une conclusion, est ajouté au contexte. Ce qui me le fait penser, c’est la règle d’inférence du lambda calcul simplement typé, pour l’introduction d’une constante (mais c’est un des détails qui peut varier d’une source à l’autre), qui ne pose que l’expression dans le langage objet comme seule condition et rapporte directement la déclaration dans la conclusion, comme expression à droite du séquent alors qu’il n’y en a même pas dans la condition.
Mais parfois je vois des conclusions avec un nouvel élément apparaissant dans le contexte, qui n’y était pas dans la condition. Au moins une règle d’inférence structurelle de la dédiction naturelle le permet même en général, la règle appelée “ weak ”, qui permet d’ajouter un élément arbitraire sous une simple condition. Il y aurait donc deux manières d’augmenter le contexte ? Sont‑elles équivalentes ? Je crois que en gros, oui, mais la question doit être posée. Dans la règle de l’introduction de l’implication dans la déduction naturelle, un élément se trouvant à gauche du séquent dans la condition de l’inférence, se trouve à droite du séquent dans la conclusion. Ça indique explicitement, que les éléments se trouvant à gauche du séquent, ne sont pas toujours des objets étrangers au langage objet et représentant ses élaborations ou ses règles de construction, ces éléments peuvent aussi être des expressions du langage objet lui‑même. Ça indique que en général, un contexte peut au moins être un ensemble d’expressions du langage objet, ce qui en donne une définition de base. Quand le contexte du séquent de la conclusion est constitué de plusieurs éléments, la formule dans la conclusion, n’est peut‑être ajoutée qu’à un élément du contexte, celui dont le type correspond, mais tout en nécessitant les autres éléments ou répartis entre plusieurs de ces élément ou autres, selon le domaine. Quand il y a plusieurs séquents dans la conclusion, ça doit être compliqué, mais les inférences de ce types sont invalides en logique intuitionniste, celle qui me semble la plus appropriée . Pour la propagation, ça doit simplement suivre l’arbre des inférences (c’est une vision trop impérative sur le moment, qui m’a fait poser une question qui n’aurait pas dut l’être, comme on peut suivre un flot de données descendant dans des fonctions, les retours dans le sens du retour étant les conclusions. Au passage, une fonction peut renvoyer une fermeture : il serait utile de savoir si une chose équivalente existe dans les démonstrations. Ça mérite réflexion.  Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] Ajout d’un cas |
 
|
|
|
|
|
|
Administrateur
|
Dim 27 Sep 2020 20:38
Re: Les logiques : notes en vrac
Les règles d’inférence, peuvent parfois se lire dans les deux sens, mais pas toujours. Avec la déduction naturelle en particulier, quelque chose se lit dans les deux sens, mais je ne sais plus si ce sont les preuves d’une certaine manière ou les règles d’inférence ; le premier cas, il me semble, mais à vérifier.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Sep 2020 10:25
Re: Les logiques : notes en vrac
Sur le sens des mots employés en parlant des séquents, voir : Sequent (ncatlab.org).
D’après cette page, le contexte c’est l’ensemble de ce qui se trouve à gauche, et les éléments de ce contexte sont effectivement de nature variable, tantôt appelés des environnements, tantôt nécessairement des propositions ou autre. Il est confirmé que l’ordre des séquents est important, en comparant une liste de séquents à des fonctions imbriquées (higher order sequent), qui se peut se comprendre comme : dans une liste de séquents, les séquents à droite sont dans le contexte défini par les séquents à gauche (équivalent à une associativité à gauche, comme l’application des fonctions curryfiées), le premier séquent tout à gauche, ayant un contexte vide. Ce qui encore, confirme la nature variable des éléments du contexte des séquents. Les éléments du contexte d’un séquent peuvent donc au moins être : des expressions dans le langage objet (implicite avec une règle de la déduction naturelle et confirmé par la page plus haut) qui peut être un langage de propositions mais pas seulement, des ensembles ou listes de choses élaborées par le langage objet et souvent appelés un environnement (explicite quand les séquents formalisent une sémantique), des séquents eux‑mêmes (quand plusieurs séquents se suivent). Depuis la même page, un lien vers le même site est indiqué, sur des définitions précises de ce que sont les séquents et comment ils sont manipulés : Sequent calculus (ncatlab.org). Mais juste après, la page précise que la nature précise des séquents est encore variable, puis fait référence à trois types de séquent parmi les plus importants. Il faut tout préciser, il n’y a pas de définition unique dans ce domaine. Il faut aussi choisir ce qui convient le mieux au domaine d’application, après en avoir bien compris le sens et les implications. Il faut être explicite, quitte à introduire le tout en répétant des choses risquant de sembler évidentes à certaines personnes. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Sep 2020 22:16
Re: Les logiques : notes en vracHibou a écrit : […] Que l’ordre puisse ne pas être important, ça me semble bien peu probable quand‑même. Dans ce cas là, mieux vaut encore écrire un seul séquent. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Sep 2020 22:34
Re: Les logiques : notes en vracHibou a écrit : […] Comme une succession de séquents est équivalente aux contextes imbriqués de fonctions imbriquées, alors ce qui est à gauche des séquents, est équivalent aux paramètres de ces fonctions et l’ordre des paramètres n’est pas important quand les paramètres sont nommés (il n’est important que quand il ne sont pas nommés pour l’appelant et ne se distingue alors que par leur position). Toujours parce que les successions de séquents sont des contextes imbriqués (de la gauche vers la droite, se lisant du plus englobant au plus interne), alors il faut sûrement faire attention aux noms des éléments à gauche des séquents, parce que si cette analogie est bien la bonne (elle me semble l’être assez clairement), alors ça signifie que dans A ⊢ B A ⊢ C, le second A masque le premier, de même que pour une fonction imbriquée, un paramètre du même nom que celui du paramètre d’une fonction englobante, masque ce paramètre. Pour éviter les masquages et surtout aussi éviter les malentendus, mieux vaut écrire A1 ⊢ B A2 ⊢ C, si les deux éléments sont différents et écrire A ⊢ B ⊢ C si les deux A était censés en désigner un seul (dans ce dernier cas, écrire A ⊢ B A ⊢ C serait même une possible erreur). Dans les notations plutôt graphiques, les séquents multiples ne sont séparés que par de longs espaces, mais ce n’est pas commode avec une écriture linéaire, non‑graphique. Je me demande si ça poserait un problème ou pas de les séparer par des points‑virgules, par exemple A1 ⊢ B ; A2 ⊢ C. Je ne crois pas avoir déjà vu d’usage du point‑virgule dans ce contexte, alors il ne devrait pas avoir d’interprétation ambiguë. Toujours à propos des écritures linéaire, j’avais rapporté il y a un peu longtemps, qu’il semble raisonnable de se permettre d’utiliser le symbole ∴ à la place du grand trait horizontal d’une règle d’inférence. Ce symbole est un caractère Unicode nommé therefore et son code‑point est U+2234. Même si l’ordre des éléments à gauche du séquent n’est pas significatif, je crois que ça ne peut que aider la lecture de fixer un numéro d’ordre aux éléments pouvant y apparaître et de poser une convention de nommage pour distinguer les sortes de ces éléments, comme autrement rien ne distingue leurs sortes ; par exemple écrire en lettres grecques majuscules les éléments ayant le rôle d’ensemble de jugements de typage, en lettres latine majuscules les ensembles de variables (juste un exemple sans intérêt réel), en lettres minuscules, les états, et utiliser l’apostrophe pour signifier les dérivations, etc, et par exemple poser qu’un ensemble de types est toujours écrit avant un ensemble de variables quand les deux sont présents, pour donner une idée de comment poser de telles conventions. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] Correction d’une erreur |
|
|
|
|
Administrateur
|
Mar 29 Sep 2020 17:56
Re: Les logiques : notes en vrac
Normalement, la règle de la coupure, cut [1], n’existe pas dans la déduction naturelle, seulement dans le calcul des séquents. Pourtant il semble que dans la déduction naturelle une règle dérivée nommée subst [2], peut faire penser à la règle de la coupure. Toutes les deux sont des règles structurelles (bien que l’une des deux soit dérivée).
[1] (cut) C1 ⊢ A, B1 ; C2 ⊢ A, B2 ∴ C1, C2 ⊢ B1, B2 Utilisée pour simplifier des preuves, mais il a été démontré que ce qui est démontrable en faisant usage de cette règle, est aussi démontrable sans cette règle, quoique parfois en résultant une preuve beaucoup plus longue, voir « infiniment » plus longue, presqu’au sens propre. [2] (subst) R ⊢ A ; A, B ⊢ C ∴ R, B ⊢ C Comme la règle cut, cette règle met une conséquence à la corbeille, et la retire même en plus d’un contexte où elle était copiée. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Mar 29 Sep 2020 18:06
Re: Les logiques : notes en vracHibou a écrit : […] Il n’en va pas de même avec les antécédents à gauche des séquents, qui peuvent faire référence aux conséquences à droite de séquents se trouvant plus à gauche. Un exemple tiré du précédent message : dans R ⊢ A ; A, B ⊢ C ∴ R, B ⊢ C , le second A est une copie du premier, il ne le masque pas immédiatement, seulement après. En termes d’analogie avec des fonctions imbriquées, c’est une valeur passée en paramètre d’une fonction plus interne. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Mar 29 Sep 2020 18:52
Re: Les logiques : notes en vracHibou a écrit : Normalement, la règle de la coupure, cut [1], n’existe pas dans la déduction naturelle, seulement dans le calcul des séquents. Pourtant il semble que dans la déduction naturelle une règle dérivée nommée subst [2], peut faire penser à la règle de la coupure. Toutes les deux sont des règles structurelles (bien que l’une des deux soit dérivée). Les autres règles structurelles, sont weakening — en abrégé, weak —, contraction — en abrégé, contr — et exchange — en abrégé, xch. Même une autre aperçu quelque part, mais qui n’avait pas de nom. (weak) A1, A2 ⊢ B ∴ A1, C, A2 ⊢ B A1 et/ou A2 peuvent être vides, c’est à dire absents. (contr) A1, B, B, A2 ⊢ C ∴ A1, B, A2 ⊢ C Même remarque que pour weak. (xch) A1, B1, A2, B2, A3 ⊢ C ∴ A1, B2, A2, B1, A3 ⊢ C A1 et/ou A2 et/ou A3, peuvent être vides, c’est à dire absents. (sans nom) A1, ⊤, A2 ⊢ B ∴ A1, A2 ⊢ B Ce n’est pas la lettre T majuscule, c’est le symbole ⊤, truth, U+22A4 dans Unicode. À part ça, même remarque que pour weak. Il semble que les mêmes règles valent peut‑être pour le côté droit du séquent, mais je n’en suis pas sûr ou alors peut‑être que ce sont des règles dérivées ou pas toujours valable selon les systèmes de déduction. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Mar 29 Sep 2020 19:25
Re: Les logiques : notes en vrac
Précédemment, je disais que l’ordre des éléments du contexte d’un séquent (pas l’ordre des séquents) n’est généralement pas important, et je le fondais sur justement l’une de ces règles structurelles. Il se trouve justement que certains systèmes de déduction, n’incluent pas certaines règles structurelles ou même n’en incluent aucune, et dans ce cas là, l’ordre des éléments du contexte d’un séquent, est significatif, même si je ne sais pas de quelle manière, qui doit dépendre du modèle ou de la sémantique de la logique. C’est le cas au moins pour la logique linéaire (la logique des ressources, comme elle est parfois présentée), qui accepte xch, mais n’inclut les deux autres que sous une forme restreinte : contr et weak.
Du coup, quand il est possible d’avoir des éléments du contexte en multiple exemplaires, l’interprétation des séquents comme des fonctions, ne vaut plus ou alors il faut permettre que les fonctions aient des paramètres du même nom, qui soient une copie, l’un de l’autre ou la réciproque, regroupés ou non. Ça se peut se représenter, mais en créant un type dédié et polymorphe. Un type qui ne serait plus l’ensemble d’éléments totalement distinctes (ex. type tuple ou type record), dont on peut avoir l’habitude, il faudrait y faire attention. Simplement ajouter un compteur de nombre de copies à chaque élément ne suffirait pas, si les copies ne se suivent pas toutes. Un autre problème se pose aussi : quand il est fait référence à un élément de contexte apparaissant plusieurs fois, celui de quel ordre faut‑il sélectionner ? Ou alors quand l’ordre est important, les éléments sont unique et quand leur nombre est important leur ordre ne l’est pas ? Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Mer 30 Sep 2020 10:52
Re: Les logiques : notes en vrac
Dans l’avant dernier message, je rapportais que les éléments d’un contexte, doivent au moins parfois se lire comme étant possiblement vides ou absents.
De manière assez similaire, un contexte vide peut au moins parfois se lire comme un contexte de base implicite et simplement omis pour alléger l’écriture. Mais je crois que ça ne doit être valable que pour le séquent le plus à gauche, parce que comme je le comprend, même avec un contexte vide dans un séquent suivant un autre séquent, on est quand‑même dans le contexte des séquents les plus à gauche. C’est à dire que en général, ⊢ A peut devoir se lire comme C ⊢ A où C est implicite, mais A ⊢ B ; ⊢ C, devrait se lire comme C dans le contexte A. Avec les deux cas en même temps, ⊢ A ; ⊢ B se lirait comme A dans un contexte implicite C, et B dans le contexte du premier séquent, c’est à dire ce même contexte implicite. Je dis en général, parce que ça ne me semble pas correspondre à la logique linéaire, qui logiquement (  ), ne peut que ne pas imbriquer les séquents et au lieu de ça, ne peut que créer un nouveau séquent représentant tout le contexte. À moins que ça ne puisse se représenter par des éléments de contextes qui seraient vides mais pourraient quand‑même masquer des éléments de contexte du même nom dans des contextes englobants, les supprimant de cette manière.Dans ce cas, il faut ajouter que certains séquent se dérivent en s’imbriquant aux précédents issus des conditions des inférences, mais d’autres se dérivent en se substituant au précédent (et transitivement, aux précédents, au pluriel). Ça ne devrait même pas être noté de la même manière, mais malheureusement, ça l’est. C’est quand‑même incroyable qu’il faille jouer aux devinettes avec des formalismes, qu’ils ne soient justement pas plus formellement définis et qu’ils s’écrivent de manières si ambiguës. Ceci suggère qu’il est possible qu’il reste éventuellement encore des choses à corriger ou des cas à distinguer, dans tout ce qui a été rapporté précédemment sur les séquents et leurs contextes. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
|
|
