The transition relation h q, S i →I h q0, S0i holds1 • for I of type (1), when S1⊆ S, S0 = S ∪ S2, and q0 = p

P.U., 26 marca 2019, godzina 15: 38 strona1

Monotonic automata

A monotonic automaton is defined as M = h Q, R, f, I i, where

• Q is a finite set of states, with f ∈ Q as the final state.

• R is a finite set of registers;

• I is a finite set of instructions of the form:

(1) I = q : check S1; set S₂; jmp p, or (2) I = q : jmp p1 and p2,

where p, p₁, p₂∈ Q and S₁, S₂ ⊆ R.

We define a configuration of M as a pair h q, S i, where q ∈ Q and S ⊆ R. The transition relation h q, S i →_I h q⁰, S⁰i holds¹

• for I of type (1), when S₁⊆ S, S⁰ = S ∪ S₂, and q⁰ = p;

• for I of type (2), when S₀⊆ S = S⁰, and q⁰ = p₁ or q⁰ = p₂. A configuration h q, S i is accepting when either q = f , or

• h q, S i →_Ih q⁰, S⁰i, where I is of type (1), and h q⁰, S⁰i is accepting, or

• h q, S i →_Ih q⁰, S i, h q⁰⁰, S i, where I is of type (2), and both h q⁰, S i, h q⁰⁰, S i are accepting.

The halting problem for monotonic automata is

“Given M, q, S, is h q, S i an accepting configuration of M?”

Example 1 Consider a finite automaton A, with states {0, ..., k}, the initial state 0, and the final state k. Given a word w = a₁...a_n, we define a monotonic M such that A accepts w if and only if the initial configuration h q₀, r⁰₀i is accepting.²

States of M are q⁰, q¹, ..., qⁿ, f where q⁰ is initial and f is final. Registers are r_i^t, for t ≤ n and i ≤ k. For all t = 0, ..., n − 1, we have an instruction

q^t: check r^t_i; set r_j^t+1; jmp q^t+1,

whenever A, reading a_t+1 in state i, can enter state j. For t = n, we take qⁿ: check rⁿ_k; set ∅; jmp f .

Then an accepting computation of A, consisting of states 0, s₁, s₂, ..., s_n = k, is represented by a computation of M, ending in h f, r⁰₀, r_i¹₁, ..., r_iⁿ_ni. Note that the instructions of M are all of type (1), i.e., there is no alternation.

Correctness: By induction with respect to n − t one shows that a configuration of the form h q^t, r₀⁰, ..., r^t_iti is accepting if and only if A accepts the suffix a_t+1...an of w from state i_t.

1Note that states are not classified as existential or universal, only instructions.

2We write sets without { } whenever it is convenient.

P.U., 26 marca 2019, godzina 15: 38 strona2

Lemma 2 The halting problem for monotonic automata is Pspace-hard.

Proof: We encode an alternating TM working in polynomial time p(n). Suppose there are k states, and let the input word be w = a1...an. Assume for simplicity that the TM does not write nor move in universal states, and that an accepting computation takes exactly p(n) steps. Define an M with registers

stan^t_s, lit^t_ia, poz^t_i,

where 1 ≤ s ≤ k, 0 ≤ t ≤ p(n), 1 ≤ i ≤ p(n), and a is any symbol of TM. The registers represent, respectively, the state, symbol and machine head at time t in position i. States of M are loop^t_i, split^t_s

1s2, and go^t_s (for appropriate t, i, s), and the final state f . The initial ID of TM is represented by the configuration

C₀ = h loop⁰₁, {lit⁰_1a1, ..., lit⁰_nan, lit⁰_n+1B, ..., lit⁰_p(n)B, stan⁰₀, poz⁰₀} i, where B is blank. For any universal state s of TM, we have these instructions:

loop^t_i : check stan^t_s, lit^t_ia, poz_j^t; set lit^t+1_ia , poz^t+1_j ; jmp loop^t_i+1; loop^t_p(n) : check stan^t_s, lit^t_p(n)a, poz^t_j; set lit^t+1_p(n)a, poz^t+1_j ; jmp split_s^{t +1}_1s2;

split^t+1_s1s2 : jmp go^t+1_s1 and go^t+1_s2 ; go^t+1_s1 : check ∅; set stan^t+1s1 ; jmp loop^t+1₁ ; go^t+1_s2 : check ∅; set stan^t+1s2 ; jmp loop^t+1₁ ,

for 1 ≤ i < p(n), and 1 ≤ j ≤ p(n), and 0 ≤ t < p(n), and the appropriate a, s, s₁, s2.

Now suppose that s is an existential state; then any move of the form (s, a) ⇒ (u, b, +ε) yields the following instructions, where 1 ≤ i < p(n), and 0 ≤ t < p(n), and j 6= i:

loop^t_i: check stan^t_s, poz^t_i, lit^t_ia; set stan^t+1_u , poz^t+1_i+ε, lit^t+1_ib ; jmp loop^t_i+1; loop^t_i: check stan^t_s, poz^t_j, lit^t_ia; set lit^t+1_ia ; jmp loop^t_i+1;

loop^t_p(n) : check stan^t_s, poz^t_p(n), lit^t_p(n)a; set stan^t+1_u , poz^t+1_p(n)+ε, lit^t+1_p(n)b; jmp loop^t+1₁ ; loop^t_p(n): check stan^t_s, poz^t_j, lit^t_p(n)a; set lit^t+1_p(n)a; jmp loop^t+1₁ .

To complete a computation we use

loop^p(n)₁ : check stan^p(n)_f ; set ∅; jmp f , where f is the accepting state of TM.

Correctness: Suppose that our TM, after t steps of computation, scans a on the i-th tape cell in an existential state s. Let (s, a) ⇒ (u, b, +ε) be an applicable move.

This ID of TM corresponds to a configuration h loop^t₁, S i, where S consists all registers stan^u_r, lit^u_jb, poz^u_j that correctly represent the computation steps u ≤ t. In particular, registers stan^t_s, lit^t_ia, poz^t_i are already set. From state loop^t₁our M collects the information about the next ID:

moving from loop^t_j to loop^t_j+1 it sets the register corresponding to the j-th tape cell. For i = j, it also updates the TM state and head position. The loop is completed by a return to loop^t+1₁ . In the universal case the tape is unchanged and the head is not moved, yet a round of p(n)

P.U., 26 marca 2019, godzina 15: 38 strona3

steps is needed to write this information into memory using states loop^t_j. After that the universal step of TM is implemented using state split^t+1_s1s2.

In the opposite direction we can observe that any computation of M must essentially obey the above pattern: the choice of registers to set is determined by TM transitions.

To make the above fully precise one should define what it means that “a set S ⊆ R encodes an ID of the form J = x₁...xjqxj+1...x_p(n)of TM at time t” and prove that in this case h loop^t₁, S i is accepting iff the TM accepts J in time p(n) − t. This pleasure is left to the reader. 

Corollary 3 Propositional intutionistic logic is Pspace-hard.

Proof: Consider a monotonic automaton M and an ID of the form C₀ = h q0, S0i. Using states and registers of M as propositional atoms, we define a set of axioms Γ so that Γ ` q₀ if and only if C₀ is accepting. The set Γ contains the atoms S₀∪ {f }; the other axioms represent instructions of M.

An axiom for q : check S1; set S2; jmp p, where S1 = {s¹₁, ..., s^k₁} and S₂= {s¹₂, ..., s^`₂}, is:

(1) s¹₁→ · · · → s^k₁ → (s¹₂→ · · · s^`₂→ p) → q.

And for every instruction q : jmp p₁ and p2, there is axiom

(2) p1→ p₂ → q.

For every S ⊆ R, we prove that Γ, S ` q if and only if C = h q, S ∪ S₀i is accepting. We think of Γ as of a type environment where each axiom is a declaration of a variable.

(⇒) Induction with respect to proofs. Any normal proof T of an atom q must be a variable or an application, say T = x ~N , The case of x : f (i.e., q = f ) is obvious; otherwise the type of x corresponds to an instruction. There are two possibilities:

(1) If x : s¹₁ → · · · → s^k₁ → (s¹₂ → · · · s<sup>`</sup><sub>2</sub> → p) → q, then T = xD<sub>1</sub>...Dk(λu1:s<sup>1</sup><sub>2</sub>...λu`:s^`₂. P ).

Terms D₁, ..., D_k are of types s¹₁, ..., s^k₁ respectively, and they must be variables declared in S, as there is no other assumption with target s¹₁, ..., s^k₁. This means that S⁰ ⊆ S. Hence the instruction corresponding to x is applicable at C = h q, S i and yields C⁰ = h p, S ∪ S⁰i. In addition we have Γ₀, S ∪ S⁰ ` P : p, whence C⁰ is accepting by the induction hypothesis.

(2) If x has type p₁ → p₂→ q then T = xT₁T₂. The appropriate universal instruction leads to two IDs: C₁ = h p₁, S i and C₂ = h p₂, S i. The judgments Γ₀, S ` T<sub>1</sub> : p<sub>1</sub> and Γ<sub>0</sub>, S ` T₂ : p₂ obey the induction hypothesis. Thus C₁, C2 are accepting and so is C.

(⇒) Induction with respect to computations.