diff -r 7f3760f39bdc -r f8845fc8f38d doc-isac/mlehnfeld/presentation.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-isac/mlehnfeld/presentation.tex	Tue Sep 17 09:50:52 2013 +0200
@@ -0,0 +1,469 @@
+% $Header: /cvsroot/latex-beamer/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex,v 1.7 2007/01/28 20:48:23 tantau Exp $
+
+\documentclass{beamer}
+
+% This file is a solution template for:
+
+% - Talk at a conference/colloquium.
+% - Talk length is about 20min.
+% - Style is ornate.
+
+
+
+% Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
+%
+% In principle, this file can be redistributed and/or modified under
+% the terms of the GNU Public License, version 2.
+%
+% However, this file is supposed to be a template to be modified
+% for your own needs. For this reason, if you use this file as a
+% template and not specifically distribute it as part of a another
+% package/program, I grant the extra permission to freely copy and
+% modify this file as you see fit and even to delete this copyright
+% notice.
+
+
+\mode<presentation>
+{
+  \usetheme{Hannover}
+  % or ...
+
+  \setbeamercovered{transparent}
+  % or whatever (possibly just delete it)
+}
+
+%\usepackage{setspace} %for "\begin{onehalfspace}"
+\usepackage[english]{babel}
+% or whatever
+
+\usepackage[utf8]{inputenc}
+% or whatever
+
+\usepackage{times}
+\usepackage[T1]{fontenc}
+% Or whatever. Note that the encoding and the font should match. If T1
+% does not look nice, try deleting the line with the fontenc.
+
+\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
+\def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
+
+\title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
+{Integrating Computation and Deduction\\
+  in the \isac-System}
+
+\subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
+
+\author[Lehnfeld] % (optional, use only with lots of authors)
+{Mathias~Lehnfeld}
+% - Give the names in the same order as the appear in the paper.
+% - Use the \inst{?} command only if the authors have different
+%   affiliation.
+
+\institute % (optional, but mostly needed)
+{
+  Vienna University of Technology\\
+  Institute of Computer Languages
+}
+% - Use the \inst command only if there are several affiliations.
+% - Keep it simple, no one is interested in your street address.
+
+% \date[CFP 2003] % (optional, should be abbreviation of conference name)
+% {Conference on Fabulous Presentations, 2003}
+% - Either use conference name or its abbreviation.
+% - Not really informative to the audience, more for people (including
+%   yourself) who are reading the slides online
+
+% \subject{Theoretical Computer Science}
+% This is only inserted into the PDF information catalog. Can be left
+% out.
+
+
+
+% If you have a file called "university-logo-filename.xxx", where xxx
+% is a graphic format that can be processed by latex or pdflatex,
+% resp., then you can add a logo as follows:
+
+% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
+% \logo{\pgfuseimage{university-logo}}
+
+
+
+% Delete this, if you do not want the table of contents to pop up at
+% the beginning of each subsection:
+\AtBeginSubsection[]
+{
+  \begin{frame}<beamer>{Outline}
+    \tableofcontents[currentsection,currentsubsection]
+  \end{frame}
+}
+
+
+% If you wish to uncover everything in a step-wise fashion, uncomment
+% the following command:
+
+%\beamerdefaultoverlayspecification{<+->}
+
+
+\begin{document}
+
+\begin{frame}
+  \titlepage
+\end{frame}
+
+\begin{frame}{Outline}
+  \tableofcontents
+  % You might wish to add the option [pausesections]
+\end{frame}
+
+
+% Structuring a talk is a difficult task and the following structure
+% may not be suitable. Here are some rules that apply for this
+% solution:
+
+% - Exactly two or three sections (other than the summary).
+% - At *most* three subsections per section.
+% - Talk about 30s to 2min per frame. So there should be between about
+%   15 and 30 frames, all told.
+
+% - A conference audience is likely to know very little of what you
+%   are going to talk about. So *simplify*!
+% - In a 20min talk, getting the main ideas across is hard
+%   enough. Leave out details, even if it means being less precise than
+%   you think necessary.
+% - If you omit details that are vital to the proof/implementation,
+%   just say so once. Everybody will be happy with that.
+
+\section[Introduction]{Introduction: Isabelle and \isac}
+%\subsection[Isabelle \& \isac]{Isabelle and \isac}
+\begin{frame}
+  \frametitle{Isabelle and \isac}
+The task of this ``Projektpraktikum'' (6 ECTS) was to
+\begin{itemize}
+\item study the concept of ``context'' in the theorem prover \textbf{Isabelle} from TU Munich
+\item study basic concepts of the math assistant \sisac{} from TU Graz
+\pause
+\item redesign \sisac{} with respect to contexts
+  \begin{itemize}
+  \item use contexts for type inference of user input
+  \item handle preconditions of specifications
+  \item clarify the transfer of context data from sub-programs to the calling program
+  \end{itemize}
+\pause
+\item introduce contexts to \sisac{} according to the new design
+\item use the coding standards of Isabelle2011 for new code.
+\end{itemize}
+\end{frame}
+
+%\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
+\begin{frame}
+  \frametitle{Computation and Deduction in a Lucas-Interpreter}
+    \includegraphics[width=100mm]{overview.pdf}
+\end{frame}
+
+\section[Contributions]{Contributions of the project to \isac}
+\subsection[Contexts]{Isabelle's Contexts, advantages and use}
+\begin{frame}
+  \frametitle{Advantages of Isabelle's Contexts}
+Isabelle's context replaced theories because \dots:
+\begin{itemize}
+\item theories are static containers of \textit{all} logical data
+\item contexts are \textit{dynamic} containers of logical data:
+  \begin{itemize}
+  \item functions for storing and retrieving various logical data
+  \item functions for type inference
+  \item provide data for Isabelle's automated provers
+  \end{itemize}
+%\item e.g. theories have no direct functions for type inference
+%\item replace function \texttt{parseNEW}
+%\item assumptions \& environment $\rightarrow$ context
+\item allow to conform with scopes for subprograms.
+\end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Isabelle's context mechanism}
+    \texttt{\small{
+      \begin{tabbing}
+xx\=xx\=in\=\kill
+%xx\=xx\=xx\=xx\=\kill
+%datatype Isac\_Ctxt =\\
+%\>\>Env of term * term\\
+%\>| Asm of term;\\
+%\\
+structure ContextData =  \alert{Proof\_Data}\\
+\>~(\alert{type T} = term list\\
+\>\>\alert{fun init \_} = []);\\
+\\
+%local\\
+%\>fun insert\_ctxt data = ContextData\alert{.map} (fn xs => distinct (data@xs));\\
+%in\\
+%\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
+%\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
+%end\\
+fun insert\_assumptions asms = \\
+\>\>\>ContextData\alert{.map} (fn xs => distinct (asms@xs));\\
+\\
+%local\\
+%\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
+%\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
+%\>\>| unpack\_asms [] = [];\\
+%\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
+%\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
+%\>\>| unpack\_envs [] = [];\\
+%in\\
+%\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
+%\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
+%end
+fun get\_assumptions ctxt = ContextData\alert{.get} ctxt;\\
+\\
+\\
+val declare\_constraints : \\
+\>\>\>term -> Proof.context -> Proof.context
+      \end{tabbing}
+    }}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Usage of Contexts}
+    \texttt{\footnotesize{
+      \begin{tabbing}
+xx\=xx\=xx\=xx\=xx\=\kill
+fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\
+\>  let\\
+\>\>    val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\
+\>\>    fun transfer [] to\_ctxt = to\_ctxt\\
+\>\>\>      | transfer (from\_asm::fas) to\_ctxt =\\
+\>\>\>\>\>          if inter op = (vars from\_asm) to\_vars = []\\
+\>\>\>\>\>         then transfer fas to\_ctxt\\
+\>\>\>\>\>          else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\
+\>  in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\
+\\
+fun parse thy str =\\
+\>(let val t = (\alert{typ\_a2real} o numbers\_to\_string)\\
+\>\>\>\>(\alert{Syntax.read\_term\_global thy} str)\\
+\>\>in SOME (cterm\_of thy t) end)\\
+\>\>\>handle \_ => NONE;\\
+\\
+fun parseNEW ctxt str = \\
+\>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
+\>\>\>handle \_ => NONE;
+      \end{tabbing}
+    }}
+
+
+\end{frame}
+
+\subsection[Redesign]{Redesign of \isac{} using contexts}
+\begin{frame}
+  \frametitle{Redesign of \isac{} using contexts}
+\begin{center} DEMO \end{center}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Deduction simplifies computation}
+\small{
+%\begin{onehalfspace}
+\begin{tabbing}
+xxx\=xxx\=\kill
+     \`$\mathit{(some)}\;\mathit{assumptions}$\\
+$\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
+%     \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
+%\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
+%\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
+\>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\ 
+     \`$x\not=3\land x\not=0$\\
+\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
+\>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
+%\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
+%\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
+\>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
+\>\>$-6 * x + 5 * x ^ 2 = 0$ \\
+\>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
+\>\>$[x = 0, x = \frac{6}{5}]$ \\
+     \`$x = 0\land x = \frac{6}{5}$\\
+\>$[\alert{x = 0}, x = \frac{6}{5}]$ \\
+     \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
+\>$[x = \frac{6}{5}]$ \\
+$[x = \frac{6}{5}]$
+\end{tabbing}
+}
+%\end{onehalfspace}
+\end{frame}
+
+\begin{frame}
+  \frametitle{More ``deduction'', \\less ``computation''}
+\footnotesize{\tt
+\begin{tabbing}
+xx\=xx\=xx\=xx\=xx\=xx\=\kill
+Script Solve\_root\_equation (e\_e::bool) (v\_v::real) =      \\
+\> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@   \\
+\>\>\>            (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\
+\>\>     (L\_L::bool list) =                                   \\
+\>\>\>            (SubProblem (Test',                           \\
+\>\>\>\>                         [linear,univariate,equation,test]\\
+\>\>\>\>                         [Test,solve\_linear])             \\
+\>\>\>\>                        [BOOL e\_e, REAL v\_v])             \\
+\>  in \alert{Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\      
+\end{tabbing}
+}
+\small{
+``Deductive'' part of Lucas-Interpretation relives the ``computational'' part: \alert{one statement becomes obsolete~!}
+}
+\end{frame}
+
+
+\begin{frame}
+  \frametitle{Redesign of \isac{} using contexts}
+Advantages of the redesign:
+\begin{itemize}
+\item type inference by \textit{local} contexts\\
+\pause
+     \alert{now user-input without type constraints~!}
+\pause
+\item consistent handling of logical data
+  \begin{itemize}
+  \item preconditions and partiality conditions in contexts
+  \item transfer of context data into subprograms clarified
+  \item transfer of context data from subprograms clarified
+  \end{itemize}
+\pause
+     \alert{now some statements become obsolete.}\\
+\end{itemize}
+\pause
+Now Lucas-interpretation shifts efforts from ``computation'' further to ``deduction''.
+\end{frame}
+
+
+
+\subsection[Code Improvement]{Improvement of functional code}
+\begin{frame}
+  \frametitle{Improvement of functional code}
+  \begin{itemize}
+  \item \textbf{code conventions}: Isabelle2011 published coding standards first time
+  \item \textbf{combinators}: Isabelle2011 introduced a library containing the following combinators:
+\\\vspace{0.2cm}
+\tiny{\tt%
+  val |$>$ : 'a * ('a -$>$ 'b) -$>$ 'b\\
+  val |-$>$ : ('c * 'a) * ('c -$>$ 'a -$>$ 'b) -$>$ 'b\\
+  val |$>>$ : ('a * 'c) * ('a -$>$ 'b) -$>$ 'b * 'c\\
+  val ||$>$ : ('c * 'a) * ('a -$>$ 'b) -$>$ 'c * 'b\\
+  val ||$>>$ : ('c * 'a) * ('a -$>$ 'd * 'b) -$>$ ('c * 'd) * 'b\\
+  val \#$>$ : ('a -$>$ 'b) * ('b -$>$ 'c) -$>$ 'a -$>$ 'c\\
+  val \#-$>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'b -$>$ 'd) -$>$ 'a -$>$ 'd\\
+  val \#$>>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'd) -$>$ 'a -$>$ 'd * 'b\\
+  val \#\#$>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'd) -$>$ 'a -$>$ 'c * 'd\\
+  val \#\#$>>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'e * 'd) -$>$ 'a -$>$ ('c * 'e) * 'd\\
+}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Example with combinators}
+    \texttt{\footnotesize{
+      \begin{tabbing}
+xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
+fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\
+\>| prep\_ori fmz thy pbt =\\
+\>\>\>let\\
+\>\>\>\>val ctxt = ProofContext.init\_global thy \\
+\>\>\>\>\> |> fold declare\_constraints fmz\\
+\>\>\>\>val ori = \\
+\>\>\>\>\> map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
+\>\>\>\>\>\> |> add\_variants\\
+\>\>\>\>val maxv = map fst ori |> max\\
+\>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
+\>\>\>\>val oris = coll\_variants ori\\
+\>\>\>\>\> |> map (replace\_0 maxv |> apfst)\\
+\>\>\>\>\> |> add\_id\\
+\>\>\>\>\> |> map flattup\\
+\>\>\>in (oris, ctxt) end;
+      \end{tabbing}
+    }}
+\dots which probably can be further polished.
+\end{frame}
+
+%\subsection[Future Development]{Preparation of Future Development}
+%\begin{frame}
+%  \frametitle{Preparation of Future Development}
+%
+%%  "Script Solve_root_equation (e_e::bool) (v_v::real) =       " ^
+%%  " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@    " ^
+%%  "            (Try (Rewrite_Set Test_simplify False))) e_e;  " ^
+%%  "     (L_L::bool list) =                                    " ^
+%%  "            (SubProblem (Test',                            " ^
+%%  "                         [linear,univariate,equation,test]," ^
+%%  "                         [Test,solve_linear])              " ^
+%%  "                        [BOOL e_e, REAL v_v])              " ^
+%%  "  in Check_elementwise L_L {(v_v::real). Assumptions})     "
+%\end{frame}
+%
+%\begin{frame}
+%  \frametitle{Preparation of Future Development}
+%    \begin{itemize}
+%    \item logical data for Isabelle provers in contexts
+%    \item \isac{} programming language more compact\\
+%      $\rightarrow$ context built automatically
+%    \end{itemize}
+%\end{frame}
+
+
+\section[Problems]{Problems encountered in the project}
+\begin{frame}
+  \frametitle{Problems encountered in the project}
+    \begin{itemize}
+    \item new Isabelle release in February 2011: update \sisac{} first
+\pause
+    \item lines of code (LOC) in Isabelle and \sisac{}\\ \vspace{0.2cm}
+\textit{
+    \begin{tabular}{lrl}
+      src/ & 1700 & $\,$k LOC\\
+      src/Pure/ & 70 & k LOC\\
+      src/Provers/ & 8 & k LOC\\
+      src/Tools/ & 800 & k LOC\\
+      src/Tools/isac/ & 37 & k LOC\\
+      src/Tools/isac/Knowledge & 16 & k LOC
+    \end{tabular}
+}
+\pause
+    \item changes scattered throughout the code ($\rightarrow$ grep)
+\pause
+    \item documentation of Isabelle very ``technical'' (no API)
+\pause
+   \item documentation of \sisac{} not up to date
+    \end{itemize}
+\end{frame}
+
+%\begin{frame}
+%  \frametitle{Lines of Code}
+%    \begin{tabular}{lr}
+%      src/ & 1700 k \\
+%      src/Pure/ & 70 k \\
+%      src/Provers/ & 8 k \\
+%      src/Tools/ & 800 k \\
+%      src/Tools/isac/ & 37 k \\
+%      src/Tools/isac/Knowledge & 16 k \\
+%    \end{tabular}
+%\end{frame}
+
+\section{Summary}
+\begin{frame}
+  \frametitle{Summary}
+The project succeeded in all goals:
+\begin{itemize}
+\item implemented Isabelle's contexts in \sisac{} such that
+\item user input requires no type constraints anymore
+\item consistent logical data is prepared for Isabelle's provers
+\end{itemize}
+\pause
+The course of the project was close to the plan:
+\begin{itemize}
+\item faster in writing new code
+\item slower in integrating the code into \sisac
+\end{itemize}
+\pause
+The project provided essential prerequisites for further development of the Lucas-interpreter.
+\end{frame}
+
+\end{document}
+
+