Le lambda-calcul est un modèle de calcul entièrement fondé sur la notion de fonction, c’est-à-dire sur l’idée d’une opération qui reçoit quelque chose en entrée et renvoie un résultat. Là où la machine de Turing imite un dispositif mécanique parcourant un ruban, le lambda-calcul adopte un point de vue tout différent: calculer y consiste uniquement à définir des fonctions, à les appliquer à des arguments et à simplifier les expressions obtenues en remplaçant progressivement chaque fonction par ce qu’elle produit. Tout y est fonction, même les nombres et les opérations les plus élémentaires, qui se trouvent reconstruits à partir de ce seul ingrédient. Le nom vient de la lettre grecque lambda, employée dans la notation pour signaler qu’on est en train de définir une fonction.
Ce système a été mis au point par le logicien américain Alonzo Church au début des années 1930, quelques années avant que Turing ne propose sa machine, et dans le même but: donner une définition précise de ce que signifie calculer. Le fait remarquable, découvert peu après, est que le lambda-calcul et la machine de Turing, malgré des apparences totalement dissemblables, définissent exactement le même ensemble de fonctions calculables. Cette équivalence entre deux approches conçues indépendamment a fortement renforcé la conviction que ces définitions capturaient bien la notion intuitive de calcul, conviction résumée aujourd’hui sous le nom de thèse de Church-Turing.
Loin d’être resté une simple curiosité logique, le lambda-calcul est devenu le fondement théorique de toute une famille de langages de programmation dits fonctionnels, comme Lisp, Haskell ou OCaml, dans lesquels on programme précisément en composant et en appliquant des fonctions. Ses idées ont profondément marqué la conception des langages modernes, y compris ceux qui ne sont pas purement fonctionnels, en particulier la manière de traiter les fonctions comme des objets manipulables à part entière. Il occupe aussi une place centrale dans les recherches sur les fondements des mathématiques et sur la vérification des programmes, où sa rigueur permet de raisonner formellement sur ce que fait réellement un morceau de code.
Laisser un commentaire