separated Isac documentation (~~/doc-isac) from Isabelle documentation (~~/src/Doc)
1 % $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 $
5 % This file is a solution template for:
7 % - Talk at a conference/colloquium.
8 % - Talk length is about 20min.
13 % Copyright 2004 by Till Tantau <tantau@users.sourceforge.net>.
15 % In principle, this file can be redistributed and/or modified under
16 % the terms of the GNU Public License, version 2.
18 % However, this file is supposed to be a template to be modified
19 % for your own needs. For this reason, if you use this file as a
20 % template and not specifically distribute it as part of a another
21 % package/program, I grant the extra permission to freely copy and
22 % modify this file as you see fit and even to delete this copyright
31 \setbeamercovered{transparent}
32 % or whatever (possibly just delete it)
35 %\usepackage{setspace} %for "\begin{onehalfspace}"
36 \usepackage[english]{babel}
39 \usepackage[utf8]{inputenc}
43 \usepackage[T1]{fontenc}
44 % Or whatever. Note that the encoding and the font should match. If T1
45 % does not look nice, try deleting the line with the fontenc.
47 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
48 \def\sisac{{\footnotesize${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}}
50 \title[\isac: Computation \& Deduction] % (optional, use only with long paper titles)
51 {Integrating Computation and Deduction\\
54 \subtitle{Projektpraktikum: Introducing Isabelle's Contexts}
56 \author[Lehnfeld] % (optional, use only with lots of authors)
58 % - Give the names in the same order as the appear in the paper.
59 % - Use the \inst{?} command only if the authors have different
62 \institute % (optional, but mostly needed)
64 Vienna University of Technology\\
65 Institute of Computer Languages
67 % - Use the \inst command only if there are several affiliations.
68 % - Keep it simple, no one is interested in your street address.
70 % \date[CFP 2003] % (optional, should be abbreviation of conference name)
71 % {Conference on Fabulous Presentations, 2003}
72 % - Either use conference name or its abbreviation.
73 % - Not really informative to the audience, more for people (including
74 % yourself) who are reading the slides online
76 % \subject{Theoretical Computer Science}
77 % This is only inserted into the PDF information catalog. Can be left
82 % If you have a file called "university-logo-filename.xxx", where xxx
83 % is a graphic format that can be processed by latex or pdflatex,
84 % resp., then you can add a logo as follows:
86 % \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
87 % \logo{\pgfuseimage{university-logo}}
91 % Delete this, if you do not want the table of contents to pop up at
92 % the beginning of each subsection:
95 \begin{frame}<beamer>{Outline}
96 \tableofcontents[currentsection,currentsubsection]
101 % If you wish to uncover everything in a step-wise fashion, uncomment
102 % the following command:
104 %\beamerdefaultoverlayspecification{<+->}
113 \begin{frame}{Outline}
115 % You might wish to add the option [pausesections]
119 % Structuring a talk is a difficult task and the following structure
120 % may not be suitable. Here are some rules that apply for this
123 % - Exactly two or three sections (other than the summary).
124 % - At *most* three subsections per section.
125 % - Talk about 30s to 2min per frame. So there should be between about
126 % 15 and 30 frames, all told.
128 % - A conference audience is likely to know very little of what you
129 % are going to talk about. So *simplify*!
130 % - In a 20min talk, getting the main ideas across is hard
131 % enough. Leave out details, even if it means being less precise than
132 % you think necessary.
133 % - If you omit details that are vital to the proof/implementation,
134 % just say so once. Everybody will be happy with that.
136 \section[Introduction]{Introduction: Isabelle and \isac}
137 %\subsection[Isabelle \& \isac]{Isabelle and \isac}
139 \frametitle{Isabelle and \isac}
140 The task of this ``Projektpraktikum'' (6 ECTS) was to
142 \item study the concept of ``context'' in the theorem prover \textbf{Isabelle} from TU Munich
143 \item study basic concepts of the math assistant \sisac{} from TU Graz
145 \item redesign \sisac{} with respect to contexts
147 \item use contexts for type inference of user input
148 \item handle preconditions of specifications
149 \item clarify the transfer of context data from sub-programs to the calling program
152 \item introduce contexts to \sisac{} according to the new design
153 \item use the coding standards of Isabelle2011 for new code.
157 %\subsection[Computation \& Deduction]{Computation and Deduction in a Lucas-Interpreter}
159 \frametitle{Computation and Deduction in a Lucas-Interpreter}
160 \includegraphics[width=100mm]{overview.pdf}
163 \section[Contributions]{Contributions of the project to \isac}
164 \subsection[Contexts]{Isabelle's Contexts, advantages and use}
166 \frametitle{Advantages of Isabelle's Contexts}
167 Isabelle's context replaced theories because \dots:
169 \item theories are static containers of \textit{all} logical data
170 \item contexts are \textit{dynamic} containers of logical data:
172 \item functions for storing and retrieving various logical data
173 \item functions for type inference
174 \item provide data for Isabelle's automated provers
176 %\item e.g. theories have no direct functions for type inference
177 %\item replace function \texttt{parseNEW}
178 %\item assumptions \& environment $\rightarrow$ context
179 \item allow to conform with scopes for subprograms.
184 \frametitle{Isabelle's context mechanism}
188 %xx\=xx\=xx\=xx\=\kill
189 %datatype Isac\_Ctxt =\\
190 %\>\>Env of term * term\\
193 structure ContextData = \alert{Proof\_Data}\\
194 \>~(\alert{type T} = term list\\
195 \>\>\alert{fun init \_} = []);\\
198 %\>fun insert\_ctxt data = ContextData\alert{.map} (fn xs => distinct (data@xs));\\
200 %\>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\
201 %\>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\
203 fun insert\_assumptions asms = \\
204 \>\>\>ContextData\alert{.map} (fn xs => distinct (asms@xs));\\
207 %\>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\
208 %\>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\
209 %\>\>| unpack\_asms [] = [];\\
210 %\>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\
211 %\>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\
212 %\>\>| unpack\_envs [] = [];\\
214 %\>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\
215 %\>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\
217 fun get\_assumptions ctxt = ContextData\alert{.get} ctxt;\\
220 val declare\_constraints : \\
221 \>\>\>term -> Proof.context -> Proof.context
227 \frametitle{Usage of Contexts}
228 \texttt{\footnotesize{
230 xx\=xx\=xx\=xx\=xx\=\kill
231 fun transfer\_asms\_from\_to from\_ctxt to\_ctxt =\\
233 \>\> val to\_vars = get\_assumptions to\_ctxt |> map vars |> flat\\
234 \>\> fun transfer [] to\_ctxt = to\_ctxt\\
235 \>\>\> | transfer (from\_asm::fas) to\_ctxt =\\
236 \>\>\>\>\> if inter op = (vars from\_asm) to\_vars = []\\
237 \>\>\>\>\> then transfer fas to\_ctxt\\
238 \>\>\>\>\> else transfer fas (insert\_assumptions [from\_asm] to\_ctxt)\\
239 \> in transfer (get\_assumptions from\_ctxt) to\_ctxt end\\
241 fun parse thy str =\\
242 \>(let val t = (\alert{typ\_a2real} o numbers\_to\_string)\\
243 \>\>\>\>(\alert{Syntax.read\_term\_global thy} str)\\
244 \>\>in SOME (cterm\_of thy t) end)\\
245 \>\>\>handle \_ => NONE;\\
247 fun parseNEW ctxt str = \\
248 \>\>\>SOME (\alert{Syntax.read\_term ctxt} str |> numbers\_to\_string)\\
249 \>\>\>handle \_ => NONE;
256 \subsection[Redesign]{Redesign of \isac{} using contexts}
258 \frametitle{Redesign of \isac{} using contexts}
259 \begin{center} DEMO \end{center}
263 \frametitle{Deduction simplifies computation}
265 %\begin{onehalfspace}
268 \`$\mathit{(some)}\;\mathit{assumptions}$\\
269 $\mathit{solve}\;(\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}, x)$\\
270 % \`$x ^ 2 - 6 * x + 9\not=0\land x ^ 2 - 3 * x\not=0$\\
271 %\>$\frac{x}{x ^ 2 - 6 * x + 9} - \frac{1}{x ^ 2 - 3 * x} = \frac{1}{x}$ \\ \\
272 %\>$\frac{x}{x ^ 2 + -1 * (6 * x) + 9} + \frac{-1 * 1}{x ^ 2 + -1 * (3 * x)} = \frac{1}{x}$ \\ \\
273 \>$\frac{3 + -1 * x + x ^ 2}{9 * x + -6 * x ^ 2 + x ^ 3} = \frac{1}{x}$ \\
274 \`$x\not=3\land x\not=0$\\
275 \>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
276 \>$\mathit{solve}\;((3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3), x)$ \\
277 %\>\>$(3 + -1 * x + x ^ 2) * x = 1 * (9 * x + -6 * x ^ 2 + x ^ 3)$ \\
278 %\>\>$(3 + -1 * x + x ^ 2) * x - 1 * (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
279 \>\>$(3 + -1 * x + x ^ 2) * x - (9 * x + -6 * x ^ 2 + x ^ 3) = 0$ \\
280 \>\>$-6 * x + 5 * x ^ 2 = 0$ \\
281 \>\>$\mathit{solve}\;(-6 * x + 5 * x ^ 2 = 0, x)$ \\
282 \>\>$[x = 0, x = \frac{6}{5}]$ \\
283 \`$x = 0\land x = \frac{6}{5}$\\
284 \>$[\alert{x = 0}, x = \frac{6}{5}]$ \\
285 \`\alert{$\mathit{Check\_Elementwise}\;\mathit{Assumptions}:x\not=0\land x = 0$}\\
286 \>$[x = \frac{6}{5}]$ \\
294 \frametitle{More ``deduction'', \\less ``computation''}
297 xx\=xx\=xx\=xx\=xx\=xx\=\kill
298 Script Solve\_root\_equation (e\_e::bool) (v\_v::real) = \\
299 \> (let e\_e = ((Try (Rewrite\_Set norm\_equation False)) \@\@ \\
300 \>\>\> (Try (Rewrite\_Set Test\_simplify False))) e\_e; \\
301 \>\> (L\_L::bool list) = \\
302 \>\>\> (SubProblem (Test', \\
303 \>\>\>\> [linear,univariate,equation,test]\\
304 \>\>\>\> [Test,solve\_linear]) \\
305 \>\>\>\> [BOOL e\_e, REAL v\_v]) \\
306 \> in \alert{Check\_elementwise L\_L \{(v\_v::real). Assumptions\}})\\
310 ``Deductive'' part of Lucas-Interpretation relives the ``computational'' part: \alert{one statement becomes obsolete~!}
316 \frametitle{Redesign of \isac{} using contexts}
317 Advantages of the redesign:
319 \item type inference by \textit{local} contexts\\
321 \alert{now user-input without type constraints~!}
323 \item consistent handling of logical data
325 \item preconditions and partiality conditions in contexts
326 \item transfer of context data into subprograms clarified
327 \item transfer of context data from subprograms clarified
330 \alert{now some statements become obsolete.}\\
333 Now Lucas-interpretation shifts efforts from ``computation'' further to ``deduction''.
338 \subsection[Code Improvement]{Improvement of functional code}
340 \frametitle{Improvement of functional code}
342 \item \textbf{code conventions}: Isabelle2011 published coding standards first time
343 \item \textbf{combinators}: Isabelle2011 introduced a library containing the following combinators:
346 val |$>$ : 'a * ('a -$>$ 'b) -$>$ 'b\\
347 val |-$>$ : ('c * 'a) * ('c -$>$ 'a -$>$ 'b) -$>$ 'b\\
348 val |$>>$ : ('a * 'c) * ('a -$>$ 'b) -$>$ 'b * 'c\\
349 val ||$>$ : ('c * 'a) * ('a -$>$ 'b) -$>$ 'c * 'b\\
350 val ||$>>$ : ('c * 'a) * ('a -$>$ 'd * 'b) -$>$ ('c * 'd) * 'b\\
351 val \#$>$ : ('a -$>$ 'b) * ('b -$>$ 'c) -$>$ 'a -$>$ 'c\\
352 val \#-$>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'b -$>$ 'd) -$>$ 'a -$>$ 'd\\
353 val \#$>>$ : ('a -$>$ 'c * 'b) * ('c -$>$ 'd) -$>$ 'a -$>$ 'd * 'b\\
354 val \#\#$>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'd) -$>$ 'a -$>$ 'c * 'd\\
355 val \#\#$>>$ : ('a -$>$ 'c * 'b) * ('b -$>$ 'e * 'd) -$>$ 'a -$>$ ('c * 'e) * 'd\\
361 \frametitle{Example with combinators}
362 \texttt{\footnotesize{
364 xx\=xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
365 fun prep\_ori [] \_ \_ = ([], e\_ctxt)\\
366 \>| prep\_ori fmz thy pbt =\\
368 \>\>\>\>val ctxt = ProofContext.init\_global thy \\
369 \>\>\>\>\> |> fold declare\_constraints fmz\\
371 \>\>\>\>\> map (add\_field thy pbt o split\_dts o the o parseNEW ctxt) fmz\\
372 \>\>\>\>\>\> |> add\_variants\\
373 \>\>\>\>val maxv = map fst ori |> max\\
374 \>\>\>\>val maxv = if maxv = 0 then 1 else maxv\\
375 \>\>\>\>val oris = coll\_variants ori\\
376 \>\>\>\>\> |> map (replace\_0 maxv |> apfst)\\
377 \>\>\>\>\> |> add\_id\\
378 \>\>\>\>\> |> map flattup\\
379 \>\>\>in (oris, ctxt) end;
382 \dots which probably can be further polished.
385 %\subsection[Future Development]{Preparation of Future Development}
387 % \frametitle{Preparation of Future Development}
389 %% "Script Solve_root_equation (e_e::bool) (v_v::real) = " ^
390 %% " (let e_e = ((Try (Rewrite_Set norm_equation False)) @@ " ^
391 %% " (Try (Rewrite_Set Test_simplify False))) e_e; " ^
392 %% " (L_L::bool list) = " ^
393 %% " (SubProblem (Test', " ^
394 %% " [linear,univariate,equation,test]," ^
395 %% " [Test,solve_linear]) " ^
396 %% " [BOOL e_e, REAL v_v]) " ^
397 %% " in Check_elementwise L_L {(v_v::real). Assumptions}) "
401 % \frametitle{Preparation of Future Development}
403 % \item logical data for Isabelle provers in contexts
404 % \item \isac{} programming language more compact\\
405 % $\rightarrow$ context built automatically
410 \section[Problems]{Problems encountered in the project}
412 \frametitle{Problems encountered in the project}
414 \item new Isabelle release in February 2011: update \sisac{} first
416 \item lines of code (LOC) in Isabelle and \sisac{}\\ \vspace{0.2cm}
419 src/ & 1700 & $\,$k LOC\\
420 src/Pure/ & 70 & k LOC\\
421 src/Provers/ & 8 & k LOC\\
422 src/Tools/ & 800 & k LOC\\
423 src/Tools/isac/ & 37 & k LOC\\
424 src/Tools/isac/Knowledge & 16 & k LOC
428 \item changes scattered throughout the code ($\rightarrow$ grep)
430 \item documentation of Isabelle very ``technical'' (no API)
432 \item documentation of \sisac{} not up to date
437 % \frametitle{Lines of Code}
438 % \begin{tabular}{lr}
440 % src/Pure/ & 70 k \\
441 % src/Provers/ & 8 k \\
442 % src/Tools/ & 800 k \\
443 % src/Tools/isac/ & 37 k \\
444 % src/Tools/isac/Knowledge & 16 k \\
451 The project succeeded in all goals:
453 \item implemented Isabelle's contexts in \sisac{} such that
454 \item user input requires no type constraints anymore
455 \item consistent logical data is prepared for Isabelle's provers
458 The course of the project was close to the plan:
460 \item faster in writing new code
461 \item slower in integrating the code into \sisac
464 The project provided essential prerequisites for further development of the Lucas-interpreter.