Définition par récurrencevignette|4 étapes de la construction d'un flocon de Koch. Comme beaucoup d'autres fractales, cette courbe est définie par récurrence. En mathématiques, on parle de définition par récurrence pour une suite, c'est-à-dire une fonction définie sur les entiers positifs et à valeurs dans un ensemble donné. Une fonction est définie par récurrence quand, pour définir la valeur de la fonction en un entier donné, on utilise les valeurs de cette même fonction pour des entiers strictement inférieurs.
Filtrage par motifLe filtrage par motif est la vérification de la présence de constituants d'un motif par un programme informatique, ou parfois par un matériel spécialisé. Par contraste avec la reconnaissance de forme, les motifs sont complètement spécifiés. De tels motifs concernent conventionnellement des séquences ou des arbres. Par exemple "HDpdf" peut signifier : "Toute chaîne contenant HD et se terminant par pdf".
Théorie des ensemblesLa théorie des ensembles est une branche des mathématiques, créée par le mathématicien allemand Georg Cantor à la fin du . La théorie des ensembles se donne comme primitives les notions d'ensemble et d'appartenance, à partir desquelles elle reconstruit les objets usuels des mathématiques : fonctions, relations, entiers naturels, relatifs, rationnels, nombres réels, complexes... C'est pourquoi la théorie des ensembles est considérée comme une théorie fondamentale dont Hilbert a pu dire qu'elle était un « paradis » créé par Cantor pour les mathématiciens.
Ensemblevignette|Ensemble de polygones dans un diagramme d'Euler En mathématiques, un ensemble désigne intuitivement un rassemblement d’objets distincts (les éléments de l'ensemble), « une multitude qui peut être comprise comme une totalité » pour paraphraser Georg Cantor qui est à l'origine de la théorie des ensembles. Dans une approche axiomatique, la théorie des ensembles est une théorie de l'appartenance (un élément d'un ensemble est dit « appartenir » à cet ensemble).
Sûreté du typageLa sûreté du typage est un principe permettant d'améliorer la qualité de la programmation. Dans les langages à typage statique, l'un des objectifs est d'intercepter les erreurs de type de données lors de la compilation. Un type peut être vu comme un ensemble de valeurs et un ensemble d'opérateurs. La programmation objet a introduit les notions d'objets, messages, classes, héritage. Il est tentant de faire coller les classes à des types.
Ensemble videvignette|Notation de l'ensemble vide. En mathématiques, l'ensemble vide est l'ensemble ne contenant aucun élément. L'ensemble vide peut être noté d'un O barré, à savoir ∅ ou simplement { }, qui est une paire d'accolades ne contenant qu'une espace, pour représenter un ensemble qui ne contient rien. La notation ∅ a été introduite par André Weil, dans le cadre de l'institution de notations par le groupe Bourbaki. Von Neumann dans son article de 1923, qui est l'une des premières références qui l'aborde, le note O.
Ensemble (informatique)En informatique, un ensemble ou set est un type abstrait qui peut stocker certaines valeurs, sans ordre particulier, et sans répétition. Il s'agit d'une mise en œuvre informatique de la notion mathématique d'ensemble fini. Un ensemble stocke des valeurs, sans ordre défini, et ne contient pas de données en double (la tentative d'insertion d'une donnée déjà présente est sans effet). Contrairement à la plupart des autres types de collections les ensembles sont plus utilisés pour tester l'appartenance d'une valeur à cet ensemble que pour en extraire des données.
Liste (informatique)En informatique, une liste est une structure de données permettant de regrouper des données de manière à pouvoir y accéder librement (contrairement aux et aux piles, dont l'accès se fait respectivement en mode FIFO et LIFO). La liste est à la base de structures de données plus complexes comme la pile, la , les arbres, etc. L'importance de la liste comme structure de données est telle qu'elle est à la base du langage de programmation Lisp (de l'anglais list processing).
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).
Intuitionistic type theoryIntuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and philosopher, who first published it in 1972. There are multiple versions of the type theory: Martin-Löf proposed both intensional and extensional variants of the theory and early impredicative versions, shown to be inconsistent by Girard's paradox, gave way to predicative versions.
Inférence de typesL'inférence de types est un mécanisme qui permet à un compilateur ou un interpréteur de rechercher automatiquement les types associés à des expressions, sans qu'ils soient indiqués explicitement dans le code source. Il s'agit pour le compilateur ou l'interpréteur de trouver le type le plus général que puisse prendre l'expression. Les avantages à disposer de ce mécanisme sont multiples : le code source est plus aéré, le développeur n'a pas à se soucier de retenir les noms de types, l'interpréteur fournit un moyen au développeur de vérifier (en partie) le code qu'il a écrit et le programme est peu modifié en cas de changement de structure de données.
MatitaMatita is an experimental proof assistant under development at the Computer Science Department of the University of Bologna. It is a tool aiding the development of formal proofs by man-machine collaboration, providing a programming environment where formal specifications, executable algorithms and automatically verifiable correctness certificates naturally coexist. Matita is based on a dependent type system known as the Calculus of (Co)Inductive Constructions (a derivative of Calculus of Constructions), and is compatible, to some extent, with Coq.
