Unique normal forms for lambda calculus with surjective pairing (Q1117204): Difference between revisions

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.

0 references

zbMATH Keywords

confluence

0 references

term rewriting systems

0 references

extensions of lambda calculus

0 references

surjective pairing

0 references

normal form

0 references

reviewed by

Pavel Materna

0 references

MaRDI profile type

MaRDI publication profile

0 references

cites work

Pairing Without Conventional Restraints

0 references

The lambda calculus. Its syntax and semantics. Rev. ed.

0 references

\(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975

0 references

An extension of Klop's counterexample to the Church-Rosser property to \(\lambda\)-calculus with other ordered pair combinators

0 references

The categorical abstract machine

0 references

Q3785893

0 references

Q3727946

0 references

Q3918095

0 references

The Connection between Equivalence of Proofs and Cartesian Closed Categories

0 references

The Church-Rosser theorem for the typed lambda-calculus with pairing pairing

0 references

Q4083398

0 references

Q4063416

0 references

On the Church-Rosser property for the direct sum of term rewriting systems

0 references

Unique normal forms for lambda calculus with surjective pairing

0 references

full work available at URL

https://doi.org/10.1016/0890-5401(89)90014-x

0 references

Identifiers

zbMATH Open document ID

0667.03008

0 references

DOI

10.1016/0890-5401(89)90014-X

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:1117204

@@ Property / author @@
-Jan Willem Klop
@@ Property / author: Jan Willem Klop / rank @@
-Normal rank
@@ Property / reviewed by @@
-Pavel Materna
@@ Property / reviewed by: Pavel Materna / rank @@
-Normal rank
@@ Property / author @@
+Jan Willem Klop
@@ Property / author: Jan Willem Klop / rank @@
+Normal rank
@@ Property / reviewed by @@
+Pavel Materna
@@ Property / reviewed by: Pavel Materna / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / cites work @@
+Pairing Without Conventional Restraints
@@ Property / cites work: Pairing Without Conventional Restraints / rank @@
+Normal rank
@@ Property / cites work @@
+The lambda calculus. Its syntax and semantics. Rev. ed.
+Normal rank
@@ Property / cites work @@
+\(\lambda\)-calculus and computer science theory. Proceedings of the symposium held in Rome, March 25-27, 1975
+Normal rank
@@ Property / cites work @@
+An extension of Klop's counterexample to the Church-Rosser property to \(\lambda\)-calculus with other ordered pair combinators
+Normal rank
@@ Property / cites work @@
+The categorical abstract machine
@@ Property / cites work: The categorical abstract machine / rank @@
+Normal rank
@@ Property / cites work @@
+Q3785893
@@ Property / cites work: Q3785893 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3727946
@@ Property / cites work: Q3727946 / rank @@
+Normal rank
@@ Property / cites work @@
+Q3918095
@@ Property / cites work: Q3918095 / rank @@
+Normal rank
@@ Property / cites work @@
+The Connection between Equivalence of Proofs and Cartesian Closed Categories
+Normal rank
@@ Property / cites work @@
+The Church-Rosser theorem for the typed lambda-calculus with pairing pairing
+Normal rank
@@ Property / cites work @@
+Q4083398
@@ Property / cites work: Q4083398 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4063416
@@ Property / cites work: Q4063416 / rank @@
+Normal rank
@@ Property / cites work @@
+On the Church-Rosser property for the direct sum of term rewriting systems
+Normal rank
@@ Property / cites work @@
+Unique normal forms for lambda calculus with surjective pairing
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/0890-5401(89)90014-x
+Normal rank
@@ Property / OpenAlex ID @@
+W2006607295
@@ Property / OpenAlex ID: W2006607295 / rank @@
+Normal rank