Questions tagged [lambda-calculus]
For questions on the formal system in mathematical logic for expressing effective functions, programs and computation, and proofs, using abstract notions of functions and combining them through binding and substitution.
4 questions
24
votes
0
answers
3k
views
What's the smallest $\lambda$-calculus term not known to have a normal form?
For Turing Machines, the question of halting behavior of small TMs has been well studied in the context of the Busy Beaver function, which maps n to the longest output or running time of any halting n ...
- 1,734
17
votes
3
answers
3k
views
What is the history of the Y-combinator?
Inspired by the comments to this question, I wonder if someone can explain the history of the fixed point combinator (often called the Y combinator) in lambda calculus.
Where did it first appear? ...
- 8,803
10
votes
2
answers
2k
views
Scott on the consistency of the lambda calculus
I have twice heard it attributed to Dana Scott that he said something to the effect that the consistency of the lambda-calculus was an accident.
Does anyone have a reasonable-sounding source for this?...
- 2,283
8
votes
1
answer
321
views
Is every total computable function definable by a normalizing lambda term?
$\newcommand{\nat}{\mathbb{N}}$
$\newcommand{\then}{\ \Longrightarrow\ }$
A partial function $f : \mathbb{N} \to \mathbb{N}$ is said to be $\lambda$-definable if there is a term $F \in \Lambda$ such ...
- 333