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
|
Lun 7 Juil 2014 10:07
Re: Les logiques : notes en vracHibou a écrit : Il a surtout été question de HOL, à cause de la correspondance de Curry‑Howard, dont découle directement cette logique (HOL, c’est typiquement un modèle du lambda calcul simplement typé). Mais ce n’est pas la seule, il existe le Calcul des Construction (Calculus of Construction — CoC), sur lequel repose le système de démonstration Coq. Quoique qu’il me semble que la correspondance Curry‑Howard est plus claire avec Coq qu’avec HOL. Avec Coq, un type est clairement une proposition ou une affirmation, le résultat d’une fonction est plus directement et plus clairement une preuve, et une fonction est plus clairement une démonstration. Je me demande s’il est possible de rendre ces choses autant explicites avec les systèmes HOL (et je pense surtout à Isabelle/HOL) qu’elles le sont avec Coq.  Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
 
|
|
|
|
|
|
Administrateur
|
Mar 22 Juil 2014 15:31
Re: Les logiques : notes en vrac
Relations entre axiome, syntaxe, sémantique et preuve.
Ce message débroussaille quelque définitions. Ce message souligne aussi l’importance de la syntaxe dans les langages formelles. La syntaxe n’est pas une futilité à prendre à le légère, elle a une interprétation. Les règles syntaxiques, sont des axiomes. Des règles syntaxiques, on peut en effet conclure des choses, comme l’existence possible ou pas de certaines expressions. Les règles de réécriture, sont des règles d’inférences. C’est une conséquence du point précédent. Il devrait être facile de comprendre que si une chose, première, peut être réécrite comme une autre, seconde, alors ce qui peut être dit de la seconde peut aussi être dit de la première. Une preuve peut être syntaxique. C’est une conséquence du point précédent. Les lemmes sont des théorèmes. Ce sont deux quasi‑synonymes, et ce qui les distingue, ce n’est que l’emphase portée par le mot « théorème », qui est employé plutôt que le mot « lemme », quand on veut souligner l’importance. Les axiomes sont des théorèmes par à‑priori. Les axiomes sont des points de départ, parce qu’il en faut nécessairement au moins un. Ce sont des théorèmes sans preuves, mais ils peuvent être démontrables (un axiome n’est pas un théorème indémontrable). Les axiomes sont parfois des théorèmes. C’est une conséquence du point précédent. Tout autant, il est possible d’appeler un théorème, un axiome, dans le cas où on ne se soucie par de sa preuve, ou si on ne la connait pas, même en sachant qu’elle existe. Les règles d’inférences sont un type particulier d’axiome/théorème. Et souvent les logiciens traitent les règles d’inférences comme des axiomes/théorèmes. Quand on démontre un lemme/théorème, il se peut que ce soit une règle d’inférence. La différence entre les deux est d’ordre pratique (comparable à, mais plus forte, que la différence entre lemme et théorème), et n’est pas de la même nature que la différence entre axiome et théorème, une différence qui peut être formelle. Les interprétations donnent lieu à des axiomes/règles d’inférences. Ce qu’on peut dire d’une chose, peut dépendre de l’interprétation que l’on en fait. En attente : relation entre sémantique et interprétation… même chose ou pas ? (je rééditerai ce message quand je connaitrai la réponse) |
|
|
|
|
Administrateur
|
Mer 23 Juil 2014 01:59
Re: Les logiques : notes en vrac
Le lambda‑calcul a son axiomatisation et règles d’inférence (on peut même le dire au pluriel); il n’en est pas pour autant un système de déduction valable.
Ce système de calcul, comme système de déduction, n’est pas correcte (sound). C’est démontré par l’existence d’un type de fonction nommée « combinateur de point‑fixe » (fixed‑point combinator), dont l’interprétation serait un paradoxe. Ce sera peut‑être explicité un autre jour. |
|
|
|
|
Administrateur
|
Mer 23 Juil 2014 17:50
Re: Les logiques : notes en vrac
J’ajoute à la liste du premier message « notation / dénotation ».
|
|
|
|
|
Administrateur
|
Mer 23 Juil 2014 23:45
Re: Les logiques : notes en vrac
À propos de correction et complétude (soundness, completeness) des systèmes de déduction, une formulation simple et correcte.
CS152: Programming Languages — Lecture 9 — Simply Typed Lambda Calculus (cs.washington.edu) [pdf]. Dan Grossman, printemps 2011. À la page étiquetée 12 (indexée 19). Citation : A sound type system never accepts a program that can get stuck Pour un système de déduction validant une preuve, la correction, c’est de ne jamais donner de faux négatif — il permet pas de faire passer le faux pour vrai; la complétude c’est de ne jamais donner de faux positifs — il ne permet pas de faire passer le vrai pour faux. Mais il y a une autre définition plus claire pour la complétude, qui est celle que tout énoncé vrai doit être démontrable (et cette incapacité à démontrer n’est pas toujours le fait de faire passer un énoncé vrai pour faux). Rappel. Un des théorèmes de Gödel (démontré), dit qu’on doit parfois faire le choix entre les deux et qu’on ne peut pas toujours avoir les deux en même temps, qu’on doit parfois choisir : soit la correction, soit la complétude. |
|
|
|
|
Administrateur
|
Ven 25 Juil 2014 20:48
Re: Les logiques : notes en vrac
La théorie des types (les théories, en fait), est une alternative à la théorie des ensembles, pour les fondements des mathématiques.
Type theory (en.wikipedia.org) Wikipédia a écrit : In mathematics, logic, and computer science, a type theory is any of a class of formal systems, some of which can serve as alternatives to set theory as a foundation for all mathematics. Traduction a écrit : En mathématiques, logique et science informatique, une théorie des types est n’importe laquelle d’une classe de systèmes formels, dont certains peuvent servir d’alternative à la théorie des ensemble pour toutes les mathématiques. Je ne trouve pas la phrase claire en tout point, mais la partie qui me semble importante, est claire : les théories des types, sont des alternatives aux théories des ensembles. |
|
|
|
|
Administrateur
|
Ven 25 Juil 2014 22:06
Re: Les logiques : notes en vrac
Dans Brouwer‑Heyting‑Kolmogorov interpretation (en.wikipedia.org), une interprétation intéressante d’un des théorèmes d’incomplétude de Gödel.
Wikipédia a écrit : It is not in general possible for a logical system to have a formal negation operator such that there is a proof of "not" P exactly when there isn't a proof of P ; see Gödel's incompleteness theorems. Traduction a écrit :
Il n’est en général pas possible, pour un système logique, d’avoir un opérateur pour une négation formelle, tel qu’il existe une preuve de non‑P précisément quand il n’existe pas de preuve de P; voir les théorèmes d’incomplétude de Gödel. |
|
|
|
|
Administrateur
|
Sam 26 Juil 2014 16:06
Re: Les logiques : notes en vrac
Anecdote sur le vocabulaire.
L’équivalent du français CQFD — « Ce Qu’il Fallait Démontrer », se dit en Anglais, QED — Quod Erat Demonstrandum, qui est du latin (!) et que les Anglais traduisent par “which had to be desmontraded”… les Anglophone utilisent donc un acronyme d’une expression latine pour leur équivalent du CQFD. |
|
|
|
|
Administrateur
|
Sam 26 Juil 2014 21:47
Re: Les logiques : notes en vracHibou a écrit : Le lambda‑calcul a son axiomatisation et règles d’inférence (on peut même le dire au pluriel); il n’en est pas pour autant un système de déduction valable. Il y a deux choses à dire ici. D’abord expliquer le paradoxe présenté, et ensuite donner une bonne nouvelle, qui est que le lambda‑calcul typé peut être un système de déduction valide, à travers ses règles décrivant les types et associations de types valides. Le paradoxe, c’est le Paradoxe de Curry. Je ne trouve pas de référence philosophique en français, alors j’en ai choisi une en Anglais. Curry's Paradox (plato.stanford.edu). 2001‑2008. Université de Stanford a écrit : Curry's Paradox Traduction a écrit : Le Paradoxe de Curry Quel est la formulation pratique du paradoxe de Curry, qui est mentionné ici comme un contributeur plus du lambda‑calcul que de la philosophie (qui est cependant concernée) ? Voir cette formule en SML pour comprendre : Code :fun fix f x = (f (fix f)) x Cette fonction particulière, qui est ce qui en mathématique, s’appel un combinateur de point fixe, vérifie cette égalité : fix(f) = f (fix(f)), ou en notion SML, fix f = f (fix f). On peut poursuivre récursivement : fix(f) = f (fix(f)), et donc = f (f (fix(f))) et donc = f (f (f (fix(f)))), etc… À quoi peut‑elle bien servir ? À définir la récursivité, justement. Le rec, en SML, n’est rien d’autre que ce combinateur de point fixe. Maintenant voyons cette formule en lambda‑calcul : Code :λf. (λx. f (x x)) (λx. f (x x)) C’est la fonction λf. (λx. f (x x)), à laquelle est appliqué l’argument (λx. f (x x)), et qui renvoie une fonction. Notez que l’argument et l’expression de la fonction, sont identiques, ce qui fait penser à la récursivité, déjà. Posant Y = λf. (λx. f (x x)) (λx. f (x x)) Partant de Y g, on a les égalités successives suivantes : 1: Y g = 2: λf. (λx. f (x x)) (λx. f (x x)) g = -- Expansion de Y 3: (λf. (λx. f (x x)) (λx. f (x x))) g = -- Ajout de parenthèses pour rendre plus clair 4: ((λx. g (x x)) (λx. g (x x))) = -- Application et substitution [g / f] 5: g ((λx. g (x x)) (λx. g (x x))) = -- Application et substitution [(λx. g(x x)) / x] Ors, d’après (4), on sait que Y g = ((λx. g (x x)) (λx. g (x x))), donc (5) peut se réécrire : 6: g (Y g) On a Y g = g (Y g) L’application de la formule λf. (λx. f (x x)) (λx. f (x x)), nommée Y, se réduit à la même égalité que l’application de la fonction SML précédente, nommée fix. Ors la formule λf. (λx. f (x x)) (λx. f (x x)) n’a pas toujours de sens, car pour pouvoir se réduire à quelque chose de valide, il faut que x soit une fonction. Le typage aurait interdit d’instancier cette formule pour n’importe quel argument, en exigeant que x soit de type fonction (ou arrow type). Pour cette raison, le lambda‑calcul non‑typé n’est pas un système de déduction valide. Il l’est, lorsqu’il est typé — et seulement les types sont interprétables ! — et cela a été démontré, pour divers système de types, dont le lambda‑calcul simplement typé (qui n’est pas celui de SML, j’y reviendrai…). |
|
|
|
|
Administrateur
|
Dim 27 Juil 2014 01:11
Re: Les logiques : notes en vrac
J’ajoute à la liste du premier message, « sémantique vs interprétation ».
La sémantique fait penser au sens, et pour cette raison, peut être confondue avec l’interprétation. Elles sont deux choses différentes. La sémantique est interne, l’interprétation est externe. La sémantique, c’est tout ce qui dérive de l’écriture et qui n’est pas apparent dans l’écriture (ou pas directement apparent). L’interprétation est inaccessible à la sémantique, mais la sémantique est accessible à l’interprétation, autant d’ailleurs que lui sont accessibles l’écriture et sa syntaxe. Bref, la sémantique n’est pas l’aboutissement, c’est l’interprétation qui l’est, et qui fait sens en pratique. |
|
|
|
|
|
|
