Check-in [8a438a8abd]

Not logged in

Many hyperlinks are disabled.
Use anonymous login to enable hyperlinks.

Overview
Comment:Added material to the report on the handling of explicit quantifiers.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | forall-exists
Files: files | file ages | folders
SHA1:8a438a8abdfb67b6d72fac2b284dc0fc06ce5190
User & Date: 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
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.

  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