Lambda-calcul
système formel de la logique mathématique / De Wikipedia, l'encyclopédie encyclopedia
Cher Wikiwand IA, Faisons court en répondant simplement à ces questions clés :
Pouvez-vous énumérer les principaux faits et statistiques sur Λ-calcul?
Résumez cet article pour un enfant de 10 ans
Le lambda-calcul (ou λ-calcul) est un système formel inventé par Alonzo Church dans les années 1930, qui fonde les concepts de fonction et d'application. On y manipule des expressions appelées λ-expressions, où la lettre grecque λ est utilisée pour lier une variable. Par exemple, si M est une λ-expression, λx.M est aussi une λ-expression et représente la fonction qui à x associe M.
Le λ-calcul a été le premier formalisme pour définir et caractériser les fonctions récursives : il a donc une grande importance dans la théorie de la calculabilité, à l'égal des machines de Turing[1] et du modèle de Herbrand-Gödel. Il a depuis é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.