27
$\begingroup$

Consider expressions built using number $1$, arithmetical operators $+, -, *, /$ and exponentiation ^ (in case of multiple values, the principal value is assumed, the same way as it implemented in Power function in Mathematica). Is it a decidable problem to check if such an expression is zero? If so, could you please point me to an algorithm that can solve this problem?

Update: I found a reference to Richardson's Theorem, that establishes undecidablity of equality in a wider set of expressions, in particular, including the logarithm and absolute value functions.

$\endgroup$
10
  • $\begingroup$ I believe there is such an algorithm but it's quite complicated. $\endgroup$ May 3, 2013 at 18:26
  • $\begingroup$ Do you have any references? $\endgroup$ May 3, 2013 at 18:30
  • 1
    $\begingroup$ If you are thinking on variables just taking values over real numbers it is known that the full first-order theory is decidable under Schanuel's conjecture. You can find more information in en.wikipedia.org/wiki/Tarski%27s_exponential_function_problem $\endgroup$
    – boumol
    May 6, 2013 at 7:46
  • 1
    $\begingroup$ @StefanKohl In general, how do you evaluate the result of subtraction of two expression up to any desired precision? If the algorithm yields $0.000000...$ how do you know when to stop and if there is at least one non-zero digit? If you need the reciprocal of the difference, how do you know if it is defined at all? $\endgroup$ Jun 18, 2014 at 15:54
  • 1
    $\begingroup$ @ZakhariaStanley: Sorry, I made a mistake in my tentative argumentation. -- I removed my comment. Though I think the question essentially is whether the value of an expression of length $n$ as described in the question is bounded above by a computable function in $n$ or not. $\endgroup$
    – Stefan Kohl
    Jun 18, 2014 at 16:25

1 Answer 1

8
$\begingroup$

The equational theory of $\langle {\bf N}, 0, 1, +, \times, \uparrow\rangle$ is decidable, but not finitely axiomatizable.

$\endgroup$
4
  • 8
    $\begingroup$ Thanks for the reference. But it looks like a different problem. The division operator $/$ takes it beyond integers and, together with $-$ and ^, beyond reals and algebraics. $\endgroup$ May 3, 2013 at 18:54
  • $\begingroup$ That's right, I agree. $\endgroup$
    – Nik Weaver
    May 3, 2013 at 19:11
  • $\begingroup$ The link is broken $\endgroup$ Aug 29, 2023 at 8:34
  • $\begingroup$ Permanent link doi.org/10.1007/978-3-540-32275-7_17 $\endgroup$ Aug 29, 2023 at 8:46

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.