This is an old revision of the document!
Introduction: We know that Weak Monadic Second-order theory of 1 Successor (WS1S) is decidable through automata, that is, the set of satisfying interpretations of a subformula is represented by a finite-state automaton [Buc60b, Elg61]. The decision procedures (using the automata technique) have been implemented efficiently (for WS1S with certain restrictions) in MONA. The main problem with this approach is exponential blow-up in the states of the automaton due to nested quantifiers [Kla01]. We were interested in finding another way of deciding WS1S without using the automata. We began by investigating whether we can characterize relations in WS1S in a way that helps us eliminate quantifiers. Since we couldn't get any substantial results, we began looking at a subset of WS1S. This paper describes the key results that we obtained.
Conclusions and Future Directions: In the course of our mini-project we proved an interesting result about the lengths of words of a regular language. We used this result to characterize relations in the language . We hope that this is a step in the direction of our original aim: characterizing relations in WS1S.
START
Recall the syntax for WS1S:
The language is the language of WS1S with the restriction that there are no free second-order (set) variables. A w-relation is a relation on first-order variables expressible in .
The W-Problem
Characterize the set of w-relations expressible in .
We want to characterize the set by proving that a w-relation is recognized by an automaton (with parallel input) that accepts strings of the form ABC where the length of B is completely described by a union of a finite number of sets S(a,b) for some finite number of tuples (a,b) for given constants a and b.
Here, .
Terminology clarification
Define a set to be ultimately periodic iff its characteristic function is ultimately periodic.
A sequence is ultimately periodic iff there exists and such that .
Let .
Observe that a set is ultimately periodic iff it is a union of a finite number of sets of the form .
proof
- Consider an ultimately periodic set with some and . Consider the set of numbers belonging to , and the set of numbers between and belonging to . Then
- We prove the other side of the equivalence by induction.
Base Case: Clearly is ultimately periodic (, ).
Induction: The union of an ultimately periodic set (, ) and a set of the form is an ultimately periodic set with and TO EXPLAIN WITH MORE DETAIL IF NOT OBVIOUS
Little Problem
Let L be a regular language over an alphabet and
be the set of lengths of words in L. Prove that M is a union of a finite number of sets S(a,b) for some finite number of tuples (a,b). Here, .
Proof
We prove the claim by induction on the structure of the regular expression representing the language.
Notation: We say that a set has property F if it is a union of finitely many sets S(a,b) for some tuples (a,b).
We say a language L (or the corresponding regular expression) has property P if its set of lengths M has property F.
Hence, we need to prove that any regular language has property P.
Recall that Regular Expressions over an alphabet are all strings over the alphabet that can be obtained as follows:
(1) and each member of is a regular expression.
(2) If and are regular expressions, then so is their concatenation: .
(3) If and are regular expressions, then so is their union: .
(4) If is a regular expression, then so is its Kleene closure: .
(5) Nothing is a regular expression unless it follows from (1) through (4).
A Regular Language, is generated as follows:
(1) and for each .
(2) If and are regular expressions, then .
(3) If and are regular expressions, then .
(4) If is a regular expression, then .
Base Case:
The length of a single character in is 1. Thus the length of any word corresponding to a single character belongs to the set . Hence any such word has property P.
To prove the inductive step, we need the following lemma:
Lemma 1 The set where satisfies property F, that is, is equal to a union of finitely many sets of the form , .
Proof of Lemma 1
Consider the following two (mutually disjoint and exhaustive) cases:
For ,
(1) gcd(b,c)=1
(2) gcd(b,c)=d, ,
Case (1): gcd(b,c)=1 Consider the numbers contained in the set Any such number is congruent to Letting range over , we obtain for each value of a distinct congruence class :
The congruence classes are distinct by the following argument: assume there exist and such that and Then for some Hence Since b divides it must divide But gcd(b,c)=1 hence b must divide . But , hence we must have
Since there are b distinct congruence classes the set contains all natural numbers beyond . This is because of the following theorem from Elementary Number Theory: If gcd(b,c)=1 and n >= (b-1)(c-1). Then bx+cy=n has a non-negative solution, that is, one in which both x and y are non-negative integers. There are also finitely many numbers below that are contained in the set (For example, is in the set).
Hence, the set is equal to the union of a finite number of constants (less than ) and the set . Each constant can be represented in the set . In other words, if gcd(b,c) = 1, then the set where satisfies property F.
Case(2): gcd(b,c)=d, Any number of the form can be written as where and and . From (1), we know that the set satisfies property F. The set can be obtained from by multiplying the constant factors (a and b) in each set of by and so, satisfies property F.
Hence, if gcd(b,c) = d , then the set where satisfies property F.
Inductive step:
We prove that the operations union, concatenation and Kleene closure
of two regular expressions satisfying property P yield a regular expression satisfying property P.
Union: Let and be two regular expressions satisfying property P. Then, their corresponding sets of lengths and satisfy property F. The set of lengths of is simply . Hence satisfies property P.
Concatenation: Let and be two regular expressions satisfying property P. Then, their corresponding sets of lengths and satisfy property F. The set of lengths of is the finite set This set contains elements of the form By Lemma 1, satisfies property F. Set Q therefore, also satisfies property F. Thus, satisfies property P.
Kleene Closure: Let be a regular expression satisfying property P. Let the corresponding set of lengths be that satisfies property F. where is a set of the form S(a,b) and is finite. The regular expression can contain any number of repetitions (including zero) of any of the sub-regular expressions. Hence, the possible lengths of words in is given by where . Each term of this summation is of the form where .
Consider one such term: . For different values of , we get terms of the form: Any number of the form can also be obtained from by choosing the constants appropriately: Thus, the term can be written as
(Example: Consider the regular expression: . The set of lengths of words corresponding to its language is . The corresponding set for is .)
So, where . From lemma 1, we know that the sum of any two terms in this summation is a set that satisfies property F. Thus, is the sum of finitely many sets: each set satisfying property F. We can repeatedly combine the terms of all these sets and by the argument in the case for concatenation, we know that the resulting set also satisfies property F. Hence, satisfies property F.
Since, any regular expression can be constructed only by the application of the above three steps: Union, Concatenation and Kleene Closure, the language corresponding to any regular expression satisfies property P.
The unary case for the W-problem
We consider the special case of a unary relation on natural numbers corresponding to a formula with only one free variable .
This formula defines a set
Claim: Set S is ultimately periodic.
Proof:
Given formula , there exists and automaton A with input alphabet which accepts the string iff
We define the automaton on which accepts the string iff Note that .
Note that the language corresponding to is regular iff the language corresponding to is regular. Indeed, if is regular then is the concatenation of the regular expressions and and hence is regular. Conversely, if is regular, then the language corresponding to is the intersection of the languages corresponding to the regular expressions and , and hence is regular.
Furthermore, accepts string iff accepts strings .
Consider the language of By the Little Problem, the set of lengths of words in is a finite union of linear sets For all , the set is the set of lengths of a subset of the words accepted by , all of the form . Since , is a subset of the integers such that is accepted by A, i.e. a subset of S. Furthermore, the finite disjoint union contains exactly all lengths of words accepted by , hence contains exactly all integers such that is accepted by A, i.e. .
S is thus a finite union of linear sets Hence by definition, S is ultimately periodic.
The binary case for the W-problem Consider a binary relation in and the corresponding formula with two free variables and . defines a set . Elements of the set are recognized by an automaton with parallel inputs and input alphabet . The language L of A is a subset of the regular language corresponding to . Thus the input string to the automaton is of the form or or .
Claim A pair belongs to some set for some iff the sets of possible lengths of the exponents are ultimately periodic.
Proof
- Only if: Let belong to . There exists an automaton A with parallel inputs which accepts the corresponding input string.
W.l.o.g, assume Then the input string can be of one of the two forms:
(a)
(b)
case (a): We want to show that the sets , and are ultimately periodic. Due to the little problem, it is sufficient to show that the language generated by the unary alphabet : is regular.
We show that is regular by constructing an accepting automaton, . Let be the automaton that accepts the original input string (a). Let be the accepting run in . In , there exist unique states and such that . Define . Similarly there exist unique such that . Define . contains all the states of that are in between and . And, is the restriction of to the transitions in between and . . Thus the automaton is defined unambiguously.
We can similarly construct automata for the languages and . In the former case, the start state corresponds to and the final state is the state (in ) from which there is a transition on consuming . In the latter case, the final state corresponds to and the start state is that state in that is reached after consuming .
The construction of the automata for case © is along the same lines.
If: If is an ultimately periodic set. then the expression where belongs to a unary alphabet and is a regular expression. This is because for each set one can construct a regular expression (ppp…a times) concatenated with the kleene closure of (ppp…b times). Since is the finite union of sets of the form , one can construct a regular expression which is the union of all the regular expressions formed as described above. Thus, is a regular expression for . We now extend our alphabet to include , and . The above argument for still holds. (a), (b) and © are all regular expressions formed by concatenation. Thus, the input strings are accepted by finite automata. They are satisfying interpretations of some formula in because (a) can be written as , and (b) is simply . © is symmetric to (a).
The above reasoning can be extended to the n-ary case. The input string has n non-zero elements and n+1 expressions of the form . A tuple belongs to an n-ary relation iff the possible values of each exponent forms an ultimately periodic set.
References:
[Buc60a] Julius Richard Buchi. On a decision method in restricted second-order arithmetic. In Proc. Internat. Cong. on Logic, Methodol., and Philos. of Sci. Stanford University Press, 1960.
[Elg61] Calvin C. Elgot. Decision problems of Finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98:21{52, 1961.
[Kla01] Nils Klarlund, Anders Moller. MONA Version 1.4 User Manual. BRICS, Department of Computer Science, University of Aarhus, 2001.