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 : 17523
Lun 25 Mar 2019 15:58
Message Re: Les logiques : notes en vrac
Essentiel, toujours implicite, utile à dire explicitement :

Le lambda calcul lui‑même, est un système déductif (comme tous les langages). Sa version non‑typée est incohérente (comme tous les langages non‑typés ou faiblement typés), sa version typé est cohérente.

Comme dit précédemment, le lambda calcul a en fait plusieurs versions 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 : 17523
Lun 25 Mar 2019 20:01
Message Re: Les logiques : notes en vrac
La lettre gamma majuscule, Γ, est parfois utilisée pour signifier un ensemble de prémisses ou suppositions ; la lettre delta majuscule, Δ, est parfois utilisée pour signifier un ensemble de théorèmes découlant des prémisses, comme si Γ était en haut sur un séquent et Δ en bas sur le séquent.

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 : 17523
Lun 25 Mar 2019 20:04
Message Re: Les logiques : notes en vrac
Essentiel, toujours implicite, utile à dire explicitement :

Même s’il est moins célèbre, le paradoxe du Russel est autant important que les deux théorèmes de Gödel.

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 : 17523
Lun 25 Mar 2019 20:06
Message Re: Les logiques : notes en vrac
Essentiel, toujours implicite, utile à dire explicitement :

Une preuve est une évaluation d’une expression, typiquement une réduction.

Ceci signifie qu’un calcul symbolique, un calcul exacte (ex. sans approximation numérique), sont aussi des preuves.

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 : 17523
Lun 25 Mar 2019 23:22
Message Re: Les logiques : notes en vrac
Un livre référence, sur le lambda calcul non‑typé : “ Lambda Calculus: its Syntax and Semantics ”, par Henk Barendregt. La première édition est de 1984, il y en a eu d’autres, la dernière en 1987, je crois.

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 : 17523
Lun 25 Mar 2019 23:47
Message Re: Les logiques : notes en vrac
La notation de la substitution de a par b dans e, varie selon les auteurs, de ces différentes manières :

  • E[b/a]
  • [b/a]E
  • E[a := b]
  • E[a ↦ b]
  • [a ↦ b]E

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 : 17523
Mer 27 Mar 2019 17:45
Message Re: Les logiques : notes en vrac
Le lambda calcul simplement typé, n’est pas Turing complet ; sa forme non‑typée, l’est, mais elle est inconsistante.

C’est Church aussi, qui a inventé le lambda calcul simplement typé, pas seulement le non‑typé. Il a inventé la forme typée après qu’il ait été montré que la version non‑typé est inconsistante.

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 : 17523
Mer 27 Mar 2019 21:37
Message Re: Les logiques : notes en vrac
Le lambda calcul non‑typé est inconsistant, parce qu’il permet d’exprimer des choses qui n’existent pas, sous forme de récursion infinie. Le lambda calcul avec un typage à la Hindley‑Milner, qui donne un type a toutes les expressions, est inconsistant, parce qu’il permet de donner un type non‑habité à une expression. Un type non‑habité, c’est un type de quelque chose qui n’existe pas. Typiquement, un type non‑habité, est comme avec le lambda calcul non‑typé, une récursion qui ne se termine jamais. Le typage à la Hindley‑Milner permet de poser des choses indémontrables, alors qu’un type est censé, dans la correspondance de Curry‑Howard, être l’affirmation d’une chose vraie, existante.

D’après ce que je comprend, c’est la seule cause d’inconsistance dans le lambda calcul (permettre de poser une chose dont il est impossible de démontrer qu’elle est vraie, c’est à dire poser une chose fausse). Le lambda calcul simplement typé ne souffre pas de ce problème, mais il n’est pas Turing Complet et ne permet pas d’exprimer la récursion. On peut cependant prouver qu’une récursion se termine, en utilisant une logique propre à cette finalité.

Avant de considérer que le type d’une fonction est vrai (le type de la fonction, le “ arrow type ”, pas le type renvoyé par la fonction), il faudrait d’abord définir une fonction de ce type et démontrer qu’elle se termine. Dit autrement, avant d’utiliser un type dans une inférence logique, il faudrait d’abord démontrer que le type est habité. Dit autrement encore, un type comme prémisse, devrait toujours lui‑même avoir comme prémisse, une instance de ce type ; ce qui n’est pas contradiction si on défini cette instance sans poser le type comme prémisse à ce moment là.

J’insiste sur le type d’une fonction, parce qu’en pratique, c’est avec seulement les types de fonctions que ce problème se pose.

Tout ceci vaut au moins pour tout langage dans la sémantique est exprimée en termes de lambda calcul.

Le lambda calcul avec les types dépendants (les vrais, pas des pseudos types dépendants) ne permet pas de formuler des types non‑habités, sans avoir besoin de prouver qu’une fonction de ce type se termine. Mais je trouve que les types dépendants ne sont pas commodes, qu’il est plus facile de s’exprimer avec la sémantique opérationnelle. En plus, les vrais types dépendants sont apparemment internals à implémenter dans un langage ; en fait, on ne peut pas supprimer les types à la compilation, c’est à dire que ce sont des langages typés qui ne peuvent être au mieux que aussi peu efficaces que les langages à typage dynamique.

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 : 17523
Mer 27 Mar 2019 22:46
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

J’insiste sur le type d’une fonction, parce qu’en pratique, c’est avec seulement les types de fonctions que ce problème se pose.

[…]

Parce que typiquement, on peut toujours écrire une constante, même si elle d’un type structuré.

Cependant, si on étend les types en leur ajoutant des axiomes vérifiés par les valeurs de ce type (des axiomes attachés aux types), alors le problème se pose avec tous les types, pas seulement avec les types arrow. Par exemple si on posait un type en le définissant comme étant un entier, en ajoutant l’axiome que la valeur est supérieure à 5 et inférieure à 2, on poserait un type qui ne peut pas être habité, et il faudrait exposer une constante de ce type, pour montrer que ce type est habité.

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 : 17523
Mer 27 Mar 2019 22:53
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…] Mais je trouve que les types dépendants ne sont pas commodes, qu’il est plus facile de s’exprimer avec la sémantique opérationnelle. […]

Les types dépendants, sont essentiellement des types indexés. Un exemple simple d’index, est un entier. Pour cette raison, l’exemple est souvent pris, d’un type liste dont le type est indexé par la longueur. Mais en pratique, cette catégorisation est sans intérêt, et on s’intéressera plutôt à un type liste dont la longueur est compris dans un interval. Plus encore, si on prend l’exemple d’une chaîne de caractère dont tous les mots commence par une majuscule, l’index est beaucoup moins évident et sûrement pas supporté par des languages supportant des pseudos types dépendants. Sans compter que si on catégorise parfois ce type par sa longueur, on devra avoir deux index, en fait autant d’indexe que de caractéristiques possibles, même si elles ne pas toujours importantes.

Les types dépendants sont puristes, mais pas commodes. Ils sont intéressants dans le cadre de la théorie des types, mais moins intéressants dans la cadre d’un langage, surtout quand il existe d’autres moyens de faire ce que permettent les types dépendants, comme attacher un axiome à un type ou démontrer qu’une fonction se termine.

Image
Hibou57

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