SKEDSOFT

Encoding conventions: We now define the encoding conventions for natural numbers employed in our automaton construction. We define natural numbers in base 2 using a bit-serial format, with the least significant bit (LSB) appearing leftmost. This means that when viewed as inputs of DFA, numbers will be consumed LSB-first. For example, 13 is written as 1011 (or as 10110, or in general, with as many zeros to the right). Pairs of natural numbers are represented as a sequence of tuples, and in general k-tuples of natural numbers are represented as a sequence of k-tuples. k-tuples of zeros may be added to the right without changing the meaning of these representations. For example, 13, 6 is represented as 1, 00, 11, 11, 0.

Example 1 — representing x ≤ 2

Figure 20.2 shows how a DFA for x ≤ 2 is represented. Before seeing any of the bits of x (that will, as explained above, arrive LSB-first), the value of “x seen so far” is 0. At this stage, the imbalance between x and

Fig. 20.3. DFA for x y = 1. The transition names are referred to in Section 20.1.5.
2 is 2—which is what the initial state of the automaton is labeled with. When a 0 bit arrives, the magnitude of “x seen so far” is still 0. As far as the next bit of x yet to arrive is concerned, it possesses a positional weight that is two times the weight of the LSB. However, we want to restore an ‘inductive’ situation in our DFA diagram; therefore, our convention will be that we will ‘div’ (divide with truncation) both sides of the equation by 2. This results in the weight imbalance reducing to 1—exactly equal to the state label of the state to which state 2 transitions. On the other hand, if the LSB were to be 1, we advance to state 0 which is (2−1) div 2. It is also apparent that a sequence such as 011 represents, in the new format, the number 6. Since 6 ≤ 2 does not hold, the machine moves to a “black hole” state labeled with BH, and stays there forever. The language of the DFA in Figure 20.2 includes all bit-serial sequences representing natural numbers that satisfy this formula; for instance, 01 = 210 as well as 10 = 110 are both in the language of this DFA.

NFA for ∃y.(x y) = 1:                                                                                   DFA for ∃y.(x y) = 1:                                                                                    

Example 2 — ∀x.∃y.(x y) = 1
We continue example-driven, now demonstrating how to show the nonvalidity of the sentence ∀x.∃y.(x y) = 1. To that end, we start with the matrix sub-formula (x y) = 1, and build up the whole formula, as will now be described.

Subformula (x y) = 1: As illustrated in Figure 20.3, we build a DFA that can handle the bitserial left-to-right arrival of the bits comprising x y = 1.When 1, 1 arrives, the machine is thrown into the black hole (BH) state because the left-hand side of the equation adds up to at least 2 now, and will from now on never equal the right-hand side. The reason we mention at least is because the LSB of x and the LSB of y are both 1s, as captured by the pair 1, 1 that has just arrived; and hence, even if the entire sequence of tuples yet to arrive were to be 0, 0, the left-hand side would be 2. The accepting runs are either 0, 1 or 1, 0 followed by an arbitrary number of 0, 0s.

Subformula ∃y.(x y) = 1: The meaning of ∃y.x y = 1 is that one should take the disjunction of x y = 1 with y set to 0 and 1, in turn (y is a Boolean variable owing to our following a bit-serial format). In the automaton world, this effect would be attained if we project away the second component of the pairs from the alphabet (e.g., x, y would become just x). The resulting machine—an NFA now—is shown in Figure 20.4. Determinizing, we obtain the DFA also shown in the same figure. This DFA shows that if the LSB of x is a 0 or a 1, the machine can be in a final state (y can be internally chosen to be 1 or 0, respectively, thus still satisfying the equation).