Check-in [2656521773]

Not logged in

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

Overview
Comment:Added screenshot of the REPL UI.
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:2656521773fafe13abae2a392503083bc9de853a
User & Date: andy 2015-04-14 14:01:06
Context
2015-04-14
20:19
Changed the way the induction tactic handles repeated use (previous IHs are just ignored). check-in: c82ab7e9b6 user: andy tags: trunk
14:01
Added screenshot of the REPL UI. check-in: 2656521773 user: andy tags: trunk
14:00
Latest build results. check-in: b0c341eb78 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.

656
657
658
659
660
661
662

663
664
665
666
667
668
669
670
671
672
673
...
931
932
933
934
935
936
937
938











939



940

941













942
943
944
945
946
947
948
....
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
....
1811
1812
1813
1814
1815
1816
1817

1818
1819
1820
1821
1822
1823
1824
....
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
\]

(This exposition of natural deduction is by necessity quite simplified. For
an exposition of the modern form of natural deduction, see 
\mcitet{gentzen1964investigations}. For a more rigorous presentation of the 
logical connectives in natural deduction, see \mcitet{martin1996meanings}.)


\section{Arend System Description}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\subsection{Specifications}

Arend presents the rules of the underlying system as a collection of 
\emph{inference rules}. For example, figure \ref{example-spec} presents the
rules defining the set of natural numbers, together with natural number addition
and the less-than relation.
................................................................................
\caption{Semantics of the reasoning logic}
\label{reasoning-rules}
\end{figure}


\subsection{User Interface}

TODO : Screenshots of REPL, proof mode. Description of interfaces.































\section{Implementation}

\newthought{Arend currently exists} in two semi-overlapping implementations:
\begin{itemize}
\item A \emph{client-based} implementation, written in JavaScript and running
largely in the browser. (The core JavaScript proof-checker can also run 
offline, via a JavaScript engine such as \link{https://nodejs.org/}{node.js} or
................................................................................
\]
From a non-terminating definition we can inductively prove anything! So far from
being a flaw in our system, this surprising result reflects the fact that one
computational interpretation of $\bot$ is that of a non-terminating computation.
In fact, this result is simply the computational analogue of the well-known 
\emph{ex falso quodlibet} principle of classical logic.


\section{Future work}

\begin{itemize}
\item Arend's specification logic is simple enough that formalization of
    its properties should not be difficult, nonetheless, for formal correctness
    and consistency
    work needs to be done to show that it is both \emph{sound} (everything it
................................................................................
require careful handling of \emph{binders}, language constructs that introduce
new (program) variables into scope. These variables are distinct from the
logic variables, but can both contain, and be contained by, them. Although 
logics exist which provide support for reasoning about binding structures
\mcitep{miller05tocl} their usage in proofs involves additional complexity that
may be at odd with our goal of use in \emph{introductory} curriculum.


\section{Appendix I: Syntax  of the Specification Logic}
\label{spec-syntax}

\newcommand{\nterm}[1]{\mathop{\langle\text{#1}\rangle}}
\newcommand{\sterm}[1]{\mathop{\text{\emph{#1}}}}
\newcommand{\term}[1]{\mathop{\text{\texttt{``#1''}}}}

................................................................................
\end{align*}

\subsection{Operational Semantics}\label{spec-execute}

This may or may not get written. If it does, it will be based on the 
stack-based semantics of \mcitet{pfenning2006logic}.


\section[Appendix II: Specification for N, lists]{Appendix II: Specification for $\mathbb{N}$, lists}
\label{sec:nat-spec}

\newthought{The following is an example specification} included with Arend, 
one which 
desribes natural numbers with addition and the $>$ relation, and lists of 
natural numbers, with the operations of list concatenation, length, and 







>

<
<
<







 







|
>
>
>
>
>
>
>
>
>
>
>

>
>
>

>

>
>
>
>
>
>
>
>
>
>
>
>
>







 







|







 







>







 







|







656
657
658
659
660
661
662
663
664



665
666
667
668
669
670
671
...
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
....
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
....
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
....
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
\]

(This exposition of natural deduction is by necessity quite simplified. For
an exposition of the modern form of natural deduction, see 
\mcitet{gentzen1964investigations}. For a more rigorous presentation of the 
logical connectives in natural deduction, see \mcitet{martin1996meanings}.)

\clearpage
\section{Arend System Description}




\subsection{Specifications}

Arend presents the rules of the underlying system as a collection of 
\emph{inference rules}. For example, figure \ref{example-spec} presents the
rules defining the set of natural numbers, together with natural number addition
and the less-than relation.
................................................................................
\caption{Semantics of the reasoning logic}
\label{reasoning-rules}
\end{figure}


\subsection{User Interface}

Arend has two web-based user interfaces that support different kinds of 
interaction with the system: 
\begin{itemize}
\item The \emph{run-eval-print loop} (figure~\ref{fig:repl}) allows the user to
    run queries against a specification, view the results (substitution and
    derivation), and view the complete set of rules from the current 
    specification. In figure~\ref{fig:repl} the user has issued the query
    \texttt{natlist(cons(z,cons(z,nil))).} and is viewing the resulting 
    derivation (because this query has no free variables, no substitution is
    displayed). The rules of the specification (the $\mathbb{N}$ specification,
    given in full in \hyperref[sec:nat-spec]{appendix II}) are displayed below
    the input line.

\item The interactive \emph{proof assistant} allows the user to construct
    proofs for given propositions, in the context of a particular 
    specification.

\end{itemize}


\begin{figure*}[ht!]

\begin{centering}
\includegraphics[width=6.5in]{repl-sample.png}
\end{centering}

\caption{The browser-based run-eval-print-loop interface}
\label{fig:repl}
\end{figure*}


\clearpage
\section{Implementation}

\newthought{Arend currently exists} in two semi-overlapping implementations:
\begin{itemize}
\item A \emph{client-based} implementation, written in JavaScript and running
largely in the browser. (The core JavaScript proof-checker can also run 
offline, via a JavaScript engine such as \link{https://nodejs.org/}{node.js} or
................................................................................
\]
From a non-terminating definition we can inductively prove anything! So far from
being a flaw in our system, this surprising result reflects the fact that one
computational interpretation of $\bot$ is that of a non-terminating computation.
In fact, this result is simply the computational analogue of the well-known 
\emph{ex falso quodlibet} principle of classical logic.

\clearpage
\section{Future work}

\begin{itemize}
\item Arend's specification logic is simple enough that formalization of
    its properties should not be difficult, nonetheless, for formal correctness
    and consistency
    work needs to be done to show that it is both \emph{sound} (everything it
................................................................................
require careful handling of \emph{binders}, language constructs that introduce
new (program) variables into scope. These variables are distinct from the
logic variables, but can both contain, and be contained by, them. Although 
logics exist which provide support for reasoning about binding structures
\mcitep{miller05tocl} their usage in proofs involves additional complexity that
may be at odd with our goal of use in \emph{introductory} curriculum.

\clearpage
\section{Appendix I: Syntax  of the Specification Logic}
\label{spec-syntax}

\newcommand{\nterm}[1]{\mathop{\langle\text{#1}\rangle}}
\newcommand{\sterm}[1]{\mathop{\text{\emph{#1}}}}
\newcommand{\term}[1]{\mathop{\text{\texttt{``#1''}}}}

................................................................................
\end{align*}

\subsection{Operational Semantics}\label{spec-execute}

This may or may not get written. If it does, it will be based on the 
stack-based semantics of \mcitet{pfenning2006logic}.

\clearpage
\section[Appendix II: Specification for N, lists]{Appendix II: Specification for $\mathbb{N}$, lists}
\label{sec:nat-spec}

\newthought{The following is an example specification} included with Arend, 
one which 
desribes natural numbers with addition and the $>$ relation, and lists of 
natural numbers, with the operations of list concatenation, length, and 

Added report/repl-sample.png.

cannot compute difference between binary files