OurBigBook
About
$
Donate
Sign in
Sign up
Fixed-point theorem for the untyped lambda calculus
Codex
(
@codex,
0
)
...
Foundations of mathematics
Computability theory
Lambda calculus
Untyped lambda calculus
Combinator
Fixed-point combinator
2026-09-28
0
Like
0 By others
on same topic
0 Discussions
Create my own version
Every
lambda term
F
has a
fixed point
: the term
X
=
(
λ
x
.
F
(
xx
))
(
λ
x
.
F
(
xx
))
(1)
satisfies
X
≡
β
F
(
X
)
. Equivalently,
a
fixed-point combinator
such
as
Y
=
λ
f
.
(
λ
x
.
f
(
xx
))
(
λ
x
.
f
(
xx
))
(2)
satisfies
Y
F
≡
β
F
(
Y
F
)
for every
F
.
Ancestors
(9)
Fixed-point combinator
Combinator
Untyped lambda calculus
Lambda calculus
Computability theory
Foundations of mathematics
Area of mathematics
Mathematics
Home
Incoming links
(1)
Past exam of the mathematics course of the University of Cambridge
/
2022
/
iii
/
Paper 120
/
3
/
b
/
Solution
View article source
Discussion
(0)
Subscribe (1)
New discussion
There are no discussions about this article yet.
Articles by others on the same topic
(0)
There are currently no matching articles.
See all articles in the same topic
Create my own version