Extending the lambda calculus with surjective pairing is conservative
Roel de Vrijer · 2003
Consideration is given to the equational theory lambda pi of lambda calculus extended with constants pi , pi /sub 0/, pi /sub 1/ and axioms for subjective pairing: pi /sub 0/( pi XY)=X, pi /sub 1/( pi XY)=Y, pi ( pi /sub 0/X)( pi /sub 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 lambda pi and shows that it is a conservative extension of the pure lambda calculus.>