0
$\begingroup$

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)$$ ?

Improve this question
$\endgroup$
  • $\begingroup$ $x_1 \geq \sqrt{x_2}$ is equivalent to $x_1^2 \geq x_2$, which should make things easier. $\endgroup$ – Andrej Bauer Feb 17 '20 at 20:21
  • $\begingroup$ So I have to use minimisation on $|x_1^2-x_2|=0$? $\endgroup$ – Alessandro Recchia Feb 17 '20 at 22:13
  • $\begingroup$ 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? $\endgroup$ – Alessandro Recchia Feb 18 '20 at 10:40
  • $\begingroup$ * $isZero(x_2 \dot{-} x_1^2)$ $\endgroup$ – Alessandro Recchia Feb 18 '20 at 10:53
  • $\begingroup$ What's wrong with implementing the function in Python, C or Haskell? That'll prove it's recursive. $\endgroup$ – Andrej Bauer Feb 18 '20 at 13:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.