\documentclass{rtaloop}
\rtalabel{explicit-substitution-all}


\begin{document}
\begin{problem}{Delia Kesner}{}{January 1998}

\begin{abstract}
Is there
a calculus  of  explicit  substitution that   is confluent on   open terms,
simulates one-step beta-reduction and preserves beta-strong normalization?
\end{abstract}

There are confluent calculi of explicit substitutions but these do not
preserve termination (strong normalization)
\cite{CurienHardinLevy92,Mellies95}, and there are calculi that are not
confluent on open terms but which do preserve termination \cite{LescanneR94}.
C\'esar Mu\~noz presented in~\cite{Munioz:lics96} a calculus enjoying both
properties (answering \rtaref{explicit-substitution}), however, the
calculus is not able to simulate one-step of beta-reduction: if $a$
beta-reduces to $b$ in the lambda-calculus then $a$ does not necessarily
reduce to $b$ in the calculus of Mu\~{n}oz. Is there a calculus of explicit
substitution that is confluent on open terms, simulates one-step
beta-reduction and preserves beta-strong normalization?


\begin{submitted}{Jean Goubault-Larrecq}{Mon Nov 27 16:37:43 MET 2000}

This problem was solved positively in \cite{JGL:SKInT:conj}. The calculus
SKInT, introduced in \cite{GGL:SKIn}, is confluent on open terms and simulates
one-step beta-reduction (although in a slightly contorted way, see
\cite{GGL:SKIn}; the obvious translation only simulates a bit more that
one-step call-by-value beta-reduction). The paper \cite{JGL:SKInT:conj}
characterizes strongly normalizing, weakly normalizing and solvable terms
through intersection types, and preservation of strong normalization follows.
SKInT is also standardizing, has a terminating subcalculus of substitutions
$\Sigma T$, but is based on an infinite signature and finitely many rule
schemes parameterized by integers. Can we lift the latter restriction?

\end{submitted}

\end{problem}

\end{document}