Bekić's theorem

In computability theory, Bekić's theorem or Bekić's lemma is a theorem about fixed-points which allows splitting a mutual recursion into recursions on one variable at a time.[1][2][3] It was created by Austrian Hans Bekić (1936-1982) in 1969,[4] and published posthumously in a book by Cliff Jones in 1984.[5]

The theorem is set up as follows.[1][4] Consider two operators ${\displaystyle f:P\times Q\to P}$ and ${\displaystyle g:P\times Q\to Q}$ on pointed directed-complete partial orders ${\displaystyle P}$ and ${\displaystyle Q}$, continuous in each component. Then define the operator ${\displaystyle (f,g)(x,y)=(f(x,y),g(x,y))}$. This is monotone with respect to the product order (componentwise order). By the Kleene fixed-point theorem, it has a least fixed point ${\displaystyle \mu (x,y).(f,g)(x,y)}$, a pair ${\displaystyle (x_{0},y_{0})}$ in ${\displaystyle P\times Q}$ such that ${\displaystyle f(x_{0},y_{0})=x_{0}}$ and ${\displaystyle g(x_{0},y_{0})=y_{0}}$.

Bekić's theorem (called the "bisection lemma" in his notes)[4] is that the simultaneous least fixed point ${\displaystyle \mu (x,y).(f,g)(x,y)=(x_{0},y_{0})}$ can be separated into a series of least fixed points on ${\displaystyle P}$ and ${\displaystyle Q}$, in particular:

$${\displaystyle {\begin{aligned}x_{0}&=\mu x.f(x,\mu y.g(x,y))\\y_{0}&=\mu y.g(x_{0},y)\end{aligned}}}$$

In this presentation ${\displaystyle y_{0}}$ is defined in terms of ${\displaystyle x_{0}}$. It can instead be defined in a symmetric presentation:[1][6][7]

$${\displaystyle {\begin{aligned}x_{0}&=\mu x.f(x,\mu y.g(x,y))\\y_{0}&=\mu y.g(\mu x.f(x,y),y)\end{aligned}}}$$

Proof (Bekić):

${\displaystyle y_{0}=g(x_{0},y_{0})}$ since it is the fixed point. Similarly ${\displaystyle x_{0}=f(x_{0},\mu y.g(x_{0},y))=f(x_{0},y_{0})}$. Hence ${\displaystyle (x_{0},y_{0})}$ is a fixed point of ${\displaystyle (f,g)}$. Conversely, if there is a pre-fixed point ${\displaystyle (x_{1},y_{1})}$ with ${\displaystyle (x_{1},y_{1})\geq (f(x_{1},y_{1}),g(x_{1},y_{1}))}$, then ${\displaystyle x_{1}\geq f(x_{1},\mu y.g(x_{1},y)\geq x_{0}}$ and ${\displaystyle y_{1}\geq \mu y.g(x_{1},y)\geq \mu y.g(x_{0},y)=y_{0}}$; hence ${\displaystyle (x_{1},y_{1})\geq (x_{0},y_{0})}$ and ${\displaystyle (x_{0},y_{0})}$ is the minimal fixed point.