I&C Journal 1995 Journal Article
On Some Decision Problems in Programming
- D. Spreen
One of the central problems in programming is the correctness problem, i. e. , the question of whether a program computes a given function. We choose a rather general formal semantical framework, effectively given topological T 0-spaces, and study the problem to decide whether an element of the space is equal to a fixed element. Moreover, we consider the problems of deciding for two elements, whether they are equal and whether one approximates the other in the specialization order. These are one-one equivalent for a large class of spaces, including effectively given Scott domains. All these problems are undecidable. In most cases they are complete on some level of the arithmetical and/or the Boolean hierarchy. The complexity respectively depends on whether the fixed element is not finite and whether the space contains a nonfinite element. The problem of deciding whether an element is not finite is potentially Π 0 2-complete and for domain-like spaces the membership problem of any nonempty set of nonfinite elements that intersects the effective closure of its complement is Π 0 2-hard. If the given element is finite or the space contains only finite elements, the complexity also depends on the location of the given element in the specialization order and/or the boundedness of the set of lengths of all decreasing chains of basic open sets.