% $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{parse}
%\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 parse ctxt str = \\
\>\>\>(\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 (parse 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}


