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 $\mathbb {N} ^{r}$ for some arity $r$. 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 ${\mathcal {C}}_{lca}$, ${\mathcal {N}}_{\mathtt {thres,mod}}$ 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 $r\in \mathbb {N}$ and $P\subseteq \mathbb {N} ^{r}$ a (numerical) predicate of arity $r$.

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

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

The numerical predicate $P$ is said to be regular if ${\overline {P}}$ is a regular language over the alphabet $A$. 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 $A$ is the set of vectors of $r$ binary digits. That is: $\{0,1\}^{r}$. Before explaining how to encode a vector of numbers, we explain how to encode a single number.

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

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

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

$(\exists )MSO(+1)$

A predicate is regular if and only if it can be defined by a monadic second order formula $\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 $y+1=z$.

$FO(\leq ,\mod )$

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

• the order relation $y\leq z$,
• the predicate stating that a number is a multiple of a constant $m$, that is $y\equiv 0\mod m$.

Congruence arithmetic

The language of congruence arithmetic is defined as the est of Boolean combinations, where the atomic predicates are:

• the addition of a constant $x_{i}+c=x_{j}$, with $c$ an integral constant,
• the order relation $x_{i}\leq x_{j}$,
• the modular relations, with a fixed modular value. That is, predicates of the form $x_{i}\equiv c\mod m$ where $c$ and $m$ are fixed constants and $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.

Using recursion and patterns

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

The last equivalent definition of regular predicate can now be given. A predicate $P$ of arity $r\geq 1$ is regular if it satisfies the two following conditions:

• all of its sections are regular,
• there exists a threshold $t\in \mathbb {N}$ such that, for each vectors $(n_{0},\dots ,n_{r})\in \mathbb {N} ^{r}$ with each $n_{i}\geq t$, $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 $m$.

Using recognizable semigroups

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

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

Definition of non regular language

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

Properties

The class of regular numerical predicate satisfies many properties.

Satisfiability

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

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

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 $\mathbf {FO} (\leq ,\mod )$.

Decidability

It is decidable whether a predicate defined in Presburger arithmetic is regular.

Elimination of quantifier

The logic $\mathbf {FO} (\leq ,+c,\mod )$ 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 $\mathbf {FO} (\leq ,+c,\mod )$ it returns a quantifier-free formula in$\mathbf {FO} (\leq ,+c,\mod )$.