L'algorithme de Huffman : mécaniser la preuve

Dans cours

Description

Cette séance de cours couvre la mécanisation de la preuve de manuel de l'algorithme de Huffman, en mettant l'accent sur le codage Huffman, les solutions optimales et la mise en œuvre fonctionnelle. Il traite des concepts de la feuille et des nœuds intérieurs, des fonctions auxiliaires de base et des lemmas intermédiaires. La séance de cours se termine par l'officialisation de la preuve, les règles d'induction personnalisée et l'extension proposée de la portée de la preuve aux demandes.

Connectez-vous pour regarder la vidéo

Enseignant

Source officielle

https://mediaspace.epfl.ch/media/0_4rdpm6bl

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Séances de cours associées (39)

Concepts associés (38)

Arbre binaire de recherche

En informatique, un arbre binaire de recherche ou ABR (en anglais, binary search tree ou BST) est une structure de données représentant un ensemble ou un tableau associatif dont les clés appartiennent à un ensemble totalement ordonné. Un arbre binaire de recherche permet des opérations rapides pour rechercher une clé, insérer ou supprimer une clé.

Arbre enraciné

En théorie des graphes, un arbre enraciné ou une arborescence est un graphe acyclique orienté possédant une unique racine, et tel que tous les nœuds sauf la racine ont un unique parent. En informatique, c'est également une structure de données récursive utilisée pour représenter ce type de graphes. Dans un arbre, on distingue deux catégories d'éléments : les feuilles (ou nœuds externes), éléments ne possédant pas de fils dans l'arbre ; les nœuds internes, éléments possédant des fils (sous-branches).

Self-balancing binary search tree

In computer science, a self-balancing binary search tree (BST) is any node-based binary search tree that automatically keeps its height (maximal number of levels below the root) small in the face of arbitrary item insertions and deletions. These operations when designed for a self-balancing binary search tree, contain precautionary measures against boundlessly increasing tree height, so that these abstract data structures receive the attribute "self-balancing".

Algorithme de Rémy

L'algorithme de Rémy est un générateur d'arbres binaires, dont la principale application est un algorithme efficace de génération aléatoire d'arbres binaires. L'algorithme doit son nom à son inventeur Jean-Luc Rémy. L'algorithme de Rémy est dû à Jean-Luc Rémy, chercheur au Centre de recherche en informatique de Nancy. Il a été créé en 1978 sans être publié immédiatement et a fait partie du folklore de l'algorithmique et de la combinatoire énumérative jusqu'à sa parution dans une revue francophone en 1985.

Arbre splay

Un arbre splay (ou arbre évasé) est un arbre binaire de recherche auto-équilibré possédant en outre la propriété que les éléments auxquels on a récemment accédé (pour les ajouter, les regarder ou les supprimer) sont rapidement accessibles. Ils disposent ainsi d'une complexité amortie en O(log n) pour les opérations courantes comme insertion, recherche ou suppression. Ainsi dans le cas où les opérations possèdent une certaine structure, ces arbres constituent des bases de données ayant de bonnes performances, et ceci reste vrai même si cette structure est a priori inconnue.