\documentclass[acmtocl,acmnow]{acmtrans2m}
%\acmVolume{V}
%\acmNumber{N}
%\acmYear{YY}
%\acmMonth{Month}
% 

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amstext}
\usepackage{latexsym}
\usepackage{array}
\usepackage{proof}
\usepackage{code}


\usepackage{pstricks,pst-node,pst-tree}
\usepackage{graphics}
\usepackage{graphicx}
\usepackage{psfrag}
\usepackage{color}
\usepackage{floatfig}
% misc 

\def\OPTIONFull{0}

% from template
\newtheorem{theorem}{Theorem}[section]
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newdef{definition}[theorem]{Definition}
\newdef{remark}[theorem]{Remark}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% some abbreviations

\newcommand{\mygray}{\color{green}}
\newcommand{\mygreen}{\color{green}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Abbreviasions for linearization 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\tto}{\twoheadrightarrow}

\newcommand{\chars}{\mathsf{char}\;}
\newcommand{\integer}{\mathsf{int}\;}

\newcommand{\conc}{\;;\;}
\newcommand{\aunif}{\sqcup}
\newcommand{\aunifR}{\,\underline{\sqcup}\,}
\newcommand{\aunifS}{\,\underline{\sqcup}\,}
\newcommand{\aunifSub}{\;{\sqcup}\;}
\newcommand{\ares}{\Longrightarrow}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\Intro}{\mathsf{I}}
\newcommand{\Elim}{\mathsf{E}}

\newcommand{\FV}{\mathsf{FV}}
\newcommand{\FMV}{\mathsf{FMV}}
\newcommand{\dom}{\mathsf{dom}}

\newcommand{\D}{{\cal{D}}}
\newcommand{\E}{{\cal{E}}}

% \newcommand{\nnl}{\\\noindent\mbox{\hspace{-0.5cm}}}
\newcommand{\nnl}{\\}
% \newcommand{\nnll}{\\[0.5em]\noindent\mbox{\hspace{-0.5cm}}}
\newcommand{\nnll}{\\[0.5em]}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% explicit substitutions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\msub}[1]{\lbb #1 \rbb}
\newcommand{\inv}[1]{{#1}^{-1}\,}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Abbreviations for unification
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\newcommand{\unif}{\doteq}

\newcommand{\unifLHO}{\underset{A}{\doteq}}

\newcommand{\unifLHA}{\doteq}
%
\newcommand{\unifR}{\doteqdot}

\newcommand{\andl}{\wedge\;}
\newcommand{\typeLF}{\textsf{type}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\vd}{\vdash}
\newcommand{\vdN}{\Vdash}
\newcommand{\arrow}{\rightarrow}
\newcommand{\hastype}{\mathrel{:}}
\newcommand{\oftp}{\mathord{:}}
\newcommand{\ofvd}{\mathord{::}}
\newcommand{\lam}[2]{\lambda #1. #2}
\newcommand{\app}[2]{#1\; #2}
\newcommand{\clo}[2]{{#1}[#2]}
\newcommand{\ldot}{.\,}
\newcommand{\turn}{\mathord{\scriptstyle \vdash}}

\newcommand{\lbb}{{[\![}}
\newcommand{\rbb}{{]\!]}}
\newcommand{\for}{{/\!\!/}}
\newcommand{\Mu}{\lbb R/u\rbb}
\newcommand{\id}{\mathsf{id}}

\newcommand{\syn}{\Rightarrow}
\newcommand{\chk}{\Leftarrow}
\newcommand{\type}{\mathsf{type}}
\newcommand{\ctx}{\;\mathsf{ctx}}
\newcommand{\mctx}{\;\mathsf{mctx}}

\newcommand{\reduce}{{\textsf{reduce}}}

\newcommand{\bnfas}{\mathrel{::=}}
\newcommand{\bnfalt}{\mathrel{|}}

\newcommand{\Pibox}{\Pi^{\scriptscriptstyle\Box}}

\newcommand{\Psihat}{\hat{\Psi}}
\newcommand{\Gammahat}{\hat{\Gamma}}
\newcommand{\Phihat}{\hat{\Phi}}


\newcommand{\listd}{\mathsf{list }\;}
\newcommand{\nil}{\mathsf{nil}}
\newcommand{\cons}{\mathsf{cons }\;}


\newcommand{\iLF}{\tt{i}}
\newcommand{\propLF}{\tt{prop}}

\newcommand{\notLF}{\tt{not}\;}
\newcommand{\orLF}{\tt{or}\;}
\newcommand{\andLF}{\tt{and}\;}
\newcommand{\impLF}{\tt{imp}\;}
\newcommand{\forallLF}{\tt{forall}\;}
\newcommand{\existsLF}{\tt{exists}\;}
\newcommand{\eqLF}{\tt{eq}\;}
\newcommand{\eqnaLF}{\tt{e1}}
\newcommand{\eqioLF}{\tt{e2}}
\newcommand{\eqnoLF}{\tt{e3}}
%
\newcommand{\eqilLF}{\tt{e4}}
\newcommand{\eqirLF}{\tt{e7}}
\newcommand{\eqalLF}{\tt{e5}}
\newcommand{\eqarLF}{\tt{e6}}

\newcommand{\orl}{\vee}
\newcommand{\impl}{\supset}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Typesetting Deductions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newbox\tempa
\newbox\tempb
\newdimen\tempc
\newbox\tempd

\def\mud#1{\hfil $\displaystyle{#1}$\hfil}
\def\rig#1{\hfil $\displaystyle{#1}$}

\def\inruleanhelp#1#2#3{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
                        \setbox\tempd=\hbox{$\; #3$}%
                        \setbox\tempb=\vbox{\halign{##\cr
        \mud{#1}\cr
        \noalign{\vskip\the\lineskip}%
        \noalign{\hrule height 0pt}%
        \rig{\vbox to 0pt{\vss\hbox to 0pt{\copy\tempd \hss}\vss}}\cr
        \noalign{\hrule}%
        \noalign{\vskip\the\lineskip}%
        \mud{\copy\tempa}\cr}}%
                      \tempc=\wd\tempb
                      \advance\tempc by \wd\tempa
                      \divide\tempc by 2 }

\def\inrulean#1#2#3{{\inruleanhelp{#1}{#2}{#3}%
                     \hbox to \wd\tempa{\hss \box\tempb \hss}}}
\def\inrulebn#1#2#3#4{\inrulean{#1\quad\qquad #2}{#3}{#4}}

\def\ian#1#2#3{{\lineskip 4pt\inrulean{#1}{#2}{#3}}}
\def\ibn#1#2#3#4{{\lineskip 4pt\inrulebn{#1}{#2}{#3}{#4}}}

\def\lowerhalf#1{\hbox{\raise -0.8\baselineskip\hbox{#1}}}

\def\ianc#1#2#3{{\lineskip 4pt\lowerhalf{\inruleanhelp{#1}{#2}{#3}%
                   \box\tempb\hskip\wd\tempd}}}
\def\ibnc#1#2#3#4{{\lineskip 4pt\ianc{#1\quad\qquad #2}{#3}{#4}}}
\def\icnc#1#2#3#4#5{{\lineskip 4pt\ibnc{#1\quad\qquad #2}{#3}{#4}{#5}}}

\def\rulespacing{\renewcommand{\arraystretch}{3} \arraycolsep 5em}
\def\rulestretch{\renewcommand{\arraystretch}{3}}

\def\above#1#2{\begin{array}[b]{c}\relax #1\\ \relax #2\end{array}}
\def\abovec#1#2{\begin{array}{c}\relax #1\\ \relax #2\end{array}}

\def\cian#1#2#3{\ctr{\ianc{#1}{#2}{#3}}}
\def\cibn#1#2#3#4{\ctr{\ibnc{#1}{#2}{#3}{#4}}}

\def\hypo#1#2{\begin{array}[b]{c}\relax #1\\ \vdots \\ \relax #2\end{array}}
\def\hypoc#1#2{\begin{array}{c}\relax #1\\ \vdots \\ \relax #2\end{array}}
\def\hypol#1#2#3{\begin{array}[b]{c}\relax #1\\ #2 \\ \relax #3\end{array}}
\def\hypolc#1#2#3{\begin{array}{c}\relax #1\\ #2 \\ \relax #3\end{array}}

\def\ctr#1{\begin{array}{c} #1\end{array}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Higher-order term indexing based on substitution trees
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\markboth{Brigitte Pientka}{Higher-order term indexing using substitution trees}
\title{Higher-order term indexing using substitution trees}
\author{BRIGITTE PIENTKA \\ McGill University}
\begin{abstract} 
We present a higher-order term indexing strategy based on substitution
trees for simply typed lambda-terms. There are mainly two problems in
adapting first-order indexing techniques. First many operations used
in building an efficient term index and retrieving a set of candidate
terms from a large collection are undecidable in general for
higher-order terms. Second, the scoping of variables and binders in the
higher-order case presents challenges.

The approach taken in this paper is to reduce the problem to indexing
linear higher-order patterns, a decidable fragment of higher-order
terms, and delay solving terms outside of this fragment. We present
insertion of terms into the index based on computing the
most specific linear generalization of two linear higher-order  
patterns, and retrieval based on matching two linear higher-order
patterns. Our theoretical framework maintains that
terms are in $\beta\eta$-normal form, thereby eliminating the need to
re-normalize  
and raise terms during insertion and retrieval. Finally, we prove
correctness of our presented algorithms. This indexing structure is
implemented as part of the Twelf system to speed up the execution of
the tabled higher-logic  programming interpreter.  
\end{abstract}
\category{F.4.1}{Theory of Computation}{Mathematical Logic and Formal Languages}
\category{D.3.3}{Software}{Language Constructs and Features}[Frameworks]
\terms{Design, Theory}
\keywords{Indexing, type theory, logical frameworks}

\begin{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\maketitle     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}
First-order logic programming and theorem proving systems have
developed into highly sophisticated automated reasoning systems with
remarkable performance over the last decades
\cite{Ramakrishnan01:indexing}. This success is to a 
large extent due to term indexing techniques, which support these systems
to manage and use redundancy elimination techniques. In general, term
indexing is concerned with compactly storing a large collection of terms and
rapidly retrieving a set of candidate terms satisfying some property
(e.g. unifiability, instance, variant, etc.) from a large collection of
terms. 

There are many examples where term indexing is used.
In logic programming, for example, we need to select all clauses from
the program whose head unifies with the current goal
\cite{Ramesh:POPL90,Chen:SPE94,Dawson+95:jump,Dawson+95:unification}. In
tabled logic programming we memoize intermediate goals in a table and
reuse their results later in order to eliminate redundant and infinite
computation. Here we need to find all entries in the table such that
the current goal is a variant or an instance of a table entry and
re-use the associated answers 
\cite{RamakrishnanJLP99,Ramakrishnan95efficient}. Similarly, in theorem
proving we keep track of previously derived formulas to eliminate
redundancy and detect
loops \cite{McCune92,Graf+Book95,Riazanov:02,Hil03}. Since rapid
retrieval and efficient storage of large collections of terms plays a
central role in logic programming and in proof
search in general, a variety of indexing techniques have been proposed for
first-order terms (see \cite{Ramakrishnan01:indexing} for a survey). 
However, indexing techniques for higher-order terms, i.e. terms that 
contain lambda-abstractions, are largely missing thereby severely
hampering the performance of higher-order systems and limiting their
potential applications. There are mainly two problems in adapting first-order
indexing techniques. First, many operations used in building an
efficient term index and retrieving a set of candidate terms from a
large collection are undecidable in general in the higher-order setting. Second, the scoping of
variables and binders in the higher-order case presents challenges.  

In this paper, we present a higher-order term indexing technique
based on substitution trees. Substitution tree indexing
\cite{Graf+rta95} is a highly successful first-order term indexing
strategy which allows the sharing of common sub-expressions via
substitutions. We extend this idea to the higher-order setting and
present an indexing technique for higher-order terms.

The challenge in the higher-order setting 
is that many common operations on higher-order terms which are
necessary to build and maintain substitution trees or retrieve
elements from the index are undecidable in general. For example, to
build a substitution tree, we compute the most specific common
generalization between two terms. However, in general the most
specific generalization of two terms does not exist in the
higher-order setting. Similarly, retrieving all terms, which unify or
match, needs to be  efficient -- but higher-order unification is
undecidable in general. Fortunately, there exists a fragment called
higher-order patterns for which checking unifiability of
two terms and computing the most specific generalization
between two terms is decidable
\cite{Miller91iclp,Pfenning91lics}. However, even for this fragment
algorithms may not be  efficient in practice
\cite{PientkaPfenning:CADE03} and are sufficiently complex that it is
not obvious that they are a suitable basis for higher-order term
indexing techniques. 
%

In this paper we propose a general strategy for indexing
higher-order terms where we first translate higher-order terms to
linear higher-order patterns together with constraints, and second we
store linear higher-order patterns together with their constraints in
a substitution tree.  Linear higher-order patterns refine the notion
of higher-order patterns further and factor out computationally
expensive parts into constraints. As we have shown in
\cite{PientkaPfenning:CADE03} many terms encountered in practice fall
into this  fragment. Moreover, linear higher-order pattern unification
performs well in practice. In this paper, we demonstrate that linear
higher-order patterns are well suited to elegantly describe term
indexing operations such as  computing the most specific linear
generalization or checking unifiability of two terms. Moreover, we
give algorithms for inserting linear higher-order patterns into an
index and for retrieving a set of terms from the index such that the
query is an instance of the term in the index and prove the
correctness of these operations. 
%
We concentrate on simply typed terms in this
paper. However, the presented techniques can be generalized to the
dependently typed setting (see \cite{Pientka03phd}) and are in fact
implemented as part of the logical framework Twelf system
\cite{Pfenning99cade}. We have used higher-order substitution trees to
speed-up the execution of the tabled logic programming interpreter
\cite{Pientka:ICLP02,Pientka:CADE05} and to 
facilitate the generation of small proof witnesses
\cite{Pientka:ICLP05}. Preliminary results have been published in
\cite{Pientka:ICLP03}, and this paper expands the theoretical
results. The theoretical framework we present can directly serve as a
general foundation for higher-order term indexing in many higher-order
logic programming systems such as $\lambda$Prolog \cite{Nadathur99cade}, and 
higher-order theorem provers such as Bedwyr \cite{Baelde07:Bedwyr},
Isabelle \cite{Paulson86}, or Leo-II \cite{Benzmueller:IJCAR08}.
%


The paper is organized as follows:  In Section
\ref{sec:hosubstrees}, we present the general idea of higher-order
substitution trees. In Section \ref{sec:background}, we give the
theoretical background and in Section \ref{sec:thost} we describe
higher-order substitution trees more formally. In Section
\ref{sec:generalization}, we give algorithms for computing the most
specific linear generalization of two terms and inserting terms into
the index and retrieval is discussed in Section
\ref{sec:retrieve}. This is followed by a
discussion on extending the framework to dependently-typed terms in
Section \ref{sec:DepTypes}. We conclude with a discussion of
experimental results within the tabled higher-order logic programming
engine in the Twelf system (Section \ref{sec:exp}) and related
work (Section \ref{sec:related}).



\section{Higher-order substitution trees}\label{sec:hosubstrees}

We illustrate the general idea of substitution tree indexing
using a first-order example and then focus on indexing of
higher-order terms. In particular, we highlight some of the subtle
issues concerning the interplay of bound variables and meta-variables.
%
We will consider several examples in the logical framework Twelf
\cite{Pfenning99cade}, which provides a higher-order logic
programming engine to execute specifications to make the examples more
concrete. However, the issues arising are similar in other higher-order
systems which deal with lambda-terms.


\paragraph*{Example 1} To illustrate the basic idea consider the
example of equality transformations for propositional logic, described
by $A \Leftrightarrow B$.
%
In the logical framework Twelf
\cite{Pfenning99cade}, we first declare a data-type \texttt{prop} for
propositions, together with constructors for
propositions such as conjunction, implication, disjunction and
negation as follows.

\begin{center}
\begin{small}
\begin{tabular}{llp{0.5cm}ll}
{\tt{prop:}} & {\tt{type.}} & & & \\
{\tt{and:}} & {\tt{prop -> prop -> prop.  }} & & {\tt{or:}} & {\tt{prop -> prop -> prop.  }} \\
{\tt{imp:}} & {\tt{prop -> prop -> prop.  }} & &
{\tt{neg:}} & {\tt{prop -> prop.}}
\end{tabular}
\end{small}
\end{center}


Next, we present some equivalence preserving transformations
on propositions together with their encoding in 
Twelf using the predicate $\eqLF$.

\begin{minipage}[h]{5.5cm}
\begin{small}
\[
\begin{array}{lrcl}
\multicolumn{4}{l}{A \Leftrightarrow B} \\[0.5em]
%
e_1: & \neg (A \andl B) & \Leftrightarrow & (\neg A) \orl (\neg B).\\
e_2: & (A \impl B) & \Leftrightarrow & (\neg A) \orl B.\\
%
e_3: & A \impl \neg B & \Leftrightarrow & (\neg A) \orl (\neg B).\\
\end{array}
\]
\end{small}
\end{minipage}
\begin{minipage}[h]{5cm}
\begin{small}
\[
\begin{array}{ll}
\multicolumn{2}{l}{\eqLF :\;  \propLF \rightarrow \propLF \rightarrow \typeLF.}\\[1em]
%
\eqnaLF: \eqLF (\notLF (\andLF A\; B))& (\orLF (\notLF A)\; (\notLF B)).\\
\eqioLF: \eqLF (\impLF A\; B) & (\orLF (\notLF A) \; B).\\
%
\eqnoLF: \eqLF (\impLF A\; (\notLF B)) & (\orLF (\notLF A) \; (\notLF B)).\\
\end{array}
\]
\end{small}
\end{minipage}

%
First, we define predicate $\eqLF$ which represents the judgment for
equivalence preserving transformation between two propositions.
Next, we represent each equivalence transformation as a clause in a
logic program. To efficiently find the clause head which
unifies with a given goal, we would like to store these clauses in an index,
i.e. a data-structure which supports sharing of structure among these
clause heads. As we see, the three transformations share quite a lot
of structure, and in fact the last one is an instance of the previous
one. We will use it to illustrate some specific issues when inserting
these clauses one by one into a substitution tree.


Our intention is to share common structure of terms in order to share
common operations. For example, when checking whether a term $U$
unifies with any of the given 
clauses, we only want to perform the comparison against the
constructor $\orLF$ and the sub-term $(\notLF A)$ once. 
To achieve this, we compute the most
specific generalization between the given terms. For example, the most
specific generalization of the first and second clause stated is,
$\eqLF\;i_1\; (\orLF (\notLF A)\; i_2)$ where we can obtain the clause
$\eqnaLF$ by instantiating {\tt{i}}$_1$ with $(\notLF (\andLF A\; B))$
and {\tt i}$_2$ with 
$(\notLF B)$. Similarly, we can obtain the clause $\eqioLF$ by
instantiating {\tt i}$_1$ with $(\impLF A\; B)$ and {\tt i}$_2$ with
{\tt B}. 
 {\tt i}$_0$,{\tt i}$_1$, {\tt i}$_2, \ldots$ denote meta-variables
 which represent holes in terms. A term can be represented as a
 sequence of substitutions. For example, the clause $\eqnaLF$ can be described
as $\msub{(\notLF (\andLF A\; B))/i_1, (\notLF
  B)/i_2}(\eqLF\;i_1\;(\orLF (\notLF A)\; i_2))$. A substitution tree
is a tree where each node contains a set of substitutions. The tree
containing the clause $\eqnaLF$ and $\eqioLF$ is given next. The
original clauses can be obtained by composing all the 
 substitutions along one branch. To easily identify, which branch
 corresponds to which clause, we  labelled the leafs with the name of
 the clause.  
%

%
\vspace{-0.25cm}
\begin{center}
\begin{small}
%
\pstree[nodesep=0.1pt,levelsep=7ex]{%
\TR{$(\eqLF\;i_1 \; (\orLF (\notLF A)\; i_2))/i_0$} }{%
   \pstree[nodesep=0.1pt,levelsep=5ex]{\TR{\begin{tabular}{r}
                      $(\notLF(\andLF A\;B))/i_1$,\\
                      $(\notLF B)/i_2$
                     \end{tabular}
                     }}{$\eqnaLF$}
%
          \pstree[nodesep=0.1pt,levelsep=5ex]{\TR{\hspace{-0.75cm}\begin{tabular}{r}
                       $(\impLF A\;B)/i_1$,\\
                       ${\tt B}/{\tt i}_2$
                      \end{tabular}
                    }}{$\eqioLF$}
          }
\end{small}
\end{center}
\vspace{-0.1cm}

Let us now consider what happens, when we insert $\eqnoLF$. The clause
is an instance of the root of the tree, and we obtain the substitution
$(\impLF A\; (\notLF B))/i_1$ and $(\notLF B)/i_2$. Hence we call the
clause head and the substitution at the root of the tree fully compatible,
and we now continue to insert this substitution into one of the
children. However, the substitution $(\impLF A\; (\notLF B))/i_1$ and
$(\notLF B)/i_2$ is not fully compatible with any of the substitutions
in the children; hence we need to split one of the children. There are in
fact two possible splits, and therefore the two possible substitution
trees are shown in Figure \ref{fig:stree}.

%
\begin{figure}[htb]
Inserting $\eqnoLF$ to the left:
%
\begin{small}
%
\pstree[nodesep=0.1pt,levelsep=7ex]{%
\TR{$(\eqLF\;i_1 \; (\orLF (\notLF A)\; i_2))/i_0$} }{%
   \pstree[nodesep=0.1pt,levelsep=5ex]{\TR{$(\notLF B)/i_2$}}{%
     \pstree[nodesep=0.1pt,levelsep=5ex]{
       \TR{$(\notLF(\andLF A\;B))/i_1$}}{$\eqnaLF$}
%
     \pstree[nodesep=0.1pt,levelsep=5ex]{
       \TR{$(\impLF A\;(\notLF B))/i_1$}}{$\eqnoLF$}
   }
%
   \pstree[nodesep=0.1pt,levelsep=5ex]{\TR{\hspace{0.75cm}\begin{tabular}{r}
                       $(\impLF A\;B)/i_1$,\\
                       ${\tt B}/{\tt i}_2$
                      \end{tabular}
                    }}{\hspace{1.5cm}$\eqioLF$}
          }
    \end{small}
%
%
%
\\[1.5em]
 Inserting $\eqnoLF$ to the right:
%
    \begin{small}
\pstree[nodesep=0.1pt,levelsep=7ex]{%
\TR{$(\eqLF\;i_1 \; (\orLF (\notLF A)\; i_2))/i_0$} }{%
   \pstree[nodesep=0.1pt,levelsep=5ex]{\TR{\begin{tabular}{r}
                      $(\notLF(\andLF A\;B))/i_1$,\\
                      $(\notLF B)/i_2$
                     \end{tabular}
                     }}{$\eqnaLF$}
%
          \pstree[nodesep=0.1pt,levelsep=7ex]{
            \TR{$(\impLF A\;i_3)/i_1$}}{%
            \pstree[nodesep=0.1pt,levelsep=5ex]{
              \TR{\begin{tabular}{r}
                       ${\tt B}/{\tt i}_3$\\
                       ${\tt B}/{\tt i}_2$
                      \end{tabular}
                    }}{$\eqioLF$}
                  % 
            \pstree[nodesep=0.1pt,levelsep=5ex]{
              \TR{\begin{tabular}{r}
                       $(\notLF B)/i_3$\\
                       $(\notLF B)/i_2$
                      \end{tabular}
                    }}{$\eqnoLF$}
          }
        }
\end{small}
 \caption{Substitution tree after inserting $\eqnoLF$}
  \label{fig:stree}
\end{figure}

The choice on how to split nodes when inserting new elements in a tree
must be resolved in practice. Typically, we can make more informed
choices if the full set of terms we want to index is known in
advance. This is for example the case when indexing clauses in a logic
program, and we can employ techniques such as unification factoring
\cite{Dawson+95:optimizing} to obtain an optimal tree. In theorem
proving or tabled logic programming on the other hand we store
intermediate sub-goals and formulas which are encountered during proof
search. Consequently, elements are inserted into the index
incrementally, and less information is available to make informed
splitting choices. While resolving these choices in practice is
important, we focus in this paper on extending substitution trees to
indexing higher-order terms. This means we will concentrate on the
essential operation of computing the most specific generalization of
terms and substitutions in the higher-order setting.   


\paragraph*{Example 2} To illustrate the higher-order issues, we
consider some well-known equivalence preserving transformation in
first-order logic.

\[
\begin{array}{llcl}
%
e_5: & (\forall x. A(x))  \orl  B & \Leftrightarrow & \forall x. A(x)  \orl  B\\
e_6: & A  \orl (\forall x.B(x)) & \Leftrightarrow & \forall x. A  \orl  B(x)\\
e_7: & (\forall x. A(x))  \impl B & \Leftrightarrow & \forall x. A(x)  \impl  B
%
\end{array}
\]

Of course these stated equality preserving transformations are only
valid, if certain bound  variable conditions are satisfied. For
example, the first translation requires that the bound variable $x$
does not occur in $B$. These conditions are naturally enforced using
higher-order abstract syntax where bound variables in the object
language are represented by bound variables in the meta-language. We
first define the constructor $\texttt{forall}$ with type $(\iLF
\rightarrow \propLF) \rightarrow \propLF$. The universal quantifier
$\forall x.A(x)$ is then encoded as $\forallLF \lambda x. {\tt
  A}\;{\tt x}$ and
bound variables are represented by the $\lambda$-binder. The
representation of the equivalence preserving transformations is given
below.   

\begin{small}
\[
\begin{array}{lllccllcc}
%
\eqalLF: & \eqLF & (\orLF & \;\;(\forallLF \lambda x. A \;x) \;& {\tt
  B} &) &
                   (\forallLF \lambda x. (\orLF & ({\tt A}\; {\tt
                     x})\; & {\tt B})).\\
\eqarLF: & \eqLF & (\orLF & {\tt A} & (\forallLF \lambda x. {\tt B}\; {\tt x}) & ) &
                   (\forallLF \lambda x. (\orLF & {\tt A} \;& ({\tt
                     B}\;{\tt x}))).\\
\eqirLF: &\eqLF & (\impLF & (\forallLF \lambda x. {\tt A}\;{\tt x}) &  {\tt B} & ) & 
                  (\forallLF \lambda x. (\impLF & ({\tt A}\;{\tt x}) \; & {\tt B})).\\
\end{array}
\]
\end{small}

In the higher-order setting, meta-variables denote a {\it{closed}} instance of
terms. The meta-variable {\tt A} in the first translation denotes a
function which is applied 
to {\tt x}, {\tt B} however denotes an atomic proposition, and hence cannot
depend on the bound variable {\tt x}. As this example illustrates,
bound variable dependencies are naturally and elegantly encoded in
this higher-order setting, and higher-order unification must
enforce these variable dependencies. To highlight the common structure
between the three transformation, we have inserted appropriate spaces.


Inspecting the three given clauses closely, we observe that they share
a lot of structure. For example clause $\eqalLF$ and $\eqarLF$
``almost'' agree on the second argument. Our goal is to share common
structure of terms in order to share common operations even below a
binder. 
%
This means for example that we would like to
share the term $\forallLF \lambda x. \Box$ where $\Box$ is instantiated
with $\orLF (A\;x)\;B$ to obtain the terms $\eqalLF$, and we
instantiate $\Box$ with $\orLF A\;(B\; x)$ to obtain $\eqarLF$. Finally,
to obtain $\eqirLF$, we instantiate $\Box$ with with $(\impLF
(A\;x)\;B)$. Note that in all these cases $\Box$ is instantiated with
an open term which is  allowed to refer to the bound variable {\tt
  x}. Our indexing structure supports such sharing of expressions even
in the presence of binders 
and allows instantiations with open terms, i.e. terms which may
contain bound variables. This is unlike the first-order case where
holes were always instantiated with closed terms. To achieve this, we
characterize holes as a closure of a meta-variable {\tt i} together
with a delayed substitution. This substitution precisely characterizes
the dependencies we allow when instantiating the meta-variable with an
open term. For example, $(\forallLF \lambda x. \Box)$ is denoted by
$(\forallLF \lambda x. i[x/y])$ where {\tt i} is a meta-variable and
{\tt[x/y]} is a postponed substitution. When we instantiate the
meta-variable {\tt i} with $(\orLF (A\;y)\;B)$ we will apply the
substitution {\tt [x/y]} which essentially renames the variable {\tt
  y} to {\tt x}, and yields as a final result $(\forallLF \lambda
x.\orLF (A\;x)\;B)$. In the term $\orLF\;\Box\;A$, the hole denoted by
$\Box$ can be instantiated with a closed term. In this case we write
$i[.]$ for $\Box$. Since there are no bound variables involved the
postponed substitution we associate with the meta-variable {\tt i} is
the empty. 

Associating meta-variables
with a postponed substitution is a known technique from explicit
substitution calculus. However instead of using the explicit substitution
calculus based in de Bruijn indices \cite{Abadi:POPL90,Dowek95}, we
use the contextual modal type theory \cite{Nanevski:ICML05} as a
foundation which provides a high-level explanation of
meta-variables. Characterizing holes in terms as a closure of
meta-variable and a postponed substitution will allow us to
instantiate holes using first-order replacement.
%

This has two key advantages: First, the term representation 
is more compact than other representations. Traditionally, we would
represent the hole in the term $\forallLF \lambda x. \Box$  with the
application $\texttt{I}\;x$ where \texttt{I} represent the
meta-variable which is subject to instantiation. This means in
general, if we have $n$ bound variables $x_1,\ldots,x_n$, the  
meta-variable {\tt{I}} which is inserted must be applied to all of
these variables. Second, to obtain the original term, we must
instantiate \texttt{I} in  the term $\forallLF \lambda
x. \texttt{I}\;x$ with the lambda-abstraction 
$\lambda {\texttt y}.\orLF (A\;y)\;B$. To compare the result of this
instantiation with the original term, we must now re-normalize the
term, $\beta$-reducing the created redex 
$(\lambda \tt{y}.\orLF (A\;y)\;B)\;x$ to 
$[\tt{x}/y](\orLF (A\;y)\; B) = \orLF (A\;x)\;B$.
%
The goal of treating meta-variables as closures consisting of the
meta-variable itself and a postponed substitution avoids this
re-normalization step, but allows direct replacement of the
meta-variable with the appropriate instantiation. In an implementation
with de Bruijn indices and explicit substitutions
\cite{Abadi:POPL90,Dowek95},  the postponed renaming substitution can
in fact be omitted\footnote{More precisely, this corresponds
  to shifting de Bruijn indices by zero.}. As a consequence, we not
only obtain direct in-place update of meta-variables, but also a
compact representation of the term with the hole. 
This has important consequences for the theoretical development as
well as implementations. The formal description of the operations and
their correctness proofs will be substantially simpler since we do not
need to consider re-normalization. Instead, we will maintain that all
terms are in canonical forms. It has also important practical
implications. Because we treat meta-variables as closures our formal
description can be directly implemented using de Bruijn indices and
explicit substitutions following similar ideas already employed
for implementing higher-order unification \cite{Abadi:POPL90,Dowek95}.


%
To insert these three clauses into a substitution tree, we need to compute the
most specific common generalization. As mentioned earlier, this
problem is in general undecidable in the higher-order setting. To do
this in a simple manner, we first translate terms into linear higher-order
patterns \cite{PientkaPfenning:CADE03} together with
constraints. Linear higher-order patterns refine the notion of
higher-order patterns \cite{Miller91iclp,Pfenning91lics} 
where every meta-variable must be applied to {\em some}
distinct bound variables in two ways: First, linear higher-order
patterns require that every meta-variable occurs only once and
in addition every meta-variable is applied to {\em{all}}
distinct bound variables in its context. 

Maintaining these
two conditions yield a simple algorithm and allows us to delay
the occurs check during retrieval and any other complicated conditions
involving bound variable occurrences.  
%
For example, the term 
$(\forallLF \lambda x. (\impLF p(x)\;q(x)))$ should not unify with 
$(\forallLF \lambda x. (\impLF (A\;x)\;B))$, because we must
instantiate the meta-variable {\texttt B} with a closed term. Hence, it is
invalid to replace $B$ with $\texttt{q(x)}$. Checking for bound variable
dependencies in the higher-order setting is as expensive as the occurs
check, and requires a traversal of a term; hence it is beneficial to
delay any necessary bound variable checks. 

%
As we observe, meta-variables {\texttt A} and {\texttt B}
occur more than once in all of the above clauses, and moreover the
occurrence of {\texttt B} is not fully applied. For example, in
%
$\eqLF (\orLF (\forallLF \lambda x. {\tt A}\; {\tt x})\; {\tt
  B})\quad (\forallLF \lambda x. (\orLF ({\tt A}\; {\tt x})\; {\tt B})
$
%
the meta-variable {\tt B} does not depend on the bound variable
{\tt x} in $(\forallLF \lambda x. (\impLF ({\tt A}\; {\tt
      x})\; {\tt B}))$
although it occurs within the scope of the binder {\tt x}. 
Hence, {\tt  B} is
not a linear higher-order pattern, since it is not applied to all
bound variables in whose scope it occurs. In addition, the
meta-variable {\tt A} occurs twice. Before inserting the clauses into a 
substitution tree, we therefore first linearize terms by eliminating
any duplicate occurrences of meta-variables, and replacing any
meta-variable which is not fully applied with one which is. This
linearization step takes as input a clause, and produces a clause
which only contains linear higher-order patterns together with some
constraints described by $\unif$. 
The program after linearization is shown next: 

\begin{small}
\[
\begin{array}{ll}
\eqalLF: \eqLF (\orLF (\forallLF \lambda x. A \;x) \; B)\quad
                 (\forallLF \lambda x. \orLF (A'\; x) \; (B'\;x)).\\
\hspace{1cm} \forall {\tt x}. ({\tt A}'\; {\tt x}) \unif ({\tt A} \;
{\tt x}) \wedge  \forall {\tt x}.{\tt B}'\;{\tt x}   \unif {\tt B}\\[0.25em]
\eqarLF: \eqLF (\orLF A \; (\forallLF \lambda x. B\; x)) \quad
                 (\forallLF \lambda x. \orLF (A'\;x) \; (B' x)).\\
\hspace{1cm} \forall {\tt x}. ({\tt A}'\; {\tt x}) \unif {\tt A}
\wedge  \forall {\tt x}. {\tt B}'\;{\tt x}
\unif ({\tt B}\;{\tt x})\\[0.25em]
\eqirLF: \eqLF (\impLF (\forallLF \lambda x. A\;x)\; B)\quad
                 (\forallLF \lambda x. (\impLF (A'\;x) \; (B'\; x))).\\
\hspace{1cm} \forall {\tt x}. ({\tt A}'\; {\tt x}) \unif ({\tt A}\;{\tt
  x})
\wedge  \forall {\tt x}.{\tt B}'\;{\tt x}   \unif {\tt B}
%
\end{array}
\]
\end{small}

We view linearization as a standardization step, which is also in a simpler
form present in first-order indexing techniques. In the first-order
setting, terms are linearized and duplicate occurrences of
meta-variables are factored out in order to postpone the occurs
check. Our notion of linear higher-order patterns establishes a
criteria with the 
same intentions of factoring out expensive operations in the
higher-order setting. Together with the linear term, we 
simply store variable definitions, which establish the equality
between these two meta-variables. 

When inspecting the translated clauses $\eqalLF$, $\eqarLF$, and $\eqirLF$, 
even more sharing becomes apparent. For example, the clauses
$\eqalLF$ and $\eqarLF$ agree upon the last argument. We now compute the most specific generalization between these clauses, and can build up a substitution
tree. Each node in the substitution tree contains a set of
substitutions, and variable definitions which resulted from
linearizing terms are found at the leafs. 


  \begin{center}
    \begin{small}
\pstree[nodesep=0.1pt,levelsep=8ex]{%
\TR{$(\eqLF\quad i_2[\ldot] \quad (\forallLF \lambda x. i_1[x/y])) / i_0$} }{%
  \pstree[nodesep=0.1pt,levelsep=9ex]{\TR{\begin{tabular}{r}
              $(\orLF (A'\;y)\; (B'\;y))/i_1$\\
              $(\orLF (i_3[\ldot])\; (i_4[\ldot]))/i_2$\\
            \end{tabular}
          }
        }{%
          \pstree[nodesep=0.1pt,levelsep=8ex]{\TR{\begin{tabular}{r}
                $(\forallLF \lambda x. A\;x)/i_3$,\\
                ${\tt B/i_4}$
              \end{tabular}
            }}{%
            \pstree[nodesep=0.1pt,levelsep=8ex]{\TR{\begin{tabular}{l}
                  $\forall {\tt x}. {\tt A}'\;{\tt x} \unif {\tt
                    A}\;{\tt x} \;\wedge$\\
                  $\forall {\tt x}. {\tt B}'\;{\tt x}\unif {\tt B}$
                \end{tabular}
              }}{ $\eqalLF$}
          }
%
          \pstree[nodesep=0.1pt,levelsep=8ex]{\TR{\begin{tabular}{r}
                ${\tt A/i_3},$\\
                $(\forallLF \lambda x. (B\;x))/i_4$
              \end{tabular}
            }
          }{%
            \pstree[nodesep=0.1pt,levelsep=8ex]{\TR{\begin{tabular}{l}
                $\forall {\tt x}. {\tt A}'\;{\tt x} \unif {\tt A}\; \wedge$\\
                $\forall {\tt x}. {\tt B}'\;{\tt x} \unif {\tt
                  B}\;{\tt x}$
              \end{tabular}
            }
            }{ $\eqarLF$}
          }
        }
%%%%% second child
          \pstree[nodesep=0.1pt,levelsep=9ex]{\TR{\begin{tabular}{r}
                     $(\impLF (A'\;y)\; (B'\;y))/i_1$\\
                     $(\impLF (\forallLF \lambda x. A\;x)\; B)/i_2$\\
                   \end{tabular}
                 }
               }{%
                 \pstree[nodesep=0.1pt,levelsep=8ex]{\TR{\begin{tabular}{l}
                       $\forall {\tt x}. {\tt A}'\;{\tt x}\unif {\tt
                         A}\;{\tt x}\; \wedge$\\
                       $\forall {\tt x}. {\tt B}'\;{\tt x}\unif {\tt B}$
                     \end{tabular}
                   }}{$\eqirLF$}
                   }
}

\end{small}
\end{center}


\paragraph*{Summary}
 To insert a term $R$ in a substitution tree, we
first translate it into a linear higher-order pattern $R'$, together
with constraints $C$. Insertion of a  term $R'$, into the index can
then be viewed as insertion of the substitution $R'/i_0$. To insert
this substitution, we compute the most specific linear generalization
between the given substitution and the one in the tree. This will
require us to split nodes which are not fully compatible. In the
remainder of the paper, we introduce the theoretical framework for
simply typed lambda-terms with first-class meta-variables and
formalize key operations such as computing the most-specific
generalization of two terms and two substitutions. Based on this
development, we define precisely criteria when two terms (or two
substitutions) are compatible, and how to insert and retrieve a
substitution from a given substitution tree.


\section{Background}\label{sec:background}
\subsection{Contextual modal type theory}
In this section we introduce a simply typed lambda-calculus with
first-class meta-variables which allows the instantiation of
meta-variables with open terms \cite{Nanevski:ICML05}. Previously, we
have used the contextual modal type theory as a foundation for
describing linear higher-order pattern unification
\cite{PientkaPfenning:CADE03,Pientka03phd}.  

\[ \begin{array}{rrcl}
 \mbox{Types} & A,B,C & ::= & P \mid A \arrow B  \\
 \mbox{Normal Objects} & M,N & ::= & \lam{x}{M} \mid R \\
 \mbox{Atomic Objects} & R & ::= & H \cdot S \mid u[\sigma] \\
 \mbox{Head}        & H & ::= & x \mid c   \\
 \mbox{Spines} & S & ::= & \nil \mid M ; S\\[1ex]
 \mbox{Contexts} & \Gamma,\Psi & ::= & \cdot \mid \Gamma, x{:}A \\
 \mbox{Substitutions} & \sigma, \tau & ::= & \ldot \mid \sigma, N/x \mid \sigma, H\for x \\[1ex]
 \mbox{Modal Contexts} & \Delta & ::= & \cdot \mid \Delta, u{::}P[\Psi] \\[1ex]
%
\end{array} \]

We write $P$ for base types, and function types are denoted by $A
\arrow B$. We  enforce terms to be in normal form by exploiting a
presentation technique due to  Watkins et  al.~\cite{Watkins02tr} and
described in detail in \cite{Nanevski:ICML05}. While the syntax only
guarantees that terms $N$ are normal (that is, contain no
$\beta$-redices), the typing rules 
will in addition guarantee that all well-typed terms are fully
$\eta$-expanded. We will use the spine
notation \cite{Cervesato:JLC03} to describe atomic terms. The term
$((c\;M_1)\;M_2)$ is for example  represented in spine form as $c
\cdot (M_1 ; M_2 ; \nil)$. This is  convenient when we compare,
analyze and manipulate terms because we  have direct access to the
head $c$ of the term. It is also close to  our implementation where we
represent terms using spines. 

 As we mentioned, we concentrate on objects in normal form. This has
 two reasons: First, these are the only meaningful objects in the logical
framework, but in addition equality between two terms in normal form
is easily decided by simply checking whether the two terms are
syntactically equal up to  $\alpha$-renaming. Working only with normal
forms in our theoretical development significantly simplifies our
presentation and  proofs. Moreover, it is also close to our actual
implementation which maintains normal forms when inserting and
retrieving terms from an index. This means we avoid
re-normalization of terms in the implementation. 

We  follow a  bi-directional type checking approach which
characterizes objects in canonical form. In order to 
achieve this we divide the term calculus into \emph{atomic objects}
$R$ and \emph{normal objects} $M$. 
Contexts $\Gamma$ and $\Psi$ contain only declarations $x{:}A$ where
$A$ is normal and all terms  occurring in substitutions $\sigma$ are
either normal (in $N/x$) or replace $x$ by a head (in $H\for x$). 
The modal context $\Delta$ contains declarations of meta-variables
$u{::}P[\Psi]$.  We enforce that all meta-variables occurring in
well-typed terms must be of base type, i.e. they are lowered. 
%
Because any occurrence of a meta-variable $u[\sigma]\;M$ where
$u$ is of function type $(A \arrow B)[\Psi]$ and $M$ has type $A$
can be replaced by a new meta-variable $v[\sigma, M/x]$ where $v$ has
type $B[\Psi,x{:}A]$ (see also \cite{Dowek95,PientkaPfenning:CADE03}), this
is not a restriction. 
%

%
We assume global constants are declared in a signatures $\Sigma$ and never
change in the course of a typing derivation.  We therefore suppress
the signatures throughout. Moreover, we only consider well-formed
types. Typing at the level of objects is divided into four judgments: 
\[ \begin{array}{ll}
 \Delta ; \Gamma \vdash M \chk A & \mbox{Check normal object $M$ against  $A$} \\
 \Delta ; \Gamma \vdash R \syn P & \mbox{Synthesize base type $P$ for
   atomic object $R$} \\
 \Delta ; \Gamma \vdash S > A \syn P & \mbox{Synthesize base type $P$
   for spine $S$ and $A$} \\
 \Delta ; \Gamma \vdash \sigma \chk \Psi & \mbox{Check $\sigma$ against $\Psi$}
\end{array} \]

We always assume that $\Delta$ and $\Gamma$ and the subject ($M$, $R$,
or $\sigma$) are given, and that the contexts $\Delta$ and $\Gamma$
are well-formed. For synthesis $R \syn P$ we assume $R$
is given and we generate an base type $P$. Similarly, for $S > A
\syn P$ we assume $S$ and $A$ to be given, but infer the type $P$. The
typing rules are given in Figure \ref{fig:lftyping}.
%

%
\begin{figure}[h] 
  \centering
\[ \begin{array}{c@{\hspace{0.75cm}}c}
\multicolumn{2}{l}{\mbox{Normal objects\hspace{10cm}}}\\[0.5em]
\infer[{\textsf{Lam}}]
       {\Delta ; \Gamma \vdash \lam{x}{M} \chk A \arrow B}
       {\Delta ; \Gamma,x{:}A \vdash M \chk B}
 &
 \infer[{\syn}{\chk}]
       {\Delta ; \Gamma \vdash R \chk P}
       {\Delta ; \Gamma \vdash R \syn P}
%
%
 \\[0.6em]
\multicolumn{2}{l}{\mbox{Atomic objects}}\\[0.5em]
 \infer[\mathsf{var}]
       {\Delta ; \Gamma,x{:}A,\Gamma' \vdash x \cdot S \syn P}
       {\Delta ; \Gamma,x{:}A, \Gamma' \vdash S > A \syn P}
 &
 \infer[\mathsf{con}]
       {\Delta ; \Gamma \vdash c \cdot S \syn P}
       {c{:}A \in \Sigma & \Delta ; \Gamma \vdash S > A \syn P}
\\[0.5em]
 \multicolumn{2}{c}{
 \infer[\mathsf{mvar}]
       {\Delta, u{::}P[\Psi],\Delta' ; \Gamma \vdash \clo{u}{\sigma} \syn P}
       {\Delta, u{::}P[\Psi],\Delta' ; \Gamma \vdash \sigma \chk \Psi}
 }
%
%
%
\\[0.5em]
\multicolumn{2}{l}{\mbox{Spines}}\\[0.5em]
 \infer[{\sf{Scons}}]
       {\Delta ; \Gamma \vdash M\; ; \;S > A \arrow B \syn P}
       {\Delta ; \Gamma \vdash S > B \syn P
        &
        \Delta ; \Gamma \vdash M \chk A}
& 
\infer[{\sf{Snil}}]
      {\Delta ; \Gamma \vdash \nil > P \syn P}{}
%
\\[0.6em]
\multicolumn{2}{l}{\mbox{Substitutions}}\\[0.5em]
 \infer[\mathsf{sNorm}]
       {\Delta ; \Gamma \vdash (\sigma, M/x) \chk (\Psi, x{:}A)}
       {\Delta ; \Gamma \vdash \sigma \chk \Psi
        &
        \Delta ; \Gamma \vdash M \chk A}
& 
 \infer[\mathsf{sEmpty}]
       {\Delta ; \Gamma \vdash (\cdot) \chk (\cdot)}
       {\mathstrut}
%
 \\[0.6em]
%
 \infer[\mathsf{sAtom{-}v}]
       {\Delta ; \Gamma \vdash (\sigma, y\for x) \chk (\Psi, x{:}A)}
       {\Delta ; \Gamma \vdash \sigma \chk \Psi & \Gamma(y) = A}
& 
 \infer[\mathsf{sAtom{-}c}]
       {\Delta ; \Gamma \vdash (\sigma, c\for x) \chk (\Psi, x{:}A)}
       {\Delta ; \Gamma \vdash \sigma \chk \Psi & \Sigma(c) = A}
\end{array} \]  
  \caption{Bi-directional typing rules for simply-typed lambda-calculus}
  \label{fig:lftyping}
\end{figure}


In general, introduction forms for a type constructor break down a type
when read from the conclusion to the premise until it is atomic. In
our case we only have two types, base types and
functions. Lambda-abstractions are checked against their type. When
checking a normal object that happens to be atomic (that is, has the
form $R$) against a type $P$ we synthesize the type $P$ for
$R$. Technically, we synthesize a type $P'$ which must be equal to $P$.
We will leave this comparison implicit to simplify the development. 

In the case where $R$ has base type, it is either a
meta-variable $\clo{u}{\sigma}$ or it is of the form 
$c \cdot S$ or $x \cdot S$. We first concentrate on the case where 
$R = c \cdot S$ or $x \cdot S$ where $S = N_1;\ldots ;N_n; \nil$. 
In either case we are able to synthesize its type as follows. We first
look up the type $A_1 \arrow \ldots A_n \arrow P'$ for $c$ and $x$
resp. Then we can synthesize a type $P'$ for $c \cdot S$ (and $x \cdot
S$ resp.), if  for all $i$, $N_i$ checks against $A_i$. 

Because meta-variables are lowered, i.e. they must be of base type
$P$, we can easily synthesize its type by looking up the type for $u$
in the meta-variable context $\Delta$. While $\clo{u}{\sigma}$ 
synthesizes a type, we need the type of $u$, namely $P[\Psi]$ so we
can check $\sigma$ against $\Psi$.  Some renaming is left implicit
here, as the variables in the domain of $\sigma$ should match the
variables declared in $\Psi$. 
%

%
Substitutions are constructed in two possible ways: either by $M/x$
which replaces the variable $x$ with a normal term $M$, or by $H\for x$
which replaces the variable $x$ directly with a head. 
Substitutions $H\for x$ are necessary so that we can extend a given
substitution with $x\for x$ when traversing a binding operator. We
could not extend substitutions with $x/x$, since $x$ is not a
canonical term. The identity substitutions can now have the form
$x_1\for x_1, \ldots, x_n\for x_n$.  

\begin{theorem}[Decidability of type checking]
All judgments in the simply typed contextual modal type theory are decidable.
\end{theorem}
\begin{proof}
  The typing judgments are syntax-directed and therefore decidable.
\end{proof}

Since our description of substitution trees relies on a concise notion
of substitution, we carefully define ordinary substitution for
ordinary variables and contextual substitutions for meta-variables. 



\subsection{Substitution on Terms}
\label{sec:subst-term}

 In this section we start with defining the operations of substitution
 on terms.  The substitution function we need must construct
canonical terms, since those are the only ones that are well-formed
and the only ones of interest. Hence, in places where the ordinary
substitution operation would create a redex, in particular when
applying the substitution $[M/x]$ to a term $x \cdot S$, we must apply
the substitution $[M/x]$ to the spine $S$, but we also must
reduce the redex $(M \cdot [M/x]S)$ which would be created. Since when
applying $[M/x]$ to the spine $S$, we again may encounter situations
which require us to contract a redex, the substitution $[M/x]$ must be
hereditary. We therefore call this operation {\em{hereditary substitution}}.


This technique was first described for logical frameworks in
\cite{Watkins02tr}, and it only allows for objects which 
are in canonical form since only these are meaningful for
representing object-languages in logical frameworks. Here we use this
technique in the simply typed setting to ensure that terms are in
$\beta\eta$-normal form thereby eliminating the need to explicitly
consider $\beta\eta$-normalization when analyzing, manipulating and
comparing terms. The main difficulty in defining hereditary
substitutions is that this operation could easily fail to
terminate. Consider for example the term which arises when computing
the normal form of  $(\lambda y. y\;y)\;(\lambda 
x.x\;x)$. Clearly, on well-typed terms this does not occur. 
%


We define hereditary substitutions as a primitive recursive functional
where we pass in the type of the variable we substitute for. This will
be crucial in determining termination of the overall substitution
operation. If we hereditarily substitute $[\lambda y.M/x](x \cdot S)$,
then if everything is well-typed and $x:A_1 \arrow A_2$, then we will write $[\lambda y.M/x]_{A_1 \arrow A_2}(x \cdot S)$ indexing the substitution with the type for $x$. The substitution operation will be total since any side condition
can be satisfied by $\alpha$-conversion. First, we present the
ordinary capture-avoiding substitution for a single variable, $[M/x]_A
N$, $[M/x]_A S$, and$[M/x]_A \sigma$.   

\[ \begin{array}{lcll}
 [M/x]_A(\lam{y}{N}) & = & \lam{y}{N'} & \mbox{where } N' =
 [M/x]_A N \\ 
& & & \mbox{choosing $y \not\in \FV(M)$ and $y \neq x$} \\ \relax
 [M/x]_A(\clo{u}{\sigma}) & = & \clo{u}{\sigma'} & \mbox{where
 }\sigma' = [M/x]_A \sigma\\ \relax
 [M/x]_A(c \cdot S) & = & c \cdot S' & \mbox{where } S' = [M/x]_A S\\ \relax
 [M/x]_A(x \cdot S) & = & \reduce (M:A, S') & \mbox{where }S'
 = [M/x]_A S\\ \relax
 [M/x]_A(y \cdot S) & = & y \cdot S'& \mbox{where $y \neq x$ and
 } S' = [M/x]_A S\\[0.5em] \relax
%
 [M/x]_A(\nil) & = & \nil  & \\ \relax
 [M/x]_A(N ; S) & = & N' ; S' & \mbox{where } N' = [M/x]_A N \mbox{
   and }S' = [M/x]_A S\\[0.5em] \relax
 [M/x]_A(\cdot) & = & \cdot & \\ \relax
 [M/x]_A(\sigma, N/y) & = & (\sigma', N'/y) & 
\mbox{where } \sigma' = [M/x]_A \sigma \mbox{ and } N' = [M/x]_A N \\
\relax
 [M/x]_A(\sigma, c \for y) & = & (\sigma', c \for y) & 
\mbox{where } \sigma' = [M/x]_A \sigma \\ \relax
 [M/x]_A(\sigma, y' \for y) & = & (\sigma', y' \for y) & 
\mbox{where } \sigma' = [M/x]_A \sigma \mbox{ and } x \neq y'\\ \relax
 [M/x]_A(\sigma, x \for y) & = & (\sigma', M/y) & 
\mbox{where } \sigma' = [M/x]_A \sigma
%
\end{array}
\]


Next, we concentrate on eliminating possible redices which may have
been created in the case $[M/x]_A(x \cdot S)$ using the definition of
$\reduce(M:A, S)$. 

\[
\begin{array}{lcll}
\reduce (\lambda y.M : A_1 \arrow A_2, (N ; S)) & = & M''  &
\mbox{where } [N/y]_{A_1} M = M' \\
& & & \mbox{ and }  \reduce(M' : A_2, S) = M''\\\relax 
\reduce (R : P, \nil) & = & R \\ \relax
\reduce(M : A, S) & & \mbox{fails } & \mbox{otherwise}
\end{array}
\]

We first compute the
result of applying the substitution $[M/x]$ to the spine $S$ which
yields the spine $S'$. Second, we reduce any possible redices which
are created using the following definition.

Substitution may fail to be defined only if substitutions into the
subterms are undefined. The side conditions $y\not\in \FV(M)$ and $y
\neq x$ do not cause failure, because they can always be satisfied
by appropriately renaming $y$.
However, substitution may be  undefined if we try for example to
substitute an atomic term $R$ for $x$ in the term $x \cdot S$ where
the spine $S$ is non-empty. The substitution operation is well-founded
since recursive appeals to the substitution operation take place on
smaller terms with equal type $A$, or the substitution operates on
smaller types (see the case for $\reduce(\lambda y.M : A_1 \arrow A_2,
(N ; S))$). 

The first property states that the hereditary substitution operations
terminate, independently of whether the terms involved are well-typed
or not. The operation may fail if we have ill-typed terms, or yield a
canonical term as a result. 


\begin{theorem}[Termination]\mbox{}

 $[M/x]_A(N)$, $[M/x]_A R$, $[M/x]_A \sigma$, $\reduce(M:A, S)$ terminates, either by
  returning a result or failing after a finite number of steps.
\end{theorem}
\begin{proof}
  This can be verified by a nested induction, first on the structure
  of $A$, and second on the structure of the term we apply hereditary
  substitution to or the term $S$ we apply to $M:A$ in the case for $\reduce$. 
See \cite{Watkins02tr} or \cite{Nanevski:ICML05} for similar proofs in related calculi.
\end{proof}

\begin{theorem}[Substitution on Terms]\mbox{}\label{thm:substterm}
\begin{enumerate}
 \item If $\Delta ; \Gamma \vdash M \chk A$ and 
          $\Delta ; \Gamma,x{:}A,\Gamma' \vdash N \chk C$ and 
          $[M/x]_A N = N'$ \\ then 
          $\Delta ; \Gamma, \Gamma' \vdash N' \chk C$.
 \item If $\Delta ; \Gamma \vdash M \chk A$ and 
          $\Delta ; \Gamma,x{:}A,\Gamma' \vdash R \syn P$ and 
          $R' = [M/x]_A R$ \\ then 
          $\Delta ; \Gamma, \Gamma' \vdash R' \syn P$.

 \item If $\Delta ; \Gamma \vdash M \chk A$ and 
          $\Delta ; \Gamma,x{:}A,\Gamma' \vdash S > B \syn P$  and 
          $S' = [M/x]_A S$ \\ then
          $\Delta ; \Gamma, \Gamma' \vdash S' > B \syn P$.
%
 \item If $\Delta ; \Gamma \vdash M \chk A$ and 
          $\Delta ; \Gamma \vdash S > A \syn P$ \\ then
          $\reduce(M : A, S) = R$ and 
          $\Delta ; \Gamma \vdash R \syn P$.

 \item If $\Delta ; \Gamma \vdash M \chk A$ and $\Delta ;
\Gamma,x{:}A,\Gamma' \vdash \sigma \chk \Psi$ and $\sigma' = [M/x]_A \sigma$ 
\\ then $\Delta ; \Gamma,\Gamma' \vdash \sigma' \chk \Psi$.

\end{enumerate}
\end{theorem}
\begin{proof}
 By simultaneous induction on the definition of substitution, structure
 of the type $A$ occurring in the type annotation of the substitution
 $[M/x]_A$ or $\reduce(M:A, S)$ and the second derivation. Either we
 apply the substitution to a smaller term, or the type $A$ is
 decreasing or the second  derivation is decreasing. 
\end{proof}

\subsection{Simultaneous Substitutions}

Next we define simultaneous substitution $[\sigma]M$ and
$[\sigma]\tau$ by extending the ideas presented in the previous
section. The substitution is again hereditary. 
The simultaneous substitution is only total when the substitution $\sigma$ is
defined on all free variables in $M$ and $\tau$, respectively.  This
will be satisfied, because simultaneous substitution is only applied
when the assumptions of the theorem following this definition are
satisfied. Simultaneous substitutions commute with the term
constructors, as one would expect. Just as we annotated the
substitution $[M/x]_A$ with the type of the variable $x$ to ensure
termination of the hereditary substitution operation, 
we will annotate the simultaneous substitution $\sigma$ with its
domain. However, simultaneous substitution may contain substitutions
such as $x\for x$ and the type of $x$ may not always be available to
extend the context annotation (see the case for
$[\sigma]_{\psi}(\lam{y}{M})$). Fortunately, it suffices to carry an
approximation $\psi$ of its domain $\Psi$ where in fact the type for
variables which will be replaced by atomic terms can be omitted. For
example, given the simultaneous substitution 
$[x\for x, \lambda y.y / y]$ with domain $x{:}Q \arrow Q, y{:}P \arrow
P$ a valid approximation is $x{:}\_ ,  y{:}P \arrow P$. Allowing for
approximations of contexts simply allows us here to directly extend a
context with a declaration $x{:}\_$ where we do not know the type of $x$.
We only need the type for $y$, because only when we replace it with
$\lambda y.y$ a redex may be created, and we must rely on the
$\reduce$-operation to ensure that we return a canonical form. We
would like to stress that in practice when we implement substitution,
we do not need to carry this annotation $\psi$ and it does not need to
be calculated explicitely. 

\[ \begin{array}{lclp{77mm}}
 [\sigma]_{\psi}(\lam{y}{N}) & = & \lam{y}{N'}
     & where $N' = [\sigma, y\for y]_{\psi, y{:}\_}(N)$ \\
 & & & 
choosing $y \not\in \FV(\sigma), \dom(\sigma)$ \\ \relax
%
 [\sigma]_{\psi}(c \cdot S) & = & c \cdot S'
     & where $[\sigma]_{\psi}(S) = S'$ \\ \relax
 [\sigma]_{\psi}(x \cdot S) & = & R' 
     & where $[\sigma]_{\psi}(S) = S'$, $M/x \in \sigma$ and
     $x{:}A \in \psi$, \\
& & & and  $R' = \reduce (M : A, S')$ \\\relax
 [\sigma]_{\psi}(x \cdot S) & = & H \cdot S'
     & where  $H\for x \in \sigma$ and $[\sigma]_{\psi}(S) = S'$ \\ \relax
%
 [\sigma]_{\psi}(\clo{v}{\tau}) & = & \clo{v}{\tau'}
     & where $\tau' = [\sigma]_{\psi}(\tau)$ \\[0.5em]
%
 [\sigma]_\psi(\nil) & = & \nil  & \\ \relax
 [\sigma]_\psi(N ; S) & = & N' ; S' & where $N' = [\sigma]_\psi(N)$ and $S' = [\sigma]_\psi(S)$\\[0.5em] \relax
%

 [\sigma]_{\psi}(\cdot) & = & \cdot \\ \relax
 [\sigma]_{\psi}(\tau, N/y) & = & (\tau', N'/y)
     & where $\tau' = [\sigma]_{\psi}(\tau)$ and $N' = [\sigma]_{\psi}(N)$ \\ \relax
 [\sigma]_{\psi}(\tau, c\for y) & = & (\tau', c\for y)
     & where $\tau' = [\sigma]_{\psi}(\tau)$  \\ \relax
 [\sigma]_{\psi}(\tau, x\for y) & = & (\tau', H\for y)
     & where $\tau' = [\sigma]_{\psi}(\tau)$ and $(H\for x) \in \sigma$ \\ \relax
 [\sigma]_{\psi}(\tau, x\for y) & = & (\tau', M/y)
     & where $\tau' = [\sigma]_{\psi}(\tau)$ and $(M/x) \in \sigma$
%
\end{array} \]

The definition of simultaneous substitutions is a straightforward
extension of the ordinary substitution described earlier. 
Simultaneous substitutions satisfy the simultaneous substitution
principle. 


\begin{theorem}[Simultaneous Substitution on Terms]\mbox{}
\label{thm:simul-term}
\begin{enumerate}
\item If $\Delta ; \Gamma \vdash \sigma \chk \Psi$ and $\Delta ; \Psi
\vdash N \chk C$ and $[\sigma]_\psi N = N'$ then $\Delta ; \Gamma
\vdash N' \chk C$.
%
\item If $\Delta ; \Gamma \vdash \sigma \chk \Psi$ and $\Delta ; \Psi
\vdash R \syn P$ and $[\sigma]_\psi R = R'$ then $\Delta ; \Gamma
\vdash R \syn P$.
%
\item If $\Delta ; \Gamma \vdash \sigma \chk \Psi$ and $\Delta ; \Psi
\vdash S > A \syn P$ and $[\sigma]_\psi S = S'$ then \\ $\Delta ; \Gamma
\vdash S' > A \syn P$.
%
%
\item If $\Delta ; \Gamma \vdash \sigma \chk \Psi$ and $\Delta ; \Psi
\vdash \tau \chk \Theta$ then $\Delta ; \Gamma \vdash [\sigma]_\psi\tau \chk \Theta$.
\end{enumerate}
\end{theorem}
\begin{proof}
 By induction on the structure of the second given derivation and
 theorem \ref{thm:substterm} (4).
\end{proof}

%
Finally, we remark that composition of hereditary substitution is
written as $[\sigma]_\psi \tau$, and the standard composition
principles hold (see \cite{Nanevski:ICML05}). 
%
%
We emphasize that substitutions $\sigma$ are defined only on
ordinary variables $x$ and not modal variables $u$. Subsequently, we
write $\id_\Gamma$ for the identity substitution $(x_1 \for x_1, \ldots, x_n
\for x_n)$ for a context $\Gamma = (\cdot, x_1\oftp A_1, \ldots,
x_n\oftp A_n)$.   

\subsection{Contextual substitution}
Meta-variables $u[\sigma]$ give rise to new contextual substitutions,
which are only slightly more difficult than ordinary substitutions. To
understand contextual substitutions, we take a closer look at the
closure $\clo{u}{\sigma}$ which describes the meta-variable. Recall that the
substitution $\sigma$ which is associated with every meta-variable $u$
stands for a postponed substitution. As a consequence, we can apply
$\sigma$ as soon as we know which term $u$ should stand for. Moreover,
we require that meta-variables have base type $P$ and hence, we will
only substitute atomic objects for meta-variables. 

Finally because of $\alpha$-conversion, the variables that are
substituted at different occurrences of $u$ may be different.  As a
result, substitution for a meta-variable must carry a context, written
as $\msub{\Psihat.R/u}N$ and $\msub{\Psihat.R/u}\sigma$ where
$\Psihat$ binds all free 
variables in $R$.  This complication can be eliminated in an implementation
of our calculus based on de Bruijn indexes. 
In general, we must again ensure that the result is a canonical term,
and we will define contextual substitution hereditarily following the
ideas for hereditary ordinary substitutions. Just as we annotated the
substitution $[M/x]_A$ with the type of the variable $x$, we will
annotate the contextual substitution $\msub{\Psi.R/u}_{P[\Psi]}$ with the
type of the meta-variable $P[\Psi]$. We will abbreviate $P[\Psi]$ with
$\alpha$ for better readability. 


%
\[ \begin{array}{lcll}
%
 \lbb \Psihat.R/u\rbb_\alpha (\lam{y}{N}) & = & \lam{y}{N'} &
\mbox{where } N' = \lbb \Psihat.R/u\rbb_\alpha N\\ \relax
%
 \lbb \Psihat.R/u\rbb_\alpha(c \cdot S) & = & c \cdot S' &
 \mbox{where } S' = \lbb \Psihat.R/u\rbb_\alpha S\\\relax
%
 \lbb \Psihat.R/u\rbb_\alpha (x \cdot S) & = & x \cdot S' & \mbox{where
 } S' =  \lbb \Psihat.R/u\rbb_\alpha S\\ \relax
\lbb \Psihat.R/u\rbb_\alpha (\clo{u}{\tau}) & = & R' & \mbox{where }
 \tau' = \lbb \Psihat.R/u\rbb_\alpha \tau \mbox{ and } R' = [\tau'
 /\Psi]_{\psi} R
 \\ 
%
%
 \lbb \Psihat.R/u\rbb_\alpha (\clo{v}{\tau}) & = & \clo{v}{\tau'} & \mbox{where } \tau' = \lbb\Psihat.R/u\rbb_\alpha \tau 
%
%
 \mbox{ and provided $v \neq u$ }  \\[1ex]
\lbb \Psihat.R/u\rbb_\alpha (\nil) & = & \nil  & \\ \relax
 \lbb \Psihat.R/u\rbb_\alpha(N ; S) & = & N' ; S' & \mbox{where}\; N' = \lbb \Psihat.R/u\rbb_\alpha N\;\mbox{and}\; S' = \lbb \Psihat.R/u\rbb_\alpha S
\\[0.5em] \relax
 \lbb \Psihat.R/u\rbb_\alpha (\cdot) & = & \cdot & \\  \relax
 \lbb \Psihat.R/u\rbb_\alpha (\tau, N/y) & = &  \tau', N'/y & \mbox{where }
 \tau' = \lbb\Psihat.R/u\rbb_\alpha \tau \mbox{ and } N' = \lbb \Psihat.R/u\rbb_\alpha N\\
 \lbb \Psihat.R/u\rbb_\alpha (\tau, H\for y)_\alpha & = & \tau', H\for y & \mbox{where }
 \tau' = \lbb\Psihat.R/u\rbb_\alpha \tau 
\end{array} \]  

%%
Applying $\lbb \Psihat.R / u\rbb$ to the closure $\clo{u}{\tau}$ first
obtains the simultaneous substitution $\tau' = \lbb \Psi. R/u\rbb \tau$,
but instead of returning $\clo{R}{\tau'}$, it proceeds to eagerly
apply $\tau'$ to $R$. Before $\tau'$ can be carried out, however, its
domain must be renamed to match the variables in $\Psi$, denoted by
$\tau'/\Psi$.  For example, when $\tau' = (M_1/x_1,\ldots,M_n/x_n)$
and $\Psi = (y_1{:}A_1, \ldots, y_n{:}A_n)$ 
then we will rename the domain of the substitution $\tau'$ by writing
$\tau'/\Psi = (M_1/y_1, \ldots, M_n/y_n)$. 



We note that maintaining canonical forms is easy since
we enforce that every occurrence of a meta-variable must have base type.
%
While the definition of the discussed case may seem circular at first,
it is actually well-founded.  The computation of $\tau'$ recursively
invokes $\lbb\Psihat.R/u \rbb$ on $\tau$, a constituent of $\clo{u}{\tau}$.
Then $\tau'/\Psi$ is applied to $R$, but applying simultaneous
substitutions has already been defined without appeal to meta-variable
substitution. 


Substitution of a meta-variable satisfies the following contextual
substitution property.  


\begin{theorem}[Contextual Substitution on Terms] \mbox{}
\begin{enumerate}
 \item If $\Delta ; \Psi \vdash R \chk P$ and $(\Delta, u{::}P[\Psi], \Delta') ;
\Gamma \vdash N \chk C$  and $\alpha = P[\Psi]$ \\ and  $\lbb \Psihat.R/u\rbb_\alpha N = N'$
then $(\Delta, \Delta') ; \Gamma \vdash  N' \chk C$.
 \item If $\Delta ; \Psi \vdash R \chk P$ and $(\Delta, u{::}P[\Psi], \Delta') ;
\Gamma \vdash R' \syn P'$ and $\alpha = P[\Psi]$ \\ and $\lbb \Psihat.R/u\rbb_\alpha R' = R''$ 
then $(\Delta, \Delta') ; \Gamma \vdash  R'' \syn P'$.
%
 \item If $\Delta ; \Psi \vdash R \chk P$ and $(\Delta, u{::}P[\Psi], \Delta') ;
\Gamma \vdash S > A \syn P'$ and $\alpha = P[\Psi]$ \\ and $\lbb \Psihat.R/u\rbb_\alpha S = S'$ 
then $(\Delta, \Delta') ; \Gamma \vdash  S' > A \syn P'$.
%
 \item If $\Delta ; \Psi \vdash R \chk P$ and $(\Delta, u{::}P[\Psi],
\Delta') ; \Gamma \vdash \tau \chk \Theta$ and $\alpha = P[\Psi]$\\ and $\tau' = \lbb \Psihat.R/u\rbb_\alpha \tau$
then $(\Delta, \Delta') ; \Gamma \vdash \tau' \chk \Theta$.
\end{enumerate}
\end{theorem}
\begin{proof}
 By simple inductions on the second given derivation, appealing
to Theorem~\ref{thm:simul-term} in the case for meta-variables. 
\end{proof}

\subsection{Simultaneous contextual substitution}
Just as we extended ordinary substitutions to simultaneous
substitutions, we extend contextual substitution to a simultaneous
contextual substitution. 


\[ \begin{array}{rrcl}
 \mbox{Simultaneous contextual substitutions} & \theta & \bnfas & \cdot \bnfalt \theta,
 \Psihat.R/u 
\end{array}
\]

We write $\theta$ for a simultaneous substitution $\msub{\Psihat_1.R_1/u_1,
  \ldots, \Psihat_n.R_n/u_n}$.
%
We first define typing rules for simultaneous contextual
substitutions.


\[ \begin{array}{c}
 \infer[]
       {\Delta \vdash (\cdot) \chk (\cdot)}
       {\mathstrut}
%
\hspace{1cm}
 \infer[]
       {\Delta  \vdash (\theta, \Psihat.R/u) \chk (\Delta', u{::}P[\Psi])}
       {\Delta ; \Psi \vdash R \chk P
        &
        \Delta \vdash \theta \chk \Delta'}
\end{array} \]


The new operation of substitution is compositional, but two
interesting situations arise: when a variable $u$ is encountered, and
when we substitute into a lambda-abstraction. We again annotate
the simultaneous contextual substitution  $\msub{\theta}_\Delta$ with
its domain.

\[ \begin{array}{lcll}
% 
 \msub{\theta}_\Delta (\lam{y}{N}) & = & \lam{y}{N'} & \mbox{where } N' =
 \msub{\theta}_\Delta N 
\\[0.5em] \relax
%
 \msub{\theta}_\Delta (c \cdot S) & = & c \cdot S' & \mbox{where } S' =
 \msub{\theta}_\Delta S\\ \relax
 \msub{\theta}_\Delta (x \cdot S) & = & x \cdot S' & \mbox{where } S'
 = \msub{\theta}_\Delta S\\ \relax
 \msub{\theta}_\Delta (u[\sigma]) & = & R' & 
\mbox{where } \theta = (\theta_1, \Psihat.R/u, \theta_2)\; \mbox{and }
\sigma' = \msub{\theta}_\Delta (\sigma) \\
& & & \mbox{and } R' = [\sigma']_\psi R\; \mbox{where}\;u{::}P[\Psi]
\in \Delta\\[0.5em]
%
 \msub{\theta}_\Delta (\nil) & = & \nil & \\ \relax
 \msub{\theta}_\Delta (N ; S) & = & (N' ; S') & \mbox{where } N'
 = \msub{\theta}_\Delta N\; \mbox{and}\; S'
 = \msub{\theta}_\Delta S\\[0.5em] \relax
%
\msub{\theta}_\Delta (\cdot) & = & \cdot & \\
 \msub{\theta}_\Delta (\sigma, N/y) & = & (\sigma', N'/y) & 
\mbox{where } \sigma' = \msub{\theta}_\Delta \sigma \mbox{ and } N' =
\msub{\theta}_\Delta N \\ \relax
 \msub{\theta}_\Delta (\sigma, H \for y)\mbox{\hspace{0.5cm}} & = & (\sigma' , H\for y) &
 \mbox{where } \sigma' = \msub{\theta}_\Delta \sigma \\[1em]%\relax
\end{array}
\]

We remark that the rule for substitution into a
lambda-abstraction does not need to extend the substitution
$\theta$ nor does it need any other restrictions. This is because the
object $R$ is defined in a different context, which is accounted for
by the explicit substitution stored at occurrences of $u$. Finally,
consider the case of substituting into a closure, which is the
critical case of this definition.  

\[ \begin{array}{lcll}
 \msub{\theta}_\Delta (u[\sigma]) & = & R' &
\mbox{where } \theta = (\theta_1, \Psihat.R/u, \theta_2)\;
\mbox{and } \sigma' = \msub{\theta}_\Delta(\sigma) \\
& & &  
\mbox{and } R' = [\sigma']_\psi R \; \mbox{where}\;u{::}P[\Psi]
\in \Delta
\end{array} \]

 This is clearly well-founded, because $\sigma$ is a subexpression
(so $\lbb \Psihat.R/u\rbb\sigma$ will terminate) and the application of an ordinary
substitution has been defined previously without reference to
the new form of substitution. 
%
Similar to composition of ordinary substitution,
composition for contextual substitutions holds (see \cite{Nanevski:ICML05}).


\subsection{Pattern substitutions}
An important fragment of higher-order terms, is the pattern
fragment. While in general many algorithms such as  unification are
undecidable in the general higher-order case, these operations become
decidable with suitable restrictions to patterns
\cite{Miller91jlc}. Higher-order patterns are terms where
meta-variables must be applied to some distinct bound variables.  
In our setting, this means that  substitution $\sigma$ which is associated
with the meta-variable $u[\sigma]$ must be a pattern
substitution of the form  $[x_{\phi(1)} \for x_1, \ldots,
x_{\phi(n)} \for x_n]$. In other words the pattern substitution is just a
renaming of some variables. 

When we consider only closures of meta-variables together with pattern
substitutions then applying the contextual substitution $\theta$ to a term
$M$ will directly yield a canonical term and it is unnecessary to
annotate $\msub{\theta} M$ with the domain of $\theta$. In the
subsequent development, we therefore omit this annotation.

Finally, we note that applying a contextual substitution $\theta$ to a
pattern substitution $\sigma$ does not change $\sigma$ itself, since
the range of $\sigma$ refers only to bound variables, while $\theta$
refers to meta-variables. 

\begin{lemma}\label{lemma:modSubPatSub}\mbox{}\\
If $\Delta' \vd \theta \chk \Delta$ and $\sigma$ is a pattern
substitution, s.t. $\Delta; \Gamma \vd \sigma \chk \Psi$ then 
$\msub{\theta}_\Delta(\sigma) = \sigma$. 
\end{lemma}
\begin{proof}
Induction on the structure of $\sigma$.
\end{proof}

To keep the algorithms for insertion and retrieval similar to the
first-order setting and achieve efficient implementations, we will
subsequently concentrate on linear higher-order patterns. 
Linear higher-order patterns enforce two conditions: First, they not
only guarantee that every meta-variable is associated with \emph{some
distinct bound variables}, but with \emph{all bound variables in whose
scope the meta-variable occurs in}. If the meta-variable $u[\sigma]$ occurs
in the context $\Psi$, then $\sigma$ is a substitution with domain and
range $\Psi$. This restriction ensures that we can avoid expensive
bound variable checks when computing instantiations for the
meta-variable $u$. We will write $\pi_\Gamma$ for a pattern
substitution. Second, we ensure that every meta-variable occurs only
once in a given term. This criteria ensures that we can avoid the
occurs check when we retrieve unifiable terms, and leads in general to 
simpler algorithms.  

\section{Formalizing higher-order substitution trees}\label{sec:thost}

Higher-order substitution trees are designed for linear higher-order
patterns and are built with contextual substitutions. Recall the
example given earlier, where we described equality preserving
transformations on logical propositions. One such transformation was
the following: 

\[
\eqLF\;\;  (\orLF  \;\;(\forallLF \lambda x. A \;x) \; B )\;\;\; 
                   (\forallLF \lambda \tt{x}. (\orLF \; (A\; x)\;  B)).
\]

In this example, {\tt A} and {\tt B} denote meta-variables which are present
in the original query, while {\tt x} denotes an ordinary bound
variable. In our contextual modal type theory, this term would be
represented as follows:


\[
\begin{array}{lclclcl}
\eqLF & \cdot &   ((\orLF  & \cdot &  ((\forallLF \cdot ((\lambda
x. u[x \for y])\;\;;\;\;\nil)) & ; & \texttt{v}[\cdot]\;\;;\;\;\nil))\;;\\
 & & \;(\forallLF & \cdot & ((\lambda \tt{x}. (\orLF \cdot (u[x \for y]\;\;;\;\;
 v[\cdot]\;\;;\;\;\nil))) & ;& \nil))\\
& & \; \nil) & \\[0.5em] \relax
\end{array}
\]


The meta-variables $\tt{u}[x \for y]$ and ${\tt v}[\cdot]$
directly encode the 
dependencies which must be obeyed. The type of ${\tt u}$ is
${\tt{prop}}[\tt{x:i}]$ while the type of ${\tt v}$ is ${\tt{prop}}[.]$.
As we can see, the meta-variable {\tt v}$[\cdot]$ is not fully applied
in the term  
$(\lambda \tt{x}. (\orLF \cdot (u[x \for y]\;\;;\;\;v[\cdot]\;\;;\;\;\nil)))$ 
because  the substitution associated
with the meta-variable {\tt v} is empty although {\tt v}$[\cdot]$ occurs
within the scope of a lambda-binder. Moreover, the meta-variable
$\tt{u}[x \for y]$ occurs twice in this term. Hence we translate this
term into a linear higher-order pattern:

\[
\begin{array}{lclclcl}
\eqLF & \cdot &   ((\orLF  & \cdot &  ((\forallLF \cdot ((\lambda
x. u[x \for y])\;\;;\;\;\nil)) & ; & \texttt{v}[\cdot]\;\;;\;\;\nil))\;;\\
 & & \;(\forallLF & \cdot & ((\lambda \tt{x}. (\orLF \cdot (w_1[x \for y]\;\;;\;\;
 w_2[x \for y]\;\;;\;\;\nil))) & ;& \nil))\;\;;\;\;\\
& &  \nil) & \\[0.5em] \relax
& & \multicolumn{5}{r}{\mbox{where}\;\forall x\,.\,\tt{w_1[x \for y] \unif u[x \for y]}\;\; \wedge\;\;\forall x\,.\, \tt{w_2[x \for y] \unif v[\cdot]}
  }
\end{array}
\]

When computing the most specific
generalization between two terms to build the substitution
tree, we will create internal meta-variables. For example,
{\tt i}$_3[\cdot]$ and {\tt i}$_4[\cdot]$ are internal meta-variables in 


\[
\begin{array}{lclcl}
\eqLF & \cdot &   ((\orLF  & \cdot &  (\texttt{i}_3[\cdot] \;\; ; \;\; \texttt{i}_4[\cdot]\;\;;\;\;\nil))\;;\\
 & & \;(\forallLF & \cdot & ((\lambda x. (\orLF \cdot (w_1[x \for y]\;\;;\;\;
 w_2[x \for y]\;\;;\;\;\nil))) \;\; ; \;\; \nil)) \;\;; \;\;\\
& & \;\nil)
\end{array}
\]


In the definition of higher-order substitution trees we will distinguish
between a modal context $\Delta$ which denotes the original  
meta-variables such as $\tt u$, $\tt v$, and $\tt w$, a modal
context $\Omega$ for the internal meta-variables $\tt i_3$ and
$\tt i_4$, and a context $\Gamma$ denoting ordinary
variables. A higher-order substitution tree is an ordered n-ary tree.

\begin{enumerate}
\item A node with a contextual substitution $\rho$  such
  that  $\Delta \vd  \rho \chk \Omega$ and no children is called a
  leaf and is a tree.
\item If  $N_1,\ldots, N_n$ are trees such that for every $i$, $N_i$
  has a substitution $\rho_i$, such that  $(\Delta, \Omega_i) \vd 
  \rho_i \chk \Omega$, and a list of children $C_i$, \\
  then a node with a contextual substitution $\rho$, such that
  $(\Delta, \Omega) \vd \rho \chk   \Omega'$, and children
  $N_1,\ldots, N_n$  is a tree. 
\end{enumerate}

For every path from the top node
$\rho_0$ where $(\Delta, \Omega_1) \vd \rho_0 \chk \Omega_0$ to
the leaf node $\rho_n$, we have $\Delta \vd
\msub{\rho_n}(\msub{\rho_{n-1}}\ldots\rho_0) \chk \Omega_0$. In
other words, there are no internal meta-variables left 
after we compose all the substitutions $\rho_n$ up to 
$\rho_0$.  We assume that all meta-variables occurring in one path are
unique, and are fully applied, i.e. every meta-variable $u{::}P[\Psi]$
where $\Psi = x_1{:}A_1, \ldots, x_n{:}A_n$ is applied to all the
bound variables in $\Psi$. 
%
%
More formally we can define substitution trees as follows: \label{def:tree}

\[
\begin{array}{lcl}
\mbox{Node N} & \bnfas & (\Omega \turn \rho  \tto C)\\
\mbox{Children C} & \bnfas & [N , C] \bnfalt \nil
\end{array}
\]    

A tree is a node $N$ with a contextual substitution $\rho$ and a list
of children $C$. If the list of children is empty, we have reached a leaf.
In general, we will write $\Delta \vd N \hastype
\Omega'$ where $N = (\Omega \turn \rho \tto C)$ which means that 
$(\Delta, \Omega) \vd \rho \chk \Omega'$ and all the children $N_i$
in $C$, $\Delta \vd N_i \hastype \Omega$.
%
To characterize, well-formed substitution trees we employ the following judgments:

\[
\begin{array}{lp{9cm}}
\Delta \vdash N : \Omega & \mbox{Node $N$ is a valid substitution tree with domain $\Omega$}\\
\Delta \vdash C : \Omega & \mbox{The children $C$ are valid substitution trees with domain $\Omega$}
\end{array}
\]

We can now formalize the invariants about the domains and range of
substitutions occurring in the nodes of the substitution trees. The
rule $\mathsf{Leaf}$ is a special, but important, case of the rule
$\mathsf{Node}$. 

\begin{small}
\[
\begin{array}{c}
%
  \infer[\mathsf{Leaf}]{\Delta \vdash N : \Omega}{
  N = \cdot \turn \rho \tto \nil & 
  \Delta \vdash \rho \chk \Omega}
\\[1em]
  \infer[\mathsf{Node}]{\Delta \vdash N : \Omega}{
  N = \Omega_0 \turn \rho \tto C & C \neq \nil & 
  \Delta , \Omega_0 \vdash \rho \chk \Omega & 
  \Delta \vdash C : \Omega_0}
\\[1em]
% 
\infer[\mathsf{Empty}]{\Delta \vdash \nil : \Omega}{} 
\hspace{1cm}
\infer[\mathsf{Children}]{\Delta \vdash [N ; C] : \Omega}{
  \Delta \vdash N : \Omega & 
  \Delta \vdash C : \Omega
}
\end{array}
\]
\end{small}


Note that there are no typing dependencies among the variables in
$\Omega$ and they can be arbitrarily re-ordered. Moreover, we point
out that while it is convenient to consider the simultaneous contextual
substitution $\rho_i$ in the theory, in practice we only carry the
mappings which are not the identity.

The algorithms for insertion and retrieval in substitution trees are 
based on the most specific linear generalization (mslg) and matching.
Types themselves do not play a role when computing the mslg and
matcher. However, we assume the term is well-typed before 
it is inserted into the substitution tree, and we will show that
the term can be decomposed into contextual substitutions such that
their composition results in the original term. 


\section{Insertion}\label{sec:generalization}
Insertion of a term $R$ into the index is viewed as insertion of the
substitution $\Psihat.R/i_0$. Assuming that $R$ has type $P$ in a modal context
$\Delta$ and a bound variable context $\Psi$. $\Psihat.R/i_0$ is a contextual
substitution such that $\Delta \vd \Psihat.R/i_0 \chk i_0\ofvd
P[\Psi]$. 
%
This will simplify the following theoretical development. 
The insertion process works by following down a path in the tree that is  {\em compatible} with the contextual substitution $\rho$. To formally define insertion, we first
describe the most specific linear generalization of two objects, and
then show how to compute the most specific linear generalization (mslg) of two
contextual substitutions.

\subsection{Most specific generalization of two linear objects}
Computing the most specific linear generalization of two contextual 
substitutions relies on finding the most specific linear
generalization of two objects. Recall that we require 
that all objects are linear higher-order patterns and are in canonical
forms. Moreover, we assume that all meta-variables are lowered
and have base type. We define the computation of the most specific
linear generalization of two terms next.

\[
\begin{array}{lclll}
(\Delta, \Omega); \Gamma \vd & M_1 \aunif M_2 & \hastype A &
 \ares  M / (\Omega',\;\theta_1, \theta_2) & 
 \;\;M \mbox{ is the mslg of } M_1 \mbox{ and } M_2\\ % [1em]
(\Delta, \Omega); \Gamma \vd & R_1 \aunifR R_2 & \hastype P &
 \ares  R / (\Omega',\;\theta_1, \theta_2) & 
 \;\;R \mbox{ is the mslg of } R_1 \mbox{ and } R_2\\% [1em]
(\Delta, \Omega); \Gamma \vd & S_1 \aunifS S_2 & \hastype A > P & 
\ares S / (\Omega',\;\theta_1, \theta_2) & 
 \;\;S \mbox{ is the mslg of } S_1 \mbox{ and } S_2
\end{array}
\]  


If the canonical terms $M_1$ and $M_2$ have type $A$ in modal context $(\Delta,
\Omega)$ and bound variable context $\Gamma$, then $M$ is the most
specific linear generalization of $M_1$ and $M_2$ such that
$\msub{\theta_1}M$ is equal to $M_1$ and
$\msub{\theta_2}M$ is equal to $M_2$. Moreover, $\theta_1$
and $\theta_2$ are contextual substitutions which map meta-variables from
$\Omega'$ to the modal context $(\Delta, \Omega)$. Finally, $(\Delta,
\Omega') ; \Gamma \vd M \chk A$. Similar invariants hold for atomic
terms and spines.
%

We think of $M_1$ ($R_1$, or $S_1$) as an object which is already in the index
and $M_2$ ($R_2$, or $S_2$) is the object to be inserted. As a consequence,
only $M_1$ ($R_1$, and $S_1$) may refer to the internal variables in 
$\Omega$, while $M_2$ ($R_2$, and $S_2$) only depends on $\Delta$.  
In defining the most specific linear generalization, we distinguish
between the internal meta-variables $i$ and the global
meta-variables $u$ in the rules, because they play different roles. The
inference rules for computing the mslg are given in Figure \ref{fig:lmsg}.  

% 
\begin{figure}
  \centering
\[\begin{array}{c} \mbox{Normal linear objects\hspace{9cm}}\\[0.5em]
\infer[{\textsf{a-lam}}]{(\Delta, \Omega); \Gamma \vd \lam{x}{M_1}
\aunif \lam{x}{M_2} \hastype A_1 \arrow A_2 \ares \lam{x}{M} /(\Omega',\;\theta_1, \theta_2)}{% 
  (\Delta ,\Omega); \Gamma, x\oftp A_1 \vd M_1 \aunif M_2  \hastype
  A_2 \ares M /  (\Omega',  \theta_1, \theta_2)}
 \\[0.75em]
%
\infer[{\textsf{a-coe}}]{(\Delta, \Omega); \Gamma \vd R_1 
\aunif R_2 \hastype P \ares R /(\Omega',\;\theta_1, \theta_2)}{% 
  (\Delta, \Omega); \Gamma \vd R_1 \aunifR R_2  \hastype P \ares R /
  (\Omega',  \theta_1, \theta_2)}
\\[0.75em]
\mbox{Atomic linear objects\hspace{9cm}} \\
\infer[{\textsf{a-mvar-same}}]{(\Delta, \Omega); \Psi \vd u[\pi_\Psi] \aunifR u[\pi_\Psi]
  \hastype P \ares u[\pi_\Psi]/ (\cdot, \cdot, \cdot)}{u\ofvd P[\Psi]) \in \Delta} 
\\[0.75em]
\infer[{\textsf{a-mvar-diff-1}}]{(\Delta, \Omega); \Psi \vd u[\pi_\Psi] \aunifR R \hastype
  P \ares i[\id_\Psi]/  (i\ofvd P[\Psi], \;\Psihat.u[\pi_\Psi]/i, \;\Psihat.R/i)}{u\ofvd P[\Psi] \in \Delta & i {\text{ must be new}} & R \neq u[\pi_\Psi]} 
\\[0.75em]
\infer[{\textsf{a-mvar-diff-2}}]{(\Delta, \Omega); \Psi \vd R \aunifR u[\pi_\Psi] \hastype P \ares i[\id_\Psi]/
  (i\ofvd P[\Psi], \;\Psihat.R/i, \;\Psihat.u[\pi]/i)}{u\ofvd P[\Psi] \in \Delta &
   R\neq i_0[\id_\Psi] \mbox{ for some $i_0$} & R \neq u[\pi] & \mbox{
     $i$ must be new}  } 
\\[0.75em]
\infer[{\textsf{a-ivar}}]{(\Delta, \Omega); \Psi \vd i[\id_\Psi] \aunifR R \hastype
  P \ares i[\id_\Psi]/  (i\ofvd P[\Psi],
  \;\Psihat.i[\id_\Psi]/i, \;\Psihat.R/i)}{i\ofvd P[\Psi] \in \Omega} 
\\[0.75em]
\infer[{\textsf{a-var}}]{(\Delta, \Omega); \Psi \vd x \cdot S_1 \aunifR x\cdot S_2
  \hastype P \ares x \cdot S / (\Omega', \theta_1, \theta_2)}{
(\Delta, \Omega); \Psi \vd S_1 \aunifS  S_2 \hastype A > P
\ares S / (\Omega', \theta_1, \theta_2) & x{:}A \in \Psi }
%
\\[0.75em]
\infer[{\textsf{a-con}}]{(\Delta, \Omega); \Psi \vd c \cdot S_1 \aunifR c\cdot S_2
  \hastype P \ares c \cdot S / (\Omega', \theta_1, \theta_2)}{
(\Delta, \Omega); \Psi \vd S_1 \aunifS  S_2 \hastype A > P
\ares S / (\Omega', \theta_1, \theta_2) & c{:}A \in \Sigma }
\\[0.75em]
\infer[{\textsf{a-diff}}]{(\Delta, \Omega); \Psi \vd R_1 \aunifR R_2 \hastype P \ares i[\id_\Psi]/
  ((i\ofvd P[\Psi]), \Psihat.R_1/i, \Psihat.R_2 /i))}{H_1 \cdot
  S_1 = R_1 & R_2 = H_2 \cdot S_2 &  H_1 \neq H_2  & i {\text{ must be new}}} 
\end{array}
\]


\[
\begin{array}{c}
\mbox{Normal linear spines\hspace{10cm}}\\[0.5em]
\infer[{\textsf{a-nil}}]{(\Delta, \Omega); \Psi \vd \nil \aunifS \nil \hastype P > P
  \ares \nil 
  / (\cdot, \cdot, \cdot)}{} 
\\[0.75em]
\infer[{\textsf{a-cons}}]{(\Delta, \Omega); \Psi \vd (M_1 ; S_1) \aunifS (M_2 ; S_2)
  \hastype A_1 \arrow A_2 > P  \ares (M ; S) / (\Omega', \theta, \theta')}{% 
  \begin{array}{lllllr}
(\Delta, \Omega); \Psi  \vd  M_1 & \aunif  & M_2 & \hastype A_1 & \ares
M  / (\Omega_1,\;\theta_1, \theta_2) & \\
  (\Delta, \Omega); \Psi  \vd  S_1 & \aunifS &  S_2 & \hastype A_2 >
   P & \ares S  /  (\Omega_2,\;\theta_1', \theta_2') & \\
\multicolumn{6}{l}{
\mbox{and } \Omega' = (\Omega_1, \Omega_2) \quad \theta =
   (\theta_1, \theta'_1) \quad \theta' = (\theta_2, \theta'_2)
}
  \end{array}
 } \\
\end{array}
\]
\caption{Linear most specific generalization}
\label{fig:lmsg}
\end{figure}

In the rule for lambda, we do not need to worry about capture,
since meta-variables and bound variables are defined in different
context. Hence, we can just traverse the body of the lambda-term.
%
Rule {\textsf{a-mvar-same}} treats the case where both terms are meta-variables. Note that we require that both meta-variables must
be the same and their associated substitutions must also be equal. 
In the rule $\textsf{a-mvar-diff-1}$ and $\textsf{a-mvar-diff-2}$, we
just create the substitution $\Psihat.u[\pi_\Psi]/i$. In general, we
would need to create $\inv{[\id_\Psi]}(u[\pi_\Psi])$, but since we know
that $\pi$ is a permutation substitution, we know that
$\inv{[\id_\Psi]}(\pi)$ always exists. In addition, the inverse
substitution of the identity is the identity. 

The different roles of meta-variables $u$ and internal
meta-variables $i$ becomes clear in the given rules. In
{\textsf{a-mvar-diff-1}} and {\textsf{a-mvar-diff-2}} we pick a new
internal meta-variable $i$ while we re-use the internal 
meta-variable $i$ in rule {\textsf{a-ivar}}. If we encounter a meta-variable $u$
and another object $R$ then we generalize and generate a new internal
meta-variable $i$. However, when we encounter an internal
meta-variable $i$ and another object R, we do not generate a new
internal meta-variable, because $i$ will be defined later on in the
branch of the substitution tree, and we will need to continue to
insert $R$ into the tree.  This is important for
maintaining the invariant that any child of $(\Delta, \Omega_2) \vd
\rho \chk \Omega_1$ has the form $(\Delta, \Omega_3) \vd \rho' 
\chk  \Omega_2$ during insertion (see the insertion algorithm later
on). 

In rule {\textsf{a-var}}, {\textsf{a-con}}, and {\textsf{a-diff}}, we
distinguish on the head symbol $H$ and compute the most specific
linear generalization of two objects $H_1\cdot S_1$ and  $H_2\cdot
S_2$. If $H_1$ and $H_2$ are not equal, then  we generate a new
internal meta-variable $i[\id_\Psi]$ together  with the
substitutions $\Psihat.(H_1 \cdot S_1)/i$ and $\Psihat. (H_2 \cdot 
 S_2)/i$ (see {\textsf{a-diff}} rule). Otherwise, we traverse the
 spines $S_1$ and $S_2$ and compute  the most specific linear
 generalization of them (see rules {\textsf{a-var}} and
 {\textsf{a-con}}). Finally, the rules for computing  the most
 specific generalization of two spines are straightforward. We
 compute the mslg of all the sub-expressions, and just  combine the
 substitution $\theta_1$ and $\theta'_1$ and $\theta_2$ and
 $\theta'_2$ respectively. As we require that all meta-variables occur
 uniquely, there are no dependencies among 
 $\Omega_1$ and $\Omega_2$.  

\begin{definition}[Compatibility of atomic objects]\mbox{}\\
  If $(\Delta, \Omega) ; \Psi \vd R_1 \aunifR R_2 \hastype P \ares
  i[\id_\Psi] / (i\ofvd P[\Psi], \Psihat.R_1/ i, \Psihat.R_2/i)$, then
two atomic objects $R_1$ and $R_2$ are called incompatible. Otherwise, we call
$R_1$ and $R_2$ compatible. 
\end{definition}

In other words, we call two terms compatible, if they share at least
the head symbol or a lambda-prefix. We are now ready to prove
correctness of the algorithm for computing the most specific linear
generalization of linear higher-order patterns.


\begin{theorem}[Soundness of mslg for objects]\label{lemma:mslgTermSound}\mbox{}
  \begin{enumerate}
  \item If $(\Delta, \Omega); \Gamma \vd M_1 \aunif M_2 \hastype A \ares M
/ (\Omega', \theta_1, \theta_2)$ and\\
\mbox{\hspace{0.3cm}}
$(\Delta, \Omega); \Gamma \vd M_1 \chk A$ and 
   $(\Delta, \Omega); \Gamma \vd M_2 \chk A$ \\
then $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and 
     $(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ and \\
\mbox{\hspace{0.7cm}}
$ M_1 = \msub{\theta_1}M$
and $M_2 = \msub{\theta_2}M$  and $(\Delta, \Omega');
\Gamma \vd M \chk A$. 
%
  \item If $(\Delta, \Omega); \Gamma \vd R_1 \aunifR R_2 \hastype P \ares R
/ (\Omega', \theta_1, \theta_2)$ and\\
\mbox{\hspace{0.3cm}}
$(\Delta, \Omega); \Gamma \vd R_1 \syn P$ and 
   $(\Delta, \Omega); \Gamma \vd R_2 \syn P$ \\
then $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and 
     $(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ and \\
\mbox{\hspace{0.7cm}}
$ R_1 = \msub{\theta_1}R$
and $R_2 = \msub{\theta_2}R$  and $(\Delta,\Omega');
\Gamma \vd R \syn P$.
%
\item If $(\Delta, \Omega); \Gamma \vd S_1 \aunifS S_2 \hastype A
  > P \ares S / (\Omega', \theta_1, \theta_2)$ and \\
\mbox{\hspace{0.3cm}}
$(\Delta, \Omega); \Gamma \vd S_1 > A \syn P$ and 
   $(\Delta, \Omega); \Gamma \vd S_2 > A \syn P$ \\
then $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and 
$(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ and \\
\mbox{\hspace{0.7cm}}
$(\Delta, \Omega'); \Gamma \vd S > A \syn P$ 
and $S_1 = \msub{\theta_1}S$ and $S_2 = \msub{\theta_2}S$.
  \end{enumerate}
\end{theorem}
%
%
\begin{proof}
  Simultaneous induction on the structure of the first derivation. 
\end{proof}

Next, we prove completeness. 

%
\begin{theorem}[Completeness of mslg of terms]\label{lemma:mslgTermComplete}\mbox{}
\begin{enumerate}
\item If $\Delta, \Omega \vd \theta_1 \chk \Omega'$ and 
      $\Delta, \Omega \vd \theta_2 \chk \Omega'$ and 
  $\theta_1$ and $\theta_2$ are incompatible and \\
  $\Delta, \Omega ; \Gamma \vd M_1 \chk A$,   $\Delta ; \Gamma \vd M_2 \chk A$, and
  $\Delta, \Omega' ; \Gamma \vd M \chk A$ and \\
  $M_1 = \msub{\theta_1}M$ and $M_2 = \msub{\theta_2}M$\\
then there exists a contextual substitution $\theta^*_1$, $\theta^*_2$, and
a modal context $\Omega^*$, such that 
$(\Delta, \Omega) ; \Gamma \vd M_1 \aunif M_2 \hastype A \ares M / (\Omega^*, \theta^*_1, \theta^*_2)$
and $\theta^*_1 \subseteq \theta_1$,  $\theta^*_2 \subseteq \theta_2$ and $\Omega^* \subseteq \Omega'$.
%
\item If $\Delta, \Omega \vd \theta_1 \chk \Omega'$ and 
      $\Delta, \Omega \vd \theta_2 \chk \Omega'$ and 
  $\theta_1$ and $\theta_2$ are incompatible and \\
  $\Delta, \Omega ; \Gamma \vd R_1 \syn P$,   $\Delta ; \Gamma \vd R_2 \syn P$, and
  $\Omega', \Delta ; \Gamma \vd R \syn P$ and \\ 
  $R_1 = \msub{\theta_1}R$ and $R_2 = \msub{\theta_2}R$\\
then there exists a contextual substitution $\theta^*_1$, $\theta^*_2$, and
a modal context $\Omega^*$, such that 
$(\Delta, \Omega) ; \Gamma \vd R_1 \aunifR R_2 \hastype P \ares R / (\Omega^*, \theta^*_1, \theta^*_2)$
and $\theta^*_1 \subseteq \theta_1$,  $\theta^*_2 \subseteq \theta_2$ and $\Omega^* \subseteq \Omega'$.
%
\item If $\Delta, \Omega \vd \theta_1 \chk \Omega'$ and   
      $\Delta, \Omega \vd \theta_2 \chk \Omega'$ and
  $\theta_1$ and $\theta_2$ are incompatible and\\
  $(\Delta, \Omega) ; \Gamma \vd S_1 > A \syn P$, \;  $(\Delta, \Omega) ; \Gamma \vd S_2 > A \syn P$, and \\  $(\Delta, \Omega') ; \Gamma \vd S > A \syn P$ and 
      $S_1 = \msub{\theta_1}S$  and $S_2 = \msub{\theta_2}S$\\
then there exists a contextual substitution $\theta^*_1$, $\theta^*_2$, and
a modal context $\Omega^*$, such that $(\Delta, \Omega) ; \Gamma \vd S_1
\aunifS S_2 \hastype A \ares S / ({\Omega^*},
\theta^*_1, \theta^*_2)$ and $\theta^*_1 \subseteq \theta_1$,  $\theta^*_2 \subseteq \theta_2$ and $\Omega^* \subseteq \Omega'$.
\end{enumerate}
\end{theorem}
\begin{proof}
  Simultaneous induction on the structure of $M$, $R$, and $S$. 
\end{proof}

In the next section, we extend the soundness and completeness property to substitutions.

\subsection{Most specific generalization of two contextual substitutions}
Building on the previous algorithm for computing the most specific
generalization of two linear higher-order patterns, we extend the
algorithm to contextual substitutions. We begin by giving the
judgments for computing the most specific linear generalization of two
contextual substitutions. 

\[ 
\begin{array}{ll}
\Delta, \Omega_1 \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_2
\ares \rho / (\Omega, \theta_1, \theta_2) & \;\;\;\;\rho \mbox{ is the
  mslg of } \rho_1 \mbox{ and } \rho_2
\end{array}
\]

Intuitively, we will be able to obtain $\rho_1$ by composing
$\theta_1$ with $\rho$, and we yield $\rho_2$ by composing $\theta_2$
with $\rho$. We assume $\rho_1$ and $\rho_2$ are well-typed, and have
the domain $\Omega_2$ and range $(\Omega_1, \Delta)$. 


We think of $\rho_1$ as the contextual substitution which is
already in the index, while the contextual substitution $\rho_2$ is to
be inserted. As a consequence, only $\rho_1$ will refer to the
internal meta-variables in $\Omega_1$, while $\rho_2$ only depends on
the meta-variables in $\Delta$. The result of the mslg are the
contextual substitution $\theta_1$ and $\theta_2$, where $\Delta, \Omega_1 \vd
\theta_1 \chk \Omega$ and 
$\Delta, \Omega_1 \vd \theta_2 \chk \Omega$. In other words,
$\theta_1$ (resp. $\theta_2$) only replaces internal meta-variables
in $\Omega$. 

First, we give the rules for computing the most specific linear
generalization of two contextual substitutions. 

%
\begin{small}
\[
\begin{array}{c}
\infer{(\Delta, \Omega) \vd \cdot \aunifSub \cdot \hastype \cdot \ares \cdot /
  (\cdot, \cdot, \cdot)}{} 
\\[0.75em]
\infer{(\Delta, \Omega_1) \vd (\rho_1, \Psihat.R_1/i) \aunifSub (\rho_2, \Psihat.R_2/i)
  \hastype (\Omega_2, i\ofvd P[\Psi]) \ares (\rho, \Psihat.R/i) \;/\;
  (\Omega, \theta, \theta'))}{
  \begin{array}{lcllcl}
(\Delta, \Omega_1) & \vd & \rho_1 \aunifSub \rho_2 & \hastype \Omega_2 &
\ares &  \rho \;/\; (\Omega'_1, \theta_1, \theta_2) \\
(\Delta, \Omega_1); \Psi & \vd & R_1 \aunifR R_2 & \hastype P & \ares &
R \;/\; (\Omega'_2, \theta'_1, \theta'_2) \\
\multicolumn{6}{l}{
\Omega = (\Omega'_1, \Omega'_2) \quad \theta = (\theta_1, \theta'_1) \quad \theta' = (\theta_2, \theta'_2)
}
  \end{array}
}
\end{array}
\]
\end{small}


Note, that we are allowed to just combine the contextual substitutions
$\theta_1$ ($\theta_2$ resp.) and $\theta'_1$ ($\theta'_2$ resp.)
since we require that they refer to distinct meta-variables and all
the meta-variables occur uniquely. 

Similar to the compatibility of two terms, we can define the
compatibility of two substitutions.   

\begin{definition}[Compatibility of contextual substitutions]\mbox{}\\
If $(\Delta, \Omega_1) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_2
\ares \id_{\Omega_1} / (\Omega, \rho_1, \rho_2)$, then 
two contextual substitutions $\rho_1$ and $\rho_2$ are incompatible. Otherwise, we call
$\rho_1$ and $\rho_2$ compatible.
\end{definition}

As a consequence, if $\rho_1$ and $\rho_2$ are incompatible, then for
any $\Psihat.R/i \in \rho_1$ and $\Psihat.R'/i \in \rho_2$, we know
that $R$ and $R'$ are incompatible. Next, we prove soundness and
completeness of this algorithm.


%
\begin{theorem}[Soundness for mslg of substitutions]\label{lemma:mslgSubSound}\mbox{}\\
If $(\Delta, \Omega_1) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_2 \ares
\rho / (\Omega, \theta_1, \theta_2)$ and \\ \mbox{\hspace{0.4cm}}$(\Delta, \Omega_1) \vd \rho_1 \chk \Omega_2$ and 
$(\Delta, \Omega_1) \vd \rho_2 \chk \Omega_2$ \\
%
then  $(\Delta,\Omega) \vdash \rho \chk \Omega_2$, $(\Delta,\Omega_1)
\vdash \theta_1 \chk \Omega$, $(\Delta, \Omega_1) \vdash \theta_2 \chk
\Omega$, and \\ \mbox{\hspace{0.75cm}}$\msub{\theta_1}\rho = \rho_1$ and $\msub{\theta_2}\rho = \rho_2$
\end{theorem}
\begin{proof}
  Induction on the first derivation.
\end{proof}

%
\begin{theorem}[Completeness for mslg of contextual substitutions]\label{lemma:mslgSubComplete}\mbox{}\\
If $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and $(\Delta,
\Omega) \vd \theta_2 \chk \Omega'$ and $\theta_1$ and $\theta_2$
are incompatible and\\ $\rho_1 = \msub{\theta_1}\rho$ and 
 $\rho_2 =  \msub{\theta_2}\rho$ then 
 $(\Delta, \Omega) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_1 \ares
 \rho / (\Omega^*, \theta_1^*, \theta_2^*)$ such that $\Omega^*
 \subseteq \Omega'$, $\theta_1^* \subseteq \theta_1$, $\theta_2^*
 \subseteq \theta_2$.
\end{theorem}
%
\begin{proof}
  Induction on the structure of $\rho$.
\end{proof}
%


\subsection{Insertion into substitution tree}
In this section we describe the final layer, namely the traversal of
the substitution tree to insert a substitution $\delta$. To insert 
the contextual substitution $\delta$ into a substitution tree, we  
need to traverse the index tree and compute at each node $N$ with
substitution $\rho$ the mslg between $\rho$ and $\delta$. Recall the
formal definition of substitution trees given earlier on page
\pageref{def:tree}.  

\[
\begin{array}{lcl}
\mbox{Node N} & \bnfas & (\Omega \turn \rho  \tto C)\\
\mbox{Children C} & \bnfas & [N , C] \bnfalt \nil
\end{array}
\]    

A tree is a node $N$ with a contextual substitution $\rho$ and a list
of children $C$. If the list of children is empty, we have reached a leaf.
In general, we will write $\Delta \vd N \hastype
\Omega'$ where $N = (\Omega \turn \rho \tto C)$ which means that 
$(\Delta, \Omega) \vd \rho \chk \Omega'$ and all the children $N_i$
in $C$, $\Delta \vd N_i \hastype \Omega$.

To insert a new substitution $\delta$ into the substitution tree $N$, we proceed in two steps. First,
we inspect all the children $N_i$ of a parent node $N$, where $N_i =
\Omega_i \turn \rho_i \tto C_i$ and check if $\rho_i$ is compatible with
$\delta$. This compatibility check has three possible results: 
\begin{enumerate}
\item $(\Delta, \Omega_i) \vd \rho_i \aunifSub \delta \hastype \Omega
  \ares \id _{\Omega} / (\Omega', \rho_i, \delta)$ : \\This means $\rho_i$ and
  $\delta$ are not compatible

\item $(\Delta, \Omega_i) \vd \rho_i \aunifSub \delta \hastype \Omega
  \ares \rho_i / (\Omega_i, \id_{\Omega_i}, \theta_2)$ \\
This means $\delta$ is an instance of $\rho_i$ and we continue to 
insert $\theta_2$ into the children $C_i$. In this case
$\msub{\theta_2}\delta$ is equivalent to $\rho_i$ and we call 
$\delta$ {\em{fully compatible}} with $\rho_i$.
%
\item $(\Delta, \Omega_i) \vd \rho_i \aunifSub \delta \hastype \Omega
  \ares \rho' / ({\Omega''}, \theta_1, \theta_2)$\\
  $\rho_i$  and $\delta$ are compatible, but we need to replace node
$N_i$ with a new node $\Omega'' \turn \rho' \tto C'$ where $C'$
contains two children, the child node $\Omega_i\turn \theta_1 \tto
C_i$ and the child node $\cdot \turn \theta_2 \tto \nil$. In this case
we call $\delta$ {\em {partially compatible}} with $\rho_i$.
\end{enumerate}

The idea is to iterate through the list of children and collect all
nodes which are fully compatible or at least partially compatible. If
there is a fully compatible child $N$, we continue the insertion by 
considering node $N$. If there are no fully compatible
children but a partially compatible node $N$ we need to split $N$. 

%
In general, there may be more than one fully compatible node and also
more than one partially compatible node. In an implementation we need
to resolve these choices. We employ a simple heuristic which orders the
sets of fully and partially compatible nodes according to the number
of elements the substitution contains only counting those elements
which are not mapped to themselves. A node which contains a $n$ such 
elements has size $n$ and is preferred over a node of size $m$ if $n$
is greater than $n$.
%

If no node is compatible, we simply create a new node with the
substitution we intended to insert. To simplify the algorithms we only
consider trees with at least one entry and a default identity substitution at
the root. The substitution tree which contains as the only entry the
term $\Psihat.R$ for example, is a tree with the default identity substitution
$\Psihat.i_0[\id_\Psi]/i_0$ at the root and one child with the substitution
$\Psihat.R/i_0$. 

The filtering process to collect all nodes which are fully and
partially compatible can be formalized by using the following
judgment. We will distinguish between the fully compatible 
children, which we collect in $V$, and the partially compatible
children, which we collect in $S$. 

\[
\begin{array}{llcl}
\mbox{Fully compatible children} & V & \bnfas & \cdot \bnfalt V, (N,\,\theta)\\
\mbox{Partially compatible children} & S & \bnfas & \cdot \bnfalt
S,\,(N, \Omega\turn \rho, \theta_1, \theta_2)%\\[1em]
\end{array}
\]

Note that it is not quite enough to just identify the children nodes
$N$ which are fully compatible or partially compatible. Instead, we
need to track more information. For example, if we identify a child
node $N$ where $N = \Omega' \vd \rho_i \tto C_i$ is fully compatible
with $\delta$, then this means that $\delta$ is an instance of
$\rho_i$ and there exists a contextual substitution $\theta$
such that $\msub{\theta}\rho_i = \delta$.  Similarly, if we identify a
child node $N$ where $N = \Omega' \vd \rho_i \tto C_i$ is partially
compatible with $\delta$, then this means that mslg between $\rho_i$
and $\delta$ is the contextual substitution $\rho$, and $\rho_i =
\msub{\theta_1}\rho$ and $\delta = \msub{\theta_2}\rho$.  
%
Now we can define the following judgment:
\[
\Delta \vd C \aunif \delta \hastype \Omega \ares (V,S)
\]

Given some children $C$ and a contextual substitution $\delta$, where
the domain of each child in $C$ and of the contextual substitution
$\delta$ is $\Omega$, we can compute fully compatible children $V$ and
the partially compatible children $S$. 

$\delta$ is a contextual substitution  such that $\Delta \vd \delta
\chk \Omega$, and for all the children $C_i = (\Omega_i \turn \rho_i
\tto C')$ in $C$, we have $\Delta, \Omega_i \vd \rho_i \chk
\Omega$. Then $V$ and $S$ describe all the children from $C$ which are
compatible with $\delta$. We distinguish three cases. 

%
\begin{small}
\[
\begin{array}{c}
\infer[]{\Delta \vd \nil \aunif \delta \hastype
  \Omega \ares (\cdot, \cdot)}{}
\\[1em]

\infer[NC]{\Delta \vd [(\Omega_1 \turn \rho_1 \tto C_1) , C] \aunif \delta \hastype
  \Omega \ares (V, S)}{%
  \Delta \vd C \aunif \delta \hastype \Omega \ares (V, S) &
  \Delta, \Omega_1 \vd \rho_1 \aunifSub \delta \hastype \Omega \ares
  \id_{\Omega} / (\Omega, \rho_1, \delta)}
\\[1em]
\infer[FC]{\Delta \vd [(\Omega_1 \turn \rho_1 \tto C_1) , C] \aunif \delta \hastype
  \Omega \ares ((V,\; ((\Omega_1 \turn \rho_1 \tto C_1), \theta_2)), \;S)}{%
  \Delta \vd C \aunif \delta \hastype \Omega \ares (V, S) &
  \Delta, \Omega_1 \vd \rho_1 \aunifSub \delta \hastype \Omega \ares
  \rho_1 / (\Omega_1, \id_{\Omega_1}, \theta_2) & \rho_1 \neq
  \id_{\Omega_1}}
\\[1em]
\infer[PC]{\Delta \vd [(\Omega_1 \turn \rho_1 \tto C_1) , C] \aunif \delta \hastype
  \Omega \ares (V, (S\;,\; ((\Omega_1 \turn \rho_1 \tto C_1),
  \Omega_2 \turn \rho, \theta_1, \theta_2))}{%
  \Delta \vd C \aunif \delta \hastype \Omega \ares (V, S) &
  \Delta, \Omega_1 \vd \rho_1 \aunifSub \delta \hastype \Omega \ares
  \rho / (\Omega_2, \theta_1, \theta_2) & \rho \neq \rho_1 \neq \id_{\Omega_2}}
\end{array}
\]
  
\end{small}


The $NC$ rule describes the case where the child $C_i$ is not
compatible with $\delta$. Rule $FC$ describes the case where $\delta$
is fully compatible with the child $C_i$ and the rule $PC$ describes
the case where $\delta$ is partially compatible with $C_i$. 
Before we describe the traversal of the substitution
tree, we prove some straightforward soundness properties about these
rules. The first lemma essentially states that $\delta$ is an instance
of all nodes collected in $V$. Moreover, for every node $N_i$ with
substitution $\rho_i$ in $S$, there exists a $\rho'$ which is the most specific
generalization of $\rho_i$ and $\delta$.  

%
\begin{lemma}[Insertion of substitution into tree]\label{lemma:childInsert}\mbox{}\\
If $\Delta \vd C \aunif \delta \hastype \Omega \ares (V, S)$ and 
$\Delta \vd \delta \chk \Omega$ and for any $(\Omega_i \turn \rho_i
\tto C') \in C$ with $\Delta, \Omega_i \vd \rho_i \chk \Omega$ then 
  \begin{enumerate}
  \item for any $(N_i, \theta_2) \in V$ where $N_i = (\Omega_i \vd \rho_i \tto
    C_i)$, we have $\msub{\theta_2}\rho_i = \delta$.
  \item for any $(N_i, \Omega' \vd \rho', \theta_1, \theta_2) \in S$
    where $N_i = (\Omega_i \vd \rho_i \tto C_i)$, we have
    $\msub{\theta_2}\rho' = \delta$ and $\msub{\theta_1}\rho' = \rho_i$.
  \end{enumerate}
\end{lemma}
\begin{proof}
By structural induction on the first derivation and by using the
previous soundness theorem for mslg of substitutions (theorem
\ref{lemma:mslgSubSound}).
\end{proof}
%


Next, we show insertion of a substitution $\delta$ into a substitution
tree $N$. The main judgment is the following:

\vspace{-0.5cm}
\[
\begin{array}{ll}
\Delta \vd N \aunif \delta \hastype \Omega \ares N' &
\mbox{Insert $\delta$ into the substitution tree $N$} 
\end{array}
\]

If $N$ is a substitution tree and $\delta$ is not already in the tree,
then $N'$ will be the new substitution tree after inserting $\delta$
into $N$. We write $[N'_i/N_i]C$ to indicate that the i-th node $N_i$ in
the children $C$ is replaced by the new node $N'_i$. Recall that the
substitution $\delta$ which is inserted into the substitution tree $N$
does only refer to meta-variables in $\Delta$ and does not contain
any internal meta-variables. Therefore, a new leaf with substitution
$\delta$ must have the following form: $\cdot \turn \delta \tto
\nil$. Similarly, if we split the current node and create a new leaf
$\cdot \turn \theta_2 \tto \nil$ (see rule ``Split current node'').

\begin{small}
\[
\begin{array}{c}
\multicolumn{1}{l}{\mbox{Create new leaf\hspace{10cm}}}\\[0.5em]
\infer{\Delta \vd (\Omega' \turn \rho \tto C) \aunif \delta \hastype
  \Omega \ares (\Omega' \turn \rho \tto (C ,  (\cdot \turn \delta
  \tto \nil))}{%
\Delta \vd C \aunif \delta \hastype \Omega \ares (\cdot, \cdot)} 
\\[1em]
\multicolumn{1}{l}{\mbox{Recurse\hspace{10cm}}}\\[0.5em]
\infer{\Delta \vd (\Omega' \turn \rho \tto C) \aunif \delta \hastype \Omega \ares (\Omega' \turn \rho \tto [N'/N_i]C}{%
\Delta \vd C \aunif \delta \hastype \Omega \ares (V, S) & 
N_i \in C & (N_i, \theta_2) \in V & \Delta \vd N_i \aunif \theta_2
\ares N'} 
\\[1em]
\multicolumn{1}{l}{\mbox{Split current node}}\\[0.5em]
\infer{\Delta \vd (\Omega' \turn \rho \tto C) \aunif \delta \hastype
  \Omega \ares (\Omega' \turn \rho \tto [(\Omega^* \turn \rho \tto ((\Omega_i \turn \theta_1 \tto C_i) ,(\cdot \turn \theta_2 \tto \nil)))/N_i]C)}{%
\Delta \vd C \aunif \delta \hastype \Omega \ares (\cdot, S) \hspace{0.4cm}
{N_i \in C \hspace{0.4cm} N_i = (\Omega_i \turn \rho_i \tto
  C_i)\hspace{0.4cm}}
{(N_i, \Omega^* \turn \rho, \theta_1, \theta_2) \in S}}
\end{array}
\]
\end{small}

The above rules always insert a substitution $\delta$ into the
children $C$ of a node $\Omega \turn \rho \tto C$. We start inserting
a substitution $\Psihat.R/i_0$ into the empty substitution tree which
contains the identity substitution $\Psihat.i_0[\id]/i_0$ and has an empty
list of children. This allows us to treat insertion of a substitution
$\delta$ into a substitution tree uniformly. After the first
insertion, we obtain the substitution tree which contains the identity
substitution  $\Psihat.i_0[\id]/i_0$ and the child of this node
contains the substitution $\Psihat.R/i_0$.  

%
As we mentioned in the beginning, there may not be a unique
substitution tree, and the order in which elements are inserted
matters. More importantly, there are in fact two choices which need to
be resolved when inserting a given element into a tree. The first one
arises when we recursively insert a substitution into the substitution
tree using the rule Recurse. This involves first computing a list of
fully compatible children $V$. However, there may be in fact more than
one fully compatible child, and hence we must choose one to recurse
on. The second one arises in the split rule because there maybe be
more than one partially compatible child in the set $S$. As mentioned
earlier, these two choices must be resolved in an
implementation. These choices are already present in the first-order
setting, we can employ similar heuristics to resolve them. The
higher-order framework we describe does not add any additional choices.

When inserting the contextual substitution $\theta_2$ into the tree
$N_i$, we possibly obtain a new tree $N'$, and 
we must replace the old tree $N_i$ with the new one. In practice,
these updates are done destructively, and there is no need to
explicitly return a tree $N'$ and explicitly perform this replacement.


Next, we prove soundness of the insertion algorithm -- we prove that
in fact no matter what choice we make, we obtain a correct
substitution tree. This leads us to the following soundness statement 
where we show that if we insert a substitution $\delta$ into the
children $C$, then there exists a child $C_i = \Omega_i \turn \rho_i
\tto C'_i$ in $C$ and a path from $\rho_i$ to $\rho_n$, where $\rho_n$
is at a leaf such that $\msub{\rho_n}\msub{\rho_{n-1}}\ldots \rho_i =
\delta$. 

\begin{theorem}[Soundness of insertion]\mbox{}\\
If $\Delta \vd (\Omega' \turn \rho' \tto C) \aunif \delta \hastype
\Omega \ares (\Omega' \turn \rho' \tto C')$ \\then there exists a child
$C_i = (\Omega_i \turn \rho_i \tto C')$  and  a path from $\rho_i$ to
$\rho_n$ such that $\msub{\rho_n}\msub{\rho_{n-1}}\ldots \rho_i = \delta$.
\end{theorem}
\begin{proof}
  By induction on the first derivation using the previous lemma \ref{lemma:childInsert}.
\end{proof}

\section{Retrieval}\label{sec:retrieve}

In general, we can retrieve all terms from the index which satisfy
a given property. This property may be finding all terms from the
index which unify with a given term $M$ or finding all
terms $N$ from the index, such that a given term $M$ is an instance or
variant of $N$. One advantage of substitution trees is that all these
retrieval operations can be implemented with only small changes. A key
challenge in the higher-order setting is to design efficient retrieval
algorithms which will perform well in practice. We will show  how to
retrieve terms which are an instance of a given term in the
index, and discuss how to modify this algorithm to retrieve all
elements which are unifiable with a given term, and check for variant.


\subsection{Instance checking for linear higher-order patterns}
First, we present an instance checking algorithm for linear higher-order
patterns. 
% 
Instance checking or matching for higher-order terms was
only recently proven to be decidable \cite{Sterling:LICS07}, but
efficient algorithms do not exist for the general fragment. We
therefore concentrate on linear higher-order patterns. The advantage
will be that instance checking is similar to the first-order case, and
easily can be modified to allow checking for unifiability of two terms.

%
We treat again internal meta-variables differently than
global meta-variables. The principal judgment are as follows: 

\[
\begin{array}{lclll}
\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd M_1 & \unif & M_2 & \hastype A/ (\theta, \rho) &
\mbox{$M_2$ is an instance of $M_1$}\\
\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd R_1 & \unifR & R_2 & \hastype P/ (\theta, \rho) &
\mbox{$R_2$ is an instance of $R_1$}\\
\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd S_1 & \unifR & S_2 & \hastype A > P / (\theta, \rho) & 
\mbox{$S_2$ is an instance of $S_2$}\\
\end{array}
\]
Again we assume that $M_1$ ($R_1$, $S_1$ resp.) must be well-typed in the modal
context $\Delta, \Omega$ and the bound variable context $\Gamma$.  $M_2$ ($R_2$,
$S_2$ resp.) are well-typed in the modal context $\Delta_2$ and the
bound variable context $\Gamma$. In other words
$M_1$ only contains internal meta-variables and is stored in the
index, while $M_2$ is given, and that the meta-variables occurring in
$M_1$ are distinct from the meta-variables occurring in $M_2$. 
 More formally this is stated as 
$(\Delta_1, \Omega) ; \Gamma \vd M_1 \chk A$ and $\Delta_2; \Gamma \vd
M_2 \chk A$ and $\Delta = (\Delta_2, \Delta_1)$. 
$\rho$ is the substitution for the internal meta-variables in $\Omega$ while
$\theta$ is the substitution for some meta-variables in
$\Delta_1$.  Moreover, we maintain that $\msub{\theta,\rho}M_1$ is syntactically 
equal to $M_2$. We will treat $\Omega$ as a linear context in the
formal description given below. This will make it easier to prove the
relationship between insertion and retrieval later on.

\begin{small}
  \[
  \begin{array}{c}
\multicolumn{1}{l}{\mbox{Normal terms \hspace{10cm}}}\\[0.7em]
  \infer[{\textsf{lam}}]{\Delta_2 ; (\Delta_1, \Omega); \Gamma \vd \lambda x. M_1 \unifLHA  \lambda x. M_2 \hastype A_1 \arrow A_2\;/\;(\theta, \rho)}{%
\Delta_2 ; (\Delta_1, \Omega); \Gamma, x{:}A_1 \vd M_1 \unifLHA M_2 \hastype A_2\;/\;
    (\theta, \rho)}
\\[0.7em]
\infer[\textsf{coe}]{\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd R_1 \unifLHA R_2 \hastype   P\;/\; (\theta, \rho)}{%
\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vdash R_1 \unifR  R_2 \hastype
P \;/\;(\theta, \rho)}
\end{array}
\]
%
%
  \[
\begin{array}{c}
%
\multicolumn{1}{l}{\mbox{Atomic terms \hspace{8cm}}}\\[0.7em]
  \infer[\textsf{meta-1}]{\Delta_2 ; (\Delta_1, i\ofvd P[\Gamma]) ; \Gamma \vd
    i[\id_\Gamma] \unifR R \hastype P \;/\; (\cdot,
    (\Gammahat.R/i))}{}
\\[0.7em]
  \infer[\textsf{meta-2}]{\Delta_2 ; (\Delta_1, \cdot);
    \Gamma \vd u[\pi_\Gamma] \unifR R \hastype P\;/\; (\Gammahat.(\inv{[\pi]}R /
    u), \cdot)}{u\ofvd P[\Gamma] \in \Delta_1}
\\[0.7em]
  \infer[\textsf{head}]{\Delta_2 ;(\Delta_1, \Omega); \Gamma \vd H \cdot S_1 \unifR
    H\cdot S_2 \hastype P\;/\;
    (\theta, \rho)}{\Delta_2 ; (\Delta_1, \Omega);\Gamma \vdN S_1 \unifR S_2
    \hastype A > P \;/\; (\theta, \rho) \hspace{1cm}
   \mbox{where}\; \Sigma(H) = A\; \mbox{or}\; \Gamma(H) = A}
\\[0.7em]
\multicolumn{1}{l}{\mbox{Spines}}\\
   \infer[{\sf{Snil}}]{\Delta_2 ; (\Delta_1, \cdot); \Gamma \vdN \nil \unifR \nil
     \hastype P > P \;/\; (\cdot , \cdot)}{} 
\\[1em]
 \infer[\textsf{Scons}]{
\Delta_2 ; (\Delta_1 , \Omega_1,\Omega_2) ; \Gamma \vdN (M_1 ; S_1) \unifR (M_2 ; S_2)
   \hastype A_1 \arrow A_2 > P \;/\; ((\theta_1,\theta_2),\, (\rho_1,
   \rho_2))}{
   \begin{array}{l}
\Delta_2 ; (\Delta_1 , \Omega_1); \Gamma \vd M_1 \unifR M_2  \hastype A_1 \;/\;
(\theta_1 , \rho_1)
 \\
\Delta_2 ; (\Delta_1, \Omega_2); \Gamma \vdN S_1  \unifR S_2 \hastype A_2 > P \;/\; (\theta_2, \rho_2)
   \end{array}
}
  \end{array}
  \]  
\end{small}


Note that we need not  worry about capture in the rule for lambda
expressions since  meta-variables and bound variables are
defined in different contexts. In the rule {\textsf{Scons}}, we are allowed to union the 
two substitutions $\theta_1$ and $\theta_2$, as the linearity
requirement ensures that the domains of both substitutions are
disjoint. Note that the case for matching a meta-variable $u[\pi]$
with another term $R$ is simpler and more efficient than  
in the general higher-order pattern case. In particular, it does not require
a traversal of $R$ (see rules {\sf{meta-1}} and {\sf{meta-2}}). 


Since the inverse of
the substitution $\pi$ can be computed directly and will be total, we
know $\inv{[\pi]}R$ exists and can simply generate a substitution
$\Gammahat.\inv{[\pi]}R/u$. The algorithm can be easily specialized to retrieve
variants by requiring in the {\sf{meta-2}} rule that $R$ must be
$u[\pi]$. To check unifiability we need to add the dual rule to
{\sf{meta-2}} where we unify $R$ with an meta-variable
$u[\pi]$. The only complication is that $R$ may contain internal
meta-variables which are defined later on the path in the substitution
tree. Now we show soundness and completeness of the retrieval algorithm. We
first show soundness and completeness of the instance algorithm for
terms. 

%
\begin{theorem}[Soundness of instance algorithm for terms]\label{lemma:ObjUnifSound}\mbox{}
  \begin{enumerate}
  \item If $\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd M_1 \unifLHA M_2 \hastype A
    / (\theta, \rho)$ \\where
    $(\Delta_1, \Omega) ;  \Gamma \vd M_1 \chk A$ and 
    $\Delta_2 ; \Gamma \vd M_2 \chk A$ then 
    $\msub{\theta, \rho}M_1 =  M_2$.
  \item If $\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd R_1 \unifR R_2 \hastype P
    / (\theta, \rho)$  \\where
    $(\Delta_1, \Omega) ; \Gamma \vd R_1 \syn P$ and 
    $\Delta_2 ; \Gamma \vd R_2 \syn P$ then 
    $\msub{ \theta, \rho}R_1 =   R_2$.
  \item If $\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd S_1 \unifR S_2 >
    A \syn P  / (\theta, \rho)$ \\
    where $(\Delta_1, \Omega) ;  \Gamma \vd S_1 > A \syn P$ and 
    $\Delta_2 ; \Gamma \vd S_2  > A \syn P$ then $\msub{ \theta, \rho}S_1 = S_2$.
  \end{enumerate}
\end{theorem}
\begin{proof}
  Simultaneous structural induction on the first derivation. 
\end{proof}

For completeness we show that if the term $M_2$ is an instance of a
linear term $M$ then the given algorithm will succeed and return 
substitution $\theta^*$ for the meta-variables and a substitution
$\rho^*$ for the internal meta-variables occurring in $M$. This
establishes a form of local completeness of the given retrieval
algorithm. We will show later a global completeness theorem, which
states that any time we compute the msgl of a term $M_1$ and $M_2$ to
be $M$, then we can show that $M_2$ is in fact an instance of $M$.
More generally, we show that any time we insert a substitution  $\Gammahat.M_2/i_0$ we can
also retrieve it. 

%
\begin{theorem}[Completeness of instance algorithm for terms]\mbox{}
\label{lemma:compInst}
\begin{enumerate}
\item If $(\Delta_1, \Omega) ; \Gamma  \vd M_1 \chk A$ and
  $\Delta_2; \Gamma \vd M_2\chk A$ and \\
   $\Delta_2 \vd \theta \chk \Delta_1$
  and $\Delta_2 \vd \rho \chk \Omega$ and
  $\msub{\theta,\rho}M_1 = M_2$ then\\
  $\Delta_2 ; (\Delta_1, \Omega);
  \Gamma \vd M_1 \unifLHA M_2 \hastype A / (\theta^*, \rho)$ where
  $\theta^* \subseteq \theta$.
\item If $(\Delta_1, \Omega) ; \Gamma  \vd R_1 \syn P$ and
  $\Delta_2; \Gamma \vd R_2 \syn P$ and \\
   $\Delta_2 \vd \theta \chk \Delta_1$
  and $\Delta_2 \vd \rho \chk \Omega$ and
  $\msub{\theta,\rho}R_1 = R_2$ then\\
  $\Delta_2 ; (\Delta_1, \Omega);
  \Gamma \vd R_1 \unifR R_2 \hastype P / (\theta^*, \rho)$ where
  $\theta^* \subseteq \theta$.
\item If $(\Delta_1, \Omega) ; \Gamma  \vd S_1 > A \syn P$ and
  $\Delta_2; \Gamma \vd S_2 > A \syn P$ and\\
  $\Delta_2 \vd \theta \chk \Delta_1$
  and $\Delta_2 \vd \rho \chk \Omega$ and
  $\msub{\theta,\rho}S_1 = S_2$ then\\
  $\Delta_2 ;(\Delta_1, \Omega);
  \Gamma \vd S_1 \unifLHA S_2 \hastype A > P / (\theta^*,
  \rho)$ where $\theta^* \subseteq \theta$.
\end{enumerate}
\end{theorem}
\begin{proof}
Simultaneous structural induction on the first typing derivation.
\end{proof}

\subsection{Instance checking for contextual substitutions}
The instance algorithm for terms can be straightforwardly extended
to instances of substitutions. We define the following judgment for
it:

\[
\begin{array}{ll}
\Delta_2 ; (\Delta_1, \Omega) \vd \rho_1 \unif \rho_2 \hastype \Omega' / (\theta,
\rho) & \rho_2 \mbox{ is an instance of $\rho_1$}
\end{array}
\]

We assume that $\rho_1$ is a contextual substitution from a
modal context $\Omega'$ to a modal context $\Delta, \Omega$, and  and
$\rho_2$ is a contextual substitution from $\Omega'$ to the modal
context $\Delta_2$. Our goal is to check whether $\rho_2$ is an
instance of $\rho_1$. The result of this is the contextual substitution
$\rho$ for the meta-variables in $\Omega$ and the contextual
substitution $\theta$ for the meta-variables in
$\Delta$ such that $\msub{\theta,\sigma}\rho_1$ is syntactically
equal to $\rho_2$. Again we enforce the linearity criteria for
internal meta-variables in $\Omega$ but leave it implicit for the
meta-variables in $\Delta_1$.

%
\begin{small}
\[
\begin{array}{c}
\infer{\Delta_2 ; (\Delta_1, \cdot) \vd \cdot \unif \cdot \hastype \cdot  /
  (\cdot, \cdot)}{} \\[1em]
\infer{\Delta_2 ; (\Delta_1, \Omega'_1, \Omega''_2) \vd (\rho_1, \Psihat.R_1/i) \unif (\rho_2, \Psihat.R_2/i)
  \hastype (\Omega_2, i\ofvd P[\Gamma])) /
  ((\theta, \theta'), (\rho, \rho')}{
\Delta_2 ; (\Delta_1, \Omega''_1) \vd \rho_1 \unif \rho_2 \hastype \Omega_2 
/ (\theta, \rho) &
\Delta_2 ; (\Delta_1, \Omega'_1); \Gamma \vd R_1 \unif R_2 \hastype P  / (\theta', \rho')}
\end{array}
\]
\end{small}


Next, we show soundness of retrieval for substitutions. 

%
\begin{theorem}[Soundness of retrieval for substitutions]\label{lemma:mslgRetrieveSound}\mbox{}\\
If $\Delta_2; (\Delta_1, \Omega) \vd \rho_1 \unif \rho_2 \hastype \Omega' /
(\theta, \rho)$ and $(\Delta_1, \Omega) \vd \rho_1 \chk \Omega'$
and $\Delta_2 \vd \rho_2 \chk \Omega'$ and $(\Delta_1, \Delta_2)
= \Delta$ and all the variables in $\Omega$, $\Delta_1$ and
$\Delta_2$ are distinct then 
$\msub{ \theta, \rho}\rho_1 = \rho_2$.
\end{theorem}
\begin{proof}
Structural induction on the first derivation and using previous theorem \ref{lemma:ObjUnifSound}.
\end{proof}


Finally, we show the global completeness of the mslg and instance
algorithm which relates insertion and retrieval.
We show that if the mslg of object $M_1$ and $M_2$
returns the contextual substitutions $\theta_1$ and $\theta_2$ together
with the mslg $M$, then in fact the retrieval algorithm shows that
$M_1$ is an instance of $M$ under $\theta_1$ and $M_2$ is an instance
of $M$ under $\theta_2$. This guarantees that any time we insert a
term $M_2$ we can in fact retrieve it. We assume here that the set of
meta-variables in $M_1$ is distinct from the set of meta-variables in
$M_2$ which simplifies this proof slightly, since this guarantees that
the mslg $M$ only refers to meta-variables in $\Omega'$.

%
\begin{theorem}[Interaction between mslg and instance algorithm]\label{lemma:interactObj}\mbox{}
\begin{enumerate}
\item If  $(\Delta_1, \Omega) ; \Gamma \vd M_1 \chk A$ and
  $\Delta_2 ; \Gamma \vd M_2 \chk A$ and  \\
$(\Delta_2 , \Delta_1), \Omega ; \Gamma \vd M_1 \aunif M_2 \hastype A \ares M
    / (\Omega', \rho_1, \rho_2)$ then \\
   $(\Delta_1 ; \Omega'; \Gamma \vd M \unif M_1 \hastype A / (\cdot,  \rho_1)$ and 
 $\Delta_2 ; \Omega'; \Gamma \vd M \unif M_2 \hastype A /
 (\cdot, \rho_2)$.

\item If  $(\Delta_1, \Omega) ; \Gamma \vd R_1 \syn P$ and
  $\Delta_2 ; \Gamma \vd R_2 \syn P$ and \\
$(\Delta_2 , \Delta_1), \Omega ; \Gamma \vd R_1 \aunifR R_2 \hastype P \ares R
    / (\Omega', \rho_1, \rho_2)$ then \\
   $\Delta_1; \Omega'; \Gamma \vd R \unifR R_1 \hastype P / (\cdot,  \rho_1)$ and 
 $\Delta_2 ; \Omega'; \Gamma \vd R \unifR R_2 \hastype P /
 (\cdot, \rho_2)$.

\item If  $(\Delta_1, \Omega) ; \Gamma \vd S_1 > A \syn P$ and
  $\Delta_2 ; \Gamma \vd S_2 > A \syn P$ and \\
$(\Delta_2, \Delta_1), \Omega; \Gamma \vd S_1 \aunifS S_2 \hastype A > P \ares S
    / (\Omega', \rho_1, \rho_2)$ then\\ 
$\Delta_1 ; \Omega'; \Gamma \vd S \unif S_1 \hastype A > P / (\cdot,
    \rho_1)$ and 
 $\Delta_2  ; \Omega'; \Gamma \vd S \unif S_2 \hastype A >
 P / (\cdot, \rho_2)$.
\end{enumerate}
\end{theorem}
\begin{proof}
  Simultaneous structural induction on the first derivation. 
\end{proof}

%
\begin{theorem}[Insertion and retrieval for substitutions]\label{lemma:mslgInteract}\mbox{}\\
If $\Delta_2 , \Delta_1, \Omega  \vd \rho_1 \aunifSub \rho_2 \hastype
\Omega' \ares \rho / (\Omega'', \theta_1, \theta_2)$ and \\
$(\Delta_1, \Omega) \vd \rho_1 \chk \Omega'$
and $\Delta_2 \vd \rho_2 \chk \Omega'$ and $(\Delta_1, \Delta_2)
= \Delta$
 then\\
$\Delta_1 ;  \Omega''  \vd \rho \unif \rho_1 \hastype \Omega' /
(\cdot, \theta_1)$ and 
$\Delta_2 ; \Omega''  \vd \rho \unif \rho_2 \hastype \Omega' /(\cdot, \theta_2)$
\end{theorem}
\begin{proof}
Structural induction on the first derivation and use of lemma \ref{lemma:interactObj}.
\end{proof}

Next, we show how to traverse the tree, to find a path
$\msub{\rho_n}\msub{\rho_{n-1}}\ldots\rho_1$ such that $\rho_2$ is an
instance of it and return a contextual substitution $\theta$ such that 
$\msub{\theta}\msub{\rho_n}\msub{\rho_{n-1}}\ldots\rho_1 = \rho_2$.
Traversal of the tree is straightforward.

\begin{small}
\[
\begin{array}{c}
%
\infer{\Delta \vd [(\Omega \turn \rho \tto C), C'] \unif \rho_2 \hastype
  \Omega' / (\theta',\theta)}{%
\Delta, \Omega \vd \rho \unif \rho_2 \hastype \Omega' / (\theta',
\rho') & 
\Delta \vd C \unif \rho' \hastype \Omega / \theta}
\\[1em]
\multicolumn{1}{l}{\mbox{}}\\[0.5em]
\infer{\Delta \vd [(\Omega \turn \rho \tto C), C'] \unif \rho_2 \hastype \Omega' / \theta}{%
\mbox{there is no derivation such that} \Delta, \Omega \vd \rho \unif \rho_2
\hastype \Omega' / (\theta',\rho') \\
{\hspace{6cm}\Delta \vd C' \unif \rho \hastype \Omega / \theta}}
%
\end{array}
\]
\end{small}

\begin{theorem}[Soundness of retrieval]\mbox{}\\
If $\Delta \vd C \unifLHA \rho' \hastype \Omega' / \theta$ then
there exists a child $C_i$ with substitution $\rho_i$ in $C$ such that
the path
$\msub{\theta}\msub{\rho_n}\msub{\rho_{n-1}}\ldots\msub{\rho_i} =
\rho'$. 
\end{theorem}
\begin{proof}
  By structural induction on the first derivation and use of
 lemma \ref{lemma:mslgRetrieveSound}.
\end{proof}

Finally, we show that if we insert $\rho$ into a substitution tree and
obtain a new tree, then we are able to retrieve $\rho$ from it.

\begin{theorem}[Interaction between insertion and retrieval]\mbox{}\\
If $\Delta \vd (\Omega \vd \rho \tto C) \aunif \rho_2 \hastype \Omega
\ares (\Omega \vd \rho \tto C')$ then 
$\Delta \vd C' \unif \rho_2 / \id_\Delta$.
\end{theorem}
\begin{proof}
  Structural induction on the derivation using theorem \ref{lemma:mslgInteract}.
\end{proof}



\section{Extension to dependently typed terms}\label{sec:DepTypes} 

Substitution trees are especially suited for indexing dependently
typed terms, since they provide more flexibility than indexing
techniques such as discrimination tries or path indexing techniques
which only allow us to share 
common prefixes. To illustrate this point, we define a data-structure
for lists consisting of characters and we keep track of the size of
the list by using dependent types.  

\[
\begin{array}{ll}
\chars\; : \type. & \listd: \integer \arrow \type.\\
{\mathsf{a}} : \chars. & \nil : \listd\; 0.\\
{\mathsf{b}} : \chars. & \cons  : \Pi n{:}\integer. \chars \arrow \listd n \arrow \listd (n + 1). \\
{\mathsf{test}}: \Pi n{:}\integer.\listd n \arrow \type.
\end{array}
\]

The size of lists is an explicit argument to the predicate {\sf
  test}. Hence {\sf test} takes in two arguments, the first one is the
size of the list and the second one is the actual list. The list
constructor {\sf cons} takes in three arguments. The first one
denotes the size of the list, the second argument denotes the head and
the third one denotes the tail. To illustrate, we give a few
examples. We use gray color for the index arguments. 
\[
\begin{array}{l}
{\mathsf{test}}\; {\mygray{4}}\; (\cons {\mygray{3}}\; a\; (\cons
{\mygreen{2}}\; a\; (\cons{\mygreen{1}}\; a \; (\cons {\mygreen{0}}\; b\;\nil))))\\
{\mathsf{test}}\; {\mygray{5}}\; (\cons{\mygreen{4}}\;  a\; (\cons
{\mygreen{3}}\; a\; (\cons {\mygreen{2}}\; a \; (\cons {\mygreen{1}}\;
a\;(\cons {\mygreen{0}}\; b\; \nil)))))\\
{\mathsf{test}}\; {\mygray{6}}\; (\cons {\mygray{5}}\; a\; (\cons
{\mygray{4}}\; a\; (\cons {\mygray{3}}\; a \; (\cons {\mygray{2}}\;
b\;(\cons {\mygray{1}}\; a\;(\cons {\mygray{0}}\; b\; \nil))))))\\
\end{array}
\] 

If we use non-adaptive indexing techniques such as 
discrimination tries, we process the term from left to right and we
will be able to share common prefixes. In the given
example, such a technique discriminates on the first argument,
which denotes the size of the list and leads to no sharing between the second
argument. The substitution tree on the other hand allows us to share the
structure of the second argument. The most specific linear
generalization in this example is 

\[
{\mathsf{test}}\; i_1[\id]\;(\cons i_2[\id]\;a\;(\cons
i_3[\id]\;a\;(\cons i_4[\id]\;a\; (\cons i_5[\id]\;i_6[\id]\;\nil)))).
\]

This allows us to skip over the first argument denoting the size
and indexing on the second argument,  
the actual list. It has been sometimes argued that it is possible to
retain the flexibility in non-adaptive indexing techniques by 
reordering the arguments to ${\mathsf{test}}$. However, this only works
easily in an untyped setting and it is not clear how to maintain
typing invariants in a dependently typed setting if we allow arbitrary
reordering of arguments. Hence higher-order substitution trees offer
an adaptive compact indexing data-structure while maintaining typing
invariants. 

However, there are unique challenges of designing and implementing
higher-order substitution trees for dependently typed terms. For
example, transforming dependently typed terms into linear
higher-order patterns may result in ill-typed terms -- or better
linear higher-order patterns are only well-typed modulo variable
definitions. Fortunately, linear higher-order patterns are still
approximately well-typed. It were these complex issues which lead us
to carefully formalize substitution trees in the simply typed setting.

We may think of linear terms as a representation which is only used
internally, and all linear terms are well-typed modulo variable
definitions. Then we can show that simple types (e.g. types where
dependencies have been erased) are preserved in substitution trees,
and all intermediate variables introduced are only used within this
data-structure, but do not leak outside. As a consequence, we will
always obtain a dependently typed term after composing the contextual
substitutions in one branch of the substitution tree and solving the
variable definitions.

\section{Implementation and experimental results}\label{sec:exp}

We have implemented substitution trees to manage the table in the
tabled higher-order logic programming engine \cite{Pientka:CADE05} to
permit lookup and possible insertion of terms to be performed in a
single pass as part of the Twelf system \cite{Pfenning99cade}. The
Twelf system is an implementation of the logical framework LF together
with a logic programming engine using  the typed functional language
SML of New Jersey 110.0.3. 

In the tabled higher-order logic programming engine  we store 
intermediate subgoals in a memoization table which is
implemented as a substitution tree. Each tabled predicate has its own
substitution tree. Our implementation is a high-level implementation
which relies on the existing data-structure for terms and types to
smoothly integrate it into the existing framework. In our
implementation, de Bruijn indices are used to implement bound
variables and meta-variables, and terms are implemented using spine
notation as described in this paper.  

The substitution tree itself is implemented as a linked tree, where a
node contains as data a substitution together with the context of
meta-variables occurring in the range of this substitution and a list of
pointers to other substitution trees which constitute its children. 
The substitution at each node is implemented as a set using C. Okasaki's
implementation of red-black trees. This allows for destructive updates
within the tree. 

In the implementation we use two different de Bruijn indices -- one
for bound variables and global meta-variables (from $\Delta$), and one
for internal meta-variables (from $\Omega$). To distinguish between bound
variables and global meta-variables we in addition carry a
marker. Internal existential variables $i$ will be instantiated at a
later point as we traverse the tree. Global meta-variables on the
other hand are only subject to instantiation if we check whether the
current subgoal is an instance of one in the table.

At the leafs of the substitution tree, we store linear residual
equations, context $\Gamma$, the meta-variables occurring
in the residual equations and in $\Gamma$, as well as a pointer to the
answer list. 
%
We maintain that terms are kept in $\beta\eta$-normal form, as also
described in this paper. Before inserting a term in the index we
normalize and linearize it to obtain a standard form. In the
subsequent discussion, we compare the performance of the tabled engine
with and without indexing. 


\subsection{Experimental results}
In this section, we discuss examples from three different applications
which use the tabled logic programming engine in Twelf. Here we focus
on an evaluation of the indexing technique. For a more in-depth
discussion of tabling we refer the reader to 
\cite{Pientka:ICLP02,Pientka:CADE05}. All experiments were done on a 
machine with the following specifications: 1.60GHz Intel Pentium
Processor, 256 MB RAM. We are using SML of New Jersey 110.0.3 under
Linux Red Hat 7.1. Times are measured in seconds. All the examples use
variant checking as a retrieval mechanism. Although we have
implemented instance checking, which allows us to check if a table
entry subsumes the given goal, we did not observe substantial
performance improvements. This is mostly due to the fact that the
surrounding tabling engine can maintain stronger invariants if we
support only variant checking and eliminates the need to perform a
lookup on the table to retrieve answers.  
A similar observation has been made for tabling in the  first-order
logic programming engine XSB \cite{RamakrishnanJLP99}. Potentially
instance checking becomes more important in theorem proving, as the
experience in the first-order setting shows. We compare our tabling
engine without term indexing and without linearization to the one
which supports substitution tree indexing.

\subsection{Parsing of first-order formulae}
Parsing and recognition algorithms for grammars are excellent examples
for tabled evaluation, since we often want to mix right and left
recursion (see also \cite{Warren+book99}). In this example, we adapted
ideas from \cite{Warren+book99} to implement a parser for
first-order formulas using higher-order abstract syntax.
The simplest
way to implement left and right associativity properties of
implications, conjunction and disjunction is to mix right and left
recursive program clauses. Clauses for conjunction and disjunction are
left recursive, while the program clause for implication is right
recursive. Such an implementation of the grammar is straightforward mirroring the defined properties such as left and right associativity and precedence ordering.

\begin{center}
\begin{tabular}[h]{r|r|r||r|r}
\hspace{0.25cm}\#tok & noindex & index & reduction & improvement\\
& & & in time & factor\\
\hline 
20 &  $\;\;$0.13 & $\;\;$0.07 & 46\% & 1.85\\
%32 & $\;\;$0.72 & $\;\;$0.36 & & 2.00\\
58 &  $\;\;$2.61 & $\;\;$1.25 & 52\% & 2.08\\
117 & 10.44 & $\;\;$5.12 &  51\% &  2.03\\ 
178 & 32.20 &  13.56 & 58\% & 2.37\\
235 & 75.57 & 26.08 & 66\% & 2.90\\
\end{tabular}
\end{center}    

The first column denotes the number of tokens which are parsed. This
example illustrates that indexing can lead to improvements by over a
factor of 2.90. In fact, the more tokens need to be parsed and the longer the
tabled logic programming engine runs, the larger the benefits of
indexing. The table grows up to over 4000 elements in this
example. This indicates that indexing prevents to some extent program
degradation due to large tables and longer run-times. 

\subsection{Refinement type-checker}
In this section, we discuss experiments with a bi-directional
type-checking algorithm for a small functional language with
intersection types which has been developed by Davies and
Pfenning~\cite{Davies+ICFP00}. 
We use an implementation of the bi-directional type-checker in Twelf
by F. Pfenning. The type-checker is executable with the original 
logic programming interpreter, which performs a depth-first
search. However, redundant computation may severely hamper 
its performance as there are several derivations for proving that a
program has a specified type.

We give several examples which are grouped in three categories. In the
first category, we are interested in finding the first answer to a
type checking problem and once we have found the answer execution
stops. The second category contains example programs which are not
well-typed and the implemented type-checker rejects these programs as
not well-typed. The third category are examples where we are
interested in finding all answer to the type-checking
problem.

\begin{small}
\begin{center}
\begin{tabular}[h]{l|r|r||r|r}
\multicolumn{4}{c}{First answer}\\[0.5em]
 \multicolumn{1}{c}{example} & \multicolumn{1}{c}{noindex} &
\multicolumn{1}{c}{index} & \multicolumn{1}{c}{reduction} &
\multicolumn{1}{c}{improvement} \\
& & & \multicolumn{1}{c}{time} & \multicolumn{1}{c}{factor}\\
\hline
 sub1 & 3.19   &  0.46  & 86\% & 6.93 \\
 sub2 & 4.22 & 0.55 &  87\% & 7.63\\
 sub3 &  5.87  & 0.63 &  89\% & 9.32\\
 mult   & 7.78  & 0.89  & 89\% & 8.74 \\
 square1 & 9.08 & 0.99 & 89\% & 9.17 \\
 square2 &  9.02  &  0.98 & 89\% & 9.20 
\end{tabular}     
\end{center}

\begin{center}
\begin{tabular}[h]{l|r|r||r|r}
\multicolumn{4}{c}{Not provable}\\[0.5em]
 \multicolumn{1}{c}{example} & \multicolumn{1}{c}{noindex} &
\multicolumn{1}{c}{index} & \multicolumn{1}{c}{reduction} & \multicolumn{1}{c}{improvement} \\
& & & \multicolumn{1}{c}{time} & \multicolumn{1}{c}{factor}\\
\hline
multNP1 & 2.38  & 0.38  & 84\% & 6.26  \\
multNP2 & 2.66 & 0.51 &  81\% & 5.22\\ 
plusNP1 & 1.02 & 0.24 & 76\% & 4.25\\
plusNP2 &  6.48  & 0.85  & 87\% & 7.62  \\
squareNP1 & 9.29  & 1.09  & 88\% & 8.52  \\
squareNP2 & 9.26 & 1.18 & 87\% & 7.85
\end{tabular}     
\end{center}

\begin{center}
\begin{tabular}[h]{l|r|r||r|r}
\multicolumn{4}{c}{All answers}\\
 \multicolumn{1}{c}{example} & \multicolumn{1}{c}{noindex} &
\multicolumn{1}{c}{index} & \multicolumn{1}{c}{reduction} & \multicolumn{1}{c}{improvement} \\
& & & \multicolumn{1}{c}{time} & \multicolumn{1}{c}{factor}\\
\hline
sub1 &  6.88  &   0.71 & 90\% & 9.69  \\
sub2 & 3.72 & 0.48 & 87\% & 7.75\\
sub3 & 4.99 & 0.59  & 88\% & 8.46\\ 
mult & 9.06  &   0.98  & 89\% & 9.24 \\
square1 & 10.37 & 1.11 & 89\% & 9.34\\
square2 & 10.30  &  1.08  & 90\% & 9.54 
\end{tabular}      
\end{center}  
\end{small}

As the results demonstrate indexing leads to substantial improvements
by over a factor of 9. Table sizes are around 500 entries. 


\subsection{Evaluating Mini-ML expression via reduction}
In the third experiment we use an implementation which  evaluates
expressions of a small functional language via reduction. The
reduction rules are highly non-deterministic containing reflexivity
and transitivity rules. 

\begin{center}
\begin{tabular}{l|r|r||r|r}
\multicolumn{1}{c}{example} & \multicolumn{1}{c}{noindex} & \multicolumn{1}{c}{index} & \multicolumn{1}{c}{reduction} & \multicolumn{1}{c}{improvement} \\
& & & \multicolumn{1}{c}{time} & \multicolumn{1}{c}{factor}\\
\hline
mult1 &  10.86        &    6.26  & 57\% & 1.73\\

mult2 &  39.13        &   18.31  & 47\% & 2.14\\
addminus1 &  54.31        &   14.42  & 73\% & 3.77\\
addminus2 & 57.34 & 15.66 & 73\% & 3.66\\
addminus3 & 55.23 & 25.45 & 54\% & 2.17\\
addminus4 & 144.73 & 56.63 & 61\% & 2.55\\
minusadd1 & 1339.16 &  462.83  & 65\% & 2.89\\
\end{tabular}  
  
\end{center}


As the results demonstrate, performance is improved by up to
3.77. Table size was around 500 entries in the table. The limiting
factor in this example is not necessarily the table size but the large
number of suspended goals which is over 6000. This may be the reason
why the speed-up is not as large as in the refinement type-checking example.


\section{Related work}\label{sec:related}
We have presented a higher-order term indexing technique, called
higher-order substitution trees. We only know of two other prior attempts to
design and implement a higher-order term indexing technique. L.~Klein
\cite{Klein97} developed in his master's thesis a higher-order term
indexing technique for simply typed terms where algorithms are based
on a fragment of Huet's higher-order unification algorithm, the
simplification rules. Since the most specific
linear generalization of two higher-order terms does not exist in general, he
suggests to maximally decompose a term into its atomic subterms. This
approach results in larger substitution trees and stores redundant
substitutions. In addition, he does not use explicit substitutions
leading to further redundancy in the representation of terms. As no
linearity criteria is exploited, the consistency checks need to be
performed eagerly, potentially degrading the performance.

Necula and Rahul briefly discuss the use of automata driven
indexing for higher-order terms in \cite{Necula+01:oracle}. Their
approach is to ignore all higher-order features when maintaining the
index, and return an imperfect set of candidates. Then full higher-order
unification on the original terms is used to filter out the ones which
are in fact unifiable in a post-processing step. They also implemented
Huet's unification algorithm, which is highly
nondeterministic. Although they have achieved substantial speed-up
for their application in proof-carrying code, it is not as general as 
the technique we have presented here. The presented
indexing technique is designed as a perfect filter for linear
higher-order patterns. For objects which are not linear higher-order
patterns, we solve variable definitions via higher-order unification,
but avoid calling higher-order unification on the original term.

More recently, Theiss and Benzm\"uller explore higher-order term
indexing in their implementation of Leo-II, a higher-order resolution
theorem prover \cite{Theiss:IWIL06}. Their approach is based on
coordinate and path indexing \cite{AICPub498:1989}. The work mostly
focuses on efficient data-structure of lambda-terms based on de Bruijn
indices together with a path-indexing structure. Terms are not
represented using spines, which means that there is no easy access to
the head of a lambda-term. Moreover, there is no notion of
meta-variables as closures. To implement path-indexing for
lambda-terms, the authors keep track of the scope of lambda-binders
using a scope number. Their indexing structure is partly designed to
speed-up $\beta$-reduction, and the impact on theorem proving is not
yet fully known.

Higher-order substitution trees provide a very flexible term indexing
structure. As mentioned earlier, they are particular suited for
dependently-typed systems, since there is no sharing of
prefixes. However, in general there may be multiple ways to insert a
term and no optimal substitution trees exist, and these choices must
be resolved in an implementation. 
%
%
One may consider obtaining an even more compact tree by computing the
generalization of $(\andLF (\notLF A)\;(\notLF B))$ and $(\orLF (\notLF
A)\;(\notLF B))$  as $i[\notLF A/x, \notLF B/y]$ where we can obtain the
first term by instantiating $i$ with $(\andLF x\;y)$ and the second
one by instantiating $i$ with $(\orLF x\;y)$. A similar idea is
employed in the first-order setting in context trees
\cite{Ganzinger:JAR04}. In the higher-order setting however to allow
this extension is non-trivial since the term $i[\notLF A/x, \notLF
B/y]$ is outside the decidable pattern fragment. For example, if we
match $(\impLF (\notLF A) (\notLF B))$ against $i[\notLF A/x, \notLF
B/y]$, then there are four possible instantiations for $i$: 
$(\impLF x\;y)$, $(\impLF (\notLF A)\;y)$, $(\impLF x\;(\notLF B))$, 
$(\impLF (\notLF A)\;(\notLF B))$. This nondeterminism would
significantly complicate insertion and retrieval.


\section{Conclusion}
We have presented the theoretical foundation for higher-order
substitution trees based on linear higher-order patterns, 
developed algorithms for computing most specific generalizations of
two linear higher-order patterns, and proved the correctness of
inserting and retrieving elements from a substitution tree. The
presented framework can serve as a general foundation for higher-order
term indexing in many higher-order logic programming systems such as
$\lambda$Prolog \cite{Nadathur99cade}, and higher-order theorem
provers such as Bedwyr \cite{Baelde07:Bedwyr}, Isabelle
\cite{Paulson86}, or Leo-II \cite{Benzmueller:IJCAR08}.   

We have implemented substitution trees within the Twelf system
\cite{Pfenning99cade} as part of the higher-order tabled logic
programming engine. As our experimental result show, this lead to an
improvement of up to a factor of 10 for the tabling engine.
In the tabling engine, the table is a dynamically built
index, i.e. when evaluating a query we store intermediate goals
encountered during proof search. We have also used our substitution tree
implementation to index higher-order logic programs (see
\cite{Pientka:ICLP05}). The use of indexing in this setting was
motivated by the need to easily retrieve all clauses which unify with
a current goal. This was difficult to incorporate in the existing
previous implementation, and substitution trees provided a flexible
way to deal with this issue. For this we build the index statically,
observing the order of the clauses from the program.   

Our experimental results and implementation demonstrate that indexing
in the higher-order setting is feasible and beneficial in
practice. However, much work remains to be done on the implementations
of higher-order logic programming systems and higher-order theorem
provers to explore the full impact of these techniques. In the setting
of substitution tree indexing for example, we can compute an optimal
substitution tree via unification factoring
\cite{Dawson+95:unification} for a static set of terms to get the best
sharing among clause  heads. Hence an important question is how these
results carry over to higher-order case. Another important observation
is that clause heads typically do not use deeply nested terms, but are 
fairly shallow. This results in shallow substitution trees which are
wide but not very deep. In the future, we plan to explore and optimize
substitution tree indexing for indexing higher-order logic programming
clauses.      


\section*{Acknowledgments} I would like to thank the reviewers for
their thorough and extensive comments which helped improve this work substantially.

\bibliographystyle{acmtrans}
\begin{thebibliography}{}

\bibitem[\protect\citeauthoryear{Abadi, Cardelli, Curien, and L\'{e}vy}{Abadi
  et~al\mbox{.}}{1990}]{Abadi:POPL90}
{\sc Abadi, M.}, {\sc Cardelli, L.}, {\sc Curien, P.-L.}, {\sc and} {\sc
  L\'{e}vy, J.-J.} 1990.
\newblock Explicit substitutions.
\newblock In {\em 17th {ACM} SIGPLAN-SIGACT Symposium on Principles of
  Programming Languages (POPL'90)}. ACM Press, 31--46.

\bibitem[\protect\citeauthoryear{Baelde, Gacek, Miller, Nadathur, and
  Tiu}{Baelde et~al\mbox{.}}{2007}]{Baelde07:Bedwyr}
{\sc Baelde, D.}, {\sc Gacek, A.}, {\sc Miller, D.}, {\sc Nadathur, G.}, {\sc
  and} {\sc Tiu, A.} 2007.
\newblock The {Bedwyr} system for model checking over syntactic expressions.
\newblock In {\em 21st Conference on Automated Deduction}, {F.~Pfenning}, Ed.
  Lecture Notes in Artificial Intelligence (LNAI 4603). Springer, 391--397.

\bibitem[\protect\citeauthoryear{Benzm{\"u}ller, Theiss, Paulson, and
  Fietzke}{Benzm{\"u}ller et~al\mbox{.}}{2008}]{Benzmueller:IJCAR08}
{\sc Benzm{\"u}ller, C.}, {\sc Theiss, F.}, {\sc Paulson, L.}, {\sc and} {\sc
  Fietzke, A.} 2008.
\newblock Leo-{II} - {A} {C}ooperative {A}utomatic {T}heorem {P}rover for
  {H}igher-{O}rder {L}ogic (System Description).
\newblock In {\em 4th International Joint Conference on Automated Reasoning
  (IJCAR'08)}. Lecture Notes in Artificial Intelligence (LNAI 5195). Springer, 162--170.

\bibitem[\protect\citeauthoryear{Cervesato and Pfenning}{Cervesato and
  Pfenning}{2003}]{Cervesato:JLC03}
{\sc Cervesato, I.} {\sc and} {\sc Pfenning, F.} 2003.
\newblock A linear spine calculus.
\newblock {\em Journal of Logic and Computation\/}~{\em 13,\/}~5, 639--688.

\bibitem[\protect\citeauthoryear{Chen, Ramakrishnan, and Ramesh}{Chen
  et~al\mbox{.}}{1994}]{Chen:SPE94}
{\sc Chen, T.}, {\sc Ramakrishnan, I.~V.}, {\sc and} {\sc Ramesh, R.} 1994.
\newblock Multistage indexing for speeding prolog executions.
\newblock {\em Software -- Practice and Experience\/}~{\em 24,\/}~12,
  1097--1119.

\bibitem[\protect\citeauthoryear{Davies and Pfenning}{Davies and
  Pfenning}{2000}]{Davies+ICFP00}
{\sc Davies, R.} {\sc and} {\sc Pfenning, F.} 2000.
\newblock Intersection types and computational effects.
\newblock In {\em 5th International Conference on Functional
  Programming (ICFP'00)}. ACM Press, 198--208.

\bibitem[\protect\citeauthoryear{Dawson, Ramakrishnan, Ramakrishnan, and
  Swift}{Dawson et~al\mbox{.}}{1995}]{Dawson+95:optimizing}
{\sc Dawson, S.}, {\sc Ramakrishnan, C.~R.}, {\sc Ramakrishnan, I.~V.}, {\sc
  and} {\sc Swift, T.} 1995.
\newblock Optimizing clause resolution: Beyond unification factoring.
\newblock In {\em International Logic Programming Symposium}, MIT Press. 194--208.

\bibitem[\protect\citeauthoryear{Dawson, Ramakrishnan, Skiena, and
  Swift}{Dawson et~al\mbox{.}}{1995}]{Dawson+95:unification}
{\sc Dawson, S.}, {\sc Ramakrishnan, C.~R.}, {\sc Skiena, S.}, {\sc and} {\sc
  Swift, T.} 1995.
\newblock Principles and practice of unification factoring.
\newblock {\em ACM Transactions on Programming Languages and Systems\/}~{\em
  18,\/}~6, 528--563.

\bibitem[\protect\citeauthoryear{Dawson, Ramakrishnan, and
  V.Ramakrishnan}{Dawson et~al\mbox{.}}{1995}]{Dawson+95:jump}
{\sc Dawson, S.}, {\sc Ramakrishnan, C.~R.}, {\sc and} {\sc V.Ramakrishnan, I.}
  1995.
\newblock Design and implementation of jump tables for fast indexing of logic
  programs.
\newblock In {\em International Symposium on Programming Language
  Implementation and Logic Programming (PLILP'95)}. Lecture Notes in Computer
  Science (LNCS 982). Springer, 133--150.

\bibitem[\protect\citeauthoryear{Dowek, Hardin, and Kirchner}{Dowek
  et~al\mbox{.}}{1995}]{Dowek95}
{\sc Dowek, G.}, {\sc Hardin, T.}, {\sc and} {\sc Kirchner, C.} 1995.
\newblock Higher-order unification via explicit substitutions.
\newblock In {\em 10th Annual Symposium on Logic in
  Computer Science}, {D.~Kozen}, Ed. IEEE Computer Society Press, 366--374.

\bibitem[\protect\citeauthoryear{Ganzinger, Nieuwenhuis, and Nivela}{Ganzinger
  et~al\mbox{.}}{2004}]{Ganzinger:JAR04}
{\sc Ganzinger, H.}, {\sc Nieuwenhuis, R.}, {\sc and} {\sc Nivela, P.} 2004.
\newblock Fast term indexing with coded context trees.
\newblock {\em Journal of Automated Reasoning\/}~{\em 32,\/}~2, 103--120.

\bibitem[\protect\citeauthoryear{Graf}{Graf}{1995a}]{Graf+rta95}
{\sc Graf, P.} 1995a.
\newblock Substitution tree indexing.
\newblock In {\em 6th International Conference on Rewriting
  Techniques and Applications, Kaiserslautern, Germany}. Lecture Notes in
  Computer Science (LNCS 914). Springer-Verlag, 117--131.

\bibitem[\protect\citeauthoryear{Graf}{Graf}{1995b}]{Graf+Book95}
{\sc Graf, P.} 1995b.
\newblock {\em Term Indexing}.
\newblock Lecture Notes in Artificial Intelligence (LNAI 1053).
  Springer-Verlag.

\bibitem[\protect\citeauthoryear{Hillenbrand}{Hillenbrand}{2003}]{Hil03}
{\sc Hillenbrand, T.} 2003.
\newblock \textsc{Citius altius fortius:} lessons learned from the theorem
  prover \textsc{Waldmeister} (invited paper).
\newblock In {\em Proceedings of the 4th International Workshop on First-Order
  Theorem Proving}, {I.~Dahn} {and} {L.~Vigneron}, Eds. Electronic Notes in
  Theoretical Computer Science, vol. 86.1. Elsevier Science.

\bibitem[\protect\citeauthoryear{Klein}{Klein}{1997}]{Klein97}
{\sc Klein, L.} 1997.
\newblock Indexing f{\"u}r {T}erme h{\"o}herer {S}tufe.
\newblock Diplomarbeit, FB 14, Universit{\"a}t des {S}aarlandes,
  {S}aarbr{\"u}cken, Germany.

\bibitem[\protect\citeauthoryear{McCune}{McCune}{1992}]{McCune92}
{\sc McCune, W.} 1992.
\newblock Experiments with discrimination-tree indexing and path indexing for
  term retrieval.
\newblock {\em Journal of Automated Reasoning\/}~{\em 9,\/}~2, 147--167.

\bibitem[\protect\citeauthoryear{Miller}{Miller}{1991a}]{Miller91jlc}
{\sc Miller, D.} 1991a.
\newblock A logic programming language with lambda-abstraction, function
  variables, and simple unification.
\newblock {\em Journal of Logic and Computation\/}~{\em 1,\/}~4, 497--536.

\bibitem[\protect\citeauthoryear{Miller}{Miller}{1991b}]{Miller91iclp}
{\sc Miller, D.} 1991b.
\newblock Unification of simply typed lambda-terms as logic programming.
\newblock In {\em 8th International Logic Programming Conference}. MIT
  Press, 255--269.

\bibitem[\protect\citeauthoryear{Nadathur and Mitchell}{Nadathur and
  Mitchell}{1999}]{Nadathur99cade}
{\sc Nadathur, G.} {\sc and} {\sc Mitchell, D.~J.} 1999.
\newblock System description: {Teyjus} -- a compiler and abstract machine based
  implementation of {L}ambda {P}rolog.
\newblock In {\em 16th International Conference on Automated
  Deduction (CADE'99)}, {H.~Ganzinger}, Ed. Lecture Notes in Computer
  Science (LNCS 1632). Springer, 287--291.

\bibitem[\protect\citeauthoryear{Nanevski, Pfenning, and Pientka}{Nanevski
  et~al\mbox{.}}{2008}]{Nanevski:ICML05}
{\sc Nanevski, A.}, {\sc Pfenning, F.}, {\sc and} {\sc Pientka, B.} 2008.
\newblock Contextual modal type theory.
\newblock {\em ACM Transactions on Computational Logic\/}~{\em 9,\/}~3.

\bibitem[\protect\citeauthoryear{Necula and Rahul}{Necula and
  Rahul}{2001}]{Necula+01:oracle}
{\sc Necula, G.} {\sc and} {\sc Rahul, S.} 2001.
\newblock Oracle-based checking of untrusted software.
\newblock In {\em 28th {ACM} SIGPLAN-SIGACT Symposium on Principles of
  Programming Languages (POPL'01)}. ACM Press, 142--154.

\bibitem[\protect\citeauthoryear{Paulson}{Paulson}{1986}]{Paulson86}
{\sc Paulson, L.~C.} 1986.
\newblock Natural deduction as higher-order resolution.
\newblock {\em Journal of Logic Programming\/}~{\em 3}, 237--258.

\bibitem[\protect\citeauthoryear{Pfenning}{Pfenning}{1991}]{Pfenning91lics}
{\sc Pfenning, F.} 1991.
\newblock Unification and anti-unification in the {Calculus} of
  {Constructions}.
\newblock In {\em 6th Annual {IEEE} Symposium on Logic in Computer Science}.
IEEE  Computer Society Press, 74--85.

\bibitem[\protect\citeauthoryear{Pfenning and Sch{\"u}rmann}{Pfenning and
  Sch{\"u}rmann}{1999}]{Pfenning99cade}
{\sc Pfenning, F.} {\sc and} {\sc Sch{\"u}rmann, C.} 1999.
\newblock System description: {Twelf} --- a meta-logical framework for
  deductive systems.
\newblock In {\em 16th International Conference on Automated
  Deduction (CADE'99}, {H.~Ganzinger}, Ed. Lecture Notes in
Artificial Intelligence (LNAI 1632). Springer, 202--206.

\bibitem[\protect\citeauthoryear{Pientka}{Pientka}{2002}]{Pientka:ICLP02}
{\sc Pientka, B.} 2002.
\newblock A proof-theoretic foundation for tabled higher-order logic
  programming.
\newblock In {\em 18th International Conference on Logic Programming}, {P.~Stuckey}, Ed. Lecture Notes in Computer Science
  (LNCS 2401). Springer, 271 --286.

\bibitem[\protect\citeauthoryear{Pientka}{Pientka}{2003a}]{Pientka:ICLP03}
{\sc Pientka, B.} 2003a.
\newblock Higher-order substitution tree indexing.
\newblock In {\em 19th International Conference on Logic Programming}, {C.~Palamidessi}, Ed. Lecture Notes in Computer Science (LNCS 2916).
  Springer, 377--391.

\bibitem[\protect\citeauthoryear{Pientka}{Pientka}{2003b}]{Pientka03phd}
{\sc Pientka, B.} 2003b.
\newblock Tabled higher-order logic programming.
\newblock Ph.D. thesis, Department of Computer Science, Carnegie Mellon
  University.
\newblock CMU-CS-03-185.

\bibitem[\protect\citeauthoryear{Pientka}{Pientka}{2005}]{Pientka:CADE05}
{\sc Pientka, B.} 2005.
\newblock Tabling for higher-order logic programming.
\newblock In {\em 20th International Conference on Automated Deduction (CADE'05)}, {R.~Nieuwenhuis}, Ed. Lecture Notes in Computer Science,
  (LNCS 3632). Springer, 54--68.

\bibitem[\protect\citeauthoryear{Pientka and Pfenning}{Pientka and
  Pfenning}{2003}]{PientkaPfenning:CADE03}
{\sc Pientka, B.} {\sc and} {\sc Pfenning, F.} 2003.
\newblock Optimizing higher-order pattern unification.
\newblock In {\em 19th International Conference on Automated Deduction
  (CADE'03), Miami, USA}, {F.~Baader}, Ed. Lecture Notes in Artificial
  Intelligence (LNAI 2741). Springer, 473--487.

\bibitem[\protect\citeauthoryear{Ramakrishnan, Rao, Sagonas, Swift, and
  Warren}{Ramakrishnan et~al\mbox{.}}{1995}]{Ramakrishnan95efficient}
{\sc Ramakrishnan, I.}, {\sc Rao, P.}, {\sc Sagonas, K.}, {\sc Swift, T.}, {\sc
  and} {\sc Warren, D.} 1995.
\newblock Efficient tabling mechanisms for logic programs.
\newblock In {\em 12th International Conference on Logic
  Programming}, {L.~.Sterling}, Ed. MIT Press, 697--711.

\bibitem[\protect\citeauthoryear{Ramakrishnan, Rao, Sagonas, Swift, and
  Warren}{Ramakrishnan et~al\mbox{.}}{1999}]{RamakrishnanJLP99}
{\sc Ramakrishnan, I.~V.}, {\sc Rao, P.}, {\sc Sagonas, K.}, {\sc Swift, T.},
  {\sc and} {\sc Warren, D.} 1999.
\newblock Efficient access mechanisms for tabled logic programs.
\newblock {\em Journal of Logic Programming\/}~{\em 38,\/}~1 (Jan), 31--54.

\bibitem[\protect\citeauthoryear{Ramakrishnan, Sekar, and
  Voronkov}{Ramakrishnan et~al\mbox{.}}{2001}]{Ramakrishnan01:indexing}
{\sc Ramakrishnan, I.~V.}, {\sc Sekar, R.}, {\sc and} {\sc Voronkov, A.} 2001.
\newblock Term indexing.
\newblock In {\em Handbook of Automated Reasoning}, {A.~Robinson} {and}
  {A.~Voronkov}, Eds. Vol.~2. Elsevier Science Publishers B.V., 1853--1962.

\bibitem[\protect\citeauthoryear{Ramesh, Ramakrishnan, and Warren}{Ramesh
  et~al\mbox{.}}{1990}]{Ramesh:POPL90}
{\sc Ramesh, R.}, {\sc Ramakrishnan, I.~V.}, {\sc and} {\sc Warren, D.~S.}
  1990.
\newblock Automata-driven indexing of Prolog clauses.
\newblock In {\em 17th ACM SIGPLAN-SIGACT Symposium on
  Principles of Programming Languages (POPL'90)}. ACM Press, 
  281--291.

\bibitem[\protect\citeauthoryear{Riazanov and Voronkov}{Riazanov and
  Voronkov}{2002}]{Riazanov:02}
{\sc Riazanov, A.} {\sc and} {\sc Voronkov, A.} 2002.
\newblock The design and implementation of Vampire.
\newblock {\em AI Communications\/}~{\em 15,\/}~2, 91--110.

\bibitem[\protect\citeauthoryear{Sarkar, Pientka, and Crary}{Sarkar
  et~al\mbox{.}}{2005}]{Pientka:ICLP05}
{\sc Sarkar, S.}, {\sc Pientka, B.}, {\sc and} {\sc Crary, K.} 2005.
\newblock Small proof witnesses for LF.
\newblock In {\em 21st International Conference on Logic Programming}, {M.~Gabbrielli} {and} {G.~Gupta}, Eds. Lecture Notes in Computer
  Science (LNCS 3668). Springer-Verlag, 387--401.

\bibitem[\protect\citeauthoryear{Sterling}{Sterling}{2007}]{Sterling:LICS07}
{\sc Sterling, C.} 2007.
\newblock Higher-order matching, games and automata.
\newblock In {\em 22nd Annual IEEE Symposium on Logic in Computer Science
  (LICS'07)}. IEEE Computer Society Press, 326--335.

\bibitem[\protect\citeauthoryear{Stickel}{Stickel}{1989}]{AICPub498:1989}
{\sc Stickel, M.~E.} 1989.
\newblock The path-indexing method for indexing terms.
\newblock Tech. Rep. 473, AI Center, SRI International, 333 Ravenswood Ave.,
  Menlo Park, CA 94025. Oct.

\bibitem[\protect\citeauthoryear{Theiss and Benzm{\"u}ller}{Theiss and
  Benzm{\"u}ller}{2006}]{Theiss:IWIL06}
{\sc Theiss, F.} {\sc and} {\sc Benzm{\"u}ller, C.} 2006.
\newblock {T}erm {I}ndexing for the {LEO}-{II} {P}rover.
\newblock In {\em 6th International Workshop on the Implementation of Logics}.


\bibitem[\protect\citeauthoryear{Warren}{Warren}{1999}]{Warren+book99}
{\sc Warren, D.~S.} 1999.
\newblock {\em Programming in tabled logic programming}.
\newblock draft available from
  http://www.cs.sunysb.edu/\~warren/xsbbook/book.html.

\bibitem[\protect\citeauthoryear{Watkins, Cervesato, Pfenning, and
  Walker}{Watkins et~al\mbox{.}}{2002}]{Watkins02tr}
{\sc Watkins, K.}, {\sc Cervesato, I.}, {\sc Pfenning, F.}, {\sc and} {\sc
  Walker, D.} 2002.
\newblock A concurrent logical framework {I}: Judgments and properties.
\newblock Tech. Rep. CMU-CS-02-101, Department of Computer Science, Carnegie
  Mellon University.

\end{thebibliography}



\begin{received}
Received August 2007 ;
revised June 2008;
accepted October 2008;
\end{received}

\elecappendix
%
%
%
%

\section{Detailled proofs of previous theorems }

\begin{theorem}[Soundness of mslg for objects]\mbox{}

\mbox{\textsc{(previous Thm. \ref{lemma:mslgTermSound} on page \pageref{lemma:mslgTermSound})}}

%
%
  \begin{enumerate}
  \item If $(\Delta, \Omega); \Gamma \vd M_1 \aunif M_2 \hastype A \ares M
/ (\Omega', \theta_1, \theta_2)$ and\\
\mbox{\hspace{0.5cm}}$(\Delta, \Omega); \Gamma \vd M_1 \chk A$ and 
   $(\Delta, \Omega); \Gamma \vd M_2 \chk A$ \\
then $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and 
     $(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ and \\
\mbox{\hspace{0.7cm}}$ M_1 = \msub{\theta_1}M$
and $M_2 = \msub{\theta_2}M$  and $(\Delta, \Omega');
\Gamma \vd M \chk A$ . 
%
  \item If $(\Delta, \Omega); \Gamma \vd R_1 \aunifR R_2 \hastype P \ares R
/ (\Omega', \theta_1, \theta_2)$ and\\
\mbox{\hspace{0.5cm}}$(\Delta, \Omega); \Gamma \vd R_1 \syn P$ and 
   $(\Delta, \Omega); \Gamma \vd R_2 \syn P$ \\
then $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and 
     $(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ and \\
\mbox{\hspace{0.7cm}}$ R_1 = \msub{\theta_1}R$
and $R_2 = \msub{\theta_2}R$  and $(\Delta,\Omega');
\Gamma \vd R \syn P$.
%
\item If $(\Delta, \Omega); \Gamma \vd S_1 \aunifS S_2 \hastype A
  > P \ares S / (\Omega', \theta_1, \theta_2)$ and \\
\mbox{\hspace{0.5cm}}$(\Delta, \Omega); \Gamma \vd S_1 > A \syn P$ and 
   $(\Delta, \Omega); \Gamma \vd S_2 > A \syn P$ \\
then $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and 
$(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ and \\
\mbox{\hspace{0.7cm}}$(\Delta, \Omega'); \Gamma \vd S > A \syn P$ 
and $S_1 = \msub{\theta_1}S$ and $S_2 = \msub{\theta_2}S$.
  \end{enumerate}
\end{theorem}
%
%
\begin{proof}
  Simultaneous induction on the structure of the first derivation. 

We give here a few cases. 

\paragraph*{Case} $\D = (\Delta, \Omega); \Gamma \vd \lambda x. M_1 \aunif
  \lambda x. M_2 \hastype A_1 \arrow A_2 \ares \lambda x. M / (\Omega', \theta_1, \theta_2)$ \nnll
%
%
$(\Delta, \Omega) ; \Gamma, x\oftp A_1 \vd M_1 \aunif M_2 \hastype
A_2 \ares M / (\Omega', \theta_1, \theta_2)$ \hfill by premise\nnl
$(\Delta, \Omega) ; \Gamma \vd \lambda x. M_1 \chk A_1 \arrow A_2$ \hfill  by assumption \nnl
$(\Delta, \Omega) ; \Gamma, x\oftp A_1 \vd M_1 \chk A_2$ \hfill by inversion \nnl
$(\Delta, \Omega) ; \Gamma \vd \lambda x. M_2 \chk A_1 \arrow A_2$ \hfill by assumption \nnl
$(\Delta, \Omega) ; \Gamma, x\oftp A_1 \vd M_2 \chk A_2$ \hfill by inversion\nnl
$(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ \hfill by i.h. \nnl
$(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ \hfill by i.h. \\
$M_1 = \msub{\theta_1}M$ \hfill by i.h. \nnl
$\lambda x. M_1 = \lambda x. \msub{\theta_1}M$ \hfill by rule\nnl
$\lambda x. M_1 =  \msub{\theta_1}(\lambda x.M)$ \hfill
by contextual substitution definition\\ 
$M_2 = \msub{\theta_2}M$ \hfill by i.h. \nnl
$\lambda x. M_2 = \lambda x. \msub{\theta_2}M$ \hfill by rule\nnl
$\lambda x. M_2 = \msub{\theta_2}(\lambda x.M)$ \hfill
 by contextual substitution definition \nnl
$(\Delta , \Omega') ; \Gamma, x\oftp A_1 \vd M \chk A_2$ \hfill by i.h.\nnl
$(\Delta , \Omega') ; \Gamma \vd \lambda x.M \chk A_1 \arrow A_2$ \hfill by rule
%

\paragraph*{Case} $\D = (\Delta ; \Omega) ; \Gamma \vd R_1 \aunif R_2 : P \ares R / (\Omega', \theta_1, \theta_2)$\nnll
%
$(\Delta , \Omega) ; \Gamma \vd R_1 \aunifR R_2 : P \ares R / (\Omega', \theta_1, \theta_2)$\hfill by premise\nnl
$(\Delta , \Omega) ; \Gamma \vd R_1 \chk P$ \hfill by ass \nnl
$(\Delta , \Omega) ; \Gamma \vd R_1 \syn P$  \hfill by
rule \nnl
$(\Delta , \Omega) ; \Gamma \vd R_2 \chk P$ \hfill by ass \nnl
$(\Delta , \Omega) ; \Gamma \vd R_2 \syn P$  \hfill by rule \nnl
$(\Delta , \Omega) \vd \theta_1 \chk \Omega'$ \hfill by i.h. \nnl
$(\Delta , \Omega) \vd \theta_2 \chk \Omega'$ and \nnl
$R_1 = \msub{\theta_1}R$ and $R_2 = \msub{\theta_2}R$  and $(\Omega', \Delta ); \Gamma \vd R \syn P$ \nnl
$(\Delta, \Omega' ); \Gamma \vd R \chk P$ \hfill by rule
% 

\paragraph*{Case} $\D = (\Delta, \Omega); \Gamma \vd u[\pi_\Gamma] \aunifR u[\pi_\Gamma] \hastype P 
                         \ares u[\pi_\Gamma] / (\cdot, \cdot, \cdot)$\nnll
%
$u \ofvd P[\Psi] \in \Delta$ and $\Delta ; \Gamma \vd \pi \chk \Psi$\hfill by premise \nnl
$(\Delta, \Omega) ; \Gamma \vd u[\pi_\Gamma] \syn P$ \hfill by assumption\nnl
$ u[\pi_\Gamma] = u[\pi_\Gamma] $ \hfill by reflexivity \nnl
$(\Delta, \Omega) \vd \cdot \chk \cdot$ \hfill by rule\nnl
$\Delta ; \Gamma \vd u[\pi_\Gamma]\syn P$\hfill by rule\nnl
%

\paragraph*{Case} $\D = (\Delta, \Omega); \Gamma \vd u[\pi_\Gamma] \aunifR
  R \hastype P \ares i[\id_\Gamma] / (i\ofvd P[\Gamma],\;
  \Gammahat.u[\pi_\Gamma]/i,\;\Gammahat.R/i)$\nnll
%
$u \ofvd P[\Psi] \in \Delta$ and $\Delta ; \Gamma \vd \pi \chk \Psi$\hfill by premise \nnl
$(\Delta, \Omega) ; \Gamma \vd u[\pi_\Gamma] \syn P$ \hfill by assumption\nnl
$(\Delta, \Omega) ; \Gamma \vd R \syn P$ \hfill by assumption\nnl
$(\Delta, \Omega) ; \Gamma \vd R \chk P$ \hfill by rule\nnl
$(\Delta, \Omega) ; \Gamma \vd u[\pi_\Gamma] \chk P$ \hfill by rule\nnl
$u[\pi_\Gamma] = \msub{\Gammahat.u[\pi_\Gamma]/i}i[\id_\Gamma]$ \hfill \nnl
$u[\pi_\Gamma] = u[\pi_\Gamma]$ \hfill by reflexivity \nnl
%
$R = \msub{\Gammahat.R/i}i[\id_\Gamma]$ \hfill \nnl
$R =  R$ \hfill by reflexivity \nnl
%
$(\Delta, \Omega) \vd \Gammahat.R/i \chk i\ofvd P[\Gamma]$ \hfill by rule using assumption
\nnl
$(\Delta, \Omega) \vd u[\pi_\Gamma]/i \chk i\ofvd P[\Gamma]$ \hfill by rule using assumption\nnl
$(\Delta, i\ofvd P[\Gamma]) ; \Gamma \vd \id_\Gamma
\chk \Gamma$ \hfill by definition\nnl
$(\Delta, i\ofvd P[\Gamma]) ; \Gamma \vd i[\id_\Gamma]\syn P$  \hfill by rule\\
%

\paragraph*{Case} $\D = (\Delta, \Omega) ; \Gamma \vd c \cdot S_1 \aunifR
  c \cdot S_2 \hastype P \ares c\cdot S / (\Omega',\;\theta_1,\;\theta_2)$\nnll
%
$(\Delta, \Omega); \Gamma \vd S_1 \aunifR S_2 \hastype A > P
\ares S / (\Omega', \theta_1, \theta_2)$ \hfill by premise \nnl
$(\Delta, \Omega); \Gamma \vd c\cdot S_1 \syn P$ \hfill by assumption\nnl
$(\Delta, \Omega); \Gamma \vd S_1 > A \syn P$ \hfill by inversion\nnl
$(\Delta, \Omega); \Gamma \vd c\cdot S_2 \syn P$ \hfill by assumption\nnl
$(\Delta, \Omega); \Gamma \vd S_2 > A \syn P$ \hfill by inversion\nnl
$S_1 = \msub{\theta_1}S$ \hfill by i.h. \nnl
$S_2 = \msub{\theta_2}S$ \hfill by i.h. \nnl
$(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ \hfill by i.h.\nnl
$(\Delta, \Omega) \vd \theta_2 \chk \Omega'$ \hfill by i.h.\nnl
%
$c\cdot S_1 = c\cdot \;\msub{\theta_1}S$ \hfill by rule \nnl 
$c\cdot S_1 = \msub{\theta_1}(c\cdot S)$ \hfill by contextual substitution definition \nnl
%
$c\cdot S_2 = c\cdot \;\msub{\theta_2}S $\hfill by rule \nnl
$c\cdot S_2 =  \msub{\theta_2}(c\cdot\;S)$ \hfill
 by contextual substitution definition \nnl
$(\Delta , \Omega') ; \Gamma \vd S > A \syn P$ \hfill by i.h.\nnl
$(\Delta , \Omega') ; \Gamma \vd c \cdot S \syn  P$\hfill by rule 
%

\paragraph*{Case} $\D = (\Delta, \Omega);\Gamma \vd R_1 \aunifR R_2
   \hastype P \ares i[\id_\Gamma] / (i\ofvd P[\Gamma] ,\;\Gammahat.R_1 /i,\;\Gammahat.R_2/i)$\nnll
%
$R_1 = H_1 \cdot S_1$ and $R_2 = H_2 \cdot S_2$ and $H_1 \neq H_2$ \hfill by premise\nnl
$(\Delta, \Omega) ; \Gamma \vd H_1 \cdot S_1 \syn P$ 
\hfill by assumption\nnl
$(\Delta, \Omega) ; \Gamma \vd H_1 \cdot S_1 \chk P$ \hfill by rule \nnl
$(\Delta, \Omega) ; \Gamma \vd H_2 \cdot S_2 \syn P$
\hfill by assumption\nnl
$(\Delta, \Omega) ; \Gamma \vd H_2 \cdot S_2 \chk P$ \hfill by rule \nnl
$H_1 \cdot S_1 = \msub{\Gammahat.(H_1 \cdot  S_1)/i}(i[\id_\Gamma])$ \hfill by contextual substitution definition\nnl
%
$H_1 \cdot S_1 = H_1 \cdot  S_1$ \hfill by reflexivity\nnl
%
$H_2 \cdot S_2 = \msub{\Gammahat.(H_2 \cdot S_2)/i}(i[\id_\Gamma])$ \hfill by contextual substitution definition\nnl
%
$H_2 \cdot S_2 = H_2 \cdot  S_2 $ \hfill by reflexivity\nnl
$(\Delta, i\ofvd P[\Gamma]); \Gamma \vd \id_\Gamma \chk \Gamma$ \hfill by definition\nnl
$(\Delta, i\ofvd P[\Gamma]); \Gamma \vd i[\id_\Gamma] \syn P$ \hfill by rule 
%

\paragraph*{Case} $\D = (\Delta, \Omega); \Gamma \vd (M_1 ; S_1) \aunifS
  (M_2; S_2) \hastype (A_1 \arrow A_2) > P $\\
  \mbox{\hspace{7.5cm}$\ares (M ; S) / (\Omega', \theta, \theta')$}\nnll
%
$ (\Delta, \Omega); \Gamma \vd M_1 \aunif M_2 \hastype A_1  \ares M  /
  (\Omega_1, \;\theta_1,\;\theta_2)$ \hfill by premise\nnl
$(\Delta, \Omega); \Gamma \vd S_1 \aunifS S_2 \hastype A_2 > P  \ares S  /
  (\Omega_2, \;\theta'_1,\;\theta'_2)$ \hfill \nnl
$\Omega' = (\Omega_1, \Omega_2)$, $\theta = (\theta_1, \theta'_1)$,
$\theta'= (\theta_2,\theta'_2)$ \hfill \nnl
$(\Delta, \Omega); \Gamma \vd (M_1 ; S_1) > A_1 \arrow A_2 \syn P$\hfill by
assumption \nnl
$(\Delta, \Omega); \Gamma \vd M_1 \chk A_1$ \hfill by inversion\nnl
$(\Delta, \Omega); \Gamma \vd S_1 > A_2 \syn P$ \hfill \nnl
%
$(\Delta, \Omega); \Gamma \vd (M_2 ; S_2) > A_1 \arrow A_2 \syn P$ \hfill by
assumption \nnl
$(\Delta, \Omega); \Gamma \vd M_2 \chk A_1$ \hfill by inversion\nnl
$(\Delta, \Omega); \Gamma \vd S_2 > A_2 \syn P$ \hfill \nnl
$M_1 = \msub{\theta_1}M$ \hfill  by i.h.\nnl
$M_2 = \msub{\theta_2}M$ \hfill  by i.h.\nnl
$(\Delta, \Omega_1) ; \Gamma \vd M \chk A_1$ \hfill  by i.h. \nnl
$(\Delta, \Omega) \vd \theta_1 \chk \Omega_1$ \hfill by i.h.\nnl
$(\Delta, \Omega) \vd \theta_2 \chk \Omega_1$ \hfill by i.h.\nnl
$(\Delta, \Omega') ; \Gamma \vd M \chk A_1$ \hfill  by weakening \nnl
%
$S_1 = \msub{\theta'_1}S$ \hfill  by i.h.\nnl
$S_2 = \msub{\theta'_2}S$ \hfill  by i.h.\nnl
$(\Delta, \Omega_2) ; \Gamma \vd S > A_2 \syn P$ \hfill  by i.h. \nnl
$(\Delta, \Omega) \vd \theta'_1 \chk \Omega_2$ \hfill by i.h.\nnl
$(\Delta, \Omega) \vd \theta'_2 \chk \Omega_2$ \hfill by i.h.\nnl
$(\Delta, \Omega',) ; \Gamma \vd S > A_2 \syn P$ \hfill  by weakening \nnl 
%
$(\Delta, \Omega) \vd (\theta_1, \theta'_1) \chk \Omega'$ \hfill  $\theta_1$ and $\theta'_1$
refer to distinct meta-variables\nnl
\mbox{\hspace{1cm}}\hfill  by typing rules for contextual substitutions\nnl
$(\Delta, \Omega) \vd (\theta_2, \theta'_2)  \chk \Omega'$  \hfill 
  $\theta_2$ and $\theta'_2$ refer to distinct meta-variables \nnl
\mbox{\hspace{1cm}}\hfill by typing rules for contextual substitutions\nnl
%
$M_1 = \msub{\theta_1, \theta'_1}M$ \hfill by  lemma weakening
%
\nnl
$M_2 = \msub{\theta_2,\theta'_2}M$ \hfill  by lemma weakening
%
\nnl
%
$S_1 = \msub{\theta_1, \theta'_1}S$ \hfill   by lemma weakening
%
\nnl
$S_2 = \msub{\theta_2, \theta'_2}S$ \hfill   by lemma weakening
% 
\nnl
%
$(M_1 ; S_1) = (\msub{\theta_1, \theta'_1}M ; \msub{\theta_1, \theta'_1}S)$ \hfill  by rule
\nnl
$(M_1 ; S_1) = \msub{\theta_1, \theta'_1}(M ;S)$ \hfill  by contextual substitution definition\nnl 
%
$(M_2 ; S_2) = (\msub{\theta_2, \theta'_2}M ; \msub{\theta_2, \theta'_2}S)$ \hfill  by rule\nnl
$(M_2 ; S_2) = \msub{\theta_2, \theta'_2}(M ;S)$ \hfill  by contextual substitution definition\nnl
%
$(\Delta, \Omega') ; \Gamma \vd (M\; ;\; S) > A_1 \arrow A_2 \syn P$ \hfill by rule
% 

\end{proof}

\begin{theorem}[Completeness of mslg of terms]\mbox{}

\mbox{\textsc{(previous Thm. \ref{lemma:mslgTermComplete} on page \pageref{lemma:mslgTermComplete})}}
% 
\mbox{}
\begin{enumerate}
\item If $\Delta, \Omega \vd \theta_1 \chk \Omega'$ and 
      $\Delta, \Omega \vd \theta_2 \chk \Omega'$ and 
  $\theta_1$ and $\theta_2$ are incompatible\\ and 
  $\Delta, \Omega ; \Gamma \vd M_1 \chk A$,   $\Delta ; \Gamma \vd M_2 \chk A$, and
  $\Delta, \Omega' ; \Gamma \vd M \chk A$ and \\
  $M_1 = \msub{\theta_1}M$ and $M_2 = \msub{\theta_2}M$\\
then there exists a contextual substitution $\theta^*_1$, $\theta^*_2$, and
a modal context $\Omega^*$, such that 
$(\Delta, \Omega) ; \Gamma \vd M_1 \aunif M_2 \hastype A \ares M / (\Omega^*, \theta^*_1, \theta^*_2)$
and $\theta^*_1 \subseteq \theta_1$,  $\theta^*_2 \subseteq \theta_2$ and $\Omega^* \subseteq \Omega'$
%
\item If $\Delta, \Omega \vd \theta_1 \chk \Omega'$ and 
      $\Delta, \Omega \vd \theta_2 \chk \Omega'$ and 
  $\theta_1$ and $\theta_2$ are incompatible\\ and 
  $\Delta, \Omega ; \Gamma \vd R_1 \syn P$,   $\Delta ; \Gamma \vd R_2 \syn P$, and
  $\Omega', \Delta ; \Gamma \vd R \syn P$ and \\ 
  $R_1 = \msub{\theta_1}R$ and $R_2 = \msub{\theta_2}R$\\
then there exists a contextual substitution $\theta^*_1$, $\theta^*_2$, and
a modal context $\Omega^*$, such that 
$(\Delta, \Omega) ; \Gamma \vd R_1 \aunifR R_2 \hastype P \ares R / (\Omega^*, \theta^*_1, \theta^*_2)$
and $\theta^*_1 \subseteq \theta_1$,  $\theta^*_2 \subseteq \theta_2$ and $\Omega^* \subseteq \Omega'$
%
\item If $\Delta, \Omega \vd \theta_1 \chk \Omega'$ and   
      $\Delta, \Omega \vd \theta_2 \chk \Omega'$ and
  $\theta_1$ and $\theta_2$ are incompatible and\\
  $(\Delta, \Omega) ; \Gamma \vd S_1 > A \syn P$, \;  $(\Delta, \Omega) ; \Gamma \vd S_2 > A \syn P$, and \\  $(\Delta, \Omega') ; \Gamma \vd S > A \syn P$ and 
      $S_1 = \msub{\theta_1}S$  and $S_2 = \msub{\theta_2}S$\\
then there exists a contextual substitution $\theta^*_1$, $\theta^*_2$, and
a modal context $\Omega^*$, such that $(\Delta, \Omega) ; \Gamma \vd S_1
\aunifS S_2 \hastype A \ares S / ({\Omega^*},
\theta^*_1, \theta^*_2)$ and $\theta^*_1 \subseteq \theta_1$,  $\theta^*_2 \subseteq \theta_2$ and $\Omega^* \subseteq \Omega'$.
\end{enumerate}
\end{theorem}
\begin{proof}
  Simultaneous induction on the structure of $M$, $R$, and $S$. We
  give a few cases.

\paragraph*{Case}  $R = u[\pi_\Gamma]$ and $u\ofvd P[\Gamma] \in  \Delta$
%
\nnl
$(\Delta, \Omega) ; \Gamma \vd u[\pi_\Gamma] \syn P$ \hfill by assumption\nnl
% 
$R_1 = \msub{ \theta_1}(u[\pi_\Gamma])$ \hfill by assumption\nnl
$R_1 = u[\pi_\Gamma]$ \hfill by contextual substitution definition\nnl
$R_2 = \msub{ \theta_2}(u[\pi_\Gamma])$ \hfill by assumption\nnl
$R_2 = u[\pi_\Gamma]$ \hfill by contextual substitution definition\nnl
%
$(\Delta, \Omega) ; \Gamma \vd u[\pi_\Gamma] \aunifR u[\pi_\Gamma] \hastype P
\ares u[\pi_\Gamma] / (\cdot, \cdot, \cdot)$ \hfill by rule\nnl
$\cdot \subseteq \Omega'$, $\cdot \subseteq \theta_1$,
$\cdot \subseteq \theta_2$ \hfill 
% 

 \paragraph*{Case}  $M = \lambda x.M'$.
%
\nnl
$M_1 = \msub{\theta_1}(\lambda x. M')$ \hfill by assumption\nnl
%
$M_1 = \lambda x. \msub{\theta_1}M'$ \hfill by contextual substitution definition\nnl
%
$M'_1 = \msub{ \theta_1}M'$ and $M_1 = \lambda x.M'_1$ \hfill by inversion\nnl
%
$M_2 = \msub{\theta_2}(\lambda x. M')$ \hfill by assumption\nnl
%
$M_2 = \lambda x. \msub{\theta_2}M'$ \hfill by contextual substitution definition\nnl
%
$M'_2 = \msub{\theta_2}M'$ and $M_2 = \lambda x.M'_2$ \hfill by inversion\nnl
%
$(\Delta, \Omega') ; \Gamma \vd \lambda x.M' \chk A_1 \arrow A_2$ \hfill by assumption \nnl
$(\Delta, \Omega') ; \Gamma, x{:}A_1 \vd M' \chk  A_2$ \hfill by inversion \nnl
$(\Delta, \Omega) ; \Gamma \vd \lambda x.M'_1 \chk A_1 \arrow A_2$ \hfill by assumption \nnl
$(\Delta, \Omega) ; \Gamma, x{:}A_1 \vd M'_1 \chk  A_2$ \hfill by inversion \nnl
$(\Delta, \Omega) ; \Gamma \vd \lambda x.M'_2 \chk A_1 \arrow A_2$ \hfill by assumption \nnl
$(\Delta, \Omega) ; \Gamma, x{:}A_1 \vd M'_2 \chk  A_2$ \hfill by inversion \nnl
%
$(\Delta, \Omega); \Gamma, x\oftp A_1 \vd M'_1 \aunif M'_2
\hastype A_2 \ares M' / (\Omega^*, \theta^*_1, \theta^*_2)$ \hfill by i.h.\nnl
$\Omega^* \subseteq \Omega'$, $\theta^*_1 \subseteq  \theta_1$, $\theta^*_2 \subseteq \theta_2$ \nnl
$(\Delta, \Omega); \Gamma\vd \lambda x.M'_1 \aunif \lambda x.M'_2
\hastype A_1 \arrow A_2 \ares \lambda x.M' / (\Omega^*, \theta^*_1, \theta^*_2)$ \hfill by rule
% 

\paragraph*{Case}  $R = i[\id_\Gamma]$
%
\nnl
$(\Delta ; \Omega) ; \Gamma \vd i[\id_\Gamma] \syn P$ \hfill by assumption\nnl
$i\ofvd P[\Gamma] \in \Omega$ \hfill by inversion \nnl
$R_1 = \msub{\theta_1}(i[\id_\Gamma])$ \hfill by assumption \nnl
%
$R_2 = \msub{\theta_2}(i[\id_\Gamma])$ \hfill by assumption \nnl
$\Gammahat.R'/i \in \theta_1$ and $\Gammahat.R''/i \in \theta_2$ \hfill by assumption\nnl
$R'$ and $R''$ are incompatible \hfill by assumption\nnl
$R_1 = R'$ \hfill by contextual substitution definition \nnl
$R_2 = R''$ \hfill by contextual substitution definition 

\paragraph*{Sub-Case 1}: $R_1 = u[\pi_\Gamma]$ and $R_2 = R''$\nnl
%
$(\Delta, \Omega); \Gamma  \vd u[\pi_\Gamma] \aunifR R'' \hastype P \ares i[\id_\Gamma] / (i\ofvd P[\Gamma],  \Gammahat.u[\pi_\Gamma]/i, \Gammahat.R''/i)$ \hfill by rule\nnl
$i\ofvd P[\Gamma] \subseteq \Omega'$, $
  (\Gammahat.u[\pi_\Gamma]/i) \subseteq \theta_1$, $(\Gammahat.R''/i) \subseteq \theta_2$\hfill

\paragraph*{Sub-Case 2}: $R_1 = R'$ and $R_2 = u[\pi_\Gamma]$\nnl
$(\Delta, \Omega); \Gamma  \vd R' \aunifR u[\pi_\Gamma] \hastype P \ares i[\id_\Gamma] / (i\ofvd P[\Gamma],   \Gammahat.R'/i, \Gammahat.u[\pi_\Gamma]/i)$ \hfill by rule\nnl
$(i\ofvd P[\Gamma] \subseteq \Omega'$, 
$(\Gammahat.u[\pi_\Gamma]/i) \subseteq \theta_2$, $(\Gammahat.R'/i)
\subseteq \theta_1$ 


\paragraph*{Sub-Case 3}: $R_1 = H_1 \cdot S_1$ and $R_2 = H_2\cdot S_2$\nnl
%
$H_1\cdot S_1$ is incompatible with $H_2\cdot S_2$ and $H_1 \neq H_2$ \hfill by assumption\nnl
$(\Delta, \Omega); \Gamma  \vd H_1 \cdot S_1 \aunifR
  H_2\cdot S_2 \hastype P \ares i[\id_\Gamma] / (i\ofvd P[\Gamma],  \Gammahat.(H_1\cdot S_1)/i, \Gammahat.(H_2\cdot S_2)/i)$
\hfill \nnl \mbox{\hspace{1cm}} \hfill by rule\nnl
$(i\ofvd P[\Gamma]) \subseteq \Omega'$,
  $(\Gammahat.H_1\cdot S_1/i)\subseteq \theta_1$, $(\Gammahat.H_2\cdot S_2/i) \subseteq \theta_2$
%

\end{proof}

\begin{theorem}[Soundness for mslg of substitutions]
\mbox{}

\mbox{\textsc{(previous Thm. \ref{lemma:mslgSubSound} on page \pageref{lemma:mslgSubSound})}}
% 
\mbox{}\\
If $(\Delta, \Omega_1) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_2 \ares
\rho / (\Omega, \theta_1, \theta_2)$ and \\ \mbox{\hspace{0.5cm}}$(\Delta, \Omega_1) \vd \rho_1 \chk \Omega_2$ and 
$(\Delta, \Omega_1) \vd \rho_2 \chk \Omega_2$ \\
%
then  $(\Delta,\Omega) \vdash \rho \chk \Omega_2$, $(\Delta,\Omega_1)
\vdash \theta_1 \chk \Omega$, $(\Delta, \Omega_1) \vdash \theta_2 \chk
\Omega$, and \\ \mbox{\hspace{0.5cm}}$\msub{\theta_1}\rho = \rho_1$ and $\msub{\theta_2}\rho = \rho_2$
\end{theorem}
\begin{proof}
  Induction on the first derivation.

\paragraph*{Case}  $\D = (\Delta, \Omega_1) \vd \cdot \hastype \cdot \ares \cdot /
  (\cdot, \cdot, \cdot)$ \nnl
%
%
$\cdot = \cdot$  \hfill by syntactic equality\\
$\cdot = \msub{\cdot}(\cdot)$ \hfill contextual substitution definition
% \nnl

\paragraph*{Case} 
$\D = (\Delta, \Omega_1) \vd (\rho_1, \Psihat.R_1/i) \aunifSub (\rho_2,
\Psihat.R_2/i)\hastype (\Omega_2, i\ofvd P[\Psi])$\\
\mbox{\hspace{1cm}}\hfill $ \ares (\rho, \Psihat.R/i) /((\Omega, \Omega'), (\theta_1, \theta'_1), (\theta_2, \theta'_2))$\nnl
%
$(\Delta, \Omega_1) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_2
\ares \rho / (\Omega, \theta_1, \theta_2)$ \hfill by premise \nnl
$(\Delta, \Omega_1); \Psi \vd R_1 \aunifR R_2 \hastype P \ares R / (\Omega', \theta'_1, \theta'_2)$ \hfill by premise\nnl
%
$(\Delta, \Omega_1) \vd (\rho_1, \Psihat.R_1/i) \chk (\Omega_2, i\ofvd P[\Psi])$ \hfill by assumption \nnl
%
$(\Delta, \Omega_1) \vd \rho_1 \chk \Omega_2 $ \hfill by inversion \nnl
$(\Delta, \Omega_1); \Psi \vd R_1 \chk P$ \hfill  \nnl
%
$(\Delta, \Omega_1); \Psi \vd R_1 \syn P$\hfill by inversion \nnl
%
$(\Delta, \Omega_1) \vd (\rho_2, \Psihat.R_2/i) \chk (\Omega_2, i\ofvd P[\Psi])$ \hfill by assumption \nnl
%
$(\Delta, \Omega_1) \vd \rho_2 \chk \Omega_2 $ \hfill by inversion \nnl
$(\Delta, \Omega_1); \Psi \vd R_2 \syn P$\hfill  \nnl
%
$(\Delta, \Omega') ; \Psi \vdash R \syn P$ \hfill by
soundness theorem \ref{lemma:mslgTermSound} \nnl
$(\Delta, \Omega') ; \Psi \vdash R \chk P$  \hfill by rule \nnl
%
$R_1 = \msub{\theta'_1}R$, $\Delta, \Omega_1 \vdash \theta_1' \chk
\Omega'$ \hfill by soundness theorem \ref{lemma:mslgTermSound} \nnl
$R_2 = \msub{\theta'_2}R$, $\Delta, \Omega_1 \vdash \theta_2' \chk
\Omega'$ \hfill by soundness theorem \ref{lemma:mslgTermSound} \nnl
$R_1 = \msub{\theta_1, \theta'_1}R$ \hfill by weakening \nnl
$R_2 = \msub{\theta_2, \theta'_2}R$ \hfill by weakening \nnl
%
$\rho_1 = \msub{\theta_1}\rho$ \hfill by i.h. \nnl
$\rho_2 = \msub{\theta_2}\rho$ \hfill by i.h. \nnl
%
%
$\rho_1 = \msub{\theta_1, \theta'_1}\rho
$ \hfill by weakening lemma % \ref{lemma:weakModSub2} 
\nnl
$\rho_2 = \msub{\theta_2,\theta'_2}\rho$ \hfill by weakening lemma 
%
\nnl
%
$(\rho_1, \Psihat.R_1/i) = (\msub{\theta_1, \theta'_1}\rho,
\; \msub{\theta_1, \theta'_1}\Psihat.R/i)$  \hfill by rule \nnl
$(\rho_2, \Psihat.R_2/i) = (\msub{\theta_2,\theta'_2}\rho,
\; \msub{\theta_2, \theta'_2}\Psihat.R/i)$ \hfill by rule \nnl
%
$(\rho_1, \Psihat.R_1/i) = \msub{\theta_1, \theta'_1}(\rho,\Psihat.R/i)
$ \hfill by contextual substitution definition\nnl
$(\rho_2, \Psihat.R_2/i) = \msub{\theta_2,\theta'_2}(\rho, \Psihat.R/i)
$ \hfill by contextual substitution definition \nnl
$(\Delta, \Omega) \vd \rho \chk \Omega_2$ \hfill by i.h.\nnl
%
%
$(\Delta, \Omega, \Omega') \vd \rho \chk \Omega_2$ \hfill by weakening\nnl
$(\Delta, \Omega, \Omega') ; \Psi \vd R \chk P$ \hfill by weakening\nnl
$(\Delta, \Omega, \Omega') \vd (\rho, \Psihat.R/i) \chk (\Omega_2,
i\ofvd P[\Psi])$\hfill by rule \nnl
%
$\Delta, \Omega_1) \vd (\theta_1, \theta_1') \chk (\Omega, \Omega') $
\hfill by typing rules\nnl
$\Delta, \Omega_1) \vd (\theta_2, \theta_2') \chk (\Omega, \Omega') $
\hfill by typing rules

%
%
\end{proof}


\begin{theorem}[Completeness for mslg of contextual
  substitutions]\mbox{}

\mbox{\textsc{(previous Thm. \ref{lemma:mslgSubComplete} on page
    \pageref{lemma:mslgSubComplete})}}

%\label{lemma:mslgSubComplete}

If $(\Delta, \Omega) \vd \theta_1 \chk \Omega'$ and $(\Delta,
\Omega) \vd \theta_2 \chk \Omega'$ and $\theta_1$ and $\theta_2$
are incompatible and\\ $\rho_1 = \msub{\theta_1}\rho$ and 
 $\rho_2 =  \msub{\theta_2}\rho$ then 
 $(\Delta, \Omega) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_1 \ares
 \rho / (\Omega^*, \theta_1^*, \theta_2^*)$ such that $\Omega^*
 \subseteq \Omega'$, $\theta_1^* \subseteq \theta_1$, $\theta_2^*
 \subseteq \theta_2$.
\end{theorem}
%
\begin{proof}
  Induction on the structure of $\rho$.

\paragraph*{Case}  $\rho = \cdot$ \nnll
%
$\rho_1 = \msub{\theta_1}(\cdot)$ \hfill by assumption\nnl
 $\rho_1 = \cdot$ and $\Omega_1 = \cdot$ \hfill by inversion\nnl
%
$\rho_2 = \msub{\theta_2}(\cdot)$ \hfill by assumption\nnl
$\rho_2 = \cdot$ and $\Omega_1 = \cdot$ \hfill by inversion\nnl
%
$(\Delta, \Omega) \vd \cdot \aunifSub \cdot \hastype \cdot \ares \cdot
/ (\cdot, \cdot, \cdot)$ \hfill by rule\nnl
$\cdot \subseteq \Omega_1$, $\cdot \subseteq \theta_1$, $\cdot
\subseteq \theta_2$ 
% 

\paragraph*{Case}  $\rho = (\rho', \Psihat.R/i)$\nnll
%
$\rho'_1 = \msub{\theta_1}(\rho', \Psihat.R/i)$ \hfill by assumption \nnl
$\rho'_1 = (\msub{ \theta_1}(\rho'),\;\Psihat.\msub{\theta_1}R/i)$ \hfill by contextual substitution definition\nnl
$\rho'_1 = (\rho_1, \Psihat.R_1/i)$\hfill by equality \nnl
$\rho_1 = \msub{\theta_1}\rho'$ \hfill \nnl
$R_1 = \msub{\theta_1}R$ \hfill \nnl
$\rho'_2 = \msub{\theta_2}(\rho', \Psihat.R/i)$ \hfill by assumption \nnl
$\rho'_2 = (\msub{\theta_2}(\rho'),\;\Psihat.\msub{\theta_2}R/i)$ \hfill by contextual substitution definition\nnl
$\rho'_2 = (\rho_2, \Psihat.R_2/i)$ \hfill by equality \nnl
$\rho_2 = \msub{\theta_2}\rho'$ \hfill \nnl
$R_2 = \msub{\theta_2}R$ \hfill \nnl
$(\Delta, \Omega) ; \Psi \vd R_1 \aunifR R_2 \hastype P \ares R /
(\Omega^*, \theta_1^*, \theta_2^*)$ \hfill by completeness lemma
\ref{lemma:mslgTermComplete} \nnl
$\Omega^* \subseteq \Omega'$, $\theta_1^* \subseteq \theta_1$,
$\theta_2^* \subseteq \theta_2$ \hfill \nnl
%
$(\Delta, \Omega) \vd \rho_1 \aunifSub \rho_2 \hastype \Omega_1 \ares \rho' /
(\Omega^{**}, \theta_1^{**}, \theta_2^{**})$ \hfill by i.h. \nnl
$\Omega^{**} \subseteq \Omega'$, $\theta_1^{**} \subseteq \theta_1$,
$\theta_2^{**} \subseteq \theta_2 $ \hfill\nnl
$(\Delta, \Omega) \vd (\rho_1, \Psihat.R_1/i) \aunifSub (\rho_2, \Psihat.R_2/i) \hastype
(\Omega_1, i\ofvd P[\Psi])$\nnl
\hfill $\ares (\rho', \Psihat.R/i) /
((\Omega^{**}, \Omega^{*}), \; (\theta_1^{**},\theta_1^{*}),\;
(\theta_2^{**},\theta_2^{*}))$\hfill by rule\nnl
%
$(\Omega^{**}, \Omega^{*}) \subseteq \Omega'$, $(\theta_1^{**}, \theta_1^*) \subseteq \theta_1$,
$(\theta_2^{**}, \theta_2^{*}) \subseteq \theta_2$ \hfill

%
\end{proof}


\begin{lemma}[Insertion of substitution into tree]\mbox{}

\mbox{\textsc{(previous Lemma \ref{lemma:childInsert} on page \pageref{lemma:childInsert})}}
%

If $\Delta \vd C \aunif \delta \hastype \Omega \ares (V, S)$ and 
$\Delta \vd \delta \chk \Omega$ and for any $(\Omega_i \turn \rho_i
\tto C') \in C$ with $\Delta, \Omega_i \vd \rho_i \chk \Omega$ then 
  \begin{enumerate}
  \item for any $(N_i, \theta_2) \in V$ where $N_i = (\Omega_i \vd \rho_i \tto
    C_i)$, we have $\msub{\theta_2}\rho_i = \delta$.
  \item for any $(N_i, \Omega' \vd \rho', \theta_1, \theta_2) \in S$
    where $N_i = (\Omega_i \vd \rho_i \tto C_i)$, we have
    $\msub{\theta_2}\rho' = \delta$ and $\msub{\theta_1}\rho' = \rho_i$.
  \end{enumerate}
\end{lemma}
\begin{proof}
By structural induction on the first derivation and by using the
previous soundness lemma for mslg of substitutions (lemma
\ref{lemma:mslgSubSound}).

\paragraph*{Case} 
 $\D = \ianc{}{\Delta \vd \nil \aunif \delta \hastype \Omega \ares (\cdot, \cdot)}{}$.

Trivially true.

\paragraph*{Case}
 $\D = \ianc{\begin{array}{lrl}
   \Delta & \vd C \aunif \delta \hastype \Omega & \ares (V, S) \\
   \Delta, \Omega_1 & \vd \rho_1  \aunifSub \delta \hastype \Omega & \ares
   \id_{\Omega} / (\Omega, \rho_1, \delta) 
   \end{array}}{ \Delta \vd [(\Omega_1 \turn \rho_1 \tto C_1) , C] \aunif \delta \hastype
  \Omega \ares (V, S)}{NC}$\\[1em] 
%
By i.h., for any $(N_i, \theta_2) \in V$, $N_i = (\Omega_i \vd \rho_i \tto
C_i)$, we have $\msub{\theta_2}\rho_i = \delta$ and for any $(N_i, \Omega' \vd \rho', \theta'_1, \theta'_2) \in S$
    where $N_i = (\Omega_i \vd \rho_i \tto C_i)$, we have
    $\msub{\theta'_2}\rho' = \delta$ and $\msub{\theta'_1}\rho' =
    \rho_i$. 
%
%

 \paragraph*{Case}  
% \paragraph{Case} 
$\D = \ianc{%
  \begin{array}{lrl}
  \Delta & \vd C \aunif \delta \hastype \Omega & \ares (V, S)\\
  \Delta, \Omega_1 & \vd \rho_1 \aunifSub \delta \hastype \Omega & \ares
  \rho_1 / (\Omega_1, \id_{\Omega_1}, \theta_2)
  \end{array}}{\Delta \vd
  [(\Omega_1 \turn \rho_1 \tto C_1) , C] \aunif \delta \hastype \Omega
  \ares ((V\;,\; (\Omega_1 \turn \rho_1 \tto C_1)), S)}{FC}$\\[1em] % \nnll
%
%
By i.h., for any $(N_i, \theta_2) \in V$, $N_i = (\Omega_i \vd \rho_i \tto
    C_i)$, we have $\msub{\theta_2}\rho_i = \delta$ and for any $(N_i, (\Omega' \vd \rho', \theta'_1, \theta'_2)) \in S$
    where $N_i = (\Omega_i \vd \rho_i \tto C_i)$, we have
    $\msub{\theta'_2}\rho' = \delta$ and $\msub{\theta'_1}\rho' =
    \rho_i$. By soundness lemma \ref{lemma:mslgSubSound},
    $\msub{\theta_2}\rho_1 = \delta$, therefore for any $(N_i, \theta') \in
    (V,\; ((\Omega_1 \turn \rho_1 \tto C_1), \theta_2))$, where $N_i = (\Omega_i \vd \rho_i \tto
    C_i)$ we have $\msub{\theta'}\rho_i = \delta$.
%
%

\paragraph*{Case}\mbox{} \\
 $\D = \ianc{\begin{array}{lrl}
  \Delta & \vd C \aunif \delta \hastype \Omega & \ares (V, S) \\
  \Delta, \Omega_1 & \vd \rho_1 \aunifSub \delta \hastype \Omega & \ares
  \rho^* / (\Omega_2, \theta_1, \theta_2)
  \end{array}}{\Delta \vd [(\Omega_1 \turn
  \rho_1 \tto C_1) , C] \aunif \delta \hastype \Omega \ares (V,
  (S\;,\; ((\Omega_1 \turn \rho_1 \tto C_1),  \Omega_2 \turn \rho^*,
  \theta_1, \theta_2))}{PC}$ \\[1em]% \nnll
%
%

By i.h., for any $(N_i, \theta'_2) \in V$, $N_i = (\Omega_i \vd \rho_i
\tto C_i)$, we have $\msub{\theta'_2}\rho_i = \delta$ and for any $(N_i, (\Omega' \vd \rho', \theta'_1, \theta'_2)) \in S$
where $N_i = (\Omega_i \vd \rho_i \tto C_i)$, we have $\msub{\theta'_2}\rho' = \delta$ and $\msub{\theta'_1}\rho' =
\rho_i$. By soundness lemma \ref{lemma:mslgSubSound},
$\msub{\theta_2}\rho^* = \delta$ and $\msub{\theta_1}\rho^* = \rho_1$,
therefore for any $(N_i, \Omega' \vd \rho', \theta'_1, \theta'_2) \in
(S\;,\; ((\Omega_1 \turn \rho_1 \tto C_1), \Omega_2 \turn \rho^*,
\theta_1, \theta_2))$, where $N_i = (\Omega_i \vd \rho_i \tto C_i)$ we
have $\msub{\theta'_1}\rho' = \rho_i$ and $\msub{\theta'_2}\rho' =
\delta$. 
%
%

\end{proof}


\begin{theorem}[Soundness of instance algorithm for terms]
\mbox{}

\mbox{{\textsc{(previous  Thm. \ref{lemma:ObjUnifSound} on page \pageref{lemma:ObjUnifSound})}}}
%
%

  \begin{enumerate}
  \item If $\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd M_1 \unifLHA M_2 \hastype A
    / (\theta, \rho)$ \\where
    $(\Delta_1, \Omega) ;  \Gamma \vd M_1 \chk A$ and 
    $\Delta_2 ; \Gamma \vd M_2 \chk A$ then 
    $\msub{\theta, \rho}M_1 =  M_2$.
  \item If $\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd R_1 \unifR R_2 \hastype P
    / (\theta, \rho)$  \\ where
    $(\Delta_1, \Omega) ; \Gamma \vd R_1 \syn P$ and 
    $\Delta_2 ; \Gamma \vd R_2 \syn P$ then 
    $\msub{ \theta, \rho}R_1 =   R_2$.
  \item If $\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd S_1 \unif S_2 >
    A \syn P  / (\theta, \rho)$ \\
    where $(\Delta_1, \Omega) ;  \Gamma \vd S_1 > A \syn P$ and 
    $\Delta_2 ; \Gamma \vd S_2  > A \syn P$ then $\msub{ \theta, \rho}S_1 = S_2$.
  \end{enumerate}
\end{theorem}
\begin{proof}
  Simultaneous structural induction on the first derivation. The proof

%
\paragraph*{Case}  $\D = \ianc{}{\Delta_2 ; (\Delta_1,i\ofvd P[\Gamma] ) ; \Gamma \vd
    i[\id_\Gamma] \unifR R \hastype P \;/\; (\cdot,  (\Gammahat.R/i))}{\textsf{mvar-1}}$\\[1em]
%
\nnl
%
$(\Delta_1, i\ofvd P[\Gamma]) ; \Gamma \vd i[\id_\Gamma] \syn P$ \hfill by assumption\nnl
$\Delta_2 ; \Gamma \vd R \syn P$ \hfill by assumption\nnl
$R = R$ \hfill by reflexivity \nnl
$\msub{ \Psihat.R/i}(i[\id_\Gamma]) = R$ \hfill by substitution definition 
%

\paragraph*{Case}  $\D =   \ianc{u\ofvd P[\Gamma] \in \Delta}{(\Delta, \Omega);
    \Gamma \vd u[\pi_\Gamma] \unifR R \hastype P\;/\; (\Gammahat.(\inv{[\pi_\Gamma]}R /
    u), \cdot)}{\textsf{mvar-2}}$\\[1em]
%
\nnl
%
%
$\Delta_1 ; \Gamma \vd u[\pi_\Gamma] \syn P$ where $u\ofvd P[\Gamma] \in
\Delta_1$ \hfill by assumption\nnl
$\Delta_2 ; \Gamma \vd R \syn P$ \hfill by assumption\nnl
$[\pi_\Gamma](\inv{[\pi_\Gamma]}R) = R$ \hfill by property of inversion\nnl
$\msub{ \Gammahat.\inv{[\pi_\Gamma]}R/u}(u[\pi_\Gamma]) = R$ \hfill by substitution definition

\paragraph*{Case}  $\D =   \ianc{\Delta_2 ; (\Delta_1,
    \Omega); \Gamma, x{:}A_1 \vd M_1 \unifLHA M_2 \hastype A_2\;/\;
    (\theta, \rho)}{\Delta_2 ; (\Delta_1, \Omega); \Gamma \vd \lambda x. M_1 \unifLHA  \lambda
    x. M_2 \hastype A_1 \arrow A_2\;/\;(\theta,
    \rho)}{\textsf{lam}}$\\[1em]
%
\nnl
%
$(\Delta_1, \Omega) ; \Gamma \vd \lambda x. M_1 \chk A_1 \arrow A_2$ \hfill by
assumption\nnl
$(\Delta_1, \Omega) ; \Gamma, x\oftp A_1 \vd M_1 \chk A_2$ \hfill by
inversion \nnl
$\Delta_2 ; \Gamma \vd \lambda x.M_2 \chk A_1 \arrow A_2$ \hfill
by assumption \nnl
$\Delta_2, ; \Gamma, x\oftp A_1 \vd M_2 \chk A_2$ \hfill by
inversion \nnl
$\msub{ \theta, \rho}M_1 = M_2$ \hfill by i.h.
\nnl
$\msub{\theta, \rho}\lambda x.M_1 = \msub{\theta, \rho}\lambda x.M_2$
\hfill by equality and contextual substitution definition

\paragraph*{Case}  $\D =  \Delta_2 ; (\Delta_1 , \Omega_1, \Omega_2) ; \Gamma \vdN (M_1 ; S_1) \unifLHA (M_2 ; S_2)
   \hastype A_1 \arrow A_2 > P \;$\\ 
\mbox{\hspace{1cm}}\hfill   $/\;((\theta_1,\theta_2),\, (\rho_1, \rho_2))$\nnl
%
$\Delta_2 ; (\Delta_1, \Omega_1); \Gamma \vd M_1 \unifLHA M_2 \hastype
A_1 \;/\;(\theta_1 , \rho_1)$ \nnl
$\Delta_2 ; (\Delta_1 , \Omega_2); \Gamma \vdN S_1  \unifLHA S_2 \hastype A_2 > P \;/\; (\theta_2, \rho_2)$
\hfill by premise
\nnl
%
$(\Delta_1; \Omega_1,\Omega_2) ; \Gamma \vd (M_1 ; S_1) < A_1 \arrow A_2 \syn P$
\hfill by assumption\nnl
$(\Delta_1; \Omega_1) ; \Gamma \vd M_1 \chk A_1$ \hfill by
inversion \nnl
$(\Delta_1; \Omega_2) ; \Gamma \vd S_1 < A_2 \syn P$ \hfill \nnl
%
$\Delta_2; \Gamma \vd (M_2 ; S_2) < A_1 \arrow A_2 \syn P$
\hfill by assumption\nnl
$\Delta_2 ; \Gamma \vd M_2 \chk A_1$ \hfill by
inversion \nnl
$\Delta_2 ; \Gamma \vd S_2 < A_2 \syn P$ \hfill \nnl
%
$\msub{ \theta_1, \rho_1}M_1 = M_2$ \hfill by i.h.\nnl
$\msub{ \theta_2, \rho_2}S_1 = S_2$ \hfill by i.h.\nnl
%
$\msub{ \theta_1, \theta_2,\rho_1,
\rho_2}M_1 = M_2$ \hfill by weakening (using linearity condition)\nnl
$\msub{ \theta_1, \theta_2,\rho_1,
\rho_2}S_1 = S_2$ \hfill by weakening (using linearity condition)\nnl
$\msub{ \theta_1, \theta_2,\rho_1,
\rho_2}(M_1\;S_1) = \msub{\id_{\Delta_2} \theta_1, \theta_2,\rho_1,
\rho_2}(M_2\;S_2)$\hfill
  by rule \nnl \hfill and substitution definition 


%
\end{proof}

\begin{theorem}[Completeness of instance algorithm for terms]
\mbox{}

\mbox{\textsc{(previous  Thm. \ref{lemma:compInst} on page \pageref{lemma:compInst})}}

\begin{enumerate}
\item If $(\Delta_1, \Omega) ; \Gamma  \vd M_1 \chk A$ and
  $\Delta_2; \Gamma \vd M_2\chk A$ and \\
   $\Delta_2 \vd \theta \chk \Delta_1$
  and $\Delta_2 \vd \rho \chk \Omega$ and
  $\msub{\theta,\rho}M_1 = M_2$ then\\
  $\Delta_2 ; (\Delta_1, \Omega);
  \Gamma \vd M_1 \unifLHA M_2 \hastype A / (\theta^*, \rho)$ where
  $\theta^* \subseteq \theta$.
\item If $(\Delta_1, \Omega) ; \Gamma  \vd R_1 \syn P$ and
  $\Delta_2; \Gamma \vd R_2 \syn P$ and\\
   $\Delta_2 \vd \theta \chk \Delta_1$
  and $\Delta_2 \vd \rho \chk \Omega$ and
  $\msub{\theta,\rho}R_1 = R_2$ then\\
  $\Delta_2 ; (\Delta_1, \Omega);
  \Gamma \vd R_1 \unifR R_2 \hastype P / (\theta^*, \rho)$ where
  $\theta^* \subseteq \theta$.
\item If $(\Delta_1, \Omega) ; \Gamma  \vd S_1 > A \syn P$ and
  $\Delta_2; \Gamma \vd S_2 > A \syn P$ and\\
  $\Delta_2 \vd \theta \chk \Delta_1$
  and $\Delta_2 \vd \rho \chk \Omega$ and
  $\msub{\theta,\rho}S_1 = S_2$ then\\
  $\Delta_2 ;(\Delta_1, \Omega);
  \Gamma \vd S_1 \unifLHA S_2 \hastype A > P / (\theta^*,
  \rho)$ where $\theta^* \subseteq \theta$.
\end{enumerate}
\end{theorem}
\begin{proof}
Simultaneous structural induction on the first typing derivation.


\paragraph*{Case}  $\D = \ianc{(\Delta_1, \Omega); \Gamma, x\oftp
    A_1 \vd M_1 \chk A_2}{(\Delta_1, \Omega); \Gamma \vd \lambda x.M_1
    \chk A_1 \arrow A_2}{}$% \\[1em]
%
\nnll
%
$\Delta_2 ; \Gamma \vd \lambda x.M_2 \chk A_1 \arrow A_2$
\hfill by assumption\nnl
$\Delta_2 ; \Gamma, x\oftp A_1 \vd M_2 \chk A_2$ \hfill by inversion \nnl
$\msub{\theta, \rho}(\lambda x.M_1) = \lambda x.M_2$
\hfill by assumption\nnl 
$\lambda x.\msub{\theta, \rho}(M_1) = \lambda x.M_2$\hfill by substitution definition\nnl
$\msub{\theta, \rho}(M_1) = M_2$ \hfill by syntactic equality\nnl
$\Delta_2 ; (\Delta_1, \Omega) ; \Gamma, x\oftp A_1 \vd M_1 \unifLHA M_2 \hastype A_2 /
(\theta^*, \rho^*)$ \hfill by i.h. \nnl
$\theta^* \subseteq \theta$ and $\rho^* \subseteq \rho$ \hfill \nnl
$\Delta_2 ; (\Delta_1, \Omega) ; \Gamma \vd \lambda x.M_1 \unifLHA \lambda x.M_2
\hastype A_1 \arrow A_2 /
(\theta^*, \rho^*)$ \hfill by rule \nnl

\paragraph*{Case}  $\D = \ianc{}{(\Delta_1, i\ofvd P[\Gamma]) ; \Gamma \vd i[\id_\Gamma] \syn P}{}$ \\[1em]
%
\nnl
%
% 
$i\ofvd P[\Gamma] ; \Gamma \vd i[\id_\Gamma] \syn P$ \hfill by rule \nnl
% 
$\Delta_2 ; \Gamma \vd R_2 \syn P$ \hfill by assumption\nnl
$\msub{ \theta,\rho} (i[\id_\Gamma]) = R_2$ \hfill by
assumption \nnl
$\Gammahat.R_2/i \in \rho$ \hfill by assumption\nnl
% 
$\Delta_2 ; (\Delta_1, i\ofvd P[\Gamma]) ; \Gamma \vd i[\id_\Gamma]
\unifLHA R_2 \hastype P / (\cdot, \Gammahat.R_2/i)$ \hfill by rule \nnl
$\cdot \subseteq \id_\Delta$ and $(\Gammahat.R_2/i) \subset \rho$ \hfill % \nnl

\paragraph*{Case}  $\D = \ianc{u\ofvd P[\Gamma] \in \Delta_1}{(\Delta_1, \cdot) ; \Gamma \vd u[\pi_\Gamma] \syn P}{}$ \\[1em]
%
%
\nnl
%
$u\ofvd P[\Gamma] ; \Gamma \vd u[\pi_\Gamma] \syn P$ \hfill by rule \nnl
$\Delta_1 = \Delta'_1, u\ofvd P[\Gamma], \Delta''_1$ \hfill \nnl
$\Delta_2 ; \Gamma \vd R_2 \syn P$ \hfill by assumption\nnl
$\theta = (\theta_1, \Gammahat.R/u, \theta_2)$ \hfill by assumption \nnl
$\msub{ \theta,\rho} (u[\pi_\Gamma]) = R_2$ \hfill by assumption \nnl
$[\pi_\Gamma]R = R_2$\hfill by substitution definition\nnl
$R = \inv{[\pi_\Gamma]}R_2$ and $[\pi_\Gamma](\inv{[\pi_\Gamma]}R_2) = R_2$ \hfill by inverse substitution property\nnl
$\Delta_2, u\ofvd P[\Gamma] ; \Gamma \vd u[\pi_\Gamma] \unifLHA R_2 \hastype
P / (\Gammahat.\inv{[\pi_\Gamma]}R_2/u, \cdot)$ \hfill by rule\nnl
$(\Gammahat.\inv{[\pi_\Gamma]}R_2/u) \subseteq \theta$ and $\cdot \subseteq \rho$\hfill
% 

\paragraph*{Case}  $\D = \ibnc{(\Delta_1, \Omega) ; \Gamma \vd M_1 \chk A_1}{%
(\Delta_1, \Omega); \Gamma \vdN S_1 > A \syn P}{(\Delta_1, \Omega) ; \Gamma \vdN (M_1;S_1) >  A_1 \arrow A \syn P}{}$\\[1em]
%
%
\nnl
$\msub{\theta, \rho}(M_1 ; S_1) = S'$ \hfill by
assumption\nnl
$\msub{\theta, \rho}(M_1)\;;\;\msub{\theta, \rho}(S_1) = S'$ \hfill by
substitution definition\nnl
$S' = (M_2; S_2)$ \hfill by inversion\nnl
$\msub{\theta, \rho}(M_1) = M_2$ \hfill by inversion \nnl
$\msub{\theta, \rho}(S_1) = S_2$ \hfill by inversion \nnl
$\Delta_2 ; \Gamma \vd (M_2 ; S_2) > A_1 \arrow A \syn P$ \hfill by assumption \nnl
$\Delta_2 ; \Gamma \vd M_2 \chk A_1$ \hfill by inversion \nnl
$\Delta_2 ; \Gamma \vd S_2 > A \syn P$
\hfill \nnl
%
$\Delta_2 ; (\Delta_1, \Omega_1) ; \Gamma \vd M_1 \unif M_2 \hastype A_1
/ (\theta^*_1, \rho_1)$ and $\theta^*_1 \subseteq \theta$  \hfill by i.h.\nnl
$\Delta_2 ; (\Delta_1, \Omega_2); \Gamma \vd S_1 \unif S_2 \hastype  A >
P / (\theta^*_2, \rho_2)$ and $\theta^*_2 \subseteq \theta$ \hfill by i.h.\nnl
%
$(\Delta, \Omega) ; \Gamma \vd (M_1 ; S_1) \unif (M_2 ; S_2)
\hastype A_1 \arrow A > P / ((\theta^*_1, \theta^*_2), (\rho_1, \rho_2))$ \hfill by
rule\nnl
$(\theta^*_1, \theta^*_2) \subseteq \theta$ \hfill by subset property

 \end{proof}


\begin{theorem}[Interaction between mslg and instance algorithm]\mbox{}

\mbox{\textsc{(previous Thm. \ref{lemma:interactObj} on page \pageref{lemma:interactObj})}}

\begin{enumerate}
\item If  $(\Delta_1, \Omega) ; \Gamma \vd M_1 \chk A$ and
  $\Delta_2 ; \Gamma \vd M_2 \chk A$ and  \\
$(\Delta_2 , \Delta_1), \Omega ; \Gamma \vd M_1 \aunif M_2 \hastype A \ares M
    / (\Omega', \rho_1, \rho_2)$ then \\
   $(\Delta_1 ; \Omega'; \Gamma \vd M \unif M_1 \hastype A / (\cdot,  \rho_1)$ and 
 $\Delta_2 ; \Omega'; \Gamma \vd M \unif M_2 \hastype A /
 (\cdot, \rho_2)$.

\item If  $(\Delta_1, \Omega) ; \Gamma \vd R_1 \syn P$ and
  $\Delta_2 ; \Gamma \vd R_2 \syn P$ and\\
$(\Delta_2 , \Delta_1), \Omega ; \Gamma \vd R_1 \aunifR R_2 \hastype P \ares R
    / (\Omega', \rho_1, \rho_2)$ then \\
   $\Delta_1; \Omega'; \Gamma \vd R \unifR R_1 \hastype P / (\cdot,  \rho_1)$ and 
 $\Delta_2 ; \Omega'; \Gamma \vd R \unifR R_2 \hastype P /
 (\cdot, \rho_2)$.

\item If  $(\Delta_1, \Omega) ; \Gamma \vd S_1 > A \syn P$ and
  $\Delta_2 ; \Gamma \vd S_2 > A \syn P$ and \\
$(\Delta_2, \Delta_1), \Omega; \Gamma \vd S_1 \aunifS S_2 \hastype A > P \ares S
    / (\Omega', \rho_1, \rho_2)$ then\\ 
$\Delta_1 ; \Omega'; \Gamma \vd S \unif S_1 \hastype A > P / (\cdot,
    \rho_1)$ and 
 $\Delta_2  ; \Omega'; \Gamma \vd S \unif S_2 \hastype A >
 P / (\cdot, \rho_2)$.
\end{enumerate}
\end{theorem}
\begin{proof}
  Simultaneous structural induction on the first derivation. 


Let
  $\Delta = \Delta_2, \Delta_1$.

\paragraph*{Case}  $\D = \ianc{(\Delta_2, \Delta_1, \Omega); \Gamma, x\oftp A_1 \vd M_1 \aunif M_2  \hastype A_2 \ares M /  (\Omega',  \rho_1, \rho_2)}{(\Delta, \Omega); \Gamma \vd \lambda x. M_1 \aunif \lam x. M_2 \hastype A_1 \arrow A_2 \ares \lambda x. M /(\Omega',\;\rho_1, \rho_2)}{}$\\[1em]
%
%
\nnl
$\Delta_1 ; \Omega' ; \Gamma, x\oftp A_1 \vd M \unifLHA M_1 \hastype A_2 / (\cdot, \rho_1)$ \hfill by i.h.\nnl
$\Delta_1 ; \Omega' ; \Gamma \vd \lambda x.M \unifLHA \lambda x.M_1 \hastype A_1 \arrow A_2 / (\cdot, \rho_1)$ \hfill by rule\nnl
%
%
$\Delta_2 ; \Omega' ; \Gamma, x\oftp A_1 \vd M \unifLHA M_2 \hastype A_2 / (\cdot, \rho_2)$ \hfill by i.h.\nnl
$\Delta_2 ; \Omega' ; \Gamma \vd \lambda x.M \unifLHA \lambda x.M_2 \hastype A_1 \arrow A_2 / (\cdot, \rho_2)$ \hfill by rule

\paragraph*{Case}  $\D = \ianc{u\ofvd (P[\Gamma]) \in \Delta}{(\Delta, \Omega); \Gamma \vd u[\pi_\Gamma] \aunifR R
  \hastype P \ares i[\id_\Gamma]/ (i{::}P[\Gamma], \Gammahat.u[\pi_\Gamma]/i, \Gammahat.R/i)}{}$\\[1em]
%
\nnl
%
$\Delta_1 ; i{::}P[\Gamma] ; \Gamma \vd i[\id_\Gamma] \unifR R \hastype P / (\cdot, \Gammahat.R/i)$  \hfill by rule {\sf{meta-1}}\nnl
%
$\Delta_1 ; i{::}P[\Gamma] ; \Gamma \vd i[\id_\Gamma] \unifR u[\pi_\Gamma] \hastype P / (\cdot, \Gammahat.u[\pi_\Gamma]/i)$  \hfill by rule {\sf{meta-1}}\nnl


\paragraph*{Case}  $\D = (\Delta, \Omega); \Gamma \vd H_1 \cdot S_1 \aunifR H_2 \cdot S_2 \hastype P \ares i[\id_\Gamma]/$\\
\mbox{\hspace{1cm}$\;$} \hfill $((i\ofvd P[\Gamma]), (H_1\cdot S_1/i), (H_2\cdot S_2 /i))$\nnl
%
%
\nnl
$H_1 \neq H_2 $ and  $i {\text{ must be    new}}$ \hfill by inversion\nnl
$\Delta_1 ; \Omega ; \Gamma \vd i[\id_\Gamma] \unifR H_1\cdot S_1
\hastype P / (\cdot , \Gammahat.H_1\cdot S_1/i)$ \hfill by {\textsf{meta-1}} \nnl
$\Delta_2 ; \Omega; \Gamma \vd i[\id_\Gamma] \unifR H_2\cdot S_2
\hastype P / (\cdot , \Gammahat.H_2\cdot S_2/i)$  \hfill by
{\textsf{meta-1}}


\paragraph*{Case}  $\D = (\Delta, \Omega); \Gamma \vd (M_1 ; S_1) \aunifS (M_2 ; S_2)
  \hastype A_1 \arrow A_2 > P  \ares$ \\
\mbox{\hspace{1cm}}\hfill$(M ; S) / ((\Omega_1,\Omega_2), (\rho_1,\rho_2), (\rho'_1, \rho'_2))$
%
%
\nnll
%
$(\Delta, \Omega); \Gamma \vd M_1 \aunif M_2 \hastype A_1 \ares M / (\Omega_1,\;\rho_1, \rho'_1)$ \hfill by inversion\nnl
%
$(\Delta, \Omega); \Gamma\; \vd \;S_1 \aunifS S_2 \hastype A_2 > P \ares S  /  (\Omega_2,\;\rho_2, \rho_2')$ \hfill \nnl
%
$(\Delta, \Omega); \Gamma \vd (M_1 ; S_1) > A_1 \arrow A_2 \syn P$
\hfill by assumption \nnl
%
$(\Delta, \Omega) ; \Gamma\; \vd M_1 \chk A_1$ \hfill \nnl
$(\Delta, \Omega) ; \Gamma\; \vd S_1 > A_2 \syn P$ \hfill by inversion\nnl
%
%
$(\Delta, \Omega); \Gamma \vd (M_2 ; S_2) > A_1 \arrow A_2 \syn P$ \hfill by assumption \nnl
%
$(\Delta, \Omega) ; \Gamma\; \vd M_2 \chk A_1$ \hfill \nnl
$(\Delta, \Omega) ; \Gamma\; \vd S_2 > A_2 \syn P$ \hfill by inversion\nnl
%
$\Delta_1 ; \Omega_1; \Gamma \vd M \unifR M_1 \hastype A_1 / (\cdot, \rho_1)$ \hfill by i.h.\nnl
%
$\Delta_2 ; \Omega_1; \Gamma \vd M \unifR M_2 \hastype A_1 / (\cdot, \rho'_1)$  \hfill by i.h.\nnl
%
%
$\Delta_1 ; \Omega_2; \Gamma\; \vd \;S \unifLHA S_1 \hastype A_2 > P  / (\cdot, \rho_2)$ \hfill by i.h.\nnl
%
$\Delta_2, \Omega_2; \Gamma\; \vd \;S \unifLHA S_2 \hastype A_2 > P  /  (\cdot, \rho_2)$ \hfill by i.h.\nnl
%
%
$\Delta_1 ;  \Omega_1,\Omega_2 ; \Gamma \vd (M ; S) \unifLHA (M_1 ; S_1) \hastype A_1 / (\cdot, (\rho_1, \rho'_1))$ \hfill by rule \nnl
$\Delta_2 , \Omega_1, \Omega_2; \Gamma \vd (M ; S) \unifLHA (M_2 ; S_2) \hastype A_1 / (\cdot , (\rho_2, \rho'_2))$ \hfill by rule
%%
\end{proof}


\end{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%




