[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]


Problem #17

Originator: Roel C. de Vrijer
Date: April 1991

Summary: Is a certain conditional rewrite system, which is a linearization of Combinatory Logic extended with surjective pairing, confluent?

Is the following semi-equational conditional term rewriting system (a linearization of Combinatory Logic extended with surjective pairing) confluent:

Ixx
Kxyx
Sxyz(xz)(yz)
D1(Dxy)x
        D2(Dxy)y
x ↔* y ⇒      D(D1x)(D2y)x
x ↔* y ⇒    D(D1x)(D2y)y 

If yes, does an effective normal form strategy exist for it? See [Kd89][dV89].

References

[dV89]
Roel C. de Vrijer. Extending the lambda calculus with surjective pairing is conservative. In Fourth Symposium on Logic in Computer Science, pages 204–215. IEEE, 1989.
[Kd89]
Jan Willem Klop and Roel C. de Vrijer. Unique normal forms for lambda calculus with surjective pairing. Information and Computation, 80:97–113, 1989.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]