1.1 --- a/doc-src/isac/chuber/bakk_thesis_prelim.tex Thu Jul 21 15:07:26 2011 +0200
1.2 +++ b/doc-src/isac/chuber/bakk_thesis_prelim.tex Thu Jul 21 16:47:34 2011 +0200
1.3 @@ -1,9 +1,9 @@
1.4 -\documentclass{article}
1.5 +\documentclass[12pt]{article}
1.6 \usepackage{a4}
1.7 \usepackage{times}
1.8 \usepackage{latexsym}
1.9 -%\bibliographystyle{alpha}
1.10 -\bibliographystyle{abbrv}
1.11 +\bibliographystyle{alpha}
1.12 +%\bibliographystyle{abbrv}
1.13 \usepackage{graphicx}
1.14
1.15 \def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}$}
1.16 @@ -12,73 +12,91 @@
1.17 \title{Tentative Title:\\
1.18 Theory of Functional Programming\\
1.19 Introduced by Isabelle and \isac}
1.20 -\author{n.n.\\
1.21 +\author{n.n\\
1.22 {\tt TODO@xxx.at}}
1.23
1.24 \begin{document}
1.25 \maketitle
1.26 -\abstract{
1.27 -TODO
1.28 -}
1.29 +%\abstract{
1.30 +%TODO
1.31 +%}
1.32
1.33 \section{Background}
1.34
1.35 -``Functional programing'' (FP) is one of the leading paradigms in programming besides ``object oriented programming'' \cite{?} and ``logic / constraint programming'' \cite{}. One advantage of FP are general and elegant approaches to the mathematical theory of programming.
1.36 +``Functional programing'' (FP) is one of the leading paradigms in programming besides ``object oriented programming'' %\cite{?}
1.37 +and ``logic (or constraint) programming'' \cite{?}. One advantage of FP are general and elegant approaches to the mathematical theory of programming \cite{?}.
1.38
1.39 -Presently FP gains importance in face of the ``multi-core crisis'' \cite{}: functional programs are ready to exploit many cores in parallel.
1.40 +Presently FP gains importance in face of the ``multi-core crisis'' \cite{?}: functional programs are ready to exploit many cores in parallel. In spite of this fact, at Graz University of Technology (TUG) FP has vanished during recent years, and it is of actual importance to include FP again in education.
1.41
1.42 -In spite of this fact, at Graz University of Technology (TUG) FP has vanished during recent years, and it is of actual importance to include FP again in education.
1.43 -
1.44 -In order to support such education this thesis will employ advanced tools developed in the intersection between computer science and mathematics: The computer theorem prover Isabelle \cite{} and the educational math assistant \sisac.
1.45 +In order to support such education this thesis will compile a course based on advanced tools developed in the intersection between computer science and mathematics: The computer theorem prover Isabelle \cite{Nipkow-Paulson-Wenzel:2002} and the educational math assistant \sisac.
1.46
1.47 \section{Goal}
1.48
1.49 -The goal of this thesis is generation of interactive course material on the topic, implemented in Isabelle and \sisac.
1.50 +The goal of this thesis is generation of interactive course material on FP and respective theory of programming, implemented in Isabelle and \sisac.
1.51
1.52 -In Isabelle the material shall exploit the recently implemented ``function package'' \cite{}. This package is the most advanced in comparison to other provers and supports all what is needed for programming and proving properties of programs.
1.53 +The material shall use most recent developments, for instance the ``function package'' \cite{krauss:funs} recently implemented in Isabelle. This package supports all what is needed for programming and proving properties of programs.
1.54
1.55 -Experience shows, that in early phases of programming (as well as of doing mathematics \cite{?}) proceeding step by step in a program is important for learning. This will be done by implementing selected programs into \sisac.
1.56 +Although addressing most recent developments and theory at the state of the art, the material also shall serve in early phases of programming. Experience shows, that in early phases (in analogy to doing mathematics \cite{?}) proceeding step by step in a program is important for learning. This will be done by implementing selected programs into \sisac.
1.57
1.58 -The interactive course material shall serve in certain courses at TUG and in the recently established ``entry and orientation phase'' (Studien-Eingangs und -Oreintierungs Phase, STEOP).
1.59 +The interactive course material shall serve in certain courses at TUG and in the recently established ``entry and orientation phase'' (Studien-Eingangs und -Orientierungs Phase, STEOP).
1.60
1.61 \section{State of the Art}
1.62 +The thesis cover a wide range of topics some of which will be presented in more detail to be agreed on.
1.63
1.64 +\paragraph{Theory of functional programming ?}
1.65 TODO
1.66
1.67 -%supports different kinds of function definitions (providing more or less automated support by the prover), mutual, nested and higher-order recursion, partiality
1.68 +\paragraph{Proof tools for FP}
1.69 +Isabelle's function package \cite{krauss:funs} is the most advanced in comparison to other provers. It supports two different way of function definitions, one providing full automation (applicable in simple cases) and another featuring interactive proofs of termination.
1.70
1.71 -%Coq \cite{}
1.72 +The function package covers the full range of FP: mutual, nested and higher-order recursion, partiality
1.73 +
1.74 +The other European computer theorem prover, Coq \cite{}, has less powerful support for FP (TODO)
1.75 +
1.76 +\paragraph{Didactics of FP} is concern of very different opinions: At some universities FP is addressed in introductory courses, while at other universities FP is considered an abstract topic addressed in higher semesters. The choice between these extreme alternatives seems to be related to principcal considerations on software construction \cite{aichernig:ingenieur}.
1.77 +
1.78 +The planned course might provide a bridge between the alternatives, addressing novices as well as advanced students by employing computer theorem provers.
1.79 +
1.80 +\paragraph{Educational math assistants,} if based on computer theorem proving, are appropriate to serve introduction to FP in a specific way: If considering evaluation of functional programs as rewriting, there is an obstacle. Empirical data show that students do not learn to apply rules at high-school --- for instance, the cannot apply the law of distributivity in algebra consciously, they do algebra in the same way they they use their mother language.
1.81 +
1.82 +The experimental system \sisac{}\footnote{http://www.ist.tugraz.at/projects/isac/} developed at TU Graz seems appropriate to provide experience in rigorous application of rewrite rules as a prerequisite to understand evaluation in FP.
1.83
1.84
1.85 \section{Thesis Structure}
1.86
1.87 -The main point of this thesis is the interactive course material, and the thesis serves this point in several ways:
1.88 +The main result of this thesis is the interactive course material, accompanied by a thesis.
1.89
1.90 -general survey on FP
1.91 +\paragraph{The interactive course material} will be implemented as Isabelle theories. Isabelle provides a document preparation system for theories which shall lead for a twofold presentation of the course: as (a) pdf-file(s) and as theories supporting interactive learning.
1.92
1.93 -description of the state of the art in proof tools specialized on FP
1.94 +For stepwise exercises in \sisac{} an additional Isabelle theory is required, which contains the specifications and programs for the respective exercises in ML-sections.
1.95
1.96 -didactic consideration about the course (what has been omitted, ...)
1.97 +\paragraph{The thesis} completes the work as required for a bakkalaureate.
1.98
1.99 -future work, probably extending the course to more advanced topics
1.100 -
1.101 -future work, extending the course to more elementary topics, probably usable at high school
1.102 -
1.103 -...
1.104 -
1.105 -...
1.106 +%general survey on FP
1.107 +%
1.108 +%description of the state of the art in proof tools specialized on FP
1.109 +%
1.110 +%didactic consideration about the course (what has been omitted, ...)
1.111 +%
1.112 +%future work, probably extending the course to more advanced topics
1.113 +%
1.114 +%future work, extending the course to more elementary topics, probably usable at high school
1.115 +%
1.116 +%...
1.117 +%
1.118 +%...
1.119
1.120
1.121 \section{Timeline}
1.122
1.123 The main work shall be done during this summer as much as possible.
1.124
1.125 -Milestones
1.126 -\subsection{TODO}
1.127 -study introductory material for Isabelle; contact Alexander Kraus and others for similar course material
1.128 +%Milestones
1.129 +%\subsection{TODO}
1.130 +%study introductory material for Isabelle; contact Alexander Kraus and others for similar course material
1.131 +%
1.132 +%\subsection{TODO}
1.133 +%\sisac =''=
1.134
1.135 -\subsection{TODO}
1.136 -\sisac =''=
1.137 -
1.138 -%\bibliography{bib/TODO}
1.139 +\bibliography{references}
1.140 \end{document}
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/doc-src/isac/chuber/references.bib Thu Jul 21 16:47:34 2011 +0200
2.3 @@ -0,0 +1,28 @@
2.4 +@Article{aichernig:ingenieur,
2.5 + author = {Bernhard K. Aichernig and Peter Lucas},
2.6 + title = {Softwareentwicklung --- eine {I}ngenieursdisziplin!(?)},
2.7 + journal = {Telematik, Zeitschrift des Telematik-Ingenieur-Verbandes (TIV)},
2.8 + year = {1998},
2.9 + volume = {4},
2.10 + number = {2},
2.11 + pages = {2-8},
2.12 + note = {http://www.ist.tu-graz.ac.at/publications},
2.13 + annote = {}
2.14 +}
2.15 +
2.16 +@Book{Nipkow-Paulson-Wenzel:2002,
2.17 + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
2.18 + title = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
2.19 + publisher = {Springer},
2.20 + series = {LNCS},
2.21 + volume = 2283,
2.22 + year = 2002
2.23 +}
2.24 +@PhdThesis{krauss:funs,
2.25 + author = {Alexander Krauss},
2.26 + title = {Automating Recursive Definitions and Termination Proofs in Higher-Order Logic},
2.27 + school = {Technische Universit\"at M\"unchen},
2.28 + year = {2009},
2.29 + OPTnote = {http://www4.in.tum.de/~krauss/diss/}
2.30 +}
2.31 +