[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #5

Originator: Albert Meyer, Roel C. de Vrijer
Date: April 1991

Summary: Does surjective pairing conservatively extend λβη-conversion?

Do the surjective pairing axioms

conservatively extend λβη-conversion on pure untyped lambda terms? More generally, is surjective pairing always conservative, or do there exist lambda theories, or extensions of Combinatory Logic for that matter, for which conservative extension by surjective pairing fails? (Surjective pairing is conservative over the pure λβ-calculus; see [dV89]). Of course, there are lots of other λβ, indeed λβη, theories where conservative extension holds, simply because the theory consists of the valid equations in some λ model in which surjective pairing functions exist, e.g., D_∞.

Comment sent by Kristian Støvring

Date: Tue, 22 Nov 2005 00:18:13 +0100

The problem has been solved with a positive answer [Stø05, Stø06]. The generalization to arbitrary lambda theories remains open.

References

[dV89]

Roel C. de Vrijer. Extending the lambda calculus with surjective pairing is conservative. In Fourth Symposium on Logic in Computer Science, pages 204–215. IEEE, 1989.

[Stø05]

Kristian Støvring. Extending the extensional lambda calculus with surjective pairing is conservative. Research Report BRICS RS-05-35, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2005.

[Stø06]

Kristian Støvring. Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, 2(2:1):1–14, 2006.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]