diff -r 7f3760f39bdc -r f8845fc8f38d src/Doc/isac/mlehnfeld/presentation.tex --- a/src/Doc/isac/mlehnfeld/presentation.tex Mon Sep 16 12:27:20 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,469 +0,0 @@ -% $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 . -% -% 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 -{ - \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}{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} - -