Even simple programs are hard to analyze

ABSTRACT

It has long been known that most questions of interest about the behavior of programs are recursively undecidable. These questions include whether a program will halt, whether two programs are equivalent, whether one is an optimized form of another, and so on. On the other hand, it is possible to make some or all of these questions decidable by suitably restricting the computational ability of the programming language under consideration. The Loop language of Meyer and Ritchie [MR], for example, has a decidable halting problem, but undecidable equivalence. Restricting the computational ability still further, virtually all of these questions are decidable for finite automata and generalized sequential machines (except that Griffiths [Gri] has shown equivalence undecidable for nondeterministic gsms).A natural question to ask is how hard it is to solve these problems for programming languages for which they are decidable, and it is with this area that we are concerned in this paper. In particular we describe a programming language modeled on current higher-level languages which has exactly the computational power of deterministic finite state transducers with final states, and analyze the space and time required to decide various questions of programming interest about the language. We find that questions about halting, equivalence, and optimization are already intractable for this very simple language. We also study extensions to the language such as simple arithmetic capabilities, arrays, and recursive subroutines with both call-by-value and call-by-name parameter passing mechanisms, some of which extend the capabilities of the language and/or increase the complexity of its decidable problems. In one case, that of recursion with call-by-name, the previously decidable questions are seen to become undecidable.

REFERENCES

• 1: Stephen A. Cook, Characterizations of Pushdown Machines in Terms of Time-Bounded Computers, Journal of the ACM (JACM), v.18 n.1, p.4-18, Jan. 1971 [doi>10.1145/321623.321625]
• 2: T. V. Griffiths, The unsolvability of the Equivalence Problem for Λ-Free nondeterministic generalized machines, Journal of the ACM (JACM), v.15 n.3, p.409-413, July 1968 [doi>10.1145/321466.321473]
• 3: John E. Hopcroft , Jeffrey D. Ullman, Formal languages and their relation to automata, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1969
• 4: Neil D. Jones , William T. Laaser, Complete problems for deterministic polynomial time, Proceedings of the sixth annual ACM symposium on Theory of computing, p.40-46, April 30-May 02, 1974, Seattle, Washington, United States [doi>10.1145/800119.803883]
• 5: {MR} Meyer, Albert R., and Dennis M. Ritchie, Computational Complexity and Program Structure, IBM Research Paper RC-1817, May 1967.
• 6: {MS} Meyer, Albert R., and L. J. Stockmeyer, The equivalence problem for regular expressions with squaring requires exponential space, Thirteenth Annual Symposium on Switching and Automata Theory, October 1972, pp. 125-129.
• 7: Marvin Lee Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 8: {Ros} Rosenberg, Arnold, On multi-head finite automata, Proceedings of the Fifth Annual Symposium on Switching Circuit Theory and Logical Design, 1963, pp. 221-228.