If space and time are discussed on the same page, as they are here, I'll use ps for polynomial space, and pt for polynomial time. For example, et ≥ ps. Let's see why this should be so.
Let m1 accept l1 in polynomial space, hence l1 is a ps language. Given an input word w, m1 can be treated as a bounded tm, or a btm. Its head will never move to the right of p(|w|), so we can cut the tape off at that point. If we include blanks, there are 3p possible snapshots of length p. Combine this with the position of the head on the tape, and the state of the machine, and the number of configurations is exponential. If m1 ever repeats a configuration, it is caught in an infinite loop. This is impossible, since m1 always halts. Without changing m1 in any way, we see that l1 belongs to et.
Next, let m1 be an ntm that recognizes l1 in polynomial time, whence l1 is npt. Let m2 be a tm that simulates m1 in the usual way, with its exponential slowdown. The size of the stack is proportional to p(|w|), hence the space consumed is a polynomial function of |w|. In other words, l1 is ps. Put this all together and write the following.
et ≥ ps ≥ npt ≥ pt
To bring nps into the picture, we need to explore quantified boolean expressions.
{ ∀x: x}
{ ∀x: { ∃y: (x|y) & (~x|~y) } }
The first says that for every x, x is true. Well - set x to false and that doesn't work, so the statement fails.
The second says that for every x, there is some y, such that x|y is true, and ~x|~y is also true. Set y = ~x, and this qbe is satisfied.
If all quantifiers are existential, the quantified boolean expression is merely a traditional boolean expression, and we are back to satisfiability. So, if a procedure validates an arbitrary qbe in polynomial time, then it solves satisfiability as well. The qbe problem is np hard.
Nobody knows if qbe's can be validated in np time, sowe we can't really call this problem np complete.
First the tm validates the syntax, and fails if the input word is not a well formed qbe. Free variables are not permitted.
An isGood() routine is passed, by offsets, a subformula within the input word. This begins with an open brace and ends with a close brace. The subformula specifies a quantifier and a variable. Assume the newly quantified variable is x.
Set x to 0 and push this result on the stack. This assignment hides any earlier definition of x. Evaluate the expression using substitution. Variables are replaced with 0 or 1, according to their values on the stack. If an inner qbe is encountered, call isGood() to see if it is true or false. If the entire expression comes out true, and the quantifier is existential, return true. We have found an x that works. If the expression comes out false, or the quantifier is universal, set x = 1 on the stack and evaluate the expression again. Return the result, true or false.
The first call to isGood(), when the stack is empty, sends the tm into success or failure, thus solving the qbe problem. The tm runs in linear space and exponential time. In other words, qbe is a ps problem.
You might think an ntm could solve the problem faster, but it's not clear how to use nondeterminism to make this happen.
Recall the reasoning used to prove satisfiability is np complete, as this proof is similar. Write a string of snapshots #x0#x1#x2#x3#x4#…#xk#, where k = qp3p, and q is the number of states in m1. We already showed that m1 terminates before this many steps are taken. Also, with a bound on space, each xi has length equal to p.
For convenience, repeat the last frame, until k becomes a power of 2.
Define an array as a set of boolean variables, one for each position in [0,p], crossed with each character in our snapshot alphabet. Remember that these characters include 0, 1, blank, and the composites, one per snapshot, that encode the input, current state, and next transition. An array automatically brings in the clauses that force exactly one character in each position.
One can write a boolean expression based upon two arrays s and t, such that t follows from s. Implications map 0 to 0, 1 to 1, blank to blank - except where there is a state transition. A final state simply carries forward, so that t becomes a copy of s. Remember that satisfiability built an entire chain of these arrays, with connecting logic between. We can't do that here, because the number of snapshots is exponential in p. The resulting boolean expression would be humungous! We need to take advantage of the universal quantifier.
The qbe starts out by asserting the existence of two arrays corresponding to the first and last snapshots. Call these s and t. Thus s is set to the input word (and the machines start state), and t has to have a final state.
Next, there exists an array m (for middle), halfway in between s and t.
Inside this scope, define a toggle variable u using the universal quantifier. For every u, true or false, the following must hold. There exists two arrays a and b, and if u is false, a = s and b = m, and if u is true, a = m and b = t.
At this point the construction of the qbe is recursive. There exists an array m halfway between a and b, and a universally quantified variable u, and arrays c and d, which are set to a and m, or m and b. Then assert the existence of another array halfway in between c and d, and another universal variable, and two more arrays, and so on. At the bottom of the procedure, when arrays are adjacent, we don't need m or u; boolean implications can be used, as they were in satisfiability, to force the second array to follow from the first.
The number of arrays is log2(k), which is proportional to p. Each array has p positions, so the number of variables in the qbe is prportional to p2. Each variable brings in a fixed number of clauses, so the entire qbe grows as p2. The conversion takes place in polynomial time.
Now I'm going to pull a rabbit out of my hat. Nothing in the above assumes m1 is deterministic. It need not be. Thus l1, living in np space, has been converted into a qbe, which can be solved in p space. When we switch to a deterministic machine, we may require a little more space, and a lot more time, but the bound on space remains polynomial. In other words, nps = ps. Here it is, all in one line.
et ≥ nps = ps ≥ npt ≥ pt