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
|
Sam 26 Mai 2018 14:24
Re: Les logiques : notes en vrac
Il n’existe pas qu’une logique du lambda calcul, mais plusieurs. Il existe une logique pour chacune de ses variantes concernant les types. On distingue principalement :
Cette liste n’est pas exhaustive, mais le plus important y est mentionné. De plus, mais c’est moins important pour la logique je crois, il existe deux familles de typage du lambda calcul : à la Curry, “ lambda calculus with type assignment ”, où le type est explicite, et à la Church, “ type lambda calculus ”, où le type est implicite.  Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
 
|
|
|
|
|
|
Administrateur
|
Sam 26 Mai 2018 14:43
Re: Les logiques : notes en vrac
Une question que je me pose : il a été démontré depuis longtemps, que le lambda calcul non‑typé permet de représenté toutes les fonctions calculables, mais est‑ce le cas aussi des lambda calculs typés ?
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Dim 27 Mai 2018 00:21
Re: Les logiques : notes en vracHibou a écrit :
Dans la logique du premier ordre au moins, la formule S ⊨ F se lit comme ayant n’importe laquelle de ces significations :
Ce n’est pas tout à fait une conséquence dans ce cas, mais plutôt un jugement. Au passage, on a là une définition de ce qu’est un modèle. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Dim 27 Mai 2018 00:41
Re: Les logiques : notes en vrac
Appliqués dans une même logique, le calcul des séquents, la déduction naturelle et les systèmes à la Hilbert, sont équivalents pour ce qui est de la démonstrabilité, ils ne différent que par des aspects pratiques.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Dim 27 Mai 2018 22:38
Re: Les logiques : notes en vrac
Il existe une importe opposition entre sémantique dénotationnelle et sémantique opérationnelle. Même si je crois que ce qui est compréhensible dans l’une l’est aussi dans l’autre, il y doit y avoir des différences pratiques.
La sémantique opérationnelle, est celle d’une machine virtuelle, la sémantique dénotationnelle, est celle des objet mathématique. Je me demande si le lambda calcul a les deux sémantiques ou une seule des deux et laquelle. Même question pour SML. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Mai 2018 16:33
Re: Les logiques : notes en vrac
Il existe assez une opposition entre théorie des types et théorie des ensembles, d’un part, et entre théorie des catégories et théorie des ensembles, d’une autre part.
Il existe quand‑même une petite superposition entre théorie des types et théorie des ensembles. J’ignore s’il existe aussi une petite superposition entre théorie des catégories et théorie des ensembles. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Mai 2018 17:22
Re: Les logiques : notes en vrac
Je me demande si les types quotient sont considérés comme des types algébriques. Je ne crois pas, mais leur nom peut le faire penser.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Mai 2018 18:38
Re: Les logiques : notes en vrac
Un format permettant d’échanger de preuves entre des assistants de preuves, peut être vu comme un certificat de preuve. C’est le cas du format OpenTheory.
Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Lun 28 Mai 2018 22:18
Re: Les logiques : notes en vrac
Il me semble que ces quatre expressions désignent la même chose :
La première expressions, les types dépendants, est la plus répandue dans la littérature où la logique est appliquée à l’informatique. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
Administrateur
|
Mer 30 Mai 2018 17:15
Re: Les logiques : notes en vrac
Une règle des système de typage.
Si une expression E1 a un type T, si l’expression E1 peut s’évaluer en l’expression E2, alors E2 doit avoir aussi le type T (en notant qu’une expression peut éventuellement être de plusieurs types). Cette condition est requise pour qu’un système de typage soit correcte (sa soundness). C’est le principe de la préservation du type, ou type preservation. Hibou57 « La perversion de la cité commence par la fraude des mots » [Platon] |
|
|
|
|
|
|
