3.6  Decidable Properties for Recursive Finite-Domain Programs

The first theorem of this section provides a generalization of the decidability of the emptiness problem for finite-state automata.

Theorem 3.6.1    The emptiness problem is decidable for pushdown automata.

Proof     Consider any pushdown automaton M₁ = <Q, , , ₁, q₀, Z₀, F>. Let c be a new symbol not in . Let ₂ be ₁ with each transition rule of the form (q, , , p, ) being replaced with a transition rule of the form (q, c, , p, ). Let M₂ be the pushdown automaton <Q, {c}, , ₂, q₀, Z₀, F>.

Intuitively, we see that M₂ is the pushdown automaton M₁ modified to read the symbol c whenever M₁ is to make a move that reads no input symbol. By construction, M₁ can reach configuration (uqv, w) in t moves if and only if there exists u_c such that M₂ can reach configuration (u_cqv, w) in t moves, where u_c is a string obtained from u by insertion of some c's and |u_c| = t. Thus, T(M₁) = Ĝ if and only if T(M₂) = Ĝ.

Denote m as the constant that the pumping lemma for context-free languages implies for L(M₂). The shortest string x in L(M₂) cannot be longer than m. Otherwise, a contradiction would arise because by the pumping lemma if x is in L(M₂) and if its length is at least m, then a shorter string is also in L(M₂).

On input x the pushdown automaton M₂ can have at most |x| moves. Consequently, the emptiness of L(M₂) or, equivalently, of L(M₁) can be checked by considering all the possible execution sequences of M₂ or, equivalently, of M₁ that consist of no more than m moves.

The decidability of the emptiness problem for pushdown automata can be used for showing the decidability of some problems for finite-state transducers. One such example is the decidability of the equivalence problem for deterministic finite-state transducers. For the general class of finite-state transducers as well as the class of pushdown automata the problem is undecidable (Corollary 4.7.1 and Corollary 4.7.2, respectively). On the other hand, for deterministic pushdown automata and for deterministic pushdown transducers the problem is open.

Corollary 3.6.1    The equivalence problem is decidable for deterministic finite-state transducers.

Proof     Consider any two deterministic finite-state transducers M₁ and M₂. From M₁ and M₂ a finite-state automaton M₃ can be constructed such that M₃ accepts the empty set if and only if L(M₁) = L(M₂). The construction can be as in the proof of Theorem 2.6.4.

On the other hand, one can also construct from M₁ and M₂ a pushdown automaton M₄ that accepts a given input if and only if both M₁ and M₂ accept it, while providing different outputs. That is, M₄ accepts the empty set if and only if M₁ and M₂ agree in their outputs on the inputs that they both accept.

A computation of M₄ on a given input consists of simulating in parallel, as in the proof of Theorem 3.5.1, the computations of M₁ and M₂ on such an input. The simulation is in accordance with either of the following cases, where the choice is made nondeterministically.

Case 1

M₄ simulates accepting computations of M₁ and M₂ that provide outputs of different lengths. During the simulation, M₄ ignores the outputs of M₁ and M₂. However, at each instant of the simulation, the pushdown store of M₄ holds the absolute value of the difference between the length of the outputs produced so far by M₁ and M₂. M₄ accepts the input if and only if it reaches accepting states of M₁ and M₂ at the end of the input, with a nonempty pushdown store.

Case 2

M₄ simulates accepting computations of M₁ and M₂ that provide outputs differing in their jth symbol, for some j that is no greater than their lengths. The simulation is similar to that in Case 1. The main difference is that M₄ records in the pushdown store the changes in the length of the output of M_i only until it establishes (nondeterministically) that M_i reached its jth output symbol, i = 1, 2. In addition, M₄ records in its finite-state control the jth output symbols of M₁ and M₂. Upon completing the simulation, M₄ accepts the input if and only if its pushdown is empty and the recorded symbols in the finite-state control are distinct.

The uniform halting problem is undecidable for pushdown automata (Corollary 4.7.3). However, the decidability of the emptiness problem for pushdown automata can be used to show the decidability of the uniform halting problem for deterministic pushdown automata.

Theorem 3.6.2    The uniform halting problem is decidable for deterministic pushdown automata.

Proof     Consider any deterministic pushdown automaton M₁. From M₁ a deterministic pushdown automaton M₂, similar to that in the proof of Lemma 3.5.1, can be constructed. The only difference is that here M₂ accepts a given input if and only if it determines that M₁ reaches a simple loop. By construction, M₂ accepts an empty set if and only if M₁ halts on all inputs.

The proof of the last theorem fails for nondeterministic pushdown automata because accepting computations of nondeterministic pushdown automata can include simple loops, without being forced to enter an infinite loop.

Theorem 3.6.3    The halting problem is decidable for pushdown automata.

Proof     Consider any pair (M, x) of a pushdown automaton M and of an input x for M. From x, a finite-state automaton M_x can be constructed that accepts only the input x. However, from M, a pushdown automaton M₁ can be constructed to accept a given input if and only if M has a sequence of transition rules that leads M to a simple loop on the input. The construction can be similar to the proof of Theorem 3.6.2.

From M and M_x, a pushdown automaton M_a,x can be constructed that accepts the intersection of L(M) with L(M_x) (see Theorem 3.5.1). By construction, M_a,x accepts a nonempty set if and only if M accepts x. By Theorem 3.6.1 it can be determined if M_a,x accepts a nonempty set. If so, then M is determined to halt on input x. Otherwise, in a similar way, a pushdown automaton M_1,x can be constructed to accept the intersection of L(M₁) and L(M_x). By construction, M_1,x accepts the empty set if and only if M has only halting computations on input x. The result then follows from Theorem 3.6.1.

[next] [prev] [prev-tail] [front] [up]