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ć in 1969, and published posthumously in a book by Cliff Jones in 1984.
The theorem is set up as follows. Consider two operators and on pointed directed-complete partial orders and, continuous in each component. Then define the operator. This is monotone with respect to the product order. By the Kleene fixed-point theorem, it has a least fixed point, a pair in such that and.
Bekić's theorem is that the simultaneous least fixed point can be separated into a series of least fixed points on and, in particular the fixed point is equal to as follows:
In this presentation is defined in terms of. It can instead be defined in a symmetric presentation:
Proof :
Variants
In a complete lattice
A variant of the theorem strengthens the conditions on and to be that they are complete lattices, and finds the least fixed point using the Knaster–Tarski theorem. The requirement for continuity of and 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.Given two functors and such that all and exist, the fix-point is carried by the pair: