Today, a small
package was waiting for me at my door step, containing 52 printed and
stapled copies of a paper that I wrote a while ago. To be more precise, two years ago, when I submitted the main results of my math Diploma Thesis to the Israel Journal of Mathematics. Next year at christmas eve, it was accepted and published online. And now, it seems, it finally went into print. So my paper now has page numbers and I have this pile of printouts that outnumbers the set of possibly interested readers by four dozens or more, and they would probably just download the online version instead of asking for this print out. This seems all very anachronistic to me.
Nice christmas present: I just got message that the paper “Loop subgroups of Fr and the image of their stabilizer subgroups in GLr(ℤ)” that I extracted from my Diploma thesis in Mathematics, and which I submitted to the Israel Journal of Mathematics in November 2010 was finally published today, in “Online First“ form and under the doi 10.1007/s11856-011-0213-3.
I’m currently running the problem class for the graph theory course at the Karlsruhe Institute of Technology, held by Prof. Maria Axenovich. On one problem sheet, I felt like setting the question in verse, and indeed, two students submitted their solution is in verse form as well. I have assembled the problem and both solution – enjoy!
Der Würfelspiel-Programmier-Wettbewerb des Linux-Magazins ist schon bald ein Jahr her. Inzwischen ist ein Artikel (für hier auf A4 neu formatiert) von mir im Eulenspiegel, dem Magazin der Mathe- und Informatikfachschaft des KIT, erschienen, in dem ich Rebeccas und meine mathematische Herangehensweise and das Problem erläutere und unsere Implementierung vorstelle.
Unser Code ist in gewissen Sinne am stärksten, da keine Strategie gegen unsere eine Gewinnwahrscheinlichkeit >50% hat. Dass wir trotzdem nicht den Wettbewerb gewinnen war absehbar, da die Anzahl der gesamten Spiele entscheidend ist, man also um zu Gewinnen gegen die vielen nicht-optimalen Bots möglichst viele Siege herausholen muss – genaueres dazu im Text.
A newly founded Logic Group in Mumbai, which seems to be a private thing but some professors from the IIT Bombay are taking part, has approached me and asked if I can give a talk about Church’s lambda calculus and how he used it to show that Hilbert’s Entscheidungsproblem is not solvable. They are starting a series of talk on logic on the occasion of Turing’s 100th birth year and because I am finally leaving the IIT campus in two days, my talk turned out to be the opening talk for the series. Roughly guessed about fifty people attended, some professors but most of them students from fields other than mathematics and computer science – I hope that they were not too confused by distinguishing truth and provability, expressability and computability, of which I did not give a proper explanation.
I started with a historical exposition of the state of logic in the beginning 20th century, then gave an introduction to lambda calculus, encoding of natural numbers in then, Gödel encoding. Finally I sketched the proof of the unsolvability of the question whether a lambda term has a normal form and then concluded by showing how this implies that the Entscheidungsproblem is not solvable.
I have before hand written out the talk in full, and again I ended up saying completely different things – or at least said things completely different. Nevertheless, I am sharing the (planned) text of my talk, including the timeline that I draw on the whiteboard.
As the project for the course “System specification and implementation”, which introduced the Event-B formalism to us, I modeled the algorithm given in one of the constructive proofs of Vizing’s theorem and showed it to be correct, using the Event-B tool Rodin. Vizing’s theorem states
For a finite undirected graph without autoloops and without multiple edges, at any vertex of which no more than N edges meet, N+1 colors suffice for an edge coloring such that edges incident on the same vertex are of different color.
You can find more details about my approach and my conclusions about Event-B and Rodin in the project report and you can download my Rodin model.
I was asked in the comments about my conclusions, so I’ll reply here. The proof looks unweidly, but I do think that refinement based proofs, where possible, increase clarity, as more, but smaller steps have to be looked at. Also note that I had no prior exposure to Rodin, so some thing could have been done quicker and easier with more experience. But Rodin itself is not the theorem proving tool of my choice. More detail in the report, shortly put: Its math is too weak and not expressive enough, individual proofs are WORN (write-once-read-never) and can easily be lost when changing the models and there is too little emphasis on correctness, e.g. no trusted core base approach known from dedicated theorem provers. So I would use a different tool for proving mathematical statements, nevertheless the idea of refinements, and trying to find those small-steps-refinements, can also help coming up with better proofs in those tools.
My third submission to the Archive of Formal Proof has been published yesterday: A proof that there exists exactly one general triangle. Given that yesterday was the first of April, this is obviously not meant too be taken too serious; nevertheless it is not a prank either: The math is sound and now even formally verified using Isabelle.
For a course at the IIT Bombay on functional programing, I was preparing a presentation on Alonzo Church’s theorem, based on his original 1936 paper “An Unsolvable Problem of Elementary Number Theory” where he first showed that the Entscheidungsproblem is not solvable. In that paper, he states a theorem (Theorem II) “If a formula has a normal form […] any sequence of reductions of the formula must (if continued) terminate in the normal form”. This seems to be wrong. Consider the lambda expression KIΩ, where K=(λxy.x), I=(λx.x) and Ω=(λx.xx)(λx.xx). This has a normal form I. But because Ω reduces to Ω, there is a non-terminating sequence KIΩ → KIΩ → ⋯, in contradiction to Church’s claim. The same example contradicts his Theorem III: “If a formula has a normal form, every well-formed part of it has a normal form.”, which is used in the very proof of his main result, Theorem XVIII.
There is no proof for Theorem II in this paper. He cites it from the then forthcoming paper “Some properties of Conversion” by him and J. B. Rosser. There, proofs are given (see Theorem 2 and its Corollary) but they are quite impenetrable to me. So I was searching for some correction paper, or any other discussion of this issue, but could not find any. Does any reader of this blog know more? What happened in that times when a paper had an error in some proof? What would happen now? Or is this not an error after all, but just a subtle difference between the definitions of λ-calculus as we know and as they introduced it?
Unrelated to this question: The professor asked me to write down a summary of (my interpretation of) the importance and impact of Church’s paper with regard to Gödel and Hilbert’s program, and how that relates to Böhm’s theorem. In the spirit of sharing, I have uploaded my thoughts on Church and Böhm, comments are welcome.
Update: Christian von Essen solved the riddle in a comment to this post: Church only considers lambda abstractions as well-formed when the bound variable actually occurs (freely) in the abstracted term. This does not allow for the K combinator and thus there is no problem.
Since a few months, I have been playing around with Isabelle, a theorem prover system. I find it very intriguing to have proofs of mathematical statements checked by something as pendantic and comprehensive as a machine. Mathematicians always claim that their statements are true in all eternity, but the proofs are just checked by error-prone human beings. Especially with complex, large proofs that are only read by a handful of people, I doubt that these are always fully correct. Note that this does not imply that I doubt that the results are correct. They probably are. But a bit of doubt remains. A computer-checked proof, in contrast, can not accidentially omit corner cases, leave out seemingly “trivial” assumtions of used theorems or be misled by slightly differing definition from different sources.
I was hoping to check at least parts of my diploma thesis using Isabelle, but it turns out that the standard algebra library shipped with Isabelle is not complete enough. Even free groups were missing. This was motivation enough to try to formalize them and prove the universal property and some isomorphisms (The free group over the empty set is the unit group, the free group over one generator is the additive group of integers and free groups over sets of same cardinality are isomophic). I submitted the resulting theory to the Archive of Formal Proofs and it was accepted. You can view the complete document or the document without proofs.
I did not formalize the fact that isomorphic free groups have bases of same cardinality. As far as I know there is no simple argument that works directly with free groups. The proofs I have seen pass to the abelianization of the free group, i.e. the free module over ℤ and apply the well known proof from the analogous statement about vector spaces. But if someone knows an elementary proof of this fact, I’d like to hear about it.
While writing my diploma thesis, I often wished I had a blackboard in my room: A place to quickly scribble some ideas on, somewhere where I can easily erease and replace stuff. Also, somewhere where you can literally (and not just figuratively) step back from and look at from the distance.
For my 25th birthday, my parents organized a discharged part of a blackboard from my old scool, and yesterday, we installed it in my room in Karlsruhe:
Although my diploma thesis is finished, I’m sure it will be a nice and useful piece of furniture, and if only to draw funny things on (as my girlfriend did on this picture).
Earlier today, I went to a local copy shop and had my diploma thesis printed. This afternoon, I will hand it in. The title is “Loop subgroups of Fr and the images of their stabilizer subgroups in GLr(ℤ)” and discusses a group-theoretical result. I assume that very few readers care about the content of the thesis, but maybe some are interested in a few assorted LaTeX hints. I’m also publishing the full TeX source code, maybe someone can make use of it.
I’m using the varioref package, in conjunction with the cleveref package. This provides a command \vref{fig:S3S4l} which will expand to, for example, to “Figure 1 on page 11”. But if the referenced figure is actually on the current page, the next page, the previous page or the facing page (in two-side layouts), it will say so: “Figure 1 on this page.”
This is very nice, but I assume that the reader of my thesis is able to find Figure 1 when it is visible, i.e. on the current or facing page. One can remove the referencing texts with the commands \def\reftextfaceafter{}, \def\reftextfacebefore{} and \def\reftextcurrent{}. But because varioref puts a space between “Figure 1” and this text, we will get a superfluous space – even before punctuation.
The remedy is the command \unskip, which removes this space again. So I use in my preamble:
Bilder
\def\reftextfaceafter {\unskip}%
\def\reftextfacebefore{\unskip}%
\def\reftextcurrent {\unskip}%
I chose the Palatino font for my thesis, using the mathpazo package. Various sources (such as the KOMA-Script manual) suggest to use 5% extra leading:
\linespread{1.05}
I don’t have too many figures and tables in my thesis, and I want them to be numbered simple 1, 2, ... By default, LaTeX would say 1.1, 1.2, 2.1, ... This can be fixed using the remreset package and these commands:
\makeatletter
\@removefromreset{figure}{chapter}
\renewcommand{\thefigure}{\arabic{figure}}
\@removefromreset{table}{chapter}
\renewcommand{\thetable}{\arabic{table}}
\makeatother
LaTeX already avoids these, but I wanted to get rid of them completely. This can be done with:
% Disable single lines at the start of a paragraph (Schusterjungen) \clubpenalty = 10000 % Disable single lines at the end of a paragraph (Hurenkinder) \widowpenalty = 10000 \displaywidowpenalty = 1000
I had to typeset tables with some lines struck, and I could not find a ready command for that. I used the following definition, based on the code for \hline. Note that it probably does not adjust well to other font sizes and needs to be adjusted manually:
\makeatletter
\def\stline{%
\noalign{\vskip-.7em\vskip-\arrayrulewidth\hrule \@height \arrayrulewidth\vskip.7em}}
\makeatother
According to the KOMA manual, the title page as set by LaTeX is not meant to be the cover of a publication, and therefore has to be set with the margins of a right page – i.e. a larger right margin and a smaller left margin. But when printing cheaply, one often just put a transparent sheet on top of the print, so the title page is the cover. You can convince KOMA that you are right by using
\KOMAoptions{twoside=false}
\begin{titlepage}
...
\end{titlepage}
\KOMAoptions{twoside=true}
LaTeX would put the list of algorithms on a new right page. I found this a waste of paper for my few algorithms, and preferred to put the list right after the table of contents. You can override the LaTeX behavior using:
\tableofcontents
{
\let\cleardoublepage\relax % book
\let\clearpage\relax % report
\let\chapter\section
\listofalgorithms
}
This code also reduces the size of the heading to that of a section. The same trick also works with \chapter.
LaTeX with the hyperref package creates nice PDF bookmarks from your chapter and section titles. Unfortunately, PDF bookmark names can only be plain strings, while the titles in the document might contain some math symbols. You can make both happy with \texorpdfstring:
\section{Stabilizer subgroups in \texorpdfstring{$\GL_r(\Z/2\Z)$}{GL\_r(Z/2Z)}}
The diploma thesis contains a small note which I have to sign, saying that I created it on my own etc. Below that, I put two labeled lines for date and signature, using the tabbing environment:
\begin{tabbing}
\rule{4cm}{.4pt}\hspace{1cm} \= \rule{7cm}{.4pt} \\
Ort, Datum \> Unterschrift
\end{tabbing}
For a recent university seminar, I wrote a haskell program to render and edit iterated function systems (IFS), which generates a certain class of fractals, namely self-similar sets. I think the result is quite nice, so I’m sharing the code.
With FrakView you can view a rendering of the attractor of the IFS, with a choice of two algorithms (a straight forward, and a probabilistic), configurable depth and anti-aliasing. You can also modify the IFS by dragging the colored boxes with arrows you see on the screenshot. For the academically inclined, there is also support to visualize cylinder sets and otherwise explore the coding space of the IFS a bit.
The program is written in haskell and uses gtk2hs, the gtk bindings for haskell. It might be interesting for other gtk2hs programmers to see how FrakView solves some issues: For example, it uses the CoroutineT monad transformer I recently blogged about – check out the pausingForM_ function in GUI.hs. Also, the current state of the screen is in one algebraic data type (ScreenConfig) that supports equality checks, so when the user interacts, the code recomputes the new ScreenConfig (using getRenderer), but only redraws the screen if it differs from the previous. This is much easier and more robust than having to decide for each possible user interaction whether it changes what’s on the screen.
You can get the source from the FrakView darcs repository.