Testing for the Church-Rosser Property

ABSTRACT

The central notion in a replacement system is one of a transformation on a set of objects. Starting with a given object, in one “move” it is possible to reach one of a set of objects. An object from which no move is possible is called irreducible. A replacement system is Church-Rosser if starting with any object a unique irreducible object is reached. A generalization of the above notion is a replacement system (S, ⇒, ≡), where S is a set of objects, ⇒ is a transformation, and ≡ is an equivalence relation on S. A replacement system is Church-Rosser if starting with objects equivalent under ≡, equivalent irreducible objects are reached. Necessary and sufficient conditions are determined that simplify the task of testing if a replacement system is Church-Rosser. Attention will be paid to showing that a replacement system (S, ⇒, ≡) is Church-Rosser using information about parts of the system, i.e. considering cases where ⇒ is ⇒1 ∪ ⇒2, or ≡ is (≡1 ∪ ≡2)*.

REFERENCES

• 1: Arm, A. V., SETh1, R., ANt) ULLMAt~, J. D. Code optimization and finite Church-Rosser theorems, in Design and Optimization of Compilers, R. Rustin, Ed., Prentice-Hall, Englewood Cliffs, N.J., 1972, pp. 89-105.
• 2: ALLEn, F.E. Program optimization. Annual Review in Automatic Programming, Vol. 5, Pergamon, New York, 1969, pp. 239-307.
• 3: Frances E. Allen, Control flow analysis, Proceedings of a symposium on Compiler optimization, p.1-19, July 27-28, 1970, Urbana-Champaign, Illinois
• 4: COBHAM, A., FRIDSttAL, F., AND NORTH, J.H. An application of linear programming to the minimization of Boolean functions. Proc. 2nd Annual Symp. on Switching Circuit Theory and Logical Design, AIEE Pub. $134, Sept. 1961, pp. 3-9.
• 5: John Cocke, Programming languages and their compilers: Preliminary notes, Courant Institute of Mathematical Sciences, New York University, 1969
• 6: CuR~Y, H. B., AND F~.~s, R. Combinatory Logic. North-Holland Pub. Co., Amsterdam, 1968, 89-90.
• 7: HECHT, M. S., AND ULLMAN, J. D. Flow graph reducibility. SIAM J. Computing 1, 2 (June 1972), 188-202.
• 8: KARP, R.M. Reducibility among combinatorial problems. In Complexity of Computer Computations, R. E. Miller and J. W. Thatcher, Eds., Plenum Press, New York, 1972, pp. 85-103.
• 9: 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., Amsterdam, 1963, pp. 33-70.
• 10: N~WMAN, M. H.A. On theories with a combinatorial definition of equivalence. Ann. Math ~, 2 (April 1942), 223-243.
• 11: J. Nievergelt, On the automatic simplification of computer programs, Communications of the ACM, v.8 n.6, p.366-370, June 1965 [doi>10.1145/364955.364963]
• 12: QUINg, W.V. The problem of simplifying truth functions. Amer. Math. Mon. 59 (Oct. 1952), 521-531.
• 13: ROSES, B.K. Subtree replacement systems. Tech. Rep. 2-71, Center for Res. in Computing Tech., Harvard U., Cambridge, Mass., 1971.
• 14: Barry K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, Journal of the ACM (JACM), v.20 n.1, p.160-187, Jan. 1973 [doi>10.1145/321738.321750]

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS

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

General Terms:
Theory, Verification