Reasoning about recursively defined data structures

ABSTRACT

A decision algorithm is given for the quantifier-free theory of recursively defined data structures which, for a conjunction of length n, decides its satisfiability in time linear in n. The first-order theory of recursively defined data structures, in particular the first-order theory of LISP list structure (the theory of CONS, CAR, CDR), is shown to be decidable but not elementary recursive.

REFERENCES

• 1: {Boyer and Moore 1977} R. Boyer and J Moore, "A Lemma Driven Automatic Theorem Prover for Recursive Function Theory", Proceedings of the Fifth IJCAI, 1977.
• 2: {Downey and Sethi 1977} P. Downey and R. Sethi, "Finding Common Subexpressions", submitted for publication.
• 3: {Goguen et al 1975} J. Goguen, J. Thatcher, E. Wagner and J. Wright, "Abstract Data-types as Initial Algebras and Correctness of Data Representations", Conference on Computer Graphics, Pattern Recognition and Data Structure, May 1975.
• 4: {Guttag, Horowitz, Musser 1976} J. Guttag, E. Horowitz and D. Musser, "Abstract Data Types and Software Validation", Technical Report ISI/RR-76-48, Information Sciences Institute, University of Southern California, August 1976, to appear CACM.
• 5: {Guttag and Horning 1977} J. Guttag and J. Horning, "The Algebraic Specification of Abstract Data Types", to appear Acta Informatica.
• 6: {Hoare 1975} C. A. R. Hoare, "Recursive Data Structures", International Journal of Computer and Information Sciences, June 1975.
• 7: {Johnson and Tarjan 1977} D. S. Johnson and R. E. Tarjan, "Finding Equivalent Expressions", manuscript.
• 8: {Mal'cev 1961} A. Mal'cev, "On the Elementary Theories of Locally Free Universal Algebras", Soviet Mathematics - Doklady, 1961.
• 9: {Mal'cev 1962} A. Mal'cev, "Axiomatizable Classes of Certain Types of Locally Free Algebras", Sibirskii Matematicheskii Zhurnal, 1962.
• 10: {McCarthy 1977} J. McCarthy, "Representations of Recursive Programs in First Order Logic", manuscript.
• 11: {Nelson and Oppen 1977} C. G. Nelson and D. C. Oppen, "Fast Decision Algorithms based on Union and Find", Proceedings of the 18th Annual IEEE Symposium on Foundations of Computer Science, October 1977.
• 12: Greg Nelson , Derek C. Oppen, A simplifier based on efficient decision algorithms, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-150, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512775]
• 13: {Paterson and Wegman 1977} M. Paterson and M. Wegman, "Linear Unification", to appear JCSS.
• 14: {Rackoff 1975} C. Rackoff, "The Computational Complexity of some Logical Theories", Ph. D. thesis, M. I. T., 1975.
• 15: {Tenney 1972} R. Tenney, "Decidable Pairing Functions", Ph. D. thesis, Cornell University, 1972.
• 16: {Tenney 1977} R. Tenney, "Decidable Pairing Functions", submitted for publication.
• 17: {Zilles 1975} S. Zilles, "Abstract Specifications for Data Types", IBM Research Laboratory, San Jose, 1975.