Subversion Repositories TPPL

Rev

Rev 57 | Blame | Compare with Previous | Last modification | View Log | RSS feed

% /usr/share/doc/latex-beamer/solutions/conference-talks/conference-ornate-20min.en.tex

%\documentclass{beamer} % is [11pt]
\documentclass[10pt]{beamer}
\mode<presentation>
{
  \usetheme{Hannover}
  \setbeamercovered{transparent}
}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage[normalem]{ulem
}%strike-through in texts by \sout
\usepackage{cancel}        %strike-through in math by \cancel

\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}$}}
\def\dedu{{\sc Deducation}}

\title[Computer Algebra\\$\leadsto$\\Isabelle\\$\;$]
  {More Computer Algebra for Isabelle ?}
\subtitle{Computation meets Deduction}
\author{Wolfgang Schreiner\\ Walther Neuper}
\institute{Research Institute for Symbolic Computation\\
  Johannes Kepler University Linz}

\date{Munich, 6.2.2013
}
%\subject{This is only inserted into the PDF information catalog}

%WN080919 did not work ...
% \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>
    \frametitle{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}
  \frametitle{Outline
}
  \tableofcontents
  % You might wish to add the option [pausesections]
\end{frame}

\section[Motivations]{Motivations
}
%\subsection[TODO]{TODO}
\begin{frame}
\frametitle{RISC Linz}
3 full professors, 6 associate professors, 9 other faculty members,
about 6 postdocs and 20 PhD students.\\

\begin{itemize}
\item Computer Algebra/Algebraic Geometry
\begin{itemize}
\item Winkler, Schicho, \ldots
\end{itemize}
\item Algorithmic Combinatorics
\begin{itemize}
\item Paule, Kauers, Schneider, Pillwein, \ldots
\end{itemize}
\item Automated Theorem Proving (Theorema)
\begin{itemize}
\item Buchberger, Jebelean, Kutsia, \ldots
\end{itemize}
\item Formal Methods, Parallel/Distributed Computing
\begin{itemize}
\item Schreiner, Lichtenberger, \ldots
\end{itemize}
\end{itemize}

DK ``Computational Mathematics'', SFB ``Algorithmic and Enumerative Combinatorics'',
various R\&D projects.
\end{frame}

\begin{frame}
\frametitle{{\isac}-Project Graz}
\begin{itemize}
\item at Institute for Software Technology, Univ.of Technology\\
{\small headed by Peter Lucas formerly}
\item experimental system for math education
  \begin{itemize}
  \item {\sisac} is ``{\footnotesize${\cal I}\mkern-2mu{\cal
S}\mkern-5mu{\cal A}$
}belle for {\footnotesize${\cal C}$}alculations
in applied math''
  \item math-engine builds upon Isabelle
  \item ``Lucas-Interpretation''
    \begin{enumerate}
    \item determines a next step in a calculation
    \item checks a step (expression / thm) input by students
    \end{enumerate}
  \item experiments with user-guidance
  \end{itemize}
\pause
\item requires Computer Algebra (CA)
  \begin{itemize}
  \item joint student projects with RISC Linz
  \item implement CA using \alert{SML}
  \item found: \alert{better done using Isabelle}'s function package
\\and code generator
  \end{itemize}
\end{itemize}
\end{frame}

\section[CA $\leadsto$ Isabelle]{Computer Algebra's (CA) Steps towards Isabelle}

\subsection[1: Isabelle Mechanisms]{Step 1: Exploit Isabelle's Computational Mechanisms}
\begin{frame} \frametitle{1: Exploit Isabelles Mechanisms}
Example \textbf{Cancellation of polynomials}: \alert{implicit} specification \dots
{\tt\tiny
\begin{tabbing}
123\=12\=12\=12\=12\kill
\>   locale gcd\_poly = \\
\>\>     fixes gcd\_poly :: int poly -> int poly -> int poly \\
\>\>     assumes gcd\_poly a b = c \\
\>\>\>       and not (a = [:0:]) \\
\>\>\>       and not (b = [:0:]) \\
\>\>\>       ==> c dvd a and c dvd b \\
\>\>\>\>         and forall c'. (c' dvd a  and  c' dvd b) => c' =< c
\end{tabbing}
}
\pause
\dots by 77 functions in 600 LoCs shall ease interactive proof \dots
{\footnotesize
\begin{tabbing}
12\=12\=12\=12\=12\kill
\> lemma cancel:\\
\>\> assumes \sout{asm1: "(x$\hat{\;\;}$2 - y$\hat{\;\;}$2) = (x + y) * (x - y)"} \\
\>\>\> \sout{and asm2: "x$\hat{\;\;}$2 - x * y = x * (x - y)"}\\
\>\>\> \sout{and asm3: "x $\not=$ 0" and} asm4: "x$\hat{\;\;}$2 - x * y $\not=$ 0" \\
\>\> shows "(x$\hat{\;\;}$2 - y$\hat{\;\;}$2) / (x$\hat{\;\;}$2 - x * y) = (x + y) / (x::real)"\\
\>\> apply (insert \sout{asm1 asm2 asm3} asm4)\\
\>\> apply simp\\
\> done
\end{tabbing}
}%\small
\pause
\dots and automate simplification:
{\tiny
$$\frac{x^2-y^2}{x^2-x\cdot y}=\frac{\cancel{(x+y)}\cdot(x-y)}{\cancel{(x+y)}\cdot x}=\frac{x-y}{x}\;\land\;x+y\not=0\;\land\;x\not=0$$
}
\end{frame}

\begin{frame} \frametitle{1: Exploit Isabelles Mechanisms}
For \texttt{gcd\_poly}, for instance, do the following:
\begin{enumerate}
\item implement the 77 functions using the \emph{function package}.
\item prove the postcondition: {\small $
c \;{\it dvd}\; a \land c \;{\it dvd}\; b \land \forall
c^\prime. (c^\prime \;{\it dvd}\; a \land c^\prime \;{\it dvd}\; b)
\Rightarrow c^\prime \leq c$}
\item use generated theorems interactively, e.g. \\
  {\footnotesize{\texttt{value ``gcd\_poly}\\
  \hspace{0.3cm}\texttt{poly [:poly [:0, 0, 1:] x:] poly [:2:] y
}\\ %fixme constant coeff
  \hspace{0.3cm}\texttt{poly [:poly [:0, 1, 1:] x:] poly [:1:] y''} %fixme constant coeff
  }}%small
\item translate the 77 functions to SML by code generator
\item integrate the generated code into the simplifier.\\
\end{enumerate}

\pause
\bigskip
Note: {\small\texttt{gcd\_poly \_\_ [:0:]}} would cause
\textbf{non-termination} in several deeply nested functions (violation
of precondition).
\end{frame}

\begin{frame} \frametitle{1: Exploit Isabelles Mechanisms}
Possible directions:
\begin{itemize
}
\item make CA functions existing in Isabelle efficient via code
generation: Differential Equations,
%\footnote{http://afp.sourceforge.net/entries/Ordinary\_Differential\_Equations.shtml},
Fast Fourier Transform,
%\footnote{http://afp.sourceforge.net/entries/FFT.shtml}
Gauss-Jordan Elimination
\footnote{http://afp.sourceforge.net/entries/Gauss-Jordan-Elim-Fun.shtml},
etc
\item compute results from existing CA (instead of
checking {\em given} results): Gr\"obner
Bases~\footnote{http://isabelle.in.tum.de/dist/library/HOL/Groebner\_Basis.html},
etc
\item implement new CA functionality for selected topics
\item explore Isabelle's mechanisms to their limits: function package,
code generation, syntax, exception handling, etc
\end{itemize}
\pause
Open issues:
\begin{itemize}
\item How handle partiality? ``Totalization'' ($\frac{a}{0}\leadsto
0$
, \dots) --- non-evaluation like in CAS (${\it hd}\;[\,]\leadsto{\it
hd}\;[\,]$
, \dots) --- guarding evaluation by preconditions?
\item Nested exception handling in nested functions?
\item \dots?
\end{itemize}
\end{frame}

\begin{frame} \frametitle{1: Exploit Isabelles Mechanisms}
{\it
Summary:  
\medskip \\
Isabelle's computational mechanisms (function package $+$ code
generator) appear \alert{powerful engough to tackle implementation of
CA}, which
\begin{enumerate}
\item includes most advanced functionality implemented in contemporary
CAS,
\item is more trustable than respective CA implementations
\item allow straight forward proving correctness
\item is efficient enough for engineering practice due to code
generation.
\end{enumerate}
}%\it
\end{frame}

\subsection[2: multivalued funs]{Step 2: Novel Approaches to ``multivalued functions''}
\begin{frame} \frametitle{Step 2: ``multivalued functions''}
Examples: terms with multivalued ``functions'':
{\footnotesize
\[
\begin{aligned}
  \sin{x} &= y  \\
  x       &= \arcsin{y} \quad ???\\
  x       &=
  \begin{cases}
    \{\} & y<-1 \;\lor\; 1< y\\
    \!\begin{aligned
}[b
]%http://tex.stackexchange.com/questions/5183/split-like-environment-inside-cases-environment
       & \{x. \;\sin{x}=y\land
           \forall x^\prime. \;\sin{x^\prime}=y \Rightarrow \\
       & \quad \exists k\in{\cal Z}.\;x^\prime =  2k   \pi-x
                                 \lor x^\prime = (2k+1)\pi+x\}
    \end{aligned
}           & -1 \leq y \;\land\; y < 0\\[1ex]%#
    \!\begin{aligned}[b]%http://tex.stackexchange.com/questions/5183/split-like-environment-inside-cases-environment
       & \{x. \;\sin{x}=y\land
           \forall x^\prime. \;\sin{x^\prime}=y \Rightarrow \\
       & \quad \exists k\in{\cal Z}.\;x^\prime =  2k   \pi+x
                                 \lor x^\prime = (2k+1)\pi-x\}
    \end{aligned}           & 0 \leq y \;\land\; y \leq 1
  \end{cases}
\end{aligned}
\]

\[
 \arctan x + \arctan y = arctan \left( \frac{x+y}{1-xy} \right) +
  \begin{cases}
   \pi  & xy > 1 \land x > 0 \\
   0    & xy < 1  \\
   -\pi & xy > 1 \land x < 0
  \end{cases}
\
]
}%small

\bigskip
These terms give raise to \textbf{branching problems},\\
branches connected with assumptions.
\end{frame}

\begin{frame} \frametitle{Step 2: ``multivalued functions''}
Major deficiencies in state-of-the-art CA result from \\
(1) under-\textit{specification}
and (2) weak \textit{deductive mechanisms}.

\bigskip
\alert{Isabelle {\em has} concepts and mechanisms} to tackle the deficiencies:
\begin{enumerate}
\item $\log, \exp, \sin, \arcsin, etc$ are rigorously \textit{specified} as functions (not relations)
\item \textit{Deductive mechanisms} are present: provers, contexts,
tactics, etc.
\end{enumerate}

\pause
\bigskip
Using these mechanisms \alert{promise substantial advances} in:
\begin{itemize}
\item Simplification involving multivalued ``functions'', radicals.
\item Integration of terms containing multivalued ``functions''
\item Equation solving with multivalued ``functions''.
\end{itemize}

\end{frame}

\begin{frame} \frametitle{Step 2: ``multivalued functions''}
Possible directions:
\begin{itemize}
\item Clarify principles for overcoming deficiencies in CA
  \begin{itemize}
  \item Which provers for which kinds of assumptions ?
  \item Handle assumptions using Isabelle's contexts
  \item Expressiveness of assumptions (full predicate calculus ?)
  \end{itemize}
\item Design specific improvements for particular deficiencies
\item Implement improvements for selected topics in Isabelle
\end{itemize}

\pause
\medskip
Open issues:
\begin{itemize}
\item Interplay between computation and deduction during
simplification: How stop simplifier for
  \begin{itemize}
  \item for automated proof ?
  \item for interactive proving ?
  \item for debugging (inspecting context, etc) ?
  \end{itemize}
\item Code generation for functions with integrated proving
\item How call deductive mechanisms from generated code ?
\end{itemize}
\end{frame}

\begin{frame} \frametitle{Step 2: ``multivalued functions''}
{\it
Summary:
\medskip\\
``Multivalued functions'' is an important topic, \\
suffers from
\alert{long-standing deficiencies unresolved in CA}.
\pause
\medskip\\
Handling assumptions appears most \alert{promising by deductive mechanisms}
\dots not yet tackled, because
\begin{itemize}
\item CA developers are not interested (e.g. no logics) ?
\item TP systems are not ready (e.g. no complex functions yet) ?\medskip
\end{itemize}
\pause
Calling deductive mechanisms during computation would
require \alert{Isabelle to adapt}
\begin{itemize}
\item the simplifier for calls during ``execution'' of
functions
\item the code generator for inserting ``call-backs'' to provers.
\end{itemize}
}%\it
\end{frame}

\subsection[3: Modularisation]{Step 3: Modularisation for Large CA Features}
\begin{frame} \frametitle{Step 3: Modularisation for CA}
Example \textbf{Symbolic Integration}: the
Risch-algorithm~\footnote{as well as improvements by Lazard/Rioboo/Trager and others}
decomposes an integral into polynomial parts
{\footnotesize
$$\int{\frac{x^5-2x^4+x^3+x+5}{x^3-2x^2+x-2}}dx=\int{x^2}dx+\int{\frac{3}{x-2}}dx+\int{\frac{-x-1}{x^2+1}}dx$$
}
and transcendental parts
{\footnotesize
\[
\begin{aligned}
  \int{\frac{-e^x-x+ \ln(x)x+\ln(x)xe^x}{x(e^x+x)^2}}dx &= \\
    \int{\frac{1+e^x}{(e^x+x)^2}}=-\frac{1}{e^x+x} \;\dots\; \\
    \dots &\\
    \dots &= -\frac{\ln(x)}{e^x+x}
\end{aligned}
\
]
}
\dots cascade of sub-problems: apply Liouville's theorem, compute the Risch differential equation, \dots

\bigskip
The amount of sub-problems raises the issue of \textbf{modularisation
}.
%?TODO: show implicit specification for one sub-problem?
\end{frame}

\begin{frame} \frametitle{Step 3: Modularisation for CA}
Possible directions:
\begin{itemize}
\item Clarify concepts of modularisation for CA in large
\item Relation of deductive and computational structure\\
in the architecture
\item Comparison with other approaches\\
{\small VDM, ``System of Systems'', ``Design by Contract'', \dots}
\end{itemize}

\pause\medskip
Open issues:
\begin{itemize}
\item Representation of \textit{implicit} specifications in Isabelle?\\
  locales? an additional type of data? \dots
\item What is the structure of collections of such specifications?\\
  trees? dags? \dots
\item How adjust presentation of collections to Isabelle/Isar's document model?
\end{itemize}
\end{frame}

\begin{frame} \frametitle{Step 3: Modularisation for CA}
{\it
Summary:
\medskip\\
Large CA modules exhibit \alert{computational {\em and} deductive
structure}.
\medskip\\
Need to connect \alert{programs with implicit specifications}:
\begin{itemize}
\item preconditions
  \begin{itemize}
  \item require evaluation by deductive mechanisms
  \item guard programs, i.e. start execution if preconditions 'true'
  \end{itemize}
\item postconditions of sub-programs
  \begin{itemize}
  \item support proving the postcondition of the main-program
  \item fill contexts for evaluating preconditions of sub-programs.\medskip
  \end{itemize}
\end{itemize}
In Isabelle, this connection involves rethinking of
\begin{itemize}
\item the function package
\item the document model (multitude of parallel models)
\end{itemize}
}%\it
\end{frame}

\subsection[4: Open Issues 1..3]{Step 4: Tackle Open Issues from Points 1..3}
\begin{frame} \frametitle{Step 4: Tackle Open Issues}
Advancing CA beyond the state-of-the-art stepwise increases
challenges for Isabelle:
\begin{enumerate}
\item guard computation (i.e. evaluation by simplification, execution of generated code); thus improve
  \begin{itemize}
  \item conciseness of code (no specific code for partiality!)
  \item acceptance by mathematicians and engineers ($\frac{a}{0}=0..$)
  \end{itemize}
\item call deductive mechanisms during computation\\
  (Step 2: ``multivalued functions'')
\item connect functions with implicit specifications\\
  (Step 3: large modules)
\item Further issues
  \begin{itemize
}
  \item enhance calculational mechanisms: floating-point arithmetic,
% Linear arithmetic, Presburger arithmetic, floating-point
% arithmetic, normalising terms in semi-rings, etc.
  \item parallel execution, exception handling, \dots
  \end{itemize}
\end{enumerate
}
Sort out the issues to a consistent design. %,\\
%Sort out the issues to a project plan.
\end{frame}

\subsection[5: Beyond CA?]{Step 5: Towards Application beyond CA ?
}
% AFP: 2012-11-14: A Separation Logic Framework for Imperative HOL
% Author: Peter Lammich and Rene Meis\\
% ?Florian: ``...As we target Imperative HOL, our programs can be translated to efficiently executable code in various target languages, including ML, OCaml, Haskell, and Scala.'' ... how does ImpHOL relate to codegen ?

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-20}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-30}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-40}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-50}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-60}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-70}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Visions for engineering}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/prog-prove-0ALL}
\end{figure}
\end{frame}

\section[Cooperations?]{Cooperations ?}

\begin{frame} \frametitle{Cooperations?}  
This presentation intends to prepare for future
co-operations between Theorem Proving Group and RISC. Possible first
steps:
\begin{itemize}
\item Implement CA (gcd\_poly, cylindrical algebraic
decomposition, Gr\"obner bases, etc) in Isabelle as is
($\approx$ Step 1).\\ \textit{Means: isabelle-users@cl.cam.ac.uk}
\pause
\item Improve state-of-the-art of CA, probably with ad-hoc adaptions
of Isabelle ($\approx$ Step 1 $\leadsto$ Step 2).\\ \textit{Means:
\_?\_
}
%\pause
\item Contribute to integration of Isabelle's computational and
deductive mechanisms ($\approx$ Step 3 $+$ 4).\\ \textit{Means: PostDoc
familiar with Isabelle development
}
\pause
%\item \dots
\item \dots
\item Promote Isabelle as a Formal-Methods tool in Engineering?
%Provide verified CAS for engineering (not only software e.!)?\\
($\leadsto$ Step 5)\medskip
\end{itemize}
Target: funded research project(s).
\end{frame}


\end{document
}