Check-in [c98b0d6d4e]

Not logged in

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
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

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