Subversion Repositories TPPL

Rev

Blame | Last modification | View Log | RSS feed

% outdated version kept for simple copies
% outdated version kept for simple copies
% outdated version kept for simple copies

\documentclass{beamer}
\mode<presentation>
{
  \usetheme{Hannover}
  \setbeamercovered{transparent}
}
\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage[normalem]{ulem}

\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[TP-based\\Prog.Lang.]
  {Design and Prototype for a\\TP-based Programming Language\\
   \alert{************* DRAFT VERSION *************}
}
%\subtitle{Preparation for Cooperation Linz --- Munich}
\subtitle{Preparation for a Research Proposal}
\author{Wolfgang {Schreiner}\\Walther Neuper}
\institute{Research Institute for Symbolic Computation\\
  Johannes Kepler University Linz}

\date{Munich, ddmmyy
}
%\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[Undefined CA]{Computer Algebra is Undefined in Terms of Logics}
\begin{frame}
\frametitle{Motivations I}
There are well-known deficiencies in Computer Algebra:
\begin{itemize}
\item
  \begin{thebibliography}{10}
    \bibitem{davenport-10:multivalued}James Davenport.
    \newblock The challenges of multivalued "functions".
    \newblock {\em Lecture Notes in Computer Science
}, 6167:1--12, 2010.
    % \newblock Invited talk at Artificial Intelligence and Symbolic Computation
    % 2010, part of the Conferences in Intelligent Mathematics 2010, 4-10 July
    % 2010. Paris, France.
  \end{thebibliography}
  Why not manage conditions by use of TP machinery~!?!
\item Solutions of equations get lost
\item TODO
\item TODO
\end{itemize
}
%\pause
\bigskip \textit{\textbf{Contribute to adopting Computer Algebra as \\
trustable parts in mechanised proofs!}}
\end{frame}

\subsection[Weak Computation]{Isabelle Lacks some of Advanced Computer Algebra}
\begin{frame}
\frametitle{Motivations II
}
Isabelle is a Theorem Prover (TP), calculational abilities are being gradually improved,
%\pause
however:
  \begin{thebibliography}{10}
    \bibitem[TFH12]{isa-robot-12}
    Holger T\"aubig, Udo Frese, Christoph L\"uth et.al.
    \newblock Guaranteeing functional safety: Design for provability and
      computer-aided verification.
    \newblock {\em Autonomous Robots}, 32(3):303--331, April 2012.    
  \end{thebibliography}
\medskip still state on p.326: \dots \textit{`` involves extensive algebraic
manipulations, a task for which theorem provers like
Isabelle are not ideally suited.''
}

%\pause
\bigskip \textit{\textbf{Contribute to extending Isabelle's executable fragment to a ``TP-based programming language''!}}
\end{frame}

\subsection[Informal Engineering]{Engineering is not at the State-of-the-Art in Formality}
\begin{frame}
\frametitle{Motivations III}
Software support for engineering advances in various directions \dots
\begin{itemize}
\item virtual prototyping
\item simulation
\item visualisation
\item animation
\end{itemize
}
%\dots
\medskip \dots advertised as ``System Modelers'':\\
\texttt{http://www.\textbf{maple}soft.com/products/maplesim/\\
http://www.\textbf{wolfram}.com/system-modeler/
}\\

%\pause
\bigskip \textit{\textbf{Contribute to %underpinning
software for engineers with logical/formal foundations and tools!}}
\end{frame}

\begin{frame} \frametitle{Logical/formal SW support \\for engineers}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/fig-TPPL-survey-20}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Logical/formal SW support \\for engineers}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/fig-TPPL-survey-50}
\end{figure}
\end{frame}

\begin{frame} \frametitle{Logical/formal SW support \\for engineers}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/fig-TPPL-survey-60}
\end{figure}
\end{frame
}

% \begin{frame} \frametitle{Logical/formal SW support \\for engineers}
% \begin{figure} [htb]
% \includegraphics[width=100mm]{fig/fig-TPPL-survey-70}
% \end{figure}
% \end{frame}

\begin{frame} \frametitle{Logical/formal SW support \\for engineers}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/fig-TPPL-survey-80}
\end{figure}
\end{frame}

\section[Goals]{Research Goals}

\subsection[Deduct. -- Comput.]{Reconsider Deduction --- Computation}
\begin{frame} \frametitle{Deduction --- Computation}
\begin{figure} [htb]
\includegraphics[width=100mm]{fig/fig-TPPL-dedu-comp-0ALL}
\end{figure}
\end{frame
}

%\subsection[Computer Algebra]{Provide Computer Algebra for Proofs}
\subsection[Computer Algebra]{Make Computer Algebra Trustable Parts of Proofs}
\begin{frame} \frametitle{E.g. algebraic simplification}
{\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\\
\>\>\>\> $\frac{x^2-y^2}{x^2-x\cdot y}=\frac{\not{(x+y)}\cdot(x-y)}{\not{(x+y)}\cdot x}=\frac{x-y}{x}\;\land\;x+y\not=0\;\land\;x\not=0$
\\
%\\
\> lemma add:\\
\>\> 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$\hat{\;\;}$2 - x * y $\not=$ 0" and asm4: "x $\not=$ 0"\\
\>\> shows "x / (x$\hat{\;\;}$2 - y$\hat{\;\;}$2) + y / (x$\hat{\;\;}$2 + x * (y::real)) =\\
\>\>\> x * x / (x * (x + y) * (x - y)) + y * (x - y) / (x * (x + y) * (x - y))"\\
\>\> apply (insert \sout{asm1 asm2} asm3 asm4)\\
\>\> apply simp\\
\>\> apply (simp add: algebra\_simps)\\
\> done\\
\>\>\>\> $\frac{x}{x^2-y^2}+\frac{y}{x^2-x\cdot y}=
          \frac{x\cdot x}{x\cdot(x-y)\cdot(x+y)}+\frac{y\cdot(x+y)}{x\cdot(x-y)\cdot(x+y)}=
          \frac{x\cdot x+y\cdot(x-y)}{x\cdot(x+y)\cdot(x-y)}\;\land\dots$
\\
\end{tabbing}
}%small
\end{frame}

% \begin{frame} \frametitle{Improve SW support \\for engineers}
% \begin{figure} [htb]
% \includegraphics[width=100mm]{fig/fig-TPPL-survey-50}
% \end{figure}
% \end{frame}

\begin{frame} \frametitle{Implement Trustable CA \footnote{\small TP is ``Theorem proving'', CA is ``Computer Algebra''}}
{\small
\begin{itemize}
\item Improve particularly error-prone parts of CA:
  \begin{itemize}
  \item transformation of terms with ``multivalued functions''
  \item equations with terms of ``multivalued functions''
  \item \dots TODO
  \end{itemize}
\item CA algorithms which are missing in Isabelle:
  \begin{itemize}
  \item Algebra, simplification --- algebraic simplification
  \item Gr\"obner Bases --- solving equational systems
  \item Multivariate Analysis --- integration
  \item Information Theory --- non-Shannon-type inequalities
  \end{itemize}
\item Implement CA in different kinds of integration with Isabelle:
  \begin{itemize}
  \item external oracle with subsequent verification by Isabelle
  \item \dots ?
  \item implementation in a ``TP-based program'', see below
  \end{itemize}
\item Implement the (ded.+alg.) knowledge for the case study
\end{itemize}
}%small
\end{frame}

%\subsection[]{Extend Executable Fragement of Isabelle}
%\subsection[Prog. Language]{Develop a Programming Language for Isabelle}
\subsection[Prog. Language]{Prototype a TP-based Programming Language}
\begin{frame} \frametitle{Prototype TP-based PL}
{\small
\begin{itemize}
\item Extend the executable fragment of Isabelle:
  \begin{itemize}
  \item combine many functions in one program
  \item call Computer Algebra in a ``trustable'' way
  \item consider parallelism (parallel map in matrices, etc)
  \end{itemize}
\item Extend interpretation beyond the simplifier:
  \begin{itemize}
  \item interpretation over several functions
  \item extend respective proof tools
  \item provide guards (pre/postcondition) for subprograms
  \item provide tools for debugging (inspect contexts, \dots)
  \end{itemize}
\item Extend code generation to the full range of the PL\\
  (Code generation is a major motivation in engineering !)
\item Exemplary application of the TP-based PL
  \begin{itemize}
  \item to engineering problems in the case study
  \item to CA algorithms
  \end{itemize}
\end{itemize}
}%small
\end{frame}

%\subsection[Support Engineering]{Support Usage in an Engineering Domain}
\subsection[Support Engineering]{Perform a Case Study in Formal Domain Engineering}
\begin{frame} \frametitle{Formal Domain Engineering}
{\small
\begin{itemize}
\item Start with 3 different institutes at TU Graz
  \begin{itemize}
  \item identify topics and engineering problems
    \begin{itemize}
    \item promising for current research
    \item promising for education in ``Formal Methods''
    \end{itemize}
  \item identify (deductive) Isabelle knowledge required
  \item request CA algorithms required for solving the problems
  \end{itemize}
\item Select the most promising and affordable problems
\item For the selected problems, within 3-5 student projects
  \begin{enumerate}
  \item implement the deductive knowledge (def, thm, proof?)
  \item implement a hierarchy of specifications
  \item implement the programs built upon Pt.1,2 and \\
    {\footnotesize the CA algorithms developed in the other part of the project.}
  \end{enumerate}
\end{itemize}
}%small
\end{frame}

\section[Organisation]{Organisational Considerations}
\subsection[Proposal Arguments]{Argumentation in Proposal}
\begin{frame} \frametitle{Argumentation in Proposal}
{\small
\begin{enumerate}
\item Aims in relation to the state-of-the-art:
  \begin{itemize}
  \item integrate TP with CA for mutal advancement \dots\\
    {\footnotesize TP advances in computational power, CA in trustability}
  \item narrow the gap between TP and engineering practice\\
    {\footnotesize by an easy-to-use TP-based programming language}
  \item make programs trustable for multi-core machines\\
    {\footnotesize by automated code generation}
  \end{itemize}
\item How the project breaks new ground scientifically:
  \begin{itemize}
  \item it decisively extends Isabelle's computational power
  \item it certifies CA by automatically generating code
  \item it certifies parallel programs by code generation
  \end{itemize
}
%\item Importance of the expected results for the discipline:
\item Importance of the TP-based language for the discipline:
  \begin{itemize}
  \item deeper insight into ``deduction --- computation''
  \item a novel ``missing link'' between TP and engineering
  \item prototype for strengthening ``Formal Methods''
  \end{itemize}
\end{enumerate}
}%small
\end{frame}

\subsection[Time + Personnel]{Time Line and Personnel}
\begin{frame} \frametitle{Time Line and Personnel}
\begin{itemize}
\item Time Line: 3 years (beginning as soon as possible)
\item Personnel:
  \begin{itemize
}
  \item PhD for Computer Algebra (CA)
  \item PhD for TP-based programming language
  \item PostDoc for ensuring integration with Isabelle,\\ %?into? Isabelle
           for supporting case study in formal domain engineering  
  \item 3-5 Master projects in case study
  \end{itemize}
\item Staff:
  \begin{itemize}
  \item Wolfgang Schreiner: project leader
  \item Franz Winkler: supervisor of PhD on CA
  \item Walther Neuper: case study at TU Graz
  \end{itemize
}
%\item Funding Agency: FWF --- Fonds Wissenschaftlicher Forschung, Austria
\end{itemize}
\end{frame}

\subsection[Cooperation]{Cooperation Munich --- Linz}
\begin{frame} \frametitle{Cooperation Munich --- Linz
}
%TU Munich, Chair for Logic and Verification
%JKU Linz, Research Institute for Symbolic Computation
\begin{itemize}
\item PostDoc requires expertise
  \begin{itemize}
  \item in internals of Isabelle's function package
  \item in internals of Isabelle's code generator
  \item and  familiarity with Isabelle/Isar for CA integration
  \item and familiarity with the Isabelle development process
  \end{itemize}
\item How introduce Isabelle to PhDs and Master Students \\
  in the project ?
  \begin{itemize}
  \item Course(s) in Linz / in Munich ?
  \item \dots ?
  \end{itemize}
\item Possibilities for Funding Munich --- Linz ?
  \begin{itemize}
  \item FWF project with PostDoc employed in Linz
  \item \dots ?
  \item \dots ?
  \item International project ?
  \end{itemize}
\end{itemize}
\end{frame}

\begin{frame}\frametitle{}
\begin{center
}
%Let's head towards fruitful cooperation~!
We hope for fruitful cooperation Munich --- Linz~!
\end{center}
\end{frame}

\end{document
}