% $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}