Abstract
We propose a mathematical foundation for reasoning about the correctness and computational complexity of record handling algorithms, using algebraic methods recently introduced in graph theory. A class of pattern matching and replacement rules for graphs is specified, such that applications of rules in the class can readily be programmed as rapid transformations of record structures. When transformations of record structures are formalized as applications of rules to appropriate graphs, recent Church-Rosser type theorems of algebraic graph theory become available for proving that families of transformations are well behaved. In particular, we show that any Church-Rosser family of transformations can be combined with housekeeping operations involving indirect pointers and garbage collection without losing the Church-Rosser property, provided certain mild conditions on the rules defining the family are satisfied. This leads to suggestions for the design of record handling facilities in high level languages, especially when housekeeping chores are to be performed asynchronously by service processes that run in parallel with the main process. We also show how to express the net effect of two transformations as a single transformation. These results and the general theorems that support them can be used to analyze the behavior of a large record structure that can be updated asynchronously by several parallel processes or users.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
T.W. Doeppner, Parallel program correctness through refinement, Proc. 4th ACM Symp. on Principles of Programming Languages, Santa Monica, January 1977, pp. 155–169.
H. Ehrig & H.J. Kreowski, Categorical theory of graph grammars, Rept. 75-08, Tech. U. Berlin, February 1975.
H. Ehrig, M. Pfender, & H.J. Schneider, Graph grammars: an algebraic approach, Proc. 14th Ann. IEEE Symp. on Switching and Automata Theory, Iowa City, October 1973, pp. 167–180.
H. Ehrig & B.K. Rosen, Commutativity of independent transformations on complex objects, IBM Research Report RC 6251, October 1976.
D. Gries, On believing programs to be correct, CACM 20 (1977), 49–50.
H. Herrlich & G. Strecker, Category Theory, Allyn and Bacon, Rockleigh, 1973.
D.E. Knuth, The Art of Computer Programming, Vol. 1 (2nd ed.), Addison-Wesley, Reading, 1973.
B.K. Rosen, Tree-manipulating systems and Church-Rosser theorems, JACM 20 (1973), 160–187.
B.K. Rosen, Deriving graphs from graphs by applying a production, Acta Inf. 4 (1975), 337–357.
B.K. Rosen, Correctness of parallel programs: the Church-Rosser approach, Th. Comp. Sci. 2 (1976), 183–207.
R. Sethi, Testing for the Church-Rosser property, JACM 21 (1974), 671–679.
N. Wirth & C.A.R. Hoare, A contribution to the development of ALGOL, CACM 9 (1966), 413–431.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1977 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ehrig, H., Rosen, B.K. (1977). The mathematics of record handling. In: Salomaa, A., Steinby, M. (eds) Automata, Languages and Programming. ICALP 1977. Lecture Notes in Computer Science, vol 52. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-08342-1_16
Download citation
DOI: https://doi.org/10.1007/3-540-08342-1_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-08342-9
Online ISBN: 978-3-540-37305-6
eBook Packages: Springer Book Archive