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)$.