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 : 17312
Dim 10 Juin 2018 06:45
Message Re: Les logiques : notes en vrac
Une série d’articles de blog sur la théorie des catégories, appliquée à l’informatique : Category theory for programmers (bartoszmilewski.com), Bartosz Milewski, 2014.

C’est en plusieurs pages. Si la première page est longue, ce n’est pas parce que tout y est, c’est parce que chaque page se termine par une discussions dans les commentaires.

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 : 17312
Lun 11 Juin 2018 22:55
Message Re: Les logiques : notes en vrac
Il semble que ce qui est appelé kind, est le type d’un type.

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 : 17312
Mer 20 Juin 2018 23:11
Message Re: Les logiques : notes en vrac
Au cas où, attention à ne pas comprendre « imprédicatif » comme « inductif ».

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 : 17312
Dim 24 Juin 2018 18:06
Message Re: Les logiques : notes en vrac
Une proposition, c ’est un prédicat sans variable libre ou dont toutes les variables sont liées à un quantificateur : Quantification — forming propositions from predicates (cs.odu.edu).

Je dis « ou », parce que bien les deux points de vue donnent généralement une vision identique, il y a une ambiguïté sur la qualification d’un prédicat ne contenant que des constantes. Est‑ce un prédicat ou une proposition ? Il n’y a pas de variable libre, donc c’est une proposition, mais il n’y a pas de variable liées non‑plus, donc c’est un prédicat. Ce cas particulier pourrait s’appeler expression constante, mais ce serait encore ambiguë dans certains autres contexts.

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 : 17312
Jeu 28 Juin 2018 11:31
Message Re: Les logiques : notes en vrac
Je me demande s’il y a un lien entre proposition et imprédicativité.

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 : 17312
Lun 2 Juil 2018 01:03
Message Re: Les logiques : notes en vrac
Les types algébriques, n’ont pas de quantificateurs.

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 : 17312
Jeu 7 Mar 2019 21:32
Message Re: Les logiques : notes en vrac
L’axiome du choix et l’axiome de l’infini, ne sont pas considérés comme des axiomes purement logiques ; ils ne valent pas par leur forme (leur écriture) mais par leur contenu (ils sont une vue, une interprétation), c’est à dire qu’il ne sont pas purement abstraits. Ils sont pourtant assez incontournables …

C’est expliqué dans la vidéo ci‑dessous, qui au passage, rappel comment la logique est le fondement des mathématiques et non‑pas un branche des mathématiques.

Crisis in the foundation of mathematics — PBS Infinite Series — 2017

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 : 17312
Jeu 21 Mar 2019 20:12
Message Re: Les logiques : notes en vrac
HOL est une extension de la STT ; plutôt extensions au pluriel, car il existe plusieurs HOL.

Pour l’HOL la plus fondamentale, on passe de la théorie des types simples — STT — à HOL, en ajoutant à STT, l’égalité, c’est à dire la possibilité de poser l’égalité entre deux termes. L’égalité ne peut pas être posée dans le lambda calcul avec les types simples, c’est une extension de ce lambda calcul, et cette extension, donne l’HOL basique.

Quand on parle d’HOL à notre époque, c’est implicitement une HOL avec une extension supplémentaire : le typage polymorphique. L’ajout en plus du typage polymorphique, donne la variante d’HOL implémentée dans un logiciel nommé HOL4, ou même HOL tout‑court, tellement cette implémentation est considérée comme standard. Attention : HOL4 est un logiciel, HOL est une logique, bien qu’il y ait un lien entre les deux, il faut éviter d’appeler HOL4, HOL, pour ne pas entretenir la confusion.

Note : SML a un typage polymorphique, mais il ne permet pas de poser l’égalité.
 
Une autre extension encore sur la même trajectoire, donne une version d’HOl qui n’est plus nommée HOL (alors qu’elle le pourrait) : les types dépendants. L’ajout des types dépendants encore en plus, à l’HOL, donne la logique de Coq ou Twelf par exemple. Mais cette extension se fait elle‑même de manière diverse, et n’est pas standard bien que sujet de beaucoup d’intérêt.

Le format OpenTheory, pour la représentation standard de preuves en HOL, est pour une HOL du deuxième type décrit ici, c’est à dire avec le typage polymorphique. Il n’existe pas (ou je l’ignore), d’équivalent d’OpenTheory pour les HOL avec types dépendants ; que les implémentations de cette extension soit nettement divergentes ou même expérimentales, y est probablement pour quelque chose.

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 : 17312
Ven 22 Mar 2019 22:21
Message Re: Les logiques : notes en vrac
Le lambda calcul simplement typé et la théorie des types simples, ne sont pas équivalentes. Le lambda calcul simplement typé est une théorie des types, mais moins expressives que la théorie des types simples.

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 : 17312
Sam 23 Mar 2019 13:21
Message Re: Les logiques : notes en vrac
Avec un système de déduction à types polymorphes, comme l’est l’HOL courant, les preuves sont des expressions booléenne, et pour la démontrer, il faut montrer qu’elle se réduit à vrai.

Avec un système de déduction à types dépendants, comme l’est le calcul des constructions ou la théorie intuitionniste des types, une preuve est un type, et pour la démontrer, il faut montrer que le type est habité.

Image
Hibou57

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