Check-in [c98b0d6d4e]

Not logged in

Overview
Comment: Commented out tentative section of universal/existential quantification. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | trunk files | file ages | folders c98b0d6d4ee03e9397bb88734a9b4fe0bc990b7d andy 2015-04-22 20:50:02
Context
 2015-04-22 20:50 Added jsonterm module, eventually to replace term_to_json (which is terrible). check-in: 0784891462 user: andy tags: trunk 20:50 Commented out tentative section of universal/existential quantification. check-in: c98b0d6d4e user: andy tags: trunk 20:49 Added poster for appreciation reception. check-in: 8078001da1 user: andy tags: trunk
Changes

Changes to report/arend-report.pdf.

cannot compute difference between binary files

Changes to report/arend-report.tex.

 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 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,z,X)$ is equivalent to $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,z,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}. | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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 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,z,X)$ is equivalent to % $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,z,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}.