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 Unified Diffs Show Whitespace Changes Patch

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