Fixed-point combinator

Summary

A fixed-point combinator is a closed lambda term $Y$ such that $Y\, F$ is a fixed point of $F$ for every term $F$. This means that $Y\, F$ and $F\, (Y\, F)$ are equal under beta conversion. Fixed-point combinators exist in the untyped lambda calculus, the best known being Curry's $Y$ and Turing's $\Theta$. They make recursion possible in a language that has no names for functions. They do not exist in the simply typed lambda calculus, which is strongly normalizing.