×

Church-Rosser theorem for a rewriting system on categorical combinators. (English) Zbl 0672.03006

The author addresses the problem of studying the Church-Rosser problem for a rewriting system based on categorical combinators. The results presented are interesting because those combinators are used in functional programming languages and their abstract machines. It is shown that CCL\(\beta\) is non-confluent, but some subsystems are confluent.
Reviewer: A.Pettorossi

MSC:

03B40 Combinatory logic and lambda calculus
68N01 General topics in the theory of software
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Curien, P.-L., Categorical Combinators, Sequential Algorithms and Functional Programming (1986), Pitmann: Pitmann London · Zbl 0643.68004
[2] Curien, P.-L., Categorical combinators, Inform. and Control, 69, 188-254 (1986) · Zbl 0607.03005
[3] Curien, P.-L., The strong calculus of closures, or λσ-calculus (1989), Preprint
[4] Hardin, T.; Laville, A., Proof of termination of the rewriting system SUBST on CCL, Theoret. Comput. Sci., 46, 305-312 (1986) · Zbl 0618.68031
[5] Hardin, T., Résultats de confluence pour les règles fortes de la Logique Combinatoire Catégorique et liens avec les Lamba-calculus, Thèse de Doctorat, 7 (1987), Université de Paris
[6] Hardin, T., Confluence results for the pure strong CCL lambda calculi as subsystems of CCL, Theoret. Comput. Sci., 65, 291-342 (1989), (this issue). · Zbl 0707.03012
[7] Yokouchi, H., Relationship between lambda calculus and rewriting systems for categorical combinators (1988), Preprint
[8] Yokouchi, H.; Hikita, T., A rewriting system on categorical combinators with multiple arguments, (RIMS Lecture Note 655 (1988), Kyoto University), 186-208
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.