Finally, the PSpace lower bound is obtained by reducing from emptiness of register automata over \((\mathbb {N}, \lbrace =\rbrace )\) , which is PSpace-c [1]}. Since the data domains are countable, they can always simulate \((\mathbb {N},\lbrace =\rbrace )\) , and the proofs of [2]} can easily be adapted: given a NRA \(A\)  over \((\mathbb {N},\lbrace =\rbrace )\) , define a relation associating words of the form \(w\# x\)  with \(w \in L(A)\)  and \(x \in \mathcal {D}^\omega \)  to all elements of \(\mathcal {D}^\omega \) ; it is functional if and only if its domain is empty. Similarly, given some non-continuous function \(g\)  defined by some NRT, define the function \(w\#x \mapsto g(x)\)  for all \(w \in L(A)\)  and \(x \in \mathcal {D}^\omega \) . Again, it is continuous iff it is empty; similarly for uniform continuity.

Thus, given a specification represented as a NRT over a representable and decidable domain, one can examine whether it can be implemented (provided it is functional, which is then decidable) by checking whether it is computable. Indeed, computability is the most liberal criterium for being realisable. The notion of uniform computability then allows to refine this check, as for functions that are uniformly computable, one can focus on implementations that have a bounded lookahead. In the case of \((\mathbb {Q},\left\lbrace  < \right\rbrace )\) , we further get that both problems are \(\textsc {PSpace} \) -complete:

For relations given by NRT over \((\mathbb {Q},\left\lbrace  < \right\rbrace )\)  deciding functionality, continuity/computability and uniform continuity/uniform computability are PSpace-complete.


We only need to argue that \((\mathbb {Q},\left\lbrace  < \right\rbrace )\)  is representable and polynomially decidable.
Clearly rational numbers are representable.
Moreover, since \((\mathbb {Q},\left\lbrace  < \right\rbrace )\)  is homogeneous, it admits quantifier elimination, which means that any \(k\) -type can be defined by a formula polynomial in \(k\)  (actually linear). Indeed a type is just given by the linear order between the free variables.
Moreover, satisfiability of first-order logic over \((\mathbb {Q},\left\lbrace  < \right\rbrace )\)  is in PSpace.

Note that the same reasoning applies for \((\mathbb {N},\left\lbrace  = \right\rbrace )\) ; the case of \((\mathbb {N},\left\lbrace  = \right\rbrace )\)  can also be obtained by encoding it in \((\mathbb {Q},\left\lbrace  < \right\rbrace )\) .
