[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 
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_{∞}.
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.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next]  [Postscript] [PDF] [BibTeX Source] [LaTeX Source] 