[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #15

Originator: Yoshihito Toyama
Date: April 1991

Summary: Is the extension of Combinatory Logic by Boolean constants confluent?

Consider the following extension of Combinatory Logic with constants T (true), F (false), C (conditional):

Is this (non-terminating) “semi-equational” (or “natural”, as such are called in [DO90]) conditional rewrite system confluent? Note that if we take the above system plus the rule x ↔^* y ⇒ Czxy → y, the resulting conditional rewrite system is confluent (cf. [Klo92][de 90]).

References

[de 90]

Roel C. de Vrijer. Unique normal forms for Combinatory Logic with parallel conditional, a case study in conditional rewriting. Technical report, Free University, Amsterdam, 1990.

[DO90]

Nachum Dershowitz and Mitsuhiro Okada. A rationale for conditional equational programming. Theoretical Computer Science, 75:111–138, 1990.

[Klo92]

Jan Willem Klop. Term rewriting systems. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 2, chapter 1, pages 1–117. Oxford University Press, Oxford, 1992.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]