\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{Definition} [patterns]
\end{Definition}

\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{Definition}
[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{Definition}

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}

Again, both results follow from sou ndness and completeness of \ho 
disunification, so we do not engage here in a direct proof.



\subsubsection{About Cardinalities}
It seems that  a fair part of the disunification game turns around
the question of cardinality in signatures: in a 
typed context, this comes in two flavors:
\bit
\item finite (\wrt constants) vs.\ infinite signatures
\item finitary vs.\ infinitary sorts (types)
\enit

We began to approach  the first aspect in the beginning of  Chapter 
\ref{ch: fo-dis} and showed how it boils down  to the assumption of the 
$DCA$, \ie to a difference in axiomatization. The 
second one is potentially more troublesome. Let us   recall the relevant 
definitions: a type is called 
\emph{finitary} iff the set of all its  closed normal forms is 
finite. As a matter of fact, this situation occurs pretty frequently 
in a programming set  and not necessarily, as Lugiez states erroneously in the
 footnote 25 at pp. ?? in the case of constantless calculi: think in 
 general to ``enumerated'' types as in the case 
 of a \fo\ 
signature specifying different kind of   finite graphs with a \ho\ 
predicate for transitive closure; or in LF to the (unary) type of \emph{normalized} 
natural deduction derivation of a given theorem, for a well-behaved theory. Note here 
that the uniqueness of normal forms stand only up to renaming, but this 
is taken care by \ho-abstract syntax. 

As a matter of fact,  the way in which 
many-sorted \fo\  disunification \cite{CL89}deals with 
the finitary case exhaustive search; this means introducing  
 special rules for, essentially eliminating an universal quantifiers 
 by turning it into a 
finite conjunction of cases.The notion of solved form has to 
restricted so that the unknowns in solved disequation cannot vary on 
finite types. For example, given a type $i=\{a,b\}$ the  problem 
$\forall y^{i}: y \nq a \And y \nq b$ is not solved, but legits 
explosion to be applied yielding falsehood as the $DCA$ dictates.

 With respect to simple types, Lugiez \cite{Lug95} assumes without further 
ado all types to 
be infinitary, relying to the kind of explosion we have delineate in the 
latter paragraph to treat the finitary case. It would thus appears 
that --implicitly-- two different  set of rules arise for the two cases. Now, 
it is well-known that, as far as dependent types are concerned. this
difference is undecidable, due to the presence of empty types, like
\[
\exists x: natded {\rm false}.true \Lmap_{*} \bot
\]
The challenge is thus to show that the finitary rules are 
\emph{admissible}: otherwise the all enterprise have to retreat 
into more safer bounds.

More in details the question is whether the universal finitary rule at 
\ho can be emulated by an iteration of UEXPL, \ie by  recursion on 
the $\l$-term. At \fo\ they are the same. UEXPL treats every case. in 
simple types HOUEXPL proposes only an initial binding and thus looks 
like it is likely it needed iteration.

State lemma.

In this case, for universal quantifiers, the infinitary rules would 
suffice giving a partial solution to the mentioned decidability 
problem 

To be completed