[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:

Ix→x
Kxy→x
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]