Many hyperlinks are disabled.

Use anonymous login
to enable hyperlinks.

Overview

Comment: | Commented out tentative section of universal/existential quantification. |
---|---|

Downloads: | Tarball | ZIP archive | SQL archive |

Timelines: | family | ancestors | descendants | both | trunk |

Files: | files | file ages | folders |

SHA1: | c98b0d6d4ee03e9397bb88734a9b4fe0bc990b7d |

User & Date: | 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 1325 apply a substitution $X \mapsto 1$ to $\forall X, P(X)$ it is \emph{not} 1326 1326 correct to give $\forall 1, P(1)$. In addition, consider the problem of 1327 1327 applying the substitution 1328 1328 $X \mapsto Y$ to $\forall Y, P(X,Y)$; clearly, one of the $Y$'s will need to 1329 1329 be renamed. Since the $Y$ in the substitution is most likely bound somewhere 1330 1330 else in the derivation, we choose to rename the $Y$ bound within the $\forall$. 1331 1331 1332 -\subsection{Universal and Existential Quantification} 1333 - 1334 -In the specification language, variables are implicitly quantified: variables 1335 -occurring in the head of a clause are universally quantified, while 1336 -variables that occur \emph{only} in the body of a clause are existentially 1337 -quantified.\marginnote{This is the same as the implicit quantifications rules 1338 -for Prolog.} However, the reasoning language supports both implicit and 1339 -explicit quantification. We wish to preserve compatibility between the two 1340 -languages, so that queries which are provable in the specification language, 1341 -are also provable in the reasoning language. For this reason, we adopt the 1342 -following scheme with regard to implicitly quantified variables in 1343 -reasoning queries: 1344 -\begin{itemize} 1345 -\item An unquantified variable occurring \emph{to the left} of an implication 1346 - is implicitly $\forall$-quantified. 1347 -\item An unqualified variable occurring to the \emph{right} of an implication 1348 - is implicitly $\exists$-quantified. 1349 -\end{itemize} 1350 - 1351 -Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of 1352 -the implicit quantification in the specification. However, these rules match 1353 -the normal expectation for proof-style statements. For example: 1354 -\begin{itemize} 1355 -\item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$ is equivalent to 1356 - $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. 1357 -\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land 1358 - \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 1359 - \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$. 1360 -\end{itemize} 1361 - 1362 -Internally, when processing a proof tree, Arend maintains two sets of 1363 -in-scope variables: \emph{universals} and \emph{existentials}. Universals are 1364 -those introduced by the $\forall$-R and $\exists$-L rules; they implicitly 1365 -represent fresh \emph{constants} and cannot be bound by unification. 1366 -Existentials are introduced by $\exists$-R and $\forall$-L rules; they are 1367 -true variables which have simply not been instantiated yet. In fact, the 1368 -behavior of unification is to supply the instantiation of one or more 1369 -existential variables, possibly in terms of the in-scope universal variables. 1332 +%\subsection{Universal and Existential Quantification} 1333 +% 1334 +%In the specification language, variables are implicitly quantified: variables 1335 +%occurring in the head of a clause are universally quantified, while 1336 +%variables that occur \emph{only} in the body of a clause are existentially 1337 +%quantified.\marginnote{This is the same as the implicit quantifications rules 1338 +%for Prolog.} However, the reasoning language supports both implicit and 1339 +%explicit quantification. We wish to preserve compatibility between the two 1340 +%languages, so that queries which are provable in the specification language, 1341 +%are also provable in the reasoning language. For this reason, we adopt the 1342 +%following scheme with regard to implicitly quantified variables in 1343 +%reasoning queries: 1344 +%\begin{itemize} 1345 +%\item An unquantified variable occurring \emph{to the left} of an implication 1346 +% is implicitly $\forall$-quantified. 1347 +%\item An unqualified variable occurring to the \emph{right} of an implication 1348 +% is implicitly $\exists$-quantified. 1349 +%\end{itemize} 1350 +% 1351 +%Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of 1352 +%the implicit quantification in the specification. However, these rules match 1353 +%the normal expectation for proof-style statements. For example: 1354 +%\begin{itemize} 1355 +%\item $\mathsf{nat}(X) -> \mathsf{add}(X,z,X)$ is equivalent to 1356 +% $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,z,X)$. 1357 +%\item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land 1358 +% \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 1359 +% \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$. 1360 +%\end{itemize} 1361 +% 1362 +%Internally, when processing a proof tree, Arend maintains two sets of 1363 +%in-scope variables: \emph{universals} and \emph{existentials}. Universals are 1364 +%those introduced by the $\forall$-R and $\exists$-L rules; they implicitly 1365 +%represent fresh \emph{constants} and cannot be bound by unification. 1366 +%Existentials are introduced by $\exists$-R and $\forall$-L rules; they are 1367 +%true variables which have simply not been instantiated yet. In fact, the 1368 +%behavior of unification is to supply the instantiation of one or more 1369 +%existential variables, possibly in terms of the in-scope universal variables. 1370 1370 1371 1371 1372 1372 1373 1373 \subsection{Unification} 1374 1374 1375 1375 The Robinson unification algorithm is presented, in natural deduction style, 1376 1376 in figure~\ref{unification-rules}.