
\section{HO-q}

How do we lift those results to \ho logic? One possibility not 
pursued here is to reduce  \ho problems to FO-problems modulo the 
$\eta\beta$ equality theory, as in \cite{Dow94}, possibly using what 
Kirchner calls Syntactic theories.

The other it to formulate axioms for \ho finite tress ($E_{\Sigma 
T\omega}$). Given the undecidability results, we cannot expect 
something like
\ref{EFT:complete}. What we can do is start with patterns.
Assume a suitable notion of substitution.
\begin{Def} [patterns]
\end{Def}
\begin{Notation} \ho terms are assumed to be in long $\beta\eta$ 
normal form and normalization is performed after every rewrite 
step. For the sake of readability, variables stand for their normal 
form, for example $Z : i \Imp o$ stands for \mbox{$\l x : i . Z(x)$}.
\end{Notation}

We tacitly assume for the moment that (dis)equations are well-
typed. On the other hand we parametrize Dca to kind declaration, \ie
  for each context containing say $\tau : type$ we have a Dca($\tau$) 

\begin{Def}
[Freeness theory for patterns]
\begin{itemize}
\item Equality axioms for $\l$-terms
\[
\begin{array}{ll}
(\beta): & (\l x.M)N= [N/x]M\\
(\eta): & \l x Mx = M \\
(): & M=N \Imp \l x.M=\l x .N\\
(): & N =N' \Imp MN =MN'\\
(): & M=M' \Imp MN=M'N  \\
(Ref): &  M=M\\
(Sym): &  M=N \Imp N=M\\
(Trs): & M=N \And N =P \Imp M=P\\

\end{array}
\]
\item Finite trees axioms
\[\begin{array}{lll}
(Dec) : & \l\xk  .a(\sn) \neq  \l\xk  .a(\tn) \Imp \ol{\l\xk .s_n = \l\xk 
.t_n} & a \in \Sigma \cup \{\xk\} \\
(Clh) : & \l\xk  .a(\sn) \neq  \l\xk .a(\tm) & a \not \equiv b, a, b \in 
\Sigma \cup \{\xk\} \\
(Oc1) : & \l\xk  .F(\ym) \neq \l\xk .a(\sn) & F \in FV(\sn) \\
(Oc2) : &\l\xk  .F(\ym) \neq \l\xk .a(\sn) & a \in FV(\xk) - FV(\ym) 
\\
(Dca(\tau)): &  \forall X (\bigvee\limits_{f^{\ol{\tau} \Imp \tau} \in 
\Sigma}
\exists \overline{Y} (X=f(\overline{Y})))\end{array}\]
\end{itemize}
\end{Def}

Oc1 is called a {\em cycle} and properly corresponds to Ock; Oc2 is 
instead called a {\em bound variable capture} or more simply a {\em 
capture} and it is peculiar to the \ho order nature of the term 
algebra: it happens in the case $a$ would get bound in the 
substitution.

\begin{Examplen}
Given $\Sigma = \{ all :  (i \rightarrow o) \rightarrow o, imp :  o 
\rightarrow o \rightarrow o,
and :  o \rightarrow o \rightarrow o \}$ for kinds $i,o : type$, 
Dca($o$) is 
\[
\forall X:o \ (\exists C : i \Imp o . X = all \ C \Or . \exists P_1,P_2 : o 
. x = imp \ P_1 \ P_2 \Or x = and \ P_1 \ P_2 )
\]
\end{Examplen}

Note that to allow the generality present in first-order 
disunification we should provide an algebraic model for \ho  terms: 
we limit only to the \ho Herbrand universe.


\begin{Lemma} [Clark lemma for \ho patterns]
Let $s$ and $t$ be two patterns:
\begin{enumerate}
\item if they are unifiable, $E_{\Sigma T\omega} \prv \exists (s=t)$
\item if not $E_{\Sigma T\omega}\prv \forall(s \not = t)$
\end{enumerate}
\end{Lemma}

\begin{Theorem}
$E_{\Sigma T\omega}$ is decidable
\end{Theorem}
  %\include{thref}
