Download Initiation à l`algorithmique

4.6. ANNEXES
4.6
4.6.1
193
Annexes
Type abstrait de données
Nous nous intéressons ici à une description plus formelle du type abstrait de données Sequence
selon un formalisme logique inspiré de [13]. On notera B l’ensemble des booléens ({0, 1}), E
l’ensemble des éléments, S l’ensemble des séquences, F l’ensemble des fonctions E → E et P
l’ensemble des fonctions E → B. Le vocabulaire initial de la théorie des séquences comprend
alors :
– une constante [] qui représente la séquence vide (on notera S∗ = S − {[]}) ;
– un opérateur x ◦ s qui traduit l’insertion d’un élément x ∈ E en tête de la séquence s ∈ S.
Dans ce cadre, la définition axiomatique des séquences repose sur les 2 axiomes suivants :
1. [] est une séquence : [] ∈ S,
2. x ◦ s est une séquence : ∀x ∈ E, ∀s ∈ S, x ◦ s ∈ S.
Pour chaque opération considérée, nous indiquerons sa signature, sa définition axiomatique
(souvent récursive) et son équivalent Python.
– head(s) : tête (premier élément) d’une séquence
head : S∗ → E
, x = head(x ◦ s)
s[0]
– tail(s) : queue d’une séquence (la séquence sans son premier élément)
tail : S∗ → E
, s = tail(x ◦ s)
s[1:len(s)]
– x in s : appartenance d’un
élément à une séquence
x = head(s)
in
: E × S → B , x in s
x in tail(s)
– len(s) : longueur d’une séquence (nombre d’éléments)
len([]) = 0
len
:S→N
, len(x ◦ s) = len(s) + 1
len(s)
– concat(s1 , s2 ) (ou s1 + s2 ) : concaténation de deux séquences
[] + s = s
concat: S × S → S , s1 + s2
s3 = (x ◦ s1 ) + s2 = x ◦ (s1 + s2 )
ème
– ith(s, i) (ou si ) : i
élément
de la séquence
(x
◦
s)
0 =x
ith
: S∗ × N → E , (x ◦ s)i = si−1 0 < i ≤ len(s)
s[i]