Unique normal forms for lambda calculus with surjective pairing

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

Jan Willem Klop, R. C. de Vrijer

Publication date: 1989

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

zbMATH Keywords

normal form; confluence; term rewriting systems; surjective pairing; extensions of lambda calculus

Mathematics Subject Classification ID

03B40: Combinatory logic and lambda calculus

Related Items

Unique normal form property of compatible term rewriting systems: A new proof of Chew's theorem, On interreduction of semi-complete term rewriting systems, Conditional linearization, Alpha conversion, conditions on variables and categorical logic, Unique normal forms for lambda calculus with surjective pairing, Combinatory reduction systems: Introduction and survey

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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