ON SOME DECISION-PROBLEMS IN PROGRAMMING

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 Pi(2)(0)-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 Pi(2)(0)-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. (C) 1995 Academic Press, Inc.