How to do the integral part of logarthm with minimizer?

Question

I have this function:

$r: N -> N $
$r(n) = \log_2(n)$

I have arrived at a version with maximization:

$r(n) = max(t) : n >= 2^t$

How do I rewrite it as a recursive function using a bounded minimization operator μ.

Answer 1

Assuming $r(n)$ is the integer part of $\log_2(n)$, you can write $$ r(n) = \min \{ t <n : n< 2^t \} -1 $$

In bounded minimization operator it is written:

$$r(n) = \mu t [(2^t\dot{-}n) + Eq(2^t, n) = 0]$$

Where Eq returns 1 when both parameters are one and zero otherwise.