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}.