Index: report/arend-report.tex
==================================================================
--- report/arend-report.tex
+++ report/arend-report.tex
@@ -895,12 +895,12 @@
\]
% Unification rules
\[
\inference[$=_R$]
- {[t_1 = t_2]}
- {\Gamma |- t_1 = t_2}
+ {}
+ {\Gamma |- t = t}
\qquad\qquad
\inference[$=_L$]
{\Gamma_{[t_1 = t_2]} |- G_{[t_1 = t_2]}}
{\Gamma, t_1 = t_2 |- G}
\]
@@ -1326,10 +1326,51 @@
correct to give $\forall 1, P(1)$. In addition, consider the problem of
applying the substitution
$X \mapsto Y$ to $\forall Y, P(X,Y)$; clearly, one of the $Y$'s will need to
be renamed. Since the $Y$ in the substitution is most likely bound somewhere
else in the derivation, we choose to rename the $Y$ bound within the $\forall$.
+
+\subsection{Universal and Existential Quantification}
+
+In the specification language, variables are implicitly quantified: variables
+occurring in the head of a clause are universally quantified, while
+variables that occur \emph{only} in the body of a clause are existentially
+quantified.\marginnote{This is the same as the implicit quantifications rules
+for Prolog.} However, the reasoning language supports both implicit and
+explicit quantification. We wish to preserve compatibility between the two
+languages, so that queries which are provable in the specification language,
+are also provable in the reasoning language. For this reason, we adopt the
+following scheme with regard to implicitly quantified variables in
+reasoning queries:
+\begin{itemize}
+\item An unquantified variable occurring \emph{to the left} of an implication
+ is implicitly $\forall$-quantified.
+\item An unqualified variable occurring to the \emph{right} of an implication
+ is implicitly $\exists$-quantified.
+\end{itemize}
+
+Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of
+the implicit quantification in the specification. However, these rules match
+the normal expectation for proof-style statements. For example:
+\begin{itemize}
+\item $\mathsf{nat}(X) -> \mathsf{add}(X,a,X)$ is equivalent to
+ $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,a,X)$.
+\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land
+ \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land
+ \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.
+\end{itemize}
+
+Internally, when processing a proof tree, Arend maintains two sets of
+in-scope variables: \emph{universals} and \emph{existentials}. Universals are
+those introduced by the $\forall$-R and $\exists$-L rules; they implicitly
+represent fresh \emph{constants} and cannot be bound by unification.
+Existentials are introduced by $\exists$-R and $\forall$-L rules; they are
+true variables which have simply not been instantiated yet. In fact, the
+behavior of unification is to supply the instantiation of one or more
+existential variables, possibly in terms of the in-scope universal variables.
+
+
\subsection{Unification}
The Robinson unification algorithm is presented, in natural deduction style,
in figure~\ref{unification-rules}.