Unique normal forms for lambda calculus with surjective pairing

DOI10.1016/0890-5401(89)90014-XzbMath0667.03008OpenAlexW2006607295MaRDI QIDQ1117204

R. C. de Vrijer, Jan Willem Klop

Publication date: 1989

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0890-5401(89)90014-x

zbMATH Keywords

normal formconfluenceterm rewriting systemssurjective pairingextensions of lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

Extended term rewriting systems, On confluence for weakly normalizing systems, Open problems in rewriting, Some lambda calculi with categorical sums and products, Unique normal forms for nonlinear term rewriting systems: Root overlaps, Unique normal forms for lambda calculus with surjective pairing, Call-by-name extensionality and confluence, Alpha conversion, conditions on variables and categorical logic, Conditional linearization, Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem, On interreduction of semi-complete term rewriting systems, Unnamed Item, Combinatory reduction systems: Introduction and survey

Cites Work

• The lambda calculus. Its syntax and semantics. Rev. ed.
• An extension of Klop's counterexample to the Church-Rosser property to \(\lambda\)-calculus with other ordered pair combinators
• The categorical abstract machine
• Unique normal forms for lambda calculus with surjective pairing
• The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
• \(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
• Pairing Without Conventional Restraints
• The Connection between Equivalence of Proofs and Cartesian Closed Categories
• On the Church-Rosser property for the direct sum of term rewriting systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item