Unique normal forms for lambda calculus with surjective pairing
type: Item
instance of: scholarly article
title: Unique normal forms for lambda calculus with surjective pairing
zbMATH Open document ID: 0667.03008
DOI: 10.1016/0890-5401(89)90014-X
author: R. C. de Vrijer
author: Jan Willem Klop
published in: Information and Computation
publication date: 1989-01-01T00:00:00Z
review text: Some extensions of lambda calculus with surjective pairing constants and axioms are investigated and some new results concerning consistency and conservativity of the respective extension and the normal form property and unique normal form property are obtained. Several remaining problems to be solved are stated.
Mathematics Subject Classification ID: 03B40
zbMATH DE Number: 4091463
zbMATH Keywords: confluence
zbMATH Keywords: term rewriting systems
zbMATH Keywords: extensions of lambda calculus
zbMATH Keywords: surjective pairing
zbMATH Keywords: normal form
reviewed by: Pavel Materna
MaRDI profile type: Publication
cites work: Pairing Without Conventional Restraints
cites work: The lambda calculus. Its syntax and semantics. Rev. ed.
cites work: \(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
cites work: An extension of Klop's counterexample to the Church-Rosser property to \(\lambda\)-calculus with other ordered pair combinators
cites work: The categorical abstract machine
cites work: Q3785893
cites work: Q3727946
cites work: Q3918095
cites work: The Connection between Equivalence of Proofs and Cartesian Closed Categories
cites work: The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
cites work: Q4083398
cites work: Q4063416
cites work: On the Church-Rosser property for the direct sum of term rewriting systems
full work available at URL: 0890-5401(89)90014-x
OpenAlex ID: W2006607295
description: scientific article; zbMATH DE number 4091463