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.

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.