Unique normal forms for lambda calculus with surjective pairing

We consider the equational theory λπ of λ-calculus extended with constants π, π 0, π 1 and axioms for surjective pairing: π 0(πXY) = X, π 1(πXY) = Y, π(π 0 X)(π 1 X) = X. Two reduction systems yielding the equality of λπ are introduced; the first is not confluent and, for the second, confluence is an open problem. It is shown, however, that in both systems each term possessing a normal form has a unique normal form. Some additional properties and problems in the syntactical analysis of λπ and the corresponding reduction systems are discussed.

Authors

• J.W. Klop
• R.C. de Vrijer

Keywords

No keywords are indexed for this paper.