harrisj:
Thanks for the bouquet. It's only because I happen to be
good at remembering this esoteric excreta.

You mentioned verification in P-time, and I think it's
worth exploring what that means. One
technical definition of the class NP is:

NP is the class of decision problems (languages)
*L* such that there is a polynomial time function
*f(x,c)* where *x* is a string, *c* is
another string whose size is polynomial in the size of
*x*, and *f(x, c)=True* if and only if *x* is
in *L*.

(taken from the
comp.theory FAQ)

As an example, *x* might be a graph,
*c* might be a path in that graph, and *f(x, c)*
is the function "is *c* a Hamiltonian path in the graph
*x*?"

There are at least *three* kinds of questions that
you may want to ask about this problem, given *x*.
They are:

- Is
*x* in *L*, that is, does there exist
*c* such that *f(x, c)=True*? That question
corresponds to "does the graph have a Hamiltonian cycle"?
Or "is the number composite"? This is called a "decision
problem", and is *not* necessarily verifiable in P
(unless P=NP, of course), because verifying an answer is
identical to finding
the answer.
- Given
*x*, give me a *c* which proves that
*x* is in *L*. This kind of problem is trivially
certifiable in P, because all you need to do is take the
certificate *c* and compute the value of *f(x,
c)*. This question corresponds to "find me a Hamiltonian
cycle in this graph", or "find me factors of this
number".
- Given
*x*, find me the certificate *c* which
minimises (or maximises) some cost function *cost(c)*.
This is called an "NP optimisation problem", and corresponds
to something like "find me the Hamiltonian cycle of minimal
distance" (i.e. the travelling salesman problem). I don't
know whether this kind of problem is certifiable in P or
not. Could
someone please let me know?

Now to EXPTIME. EXPTIME-hard problems are not
certifiable in P-time if the certificate is polynomial in
the size of the input. If they were, you could construct a
nondeterministic polynomial algorithm to solve them.
(Nondeterministically guess the certificate in NP time then
test it in P time.) So I guess EXPTIME-hard public-key
systems and zero-knowledge proof systema aren't feasable.
Darn.

If the certificate were not polynomial
in the size of the input, that might be a different matter.
That is, certifying EXPTIME-hard problems might be
polynomial in the size of the certificate. I'm not sure
about that one.

EXPTIME-hard problems often turn up
when dealing with logic and theorem proving (e.g. constraint
systems, conditional logic) or formal languages and the
machines which generate/recognise them (e.g. tree
automata). Here are some example EXPTIME-complete
problems:

- Evaluation of datalog queries for single rule programs
containing only a single clause.
- For tree automata, the intersection problem (i.e. given
two tree automata, is the intersection of their languages
empty) and equivalence problem (do two given tree automata
accept the same language)
- Removing recursion from formulas in the mu calculus
(i.e. given a recursive formula, give me a non-recursive
equivalent if it exists)
- Satisfiability for definite set constraints
- Determining a winning strategy for chess generalised to
an N*N board or go generalised to an N*N board. I'm not
entirely sure how you generalise chess piece movement, but
there you go.

And just for fun, here are a couple of NEXPTIME-complete
problems:

- Satisfiability for two-variable first-order logic.
- Provability in first-order multiplicative additive
linear logic

Naturally, NEXPTIME-complete problems are certifiable in
EXPTIME.

Happy theory nerding.