Histoire de la notation lambda de Church

Gilles Dowek nous la conte dans son livre Les métamorphoses du calcul.

La notation habituelle pour les fonctions est maladroite car elle ne distingue pas la fonction de la valeur prise par la fonction en un certain point.

"Pour distinguer ces deux notions, on écrit aujourd'hui la fonction non x * x mais x |-> x * x.
Cette notation |-> aurait été introduire vers 1930 par Nicolas Bourbaki, [...]
A la même époque, Church a introduit une notation similaire : lambda x (x * x), dans laquelle la flèche |-> est remplacée par la lettre grecque lambda (2). La petite histoire raconte que cette notation vient d'une notation antérieure utilisée par Whitehead et Russell (3) dès les années 1900, x surmonté de ^ (x * x), mais que l'imprimeur (4) de Church, ne sachant pas imprimer d'accent circonflexe sur un x, l'avait fait précéder d'un symbole qui ressemblait à un accent circonflexe, le lambda majuscule, devenu par la suite minuscule.
Alors la notation x |-> x * x s'est imposée, on continue d'utiliser la notation de Church en logique et en informatique [...]"

(1) appelée maplet
(2) remplacer le mot lambda par la lettre grecque
(3) celui qui est l'auteur de la phrase que nous vous avons répétée : "en mathématique, on ne sait de quoi on parle et si ce que l'on dit est vrai". Voir notre exposé sur le concept de modèle.
(4) comme nous avec l'éditeur de blogger !