UP | HOME

Algèbres et types inductifs

Table of Contents

1 Types abstraits de données : le point de vue algébrique

En programmation, les types abstraits de données permettent de définir des types de données

  • en spécifiant les opérations dans des interfaces,
  • en implémentatant ces spécifications par des types concrets.

Ils forment ce qu'on appelle des algèbres sur des signatures. Une signature correspond à une interface, alors qu'une algèbre correspond à une implémentation. Il est possible en Coq de représenter les algèbres, en utilisant des types inductifs et des fonctions.

2 Algèbres sur une signature

Signature := déclaration d'opérations avec leurs types (des noms)

  • S : ensemble de sortes
  • type (premier ordre) t ::= s | s -> t (sorte | type fonctionnel)
  • signature Σ ::= 0 | (op : t), Σ

Algèbre sur une signature Σ := (A, F)

  • Famille d'ensemble A := (A_s)s ∈ S
    • Interprétation d'un type dans A
      • A s := A_s
      • A (s -> t) := (A s) -> (A t) (ensemble des fonctions de (A s) vers (A t))
  • Famille de fonctions et de constantes F := (F_d)d ∈ Σ telle que si d = (op : t), alors F_d ∈ (A t)
    • Notation : F_d noté (F op) (type t implicite) ou même op lorsque F peut être deviné.

Morphisme d'algèbres sur une signature Σ : h : (A, F) -> (B, G)

  • famille de fonctions h := (h_s : (A_s -> B_s))s ∈ S vérifiant pour tout opérateur (op : s_1 -> … -> s_n -> s) de la signature :
    • ∀ x_1, …, x_n. h_s ((F op) x_1 … x_n) = (G op) ((hs_1 x_1) … (hs_n x_n))
  • Notation : h_s noté h si s peut être deviné.

    Forme abrégée mnémotechnique exprimant la propriété fondamentale d'un morphisme

    ∀ x_1, ..., x_n. h (op x_1 ... x_n) = op (h x_1) ... (h x_n)
    
  • Propriétés importantes
    • La composition des deux morphismes est un morphisme.
    • L'identité est un morphisme.

3 Exemples

(Voir le TP3.)

Entiers naturels

  • Sorte : N
  • Signature : 0 : N, S : N -> N
  • Algèbre (A, F)
    • A_N := nat (type nat de Coq)
    • F_0 := 0 (O : nat premier constructeur de nat)
    • F_S := (n : nat) => S n (S : nat -> nat second constructeur de nat)
  • Malgré leur apparence commune, 0 et S, bien noter la différence entre les symboles de la signature (des noms, des notations, sans sens) et les interprétations par des constantes ou des fonctions dans l'algèbre.
  • Plus petite algèbre (B, G) sur la même signature
    • B_N := {u} (ensemble singleton)
    • G_0 := u
    • G_S := (x : {u}) => x

Binaires

  • Grammaire avec deux non-terminaux (lecture de droite à gauche des chiffres binaires)

    N ::= 0 | T1 (N = forme normale)
    T1 ::= 1 | 0.T1 | 1.T1 (T1 = se terminant par un 1)
    
  • Signature (déduite de la grammaire, via les terminaux ou les conversions implicites):
    • O : N, fn : T1 -> N
    • 1 : T1, 0. : T1 -> T1, 1. : T1 -> T1
  • Algèbre (A, F) définie à partir du type inductif Binaire

    Inductive Binaire : SorteBinaire -> Type := (* un constructeur par opération *)
    | zeroFinal : Binaire N
    | unFinal : Binaire T1
    | double : Binaire T1 -> Binaire T1
    | successeurDouble : Binaire T1 -> Binaire T1
    | formeNormale : Binaire T1 -> Binaire N.
    
    • A_N := Binaire N (N : premier élément de SorteBinaire)
    • A_T1 := Binaire T1 (T1 : second et dernier élément de SorteBinaire)
    • F_0 := zeroFinal
    • F_fn := formeNormale
    • F_1 := unFinal
    • F_0. := double
    • F_1. := successeurDouble
  • Algèbre (B, G)
    • B_N := nat (type nat de Coq, en correspondance avec l'ensemble des binaires)
    • B_T1 := nat (type nat de Coq utiliser pour représenter les binaires se terminant par 1)
    • G_0 := 0 (0 : nat)
    • G_fn := (n : nat) => (S n) (S : nat -> nat)
    • G_1 := 0 (0 : nat)
    • G_0. := (n : nat) => 2∗ n + 1
    • G_1. := (n : nat) => 2∗ n + 2
  • Remarque. L'algèbre (B, G) a été définie de manière à être isomorphe à (A, F). Nous avons choisi d'interpréter T1 par nat et non par nat∗, défini comme nat privé de 0, pour simplifier, parce que ce type n'existe pas en Coq. C'est cependant entre nat∗ et (Binaire T1) qu'il existe un isomorphisme naturel, celui associant à un entier naturel non nul sa représentation binaire se terminant par un 1. Cependant, comme nat est naturellement isomorphe avec nat∗, en translatant d'une unité, ce choix ne pose aucun problème, bien qu'il impose de prendre en compte cet isomorphisme naturel dans les calculs, suivant le schéma ci-dessous.

    Binaire T1 -- f -> Binaire T1
       ∧                   ∧
       |                   |
       ∨                   ∨
      nat*     -- g ->    nat*
       ∧                   ∧
       |                   |
       ∨                   ∨
      nat      -- h ->    nat
    

    Si f est connu, par isomorphisme, g l'est, puis encore par isomorphisme h l'est. Prenons l'exemple de l'opération 0. sur les binaires, qui correspond à la fonction D doublant la valeur d'un entier naturel.

    Binaire T1 --  0. -> Binaire T1
       ∧                   ∧
       |                   |
       ∨                   ∨
      nat*     --  D  ->    nat*
       ∧                   |
       |+1                 |-1
       |                   ∨
      nat      -- F_0.->    nat
    

    L'interprétation F_0. est obtenue par composition des flèches : (-1) o D o (+1), soit la fonction qui à n associe 2∗ n + 1.

4 Initialité

Les deux exemples présentent pour une signature deux algèbres au statut différent. La première interprète la signature en utilisant des constructeurs : chaque élément de l'algèbre peut être vu comme un arbre étiqueté par les opérations de la signature : il s'agit de l'algèbre des termes bien typés. La seconde est différente : elle interprète les opérations de la signature par des constantes et des fonctions qui pour la plupart correspondent à des calculs et non à des constructeurs.

Une algèbre de termes est une algèbre dite initiale au sens suivant : pour toute algèbre (A, F) sur la même signature, il existe un unique morphisme d'algèbre de l'algèbre initiale vers l'algèbre (A, F).

Démonstration - Initialité de l'algèbre des termes

  • Soit Σ une signature.
  • Soit (A, F) une algèbre sur Σ. Soit l'algèbre des termes : à chaque sorte s, on associe les termes de la sorte s, à chaque opérateur op de la signature, le constructeur de termes noté aussi op.
  • Existence. On définit le morphisme h de vers (A, F) par récursion sur les termes, en utilisant la propriété fondamentale :
    • h (op x_1 … x_n) = op (h x_1) … (h x_n).
  • Unicité.
    • Soit h' un autre morphisme de vers (A, F). En utilisant la propriété fondamentale, on montre facilement par induction que pout tout terme t, h t = h' t.

On déduit de l'initialité que les algèbres initiales sur une signature Σ sont isomorphes. Soient (A, F) et (B, G) deux algèbres initiales sur Σ.

  • Il existe un unique morphisme de h_ab de (A, F) vers (B, G).
  • Il existe un unique morphisme de h_ba de (B, G) vers (A, F).
  • Par composition, h_ba o h_ab est un morphisme de (A, F) vers (A, F). Comme l'identité est un morphisme de (A, F) vers (A, F), par initialité, h_ba o h_ab est l'identité,
  • De même, h_ab o h_ba est l'identité.

Il existe donc une représentation canonique des algèbres initiales par l'algèbre des termes : toute autre algèbre initiale est isomorphe à l'algèbre des termes.

5 Initialité - L'exemple des binaires

(Voir le TP3.)

Rapellons la signature des binaires, utilisant deux sortes N et T1. Notons la Σb.

  • O : N, fn : T1 -> N
  • 1 : T1, 0. : T1 -> T1, 1. : T1 -> T1

Notons TΣb l'algèbre des termes sur cette signature, correspondant au type Binaire en Coq. Notons nat2 la seconde algèbre sur cette même signature, appelée (B, G) plus haut, et associant nat aux sortes N et T1.

On peut introduire une autre signature sur les sortes N et T1, en étendant celle sur les entiers naturels. Appelons la Σn.

  • 0 : N, S : N -> N,
  • 1 : T1, S1 : T1 -> T1

On définit l'algèbre des termes ainsi, en utilisant nat et ses constructeurs 0 et S. Notons la TΣn.

  • N := nat, T1 := nat
  • (0 : N) := (0 : nat), (S : N -> N) := (S : nat -> nat)
  • (1 : T1) := (0 : nat), (S : T1 -> T1) := (S : nat -> nat)

On peut aussi munir la famille Binaire de la structure d'algèbre sur Σn. Notons Bin2 cette algèbre.

  • N := Binaire N, T1 := Binaire T1
  • (0 : N) := (zeroFinal : Binaire N), (S : N -> N) := (successeurBin N : Binaire N -> Binaire N)
  • (1 : T1) := (unFinal : Binaire T1), (S : T1 -> T1) := (successeurBin N : Binaire N -> Binaire N)

On peut définir deux familles de fonctions BN et NB.

  • BN : TΣb -> nat2 : définition par récursion, utilisant la propriété fondamentale des morphismes sur Σb
  • NB : TΣn -> Bin2 : définition par récursion, utilisant la propriété fondamentale des morphismes sur Σn

Il est possible de montrer que BN est un morphisme non seulement sur la signature Σb mais aussi sur la signature Σn. De même, il est possible de montrer que NB est un morphisme non seulement sur la signature Σn mais aussi sur la signature Σb.

  • BN : Bin2 -> TΣn : morphisme d'algèbre sur Σn
  • NB : nat2 -> TΣb : morphisme d'algèbre sur Σb

Il est ainsi possible d'obtenir un endomorphisme sur TΣn et sur TΣb. Par initialité, ils sont égaux à l'identité. On a donc deux isomorphismes

  • entre Binaire N et nat,
  • entre Binaire T1 et nat.
TΣb -- BN -> nat2 -- NB -> TΣb : morphisme sur Σb
TΣn -- NB -> Bin2 -- BN -> TΣn : morphisme sur Σn

6 TODO Généralisation

Author: Hervé Grall
Version history: v1: 2020-02-04;.
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.