Check-in [e8532f2591]

Not logged in

 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 .... 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 {\Gamma, P(y) |- G} {\Gamma, \exists x: P(x) |- G} \] % Unification rules $\inference[=_R] {[t_1 = t_2]} {\Gamma |- t_1 = t_2} \qquad\qquad \inference[=_L] {\Gamma_{[t_1 = t_2]} |- G_{[t_1 = t_2]}} {\Gamma, t_1 = t_2 |- G}$ % Atomic goals ................................................................................ capturing the names $S$ and $T$, respectively, within their bodies. Thus, to apply a substitution $X \mapsto 1$ to $\forall X, P(X)$ it is \emph{not} 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{Unification} The Robinson unification algorithm is presented, in natural deduction style, in figure~\ref{unification-rules}. Note that the same algorithm is used, with minor modification, in both the Javascript and Prolog implementations (for a direct | | > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > > 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 .... 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 {\Gamma, P(y) |- G} {\Gamma, \exists x: P(x) |- G} \] % Unification rules $\inference[=_R] {} {\Gamma |- t = t} \qquad\qquad \inference[=_L] {\Gamma_{[t_1 = t_2]} |- G_{[t_1 = t_2]}} {\Gamma, t_1 = t_2 |- G}$ % Atomic goals ................................................................................ capturing the names $S$ and $T$, respectively, within their bodies. Thus, to apply a substitution $X \mapsto 1$ to $\forall X, P(X)$ it is \emph{not} 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}. Note that the same algorithm is used, with minor modification, in both the Javascript and Prolog implementations (for a direct