Tree-Manipulating Systems and Church-Rosser Theorems

ABSTRACT

Subtree replacement systems form a broad class of tree-manipulating systems. Systems with the “Church-Rosser property” are appropriate for evaluation or translation processes: the end result of a complete sequence of applications of the rules does not depend on the order in which the rules were applied. Theoretical and practical advantages of such flexibility are sketched. Values or meanings for trees can be defined by simple mathematical systems and then computed by the cheapest available algorithm, however intricate that algorithm may be. We derive sufficient conditions for the Church-Rosser property and discuss their applications to recursive definitions, to the lambda calculus, and to parallel programming. Only the first application is treated in detail. We extend McCarthy's recursive calculus by allowing a choice between call-by-value and call-by-name. We show that recursively defined functions are single-valued despite the nondeterminism of the evaluation algorithm. We also show that these functions solve their defining equations in a “canonical” manner.

REFERENCES

• 1: BLUM, E.K. Towards a theory of semantics and compilers for programming languages. J. Comput. Syst. Sci. 8 (1969), 248-275.
• 2: BRAINERI), W.S. Tree generating regular systems. Inform. and Contr. t4 (1969), 217-231.
• 3: CHURCH, A., ANn ROSSEa, J B Some properties of conversion Trans. Amer Math Soc. 89 (1936), 472-482.
• 4: CURRY, H. B., AND FEYS, R. Combinatory Logic. North-Holland Pub. Co., Amsterdam, 1958.
• 5: HINDLEY, R. The Church-Rosser property and a result in combinatory logic. Ph.D. Th., U. of Newcastle-upon-Tyne, England, 1964.
• 6: tIINDLEY, R. An abstract form of the Church-Rosser theorem, Part I. J. Symbolic Logic 84 (1969), 545-560.
• 7: KARP, R. M., AND MILLER, R.E. Parallel program schemata. J. Comput. Syst. Sci. 8 (1969), 147-195.
• 8: KLEENE, S.C. Introduction to Metamathematzcs. Van Nostrand, New York, 1952.
• 9: I~/{_~RTIN-LoF, P. A theory of types (unpublished manuscript, 1971).
• 10: John McCarthy, Recursive functions of symbolic expressions and their computation by machine, Part I, Communications of the ACM, v.3 n.4, p.184-195, April 1960 [doi>10.1145/367177.367199]
• 11: MCCARTHY, J. Basis for a mathematical theory of computation In Computer Programming and Formal Systems, P. Braffort, and D. Hirschberg (Eds), North-Holland Pub. Co, 1963, pp. 33-70.
• 12: Marvin Minsky, Form and Content in Computer Science (1970 ACM turing lecture), Journal of the ACM (JACM), v.17 n.2, p.197-215, April 1970 [doi>10.1145/321574.321575]
• 13: MITSCHKE, G. Eine algebraische Behandlung yon ;~-K-Kalkul und Kombinatorischer Logik. Ph.D. Th., Rheinischen Friedrich-Wilhelms U., Bonn, Germany, 1970.
• 14: MoRRIs, J. H. JR Lambda-calculus models of programming languages. Proj. MAC, Rep. MAC-TR-57, MIT, Cambridge, Mass., 1968.
• 15: J. W. Backus , F. L. Bauer , J. Green , C. Katz , J. McCarthy , A. J. Perlis , H. Rutishauser , K. Samelson , B. Vauquois , J. H. Wegstein , A. van Wijngaarden , M. Woodger , P. Naur, Revised report on the algorithm language ALGOL 60, Communications of the ACM, v.6 n.1, p.1-17, Jan. 1963 [doi>10.1145/366193.366201]
• 16: ROSEN, B.K. Subtree replacement systems. Tech Rep. 2-71, Ctr. for Res. in Computing Technology, Harvard U., Cambridge, Mass., 1971.
• 17: SANCHIS, L.E. Functionals defined by recursion. Notre Dame J. Formal Logic 8 (1967), 161-174.
• 18: SCHROER, D.E. The Church-Rosser theorem. Ph.D. Th., Cornell U., ithaca, N.Y., 1965.
• 19: H. R. Strong, Jr., Translating recursion equations into flow charts, Proceedings of the second annual ACM symposium on Theory of computing, p.184-197, May 04-06, 1970, Northampton, Massachusetts, United States [doi>10.1145/800161.805164]
• 20: THATCHER, J.W. Characterizing derivation trees of context-free grammars through a generalization of finite automata theory. J. Comput. Syst. Sci. 1 (1967), 317-322.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.2 Modes of Computation
          Subjects: Alternation and nondeterminism

General Terms:
Algorithms, Performance, Theory, Verification