Regular numerical predicate

The class of regular numerical predicate admits a lot of equivalent definitions. They are now given. In all of those definitions, we fix ${\displaystyle r\in \mathbb {N} }$ and ${\displaystyle P\subseteq \mathbb {N} ^{r}}$ a (numerical) predicate of arity ${\displaystyle r}$.

The first definition encodes predicate as a formal language. A predicate is said to be regular if the formal language is regular.^[3]: 25

Let the alphabet ${\displaystyle A}$ be the set of subset of ${\displaystyle \{1,\dots ,r\}}$. Given a vector of ${\displaystyle r}$ integers ${\displaystyle \mathbf {n} =(n_{0},\dots ,n_{r-1})\in \mathbb {N} ^{r}}$, it is represented by the word ${\displaystyle {\overline {\mathbf {n} }}}$ of length ${\displaystyle \max(n_{0},\dots ,n_{r-1})}$ whose ${\displaystyle i}$-th letter is ${\displaystyle \{j\mid n_{j}=i\}}$. For example, the vector ${\displaystyle (3,1,3)}$ is represented by the word ${\displaystyle \emptyset \{1\}\emptyset \{0,2\}}$.

We then define ${\displaystyle {\overline {P}}}$ as ${\displaystyle \{{\overline {\mathbf {n} }}\mid \mathbf {n} \}}$.

The numerical predicate ${\displaystyle P}$ is said to be regular if ${\displaystyle {\overline {P}}}$ is a regular language over the alphabet ${\displaystyle A}$. This is the reason for the use of the word "regular" to describe this kind of numerical predicate.

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.^[3]: 25

Our alphabet ${\displaystyle A}$ is the set of vectors of ${\displaystyle r}$ binary digits. That is: ${\displaystyle \{0,1\}^{r}}$. Before explaining how to encode a vector of numbers, we explain how to encode a single number.

Given a length ${\displaystyle l}$ and a number ${\displaystyle n\leq l}$, the unary representation of ${\displaystyle n}$ of length ${\displaystyle l}$ is the word ${\displaystyle \mid {n}\mid _{l}}$ over the binary alphabet ${\displaystyle \{0,1\}}$, beginning by a sequence of ${\displaystyle n}$ "1"'s, followed by ${\displaystyle n-l}$ "0"'s. For example, the unary representation of 1 of length 4 is ${\displaystyle 1000}$.

Given a vector of ${\displaystyle r}$ integers ${\displaystyle \mathbf {n} =(n_{0},\dots ,n_{r-1})\in \mathbb {N} ^{r}}$, let ${\displaystyle l=\max(n_{0},\dots ,n_{r-1})}$. The vector ${\displaystyle \mathbf {n} }$ is represented by the word ${\displaystyle {\overline {\mathbf {n} }}\in \left(\{0,1\}^{r}\right)^{*}}$ such that, the projection of ${\displaystyle {\overline {\mathbf {n} }}}$ over its ${\displaystyle i}$-th component is ${\displaystyle \mid {n_{i}}\mid _{\max(n_{0},\dots ,n_{r-1})}}$. For example, the representation of ${\displaystyle (3,1,3)}$ is ${\displaystyle {\begin{array}{l|l|l}1&1&1\\1&0&0\\1&1&1\end{array}}}$. This is a word whose letters are the vectors ${\displaystyle (1,1,1)}$, ${\displaystyle (1,0,1)}$ and ${\displaystyle (1,0,1)}$ and whose projection over each components are ${\displaystyle 111}$, ${\displaystyle 100}$ and ${\displaystyle 111}$.

As in the previous definition, the numerical predicate ${\displaystyle P}$ is said to be regular if ${\displaystyle {\overline {P}}}$ is a regular language over the alphabet ${\displaystyle A}$.

A predicate is regular if and only if it can be defined by a monadic second order formula ${\displaystyle \phi (x_{0},\dots ,x_{r-1})}$, or equivalently by an existential monadic second order formula, where the only atomic predicate is the successor function ${\displaystyle y+1=z}$.^[3]: 26

A predicate is regular if and only if it can be defined by a first order logic formula ${\displaystyle \phi (x_{0},\dots ,x_{r-1})}$, where the atomic predicates are:

• the order relation ${\displaystyle y\leq z}$,
• the predicate stating that a number is a multiple of a constant ${\displaystyle m}$, that is ${\displaystyle y\equiv 0\mod m}$.^[3]: 26

The language of congruence arithmetic^[1]: 140 is defined as the est of Boolean combinations, where the atomic predicates are:

• the addition of a constant ${\displaystyle x_{i}+c=x_{j}}$, with ${\displaystyle c}$ an integral constant,
• the order relation ${\displaystyle x_{i}\leq x_{j}}$,
• the modular relations, with a fixed modular value. That is, predicates of the form ${\displaystyle x_{i}\equiv c\mod m}$ where ${\displaystyle c}$ and ${\displaystyle m}$ are fixed constants and ${\displaystyle x}$ is a variable.

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.^[4]

This definition requires a fixed parameter ${\displaystyle m}$. A set is said to be regular if it is ${\displaystyle m}$-regular for some ${\displaystyle m\geq 2}$. In order to introduce the definition of ${\displaystyle m}$-regular, the trivial case where ${\displaystyle r=0}$ should be considered separately. When ${\displaystyle r=0}$, then the predicate ${\displaystyle P}$ is either the constant true or the constant false. Those two predicates are said to be ${\displaystyle m}$-regular (for every ${\displaystyle m}$). Let us now assume that ${\displaystyle r\geq 1}$. 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 ${\displaystyle P^{x_{i}=c}}$ of ${\displaystyle P}$ is the predicate of arity ${\displaystyle r-1}$ where the ${\displaystyle i}$-th component is fixed to ${\displaystyle c}$. Formally, it is defined as ${\displaystyle \{(x_{0},\dots ,x_{i-1},x_{i+1},\dots ,x_{r-1})\mid P(x_{0},\dots ,x_{i-1},c,x_{i+1},\dots ,x_{r-1})\}}$. For example, let us consider the sum predicate ${\displaystyle S=\{(n_{0},n_{1},n_{2})\mid n_{0}+n_{1}=n_{2}\}}$. Then ${\displaystyle S^{x_{0}=c}=\{(n_{1},n_{2})\mid c+n_{1}=n_{2}\}}$ is the predicate which adds the constant ${\displaystyle c}$, and ${\displaystyle S^{x_{2}=c}=\{(n_{0},n_{1})\mid n_{0}+n_{1}=c\}}$ is the predicate which states that the sum of its two elements is ${\displaystyle c}$.

The last equivalent definition of regular predicate can now be given. A predicate ${\displaystyle P}$ of arity ${\displaystyle r\geq 1}$ is ${\displaystyle m}$-regular if it satisfies the two following conditions:^[5]

• all of its sections are ${\displaystyle m}$-regular,
• there exists a threshold ${\displaystyle t\in \mathbb {N} }$ such that, for each vectors ${\displaystyle (n_{0},\dots ,n_{r})\in \mathbb {N} ^{r}}$ with each ${\displaystyle n_{i}\geq t}$, ${\displaystyle P(n_{0},\dots ,n_{r})\iff P(n_{0}+m,\dots ,n_{r}+m)}$.

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 ${\displaystyle m}$.

Given a subset ${\displaystyle s\subseteq \{0,\dots ,r-1\}}$, let ${\displaystyle {\overline {s}}}$ be the characteristic vector of ${\displaystyle s}$. That is, the vector in ${\displaystyle \{0,1\}^{r}}$ whose ${\displaystyle i}$-th component is 1 if ${\displaystyle i\in s}$, and 0 otherwise. Given a sequence ${\displaystyle \mathbf {s} =s_{0}\subsetneq \dots \subsetneq s_{p-1}}$ of sets, let ${\displaystyle P_{\mathbf {s} }=\{(n_{0},\dots ,n_{p-1})\in \mathbb {N} ^{p}\mid P(\sum n_{i}e_{i})\}}$.

The predicate ${\displaystyle P}$ is regular if and only if for each increasing sequence of set ${\displaystyle \mathbf {s} }$, ${\displaystyle P_{\mathbf {s} }}$ is a recognizable submonoid of ${\displaystyle \mathbb {N} ^{p}}$.^[2]

The predicate ${\displaystyle P}$ 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 ${\displaystyle P}$ are regular. The same property would hold for the monadic second order logic, and with modular quantifiers.^[1]

The following property allows to reduce an arbitrarily complex non-regular predicate to a simpler binary predicate which is also non-regular.^[5]

Let us assume that ${\displaystyle P}$ is definable in Presburger Arithmetic. The predicate ${\displaystyle P}$ is non regular if and only if there exists a formula in ${\displaystyle \mathbf {FO} [\leq ,R]}$ which defines the multiplication by a rational ${\displaystyle {\frac {p}{q}}\not \in \{0,1\}}$. More precisely, it allows to define the non-regular predicate ${\displaystyle \{(p\times n,q\times n)\mid n\in \mathbb {N} \}}$ for some ${\displaystyle p\not \in {0,q}}$.

The class of regular numerical predicate satisfies many properties.

As in previous case, let us assume that ${\displaystyle P}$ is definable in Presburger Arithmetic. The satisfiability of ${\displaystyle \exists \mathbf {MSO} (+1,P)}$ is decidable if and only if ${\displaystyle P}$ is regular.

This theorem is due to the previous property and the fact that the satisfiability of ${\displaystyle \exists \mathbf {MSO} (+1,\times {\frac {p}{q}})}$ is undecidable when ${\displaystyle p\neq 0}$ and ${\displaystyle p\neq q}$.^{[citation needed]}

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 ${\displaystyle \mathbf {FO} (\leq ,\mod )}$.^{[citation needed]}

It is decidable whether a predicate defined in Presburger arithmetic is regular.^[2]

The logic ${\displaystyle \mathbf {FO} (\leq ,+c,\mod )}$ considered above admit the elimination of quantifier. More precisely, the algorithm for elimination of quantifier by Cooper^[6] does not introduce multiplication by constants nor sums of variable. Therefore, when applied to a ${\displaystyle \mathbf {FO} (\leq ,+c,\mod )}$ it returns a quantifier-free formula in${\displaystyle \mathbf {FO} (\leq ,+c,\mod )}$.