Skip to main content
2 of 7
made "fix" mathsf
Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58

Strengthening the hypotheses on $P$ and $Q$ from a fixed point property (every endofunction has some fixed point) to the existence of a fixed point operator $\mathsf{fix}$) with $$ \text{for any } f:P\to P, \qquad f({\mathsf{fix}}(f)) = {\mathsf{fix}}(f), $$ there is a standard theorem in domain theory or lambda calculus (theoretical computer science) due to Hans Bekić.

We are given $h:P\times Q\to P\times Q$. Define $$ f = \lambda x.{\mathsf{fix}}_P(\lambda y.\pi_1(h(x,y))) : P\to Q $$ $$ g = \lambda y.{\mathsf{fix}}_Q(\lambda x.\pi_0(h(x,y))) : Q\to P $$ which have the properties that $$ f x = \pi_1(h(x,f x)) \quad\text{and}\quad g y = \pi_0(h(g y,y)). $$ Now let $x_0 = {\mathsf{fix}}_P(\lambda x.g(f x))$ and $y_0=f(x_0)$, so $x_0=g(y_0)$. Then $$ \pi_0(h(x_0,y_0)) = \pi_0(h(g y_0,y_0) = g(y_0) = x_0 $$ $$ \pi_1(h(x_0,y_0)) = \pi_1(h(x_0,f x_0) = f(x_0) = y_0 $$ so $(x_0,y_0)$ is a fixed point of $h$.

In fact $f$ and $g$ are variables in this, so the argument provides a fixed point operator for $P\times Q$.

Paul Taylor
  • 8.5k
  • 1
  • 29
  • 58