Check-in [dab782646e]

Not logged in

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

Overview
Comment:Full presentation (still draft).
Downloads: Tarball | ZIP archive | SQL archive
Timelines: family | ancestors | descendants | both | trunk
Files: files | file ages | folders
SHA1:dab782646e831d96b86c29452f4fd405808e5532
User & Date: andy 2015-04-26 21:15:02
Context
2015-04-27
12:59
Just making sure the poster was up-to-date. check-in: 6466816782 user: andy tags: trunk
2015-04-26
21:15
Full presentation (still draft). check-in: dab782646e user: andy tags: trunk
16:27
Fixed a missing section reference. check-in: e4688d49fd user: andy tags: trunk
Changes
Hide Diffs Side-by-Side Diffs Ignore Whitespace Patch

Changes to presentation/arend-presentation.pdf.

cannot compute difference between binary files

Changes to presentation/arend-presentation.tex.

    25     25   \usepackage{amssymb}
    26     26   \usepackage[inference, shorthand]{semantic} % Inference rules, shortcuts
    27     27   
    28     28   % ???
    29     29   \usepackage[english]{babel}
    30     30   
    31     31   % Make math look a little better
           32  +\usefonttheme[onlymath]{serif}
           33  +\usepackage{mathpazo}
    32     34   \usepackage{eulervm}
    33     35   
    34     36   % Use Raleway for most text
    35     37   \usepackage{fontspec}
    36     38   \defaultfontfeatures{Mapping=tex-text}
    37     39   \setsansfont{Raleway}
    38     40   
................................................................................
    66     68   
    67     69   \section{Background}
    68     70   
    69     71   
    70     72   \begin{frame}\frametitle{Formal proofs}
    71     73   
    72     74   Formal proofs --- an important component of computer science education.
    73         -
           75  +\vfill
    74     76   Prove
    75     77   \begin{itemize}
    76     78   \item $\forall x,y \in \mathbb{N}: x + y = y + x$.
    77     79   \item If $T$ is a complete binary tree with $n = |T|$ nodes, then the height of
    78     80       any node is at most $\lfloor \log_2 n \rfloor$.
    79         -\item The reverse of a regular language $L^\text{r}$ is itself regular.
           81  +\item The reverse of a regular language $L^\mathit{R}$ is itself regular.
    80     82   \end{itemize}
    81     83   
    82     84   \end{frame}
    83     85   
    84     86   
    85     87   \begin{frame}\frametitle{Paper proofs}
    86     88   
    87         -Paper proofs are common, but problematic:
           89  +Paper proofs are common, but problematic for education:
    88     90   \begin{itemize}
    89     91   \item Too flexible; allow a wide variety of ``almost correct'' answers.
    90     92   \item Delayed results; turn in a proof assignment, get results back a week
    91     93       later. \pause \alert{Batch processing for proofs.} 
    92     94   \item \pause Non-interactive.
    93     95   \end{itemize}
    94     96   
................................................................................
   102    104   \item \pause Automated theorem provers (e.g., AUTOMATH)
   103    105   \item \pause Model checkers
   104    106   \item \pause \alert{Proof assistants} (Abella, Coq, Arend, etc.)
   105    107   \end{itemize}
   106    108   
   107    109   \end{frame}
   108    110   
          111  +\subsection{Proof assistants}
   109    112   
   110    113   \begin{frame}\frametitle{Proof assistants}
   111    114   
   112    115   A proof assistant
   113    116   \begin{itemize}
   114    117   \item \pause \alert{Assists} the user in constructing a \alert{valid} proof.
   115    118   \item \pause \alert{Forbids} the construction of \alert{invalid} proofs.
................................................................................
   169    172   \end{itemize}
   170    173   
   171    174   (End of aside.)
   172    175   
   173    176   \end{frame}
   174    177   
   175    178   
          179  +\section{Proof assistants in education}
          180  +
          181  +\begin{frame}\frametitle{Proof assistants in education}
          182  +
          183  +We are interested in the application of proof assistants to CSCI education. 
          184  +\vfill
          185  +Why?
          186  +\begin{itemize}
          187  +\item Fixed notion of what a valid proof is (and isn't). 
          188  +\item Instant results: yes, this proof is correct; no, it isn't.
          189  +\item Interactive.
          190  +\end{itemize}
          191  +
          192  +\end{frame}
          193  +
          194  +\begin{frame}\frametitle{Problems with existing systems}
          195  +
          196  +But when it comes to undergrad education, there are some problems with 
          197  +existing systems:
          198  +\begin{itemize}
          199  +\item Complexity: powerful logics create complexity in even simple proofs.
          200  +\item Not user-friendly: Emacs + ProofGeneral are hardly intuitive.
          201  +\item Unfamiliar: Syntax often is often wildly different from any kind of 
          202  +  paper proof
          203  +\end{itemize}
          204  +
          205  +\end{frame}
          206  +
          207  +\begin{frame}\frametitle{What we don't want}
          208  +
          209  +\begin{center}
          210  +\includegraphics[width=3.5in]{ebella.png}
          211  +\end{center}
          212  +
          213  +\end{frame}
          214  +
          215  +\begin{frame}\frametitle{What we do want}
          216  +
          217  +\begin{center}
          218  +\includegraphics[width=3.5in]{proof-complete.png}
          219  +\end{center}
          220  +
          221  +\end{frame}
   176    222   
   177    223   
   178         -\begin{frame}
          224  +\begin{frame}\frametitle{Demo}
   179    225   \vfill
   180    226   \centering
   181    227   A quick demo of a proof in Arend
   182    228   \vfill
          229  +\end{frame}
          230  +
          231  +\section{Arend -- System description}
          232  +
          233  +\begin{frame}\frametitle{What is Arend?}
          234  +
          235  +Arend is a web-based proof assistant designed for use in undergraduate 
          236  +CSci education.
          237  +\vfill
          238  +\begin{itemize}
          239  +\item Based on a simple, familiar first order logic ($\forall$, $\exists$,
          240  +  $\land$, $\lor$, and $\to$).
          241  +\item \alert{Specifications} (systems to be reasoned about) are constructed
          242  +  by instructors, as are proof statements ($\forall X: \exists Y: \ldots$)
          243  +\item Students construct proofs by direct interaction: ``point-and-click''.
          244  +\item Invalid proofs cannot be constructed, and incomplete proofs are marked
          245  +  as such
          246  +\end{itemize}
          247  +
          248  +\end{frame}
          249  +
          250  +\subsection{Specification}
          251  +
          252  +\begin{frame}[fragile]\frametitle{Specification logic}
          253  +
          254  +Arend's specification logic is used to describe the systems to be reasoned
          255  +about. E.g., a specification for $\mathbb{N}, +$:
          256  +
          257  +\begin{verbatim}
          258  +"Nat-z":   nat(z).
          259  +"Nat-s":   nat(succ(N)) :- nat(N).
          260  +
          261  +"Add-z":   add(z,N,N).
          262  +"Add-s":   add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
          263  +\end{verbatim}
          264  +
          265  +\end{frame}
          266  +
          267  +\begin{frame}\frametitle{Specification logic, cont.}
          268  +
          269  +\begin{itemize}
          270  +\item A specification consists of a series of \alert{definitions}.
          271  +\item A definition consists of one or more \alert{clauses}.
          272  +\item Each clause has a name, a \alert{head}, and an (optional) \alert{body}.
          273  +\item The body of each clause must be a pure conjuction of atomic goals
          274  +  (calls to definitions)
          275  +\end{itemize}
          276  +
          277  +\end{frame}
          278  +
          279  +\begin{frame}\frametitle{Almost Prolog...}
          280  +
          281  +It looks like Prolog, but not quite:
          282  +\vfill
          283  +\begin{itemize}
          284  +\item No disjunction, except that implicit in multiple clauses.
          285  +\item No negation (``as failure'', or otherwise).
          286  +\item No proof search control structures: \texttt{!}, \texttt{->}, etc.
          287  +\end{itemize}
          288  +\vfill
          289  +Proof search (by resolution) is largely the same. (I.e., ordering of clauses
          290  +is significant for execution, but \emph{not} for proofs.)
          291  +
          292  +\end{frame}
          293  +
          294  +\begin{frame}[fragile]\frametitle{Specifications as rules}
          295  +
          296  +Clauses in the specification logic correspond almost exactly to inference
          297  +rules:
          298  +\begin{verbatim}
          299  +"Add-z":   add(z,N,N).
          300  +"Add-s":   add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
          301  +\end{verbatim}
          302  +becomes
          303  +\[
          304  +\inference[Add-z]
          305  +  {}
          306  +  {\mathsf{add}(z,N,N)}
          307  +\quad
          308  +\inference[Add-s]
          309  +  {\mathsf{add}(X,Y,Z)}
          310  +  {\mathsf{add}(\mathit{succ}(X),Y,\mathit{succ}(Z))}
          311  +\]
          312  +
          313  +\end{frame}
          314  +
          315  +\subsection{Reasoning logic}
          316  +
          317  +\begin{frame}\frametitle{Reasoning logic}
          318  +
          319  +Proofs are \alert{about} things in the specification logic, but proofs 
          320  +themselves are in the \alert{reasoning logic}.
          321  +
          322  +The reasoning logic has everything the specification logic has, plus
          323  +\begin{itemize}
          324  +\item Implication: $P \to Q$. (Note that $P$ cannot contain further 
          325  +  implications!)
          326  +\item Explicit quantification: $\forall X: \ldots$ and $\exists Y: \ldots$
          327  +\item Free use of $\land$ and $\lor$
          328  +\end{itemize}
          329  +
          330  +\end{frame}
          331  +
          332  +\begin{frame}[fragile]\frametitle{Embedding}
          333  +
          334  +Thus, the specification logic can be \alert{embedded} in the reasoning logic:
          335  +\begin{verbatim}
          336  +"Add-s":   add(succ(X),Y,succ(Z)) :- add(X,Y,Z).
          337  +\end{verbatim}
          338  +becomes
          339  +\[
          340  +\forall X,Y,Z: \mathsf{add}(X,Y,Z) \to 
          341  +  \mathsf{add}(\mathit{succ}(X),Y,\mathit{succ}(Z))
          342  +\]
          343  +
          344  +\end{frame}
          345  +
          346  +\begin{frame}\frametitle{Reasoning about specifications}
          347  +
          348  +This allows us to use the specification logic to reason \alert{about}
          349  +specifications. E.g.
          350  +\vfill
          351  +
          352  +\begin{beamerboxesrounded}[upper=block body,lower=block body,shadow=true]{Prove:}
          353  +\[
          354  +\forall X,Y: \mathsf{nat}(X) \land \mathsf{nat}(Y) \to 
          355  +  \exists Z: \mathsf{add}(X,Y,Z)
          356  +\]
          357  +\end{beamerboxesrounded}
          358  +\vfill
          359  +This proof will be \alert{about} nat and add.
          360  +
          361  +\end{frame}
          362  +
          363  +%%% --------------------------------------------------------------------------
          364  +
          365  +
          366  +\section{Implementation}
          367  +
          368  +\begin{frame}\frametitle{Implementation statistics}
          369  +
          370  +Arend's implementation consists of:
          371  +\begin{itemize}
          372  +\item 1,401 lines of Prolog
          373  +\item 6,198 lines of Javascript (of which 442 lines are test
          374  +    code)
          375  +\item 493 lines of PEG grammar specification
          376  +\item 501 lines of HTML
          377  +\item 129 lines of CSS
          378  +\item 41 source code files in total
          379  +\end{itemize}
          380  +
          381  +\end{frame}
          382  +
          383  +\begin{frame}\frametitle{Development details}
          384  +
          385  +Arend's development:
          386  +\begin{itemize}
          387  +\item Tracked using the Fossil version control system 
          388  +  (\alert{\small http://fossil-scm.org})
          389  +\item 294 commits
          390  +\item Spans eight months of development
          391  +\end{itemize}
          392  +
          393  +\end{frame}
          394  +
          395  +\begin{frame}\frametitle{Development tools}
          396  +
          397  +Some libraries and tools used:
          398  +\begin{itemize}
          399  +\item Node.JS -- Offline Javascript runtime
          400  +\item SWI-Prolog -- Prolog environment
          401  +\item Lodash -- Javascript utility library
          402  +\item jQuery -- Javascript+HTML utility library
          403  +\item qUnit -- Javascript test framework
          404  +\item Pengines -- Prolog HTTP server framework
          405  +\end{itemize}
          406  +
          407  +\end{frame}
          408  +
          409  +\begin{frame}\frametitle{Web client overview}
          410  +
          411  +Arend's user interface is a fairly straightforward web client, with a few
          412  +twists:
          413  +\begin{itemize}
          414  +\item Full \texttt{Term} datatype (incl. atoms, logic variables, and compounds).
          415  +  This allows terms to be communicated to/from the backend without any 
          416  +  special-purpose translation.
          417  +\item Unification of terms is also present in the client codebase, currently
          418  +  unused. Eventually will form part of a term pattern-matching library.
          419  +\item Pengines allows (nearly) transparent JS/Prolog interop., almost as if
          420  +  Prolog was running in the browser.
          421  +\end{itemize}
          422  +
          423  +\end{frame}
          424  +
          425  +\subsection{Backend implementation}
          426  +
          427  +\begin{frame}\frametitle{Major backend modules}
          428  +
          429  +Arend's backend (exposed via HTTP) consists of three main modules:
          430  +\begin{itemize}
          431  +\item \texttt{subst} -- Unification and substitution
          432  +\item \texttt{program} -- Goal expansion and execution for specifications
          433  +\item \texttt{checker} -- Elaboration and checking of proofs (reasoning logic)
          434  +\end{itemize}
          435  +\end{frame}
          436  +
          437  +\begin{frame}[shrink=20]\frametitle{Substitution and unification}
          438  +
          439  +{\Large Because proofs may have different substitutions in different parts of the
          440  +tree, we cannot use Prolog's (global) unification and substitution. We 
          441  +reimplement logic variables, unification, and substitution.}
          442  +\vfill
          443  +
          444  +\[
          445  +\inference[Case on $\mathsf{nat}$]
          446  +  {\inference[$X \mapsto z$]
          447  +    {\vdots}
          448  +    {\vdash \mathsf{add}(z,z,z)} &
          449  +   \inference[$X \mapsto s(N)$]
          450  +    {\vdots}
          451  +    {\mathsf{nat}(N) \vdash \mathsf{add}(s(N),z,s(N))}}
          452  +  {\mathsf{nat}(X) \vdash \mathsf{add}(X,z,X)}
          453  +\]
          454  +
          455  +
          456  +\end{frame}
          457  +
          458  +\begin{frame}\frametitle{\texttt{subst} module}
          459  +
          460  +The \texttt{subst} module implements:
          461  +\begin{itemize}
          462  +\item Custom variable type (encoded as special atoms)
          463  +\item Robinson unification algorithm over term containing these variables
          464  +\item Application of substitutions to terms
          465  +\end{itemize}
          466  +
          467  +\end{frame}
          468  +
          469  +\begin{frame}\frametitle{\texttt{program} module}
          470  +
          471  +Module \texttt{program} is responsible for handling specifications: 
          472  +\begin{itemize}
          473  +\item Expanding calls to atomic goals (e.g., \texttt{add(z,s(z),X)}) requires
          474  +  renaming variables in the body, so they don't conflict
          475  +  with variables in scope.
          476  +\item Execution of specification queries follows the resolution proof
          477  +  search procedure. Note that Arend lacks ``negation as failure''. 
          478  +\item Execution produces proof objects compatible with those used by the
          479  +  full proof checker.
          480  +\item Execution of queries is exposed via the \texttt{repl} Pengine application.
          481  +\end{itemize}
          482  +
          483  +\end{frame}
          484  +
          485  +\begin{frame}\frametitle{\texttt{checker} module}
          486  +
          487  +The most complex module in the backend, \texttt{checker} handles elaboration
          488  +and checking of proofs in the full reasoning logic.
          489  +
          490  +\begin{itemize}
          491  +\item Proof \alert{completeness} -- Does a proof contain any holes?
          492  +  (Simple recursive predicate)
          493  +\item Proof \alert{elaboration} -- Expanding a hole into a 1-level subproof
          494  +\item Proof \alert{checking} -- Is a proof correct, according to a 
          495  +  specification and the rules of the reasoning logic?
          496  +\end{itemize}
          497  +
          498  +\end{frame}
          499  +
          500  +\begin{frame}\frametitle{Proof elaboration}
          501  +
          502  +Proof elaboration, in tandem with proof checking, is at the heart of 
          503  +incremental proof construction. Consider the proof state:
          504  +\[
          505  +\inference[]
          506  +  {?}
          507  +  {\vdash P \land Q}
          508  +\]
          509  +\vfill
          510  +If we elaborate $P \land Q$, what should replace ?.
          511  +
          512  +\end{frame}
          513  +
          514  +\begin{frame}\frametitle{Proof elaboration, cont.}
          515  +
          516  +\[
          517  +\inference[]
          518  +  {\inference[]{?}{\vdash P} &
          519  +   \inference[]{?}{\vdash Q}}
          520  +  {\vdash P \land Q}
          521  +\]
          522  +\vfill
          523  +Elaboration expands a ?, in combination with either the consequent or an
          524  +antecedant, so that the result is a valid proof tree, one level deeper.
          525  +
          526  +\end{frame}
          527  +
          528  +\begin{frame}\frametitle{Proof checking}
          529  +
          530  +Checking a proof object proceeds by checking it against the \alert{rules}
          531  +of the specification logic.
          532  +\vfill
          533  +\[
          534  +\inference[$\wedge_R$]
          535  +    {\Gamma |- P & \Gamma |- Q}
          536  +    {\Gamma |- P \wedge Q}
          537  +\quad
          538  +\inference[$\wedge_L$]
          539  +    {\Gamma, P, Q |- G}
          540  +    {\Gamma, P \wedge Q |- G}
          541  +\]
          542  +(E.g.: Rules for $\land$)
          543  +
          544  +\end{frame}
          545  +
          546  +\begin{frame}\frametitle{Proof checking, cont.}
          547  +
          548  +Each node of the proof tree includes:
          549  +\begin{itemize}
          550  +\item Node type (e.g., \texttt{product}, \texttt{induction}, etc.)
          551  +\item Subproof(s) (child nodes)
          552  +\item Consequent (proposition to the right of $\vdash$)
          553  +\item Antecedents (propositions to the left of $\vdash$)
          554  +\item Current substitution
          555  +\item Variables in scope
          556  +\end{itemize}
          557  +
          558  +\end{frame}
          559  +
          560  +\begin{frame}\frametitle{Proof checking, cont.}
          561  +
          562  +Substitutions and variable bindings flow through the tree nontrially:
          563  +\vfill
          564  +\begin{itemize}
          565  +\item Substitutions flow from leaves to root, but also left-to-right in 
          566  +  conjunctions.
          567  +\item Variable scopings flow from root to leaves, but also left-to-right in
          568  +  conjunctions.
          569  +\end{itemize}
          570  +\vfill
          571  +Formalization of the complete proof checking procedure, including substitutions
          572  +and variable scopings, is ongoing.
          573  +
          574  +\end{frame}
          575  +
          576  +\begin{frame}\frametitle{Proof construction procedure}
          577  +
          578  +\begin{enumerate}
          579  +\item User selects an element (antecedent or consequent) in the current proof
          580  +  state. Path to the element along with the proof tree is passed to the server.
          581  +\item Path to the element along with the proof tree is passed to the server.
          582  +\item Server calls \texttt{checker:elaborate} to elaborate the desired element.
          583  +\item Elaborated proof is returned to client.
          584  +\item New proof is checked for completeness. Complete? then \textsc{Stop}, else
          585  +  \textsc{GoTo} 1.
          586  +\end{enumerate}
          587  +
          588  +\end{frame}
          589  +
          590  +\section{Future work}
          591  +
          592  +\begin{frame}\frametitle{The future of Arend}
          593  +
          594  +Arend is far from complete; enhancements can be divided into three areas:
          595  +
          596  +\begin{itemize}
          597  +\item Necessary features 
          598  +\item Enhancements
          599  +\item Formalization
          600  +\end{itemize}
          601  +
          602  +\end{frame}
          603  +
          604  +\begin{frame}\frametitle{Necessary features}
          605  +
          606  +Arend is missing many features that would be necessary in a large-scale
          607  +deployment:
          608  +\begin{itemize}
          609  +\item Centralized storage of specifications, assignments
          610  +\item Interop with grading backend, for storage of (in)complete assignments
          611  +\item Richer user interface: lemma construction, instantiation of $\exists$
          612  +  variables, etc. are all unspecified
          613  +\item Easy-to-deploy packaging of the entire system
          614  +\end{itemize}
          615  +
          616  +\end{frame}
          617  +
          618  +\begin{frame}\frametitle{Enhancements}
          619  +
          620  +Although not strictly necessary, there are still many enhancements that would 
          621  +make Arend a better system, either more powerful, easier to use, or both.
          622  +\begin{itemize}
          623  +\item Enhanced proofs: tactics, instructor-controlled proof automation.
          624  +\item Support for student-authored specifications
          625  +\item Alternate proof interfaces: traditional paragraph, mixed, etc.
          626  +\item Functional language for reasoning about programs, equational reasoning
          627  +\end{itemize}
          628  +
          629  +\end{frame}
          630  +
          631  +\begin{frame}\frametitle{Formalization}
          632  +
          633  +Although we believe Arend's systems to be fully adequate, being based on
          634  +existing well-studied systems, a full formalization of our systems and their
          635  +integration would be a useful addition.
          636  +\begin{itemize}
          637  +\item Full operational semantics of the specification logic
          638  +\item Proof of soundness and non-deterministic completeness of the 
          639  +  specification logic (all things proven are true, and nothing false can be
          640  +  proven)
          641  +\item Full semantics for reasoning logic, incl. substitutions and bindings
          642  +\item Proof of \alert{adequecy} of the reasoning logic with regard to the
          643  +  specification logic.
          644  +\end{itemize}
          645  +
          646  +\end{frame}
          647  +
          648  +\begin{frame}\frametitle{Conclusions}
          649  +
          650  +We believe that Arend's design will make it a valuable addition to the
          651  +undergraduate computer science curriculum. We are currently working to get
          652  +Arend into a suitable state for use in our own courses, and hope to have 
          653  +feedback from real student usage in the future.
          654  +
   183    655   \end{frame}
   184    656   
   185    657   
   186    658   %%% --------------------------------------------------------------------------
   187    659   %%% Bibliography slide
   188    660   %%% --------------------------------------------------------------------------
   189    661   
................................................................................
   191    663   \section<presentation>*{\appendixname}
   192    664   \subsection<presentation>*{For Further Reading}
   193    665   
   194    666   \begin{frame}{For Further Reading}
   195    667       
   196    668     \begin{thebibliography}{10}
   197    669       
   198         -  \beamertemplatebookbibitems
   199         -  % Start with overview books.
          670  +  \beamertemplatearticlebibitems
   200    671   
   201         -  \bibitem{Hillis:1989:CM:64121}
   202         -    W.~Daniel~Hillis
   203         -    \newblock {\em The Connection Machine}.
   204         -    \newblock MIT Press, 1989.
   205         - 
          672  +  \bibitem{clifton2015arend}
          673  +    A.~V.~Clifton
          674  +    \newblock Arend --- Proof-assistant Assisted Pedagogy
          675  +    \newblock CSU Fresno, 2015.
   206    676       
   207    677     \beamertemplatearticlebibitems
   208         -  % Followed by interesting articles. Keep the list short. 
   209    678   
   210         -  \bibitem{Hillis:1986:DPA:7902.7903}
   211         -    W.~D.~Hillis and G.~L.~Steele
   212         -    \newblock Data Parallel Algorithms
   213         -    \newblock {\em Communications of the ACM}, 29(12):1170--1183,
   214         -    1986.
          679  +  \bibitem{geuvers2009proof}
          680  +    H.~Geuvers
          681  +    \newblock Proof assistants: History, ideas and future
          682  +    \newblock {\em Sadhana}, 31(1):3--25,
          683  +    Springer, 2009.
   215    684     \end{thebibliography}
   216    685   \end{frame}
   217    686   
   218    687   
   219    688   \end{document}