Concept
Lambda-calcul
Concepts associés (66)
Normal form (abstract rewriting)
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms. Stated formally, if (A,→) is an abstract rewriting system, x∈A is in normal form if no y∈A exists such that x→y, i.e. x is an irreducible term. An object a is weakly normalizing if there exists at least one particular sequence of rewrites starting from a that eventually yields a normal form.
Sémantique dénotationnelle
En informatique, la sémantique dénotationnelle est une des approches permettant de formaliser la signification d'un programme en utilisant les mathématiques. Parmi les autres approches, on trouve la sémantique axiomatique et la sémantique opérationnelle. Cette discipline a été introduite par Christopher Strachey et Dana Scott. En général, la sémantique dénotationnelle utilise des techniques de programmation fonctionnelle pour décrire les langages informatiques, les architectures et les programmes.
Algorithme
thumb|Algorithme de découpe d'un polygone quelconque en triangles (triangulation). Un algorithme est une suite finie et non ambiguë d'instructions et d’opérations permettant de résoudre une classe de problèmes. Le domaine qui étudie les algorithmes est appelé l'algorithmique. On retrouve aujourd'hui des algorithmes dans de nombreuses applications telles que le fonctionnement des ordinateurs, la cryptographie, le routage d'informations, la planification et l'utilisation optimale des ressources, le , le traitement de textes, la bio-informatique L' algorithme peut être mis en forme de façon graphique dans un algorigramme ou organigramme de programmation.
Categorical logic
NOTOC Categorical logic is the branch of mathematics in which tools and concepts from are applied to the study of mathematical logic. It is also notable for its connections to theoretical computer science. In broad terms, categorical logic represents both syntax and semantics by a , and an interpretation by a functor. The categorical framework provides a rich conceptual background for logical and type-theoretic constructions. The subject has been recognisable in these terms since around 1970.
Thèse de Church
La thèse de Church est une thèse concernant la définition de la notion de calculabilité. Dans une forme dite « physique », elle affirme que la notion physique de la calculabilité, définie comme étant tout traitement systématique réalisable par un processus physique ou mécanique, peut être exprimée par un ensemble de règles de calcul, défini de plusieurs façons dont on a pu démontrer mathématiquement qu'elles sont équivalentes.
Programmation logique
La programmation logique est une forme de programmation qui définit les applications à l'aide : d'une base de faits : ensemble de faits élémentaires concernant le domaine visé par l'application, d'une base de règles : règles de logique associant des conséquences plus ou moins directes à ces faits, d'un moteur d'inférence (ou démonstrateur de théorème ) : exploite ces faits et ces règles en réaction à une question ou requête. Cette approche se révèle beaucoup plus souple que la définition d'une succession d'instructions que l'ordinateur exécuterait.
Function application
In mathematics, function application is the act of applying a function to an argument from its domain so as to obtain the corresponding value from its range. In this sense, function application can be thought of as the opposite of function abstraction. Function application is usually depicted by juxtaposing the variable representing the function with its argument encompassed in parentheses. For example, the following expression represents the application of the function ƒ to its argument x.
Codage de Gödel
En logique mathématique, un codage de Gödel (ou numérotation de Gödel) est une fonction qui attribue à chaque symbole et formule bien-formée de certains langages formels un entier naturel unique, appelé son code de Gödel, ou numéro de Gödel. Le concept a été utilisé par Kurt Gödel pour la preuve de ses théorèmes d'incomplétude. Un codage de Gödel peut être interprété comme un codage dans lequel un numéro est attribué à chaque symbole d'une notation mathématique, après quoi une séquence d'entiers naturels peut alors représenter une séquence de symboles.
Fonction récursive
En informatique et en mathématiques, le terme fonction récursive ou fonction calculable désigne la classe de fonctions dont les valeurs peuvent être calculées à partir de leurs paramètres par un processus mécanique fini. En fait, cela fait référence à deux concepts liés, mais distincts. En théorie de la calculabilité, la classe des fonctions récursives est une classe plus générale que celle des fonctions récursives primitives, mais plus restreinte que celle des fonctions semi-calculables (ou partielles récursives).
Church encoding
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded data in the lambda calculus this way. Terms that are usually considered primitive in other notations (such as integers, booleans, pairs, lists, and tagged unions) are mapped to higher-order functions under Church encoding.