Le lambda-calcul a été développé en
1930 par Church dans un but
double :
d'une part décrire un formalisme de représentation des
fonctions mathématiques,
d'autre part lui adjoindre quelques principes de logique afin de
développer une théorie qui puisse faire office de fondements aux
mathématiques.
Actuellement, les objets que manipule le mathématicien ne sont que
des ensembles. Par exemple un nombre réel est un ensemble de
rationnels (précisément, l'ensemble des rationnels qui le
minorent), un nombre rationnel est lui-même un couple de deux
entiers, or le couple (a,b) est défini comme étant l'ensemble
{a,{a,b}}. Enfin un entier est aussi un ensemble, 0 étant
par définition l'ensemble vide et si 0, ..., n sont définis, on
pose n+1={0, ..., n}. Ces ensembles sont les objets de base et
pour les manipuler le mathématicien dispose des ce qu'on appelle
communément les «axiomes de la théorie des
ensembles». L'alternative recherchée était donc de fonder les
mathématiques non plus sur les ensembles mais sur les fonctions. On
verra en effet plus loin comment on peut représenter les objets
mathématiques usuels (couples, entiers, etc...) par des termes du
lambda-calcul.
[...]
Vous pouvez obtenir l'intégralité de cet article
en version PostScript: