Primitive Recursion -- Definition by Cases

496 Views Asked by At

I would like to know if it is allowed to define bounded maximization by primitive recursion and definition by cases in the following way:

\begin{align*} [\mathrm{max}\,R](x, 0) &= 0,\\ [\mathrm{max}\,R](x, y + 1) &= \left\{\begin{array}{l l} y + 1 & \quad \text{if $R(x, y + 1) = true$}\\ [\mathrm{max}\,R](x, y) & \quad \text{otherwise.}\\ \end{array}\right. \end{align*}

In every source I find, maximization is always defined via the characteristic functions of the relation involved and subsequently constructed via bounded sum, so I'm questioning whether my approach actually works.

Edit: Bounded Maximization means, find the maximum $k \leq y$ such that $R(x, k)$ holds and return $0$ if no such $k$ exists.

Thanks

1

There are 1 best solutions below

0
On

Yes, the definition you presented is a primitive recursive definition of $[\max R]$ if $R$ is already primitive recursive.