lambdaway
::
lc_french
3
|
list
|
login
|
load
|
|
_h1 [[lambda_calculus]] | facts for kids _p From [[kiddle|https://kids.kiddle.co/Lambda_calculus]] _p In mathematical logic and computer science, lambda calculus, also λ-calculus, is a formal system. It was designed to investigate the definition of functions, and how to apply them. It is also a tool for analysing recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s. Church used lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. _p Lambda calculus can be used to define what is a computable function. No general algorithm can answer the question of whether two lambda calculus expressions are equivalent. This was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, such as LISP, ML and Haskell. _p Lambda calculus can be called the smallest universal programming language. It consists of just one transformation rule (variable substitution) and just one way to define a function. Each function definition comes together with a list of the function's parameters, i.e. variables that can be used inside that definition. Variable substitution means substitution of values for variables, that is, a transformation step where an application of a function to some arguments is replaced with that function's definition in which all variables (that appear in its list of parameters) are replaced with arguments used in that application. _p Lambda calculus is universal in the sense that any computable function can be expressed and evaluated using this formalism. It is thus the same as the Turing machine formalism. However, lambda calculus emphasizes the use of transformation rules. It does not care about the actual machine that implements them. It is an approach more related to software than to hardware. {hr} _h2 french _p En logique mathématique et en informatique, le lambda-calcul, également λ-calcul, est un système formel. Il a été conçu pour étudier la définition des fonctions, et la manière de les appliquer. C'est également un outil d'analyse de la récursion. Il a été introduit par Alonzo Church et Stephen Cole Kleene dans les années 1930. Church a utilisé le lambda calculus en 1936 pour donner une réponse négative au [[Entscheidungsproblem|https://fr.wikipedia.org/wiki/Problème_de_la_décision]]. _p Le lambda calculus peut être utilisé pour définir ce qu'est une fonction calculable. Aucun algorithme général ne peut répondre à la question de savoir si deux expressions en lambda calculus sont équivalentes. Il s'agit de la première question, avant même le problème de la halte, pour laquelle l'indécidabilité a pu être prouvée. Le lambda calculus a grandement influencé les langages de programmation fonctionnelle, tels que LISP, ML et Haskell. _p Le lambda calculus peut être considéré comme le plus petit langage de programmation universel. Il se compose d'une seule règle de transformation (substitution de variable) et d'une seule façon de définir une fonction. Chaque définition de fonction est accompagnée d'une liste des paramètres de la fonction, c'est-à-dire des variables qui peuvent être utilisées dans cette définition. La substitution de variables signifie la substitution de valeurs aux variables, c'est-à-dire une étape de transformation où l'application d'une fonction à certains arguments est remplacée par la définition de cette fonction dans laquelle toutes les variables (qui apparaissent dans sa liste de paramètres) sont remplacées par les arguments utilisés dans cette application. (Noter qu'on ne parle pas de variables libres, de fermeture ...) _p Le lambda calculus est universel dans le sens où toute fonction calculable peut être exprimée et évaluée à l'aide de ce formalisme. Il est donc identique au formalisme de la machine de Turing. Cependant, le lambda calculus met l'accent sur l'utilisation de règles de transformation. Il ne se soucie pas de la machine réelle qui les met en œuvre. Il s'agit d'une approche plus liée au logiciel qu'au matériel. _p See also [[kidscodecs|https://kidscodecs.com/lambda-calculus/]], [[standford|https://crypto.stanford.edu/~blynn/lambda/]], ...
lambdaway v.20211111