Graph types

ABSTRACT

Recursive data structures are abstractions of simple records and pointers. They impose a shape invariant, which is verified at compile-time and exploited to automatically generate code for building, copying, comparing, and traversing values without loss of efficiency. However, such values are always tree shaped, which is a major obstacle to practical use. We propose a notion of graph types, which allow common shapes, such as doubly-linked lists or threaded trees, to be expressed concisely and efficiently. We define regular languages of routing expressions to specify relative addresses of extra pointers in a canonical spanning tree. An efficient algorithm for computing such addresses is developed. We employ a second-order monadic logic to decide well-formedness of graph type specifications. This logic can also be used for automated reasoning about pointer structures.

REFERENCES

• 1: Hassan Aït-Kaci , Roger Nasr, Logic and inheritance, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.219-228, January 01, 1986, St. Petersburg Beach, Florida [doi>10.1145/512644.512664]
• 2: H Aït-Kaci , R Nasr, Login: A logic programming language with built-in inheritance, Journal of Logic Programming, v.3 n.3, p.185-215, Oct. 1986 [doi>10.1016/0743-1066(86)90013-0]
• 3: H. Ai't-Kaci and A. Podelski. Towards a meaning of life. In Jan Maluszyfiski and Martin Wirsing, editors, Proceedings of the 3rd International Symposium on Programming Language Implementation and Logic Programming (Passau, Germany), pages 255-274. Springer-Verlag, LNCS 528, August 1991.
• 4: Bruno Courcelle, The monadic second-order logic of graphs. I. recognizable sets of finite graphs, Information and Computation, v.85 n.1, p.12-75, March 1990 [doi>10.1016/0890-5401(90)90043-H]
• 5: J. DSrre and W.C Rounds. On subsumption and semiunification in feature algebras. In Proc. IEEE Symp. on Logics in Computer Science, pages 300-310, 1990.
• 6: Laurie J. Hendren , Joseph Hummell , Alexandru Nicolau, Abstractions for recursive pointer data structures: improving the analysis and transformation of imperative programs, Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation, p.249-260, June 15-19, 1992, San Francisco, California, United States
• 7: C.A.R. Hoare. Reeursive data structures. In~ernational Journal of Computer and Information Sciences, 4:2:105-132, 1975.
• 8: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 9: T. Reps, Incremental evaluation for attribute grammars with unrestricted movement between tree modifications, Acta Informatica, v.25 n.2, p.155-178, February 1988
• 10: D. A. Turner, Miranda: a non-strict functional language with polymorphic types, Proc. of a conference on Functional programming languages and computer architecture, p.1-16, January 1985, Nancy, France

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.2 Nonnumerical Algorithms and Problems
          Subjects: Computations on discrete structures

  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Trees

General Terms:
Algorithms, Languages, Theory