« Introduction à la complexité et sa formalisation » : différence entre les versions

De Wiki du LAMA (UMR 5127)
Aller à la navigation Aller à la recherche
Aucun résumé des modifications
Aucun résumé des modifications
Ligne 100 : Ligne 100 :
== Tri en OCaml ==
== Tri en OCaml ==


Nous allons donc écrire différentes fonction de tri dans le langage OCaml.
=== Trie par insertion en OCaml ===


=== Trie par fusion en OCaml ===
=== Tri par insertion en OCaml ===

Tout d'abord, le tri par insertion consiste :

* Prendre en argument une liste à trier.
* prendre une liste vide.
* Prendre un élément de la liste non trier.
* Insérer cette élément au bonne endroit dans la liste vide ( il faut donc parcourir la liste).
* Puis on recommence le processus de sorte a trier cette liste et a renvoyer celle-ci.

Il faut donc avoir en tête que nous manipulons bien deux listes différentes pendant l'exécution.


Pour faire cela en OCaml nous avons besoin de la fonction d'insertion :

<pre>
let rec insert e l = match l with
[] -> [e]
| x :: l' -> if e <= x
then e :: l
else x :: (insert e l')
</pre>

Cette fonction est une fonction récursive qui s'appelle donc elle même. On peut donc voir que si la liste fournis est vide, alors elle renvoie l'élément e, sinon elle insert un élément au bonne endroit.


Nous avons ensuite besoin de la fonction de tri :

<pre>
let rec trie l = match l with
[] -> []
| e::l' -> insert e (trie l')
</pre>

Cette fonction est aussi une fonction récursive qui va appeler notre fonction d'insertion pour trier la liste fournis en argument.


Pour la <b>complexité</b> de cette fonction nous allons compter le maximum de tests que peut faire trie l.
On trouve que pour chaque élément de la liste l' le coût augmente de 1.

On se retrouve donc avec une complexité total qui correspond a la somme des élément de 1 a n-1 soit (n(n-1))/2 ce qui représente une complexité O(n²).
=== Tri par fusion en OCaml ===

Nous nous intéressons donc maintenant a une fonction de tri par fusion. Le principe de cette fonction est le suivant :

* On part d'une liste à trier.
* On effectue une suite de division récursives en deux parties jusqu'à obtenir des listes de taille 1.
* On tri en suite chaque liste.
* Puis on les fusionnes entre elles tout en les triant.


== Complexité en Agda/Calf ==
== Complexité en Agda/Calf ==

Version du 10 mai 2025 à 14:49

Étudiant : ALBRECHT Maël

Tuteur : HIRSCHOWITZ Tom

Introduction

Pour introduire notre sujet nous allons partir d'un exemple, imaginer que vous vouliez trier des fichiers dans votre ordinateur ( dans notre cas des fichiers numéroter et par exemple nous souhaitons les triés par ordre croissant). Pour effectuer cette tache vous pouvez donc créer un programme qui le ferra pour vous. Malheureusement, votre programme prend beaucoup de temps a s'exécuter. Pour résoudre ce problème on se tourne vers la complexité.

Complexité

La complexité permet de mesurer l'efficacité des fonctions. Elle dépend de différents critères tel que :

  • le temps de calcul séquentiel , c'est a dire le temps qui es mis pour exécuter toute les instructions une par une.
  • le temps de calcul parallèle , c'est a dire le temps qui es mis pour exécuter toute les instructions avec plusieurs processeur donc avec des opération exécuté en simultané.
  • l'esapace disque nécessaire a ces opération qui peut donc ralonger le temps d'execution d'une opérations.
  • ainsi que beaucoup d'autre paramètre...


Pour illustrer cela nous allons utiliser deux fonctions « identité » comme exemple.

On commence donc par définir un type d'entier unaires.

1.   type nat = Z | S of nat
2.   let one = S Z
3.   let two = S (S Z) (* etc.. *)

On programme ensuite une fonction identité simple :

1.   let id1 n = n

Et une fonction identité qui inspecte son argument, puis le reconstruit :

1.   let rec id2 n = match n with
2.   | Z -> Z
3.   | S p -> S (id2 p)

Complexité en temps

On s'intéresse au nombre d'étape de calcul en fonction de la taille de l'argument.

On fait souvent des hypothèses simplificatrices pour calculer une complexité, bien sur celle ci doive être simplificatrice mais rester vrai. Ici nous comptons le nombre de tests match ... with.

  • Pour id1 : 0.
  • Pour id2 : autant que la taille de l'argument.


Notation O

Nous allons en suite introduire la notation O (dite « grand o »).

Pour cela fixons des types A et B et une « manière de compter ».

On définis donc une fonction f: A -> B.

Cette fonction f nous permet de prendre la taille de a et de trouver le temps avec f(a) soit :

taille(a) -> temps(f(a))

Cela nous permet donc de trouver :

id1: n -> 1

id2: n -> n

Pour présenter cela nous utilisons la notation suivante :

  • Complexité de id1 : O(1)
  • Complexité de id2 : O(n)

Si l'on souhaite développer cela, nous pouvons prendre :

f ∈ O(g) qui signifie f(n) ≤ c * g(n)

Avec :

  • c une constante bien choisie
  • et pour tout n ≥ n_0

BigO.png

Langages utilisés

Pour créer nos différentes fonctions et comprendre leur complexité nous avons utiliser deux langage différent :

  • Le langage OCaml, un langage fonctionnel et fortement typé.
  • Le langage Agda, qui est un langage fonctionnel, typé et qui sert en partie programmer des preuves mathématiques.
  • On utilise aussi une extension d'Agda qui se nomme Calf et qui sert a calculer la complexité d'une fonction sous forme de coûts.

Tri en OCaml

Nous allons donc écrire différentes fonction de tri dans le langage OCaml.

Tri par insertion en OCaml

Tout d'abord, le tri par insertion consiste :

  • Prendre en argument une liste à trier.
  • prendre une liste vide.
  • Prendre un élément de la liste non trier.
  • Insérer cette élément au bonne endroit dans la liste vide ( il faut donc parcourir la liste).
  • Puis on recommence le processus de sorte a trier cette liste et a renvoyer celle-ci.

Il faut donc avoir en tête que nous manipulons bien deux listes différentes pendant l'exécution.


Pour faire cela en OCaml nous avons besoin de la fonction d'insertion :

let rec insert e l = match l with
[] -> [e]
| x :: l' -> if e <= x
  then e :: l
  else x :: (insert e l')

Cette fonction est une fonction récursive qui s'appelle donc elle même. On peut donc voir que si la liste fournis est vide, alors elle renvoie l'élément e, sinon elle insert un élément au bonne endroit.


Nous avons ensuite besoin de la fonction de tri :

let rec trie l = match l with
[] -> []
| e::l' -> insert e (trie l')

Cette fonction est aussi une fonction récursive qui va appeler notre fonction d'insertion pour trier la liste fournis en argument.


Pour la complexité de cette fonction nous allons compter le maximum de tests que peut faire trie l. On trouve que pour chaque élément de la liste l' le coût augmente de 1.

On se retrouve donc avec une complexité total qui correspond a la somme des élément de 1 a n-1 soit (n(n-1))/2 ce qui représente une complexité O(n²).

Tri par fusion en OCaml

Nous nous intéressons donc maintenant a une fonction de tri par fusion. Le principe de cette fonction est le suivant :

  • On part d'une liste à trier.
  • On effectue une suite de division récursives en deux parties jusqu'à obtenir des listes de taille 1.
  • On tri en suite chaque liste.
  • Puis on les fusionnes entre elles tout en les triant.

Complexité en Agda/Calf

Deux fonctions « identité »

Conclusion