This article is an orphan, as no other articles link to it. Please introduce links to this page from related articles; try the Find link tool for suggestions. (January 2021) |
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 for some arity . 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 , 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 and a (numerical) predicate of arity .
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 be the set of subset of . Given a vector of integers , it is represented by the word of length whose -th letter is . For example, the vector is represented by the word .
We then define as .
The numerical predicate is said to be regular if is a regular language over the alphabet . 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 is the set of vectors of binary digits. That is: . Before explaining how to encode a vector of numbers, we explain how to encode a single number.
Given a length and a number , the unary representation of of length is the word over the binary alphabet , beginning by a sequence of "1"'s, followed by "0"'s. For example, the unary representation of 1 of length 4 is .
Given a vector of integers , let . The vector is represented by the word such that, the projection of over its -th component is . For example, the representation of is . This is a word whose letters are the vectors , and and whose projection over each components are , and .
As in the previous definition, the numerical predicate is said to be regular if is a regular language over the alphabet .
A predicate is regular if and only if it can be defined by a monadic second order formula , or equivalently by an existential monadic second order formula, where the only atomic predicate is the successor function .
A predicate is regular if and only if it can be defined by a first order logic formula , where the atomic predicates are:
- the order relation ,
- the predicate stating that a number is a multiple of a constant , that is .
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 , with an integral constant,
- the order relation ,
- the modular relations, with a fixed modular value. That is, predicates of the form where and are fixed constants and 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 . A set is said to be regular if it is -regular for some . In order to introduce the definition of -regular, the trivial case where should be considered separately. When , then the predicate is either the constant true or the constant false. Those two predicates are said to be -regular (for every ). Let us now assume that . 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 of is the predicate of arity where the -th component is fixed to . Formally, it is defined as . For example, let us consider the sum predicate . Then is the predicate which adds the constant , and is the predicate which states that the sum of its two elements is .
The last equivalent definition of regular predicate can now be given. A predicate of arity is -regular if it satisfies the two following conditions:
- all of its sections are -regular,
- there exists a threshold such that, for each vectors with each , .
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 .
Using recognizable semigroups
Given a subset , let be the characteristic vector of . That is, the vector in whose -th component is 1 if , and 0 otherwise. Given a sequence of sets, let .
The predicate is regular if and only if for each increasing sequence of set , is a recognizable submonoid of .
Definition of non regular language
The predicate 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 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 is definable in Presburger Arithmetic. The predicate is non regular if and only if there exists a formula in which defines the multiplication by a rational . More precisely, it allows to define the non-regular predicate for some .
Properties
The class of regular numerical predicate satisfies many properties.
Satisfiability
As in previous case, let us assume that is definable in Presburger Arithmetic. The satisfiability of is decidable if and only if is regular.
This theorem is due to the previous property and the fact that the satisfiability of is undecidable when and .
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 .
Decidability
It is decidable whether a predicate defined in Presburger arithmetic is regular.
Elimination of quantifier
The logic 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 it returns a quantifier-free formula in.
References
- ^ Péladeau, Pierre (1992). "Formulas, regular languages and Boolean circuits". Theoretical Computer Science. 101: 133–142. doi:10.1016/0304-3975(92)90152-6.
- ^ Choffrut, Christian (January 2008). "Deciding whether a relation defined in Presburger logic can be defined in weaker logics". RAIRO - Theoretical Informatics and Applications. 42 (1): 121–135. doi:10.1051/ita:2007047.
- ^ Straubing, Howard (1994). Finite Automata, Formal Logic and Circuit Complexity. Birkhäser. ISBN 978-1-4612-0289-9.
- Smoryński., Craig A. (1991). Logical number theory. 1., an introduction. Springer. p. 322. ISBN 978-3-642-75462-3.
- ^ Milchior, Arthur (January 2017). "Undecidability of satisfiability of expansions of FO with a Semilinear Non Regular Predicate over words". The Nature of Computation: 161–170.
- Cooper, D. C. (1972). "Theorem Proving in Arithmetic without Multiplication". Machine Intelligence. 7: 91–99.