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. It was created by Austrian Hans Bekić (1936-1982) in 1969, and published posthumously in a book by Cliff Jones in 1984.

The theorem is set up as follows. Consider two operators $f:P\times Q\to P$ and $g:P\times Q\to Q$ on pointed directed-complete partial orders $P$ and $Q$, continuous in each component. Then define the operator $(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 $\mu (x,y).(f,g)(x,y)$, a pair $(x_{0},y_{0})$ in $P\times Q$ such that $f(x_{0},y_{0})=x_{0}$ and $g(x_{0},y_{0})=y_{0}$.

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

$${\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 $y_{0}$ is defined in terms of $x_{0}$. It can instead be defined in a symmetric presentation:

$${\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ć):

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

Variants

In a complete lattice

A variant of the theorem strengthens the conditions on $P$ and $Q$ to be that they are complete lattices, and finds the least fixed point using the Knaster–Tarski theorem. The requirement for continuity of $f$ and $g$ can then be weakened to only requiring them to be monotonic functions.

Categorical formulation

Bekić's lemma has been generalized to fix-points of endofunctors of categories (initial $F$-algebras).

Given two functors $F:\mathbf {C} \times \mathbf {D} \to \mathbf {C}$ and $G:\mathbf {C} \times \mathbf {D} \to \mathbf {D}$ such that all $\mu X.F(X,Y)$ and $\mu Y.G(X,Y)$ exist, the fix-point $\mu \langle X,Y\rangle .\langle F(X,Y),G(X,Y)\rangle$ is carried by the pair:

$${\begin{aligned}X_{0}&=\mu X.F(X,\mu Y.G(X,Y))\\Y_{0}&=\mu Y.G(X_{0},Y)\end{aligned}}$$

Usage

Bekić's theorem can be applied repeatedly to find the least fixed point of a tuple in terms of least fixed points of single variables. Although the resulting expression might become rather complex, it can be easier to reason about fixed points of single variables when designing an automated theorem prover.