## Paper: Extending the lambda calculus with surjective pairing is conservative (at LICS 1989)

**Roel C. de Vrijer**

### Abstract

Consideration is given to the equational theory λπ of lambda calculus extended with constants π, π_{0}, π_{1} and axioms for subjective pairing: π_{0}(πXY)=X, π_{1}(πXY)=Y, π(π_{0}X )(π_{1}X)=X. The reduction system that one obtains by reading the equations are reductions (from left to right) is not Church-Rosser.
Despite this failure, the author obtains a syntactic consistency proof of λπ and shows that it is a conservative extension
of the pure λ calculus

### BibTeX

@InProceedings{deVrijer-Extendingthelambdac, author = {Roel C. de Vrijer}, title = {Extending the lambda calculus with surjective pairing is conservative }, booktitle = {Proceedings of the Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 1989)}, year = {1989}, month = {June}, pages = {204--215}, location = {Pacific Grove, CA, USA}, publisher = {IEEE Computer Society Press} }