• DocumentCode
    2597389
  • Title

    Extending the lambda calculus with surjective pairing is conservative

  • Author

    De Vrijer, Roel

  • Author_Institution
    Dept. of Math. & Comput. Sci., Free Univ., Amsterdam, Netherlands
  • fYear
    1989
  • fDate
    5-8 Jun 1989
  • Firstpage
    204
  • Lastpage
    215
  • 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, π(π0X )(π1X)=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
  • Keywords
    formal languages; formal logic; axioms; conservative extension; equational theory; lambda calculus; reduction system; surjective pairing; syntactic consistency proof; Calculus; Computer science; Equations; Functional programming; Ink; Mathematics; Roads; Writing;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1989. LICS '89, Proceedings., Fourth Annual Symposium on
  • Conference_Location
    Pacific Grove, CA
  • Print_ISBN
    0-8186-1954-6
  • Type

    conf

  • DOI
    10.1109/LICS.1989.39175
  • Filename
    39175
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2597389