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 : 15407
Sam 26 Mai 2018 14:24
Message 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 :

  • Lambda calcul non‑typé, qui donne la logique des propositions du premier ordre, FOL ;
  • simplement typé, qui donne la logique d’ordre supérieur, HOL ;
  • simplement typé avec fixed‑point combinator (je ne sais pas comment on le traduit en français) ;
  • typé avec polymorphisme (System F) ;
  • typé avec polymorphisme d’ordre supérieur (System Fω).

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.

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 : 15407
Sam 26 Mai 2018 14:43
Message 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 ?

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 : 15407
Dim 27 Mai 2018 00:21
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
Hibou a écrit : 
Turnstile (⊢, c’est quoi son nom français ?) vs entailment (⊨, c’est quoi son nom français ?) vs implication ;

⊢ s’applique à la syntaxe, et ⊨ s’applique à la sémantique. C’est déjà une différence claire entre les deux. Tous deux sont des conséquences : conséquence syntaxique pour le ⊢ et conséquence sémantique pour le ⊨. L’implication ⇒ (parfois notée ⊃ ou encore parfois assez mal notée →), est un opérateur du calcul des propositions.

[…]

Dans la logique du premier ordre au moins, la formule S ⊨ F se lit comme ayant n’importe laquelle de ces significations :

  • F est vrai dans S ;
  • S satisfait F ;
  • S est un modèle de F.

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.

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 : 15407
Dim 27 Mai 2018 00:41
Message 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.

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 : 15407
Dim 27 Mai 2018 22:38
Message 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.

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 : 15407
Lun 28 Mai 2018 16:33
Message 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.

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 : 15407
Lun 28 Mai 2018 17:22
Message 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.

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 : 15407
Lun 28 Mai 2018 18:38
Message 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.

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 : 15407
Lun 28 Mai 2018 22:18
Message Re: Les logiques : notes en vrac
Il me semble que ces quatre expressions désignent la même chose :

  • Dependent types theory, DTT (théorie des types dépendants) ;
  • Martin‑Löf type theory, MLTT (théorie des types de Martin‑Löf) ;
  • Constructive type theory, CTT (théorie constructive des types) ;
  • Intuitionistic type theory, ITT (théorie intuitioniste des types).

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.

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 : 15407
Mer 30 Mai 2018 17:15
Message 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.

Image
Hibou57

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