Regular numerical predicate

In computer science and mathematics, more precisely in automata theory, model theory and formal language, a regular numerical predicate is a kind of relation over integers. Regular numerical predicates can also be considered as a subset of formula_1 for some arity formula_2. One of the main interests of this class of predicates is that it can be defined in plenty of different ways, using different logical formalisms. Furthermore, most of the definitions use only basic notions, and thus allows to relate foundations of various fields of fundamental computer science such as automata theory, syntactic semigroup, model theory and semigroup theory.
The class of regular numerical predicate is denoted formula_3, formula_4 and REG.
Definitions.
The class of regular numerical predicate admits a lot of equivalent definitions. They are now given. In all of those definitions, we fix formula_5 and formula_6 a (numerical) predicate of arity formula_2.
Automata with variables.
The first definition encodes predicate as a formal language. A predicate is said to be regular if the formal language is regular.
Let the alphabet formula_8 be the set of subset of formula_9. Given a vector of formula_2 integers formula_11, it is represented by the word formula_12 of length formula_13 whose formula_14-th letter is formula_15. For example, the vector formula_16 is represented by the word formula_17.
We then define formula_18 as formula_19.
The numerical predicate formula_20 is said to be regular if formula_18 is a regular language over the alphabet formula_8. This is the reason for the use of the word "regular" to describe this kind of numerical predicate.
Automata reading unary numbers.
This second definition is similar to the previous one. Predicates are encoded into languages in a different way, and the predicate is said to be regular if and only if the language is regular.
Our alphabet formula_8 is the set of vectors of formula_2 binary digits. That is: formula_25. Before explaining how to encode a vector of numbers, we explain how to encode a single number.
Given a length formula_26 and a number formula_27, the unary representation of formula_28 of length formula_26 is the word formula_30 over the binary alphabet formula_31, beginning by a sequence of formula_28 "1"'s, followed by formula_33 "0"'s. For example, the unary representation of 1 of length 4 is formula_34.
Given a vector of formula_2 integers formula_11, let formula_37. The vector formula_38 is represented by the word formula_39 such that, the projection of formula_12 over its formula_14-th component is formula_42. For example, the representation of formula_16 is formula_44. This is a word whose letters are the vectors formula_45, formula_46 and formula_46 and whose projection over each components are formula_48, formula_49 and formula_48.
As in the previous definition, the numerical predicate formula_20 is said to be regular if formula_18 is a regular language over the alphabet formula_8.
formula_54.
A predicate is regular if and only if it can be defined by a monadic second order formula formula_55, or equivalently by an existential monadic second order formula, where the only atomic predicate is the successor function formula_56.
formula_57.
A predicate is regular if and only if it can be defined by a first order logic formula formula_55, where the atomic predicates are:
Congruence arithmetic.
The language of congruence arithmetic is defined as the est of Boolean combinations, where the atomic predicates are:
A predicate is regular if and only if it can be defined in the language of congruence arithmetic. The equivalence with previous definition is due to quantifier elimination.
Using recursion and patterns.
This definition requires a fixed parameter formula_60. A set is said to be regular if it is formula_60-regular for some formula_71. 
In order to introduce the definition of formula_60-regular, the trivial case where formula_73 should be considered separately. When formula_73, then the predicate formula_20 is either the constant true or the constant false. Those two predicates are said to be formula_60-regular. Let us now assume that formula_77. In order to introduce the definition of regular predicate in this case, we need to introduce the notion of section of a predicate.
The section formula_78 of formula_20 is the predicate of arity formula_80 where the formula_14-th component is fixed to formula_63. Formally, it is defined as formula_83. For example, let us consider the sum predicate formula_84. Then formula_85 is the predicate which adds the constant formula_63, and formula_87 is the predicate which states that the sum of its two elements is formula_63.
The last equivalent definition of regular predicate can now be given. A predicate formula_20 of arity formula_77 is regular if it satisfies the two following conditions:
The second property intuitively means that, when number are big enough, then their exact value does not matter. The properties which matters are the order relation between the numbers and their value modulo the period formula_60.
Using recognizable semigroups.
Given a subset formula_96, let formula_97 be the characteristic vector of formula_98. That is, the vector in formula_25 whose formula_14-th component is 1 if formula_101, and 0 otherwise. Given a sequence formula_102 of sets, let formula_103.
The predicate formula_20 is regular if and only if for each increasing sequence of set formula_105, formula_106 is a recognizable submonoid of formula_107.
Definition of non regular language.
The predicate formula_20 is regular if and only if all languages which can be defined in first order logic with atomic predicates for letters and the atomic predicate formula_20 are regular. The same property would hold for the monadic second order logic, and with modular quantifiers.
Reducing arity.
The following property allows to reduce an arbitrarily complex non-regular predicate to a simpler binary predicate which is also non-regular.
Let us assume that formula_20 is definable in Presburger Arithmetic. The predicate formula_20 is non regular if and only if there exists a formula in formula_112 which defines the multiplication by a rational formula_113. More precisely, it allows to define the non-regular predicate formula_114 for some formula_115.
Properties.
The class of regular numerical predicate satisfies many properties.
Satisfiability.
As in previous case, let us assume that formula_20 is definable in Presburger Arithmetic. The satisfiability of formula_117 is decidable if and only if formula_20 is regular.
This theorem is due to the previous property and the fact that the satisfiability of formula_119 is undecidable when formula_120 and formula_121.
Closure property.
The class of regular predicates is closed under union, intersection, complement, taking a section, projection and Cartesian product. All of those properties follows directly from the definition of this class as the class of predicates definable in formula_122.
Decidability.
It is decidable whether a predicate defined in Presburger arithmetic is regular.
Elimination of quantifier.
The logic formula_123 considered above admit the elimination of quantifier. More precisely, the algorithm for elimination of quantifier by Cooper does not introduce multiplication by constants nor sums of variable. Therefore, when applied to a formula_123 it returns a quantifier-free formula informula_125.