# How to show that a partial function is recursive?

I try to prove that this function is recursive: $$f(x_1,x_2)= \begin{cases} 2x_1-x_2 & \text{if x_1 \geqslant \sqrt{x_2}} \newline \bot & \text{otherwise} \end{cases}$$

I think that I need to use minimization operator but I don't know how to do that. $$\qquad$$ $$\qquad$$ $$\qquad$$ Maybe i have to prove that $$\mu y(|x_1-\sqrt{x_2}| = 0)$$ ?

• $x_1 \geq \sqrt{x_2}$ is equivalent to $x_1^2 \geq x_2$, which should make things easier. – Andrej Bauer Feb 17 '20 at 20:21
• So I have to use minimisation on $|x_1^2-x_2|=0$? – Alessandro Recchia Feb 17 '20 at 22:13
• Or maybe i have to demonstrate that the predicate $isZero(x_1^2 \dot{-} x_2)$ is recursive and than i need to use minimization operator as $g=\lambda x_2 (isZero(x_1^2 \dot{-} x_2))$ and after doing product between $2x_1-x_2$ and g? – Alessandro Recchia Feb 18 '20 at 10:40
• * $isZero(x_2 \dot{-} x_1^2)$ – Alessandro Recchia Feb 18 '20 at 10:53
• What's wrong with implementing the function in Python, C or Haskell? That'll prove it's recursive. – Andrej Bauer Feb 18 '20 at 13:46