Barry K. Rosen
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.
- 1 BLUM, E.K. Towards a theory of semantics and compilers for programming languages. J. Comput. Syst. Sci. 8 (1969), 248-275.Google Scholar
- 2 BRAINERI), W.S. Tree generating regular systems. Inform. and Contr. t4 (1969), 217-231.Google Scholar
- 3 CHURCH, A., ANn ROSSEa, J B Some properties of conversion Trans. Amer Math Soc. 89 (1936), 472-482.Google Scholar
- 4 CURRY, H. B., AND FEYS, R. Combinatory Logic. North-Holland Pub. Co., Amsterdam, 1958.Google Scholar
- 5 HINDLEY, R. The Church-Rosser property and a result in combinatory logic. Ph.D. Th., U. of Newcastle-upon-Tyne, England, 1964.Google Scholar
- 6 tIINDLEY, R. An abstract form of the Church-Rosser theorem, Part I. J. Symbolic Logic 84 (1969), 545-560.Google Scholar
- 7 KARP, R. M., AND MILLER, R.E. Parallel program schemata. J. Comput. Syst. Sci. 8 (1969), 147-195.Google Scholar
- 8 KLEENE, S.C. Introduction to Metamathematzcs. Van Nostrand, New York, 1952.Google Scholar
- 9 I~/{_~RTIN-LoF, P. A theory of types (unpublished manuscript, 1971).Google Scholar
- 10 McCARTHY, J. Recursive functions of symbolic expressions and their computation by machine. Comm. A CM 8, 4 (Apr. 1960), 184-195. Google Scholar
- 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.Google Scholar
- 12 MINSKY, M. Form and content in computer science. J. ACM 17, 2 (Apr. 1970), 197-215. Google Scholar
- 13 MITSCHKE, G. Eine algebraische Behandlung yon ;~-K-Kalkul und Kombinatorischer Logik. Ph.D. Th., Rheinischen Friedrich-Wilhelms U., Bonn, Germany, 1970.Google Scholar
- 14 MoRRIs, J. H. JR Lambda-calculus models of programming languages. Proj. MAC, Rep. MAC-TR-57, MIT, Cambridge, Mass., 1968.Google Scholar
- 15 NAuR, P. (Ed.) Revised report on the algorithmic language ALGOL 60 Comm. ACM 6, 1 (Jan. 1963), 1-17. Google Scholar
- 16 ROSEN, B.K. Subtree replacement systems. Tech Rep. 2-71, Ctr. for Res. in Computing Technology, Harvard U., Cambridge, Mass., 1971.Google Scholar
- 17 SANCHIS, L.E. Functionals defined by recursion. Notre Dame J. Formal Logic 8 (1967), 161-174.Google Scholar
- 18 SCHROER, D.E. The Church-Rosser theorem. Ph.D. Th., Cornell U., ithaca, N.Y., 1965.Google Scholar
- 19 STRONG, H. R. JR. Translating recurslon equations into flowcharts Second Annual ACM Syrup. on Theory of Computing, Northampton, Mass , 1970, 184-197. Google Scholar
- 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.Google Scholar
Index Terms
- Tree-Manipulating Systems and Church-Rosser Theorems
Recommendations
A mechanical proof of the Church-Rosser theorem
The Church-Rosser theorem is a celebrated metamathematical result on the lambda calculus. We describe a formalization and proof of the Church-Rosser theorem that was carried out with the Boyer-Moore theorem prover. The proof presented in this paper is ...
More Church–Rosser Proofs
The proofs of the Church–Rosser theorems for β, η, and β ∪ η reduction in untyped λ-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For β-reduction, both the standard proof and ...
A Simplified Proof of the Church---Rosser Theorem
Takahashi translation * is a translation which means reducing all of the redexes in a -term simultaneously. In [ 4 ] and [ 5 ], Takahashi gave a simple proof of the Church---Rosser confluence theorem by using the notion of parallel reduction and ...
Comments