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

Authors:**De Vrijer, R.**

### 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 = {De Vrijer, R.}, title = {Extending the lambda calculus with surjective pairing is conservative }, booktitle = {Proceedings of the Fourth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1989}, year = 1989, editor = {Rohit Parikh}, month = {June}, pages = {204--215}, location = {Pacific Grove, CA, USA}, publisher = {IEEE Computer Society Press} }