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.

Isabelle/HOL et la génération de programmes SML impératifs : notes en vrac
Auteur Message
Administrateur
Avatar de l’utilisateur
  • Genre : Télétubbie
  • Messages : 17500
Ven 18 Avr 2014 19:31
Message Isabelle/HOL et la génération de programmes SML impératifs : notes en vrac
C’est posté dans la section SML, parce que le système de preuves Isabelle est nettement orienté vers SML et aussi parce qu’il y aura dans ces notes, une orientation vers la génération de programmes SML impératifs. Comme pour le sujet des notes en vrac sur les logiques, ce seront des notes posées comme elles viennent, plus ou moins organisées, avec l’espoir de les organiser un jour. Ce sera probablement beaucoup plus désorganisé que les notes sur la logique, au moins pendant un bon bout de 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 : 17500
Ven 18 Avr 2014 19:48
Message Re: Isabelle/HOL et la génération de programmes SML impératifs : notes en vrac

Le constructeur de type 'a itself


Le constructeur de type 'a itself, est un constructeur, comme l’est, 'a list, celui qui permet de créer des types liste (par exemple int list).

Il est comme une sorte d’emballage opaque pour les types complexes ou avec paramètres (il est quand‑même utilisable avec les types simples aussi).

D’après Re: Type as argument (science.mathematics.logic.isabelle.user), ont peut le comparer à une déclaration comme datatype 'a itself = Type, déclarant simplement un constructeur (Type) sans argument.

Cette comparaison explique son usage : itself crée une constante (dans l’exemple plus haut, le constructeur Type est une constante), et ce genre de constante est nécessaire pour « encoder » un type, à la manière des tags (pensez aux tags des types dynamiques de Ada par exemple). Par exemple l’expression suivante est valide : (nat itself) = (nat itself), elle est de type bool et son évaluation donne True, tandis que ceci n’est pas une expression valide : nat = nat.

Ceci est suffisant, mais pour ajouter quelques banalités au cas où elles seraient nécessaires, quelques remarques supplémentaires…

Par exemple nat list itself est un type sans paramètres, et qui est différent du type nat list, et c’est important à noter. Par exemple [0]:nat list est correcte, mais [0]:nat list itself ne l’est pas, parce que [0] est du type nat list et non‑pas du type nat list itself. Bien que (nat itself) = (nat itself) soit une expression valide, (nat itself) = (int itself) ne l’est pas, car nat itself et int itself sont deux constantes de deux types différents.

Je ne sais pas s’il existe un moyen de créer une constante de type 'a itself à partir d’une constate de type 'a, ni même si cela a un sens formel ou pratique.

Il peut recevoir en paramètre, une variable de type, il n’est pas obligatoire de lui fournir un type concret. Par exemple 'a itself est valide autant que l’est nat itself.

Image
Hibou57

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