Why Church chose lambda

Todd asked “Why [did Church choose] lambda and not some other Greek letter?”. Here are three answers:

1

The story is that in the 10s and 20s, mathematicians and logicians used ^ as a notation for set abstraction, as in ^i : i is prime. Church used ^` (i.e., a primed version of this symbol) for function abstraction, because functions are just sets with extra properties. The first type setter/secretary read it as λ and Church was fine with. True or not? I don’t know but it’s fun.

2

This paper (link provided by Dave Herman here):

(By the way, why did Church choose the notation “λ”? In [Church, 1964, §2] he stated clearly that it came from the notation “xˆ” used for class-abstraction by Whitehead and Russell, by first modifying “xˆ” to “ˆx” to distinguish function abstraction from class-abstraction, and then changing “ˆ” to “λ” for ease of printing. This origin was also reported in [Rosser, 1984, p.338]. On the other hand, in his later years Church told two enquirers that the choice was more accidental: a symbol was needed and “λ” just happened to be chosen.)

3

This paper (link provided by Dave Herman here):

We end this introduction by telling what seems to be the story how the letter ‘λ’ was chosen to denote function abstraction. In [100] Principia Mathematica the notation for the function f with f(x) = 2x + 1 is 2xˆ +1. Church originally intended to use the notation xˆ .2x+1. The typesetter could not position the hat on top of the x and placed it in front of it, resulting in ˆx.2x + 1. Then another typesetter changed it into λx.2x + 1.

3 thoughts on “Why Church chose lambda”

1. Your quote for #2 seems to be broken; it should be ‘x̂ ‘.
See also this email which gives more support to #2 (although again from J. Rosser):

Scheme took lambda from Lisp, whose creator, John McCarthy, took it from
Alonzo Church’s lambda calculus. According to Church’s student, J.
Barkley Rosser (“Highlights of the History of the Lambda-Calculus”,
Annals of the History of Computing 6,4 [1984], 337-349; at 338), Church
took the notation from Whitehead and Russell’s Principia Mathematica,
where the class of all x such that f(x) was written as xf(x) with a caret
(^) over the first x. Rosser continues: “Because the new concept
differed quite appreciably from class membership, Church moved the caret
from over the x down to the line just the left of the x; specifically
^xf(x). Later for reasons of typography, an appendage was added to the
caret to product a lambda; the result was xf(x).” (The original
has, of course, the Greek letter where I have written .)

2. Grant says:

Thanks Porges, more evidence and I fixed the quote.