Lambda-calcul

Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930. Ce système fonde les concepts de fonction et d'application qui forment un cadre pour manipuler des expressions appelées λ-expressions. La lettre grecque λ est utilisée pour lier une variable. Par exemple, si M est une λ-expression, représentant la fonction qui associe à x l'expression M.

Le λ-calcul a été le premier formalisme pour définir et caractériser les fonctions récursives. Il revêt donc une grande importance dans la théorie de la calculabilité, au même titre que les machines de Turing^[1] et le modèle de Herbrand-Gödel. Depuis, il a été appliqué comme langage de programmation théorique et comme métalangage pour la démonstration formelle assistée par ordinateur. Le lambda-calcul peut être typé ou non.

Le lambda-calcul est apparenté à la logique combinatoire de Haskell Curry et se généralise dans les calculs de substitutions explicites.