Lambda-calcul

Le lambda-calcul, défini par Alonzo Church dans les années 1930, est une formalisation de la notion de calcul. Toute fonction calculable par une machine de Turing peut également être formulée et calculée au moyen du lambda-calcul, et réciproquement : c’est la thèse de Church-Turing, qui affirme que ces deux modèles de calcul sont équivalents. Le lambda-calcul peut aussi être considéré comme un langage de programmation abstrait et, à ce titre, il appartient aux fondements théoriques de la programmation, notamment pour la définition des langages de programmation fonctionnels.