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 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 (componentwise order). By the Kleene fixed-point theorem, it has a least fixed point , a pair in such that and .
Bekić's theorem (called the "bisection lemma" in his notes)[4] is that the simultaneous least fixed point can be separated into a series of least fixed points on and , in particular:
In this presentation is defined in terms of . It can instead be defined in a symmetric presentation:[1][6][7]
Proof (Bekić):
- since it is the fixed point. Similarly . Hence is a fixed point of . Conversely, if there is a pre-fixed point with , then and ; hence and is the minimal fixed point.
Bekić's lemma has been generalized to fix-points of endofunctors of categories (initial -algebras).[8]
Given two functors and such that all and exist, the fix-point is carried by the pair: