2018-02-23 18:58:03 +00:00
|
|
|
|
---
|
|
|
|
|
|
created_at: '2016-02-04T23:03:15.000Z'
|
|
|
|
|
|
title: Why Church chose lambda (2009)
|
|
|
|
|
|
url: http://www.wisdomandwonder.com/link/3022/why-church-chose-lambda
|
|
|
|
|
|
author: networked
|
|
|
|
|
|
points: 56
|
|
|
|
|
|
story_text:
|
|
|
|
|
|
comment_text:
|
|
|
|
|
|
num_comments: 9
|
|
|
|
|
|
story_id:
|
|
|
|
|
|
story_title:
|
|
|
|
|
|
story_url:
|
|
|
|
|
|
parent_id:
|
|
|
|
|
|
created_at_i: 1454626995
|
|
|
|
|
|
_tags:
|
|
|
|
|
|
- story
|
|
|
|
|
|
- author_networked
|
|
|
|
|
|
- story_11037982
|
|
|
|
|
|
objectID: '11037982'
|
2018-06-08 12:05:27 +00:00
|
|
|
|
year: 2009
|
2018-02-23 18:58:03 +00:00
|
|
|
|
|
|
|
|
|
|
---
|
2018-03-03 09:35:28 +00:00
|
|
|
|
Todd
|
|
|
|
|
|
[asked](http://list.cs.brown.edu/pipermail/plt-scheme/2009-May/033320.html)
|
|
|
|
|
|
“Why \[did Church choose\] lambda and not some other Greek letter?”.
|
|
|
|
|
|
Here are three
|
|
|
|
|
|
answers:
|
2018-02-23 18:19:40 +00:00
|
|
|
|
|
2018-03-03 09:35:28 +00:00
|
|
|
|
### 1
|
2018-02-23 18:19:40 +00:00
|
|
|
|
|
2018-03-03 09:35:28 +00:00
|
|
|
|
[Matthias](http://list.cs.brown.edu/pipermail/plt-scheme/2009-May/033321.html):
|
2018-02-23 18:19:40 +00:00
|
|
|
|
|
2018-03-03 09:35:28 +00:00
|
|
|
|
> 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](http://www-maths.swan.ac.uk/staff/jrh/papers/JRHHislamWeb.pdf)
|
|
|
|
|
|
(link provided by Dave Herman
|
|
|
|
|
|
[here](http://list.cs.brown.edu/pipermail/plt-scheme/2009-May/033322.html)):
|
|
|
|
|
|
|
|
|
|
|
|
> (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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.26.7908)
|
|
|
|
|
|
(link provided by Dave Herman
|
|
|
|
|
|
[here](http://list.cs.brown.edu/pipermail/plt-scheme/2009-May/033322.html)):
|
|
|
|
|
|
|
|
|
|
|
|
> 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.
|
