A note on Presburger arithmetic with array segments, permutation and equality (Q1073009)

In this paper, we examine the validity (satisfiability) problem for a language containing Presburger arithmetic, finite length array segments and some fixed second order predicates. In particular, we consider the predicates: PERM, which is used to assert that two array segments contain the same multiset of elements, and \(=\) (equality), which is used to assert that two array segments are identical (i.e., contain the same sequence of elements and have equivalent upper and lower array bounds). It is known that the afore-mentioned (unquantified) language has a decidable validity problem. (In fact, the satisfiability problem is NP- complete.) We consider the case when equality is defined in a seemingly weaker fashion. Let \(Y\simeq B\) be true if and only if array segments A and B contain the same sequence of elements. This definition of equality is more useful in the verification conditions of programs that manipulate queues and/or strings. However, we show that when this form of equality replaces the earlier variety in the previously mentioned language, the validity problem becomes undecidable.