Fixed-point combinator

Tools: Rocq (formerly Coq)

• (Lambda calculus, Semantics) A Combinator that finds a fixed-point of a functional (a function that takes a function and returns another function). There are many such combinators, such as the Curry/Y-Combinator or the Z-combinator. Formally, a fixed-point combinator is a combinator $\text{fix}$ such that for any functional $g$, $\text{fix}g$ is beta/eta-equivalent to $g(\text{fix}g)$.