Check-in [8a438a8abd]

Not logged in

Overview
Comment: Added material to the report on the handling of explicit quantifiers. Tarball | ZIP archive | SQL archive family | ancestors | descendants | both | forall-exists files | file ages | folders 8a438a8abdfb67b6d72fac2b284dc0fc06ce5190 andy 2015-04-22 10:30:20
Context
 2015-04-22 20:49 Added poster for appreciation reception. check-in: 8078001da1 user: andy tags: trunk 10:30 Added material to the report on the handling of explicit quantifiers. Leaf check-in: 8a438a8abd user: andy tags: forall-exists 10:29 Presentation work. Added PDF of presentation. Leaf check-in: a24ff57f47 user: andy tags: trunk
Changes

Changes to report/arend-report.pdf.

cannot compute difference between binary files



Changes to report/arend-report.tex.

  1348   1348       is implicitly $\exists$-quantified.
1349   1349   \end{itemize}
1350   1350
1351   1351   Note that, if \texttt{:-} is regarded as $\leftarrow$, this is the opposite of
1352   1352   the implicit quantification in the specification. However, these rules match
1353   1353   the normal expectation for proof-style statements. For example:
1354   1354   \begin{itemize}
1355         -\item $\mathsf{nat}(X) -> \mathsf{add}(X,a,X)$ is equivalent to
1356         -    $\forall X: \mathsf{nat}(X) -> \mathsf{add}(X,a,X)$.
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   1357   \item $\mathsf{nat}(X) \land \mathsf{nat}(Y) -> \mathsf{add}(X,Y,Z) \land 1358 1358 \mathsf{nat}(Z)$ is equivalent to $\forall X,Y: \mathsf{nat}(X) \land 1359 1359 \mathsf{nat}(Y) -> \exists Z: \mathsf{add}(X,Y,Z) \land \mathsf{nat}(Z)$.
1360   1360   \end{itemize}
1361   1361
1362   1362   Internally, when processing a proof tree, Arend maintains two sets of
1363   1363   in-scope variables: \emph{universals} and \emph{existentials}. Universals are
................................................................................
1424   1424
1425   1425   (This presentation is based in part on that in \mcitet{pfenning2006logic}.)
1426   1426
1427   1427   It is interesting to directly compare the two implementations of unification
1428   1428   (one of the few modules which is semantically similar in both
1429   1429   implementations). Both systems implement the same algorithm. The Javascript
1430   1430   implementation consists of
1431         -136 lines of non-comment code and is quite difficult to follow; the Prolog
1432         -implementation requires only 69 lines,
1433         -an almost 50\% reduction! This despite the fact that the Prolog implementation
1431  +\lnum{136} lines of non-comment code and is quite difficult to follow; the Prolog
1432  +implementation requires only \lnum{69} lines,
1433  +an almost \lnum{50\%} reduction! This despite the fact that the Prolog implementation
1434   1434   does \emph{not} use the built-in unification to simplify the algorithm at all;
1435   1435   it would be largely the same if only traditional assignment were used.
1436   1436
1437   1437
1438   1438   \subsection{Proof Checking}
1439   1439
1440         -The proof checker is implemented in approximately 450 lines of Prolog code. It
1440  +The proof checker is implemented in approximately \lnum{450} lines of Prolog code. It
1441   1441   essentially implements the rules of the reasoning logic presented in figure
1442   1442   \ref{reasoning-rules}, by recursively checking the proof tree. That is, it
1443   1443   first checks the root node to ensure that the proof object is consistent with
1444   1444   the conclusion (antecedents and consequent) by ensuring that it has the correct
1445   1445   number and type of subproofs. The subproofs are then recursively checked,
1446   1446   working through the tree until the axiomatic rules are reached (or, in the
1447   1447   case of an incomplete proof, a \texttt{hole} is found, indicating an unproved
................................................................................
1879   1879   \]
1880   1880   $1881 1881 \inference[By induction] 1882 1882 {\inference[->R] 1883 1883 {\inference[Case] 1884 1884 {\inference[Add-0] 1885 1885 {} 1886 - {x = 0 |- \mathsf{add}(0,0,0)} & 1886 + {\mathsf{add}(0,0,0)} & 1887 1887 \inference[Backchain] 1888 1888 {\inference[IH] 1889 - {\assume{x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{nat}^\downarrow(x')}} 1890 - {x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{add}(x',0,x')}} 1891 - {x = s(x'), \mathsf{nat}^\downarrow(x') |- \mathsf{add}(s(x'),0,s(x'))}} 1889 + {\assume{\mathsf{nat}^\downarrow(x') |- \mathsf{nat}^\downarrow(x')}} 1890 + {\mathsf{nat}^\downarrow(x') |- \mathsf{add}(x',0,x')}} 1891 + {\mathsf{nat}^\downarrow(x') |- \mathsf{add}(s(x'),0,s(x'))}} 1892 1892 {\mathsf{nat}^\uparrow(x) |- \mathsf{add}(x,0,x)}} 1893 1893 {\mathsf{nat}^\uparrow(x) -> \mathsf{add}(x,0,x)}} 1894 1894 {\mathsf{nat}(x) -> \mathsf{add}(x,0,x)} 1895 1895$
1896   1896   (This example also demonstrates one of the flaws of the derivation proof format,
1897   1897   its insatiable appetite for horizontal space.)
1898   1898