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 : 17055
Mer 27 Mar 2019 22:54
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]
Le lambda calcul avec les types dépendants (les vrais, pas des pseudos types dépendants) […]

Par exemple un langage avec lequel il est nécessaire de démontrer que les fonctions se terminent, cependant que ce langage est dit à types dépendants, ce langage n’est pas vraiment à types dépendants, parce qu’avec de vrais types dépendants, il est impossible d’écrire le type d’une fonction qui ne se termine jamais.

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 : 17055
Mer 27 Mar 2019 23:23
Message Re: Les logiques : notes en vrac
Il existe une version relationnelle de HOL, dans ce contexte, pour la distinguer, celle dont on parle ici est appelée la version fonctionnelle de HOL.

La documentation sur le format SMT‑Lib mentionne cette différence :

smtlib.cs.uiowa.edu a écrit : 
The full language of the theory SetsRelations from Figure 3.5 has the same expressive power as higher-order logic or, more precisely, higher order simple predicate logic with primitive types. (11)

[…]

11) This is a relational version of higher-order logic, as opposed to the functional versions that are more popular in computer science.

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 : 17055
Jeu 28 Mar 2019 22:32
Message Re: Les logiques : notes en vrac
Comme son nom l’indique, le lambda calcul non‑typé n’est pas typé. Mais je me demandais quand‑même à quoi pourrait correspondre une erreur de type, dans l’évaluation d’une expression en LCNT.

Je l’imagine comme ça : l’expression n’est pas réductible ou ne l’est pas jusqu’au bout. Par exemple, si on applique une opération sur des entiers, à deux caractères, la somme par exemple, alors l’expression ne sera pas réductible et restera l’expression d’une somme de deux caractères. C’est à dire que s’il n’y a pas d’erreur de type, le type serait comme la forme normale attendue d’une expression. En disant cela, je n’exclus pas que cette forme normale soit encore réductible.

Du coup, ça définie aussi ce qu’est un type : la forme normale attendue pour une expression.

On peut noter qu’une chose peut avoir plusieurs représentations, donc plusieurs forme, et qu’un type n’est alors pas purement sémantique, il n’est qu’une question de forme. Il y a nécessairement quelque chose en commun, entre ces différentes formes. Qui dit réduire à une chose en commun, dit abstraction, ce qui amène à naturellement à l’idée d’abstraction de plusieurs types, c’est à dire à l’idée de type abstrait.

En résumé : un type est une forme non‑purement significative, un type abstrait est purement significatif, et une erreur de type, c’est une impossibilité à réduire à la forme normale définie par un type.

Quand je dis plus haut que la forme normale définie par un type, peut éventuellement être encore réductible (ce qui signifie qu’il ne faut pas toujours chercher à réduire jusqu’au bout), je pense par exemple à un type dont la forme serait l’application d’une fonction. Une telle forme qui vaut alors pour elle‑même, est encore réductible, même s’il arrivait que ce soit l’expression d’une application qui ne se termine jamais, raison de plus pour dire qu’il ne faut plus réduire dès qu’on arrive à la forme normale définie par le type. Ce qui amène à la question de choisir le bon chemin pour la réduction, s’il arrive qu’il y a plusieurs solutions possibles.

Il existe cependant un type spécial de fonction dans certains langages, qui est le constructeur de type. Les applications de ces fonctions là, sont irréductibles : l’expression vaut pour elle‑même, jamais au 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 : 17055
Jeu 28 Mar 2019 22:57
Message Re: Les logiques : notes en vrac
Si un type est une forme normale d’une expression, rien de plus, alors on peut comprendre que la sémantique du LCT soit celle du LCNT.

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 : 17055
Jeu 28 Mar 2019 22:59
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

Quand je dis plus haut que la forme normale définie par un type, peut éventuellement être encore réductible (ce qui signifie qu’il ne faut pas toujours chercher à réduire jusqu’au bout), je pense par exemple à un type dont la forme serait l’application d’une fonction. Une telle forme qui vaut alors pour elle‑même, est encore réductible, même s’il arrivait que ce soit l’expression d’une application qui ne se termine jamais, raison de plus pour dire qu’il ne faut plus réduire dès qu’on arrive à la forme normale définie par le type. Ce qui amène à la question de choisir le bon chemin pour la réduction, s’il arrive qu’il y a plusieurs solutions possibles.

[…]

Un cas tordu serait celui où une expression est déjà sous une forme trop réduite. Par exemple si la forme normale attendue est l’expression d’une somme de deux entier et qu’on a un entier, par exemple si la forme normale attendue est de la forme x + y et qu’on a 2, alors il faut marcher en arrière, par exemple créer 0 + 2 à partir de 2. Dans ce cas là aussi, il y a plusieurs solutions.

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 : 17055
Jeu 28 Mar 2019 23:01
Message Re: Les logiques : notes en vrac
Hibou a écrit : 
[…]

On peut noter qu’une chose peut avoir plusieurs représentations, donc plusieurs forme, et qu’un type n’est alors pas purement sémantique, il n’est qu’une question de forme. Il y a nécessairement quelque chose en commun, entre ces différentes formes. Qui dit réduire à une chose en commun, dit abstraction, ce qui amène à naturellement à l’idée d’abstraction de plusieurs types, c’est à dire à l’idée de type abstrait.

[…]

Parfois même, plusieurs formes en même temps. Par exemple une recherche dichotomique dans un tableau à une dimension, c’est comme voir le tableau à une dimension, comme un arbre aussi, en même temps.

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 : 17055
Ven 29 Mar 2019 14:09
Message Re: Les logiques : notes en vrac
Il semble que l’application d’une fonction, telle‑quelle, non‑réduite, n’est pas considérée comme une valeur. Je me demande pourquoi et je me demande si ça poserait un problème logique.

En tous cas, il faut lire certains précédents messages en notant ce point, parce que je supposais que l’expression de l’application d’une fonction, est une valeur.

Ça me surprend que ça ne le soit pas, j’ai toujours supposé que toute expression écrite, dans le lambda calcul, est une valeur, c’est à dire que je n’ai jamais distinguer les deux.

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 : 17055
Sam 30 Mar 2019 00:27
Message Re: Les logiques : notes en vrac
Il ne faut pas confondre “ type soundness ” et “ logical soundness ”. Un système de typage peut être cohérent, mais il peut être incohérent quand il est utilisé comme système logique.

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 : 17055
Sam 30 Mar 2019 09:59
Message Re: Les logiques : notes en vrac
Dans la terminologie HOL, “ Γ ⊢ p ” signifie « p a été prouvé sous Γ » tandis qu’en logique plus en général, la même expression signifie « p peut être prouvé sous Γ ».

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 : 17055
Sam 30 Mar 2019 10:17
Message Re: Les logiques : notes en vrac
Par convention, souvent :

  • Γ désigne un ensemble d’hypothèses (peut être vide).
  • Δ désigne un second ensemble d’hypothèses (peut être vide).
  • tₙ désigne un terme.
  • xₙ désigne une variable (substituable à un terme)
  • γₙ ou τₙ désigne un type.
  • αₙ désigne une variable de type (substituable à un type).

Image
Hibou57

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