\documentclass{rtaloop}
\rtalabel{combinations}


\begin{document}
\begin{problem}{Jean-Pierre Jouannaud}{}{December 1991}

\begin{abstract}
Investigate confluence and termination of combinations of typed lambda-calculi
with term rewriting systems.
\end{abstract}

Combinations of typed $\lambda$-calculi with term-rewriting systems have been
studied
extensively in the past few years
\cite{barbanera90ijfcs}\cite{BG89:icalp}\cite{DO90:tcs}\cite{D91:rta}.
The strongest termination result
allows first-order rules as well as higher-order rules defined by a
generalization of primitive recursion.
Suppose all rules for
functional constant $F$ follow the schema:
\[
F(\bar{l}[\bar{X}],\bar{Y})\rightarrow
v[F(\bar{r}_1[\bar{X}],\bar{Y})
,...,F(\bar{r}_m[\bar{X}],\bar{Y}),\bar{Y})]
\]
where the (not necessarily disjoint) variables in $\bar{X}$ and $\bar{Y}$ are
of arbitrary order,
each of $\bar{l},\bar{r}_1,...,\bar{r}_m$ is in 
${\cal T}({\cal F,}\{\bar{X}\})$,
$v[\bar{z},\bar{Y}]$ is in ${\cal T}({\cal F,}\{\bar{Y},\bar{z}\})$,
for new variables $\bar{z}$ of appropriate types, and
$\bar{r}_1,\ldots,\bar{r}_m$ are each less than $\bar{l}$
in the multiset extension of the strict subterm ordering.
If ${\cal T(F,X)}$
is the term-algebra which includes only {\em previously\/} defined functional
constants---forbidding the use of mutually recursive functional
constants---termination is ensured \cite{JO91:lics}.
Does termination also hold when there are mutually recursive definitions?
Does this also hold when the subterm assumption is unfulfilled?
(In \cite{JO91:lics} an alternative schema is proposed, with
the subterm assumption weakened at the price of having only first-order
variables in $\bar{X}$.)
Questions of confluence of combinations of typed $\lambda$-calculi and
higher-order systems also merit investigation.
These results have been extended to combinations with more expressive type
systems \cite{barbanera93icalp}\cite{barbanera93tlca}.


\begin{remark}
An extension to the Calculus of Constructions has been reported in
\cite{FernandezBarbaneraGeuvers:lics94}. One can also allow the use of
lexicographic and other ``statuses'' for the higher-order constants when
comparing the subterms of $F$ in left and right hand sides [Jouannaud and
Okada, unpublished]. Finally, this can also be done when the rewrite rules
follow from the induction schema in the initial algebra of the constructors
\cite{BWerner}.

Important improvements of the previous works have been achieved in
\cite{blanqui03mscs} and \cite{walukiewicz03jfp}.
\end{remark}

\end{problem}
\end{document}