Put and . Then . Unlike the Curry fixed-point combinator, every finite reduct retains a closed subterm . Contracting this subterm recreates one; every other generated redex substitutes a variable and preserves it. The Church-Rosser theorem therefore proves .
With , the combinator satisfies . Every finite reduct of is, up to alpha equivalence, : the remaining copy of is its only beta-redex.
Every lambda term has a fixed point: the termsatisfies . Equivalently, a fixed-point combinator such assatisfies for every .
The set of fixed-point combinators is recursively enumerable. Enumerate closed lambda terms and finite proofs of beta equivalence, and output whenever a proof of appears for a fresh variable .
Articles by others on the same topic
A **fixed-point combinator** is a higher-order function that computes the fixed point of other functions. In simpler terms, it allows you to find a point that satisfies the condition \( f(x) = x \) for a given function \( f \). This concept is particularly important in functional programming, recursion, and lambda calculus, where named functions may not always be available due to the nature of the constructs used.