8
$\begingroup$

As far as I know, formulae involving rationals and basic arithmetic ($+$, $-$, $\cdot$ and $/$) have decidable equality. Is this still the case if we add floor rounding (or integer division)?

Define a "basic formula" by the following grammar (in Backus-Naur form):

$$ \begin{matrix} e &= &q \\ &| &v \\ &| &e + e \\ &| &e - e \\ &| &e \cdot e \\ &| &e / e \\ \end{matrix} $$ Here, $q$ stands for rational literals and $v$ for a set of variables.

A valuation is the assignment of a rational number to every variable. The semantics of such a formula for a given valuation is ordinary arithmetics. Two formulae are semantically equal if they are equal for every allowed valuation. (Division by 0 is not allowed, of course.) As far as I understand, this notion of equality is decidable. Given two formulas, we essentially multiply by all denominators, apply the distributive law everywhere and then compare summands. We've basically reduced each expression to a normal form where we can compare.

Now, let us add the floor function, which rounds down to the nearest integer. We extend the above definition by: $$ \begin{matrix} e &= &\dots \\ &| &\lfloor e \rfloor \\ \end{matrix} $$

Is equality still decidable here? It's not so obvious to me that a well-behaved normal form even exists, since the floor function satisfies some equations such as $\lfloor \lfloor x \rfloor + y \rfloor = \lfloor x \rfloor + \lfloor y \rfloor$, Hermite's identities (e.g. $\lfloor x\rfloor + \lfloor x+1/3\rfloor + \lfloor x+2/3\rfloor = \lfloor 3x\rfloor$), and so on.

Is there still some simple enough algorithm that decides whether two such formulae are equal?

Note: I could have added integer division instead of the floor function as well, but I believe that this wouldn't make a difference.

Feel free to add or suggest tags, I'm not so sure whether the question is categorized well.

Improve this question
$\endgroup$
5
  • $\begingroup$ I would state this as: "Given the decision procedure for universally quantified equalities in $(\mathbf{Q},0,1,+,-,*)$, is there also a decision procedure when we add the division and floor functions?" Otherwise, "decidable equality" sounds like it could also apply to inequalities or existentially quantified formulas, which lead to the lack of known decision procedures for Hilbert's 10th problem over the rationals. $\endgroup$
    – user44143
    Jul 22, 2019 at 16:30
  • 1
    $\begingroup$ What semantics do you intend for division by 0? I don't think "not allowed, of course" is enough. $\endgroup$
    – user44143
    Jul 22, 2019 at 16:34
  • 1
    $\begingroup$ Technicality: I think your definition of $f$ is currently incomplete; as it stands, it seems to only allow expressions with floor functions on the outside (so no arithmetic where the arguments are floor functions of other expressions would be allowed). $\endgroup$
    – user44191
    Jul 23, 2019 at 5:26
  • $\begingroup$ @MattF. I guess I'd have to extend the rationals by a formal infinity. But I'm only interested in those valuations where this division by zero does not occur. $\endgroup$
    – Manuel Bärenz
    Jul 23, 2019 at 12:49
  • $\begingroup$ @user44191, yes. I've edited the question. $\endgroup$
    – Manuel Bärenz
    Jul 23, 2019 at 12:51

1 Answer 1

Reset to default
11
$\begingroup$

Equality of formulas is undecidable. To prove this it is enough to show that an algorithm for equality of formulas would enable us to determine whether or not a multivariate polynomial with integer coefficients vanishes at at least one integer point, because the latter condition is undecidable according to the negative solution to Hilbert's Tenth Problem.

But the polynomial $f(x)$, where $x$ is a tuple of variables and $f$ has integer coefficients, does not vanish at any integer point if and only if the following equation holds at all integer points $x$: $$\Bigl\lfloor\dfrac{1}{1+f(x)^2}\Bigr\rfloor=0.$$

I believe this settles it. However it would be nice to know a simple elegant decidability result for formulas excluding division.

Improve this answer
$\endgroup$
8
  • $\begingroup$ Wow. What an unexpected connection. $\endgroup$
    – Manuel Bärenz
    Jul 23, 2019 at 12:52
  • 1
    $\begingroup$ This wouldn't work if we allow $x$ to take irrational values, right? $\endgroup$
    – Manuel Bärenz
    Jul 23, 2019 at 12:56
  • 4
    $\begingroup$ It should really say $f(\lfloor x\rfloor)$, to show the undecidability. Without that, and letting $x$ range over the reals, it is a decidable question. $\endgroup$
    – user44143
    Jul 23, 2019 at 13:02
  • $\begingroup$ Manuel, For a broader framework for the kind of question you are asking, take a look at the second answer to this post: mathoverflow.net/questions/23796/…. In this broader context, your question generalizes to "Is the universal theory of open induction decidable?" This a long-standing open question. $\endgroup$
    – Sidney Raffer
    Jul 23, 2019 at 15:32
  • 1
    $\begingroup$ Robert, Thank you! I mean mathoverflow.net/a/23858/5229 $\endgroup$
    – Sidney Raffer
    Jul 25, 2019 at 11:35

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.