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:
![{\displaystyle {\begin{aligned}x_{0}&=\mu x.f(x,\mu y.g(x,y))\\y_{0}&=\mu y.g(x_{0},y)\end{aligned}}}](//wikimedia.org/api/rest_v1/media/math/render/svg/a88523d1b45d6bef99b28e6a8430a6694b1f4b24)
In this presentation
is defined in terms of
. 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}}}](//wikimedia.org/api/rest_v1/media/math/render/svg/af00d524d9c8ae2fbd8f0fabf281cc00eaf9d2f9)
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.