\documentclass{rtaloop}
\rtalabel{surjective}


\begin{document}
  \begin{problem}{Albert Meyer, Roel C. de Vrijer}{}{April 1991}
    
    \begin{abstract}
      Does surjective pairing conservatively extend
      $\lambda\beta\eta$-conversion?
    \end{abstract}

    Do the surjective pairing axioms
    \begin{eqnarray*}
      D_{1}(Dxy) & = & x\\
      D_{2}(Dxy) & = &  y\\
      D(D_{1}x)(D_{2}x) & = & x
    \end{eqnarray*}
    conservatively extend $\lambda\beta\eta$-conversion on pure untyped lambda
    terms? More generally, is surjective pairing {\em 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 $\lambda\beta$-calculus;
    see \cite{V89:lics}). Of course, there are lots of other $\lambda\beta$,
    indeed $\lambda\beta\eta$, theories where conservative extension holds,
    simply because the theory consists of the valid equations in some
    $\lambda$ model in which surjective pairing functions exist, e.g.,
    $D_\infty$.

    \begin{submitted}{Kristian St{\o}vring}{Tue, 22 Nov 2005 00:18:13 +0100}
      The problem has been solved with a positive
      answer~\cite{stoevring:rs-05-35,Stoevring:LMCS-2006}. The generalization
      to arbitrary lambda theories remains open.
    \end{submitted}
  \end{problem}
\end{document}