 Fixed-point theorem for the untyped lambda calculus

ID: fixed-point-theorem-for-the-untyped-lambda-calculus

F

X = (λ x . F (xx)) (λ x . F (xx))

satisfies

X \equiv_{β} F (X)

Y = λ f . (λ x . f (xx)) (λ x . f (xx))

satisfies

Y F \equiv_{β} F (Y F)

for every

F

 New to topics? Read the docs here!