Cours

Notes de cours Module Informatique 2 Deug Sciences mention MIAS Sp´ecification et construction d’algorithmes : Approche fonctionnelle 1 Alain H´eaulm´e, Christophe Mauras, Ren´e Thoraval Universit´e de Nantes, Facult´e des Sciences, D´epartement d’Informatique

12 janvier 19952

1 2

Disponible ` a l’adresse : http://www.sciences.univ-nantes.fr/info/enseignement/deug/info2/cours.html Derni`ere mise ` a jour : janvier 2000

2

Table des mati` eres 1 Introduction

5

2 Concepts de base 2.1 Expressions, Valeurs, Types . . . . 2.1.1 D´efinitions . . . . . . . . . 2.1.2 En Caml . . . . . . . . . . 2.1.3 En Pascal . . . . . . . . . . 2.2 Fonctions, composition, application 2.2.1 D´efinitions . . . . . . . . . 2.2.2 En Caml . . . . . . . . . . 2.2.3 En Pascal . . . . . . . . . . 2.3 M´ethodologie . . . . . . . . . . . . 2.3.1 Sp´ecification . . . . . . . . 2.3.2 Analyse Descendante . . . . 2.4 R´ecursivit´e . . . . . . . . . . . . . 2.4.1 Principes . . . . . . . . . . 2.4.2 En Caml . . . . . . . . . . 2.4.3 En Pascal . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

. . . . . . . . . . . . . . .

7 7 7 9 10 10 10 11 12 13 13 14 16 16 17 18

3 Types et structures de donn´ ees 3.1 Abstraire les donn´ees . . . . . . 3.2 Types construits . . . . . . . . 3.2.1 En Caml . . . . . . . . 3.2.2 En Pascal . . . . . . . . 3.3 Listes . . . . . . . . . . . . . . 3.3.1 G´en´eralit´es . . . . . . . 3.3.2 En Caml . . . . . . . . 3.3.3 En Pascal . . . . . . . . 3.4 Un exemple : le type arbre . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

. . . . . . . . .

21 21 23 24 27 29 29 30 31 32

4 Ordre Sup´ erieur 4.1 Abstraire par les fonctions . . . . 4.2 Programmation d’ordre sup´erieur 4.2.1 En Caml . . . . . . . . . 4.2.2 En Pascal . . . . . . . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

. . . .

35 35 36 36 39

Preuves de programmes 5.1 El´ements de Logique . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Induction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Preuves et transformations de programmes . . . . . . . . . . . . . . . . . . . . . .

41 41 43 45

5

3

4

` TABLE DES MATIERES

6 Conclusion

49

A Syntaxe simplifi´ ee du langage Caml

51

Chapitre 1

Introduction Le cours du module Informatique 2, dispens´e en 1`ere ann´ee de Deug Sciences option MIAS (Math´ematiques, Informatique et Applications aux Sciences) `a l’Universit´e de Nantes, est consacr´e `a la sp´ecification et ` a la construction d’algorithmes, en suivant une approche fonctionnelle. Les ouvrages de r´ef´erence sont [SFLM93] pour l’aspect algorithmique et [WL99] pour l’aspect programmation. On pourra aussi utilement consulter [HHDGV92, AS89, Xuo92]. Cet enseignement a pour objectifs : – d’apprendre – `a mod´eliser des probl`emes, – `a utiliser une m´ethode pour les r´esoudre (sp´ecifier, r´ealiser, coder, analyser et prouver) ; – de donner – une formation de base en algorithmique et programmation, `a laquelle le module Informatique 1 a d´ej` a contribu´e, – une pratique d’un langage fonctionnel : Caml, associ´ee `a des compl´ements sur un langage imp´eratif : Pascal. Les pr´erequis de ce cours sont la pratique d’un langage imp´eratif, par exemple Pascal tel qu’il est pr´esent´e dans le module Informatique 1. Ce document est structur´e pour amener le lecteur `a assimiler les notions progressivement, en partant d’exemples simples et en allant peu `a peu vers davantage d’abstraction : – d’abord, il pr´esente l’ensemble des notions de base permettant de sp´ecifier puis de programmer des solutions ` a des probl`emes relativement simples (chapitre 2) ; – puis, il introduit des m´ecanismes d’abstraction permettant de concevoir des algorithmes plus complexes et plus g´en´eraux : – abstraction portant sur les informations (chapitre 3), – abstraction portant sur les fonctions (chapitre 4). Le document propose ensuite une r´eflexion sur l’activit´e qu’est la programmation, en donnant des outils th´eoriques pour prouver et transformer des programmes (chapitre 5). Enfin, la conclusion (chapitre 6) est suivie d’une d´efinition de la syntaxe du sous-ensemble du langage Caml consid´er´e dans le module (annexe A).

5

6

CHAPITRE 1. INTRODUCTION

Chapitre 2

Concepts de base 2.1 2.1.1

Expressions, Valeurs, Types D´ efinitions

L’analyse d’un probl`eme ` a r´esoudre en informatique am`ene `a mettre en ´evidence les informations dont on dispose, et les informations que l’on souhaite calculer. Ces informations peuvent ˆetre de diff´erente nature : par exemple des nombres r´eels repr´esentant des mesures physiques, des nombres entiers, rationnels (au sens math´ematique : N, Z, Q), un mot ou une phrase saisi par l’utilisateur, une suite de rationnels d´ecrivant les coefficients d’un polynˆ ome, des heures, des dates... ou toute combinaison plus complexe par exemple une suite, un ensemble, un couple d’informations d’une des formes ci-dessus. Valeurs : En informatique, on appellera valeur toute information donn´ee ou qui a ´et´e calcul´ee. Par exemple : 1, 3.1415926536, 22/7 sont des valeurs (respectivement enti`ere, d´ecimale et fractionnaire). (3, 4) est une valeur dans N 2 . Types : La n´ecessit´e de repr´esenter ces valeurs dans un format interne pour une machine (dont on ne parlera pas dans ce cours), oblige ` a pr´eciser l’ensemble auquel appartient une valeur (tout simplement parce que dans un certain codage, la touche A est repr´esent´ee par le code 01000001, et que dans un autre codage le nombre 65 est aussi repr´esent´e par le code 01000001 : il faut pouvoir distinguer les deux). De plus, une r´esolution particuli`ere d’un probl`eme peut s’appliquer `a un certain ensemble de valeurs et ne pas s’appliquer pour un autre. Par exemple la division euclidienne est d´efinie pour les polynˆ omes sur Q, mais pas pour les polynˆ omes sur Z. Ces deux raisons motivent la notion de type en informatique. D´ efinition : On appelera type un ensemble de valeurs. Un ensemble de valeurs a un int´erˆet particulier d`es lors qu’il permet d’identifier l’ensemble des valeurs auxquelles on peut appliquer une certaine op´eration. Par exemple, le fait que + soit une loi de composition interne sur Z, contribue `a l’int´erˆet du type des entiers relatifs. On utilisera donc comme types, des ensembles de valeurs munis d’op´erations permettant de calculer le r´esultat attendu (une valeur), ` a partir des donn´ees dont on dispose (des valeurs). Les types (dits de base), que l’on retrouve dans quasiment tous les langages informatiques, et que l’on utilisera donc dans l’´ecriture d’algorithmes sont les suivants : Le type entier qui regroupe en fait les entiers relatifs. On utilise peu les entiers naturels, car les op´erations fournies dans la plupart des langages s’appliquent sur les entiers relatifs (ne pas 7

8

Le Le

Le

Le

CHAPITRE 2. CONCEPTS DE BASE oublier qu’au moment de l’ex´ecution sur une machine le type entier (=Z) sera r´eduit `a un intervalle d’entiers). type r´ eel contient les nombre r´eels. La plupart des langages n’offrent des r´eels, que le sousensemble des d´ecimaux (` a virgule fixe ou flottante), avec une pr´ecision limit´ee. type caract` ere est un ensemble de caract`eres typographiques correspondant (plus ou moins) `a l’ensemble des touches du clavier. Ce type est n´ecessaire car c’est l’ensemble des “valeurs ´el´ementaires” (une touche) que l’utilisateur peut entrer au clavier. type chaˆıne est l’ensemble des suites de caract`eres : une valeur de ce type peut donc ˆetre une phrase. On doit noter caract`eres et chaˆınes entre ’ ou “ pour dire que l’on parle du caract`ere ou de la chaˆıne en tant que tel, et les distinguer des autres mots ou lettres figurant dans un algorithme. type bool´ een est l’ensemble {vrai, faux}. Cet ensemble riche par sa structure alg`ebrique (treillis, alg`ebre de Boole) est fondamental en informatique car il permet d’exprimer comment et dans quel cas un calcul doit d´ependre ou non du r´esultat d’autres calculs et des donn´ees.

Expressions : On appelle expression une forme symbolique, contenant des valeurs et des op´erateurs servant ` a exprimer une nouvelle valeur. Exemples : 1 + 1/1! + 1/2!, faux ou (3*4 = 0) sont des expressions. Toute expression a un type qui d´etermine l’ensemble dans lequel elle prend sa valeur. La premi`ere expression est de type r´eel, la seconde de type bool´een. La forme d’une expression suffit `a d´efinir son type qui d´epend de la d´efinition de l’op´erateur le plus global, et du types de ses op´erandes...qui d´ependent eux mˆemes de leur op´erateur et op´erandes... Evaluer une expression consiste ` a calculer sa valeur. La valeur du premier exemple est 2.5 ; celle du second est faux. On utilisera dans les algorithmes toute notation math´ematique usuelle pour noter les expressions. En particulier on notera f(x) le r´esultat d’une fonction f appliqu´ee `a une valeur x. On distinguera : – les op´erateurs arithm´etiques (entiers et/ou r´eels) : +, −, ∗, /, a mod b, a div b, cos, sin, xy , ln, exp ... – les op´erateurs bool´eens : ou, et, non. – les op´erateurs relationnels : =, <, >, 6=, ≤, ≥ (pour entiers, r´eels, caract`eres et chaˆınes). – l’op´erateur de concat´enation de caract`eres et chaˆınes de caract`eres : &. – l’expression alternative : si expression bool´eenne alors expression sinonexpression – l’expression de choix selon des valeurs : selon selecteur dans valeur : expression ... – l’expression de choix suivant des conditions : suivant expression bool´eenne : expression ... Les expressions alternatives et de choix ont une valeur : la valeur de l’expression correspondant `a la valeur du s´electeur ou ` a la condition vraie (qui doit ˆetre unique). Les expressions de choix peuvent comporter un choix autrement. Exemple : L’expression suivante calcule le signe du produit x * y. selon ((si x > 0 alors 1 sinon si x = 0 alors 0 sinon -1) * (suivant y > 0 : 1 y = 0 : 0 y < 0 : -1)) dans 1 : ’+’ 0 : ’0’ -1 : ’-’

2.1. EXPRESSIONS, VALEURS, TYPES

9

D´ efinition locale Pour ´ecrire des expressions de mani`ere symbolique et pour ´eviter d’´ecrire deux fois la mˆeme sous expression, on introduit la notion de d´efinition locale. Cela consiste `a nommer la valeur d’une sous-expression, et ` a utiliser ce nom dans l’expression. Exemple : L’expression soit y = cos (3.1416 * 12) dans y + 1/(2 y^2) est ´equivalent ` a : cos (3.1416 * 12) + 1/(2 (cos (3.1416 * 12))^2)

2.1.2

En Caml

Le langage Caml permet d’´ecrire des expressions et de connaˆıtre leur type et leur valeur. L’utilisation du langage se fait par interaction constante entre l’utilisateur et le syst`eme : l’utilisateur soumet une expression qui est alors typ´ee et ´evalu´ee. La plupart des expressions vues ci-dessus ont une traduction directe en Caml. Il convient cependant de distinguer les op´erations enti`eres des op´erations sur les flottants. #12 + 8;; - : int = 20 #if (6 = 7) then "oui" else "non";; - : string = "non" #true or false & (4 = 5);; - : bool = true #let y = cos (3.1416 *. 12.0) #in y +. (1.0 /. (2.0 *. y *. y)) ;; - : float = 1.5 #let x = -3 and y = 9 in #match ((if x > 0 then 1 # else if x = 0 then 0 # else -1) * (if y > 0 then 1 # else if y = 0 then 0 # else -1)) #with 1 -> ‘+‘ # | 0 -> ‘0‘ # | -1 -> ‘-‘ ;; Entr´ ee interactive: >match ((if x > 0 then 1 > else if x = 0 then 0 > else -1) * (if y > 0 then 1 > else if y = 0 then 0 > else -1)) >with 1 -> ‘+‘ > | 0 -> ‘0‘ > | -1 -> ‘-‘... Attention: ce filtrage n’est pas exhaustif. - : char = ‘-‘ Une session Caml consiste ` a soumettre au syst`eme une suite de phrases, apr`es le symbole de disponibilit´e #. Une phrase peut ˆetre soit une expression, soit une d´efinition globale, termin´ee dans les deux cas par ; ; Une d´efinition globale let x = <expression> permet de donner une valeur `a l’identificateur x pour toute la suite de la session.

10

CHAPITRE 2. CONCEPTS DE BASE

#let x = 5 + 2;; x : int = 7 #x;; - : int = 7 #let y = x + 1;; y : int = 8

2.1.3

En Pascal

Pour toutes les expressions simples, la traduction en Pascal a ´et´e vue dans le module Informatique 1. Les expressions alternatives et de choix n’ont pas de traduction directe en Pascal. On peut utiliser les instructions alternatives et de choix, en mettant dans chaque cas une instruction d’affectation `a la mˆeme variable. De mˆeme la d´efinition locale n’existe pas en Pascal , mais peut ˆetre traduite par une variable locale suppl´ementaire et une affectation.

2.2 2.2.1

Fonctions, composition, application D´ efinitions

Les expressions sont les briques de base qui permettent d’´ecrire la valeur d’un r´esultat en utilisant des op´erateurs et les valeurs donn´ees d’un probl`eme. Pour d´ecrire de fa¸con g´en´erale, l’obtention d’un r´esultat d´ependant de donn´ees inconnues, on a recours `a la notion de fonction. Cela va permettre d’´ecrire des expressions d´ependant d’inconnues que l’on appelera param`etres de la fonction. D´ efinition : Une fonction en informatique est d´efinie par la donn´ee de : – son nom – le N-uplet de ses param`etres (noms arbitraires que l’on donne aux donn´ees inconnues) – le produit cart´esien des types des param`etres (le domaine ou ensemble de d´epart), – le produit cart´esien des types des sorties (le co-domaine ou ensemble d’arriv´ee), – un P-uplet d’expressions calculant les valeurs des sorties en fonction des param`etres. Remarque : Le nom d’une fonction ne sert pas (et pourrait ˆetre supprim´e de la d´efinition cidessus) `a d´efinir son comportement, sauf dans le cas de fonctions r´ecursives (voir 2.4.1). Le nom sert seulement ` a nommer une fonction pour pouvoir l’utiliser ailleurs qu’` a l’endroit o` u elle est d´efinie. De nombreux langages (dont Caml) permettent de d´efinir des fonctions sans leur donner de nom. Exemple : On veut ´ecrire une fonction calculant le produit scalaire de deux vecteurs u et v dans R2 connaissant leurs coordonn´ees u1,u2, v1 et v2. fonction produit_scalaire : reel x reel x reel x reel -> reel u1, u2, v1, v2 -> u1 * v1 + u2 * v2 Remarque : ´ecrirait :

Cette notation se veut proche de la notation de fonction en math´ematiques o` u l’on

. : R x R x R x R -> R u1, u2, v1, v2 -> u1 * v1 + u2 * v2

2.2. FONCTIONS, COMPOSITION, APPLICATION

11

Application : L’application d’une fonction consiste `a fournir des valeurs d’entr´ee `a cette fonction. Le r´esultat de cette application de fonction est un P-uplet de valeurs, obtenues en rempla¸cant les param`etres par les valeurs fournies en entr´ee. On notera l’application d’une fonction f `a une donn´ee x par f(x). C’est ainsi que l’on utilise une fonction. Exemple : produit_scalaire (1, 0, 2.5, 3) Ecrivons maintenant une fonction orthogonaux utilisant les mˆemes param`etres et donnant un r´esultat bool´een, vrai si et seulement si les deux vecteurs sont orthogonaux. fonction orthogonaux : reel x reel x reel x reel -> booleen u1, u2, v1, v2 -> produit_scalaire(u1,u2,v1,v2) = 0 Composition : La composition de fonctions est l’application d’une fonction au r´esultat d’une application d’une autre fonction. Pour qu’une composition soit correcte, il faut v´erifier que les types des sorties de la premi`ere correspondent aux types des entr´ees de la seconde. Cette notion fondamentale en math´ematiques est aussi fort utile en informatique car elle permet de d´ecrire des calculs complexes en utilisant au mieux les fonctions d´ej`a d´efinies. Exemple : Si on dispose d’une fonction racine : reel -> reel alors on peut ´ecrire la fonction norme : fonction norme : reel x reel -> reel u1, u2 -> racine (produit_scalaire(u1,u2,u1,u2))

2.2.2

En Caml

En Caml, on peut traduire les fonctions-algorithmes pr´ec´edentes par des expressions de la forme suivante : function (par1, par2,...) -> (exp1, exp2, ...) On peut entrer simplement une fonction comme cela ; elle sera, comme toute expression, typ´ee, mais n’a pas encore de valeur : #function u1, u2, v1, v2 -> u1 *. v1 +. u2 *. v2 ;; - : float * float * float * float -> float = On peut l’´evaluer sur un exemple : #(function u1, u2, v1, v2 -> u1 *. v1 +. u2 *. v2) # (1.0, 2.0, 5.5, 4.5) ;; - : float = 14.5 Mais le plus pratique est d’inclure cette fonction dans une d´efinition globale qui permet de la nommer, et de l’utiliser ensuite pendant toute la session. #let produit_scalaire = function # u1, u2, v1, v2 -> u1 *. v1 +. u2 *. v2 ;; produit_scalaire : float * float * float * float -> float = #let orthogonaux = function # u1, u2, v1, v2 -> produit_scalaire(u1,u2,v1,v2) = 0.0;; orthogonaux : float * float * float * float -> bool = #orthogonaux(1.5, 2.0, 2.0, -1.5);; - : bool = true #let norme = function # u1, u2 -> sqrt (produit_scalaire(u1,u2,u1,u2));; norme : float * float -> float = #norme(1.0, 2.0);; - : float = 2.2360679775

12

CHAPITRE 2. CONCEPTS DE BASE

Autre exemple, d´efinissant quelques fonctions ´el´ementaires ; regardons d’abord comment la fonction exp (pr´ed´efinie) est typ´ee : #exp;; - : float -> float = #let ch = function x -> ( exp (x) +. exp ( -. x ) ) /. 2.0 ;; ch : float -> float = #let sh = function x -> ( exp (x) -. exp ( -. x ) ) /. 2.0 ;; sh : float -> float = #ch (1.0);; - : float = 1.54308063482 #sh (1.0);; - : float = 1.17520119364

2.2.3

En Pascal

L’´ecriture de fonctions en Pascal est possible, et peut ˆetre consid´er´ee comme un cas simplifi´e de proc´edures (voir module Informatique 1). En effet, on n’y utilise pas le mode de passage de param`etres en var. Les particularit´es des fonctions en Pascal concernent la fa¸con de sp´ecifier le type du r´esultat, et la fa¸con de retourner la valeur d’une fonction. Le type du r´esultat doit ˆetre un type simple ; il est indiqu´e dans l’entˆete de la fonction, apr`es les param`etres. La valeur de la fonction est affect´ee (souvent `a la fin de son texte), par une affectation nomdelafonction := valeur. Exemple : program vecteurs ; var x, y , n: real; function produit_scalaire (u1, u2, v1, v2:real):real ; begin produit_scalaire := u1 * v1 + u2 * v2 end; function norme (u1, u2: real): real; begin norme := sqrt (produit_scalaire(u1,u2,u1,u2)) end; begin readln(x,y); n := norme (x,y); writeln (’Norme = ’, n) end. Remarque : On notera ici la diff´erence de style de programmation, entre la solution donn´ee en Caml, et celle-ci. L’utilisation d’un langage fonctionnel (comme Caml), associ´e `a une interaction (top-level) permet de se concentrer sur la d´efinition d’une fonction qui calcule des valeurs en fonction d’autres valeurs. En Pascal, on doit en plus d´ecrire compl`etement l’interaction, comme ici dans le programme principal avec readln et writeln. On doit aussi se soucier de d´eclarer des variables pour stocker les donn´ees lues, les r´esultats ` a afficher, et ´eventuellement des valeurs interm´ediaires.

´ 2.3. METHODOLOGIE

2.3 2.3.1

13

M´ ethodologie Sp´ ecification

Les paragraphes pr´ec´edents ont introduit successivement les notions de type, d’expressions, de fonctions et ont donn´e un certain nombre d’exemples d’algorithmes puis de programmes. Il s’agit maintenant d’inscrire ces notions dans une m´ethodologie de conception qui permette de passer de la mani`ere la plus sˆ ure et la plus efficace, d’un probl`eme `a r´esoudre, `a sa solution en terme de programme ex´ecutable. La m´ethodologie propos´ee comporte les points suivants : Sp´ ecification : Il faut d’abord identifier le probl`eme (lui donner un nom), faire le bilan des donn´ees disponibles, pr´eciser leur type, d´efinir quel type de r´esultat on attend, et bien sˆ ur d´ecrire ce r´esultat (sans dire comment le calculer). Cette phase r´esulte en une fonction, dont on choisit le nom, on pr´ecise les types, et dont on commente le fonctionnement. Algorithme : L’´ecriture de l’algorithme consiste `a d´efinir le corps de la fonction sp´ecifi´ee. On parlera souvent de fonction-algorithme pour indiquer qu’on ´ecrit des algorithmes sous forme de fonction. Ceci se fera ´eventuellement en utilisant d’autres fonctions qu’il faudra alors sp´ecifier et pour lesquelles il faudra donner un algorithme. Ces aspects, dits d’analyse descendante, seront pr´ecis´es dans le prochain paragraphe. Programme : C’est la phase appel´ee aussi codage, o` u l’on traduit l’algorithme dans un langage donn´e (dans notre contexte Caml ou Pascal). Les principaux probl`emes sont alors d’utiliser les constructions ad´equates du langage en veillant au respect des r`egles de syntaxe, et d’utiliser les types pr´esents dans le langage en veillant `a ce que leurs limitations (par exemple sur les nombres) ne mettent pas la solution en d´efaut. V´ erification et tests : Dans le cas de la programmation en Caml, une v´erification partielle est fournie par le calcul du type : on doit v´erifier que le type calcul´e correspond au type que l’on avait sp´ecifi´e. L’exp´erience montre que dans beaucoup de cas, une erreur dans l’algorithme, entraine une erreur de type ; on retourne alors `a la phase algorithme. Dans le cas Pascal, la compilation est pr´ec´ed´ee par une v´erification de types qui permet aussi des d´etections d’erreurs. Il reste ensuite ` a r´ealiser des tests fonctionnels, qui peuvent permettre, de d´eceler d’´eventuelles erreurs de fonctionnement. Par contre, l’impossibilit´e pratique de r´ealiser des tests exhaustifs (quand au moins une donn´ee appartient `a un type infini), ne permet pas de prouver que la fonction est totalement correcte. Exemple : Un cin´ephile veut enregistrer un film de dur´ee x minutes et qui commence `a une heure donn´ee ; il veut pour cela connaˆıtre l’heure de fin et savoir si oui ou non, le film finira le lendemain. Sp´ ecification : On commence par ´etudier les informations dont on dispose, et celles que l’on veut calculer. Ce qui nous donne la sp´ecification de fonction suivante : Fin_du_film : entier*entier*entier -> entier*entier*booleen (* Fin_du_film ( hdebut,mndebut,duree) calcule l’heure de fin, la minute de fin (qui correspondent au temps de debut + duree), et un booleen vrai s’il y a passage a 0h *) Algorithme : On va utiliser l’arithm´etique modulo 60 pour calculer la minute de fin, et l’arithm´etique modulo 24, pour calculer l’heure et savoir si on passe au lendemain. On va effectuer un calcul interm´ediaire pour savoir de combien d’heures, le temps avance.

14

CHAPITRE 2. CONCEPTS DE BASE

Fin_du_film : entier*entier*entier -> entier*entier*booleen hdebut , mndebut, duree -> soit hplus = quotient ((mndebut + duree) , 60) dans( (hdebut + hplus) modulo 24, (mndebut + duree) modulo 60, (hdebut + hplus) >= 24 ) Programme :

On choisit de coder cet exemple en Caml.

#let fin_du_film = function # hdebut , mndebut, duree -> # let hplus = (mndebut + duree) / 60 # in ( (hdebut + hplus) mod 24, # (mndebut + duree) mod 60, # (hdebut + hplus)/ 24 = 1 );; fin_du_film : int * int * int -> int * int * bool = V´ erification et tests : le type calcul´e correspond bien au type sp´ecifi´e. On fera quelques tests montrant diff´erents cas possibles. # fin_du_film (22, 35, 123);; - : int * int * bool = 0, 38, true # fin_du_film (20, 45, 92);; - : int * int * bool = 22, 17, false

2.3.2

Analyse Descendante

L’´ecriture d’algorithmes est souvent une tˆache complexe, selon le nombre d’informations diff´erentes `a traiter, et la complexit´e du probl`eme lui-mˆeme. D´ efinition : Le principe de l’analyse descendante consiste `a examiner globalement le probl`eme, et `a essayer de le d´ecomposer en sous-probl`emes ind´ependants. On se contente alors de sp´ ecifier les sous-probl`emes, pour pouvoir ´ecrire l’algorithme g´en´eral, qui va utiliser les solutions des sousprobl`emes. Il reste ensuite ` a r´ ealiser un algorithme pour chacun des sous-probl`emes (cela peut aussi ˆetre d´ecompos´e selon le mˆeme principe). La d´ecomposition peut se faire de deux fa¸cons compl´ementaires : D´ ecomposition par cas : Selon les donn´ees, on constate que le traitement `a effectuer est diff´erent, et que les solutions pour chacun des cas sont ind´ependantes. On d´ecomposera alors le probl`eme en autant de sous-probl`emes qu’il y a de cas. D´ ecomposition structurelle : On met en ´evidence des r´esultats interm´ediaires qui semblent plus faciles ` a calculer en fonction des donn´ees, et qui serviront `a calculer le r´esultat final. Les sous-probl`emes consistent alors ` a calculer chacun de ces r´esultats interm´ediaires (en fonction de donn´ees et d’autres r´esultats interm´ediaires) et `a calculer les r´esultats finaux (eux aussi en fonction de donn´ees et de r´esultats interm´ediaires). Exemple : On se propose d’´ecrire une fonction de conversion entre unit´es de longueur du syst`eme m´etrique et unit´es anglo-saxonnes. On se limitera aux m`etre (m), centim`etre (cm), pied (ft) et pouce (inch). On a : 1 inch = 2.54 cm et 1 ft = 12 inch. On veut pouvoir convertir la repr´esentation d´ecimale d’une longueur dans n’importe quelle unit´e (m, cm, ft, inch), en la repr´esentation de la mˆeme longueur dans les deux unit´es de l’autre syst`eme. Par exemple 1.77 m -> 5 ft 10 inch et 30.5 ft -> 9 m 29 cm. On veut de plus, c’est une habitude, obtenir des r´esultats seulement en pouces pour des longueurs inf´erieures ` a 2 pieds. On ´ecrit la sp´ecification suivante :

´ 2.3. METHODOLOGIE

15

fonction conversion : reel * chaine -> entier * chaine * entier * chaine (* conversion (longueur, unite) est un quadruplet contenant une longueur dans la plus grande unite’, le nom de l’unite’, une seconde longueur et le nom de la deuxieme unite’. *) On commence par d´ecomposer en 2 cas : la conversion d’unit´e SI vers unit´es anglo-saxonnes, et l’inverse. Chacun des 2 cas va aussi se d´ecomposer selon l’unit´e donn´ee, mais ces deux cas pourront ˆetre trait´es ensemble ` a condition de ramener les donn´ees en cm ou en inch. Pour cela on va sp´ecifier deux fonctions : fonction cm_to_ft_inch : reel -> entier * chaine * entier * chaine (* cm_to_ft_inch (longueur) calcule le resultat en fonction d’une longueur en cm *) fonction inch_to_m_cm : reel -> entier * chaine * entier * chaine (* inch_to_m_cm (longueur) calcule le resultat en fonction d’une longueur en inch *) On peut alors r´ealiser la fonction conversion : fonction conversion : reel * chaine -> entier * chaine * entier * chaine longueur, unite -> selon unite "m" : cm_to_ft_inch (100 * longueur) "cm" : cm_to_ft_inch (longueur) "ft" : inch_to_m_cm (12 * longueur) "inch" : inch_to_m_cm (longueur) Il faut maintenant r´ealiser les fonctions sp´ecifi´ees. On va r´ealiser la fonction cm_to_ft_inch en continuant ` a d´ecomposer (structurellement), ceci en isolant comme r´esultat interm´ediaire la repr´esentation de la longueur en inch. fonction cm_to_inch : reel -> entier (* convertit cm en inch, avec arrondi *) fonction inch_to_ft_inch : entier -> entier*chaine*entier*chaine (* calcule le resultat final a partir d’une longueur en inch, superieure a 2 ft *) fonction cm_to_ft_inch : reel -> entier * chaine * entier * chaine cm -> soit inch = cm_to_inch (cm) dans si inch < 24 alors ( 0, "ft", inch, "inch") sinon inch_to_ft_inch (inch) R´ealisons maintenant les deux fonctions sp´ecifi´ees : fonction cm_to_inch : reel -> entier cm -> arrondi( cm / 2.54)

16

CHAPITRE 2. CONCEPTS DE BASE

fonction inch_to_ft_inch : entier -> entier*chaine*entier*chaine inch -> ( quotient (inch, 12), "ft", reste (inch,12), "inch") L’analyse de la fonction de conversion inch_to_m_cm est laiss´ee en exercice.

2.4 2.4.1

R´ ecursivit´ e Principes

D´ efinitions : On dit qu’une fonction f appelle une fonction g, si le texte qui d´efinit f comporte une application de la fonction g, ou une application d’une fonction h qui appelle la fonction g. L’´ecriture d’une fonction f est dite r´ ecursive, si elle s’appelle elle mˆeme. Un tel appel est dit appel r´ecursif. On parlera de r´ecursivit´e simple quand f comporte une application de f, et de r´ecursivit´e crois´ee dans le cas g´en´eral. Se pose alors le probl`eme du sens ` a donner `a de telles d´efinitions : dans un dictionnaire on ne d´efinit pas un mot en l’employant dans la d´efinition. De mˆeme, on ne peut se contenter de dire, par exemple, que la somme de deux entiers x et y est d´efinie comme ´etant la somme des entiers y et x. Bien que strictement vraie, cette affirmation ne donne aucun renseignement sur le calcul de cette somme. L’utilisation de la r´ecursivit´e, en informatique, est `a rapprocher de l’usage intensif que les math´ematiques font du principe de r´ecurrence. Les rapports entre les deux seront explicit´es au chapitre 5 (voir en particulier section 5.2 et section 5.3, page 45). Le principe de r´ecurrence sur N, permet de prouver une propri´et´e pour tout entier, en la d´emontrant pour l’entier 0, et en d´emontrant que si elle est vraie pour un entier n, elle l’est pour n + 1. D´efinir une fonction r´ecursivement consiste `a : – D´efinir la valeur de la fonction pour un ensemble de cas de base, (sans utiliser d’appels r´ecursifs) – La d´efinir dans le cas g´en´eral, en fonction de valeurs de la fonction dans des cas plus simples. La notion de “plus simple” doit pouvoir permettre d’arriver `a un cas de base, en un nombre fini d’´etapes. On peut ainsi, par exemple, d´efinir une fonction f sur N, en d´efinissant f(0) et en d´efinissant f(n) en fonction de f(n-1). Exemple : La fonction factorielle est d´efinie par n! = n ∗ (n − 1)! pour n > 0 et 0! = 1. On peut donc ´ecrire l’algorithme suivant : fonction fact : entier -> entier n -> si n = 0 alors 1 sinon n * fact (n-1) On peut aussi utiliser la r´ecursivit´e quand une fonction s’exprime simplement pour un certain sous-ensemble des donn´ees, et si l’on peut se ramener `a ce sous-ensemble. fonction distance : entier * entier -> entier (a,b) -> si a >= b alors a - b sinon distance (b,a)

´ ´ 2.4. RECURSIVIT E

17

Remarques : Pour qu’un algorithme r´ecursif se termine, il faut (il ne suffit pas) que seule une partie de cet algorithme ne comportant pas d’appel r´ecursif soit ´evalu´ee pour les cas de base. Les expressions alternatives et de choix n’´evaluent que la bonne expression, et sont donc ad´equates pour exprimer un algorithme o` u seule une partie doit ˆetre ´evalu´ee. On peut aussi utiliser les op´erateurs bool´eens et puis et ou alors, qui ont le mˆeme sens respectivement que et et ou, mais dont le second argument n’est ´evalu´e que si n´ecessaire. Le pr´edicat suivant indique si un nombre entier est pair. fonction pair : entier -> booleen n -> (n = 0) ou alors ( (n <> 1) et puis pair (n-2) ) L’´ecriture r´ecursive d’une fonction peut ˆetre tr`es simple, d`es lors que l’on connaˆıt une formule de r´ecurrence, o` u qu’elle est d´ej` a pr´esente dans la sp´ecification du probl`eme (ce qui est souvent le cas dans des exemples math´ematiques). Si ce n’est pas le cas, cette ´ecriture requiert un travail d’analyse, visant `a d´ecouvrir une m´ethode permettant de r´esoudre un probl`eme, connaissant une solution `a ce mˆeme probl`eme dans un cas plus simple. On utilise souvent pour cela une notion li´ee `a la taille des donn´ees. Par exemple, cherchons ` a d´efinir le r´esultat tri´e d’une suite de n entiers : le probl`eme est ´el´ementaire pour des suites de 1 ou 2 entiers. Pour une suite de longueur n, on peut la d´ecouper en deux : le r´esultat sera alors la fusion du tri de chacunes des deux sous-suites, la fusion consistant `a calculer une suite tri´ee issue du m´elange de deux suites tri´ees (c’est souvent ce que l’on fait pour trier `a la main un jeu de 52 cartes). On verra au chapitre 3 comment utiliser la r´ecursivit´e avec des types de donn´ees plus complexes : listes et types r´ecursifs (voir en particulier section 3.2, pages 23 et 26, ainsi que sections 3.3 et 3.4).

2.4.2

En Caml

La d´efinition d’une fonction r´ecursive doit se faire par la construction : let rec. #let rec fact = function n -> if n = 0 then 1 # else n * fact (n - 1);; fact : int -> int = La fonction puissance2 indique si oui ou non, un entier est une puissance de 2. Sa d´efinition repose sur le fait que l’ensemble des puissances de 2 contient 1 et les nombres pairs dont la moiti´e est une puissance de 2. Les op´erateurs & et or de Caml correspondent respectivement `a et puis et ou alors. #let rec pair = # function n -> (n = 0) or ( (n <> 1) & pair (n-2) ) #and puissance2 = # function n -> (n = 1) or (pair (n) & puissance2 (n/2));; pair : int -> bool = puissance2 : int -> bool = #puissance2 (65536);; - : bool = true Le calcul du quotient de la division euclidienne de a par b avec b > 0 peut s’´ecrire (la preuve sera donn´ee au chapitre 5, page 45) : #let rec quotient = function (a,b) -> # if (0<=a) & (a int =

18

CHAPITRE 2. CONCEPTS DE BASE

#quotient (25, 3);; - : int = 8 La r´ecursivit´e crois´ee est possible en d´efinissant simultan´ement les deux fonctions, avec le motcl´e and : #let rec f = function x -> if x = 1 then 0 else g(x) #and g = function y -> f (y / 2) + 1 ;; f : int -> int = g : int -> int = #f (148);; - : int = 7

2.4.3

En Pascal

En Pascal, les fonctions peuvent ˆetre r´ecursives, sans d´eclaration particuli`ere. Exemple :

Le calcul de la factorielle sp´ecifi´e en 2.4.1.

program factorielle ; var n, f: integer; function fact (n : integer):integer ; begin if n = 0 then fact := 1 else fact := n * fact (n -1) end; begin readln(n); f := fact(n); writeln (’fact (’, n, ’) = ’, f) end. Pour les r´ecursions crois´ees, le probl`eme (dˆ u au compilateur Pascal) est que l’on ne peut utiliser une fonction avant de l’avoir d´eclar´ee. Il est alors impossible de d´eclarer `a la fois f avant g et g avant f. La solution est de d´eclarer d’abord les profils des fonctions (c’est-`a-dire les types des param`etres d’entr´ee et du r´esultat), puis d’´ecrire leur corps. Ceci est d’ailleurs int´eressant dans le cadre d’une analyse descendante o` u l’on ´ecrit d’abord la sp´ecification d’une fonction (son profil), puis sa r´ealisation (le corps). Exemple :

Que calcule ce programme ?

program croise ; var n, res: integer; function f (n : integer):integer ; forward ; function g (n : integer):integer ; forward ; function f ; begin if n = 1 then f:= 0 else f:= g (n) end; function g ; begin

´ ´ 2.4. RECURSIVIT E g := f ( n div 2) + 1 end; begin readln(n); res := f(n); writeln (’f (’, n, ’) = ’, res) end.

19

20

CHAPITRE 2. CONCEPTS DE BASE

Chapitre 3

Types et structures de donn´ ees 3.1

Abstraire les donn´ ees

Dans le chapitre 2, on s’est int´eress´e `a l’expression, au traitement et `a la production d’informations (valeurs) de nature tr`es simple : entiers, r´eels, caract`eres, bool´eens, chaˆınes. On a vu que les langages informatiques mettent `a disposition imm´ediate du programmeur un certain nombre de types de base permettant de manipuler directement de telles informations. On a d´efini en 2.1.1 la notion de type comme un ensemble de valeurs muni d’op´erations. Mais le programmeur doit ´egalement pouvoir manipuler des informations de nature plus complexe : nombres rationnels, complexes, polynˆ omes, dictionnaires, etc. Il doit donc pouvoir se doter de types plus ´elabor´es permettant de prendre en compte la complexit´e de ces informations. L’objectif est de transposer ce qui a ´et´e fait sur les types de base, `a des types plus complexes. Examinons tout d’abord un type de base qui permet de mod´eliser des informations relativement complexes : le type chaˆıne de caract`eres. Le programmeur dispose d’un certain nombre de fonctionnalit´es que l’on peut classifier ainsi : Constructeur : Ecrire une constante "Bonjour" dans un programme construit implicitement une repr´esentation de cette chaˆıne. S´ electeur : On peut acc´eder au nieme caract`ere d’une chaˆıne, ce que l’on pourra noter : nieme_caractere ( "Bonjour", 4) et qui vaut : ’j’ Op´ erateur : On dispose d’une op´eration de concat´enation de deux chaˆınes, qui renvoit une chaˆıne (Exemple "Bonjour " & "Monsieur" vaut : "Bonjour Monsieur"). Pr´ edicat : On peut comparer deux chaˆınes par une fonction d’´egalit´e. De telles fonctionnalit´es permettent au programmeur de manipuler des chaˆınes de caract`eres dans un algorithme, en ignorant tout de la mani`ere dont les chaˆınes sont repr´esent´ees dans l’ordinateur. Il en va de mˆeme pour les entiers, les r´eels, etc. On souhaiterait qu’il en soit ainsi pour les informations appartenant `a des types plus ´elabor´es. Pour cela, il faut pour chaque nouveau type, disposer d’un ensemble suffisant de fonctions manipulant des informations de ce type. D´ efinition : L’abstraction des donn´ees est une m´ethode d’analyse consistant `a s´eparer : – d’une part, la fa¸con d’utiliser les informations d’un nouveau type : c’est ce que l’on appellera sp´ecifier un type, – d’autre part, les moyens permettant l’utilisation de ce type : c’est ce que l’on appelera r´ealiser un type. 21

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

22

Sp´ ecifier un type, consiste ` a lui donner un nom, `a d´ecrire l’ensemble des valeurs qu’il doit repr´esenter, et ` a sp´ecifier un ensemble suffisant de fonctions : constructeur(s), s´electeur(s), op´erateur(s) et pr´edicat(s), permettant d’utiliser ce type, dans un algorithme, comme un type de base. R´ ealiser un type consiste ` a d´ecrire comment est repr´esent´ee l’information en termes des types disponibles, et ` a r´ealiser les fonctions sp´ecifi´ees : ce point sera esquiss´e en 3.2, mais ne peut trouver une solution compl`ete que selon le langage utilis´e (voir 3.2.1 et 3.2.2). Exemple : On veut ´ecrire un logiciel de calcul sur les rationnels. Pour cela on peut sp´ecifier le type rationnel ainsi : type rationnel

(* l’ensemble Q *)

fonction rationnel : entier*entier -> rationnel (* construit un rationnel a partir de son numerateur et de son denominateur *) fonction rationnel_entier : entier -> rationnel (* construit un rationnel egal a l’entier fourni *) fonction numerateur : rationnel -> entier (* le numerateur du rationnel *) fonction denominateur : rationnel -> entier (* le denominateur du rationnel *) fonction representation_externe : rationnel -> chaine (* donne un rationnel sous la forme " 1/2 " *) fonction plus_rat : rationnel * rationnel -> rationnel (* operateur d’addition sur les rationnels *) fonction egal_rat : rationnel * rationnel -> booleen (* predicat d’egalite entre rationnels *) Le programmeur qui va utiliser ce type n’a pas `a se pr´eoccuper de la r´ealisation, par exemple il peut ´ecrire : representation_externe (plus_rat (rationnel (3,8), rationnel (2,3))) Il peut aussi d´efinir de nouvelles fonctions ainsi : fonction oppose_rat : rationnel -> rationnel r -> rationnel( - numerateur(r),denominateur(r)) fonction moins_rat : rationnel * rationnel -> rationnel r1, r2 -> si egal_rat (r1, r2) alors rationnel_entier (0) sinon plus_rat (r1, oppose_rat(r2) ) Remarque : Noter qu’on peut choisir de sp´ecifier un ensemble de fonctionnalit´es de base plus petit que celui qui vient d’ˆetre indiqu´e. Par exemple, on peut ne retenir que les fonctions rationnel, numerateur et denominateur. On d´efinira alors les fonctions rationnel_entier, plus_rat, egal_rat et representation_externe

3.2. TYPES CONSTRUITS

23

en utilisant les trois fonctionnalit´es de base retenues . . . et sans se pr´eoccuper de la r´ealisation du type rationnel.

3.2

Types construits

On s’attache maintenant ` a d´ecrire comment une valeur d’un type est repr´esent´ee `a partir de valeurs de types de base. Exemples : – Un rationnel peut ˆetre repr´esent´e par deux entiers, – Un temps par trois entiers (heure, minute et secondes), – Une date, sous la forme lundi 6 fevrier 1995, par deux chaines de caract`eres et deux entiers. – Un vecteur de R2 par deux r´eels Type produit : Tous ces exemples de valeurs sont des N-uplets qui appartiennent `a un produit cart´esien de types de base (respectivement Z 2 , Z 3 ...). On appelle type produit un type d´efini comme un produit cart´esien de types. Dans la pratique des langages informatiques, on trouve deux sortes de types produits : – Les enregistrements (ou types produits `a champs nomm´es) : un type enregistrement comporte plusieurs champs, chacun d´efini par son nom et son type. Par exemple, soit un enregistrement rationnel, comportant les champs numerateur et denominateur, chacun ´etant de type entier. Si x est un rationnel, on acc`ede `a un champ par la notation suivante : x.numerateur – Les N-uplets : sont d´efinis par un n-uplet de types. Par exemple, on peut r´ealiser le type vecteurR2 par un couple de r´eels, et noter un ´el´ement : (3.5, 9.99) Type somme : Le m´ecanisme pr´ec´edent ne permet pas de construire tous les types n´ecessaires. En effet, il impose de faire figurer le mˆeme ensemble d’informations pour toutes les valeurs d’un type. Or, dans la pratique, on aimerait pouvoir exprimer, par exemple, qu’un enregistrement d´ecrivant l’´etat civil d’une personne contienne diff´erents champs selon le sexe de cette personne. On appelle type somme un type construit par union disjointe de types. L’union disjointe de deux ensembles est une union permettant de savoir `a quel sous-ensemble appartient un ´el´ement de l’union. Un type somme peut ainsi contenir tel type d’information, ou tel autre. Ceci est tr`es utile quand pour une mˆeme entit´e (dont on veut d´efinir le type), on peut disposer d’informations diff´erentes. Exemples : On veut d´efinir un type distance qui regroupe des distances terrestres (enti`eres en m) et des distances nautiques (r´eelles en milles). On le d´efinit comme la somme des types r´eel et entier. 1852 metres, 12.5 Milles sont des ´el´ements de ce type distance. Il est important ici que l’union des deux types r´eel et entier soit disjointe, ce qui permet de savoir `a quelle partie appartient un ´el´ement de type distance. Les exemples suivants de types, d´efinis par ´enum´eration de valeurs, peuvent ˆetre assimil´es `a des types sommes, car ils sont d´efinis par une union de singletons comportant chacun une valeur. L’ensemble des chiffres romains {I, V, X, L, C, D, M } est d´efini par ´enum´eration. C’est l’union de {I}, {V} ... Il en est de mˆeme pour l’ensemble des jours de la semaine {lundi, mardi,..., dimanche} Types r´ ecursifs : Les d´efinitions de type pr´ec´edentes permettent de structurer des donn´ees qui, soit comportent toutes plusieurs informations (type produit), soit comportent selon les cas des informations diff´erentes (type somme).

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

24

On s’int´eresse maintenant au cas o` u le type d’une des composantes contient les mˆemes informations que le type ` a d´efinir. Exemple : On veut d´efinir un type personne qui comporte les champs nom, prenom, et le pere et la mere, qui sont eux aussi des personnes. Une personne contiendra donc les informations suivantes : nom, prenom, nom et pr´enom du p`ere, nom et pr´enom du p`ere du p`ere... etc Pour qu’une personne soit repr´esent´ee par une quantit´e d’information finie, il faut pr´evoir le cas d’une personne inconnue, qui servira `a d´esigner le p`ere (ou la m`ere) d’une personne de p`ere (ou de m`ere) inconnu. D´ efinition :

3.2.1

Un type, dont la d´efinition fait r´ef´erence `a lui-mˆeme est dit type r´ ecursif.

En Caml

Type produit - Enregistrement : Voici une premi`ere fa¸con de programmer le type rationnel : on d´efinit rationnel comme un type enregistrement, en donnant les noms (appel´es ´etiquettes) de champs num et den, et leurs types. #type rationnel = {num : int; den:int};; Le type rationnel est d´ efini. La construction d’un enregistrement se fait par une expression : {etiquette = expr ; ... } Par exemple, soit x = rationnel (1, 2) peut ˆetre traduit en Caml : #let x = {num = 1; den = 2};; x : rationnel = {num = 1; den = 2} #let y = {num= 3; den = 4};; y : rationnel = {num = 3; den = 4} L’acc`es `a un champ respecte la syntaxe usuelle : expr.etiquette, l’expression numerateur(r) peut ˆetre traduite en Caml : r.numerateur. La fonction plus_rat peut alors s’´ecrire : #let plus_rat = function # (r1, r2) -> {num = r1.num * r2.den + r2.num * r1.den ; # den = r1.den * r2.den} ;; plus_rat : rationnel * rationnel -> rationnel = #plus_rat (x,y);; - : rationnel = {num = 10; den = 8} Remarque : On peut aussi, au lieu de traduire chacune des expressions permettant de construire ou d’acc´eder ` a un type directement avec les constructions du langage Caml, traduire les fonctions correspondantes. Par exemple : #let numerateur = function r -> r.num ;; numerateur : rationnel -> int = Cette m´ethode a l’avantage de continuer `a cacher la repr´esentation d’un rationnel, dans les programmes l’utilisant (cf. oppose_rat en section 3.1). On peut ainsi donner une r´ealisation compl`ete des fonctions du type rationnel. Ceci permet `a un programmeur utilisant le type rationnel de tout ignorer de sa r´ealisation, et d’utiliser, s’il existe plusieurs r´ealisations, l’une quelconque d’entre elles. On peut avoir, par exemple, une r´ealisation qui r´eduit les rationnels `a chaque op´eration, une autre qui ne les r´eduit qu’au moment de donner la repr´esentation externe. L’essentiel pour l’utilisateur est d’obtenir le mˆeme r´esultat pour un calcul comme :

3.2. TYPES CONSTRUITS

25

representation_externe (plus_rat (rationnel (3,8), rationnel (2,3))) Type produit - N-uplets : en Caml. On les contruit :

L’utilisation des N-uplets (type produit non nomm´e) est tr`es simple

#(4, 7, 9);; - : int * int * int = 4, 7, 9 #(true, "bonjour");; - : bool * string = true, "bonjour" L’acc`es aux ´el´ements d’un couple se fait par les fonction fst (premier) et snd (second). #fst (4, 8);; - : int = 4 #snd (4, 8);; - : int = 8 Type somme - Enum´ er´ e : En Caml, les types ´enum´er´es sont des cas particuliers de type somme. La d´efinition suivante, indique qu’une valeur de type jour peut ˆetre soit le constructeur Lundi, soit le constructeur Mardi ... On utilisera l’expression match ... with... pour distinguer selon le constructeur utilis´e. #type jour = Lundi | Mardi | Mercredi | Jeudi | # Vendredi | Samedi | Dimanche ;; Le type jour est d´ efini. #let lendemain = function jour -> # # # # # # # lendemain : jour -> jour =

match jour with Lundi -> Mardi | Mardi -> Mercredi| Mercredi -> Jeudi | Jeudi -> Vendredi | Vendredi -> Samedi | Samedi -> Dimanche | Dimanche -> Lundi ;;

#lendemain (Mardi);; - : jour = Mercredi Type somme : Dans le cas g´en´eral, un type somme est d´efini comme le choix entre plusieurs constructeurs, chaque constructeur ´etant d´efini par son nom et la liste de ses arguments. Exemple : le constructeur Mille ` a un argument de type float. #type distance = Mille of float # | Km_metre of int * int ;; Le type distance est d´ efini. Pour construire une valeur d’un type somme, on utilise une expression de la forme : constructeur expression ou constructeur si ce constructeur n’a pas d’argument (exemple pr´ec´edent). #Km_metre (1 , 852);; - : distance = Km_metre (1, 852) #Mille (2.5);; - : distance = Mille 2.5

26

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

L’acc`es aux arguments d’une valeur d’un type somme, se fait grˆace `a l’expression de filtrage : match expression with constructeur1 motif1 -> expression1 | constructeur2 motif2 -> expression2 ... dans laquelle les motifs sont des listes d’identificateurs. L’expression match, selon le constructeur utilis´e dans l’expression va faire correspondre terme `a terme aux identificateurs du motif, les arguments du constructeur. Ces identificateurs pourront ˆetre utilis´es dans l’expression correspondante. #let EnKm = function d -> # match d with # Km_metre(km,m) -> float_of_int(m+1000*km)/. 1000.0 # | Mille (x) -> x *. 1.8519 ;; EnKm : distance -> float = #EnKm (Km_metre (3, 750));; - : float = 3.75 #EnKm (Mille 2.5);; - : float = 4.62975 Le filtrage peut aussi ˆetre effectu´e dans la d´efinition d’une fonction (´equivalente `a la formulation pr´ec´edente) : #let EnKm = function # Km_metre(km,m) -> float_of_int(m+1000*km)/. 1000.0 # | Mille (x) -> x *. 1.8519 ;; EnKm : distance -> float = Types r´ ecursifs : Le type personne, discut´e en 3.2 (page 24) peut ˆetre r´ealis´e en Caml de la fa¸con suivante : #type personne = MrouMme of string * string * personne * personne # | Inconnu ;; #let ADupont = #MrouMme ("Antoine", "Dupont", # MrouMme ("Jean", "Dupont", # MrouMme ("Pierre", "Dupont", Inconnu,Inconnu), # MrouMme ("Marie", "Granger", Inconnu,Inconnu)), # MrouMme ("Desire", "Leduc", # MrouMme ("Georges", "Leduc", # MrouMme ("Robert", "Leduc",Inconnu,Inconnu), # MrouMme ("Raymonde", "Leblanc",Inconnu,Inconnu)), # MrouMme ("Berthe", "Trognon",Inconnu,Inconnu)));;

La manipulation d’un objet d’un type r´ecursif (constructeur, acc`es, pr´edicats) ne fait appel qu’aux notions de types sommes et produits. L’´ecriture d’algorithmes sera bas´ee sur la structure inductive du type : on a vu (cf. 2.4.1) que pour d´efinir une fonction r´ecursive, il fallait la d´efinir pour des cas de base, et dans le cas g´en´eral en fonction de valeurs de la fonction pour des cas plus simples. Avec un type r´ecursif, les cas de base sont les constructeurs ne comportant pas d’argument r´ecursif (dans l’exemple suivant : V, F, Prop) ; le cas g´en´eral consiste `a d´efinir la valeur de la fonction pour une construction r´ecursive, en fonction de sa valeur pour les arguments de la construction. L’exemple suivant permet de manipuler des formules logiques du genre : “P et (non Q ou vrai)” en les repr´esentant par un type r´ecursif logique. La d´efinition peut se lire :

3.2. TYPES CONSTRUITS

27

“Une formule logique peut ˆetre V, F, le constructeur Et appliqu´e `a 2 formules logiques, le constructeur Non appliqu´e ` a une formule logique ... ou le constructeur Prop qui comporte une chaˆıne de caract`eres” #type logique = V | F | Et of logique*logique | Non of logique # | Ou of logique * logique | Prop of string ;; Le type logique est d´ efini. Pour donner une repr´esentation textuelle d’une formule, on ´ecrit une fonction r´ecursive texte, qui calcule la chaine de caract`eres qui repr´esente chacune des contructions, en fonction de la repr´esentation de ses arguments. #let rec texte = function # Et (x,y) -> "(" ^ (texte (x)) ^ " et " ^ (texte (y)) ^ ")" | # Ou (x,y) -> "(" ^ (texte (x)) ^ " ou " ^ (texte (y)) ^ ")" | # Non (x) -> "non " ^ (texte (x)) | # Prop x -> x | # V -> "V" | # F -> "F" ;; texte : logique -> string = #let formule = Et (Non(Prop "P"), Non (Et (Prop "Q", F)));; formule : logique = Et (Non (Prop "P"), Non (Et (Prop "Q", F))) #texte (formule);; - : string = "(non P et non (Q et F))"

3.2.2

En Pascal

Enregistrements : Les enregistrements en Pascal se d´eclarent avec le mot-cl´e record. L’acc`es aux champs se fait avec la notation point´ee habituelle. L’instruction with permet de mettre en facteur le nom de variable pour acc´eder ` a ses champs, uniquement par leur nom. La norme Pascal-Iso ne permet pas l’utilisation de type enregistrement en r´esultat d’une fonction ; cela est possible dans des versions de Pascal plus riches que cette norme. program rationnel ; type rationnel = record num, den : integer end; var x, y, somme : rationnel; function lire_rationnel : rationnel ; var x : rationnel; begin writeln("fraction ?"); readln(x.num, x.den); lire_rationnel := x end; function plus_rationnel (a,b : rationnel): rationnel; var z : rationnel; begin z.num := a.num * b.den + a.den * b.num ; z.den := a.den * b.den; plus_rationnel := z end; begin x := lire_rationnel; y := lire_rationnel;

28

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

somme := plus_rationnel (x, y); with somme do writeln ("somme = ", num, "/", den) end.

Enregistrements ` a champs variant : Ces enregistrements permettent de d´efinir des types sommes. Il faut d´eclarer un champ particulier, appel´e s´electeur, qui permet ensuite de distinguer diff´erentes structures d’enregistrements. On reprend un exemple du paragraphe pr´ec´edent, en Pascal : program conversion ; type nom_unite = (SI, GB); distance = record case unite : nom_unite of SI : (km, metre : integer); GB : (mille : real) end; var d_lue : distance ; dkm : real; function lire_distance : distance ; var x : distance; reponse : char ; begin writeln("Unite SI : o/n ?"); readln(reponse); if reponse = ’o’ then begin x.unite := SI; readln (x.km, x.metre) end else begin x.unite := GB; readln (x.mille) end; lire_distance := x end; function EnKm (d : distance): real; var x : real; begin case d.unite of SI : x := d.km + d.metre / 1000; GB : x := d.mille * 1.8519 ; end; EnKm := x end; begin d_lue := lire_distance; dkm := EnKm (d_lue); writeln ("Distance = ", dkm:10:3, "Km") end.

Notons au passage, l’utilisation d’un type ´enum´er´e : nom_unite, d´efini par ´enum´eration de ses valeurs possibles, et pour lequel on peut faire affectations et comparaisons. Les types r´ecursifs ne sont pas directement autoris´es en Pascal ; il faut pour le faire utiliser la notion de pointeur (qui est hors programme).

3.3. LISTES

3.3

29

Listes

3.3.1

G´ en´ eralit´ es

La plupart des algorithmes vus jusqu’ici manipulent des types de donn´ees de taille limit´ee et fixe (un entier, un enregistrement ...). Or dans le champ d’applications de l’informatique, beaucoup de probl`emes font appel ` a de grandes quantit´es d’informations ; c’est d’ailleurs dans ce cas qu’une r´esolution informatique est la plus n´ecessaire. Parmi les types ´etudi´es, seuls les types r´ecursifs permettent de mod´eliser des quantit´es d’information non born´ees ; par exemple, avec le type personne, on peut saisir un arbre g´en´ealogique, qui sur 10 g´en´erations regroupera d´eja de l’ordre d’un millier de personnes. On va maintenant ´etudier la mod´elisation de grandes quantit´es de donn´ees, dont on dispose sous la forme d’une suite de donn´ees ´el´ementaires de mˆeme type. Cette situation est tr`es courante : par exemple les fichiers d’individus (s´ecurit´e sociale ...) sont des suites d’enregistrements contenant des informations sur chaque individu, les s´eries statistiques sont des suites de valeurs ` a ´etudier... Pour manipuler ce genre de donn´ees dans un programme, une technique ´el´ementaire consiste `a utiliser la notion de vecteur (cf. Informatique 1). L’inconv´enient majeur est qu’il faut connaˆıtre le nombre de donn´ees, ou fixer une borne ` a ce nombre au moment de la conception du programme. D´ efinition : On appelle liste une suite ordonn´ee d’informations de mˆeme type, et ´ el´ ement chacune de ces informations. Une liste peut contenir plusieurs fois le mˆeme ´el´ement. On parlera du type liste, qui regroupe toutes les listes d’´el´ements. Ce type d´epend du type d’´el´ement consid´er´e pour une liste particuli`ere. On peut cependant d´efinir un ensemble de fonctions sur les listes g´en´erales au type liste. On notera element le type d’un ´el´ement. On a besoin de pouvoir construire une liste, d’y acc´eder, et de calculer des propri´et´es. Constructeurs : Pour construire une suite ordonn´ee d’´el´ements, il suffit de disposer d’une fonction de construction d’une liste sans ´el´ement, et d’une fonction de construction d’une liste compos´ee d’un ´el´ement et d’une liste : fonction liste_vide : -> liste d’element fonction ajout : element*liste d’element -> liste d’element Fonctions d’acc` es : Pour acc´eder ` a tous les ´el´ements d’une liste, il suffit de pouvoir acc´eder au premier ´el´ement, et ` a la liste restante (le deuxi`eme n’est que le premier du reste ...etc). fonction premier : liste d’element -> element fonction reste : liste d’element -> liste d’element Pr´ edicat : On a besoin de savoir si une liste est vide ou non, pour ne faire que des appels coh´erents aux fonctions pr´ec´edentes (premier et reste d’une liste vide n’ont aucun sens) fonction est_vide : liste d’element

-> booleen

Exemple d’utilisation : Dans une application de statistiques, on dispose d’une liste d’entiers dont on veut calculer, la moyenne, les valeurs maximales, le mode... fonction maximum : liste d’entier -> entier l -> si est_vide (reste (l)) alors premier (l) sinon max (premier (l), maximum (reste (l))) o` u max est suppos´e d´efini avec le type :

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

30

fonction max : entier * entier -> entier La fonction suivante ajoute un ´el´ement `a la fin d’une liste. Notons que cette fonction s’applique `a une liste d’´el´ements de type quelconque : fonction ajout_alafin : liste d’elements * element -> liste d’elements l,e -> si est_vide (l) alors ajout (e,l) sinon ajout (premier(l), ajout_alafin(reste(l),e)) Remarques : La programmation avec des listes permet de manipuler des suites de donn´ees de taille non born´ee ` a priori. La m´emoire de la machine impose cependant une limite `a cette taille, qui si elle est d´epass´ee provoquera une erreur `a l’ex´ecution. Le choix entre l’utilisation de vecteurs ou de listes d´epend surtout du type de traitement que l’on veut effectuer sur les donn´ees. L’utilisation de listes privil´egie l’acc`es aux ´el´ements dans l’ordre o` u ils sont (mˆeme s’il est facile d’´ecrire une fonction donnant le nieme ´el´ement), sans imposer de contraintes sur la taille. L’utilisation de vecteurs favorise l’acc`es `a un ´el´ement par son indice, mais impose une d´efinition pr´ealable de la taille. Les vecteurs sont particuli`erement adapt´es au calcul vectoriel et matriciel (ils ont d’ailleurs ´et´e introduits pour cela, dans les langages de programmation). Notons que la notion de vecteur (pr´esente en Pascal et en Caml ainsi que dans la plupart des langages) s’´etend simplement avec la notion de tableau (ou matrice), que l’on d´efinit comme un vecteur de vecteurs.

3.3.2

En Caml

Les constructeurs de listes se notent : – [] pour la liste vide – e::l pour l’ajout de e ` al – [e1 ; e2 ; ... en] pour la construction d’une liste `a n ´el´ements. L’acc`es aux listes en Caml peut se faire dans deux styles diff´erents : – En utilisant les fonctions d’acc`es hd pour premier et tl pour reste – En utilisant le filtrage avec la liste vide [], ou avec une liste compos´ee d’un ´el´ement e et d’une liste l not´e e::l Les exemples des fonctions du 3.3.1 peuvent se coder en Caml, avec les fonctions d’acc`es : #let rec maximum = #function l -> if tl(l) = [] then hd(l) # else max (hd(l), maximum (tl(l)));; maximum : ’a list -> ’a = #let rec ajout_alafin = #function l,e -> if l = [] then e ::l # else hd(l):: ajout_alafin(tl(l),e);; ajout_alafin : ’a list * ’a -> ’a list = ou de fa¸con ´equivalente avec filtrage : #let rec maximum = #function e::[] -> e # | e::l -> max (e, maximum (l));; Entr´ ee interactive: >function e::[] -> e > | e::l -> max (e, maximum (l)).. Attention: ce filtrage n’est pas exhaustif.

3.3. LISTES

31

maximum : ’a list -> ’a = #let rec ajout_alafin = #function [], e -> e :: [] # | p::l, e -> p :: ajout_alafin(l,e);; ajout_alafin : ’a list * ’a -> ’a list = #let x = [3; 5; 9; 2];; x : int list = [3; 5; 9; 2] #maximum (x);; - : int = 9 #ajout_alafin (x, 1);; - : int list = [3; 5; 9; 2; 1] Examinons le type de la fonction ajout_alafin : le type ’a list note une liste d’´el´ements dont le type est quelconque ; ’a est appel´ee une variable de type. On peut utiliser ajout_alafin avec n’importe quelle liste. Le type se pr´ecise uniquement au moment d’un appel : ajout_alafin (x, 1) est de type int list. On dit qu’une telle fonction est polymorphe, car elle s’applique ` a plusieurs types diff´erents de donn´ees. Listes et types r´ ecursifs : On a introduit les listes sans faire r´ef´erence aux types r´ecursifs vus en section 3.2 (page 23). Les raisons en sont l’importance des listes en tant que telles en informatique, le fait que les listes soient pr´esentes dans des langages o` u la notion de type r´ecursif n’existe pas, et le traitement particulier r´eserv´e aux listes dans les langages (dont Caml). Cependant, les listes ne sont que le cas particulier d’un type r´ecursif ne comportant qu’une seule r´ef´erence ` a lui mˆeme. Par exemple un polynˆ ome de Z[X], est soit le polynˆ ome nul, soit un polynˆ ome construit par a + X * P o` u P est un polynˆ ome et a appartient `a Z (sch´ema de H¨orner). On peut le d´efinir en Caml (comme on a d´efini le type personne, page 26) : #type polynome = Nul | aplusXfois of int * polynome;; Le type polynome est d´ efini. #let P = aplusXfois (3, aplusXfois (2, aplusXfois (1, Nul)));; P : polynome = aplusXfois (3, aplusXfois (2, aplusXfois (1, Nul))) Ce type est isomorphe au type int list (i.e. tout ´el´ement d’un des types peut ˆetre repr´esent´e dans l’autre de fa¸con unique).

3.3.3

En Pascal

Le type liste n’existe pas en Pascal mais peut ˆetre d´efini, pour un type particulier de liste, de la fa¸con suivante (ceci n’est pas au programme mais est donn´e `a titre d’illustration ; pour une explication de la notion de pointeur utilis´ee ici, on consultera un ouvrage de r´ef´erence sur Pascal) : program listes ; (* Definition du type liste et des fonctions *) type Liste = ^ Element ; Element = record valeur : integer; reste : Liste; end; var l:liste; n, lemax :integer; function liste_vide : Liste; begin liste_vide := NIL end;

32

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

function ajout (e: integer; l: Liste):Liste; var x : Liste; begin new(x); x^.valeur := e; x^.reste := l; ajout := x end; function premier (l:Liste): integer; begin premier := l^.valeur end; function reste (l:Liste): Liste; begin reste := l^.reste end; function est_vide (l:Liste): boolean; begin est_vide := l = NIL end; function max (a,b:integer):integer; begin if a < b then max := b else max := a end; (* programmation avec des listes *) function maximum (l:Liste):integer; begin if est_vide (reste(l) ) then maximum := premier (l) else maximum := max (premier(l),maximum(reste(l))); end; begin writeln ("Suite d’entiers terminee par 0"); l := liste_vide; readln (n); while n <> 0 do begin l := ajout (n, l); readln(n) end; lemax := maximum (l); writeln ("Le maximum est :", lemax) end.

On remarquera, qu’apr`es quelques efforts pour impl´ementer ce type, on peut l’utiliser simplement : l’´ecriture de la fonction maximum est tr`es proche de l’algorithme donn´e en 3.3.1.

3.4

Un exemple : le type arbre

Les exemples de types r´ecursifs (personne et logique) vus en 3.2.1 pr´esentent des similarit´es qui justifient une pr´esentation plus g´en´erale. Tous deux peuvent ˆetre repr´esent´es graphiquement par un arbre constitu´e d’une racine (la personne ou l’expression), d’o` u partent des branches vers des noeuds (les parents, ou les sousexpressions), qui sont eux mˆemes des arbres, ces ramifications se terminant par des feuilles (la personne inconnue ou les constantes). D´ efinitions : Plus g´en´eralement, on appellera arbre un ensemble d’´el´ements appel´es noeuds et un ensemble d’´el´ements appel´es feuilles, structur´es selon la r`egle suivante : un arbre peut ˆetre r´eduit `a une feuille, ou ˆetre un noeud et contenir un certain nombre d’arbres. Un arbre binaire est un arbre dont tous les noeuds contiennent deux arbres. Repr´ esentation : Un arbre peut ˆetre repr´esent´e (dans l’exemple des expressions arithm´etiques les noeuds sont les op´erations, et les feuilles les entiers) : – graphiquement (c’est le plus naturel, mais pas le plus simple `a saisir pour un ordinateur) – en notation infix´ee, par exemple : (12 + 3) * (7 - 2)

3.4. UN EXEMPLE : LE TYPE ARBRE

33

– en notation pr´efix´ee, par exemple : * (+ 12 3) (- 7 2) – en notation postfix´ee, par exemple : 12 3 + 7 2 - * (c’est la notation polonaise inverse) Utilisation : L’usage des arbres est tr`es r´epandu, pour la structuration d’informations. Citons par exemple : la classification botanique, une table des mati`eres, les coups possibles aux ´echecs, un arbre g´en´ealogique... et dans le domaine informatique : les expressions arithm´etiques, logiques, et plus g´en´eralement tout programme ´ecrit dans un langage structur´e. L’int´erˆet de la formalisation informatique des arbres r´eside dans l’ensemble d’algorithmes que l’on peut d´efinir sur eux de mani`ere g´en´erale, et qui seront autant de traitements disponibles pour chaque arbre en particulier. On peut par exemple rechercher l’ensemble des descendants, compter les noeuds, savoir si un noeud est ancˆetre d’un autre ... En Caml :

Sur le type personne, qui est un arbre binaire, on d´efinit la fonction nb_personnes_connues qui compte le nombre de noeuds de l’arbre g´en´ealogique. On pourrait d´efinir cette fonction de mani`ere similaire pour n’importe quel arbre binaire. #let rec nb_personnes_connues = function # MrouMme (nom,prenom,pere,mere) -> # 1 + nb_personnes_connues(pere) # + nb_personnes_connues(mere) | # Inconnu -> 0 ;; nb_personnes_connues : personne -> int = #nb_personnes_connues (ADupont);; - : int = 9

34

´ CHAPITRE 3. TYPES ET STRUCTURES DE DONNEES

Chapitre 4

Ordre Sup´ erieur 4.1

Abstraire par les fonctions

On se pose le probl`eme suivant : ´ecrire une fonction qui trie une liste d’´el´ements, quel que soit leur type. La seule connaissance dont on a besoin sur les ´el´ements est une relation d’ordre total, qui permet de les comparer deux ` a deux. En examinant les algorithmes usuels de tri, on constate que ce qui caract´erise chaque algorithme, c’est la m´ethode employ´ee pour comparer tous les ´el´ements entre eux, en les comparant deux ` a deux. Prenons l’exemple du tri par insertion, la m´ethode (r´ecursive) consiste `a remarquer qu’une liste vide a tous ses ´el´ements tri´es, et qu’une liste `a n ´el´ements peut ˆetre tri´ee en distinguant un de ses ´el´ements, puis en l’ins´erant ` a la bonne place, dans la liste tri´ee des n-1 autres ´el´ements. L’insertion n´ecessite de comparer l’´el´ement ` a ins´erer aux autres. Sachant que ceci caract´erise, de fa¸con intrins`eque, le tri par insertion, on souhaite pouvoir ´ecrire l’algorithme en faisant abstraction de la fonction de comparaison `a utiliser pour un type particulier d’´el´ements. L’objectif ´etant de n’´ecrire qu’une fonction de tri, utilisable pour tout type d’´el´ement. On peut exprimer cela, en sp´ecifiant que le tri est une fonction, qui a besoin pour s’ex´ecuter d’une liste d’´el´ements ` a trier et d’une fonction de comparaison entre ´el´ements, et qui donne une liste (tri´ee) d’´el´ements. En consid´erant la fonction de comparaison comme un param`etre suppl´ementaire, on ´evite d’´ecrire autant de fonctions de tri qu’il y a de types d’´el´ements. On a ainsi g´en´eralis´e l’algorithme de tri, en faisant abstraction de la fonction de comparaison. L’algorithme de tri sera de la forme : tri : liste d’elements * (element*element -> booleen) -> liste d’elements l, inf -> ... si inf (... , ...) alors ... D´ efinitions : On appelle fonction d’ordre sup´ erieur, une fonction dont le type comporte plus d’une fois le symbole fonctionnel ->. Les fonctions d’ordre sup´erieur peuvent avoir des fonctions en param`etres, donner des fonctions comme r´esultat, ou les deux `a la fois. Par ailleurs, rappelons qu’on dit qu’une fonction est polymorphe, si elle s’applique `a plusieurs types diff´erents de donn´ees. Exemples : L’op´erateur = est une fonction polymorphe, car il permet de tester l’´egalit´e d’entiers, de r´eels, de caract`eres ... La fonction de tri vue pr´ec´edemment est polymorphe car le type d’´el´ement n’est pas pr´ecis´e : on peut donc avoir des listes d’entiers, des listes de chaˆınes de caract`eres... 35

´ CHAPITRE 4. ORDRE SUPERIEUR

36

Ordre sup´ erieur et polymorphisme : L’ordre sup´erieur est un moyen efficace pour ´ecrire des fonctions polymorphes. Face ` a un probl`eme, pour lequel on dispose d’un algorithme g´en´eral, et pour lequel seuls quelques traitements d´ependent du type des donn´ees, on doit avoir la d´emarche suivante : ´ecrire une fonction d’ordre sup´erieur pour l’algorithme g´en´eral, en mettant en param`etres des fonctions pour les traitements particuliers. Par exemple, le calcul d’un pgcd dans un anneau euclidien par l’algorithme d’Euclide, peut ˆetre d´ecrit par une fonction d’ordre sup´erieur, ayant en param`etres les op´erations d´ependant du type des donn´ees (division sur Z ou Q[X]...). Fonction en r´ esultat : L’int´erˆet m´ethodologique d’une fonction qui a une fonction comme r´esultat, est d’´ecrire une “fonction abstraite”, qui appliqu´ee `a des donn´ees, va permettre de g´en´erer des fonctions. L’objectif est de n’´ecrire qu’une fonction, et d’en g´en´erer plusieurs. Ceci est possible quand, par abstraction, on constate que plusieurs fonctions “se ressemblent” et ne sont en fait que des instances particuli`eres d’une fonction plus g´en´erale. Soit `a ´ecrire les fonctions racine carr´ee, racine cubique, ... racine nieme. On pourrait bien sˆ ur ´ecrire une fonction de deux arguments, mais on pr´ef`ere, pour l’utilisateur pouvoir les fabriquer toutes. Au lieu de les ´ecrire, on ´ecrit une fonction d´ependant d’un entier n, et donnant une fonction calculant la racine nieme d’un nombre. De mani`ere analogue, on d´efinira l’addition dans Z/nZ comme une fonction qui `a un entier donn´e a associe la fonction d’addition dans Z/aZ. Sch´ emas de fonctions : On remarque que l’´ecriture de fonctions, pour un type donn´e, pr´esente souvent beaucoup de similarit´es. Par exemple, pour les listes, nombres de probl`emes se r´esolvent par un algorithme suivant le sch´ema : f :

l -> si vide (l) alors ... sinon ... premier(l) ...f(reste(l))...

Une fonction d’ordre sup´erieur permet d’´ecrire ce sch´ema, en rempla¸cant les pointill´es par des fonctions en param`etres. Fonctions de fonctions : Les math´ematiques, et en particulier l’analyse fonctionnelle, offrent beaucoup de probl`emes dans lesquels on manipule et on transforme explicitement des fonctions. Par exemple la fonction ◦ : f, g → f ◦ g, la fonction d´eriv´ee f → f 0 . Les fonctions d’ordre sup´erieur sont la formalisation naturelle, en informatique, des fonctions dans des espaces de fonctions.

4.2

Programmation d’ordre sup´ erieur

On a examin´e des situations de r´esolution de probl`eme, o` u une bonne m´ethodologie consiste `a abstraire des fonctions. Il nous reste maintenant `a ´etudier les m´ecanismes des langages permettant de mettre en oeuvre les fonctions d’ordre sup´erieur.

4.2.1

En Caml

Fonction en r´ esultat : L’ordre sup´erieur est tellement intrins`eque au langage Caml, qu’il est utilis´e jusque dans la r´ealisation des fonctions du langage, comme par exemple pour la fonction power. #power;; - : float -> float -> float = #let puissancede2 = power (2.0);;

´ 4.2. PROGRAMMATION D’ORDRE SUPERIEUR

37

puissancede2 : float -> float = #puissancede2 (10.0);; - : float = 1024.0 Application partielle : le langage Caml offre un m´ecanisme permettant d’´ecrire des “fonctions param´etriques” : en math´ematiques on passe souvent, par exemple, d’une fonction de 2 variables f (x, y) `a une fonction gx (y) d’une variable y, param´etr´ee par x, telle que gx (y) = f (x, y) ; g est alors une fonction qui ` a x associe gx , gx ´etant une fonction qui `a y associe f(x,y). C’est le cas de nombreuses fonctions de Caml dont la fonction power. La fonction power associe ` a un float, une fonction float->float. Pour l’utiliser il faut donc l’appliquer d’abord ` a un float, puis appliquer ceci `a un float. Le type de power doit ˆetre compris comme float ->(float -> float). On peut ´ecrire une fonction racine nieme, dont l’utilisation sera analogue `a celle de la fonction power : #let racineN = function n -> # function x -> power(x) (1./. float_of_int (n));; racineN : int -> float -> float = #let racine3 = racineN (3);; racine3 : float -> float = #racine3 (100.);; - : float = 4.64158883361 Le type de racineN doit ˆetre lu : int -> (float -> float). Le r´esultat de son application ` a l’entier 3 est une fonction de type float -> float, dont la d´efinition est : function x -> power(x) (1./. float_of_int (3)) La simplicit´e de l’´ecriture vient du fait qu’une fonction est consid´er´ee en Caml comme un cas particulier d’expression, ce qui permet d’´ecrire une fonction n’importe o` u dans un programme, o` u l’on peut ´ecrire une expression (ici, ` a l’endoit o` u l’on doit ´ecrire le r´esultat de la fonction). L’exemple suivant, est aussi une fonction d’ordre sup´erieur, donnant une fonction en r´esultat. Ce r´esultat peut ˆetre d´esign´e par un nom ou imm´ediatement appliqu´e `a des donn´ees : #let rec plusZnZ = function n -> # function (x, y) -> let p = x + y in # if p < 0 then plusZnZ (n)(x+n, y) # else if p < n then p # else plusZnZ (n)(x-n,y);; plusZnZ : int -> int * int -> int = #let plusZ5Z = plusZnZ (5);; plusZ5Z : int * int -> int = #plusZ5Z (4,3);; - : int = 2 #plusZnZ (3) (2,2);; - : int = 1 Le type de la fonction plusZnZ doit ˆetre lu : int->((int * int)->int). La derni`ere application doit ˆetre lue : (plusZnZ (3)) (2,2). Dans les types, l’op´erateur * est plus prioritaire que ->, et le parenth`esage par d´efaut est `a droite. Par contre, le parenth`esage par d´efaut est `a gauche dans les applications.

38

´ CHAPITRE 4. ORDRE SUPERIEUR

Une fonction f : type1->type2->type3 est appliqu´ee par : f(x)(y) o` u x est de type type1 et y de type type2. En reprenant le type polynome, d´efini en 3.3.2, on d´efinit la fonction qui `a un polynˆ ome associe la fonction polynˆ ome correspondante. #let rec horner = function (Nul,x) -> 0 | # (aplusXfois(a,p),x) -> a + x * horner(p,x);; horner : polynome * int -> int = #let fonction_polynome = function p -> # function x -> horner(p,x);; fonction_polynome : polynome -> int -> int = Fonctions en param` etres : On veut calculer une s´erie Σbi=a ui , connaissant a, b et le terme g´en´eral u, qui est une fonction int -> float. On utilise la fonction s´erie pour calculer une valeur 1 approch´ee de e = Σ∞ i=0 i ! #let rec serie = function (u, a, b) -> # if a = b then u (a) # else u (a) +. serie (u, a+1, b);; serie : (int -> float) * int * int -> float = #serie ((function n -> 1./. float_of_int (fact (n))), 0, 12);; - : float = 2.71828182829 L’exemple du tri par insertion prend une fonction en param`etre qui est transmise `a la fonction insertion. L’algorithme respecte les sp´ecifications donn´ees au paragraphe pr´ec´edent. #let rec insertion = function # (inf, x, []) -> [x] | # (inf, x, e::r) -> if inf (x,e) then x::e::r # else e::(insertion (inf,x,r));; insertion : (’a * ’a -> bool) * ’a * ’a list -> ’a list = #let rec tri = function # (inf, []) -> [] | # (inf, e::l) -> insertion (inf, e, tri(inf, l));; tri : (’a * ’a -> bool) * ’a list -> ’a list = #tri ((function (x,y)-> x int_of_char(a) # function [] -> neutre | # a::l -> opbinaire (a,

´ 4.2. PROGRAMMATION D’ORDRE SUPERIEUR

39

# generaliser(opbinaire,neutre)(l));; generaliser : (’a * ’b -> ’b) * ’b -> ’a list -> ’b = #let sigma = generaliser ((function x,y -> x + y), 0);; sigma : int list -> int = #sigma ([ 12; 45; 30; 22]);; - : int = 109 #let maximum = generaliser # ((function x,y -> if x int = #maximum([ 12; 45; 30; 22]);; - : int = 45

Fonctions de fonctions :

La composition de fonctions peut ˆetre d´efinie par :

#let rond = function (f,g) -> # function x -> f(g(x));; rond : (’a -> ’b) * (’c -> ’a) -> ’c -> ’b = #let racine = rond (sqrt, float_of_int);; racine : int -> float = #racine (10);; - : float = 3.16227766017 On notera dans le type calcul´e pour la fonction rond, que les trois variables de type ’a, ’b et ’c notent respectivement le type d’entr´ee de la premi`ere fonction (le mˆeme que le type de sortie de la seconde), son type de sortie (qui est aussi celui de la composition) et le type d’entr´ee de la deuxi`eme fonction (qui est aussi celui de la composition). L’exemple suivant calcule une valeur num´erique approch´ee de la d´eriv´ee d’une fonction sur les r´eels (on suppose que la d´eriv´ee existe) : #let derive = function f -> function x -> # let dx = 0.00001 in # ( f(x +. dx) -. f(x -. dx) ) /. (2.0 *. dx);; derive : (float -> float) -> float -> float = #let inv = derive (log);; inv : float -> float = #inv (3.);; - : float = 0.333333333336

4.2.2

En Pascal

L’utilisation de l’ordre sup´erieur est tr`es limit´e en Pascal. Les fonctions ne sont pas consid´er´ees comme des valeurs comme les autres, ce qui empˆeche d’avoir des fonctions en r´esultat de fonction. La seule possibilit´e d’ordre sup´erieur consiste `a passer des fonctions ou des proc´edures en param`etres de fonctions ou de proc´edures. Il faut pour cela sp´ecifier compl`etement le profil de la fonction param`etre, dans la liste des param`etres formels. Par exemple, on peut d´efinir un algorithme de tri selon le sch´ema suivant :

40

´ CHAPITRE 4. ORDRE SUPERIEUR

program tri; type vectentier = array[1..100]of integer; var vec : vectentier; ... function inferieur (a,b:integer): boolean; ... function superieur (a,b:integer): boolean; ... procedure tri_vecteur (var v : vectentier ; function comp (x,y:integer): boolean ); begin ... if comp (v[1], v[2]) then ... end; begin ... (* tri croissant *) tri (vec, inferieur); ... (* tri decroissant *) tri (vec, superieur); ... end.

Cette solution est limit´ee par le typage explicite des variables et fonctions pass´ees en param`etres : cela ne permet pas d’´ecrire un algorithme de tri g´en´erique, op´erant aussi bien sur des vecteurs d’entiers que de r´eels ou de chaˆınes (possible seulement avec certaines extensions de la norme Pascal).

Chapitre 5

Preuves de programmes Les objectifs de ce chapitre sont de donner des outils th´eoriques : la logique et l’induction, puis de les utiliser pour faire des raisonnements sur des programmes.

5.1

El´ ements de Logique

L’objet de la logique est d’´etudier des ´enonc´es, leurs preuves, en consid´erant uniquement leur forme et en faisant abstraction de leur sens. Son int´erˆet en informatique est de permettre de “m´ecaniser” le raisonnement sur les programmes. On va ´etudier une logique tr`es simple, permettant de mod´eliser les expressions bool´eennes.

Calcul des propositions On appelle proposition un ´enonc´e qui peut ˆetre soit vrai, soit faux. Par exemple, “3 < 0”, “la factorielle de 4 est 24”, “Socrate est un homme” sont des propositions. Pour faire abstraction du sens de ces propositions, on les notera par des symboles : P , Q... Ce qui nous int´eresse, c’est la mani`ere de combiner de telles propositions, pour faire des raisonnements. D´ efinition : L’ensemble des propositions est d´efini par les r`egles suivantes : – V , F sont des propositions, respectivement vraie et fausse, – les symboles P , Q... sont des propositions, dites propositions atomiques, – si a, b sont des propositions, alors a et b, a ou b, non a sont des propositions respectivement vraie ssi a est vraie et b est vraie, fausse ssi a est fausse et b est fausse, vraie ssi a est fausse, – toutes les propositions sont g´en´er´ees par les trois r`egles pr´ec´edentes. Connecteurs : et, ou, non sont appel´es des connecteurs. On peut d´efinir de nouveaux connecteurs : a ⇒ b par : (non a) ou b a ⇔ b par : (a et b) ou (non a et non b). Dans l’´ecriture d’une formule complexe, on pourra ne pas mettre toutes les parenth`eses, en consid´erant l’ordre croissant de priorit´e entre les connecteurs : ⇔, ⇒, ou, et, non. Table de v´ erit´ e : On peut repr´esenter la valeur de v´erit´e d’une proposition, d´ependant des valeurs des propositions atomiques qu’elle contient, par une table de v´erit´e : 41

42

CHAPITRE 5. P F F V V

Q F V F V

P et Q F F F V

P ou Q F V V V

non P V V F F

PREUVES DE PROGRAMMES

P⇒Q V V F V

P⇔Q V F F V

D´ efinitions : Une proposition est dite une tautologie, si elle a toujours la valeur de v´erit´e V . Les tautologies de la forme a ⇔ b sont particuli`erement int´eressantes, car elles montrent que les propositions a et b ont mˆemes valeurs de v´erit´e.

Alg` ebre de Boole L’ensemble des propositions muni de V , F et des op´erations et, ou, non est une alg`ebre de Boole. Ce point de vue est int´eressant car il donne les propri´et´es alg´ebriques suivantes (dont on aurait pu montrer que ce sont des tautologies en construisant les tables de v´erit´e), o` u a, b, c sont des propositions : Neutre Absorbant Commutativit´e Associativit´e Distributivit´e Idempotence Absorption Compl´ement

De Morgan

V et a F ou a F et a V ou a a et b a ou b a et(b et c) a ou(b ou c) a et(b ou c) a ou(b et c) a et a a ou a a et(a ou b) a ou(a et b) a et non a a ou non a non(non a) non(a et b) non(a ou b)

⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔ ⇔

a a F V b et a b ou a (a et b)et c (a ou b) ou c (a et b)ou(a et c) (a ou b) et (a ou c) a a a a F V a non a ou non b non a et non b

Formes canoniques Toute proposition peut s’´ecrire sous forme normale disjonctive (respectivement conjonctive), c’est `a dire sous la forme a1 ou...ou an (resp. a1 et...et an ), o` u les ai sont de la forme b1 et...et bp (resp. b1 ou...ou bp ), et o` u les bi sont des propositions atomiques ou des n´egations de propositions atomiques. Pour mettre une proposition sous forme normale disjonctive (resp. conjonctive), il faut : – Eliminer les connecteurs ⇔, ⇒, s’il y en a (en les rempla¸cant par leur d´efinition), – “D´eplacer” les n´egations vers les propositions atomiques (en utilisant les lois de De Morgan), – Mettre sous la forme ou(et...) (respectivement et(ou...)), en utilisant la distributivit´e. Exemple en caml : La d´efinition r´ecursive des propositions sugg`ere la d´efinition d’un type r´ecursif, pour les repr´esenter. Le type logique pr´esent´e en 3.2.1 convient parfaitement :

5.2. INDUCTION

43

#type logique = V | F | Et of logique*logique | Non of logique # | Ou of logique * logique | Prop of string ;; La fonction NierAtomes d´eplace les n´egations. On reconnaˆıtra dans le texte les lois de De Morgan. #let rec NierAtomes = function # Non (Et (x,y)) -> NierAtomes (Ou (Non x, Non y)) | # Non (Ou (x,y)) -> NierAtomes (Et (Non x, Non y)) | # Non (Non x) -> NierAtomes x | # Non V -> F | # Non F -> V | # Non (Prop x) -> Non (Prop x) | # Et (x, y) -> Et (NierAtomes(x), NierAtomes(y)) | # Ou (x, y) -> Ou (NierAtomes(x), NierAtomes(y)) | # V -> V | # F -> F | # Prop x -> Prop x;; NierAtomes : logique -> logique =

La fonction Distribuer met sous la forme ou(et...) : #let rec Distribuer = function # Et(Ou(x,y), z) -> Ou (Distribuer(Et(x,z)), Distribuer(Et(y,z))) | # Et(z, Ou(x,y)) -> Ou (Distribuer(Et(z,x)), Distribuer(Et(z,y))) | # Et(x,y) -> if x = Distribuer(x) & y = Distribuer(y) then Et(x,y) # else Distribuer(Et(Distribuer(x),Distribuer(y))) | # x -> x ;; Distribuer : logique -> logique =

Voici un exemple de mise sous forme normale disjonctive : #let formule = Non (Ou (Non(Prop "P"), # Non (Ou (Non (Prop "Q"), Non(F)))));; #texte (formule);; - : string = "non (non P ou non (non Q ou non F))" #texte (Distribuer (NierAtomes (formule)));; - : string = "((P et non Q) ou (P et V))"

On pourrait aussi programmer les simplifications de formules contenant V , F (`a faire en exercice). Une fonction tr`es int´eressante est la fonction qui indique si une formule est une tautologie. Il est possible d’´ecrire cette fonction, car on dispose d’une m´ethode (les tables de v´erit´e) pour le savoir (`a noter que cette m´ethode est tr`es inefficace d`es que le nombre de symboles est grand) . On a ainsi montr´e que le calcul des propositions justifie des transformations et des preuves d’´equivalence sur les expressions bool´eennes. On peut utiliser cela, manuellement pour raisonner sur un programme, ou bien construire des proc´edures automatiques.

5.2

Induction

On a cit´e en 2.4.1 le principe de r´ecurrence sur N. On utilise des d´efinitions par r´ecurrence pour ´ecrire des fonctions r´ecursives sur N. Le principe de r´ecurrence est l’outil th´eorique permettant de raisonner sur des fonctions r´ecursives sur N : on le verra `a la section suivante.

44

CHAPITRE 5.

PREUVES DE PROGRAMMES

Cependant, l’utilisation de la r´ecursivit´e ne se limite pas au seul domaine des entiers naturels. La chapitre 3 a montr´e de nombreux exemples de fonctions r´ecursives op´erant sur des types de donn´ees eux-mˆemes d´efinis r´ecursivement. On a alors vu en 3.2.1 que l’´ecriture de telles fonctions reposait sur la structure inductive du type. Il y a une analogie entre “d´efinir une fonction en 0, et en fonction de sa valeur en n-1” et “d´efinir une fonction pour les constructeurs constants, et en fonction de ses valeurs pour les arguments d’une construction”. On aimerait poursuivre l’analogie en g´en´eralisant le principe de r´ecurrence sur N. C’est ce qui est fait par le principe d’induction structurelle, qui permet de raisonner sur des ensembles d´efinis par induction.

Ensembles d´ efinis par induction L’ensemble Z[X] des polynˆ omes (cf. 3.3.2) est d´efini par : – le polynˆ ome nul, not´e Nul est un polynˆ ome, – si a appartient ` a Z et P est un polynˆ ome, alors a + X * P est un polynˆ ome, – Z[X] ne contient que des objets obtenus en appliquant un nombre fini de fois les r`egles pr´ec´edentes. De mˆeme, on pourrait d´efinir l’ensemble P, des entiers naturels pairs, par : – 0 appartient ` a P, – si n appartient ` a P, alors n+2 appartient `a P, – P ne contient que des objets obtenus en appliquant un nombre fini de fois les r`egles pr´ec´edentes. Ces ensembles ont ´et´e d´efinis par induction. De fa¸con g´en´erale, d´efinir un ensemble E par induction consiste ` a donner un sch´ema comportant : – un ensemble d’´el´ements de base appartenant `a E, – des r`egles d’induction permettant de d´ecrire de nouveaux ´el´ements de E `a partir d’´el´ements de E, – une r`egle de fermeture (que l’on pourra omettre par la suite car c’est toujours la mˆeme) : E ne contient que des objets obtenus en appliquant un nombre fini de fois les r`egles pr´ec´edentes. Les types r´ ecursifs sont des ensembles d´ efinis par induction : les ´el´ements de base sont d´efinis par les constructeurs sans argument r´ecursif ; les r`egles d’induction sont d´efinies par les constructeurs comportant (au moins) un argument r´ecursif. Remarque : N est un ensemble d´efini par induction (axiomes de Peano) : – 0 appartient ` a N, – si n appartient ` a N, alors succ(n) appartient `a N, o` u succ(n) repr´esente n+1 – N ne contient que des objets obtenus en appliquant un nombre fini de fois les r`egles pr´ec´edentes.

Principe d’induction structurelle Soit E un ensemble d´efini par induction. Pour montrer que tous les ´el´ements de E v´erifient une propri´et´e P, il suffit de montrer que : – les ´el´ements de base de E v´erifient P, – pour toute r`egle d’induction f , si e1 , ...en ∈ E v´erifient P, alors l’´el´ement f (e1 , ...en ) v´erifie P. Le principe de r´ecurrence sur N n’est que le cas particulier du principe d’induction structurelle appliqu´e `a N d´efini selon les axiomes de Peano. On le rappelle ici. Pour montrer une propri´et´e P pour tout entier n ∈ N , il suffit de montrer que : – P (0) – pour tout n, P (n) ⇒ P (n + 1)

5.3. PREUVES ET TRANSFORMATIONS DE PROGRAMMES

45

La formulation suivante est ´equivalente : Pour montrer une propri´et´e P pour tout entier n ∈ N , il suffit de montrer que : pour tout n, si pour tout k < n on a P (k) alors on a P (n).

5.3

Preuves et transformations de programmes

Les th´eories pr´esent´ees au d´ebut de ce chapitre vont permettre des raisonnements sur les programmes.

Exemple de raisonnement utilisant la logique La logique permet de justifier les calculs sur des expressions bool´eennes. On consid`ere les expressions de comparaison comme des propositions atomiques, pour raisonner sur des formules logiques. Par exemple, on veut simplifier : (x >= 4) ou ((x < 4) et (y = x + 2)) On l’´ecrit sous la forme : P ou (non P et Q) avec P: x >= 4,

Q: y = x + 2

Or on peut montrer que : P ou(non P et Q) est ´equivalent `a : P ou Q. L’expression initiale peut donc se simplifier en : (x >= 4) ou (y = x + 2)

Exemple de raisonnement par r´ ecurrence Le principe de r´ecurrence va permettre de raisonner sur des fonctions r´ecursives. Soit f une fonction r´ecursive sur les entiers naturels, dont on veut prouver que le r´esultat est juste. Si on prouve que le r´esultat de f(0) est juste, et que si le r´esultat de f(n-1) est juste alors il en va de mˆeme pour f(n), alors le r´esultat de f sera prouv´e juste pour tout n. On peut aussi vouloir prouver que le calcul de f(n) se termine ; l’hypoth`ese de r´ecurrence sera alors “le calcul de f(0) se termine”, la phase d’induction sera : “si le calcul de f(n-1) se termine alors le calcul de f(n) se termine”. Objectifs : Raisonner sur des programmes ne doit pas ˆetre consid´er´e comme une activit´e th´eorique, d´econnect´ee de la pratique. Le raisonnement doit “fonder” la pratique de la programmation. On peut distinguer les situations suivantes, o` u le raisonnement sur les programmes est utile : – Prouver qu’un programme calcule bien le r´esultat voulu ; il faut pour cela que le r´esultat voulu soit sp´ecifi´e de mani`ere non ambig¨ ue (souvent en langage math´ematique), – Prouver qu’un programme se termine, – Trouver une relation de r´ecurrence, pour concevoir une fonction r´ecursive, – Prouver que deux programmes sont ´equivalents, i.e. ils calculent le mˆeme r´esultat (probl`eme r´eput´e difficile), – Transformer un programme, en un autre programme ´equivalent, mais plus efficace (par exemple en ´evitant de calculer plusieurs fois la mˆeme chose). Etude de cas On va ´etudier la division euclidienne sur Z. Connaissant a ∈ Z et b ∈ Z ∗ , on cherche q et r tels que : a = bq + r et 0 ≤ r < |b|. Cette sp´ecification d´ecrit bien, de fa¸con unique, la solution recherch´ee. Pour la calculer, il nous faut exhiber une relation de r´ecurrence. L’id´ee est d’essayer de se ramener au cas simple o` u

46

CHAPITRE 5.

PREUVES DE PROGRAMMES

0 ≤ a < |b|, on a alors la solution q = 0, r = a qui v´erifie : a = bq + r. Pour se ramener `a ce cas, on va choisir un nouveau couple a0 , b0 (selon les signes de a et de b on prendra a0 = a + b ou a0 = a − b et on prendra b0 = b) dont la division donne q 0 , r0 et calculer q, r en fonction de q 0 , r0 . On propose ainsi le programme suivant, que l’on cherchera ensuite `a prouver : #let rec division = function (a,b) -> # if (0<=a) & (a 0 # then let (qp,rp) = division (a-b,b) # in (1 + qp, rp) # else let (qp,rp) = division(a+b, b) # in (-1 + qp, rp) ;; division : int * int -> int * int = Preuve de correction si arrˆ et : Pour prouver ce programme par r´ecurrence, on va raisonner sur le nombre n d’appels r´ecursifs engendr´es par l’appel division(a,b). On va prouver que si l’ex´ecution se termine (apr`es n appels r´ecursifs), alors le r´esultat est correct. Pour n = 0, l’ex´ecution se termine sans appel r´ecursif si et seulement si 0 ≤ a < |b|. On a alors q = 0 et r = a, qui v´erifient bien a = bq + r et 0 ≤ r < |b|. Supposons que toute ex´ecution engendrant n − 1 appels r´ecursifs donne un r´esultat correct, montrons-le au rang n. Soit l’appel division(a,b) qui g´en`ere n appels r´ecursifs ; on a alors a < 0 ou a ≥ |b|. Prenons le cas a ∗ b > 0, l’hypoth`ese au rang n − 1 nous donne : a − b = qp ∗ b + rp et 0 ≤ rp < |b|. On en d´eduit a = (qp + 1) ∗ b + rp. Le r´esultat donn´e : q = 1 + qp, r = rp v´erifie donc a = bq + r et 0 ≤ r < |b|. Dans le cas a ∗ b ≤ 0, l’hypoth`ese au rang n − 1 nous donne : a + b = qp ∗ b + rp et 0 ≤ rp < |b|. On en d´eduit a = (qp − 1) ∗ b + rp. Le r´esultat donn´e : q = −1 + qp, r = rp v´erifie donc a = bq + r et 0 ≤ r < |b|. CQFD. Preuve d’arrˆ et : Montrons maintenant que tout appel division(a,b) pour a ∈ Z et b ∈ Z ∗ se termine. Pour cela on va associer ` a la suite des appels r´ecursifs, une suite d’entiers positifs strictement d´ecroissante, qui est donc n´ecessairement finie. Si a ≥ |b|, on prend la suite des valeurs de a pour les appels successifs. La valeur suivante est a − b si b > 0 ; on a 0 ≤ a − b < a. La valeur suivante est a + b si b < 0 ; on a alors 0 ≤ a + b < a. On a donc bien, dans les deux cas, une suite positive strictement d´ecroissante. Si a < 0, on prend la suite des valeurs de −a + |b| pour les appels successifs. La valeur suivante est −(a − b) + |b| si b < 0 ; on a 0 ≤ −(a − b) + |b| < −a + |b|, car −(a − b) + |b| = −a. La valeur suivante est −(a + b) + |b| si b > 0 ; on a alors 0 ≤ −(a + b) + |b| < −a + |b|, car −(a + b) + |b| = −a. On a bien l`a aussi, dans les deux cas, une suite positive strictement d´ecroissante, ce qui termine la d´emonstration. Remarque : La preuve d’un algorithme r´ecursif comporte g´en´eralement ces deux aspects : – preuve par r´ecurrence que tous les appels v´erifient une certaine propri´et´e, que l’on appellera “propri´et´e invariante”, (dans l’exemple a = bq + r, 0 ≤ r < |b|) ; cette preuve permet de dire que l’algorithme calcule le bon r´esultat s’il se termine. – preuve que l’ex´ecution se termine parce qu’une propri´et´e dite “propri´et´e variante” vient `a ˆetre v´erifi´ee (dans l’exemple 0 ≤ a < |b|). Cette preuve peut ˆetre faite, comme dans cet exemple, en exhibant une suite enti`ere positive d´ecroissante.

Preuves et types r´ ecursifs Pour les types r´ecursifs, qui sont des ensembles d´efinis par induction, les preuves de programmes peuvent souvent se faire par induction structurelle.

5.3. PREUVES ET TRANSFORMATIONS DE PROGRAMMES

47

Reprenons l’exemple des polynˆ omes sur Z[X], pour prouver la fonction horner. #type polynome = Nul | aplusXfois of int * polynome;; #let rec horner = function (Nul,x) -> 0 | # (aplusXfois(a,p),x) -> a + x * horner(p,x);; – Pour prouver que horner(p,x) donne le bon r´esultat si l’ex´ecution se termine, il suffit de prouver que : – horner(Nul,x) = 0 – si horner(p,x) calcule p(x) alors horner(aplusXfois(a,p),x) calcule (a + x ∗ p)(x) – Pour prouver que l’ex´ecution de horner(p,x) se termine, il suffit de prouver que : – le calcul de horner(Nul,x) se termine, – si le calcul de horner(p,x) se termine, alors le calcul de horner(aplusXfois(a,p),x) se termine. Toutes ces preuves sont triviales. Les principes ´enonc´es aux chapitres 2 et 3, pour bien programmer r´ecursivement (penser aux cas de base...), sont en fait les conditions n´ecessaires et suffisantes de la preuve.

Transformations de programmes Les d´efinitions suivantes de la fonction longueurpaire sont ´equivalentes. On passe d’une solution `a la suivante par une simple transformation, en gardant le mˆeme sens. On remarquera la distance qui s´epare la solution initiale de la derni`ere solution. #let rec longueurpaire = function l -> # if l = [] then true else # if tl(l) = [] then false # else longueurpaire(tl (tl (l)));; #let rec longueurpaire = function l -> # if l = [] then true else # (function tll -> if tll = [] then false # else longueurpaire(tl (tll)))(tl(l));; #let rec longueurpaire = function l -> # if l = [] then true else # longueurimpaire (tl(l)) #and longueurimpaire = function l -> if l = [] then false # else longueurpaire (tl (l));; #let rec longueurpaire = function l -> # l = [] or longueurimpaire (tl(l)) #and longueurimpaire = function l -> # not (l = []) & longueurpaire (tl (l));;

On peut par transformations successives, de l’un en l’autre, prouver l’´equivalence de deux programmes. La preuve de l’´equivalence de deux programmes dans le cas g´en´eral (quand on ne sait pas transformer l’un en l’autre) ne sera pas abord´ee dans ce cours.

48

CHAPITRE 5.

PREUVES DE PROGRAMMES

Chapitre 6

Conclusion Ce cours, ainsi que celui du module Informatique 1, s’est concentr´e sur la conception d’algorithmes et la programmation, qui sont au coeur de la discipline informatique. Deux styles d’expression des algorithmes, imp´eratif (it´eratif) et fonctionnel (r´ecursif), ont ´et´e abord´es. Ils sont compl´ementaires et peuvent donc ˆetre choisis selon la nature du probl`eme. Le choix des langages de programmation ´etudi´es est justifi´e p´edagogiquement par leur ad´equation chacun `a un style d’expression particulier (imp´eratif en Pascal, fonctionnel en Caml). On peut cependant faire de la programmation fonctionnelle en Pascal (ce qui a ´et´e vu) et de la programmation imp´erative en Caml (voir [WL99]), ou utiliser d’autres langages (Lisp, Scheme, C...). L’essentiel est d’avoir une d´emarche scientifique d’analyse du probl`eme, de savoir abstraire les donn´ees (par cr´eation de types) et les traitements (par des fonctions d’ordre sup´erieur), pour obtenir un algorithme correct et ensuite le traduire dans un langage particulier. Un des objectifs majeurs de ce cours ´etait d’introduire la n´ecessit´e de raisonner pour programmer. Cet objectif sera poursuivi dans le module Informatique 3, par l’´etude de la complexit´e des algorithmes, la preuve de programmes imp´eratifs, l’´equivalence entre r´ecursion et it´eration. Au travers d’exemples, on a ouvert des portes vers certains domaines de l’informatique, qui tous utilisent la conception d’algorithmes : – les quelques exemples math´ematiques n’ont permis que d’entrevoir les difficult´es du calcul num´erique et du calcul formel ; c’est le domaine de l’algorithmique math´ematique ; – les manipulations d’expressions arithm´etiques et logiques (sous forme d’arbres) ne constituent qu’un aper¸cu de ce que peut faire un compilateur pour repr´esenter et transformer un programme ; c’est le domaine de l’´etude des langages et de la compilation ; – le calcul des propositions n’est que le premier maillon vers la d´emonstration automatique, et ce qui est commun´ement appel´e “intelligence artificielle” (on devrait plutˆ ot parler de simulation de raisonnement). Ce panorama ne pr´etend pas ˆetre exhaustif. Il est destin´e seulement `a appr´ehender l’informatique en tant que discipline, et en particulier `a introduire quelques domaines abord´es en 2`eme ann´ee et en second cycle informatique.

49

50

CHAPITRE 6. CONCLUSION

Annexe A

Syntaxe simplifi´ ee du langage Caml On donne seulement la syntaxe du sous-ensemble du langage Caml consid´er´e dans le module (pour la syntaxe compl`ete, voir [WL93]). Conventions lexicales. – Les commentaires s’´ecrivent : (* ceci est un commentaire *) – Les identificateurs : ident : := lettre {lettre | 0...9 | } lettre : := A...Z | a...z – Les entiers : [-] {0...9}+ – Les nombre d´ecimaux : [-] {0...9}+ [. {0...9}] [(e | E) [+ | -] {0...9}+] – Les caract`eres s’´ecrivent entre ‘, par exemple : ‘a‘ – Les chaˆınes de caract`eres s’´ecrivent entre ”, par exemple : ”bonjour” – Les mots cl´es sont : and, as, begin, do, done, downto, else, end, exception, for, fun, function, if, in, let, match, mutable, not, of, or, prefix, rec, then, to, try, type, value, where, while, with. – Sont consid´er´es commme blancs : espace, saut de ligne, tabulation, retour chariot, saut de page.

51

´ DU LANGAGE CAML ANNEXE A. SYNTAXE SIMPLIFIEE

52 Expressions, filtrage, liaison. expression ::=

Leurs formes sont d´efinies par :

identificateur

variable

|

constante

constante (y compris constructeur 0-aire)

|

( expression )

|

expression , expression { , expression }

n-uplet

|

constructeur expression

valeur construite

|

expression : : expression

liste avec premier et reste

|

[ expression { ; expression } ]

liste non vide

|

{ ´etiquette = expression { ; ´etiquette = expression } }

enregistrement

|

expression expression

application de fonction

|

op´erateur-pr´efixe expression

op´eration unaire

|

expression op´erateur-infixe expression

op´eration binaire

|

expression . ´etiquette

acc`es ` a un champ

|

if expression then expression else expression

alternative

|

match expression with filtrage

choix selon des motifs

|

function filtrage

fonction

|

let [ rec ] liaison { and liaison } in expression

expression avec d´efinition locale liste de cas

filtrage

::=

motif → expression { | motif → expression }

liaison

::=

motif = expression

Les op´erations suivantes sont class´ees par ordre de priorit´e d´ecroissante :

53 Op´eration application construction − −. mod ∗ ∗ . / /. + + . − −. :: @ ˆ = <> < <= > >= not & or , if let match function

Associativit´e droite – – gauche gauche gauche droite droite droite gauche – gauche gauche – – –

Comportement

Oppos´e entier et d´ecimal (op´erateurs pr´efixes) Modulo entier Multiplication et division, enti`eres et d´ecimales Addition et soustraction, enti`eres et d´ecimales Construction de liste Concat´enation de listes Concat´enation de chaˆınes Comparaisons non logique et logique ou logique N-uplets Alternative

´ DU LANGAGE CAML ANNEXE A. SYNTAXE SIMPLIFIEE

54 Motifs.

Leur forme est d´efinie par :

motif

::= |

identificateur

variable

constante

constante (y compris constructeur 0-aire) n’importe quoi

| |

( motif )

|

motif | motif

l’un ou l’autre

|

constructeur motif

filtre une valeur construite

|

motif : : motif

liste avec premier et reste

|

[ motif { ; motif } ]

liste non vide

|

[]

liste vide

|

motif , motif { , motif }

n-uplet

|

{ ´etiquette = motif { ; ´etiquette = motif } }

enregistrement

D´ efinitions de types. La forme d’une phrase de d´efinition de type est d´efinie par : phrase-type

::=

type def-type { and def-type }

phrase de d´efinition

def-type

::=

identificateur = def-constr { | def-constr }

somme

identificateur = { def-champ { ; def-champ } }

produit (enregistrement)

identificateur

constructeur 0-aire

|

identificateur of expr-type

constructeur n-aire

def-champ

::=

identificateur : expr-type

champ (enregistrement)

expr-type

::=

nom-de-type

voir ci-apr`es

|

( expr-type )

|

expr-type { * expr-type }+

produit cart´esien de types

|

expr-type list

liste d’un type

|

def-constr

::=

o` u nom-de-type est soit un type pr´ed´efini (int, float, char, string, bool) soit un type d´ej`a d´efini par l’utilisateur. Phrases. La forme d’une phrase est d´efinie par : phrase

::= |

expression phrase-type

d´efinition de type

55 |

let [ rec ] liaison { and liaison }

d´efinition globale

56

´ DU LANGAGE CAML ANNEXE A. SYNTAXE SIMPLIFIEE

Bibliographie [AS89]

H. Abelson et G. Sussman. Structure et interpr´etation des programmes informatiques. InterEditions, 1989.

[HHDGV92] T. Haccart-Hardin et V. Donzeau-Gouge-Vigui´e. Concepts et outils de programmation. InterEditions, 1992. [SFLM93]

P.C. Scholl, M.C. Fauvet, F. Lagnier et F. Maraninchi. Cours d’informatique : langages et programmation. Masson, 1993.

[WL93]

P. Weiss et X. Leroy. Manuel de r´ef´erence du langage Caml. InterEditions, 1993.

[WL99]

P. Weiss et X. Leroy. Le langage Caml. InterEditions, 1999.

[Xuo92]

N. H. Xuong. Math´ematiques discr`etes et informatique. Masson, 1992.

57