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

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