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