\section{Elimination of $\tensor$}

We now show how to eliminate the $\tensor$ operator preserving 
provability and denial.  We generalize the approach in 
\cite{MP90,Bar90}, where the operation was defined as follows.
For $m1: P_{1}\If G_{1}$ and  $m2: P_{2}\If G_{2}$
\beq
m1 \otimes m2 & = & \Pi \q(P_{1}\If G_1\And G_2)\mid \q = mgu(P_{1},P_{2}) 
\eneq
This definition is not adequate to our setting
\bit
\item
Strict unification and more in general \ho   unification is not unary
\item
We will have to take into account parameter (dis)equations, as well as 
closed (dis)equations stemming from left-linearization
\enit

We thus choose to compile our source into an intermediate language 
which makes unification problems explicit as simple equational problems 
in the style of the unification logic introduced in \cite{Pfenning91}.  
In a further system we will show how to perform constraint 
simplification used in \emph{Elf} and \emph{Twelf} \cite{Pfenning90}.

\newcommand{\eprv}{\stackrel{\prv}{\sim}}
\newcommand{\enprv}{\stackrel{\nprv}{\sim}}

We introduce a notion of \emph{operational equivalence} \wrt 
provability and denial: note that equivalence \wrt denial requires some 
sophistication in the notion of `allowed' goal whenever embedded 
implications are introduced. This is  essentially due to the non-admissibility of 
cut in the negative system, mentioned in Section \ref{lamrelated}.

\begin{Definition}[Operational Equivalence]\mbox{}
\label{def:opeq}
\bit
\item
We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent \wrt 
provability}, denoted $\cP_{1}\eprv \cP_{2}$, iff, for any goal $G$ we 
have $\ga\prv_{\cP_{1}} G$ iff $\ga\prv_{\cP_{1}} G$.
\item
We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent \wrt 
denial}, denoted $\cP_{1}\enprv \cP_{2}$, iff, for any goal $G$ we have 
$\ga\nprv_{\cP_{1}} G$ iff $\ga\nprv_{\cP_{1}} G$.
\item
We say that $\cP_{1}$ and $\cP_{2}$ are \emph{operationally equivalent}, 
denoted $\cP_{1}\sim \cP_{2}$, iff $\cP_{1}\eprv \cP_{2}$ and 
$\cP_{1}\nprv \cP_{2}$.  
\enit
\end{Definition}

% \begin{Lemma}
% \label{le:exchng}
% $D_{1}\tensor D_{2}\sim D_{2}\tensor D_{1}$.
% \end{Lemma}
% \begin{proof}
% Immediate.
% \end{proof}


% It is convenient to bring the source program in a sort of conjucntive 
% normal form , so that

We adapt the \emph{residuation} technique used in \cite{Pfenning?} to 
compile immediate implication into resolution.  We define in Figure
\ref{fig:otimes} the judgment 
$D_{1}\otimes D_{2} \setminus D$ by induction on (normalized) $D_{1}$, 
with the intended meaning of `$D_{1}\otimes D_{2}$ compiles to $D$. We
implicitely add the rules symmetric to $\setminus\And, \setminus\top$
and  $\setminus\Pi$.

\begin{figure}
\label{fig: otimes}
\[
\begin{array}{c}
\ianc{}{\top\otimes D \setminus D}{\setminus\top}
\qquad
\ianc{}{\perp\otimes D \setminus \perp}{\setminus\perp}
\vsk
\ianc{}{(q\ \vN_{1}\If G_{1})\otimes  (q\ \vN_{2}\If G_{2}) \setminus
(q\ \vN_{1}\If \vN_{1}\eqd \vN_2 \And G_{1}\And G_2)}{\setminus-Atm}\vsk
\ianc{ D_{1}\otimes D_{2}\setminus D}{\PIXA D_{1}\otimes 
D_{2}\setminus \PIXA D}{\setminus\Pi}\vsk
\ianc{D_{1}\otimes D_{2}\setminus D\quad D'_{1}\otimes D_{2}\setminus D'}
{(D_{1}\And D'_{1})\otimes D_{2}\setminus D\And D'}{\setminus\And}
\end{array}
\]
\caption{Judgment $D_{1}\otimes D_{2}\setminus D$}
\end{figure}


\begin{Lemma}\mbox{}
\label{le:te-ti}
\ben
\item
$ D_{1}\otimes D_{2}\setminus D$ and $D\imm Q$ iff $D_{1}\tensor D_{2} \imm Q$.
\item
$ D_{1}\otimes D_{2}\setminus D$ and $D\nimm Q$ iff $D_{1}\tensor 
D_{2} \nimm Q$.  
\enen
\end{Lemma}
\begin{proof}
By induction on $D_{1}$. We show only some significant cases in the
left-to-right direction, the converse being analogous:
\ben
\item
\bit
\item
Case:
$$\ianc{}{\top\otimes D \setminus \top}{\setminus\top}$$
and $\ga\sp\top\imm Q$ entails falsehood which implies $\ga\sp\top\imm Q$ and 
$\ga\sp D\imm Q$; thus $\ga\sp\top\otimes D\imm Q$.
\item
Case:
$$\ianc{}{q\ \vN_{1}\If G_{1}\otimes  q\ \vN_{2}\If G_{2} \setminus
q\ \vN_{1}\If \vN_{1}\eqd \vN_{2 \And G_{1}\And g_{2}}}{\setminus{\rm 
atom}}$$
By inversion $\ga\sp q\ \vN_{1}\imm Q$ and $\eqd \vN_{1}\vN_{2}$ and 
$\ga\sp G_{1}$ and $\ga\sp G_{2}$ then  $\ga\sp q\ \vN_{1}\imm Q$ and 
$\ga\sp q\ \vN_{2}\imm Q$ then  $\ga\sp q\ \vN_{1}If G_{1}\imm Q$ and 
$\ga\sp q\ \vN_{2}If G_{12}\imm Q$ then  $\ga\sp q\ \vN_{1}If 
G_{1}\tensor q\ \vN_{1}If G_{1}\imm Q$.
\item
Case:
$$\ianc{[t/x] D_{1}\otimes D_{2}\setminus [t/x]D}{\PIXA D_{1}\otimes 
D_{2}\setminus \PIXA  D}{\setminus\Pi}$$
By inversion $[t/x] D_{1}\otimes D_{2}\setminus [t/x]D$ and $\ga\sp [t/x]D\imm 
Q$ which is equivalent by IH to $\ga\sp [t/x]D\imm 
Q$ and $\ga\sp D\imm Q$ then  $\ga\sp \PIXA D_{1}\tensor  D\nimm Q$.
% \item
% Case:
% $$\ianc{D\otimes Q\setminus D'}{Q\otimes D\setminus D'}
% {\setminus{\rm exchng}$$
% it follows by a direct appleat to the inductiive hypothesis using 
% Lemma \ref{le:exchng}.
\enit
% \item
% \bit
% \item
% Case:
% $$\ianc{}{\top\otimes D \setminus \top}{\setminus\top}$$
% and $\ga\sp\top\imm Q$ iff falsehood iff $\gs\sp\top\imm Q$ and 
% $\ga\sp\D\imm Q$ iff $\ga\sp\top\otimes D\imm Q$.
% \item
% Case:
% $$\ianc{}{q\ \vN_{1}\If G_{1}\otimes  q\ \vN_{2}\If G_{2} \setminus
% q\ \cV_{1}\If \vN_{1}\eqd \vN_{2 \And G_{1}\And g_{2}}}{\setminus{\rm 
% atom}}$$
% By inversion $\ga\sp q\ \vN_{1}\imm Q$ and $\eqd \vN_{1}\vN_{2}$ and 
% $\ga\sp G_{1}$ and $\ga\sp G_{2}$ iff $\ga\sp q\ \vN_{1}\imm Q$ and 
% $\ga\sp q\ \vN_{2}\imm Q$ iff $\ga\sp q\ \vN_{1}If G_{1}\imm Q$ and 
% $\ga\sp q\ \vN_{2}If G_{12}\imm Q$ iff $\ga\sp q\ \vN_{1}If 
% G_{1}\tensor $q\ \vN_{1}If G_{1}\imm Q$.
% \item
% Case:
% $$\ianc{[t/x] D_{1}\otimes D_{2}\[t\x]D}{\Pi x:A.D_{1}\otimes 
% D_{2}\setminus \Pi x:A. D}{\setminus\Pi}$$
% By inversion $[t/x] D_{1}\otimes D_{2}\[t\x]D$ and $\ga\sp [t/x]D\imm 
% Q$ which is equivalent by IH to $\ga\sp [t/x]D\imm 
% Q$ and $\ga\sp D\imm Q$ iff $\ga\sp \Pi x:A.D_{1}\tensor  D\nimm Q$.
% \enit
\enen
\end{proof}

\begin{Corollary}
\label{co:te-ti}
$D_{1}\tensor D_{2} \sim D_{1}\otimes D_{2}$.
\end{Corollary}
\end{document}
\input{cloex}