\section{The lattice of intensional terms}
\label{lattice}

Question: is Not a complement is some kind of lattice?
An alternative characterization can be given by looking at the lattice of (fo) terms as originally investigated by \cite{Rey70} 
and \cite{Plo70}. The subsumption ordering induces a poset that can be organized in a lattice by seeing glb as unification and lub as antiunification. A bottom element represents failed unifications, while (under quotient after $\alpha$-conversion) (the equivalence class of) variables are the top. 

Since the notion of complements in arbitrary lattice is well-defined, it would be nice to correlate the two characterization,
namely showing:
\beq
Not(t) = \{t_1, \ldots, t_n \} \Bimp \forall i. t_i^c = t
\eneq

Unfortunately this in not immediately achievable since the fo terms lattice is not nice: antiunification does not correspond to
set-theoretic union; complement not being unique, distributivity
and modularity are lost. Hence the complement operation has to
be split in and-c (pseudo-complement) and or-c, as in 
\cite{Rai58}

Every (open ) term standing for the set of its instances the former lattice is embeddable in the lattice
of sets of ground terms ordered under inclusion.

\begin{Def}
The Algebra $\la \|T\Sigma \|, \sqcup, \sqcap,Not, \sqsubseteq, \top,\bot \ra. s \sqless {\rm \ iff \ } \| s \| \subseteq \| t \|$. Clearly is is a partial order. Define equationally glb and lub.
\end{Def}


\begin{Example}
$SO \cup SSX \neq \ Top$. Why not?
\end{Example}

\begin{Theorem}
%  $Not(t) = \{t_1, \ldots, t_n \} \Bimp \forall i. t_i^c = t$

\end{Theorem}

\subsection{Lattices of Coverings}


Namely:
\begin{Def} For $\xi_1, \xi_2 \in \Xi$, we say that $\xi_1 \leq\xi_2 $ iff there is (well-typed) substitution $\q$ s.t.\ $\q\xi_1 \subseteq \xi_2 $.
\end{Def}



Properties:

\begin{Pty} [Covariance]
$ s \leq t$ entails for all coverings of $s,\ t, \ \xi^t \leq \xi^s$.
\end{Pty}
This induces an order-preserving emebdding of posets of coverings;
\begin{Lemma}[Embedding]
If $ s \leq t$ there there is a order omorphism such that $\Xi^t$ can be embedded in $\Xi^s$.

\end{Lemma}
In particular the structure $\Xi_{(x:\tau)}$ of tight type coverings is, under this ordering, a chain; besides only one substitufion, determined by $def(\tau)$ induces the comparison for every pair of terms


There is an equivalent, yet slightly more complicated way to impose an ordering over $\Xi_{t:\tau}$, that is for $\xi_1, \xi_2 \in \Xi$, we say that $\xi_1 \leq_{\q_j}\xi_2$  iff there is a possibly infinite sequence of (well-typed) assignments $\la \q_j\ra$ s.t.\ $\la \q_j\ra \xi_1 =
\xi_2 $ where assignments application is inductively defined as follows for $j \in J$:

\beq \xi_0 = & \la\ra \xi\\
\xi_{n+1} = & (\q_{n+1} \xi_n) \cup \xi_n\\
\xi_\infty = & \bigcup^\infty_{n = 1} \xi_n
\eneq

\begin{Examplen}
\[
0 \Or x \leq_{\la x mapsto 0, x\mapsto s0, x \mapsto ssy \ra} 0\Or s0 \Or ss0 \Or sssy
\]
\end{Examplen}
\begin{Ppn}
$\xi_1 \leq_{\q_j}\xi_2$  iff $\xi_1 \leq\xi_2$  
\end{Ppn}


Lattices of Coverings are still lattices of intensional terms, but with the restriction of being a cover for the generator.

Moreover, the structure $\Xi_{(t:\tau)}$ can be seen as a (?) lattice, where the top is the set enumerated by $t$, bottom is the (equivalence class) of a variable of the right type and (glb) lub corresponds to (anti)unification.


