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.

Filter by
Sorted by
Tagged with
22 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 ...
John Tromp's user avatar
  • 1,679
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? ...
Dan Ramras's user avatar
  • 8,498
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?...
Charles Stewart's user avatar
8 votes
1 answer
307 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 ...
Andrew Polonsky's user avatar