Joachim Breitner


The Incredible Proof Machine

Published 2015-09-24 in sections English, Haskell, Mathe.

In a few weeks, I will have the opportunity to offer a weekend workshop to selected and motivated high school students1 to a topic of my choice. My idea is to tell them something about logic, proofs, and the joy of searching and finding proofs, and the gratification of irrevocable truths.

While proving things on paper is already quite nice, it is much more fun to use an interactive theorem prover, such as Isabelle, Coq or Agda: You get immediate feedback, you can experiment and play around if you are stuck, and you get lots of small successes. Someone2 once called interactive theorem proving “the worlds most geekiest videogame”.

Unfortunately, I don’t think one can get high school students without any prior knowledge in logic, or programming, or fancy mathematical symbols, to do something meaningful with a system like Isabelle, so I need something that is (much) easier to use. I always had this idea in the back of my head that proving is not so much about writing text (as in “normally written” proofs) or programs (as in Agda) or labeled statements (as in Hilbert-style proofs), but rather something involving facts that I have proven so far floating around freely, and way to combine these facts to new facts, without the need to name them, or put them in a particular order or sequence. In a way, I’m looking for labVIEW wrestled through the Curry-Horward-isomorphism. Something like this:

A proof of implication currying

A proof of implication currying

So I set out, rounded up a few contributors (Thanks!), implemented this, and now I proudly present: The Incredible Proof Machine3

This interactive theorem prover allows you to do perform proofs purely by dragging blocks (representing proof steps) onto the paper and connecting them properly. There is no need to learn syntax, and hence no frustration about getting that wrong. Furthermore, it comes with a number of example tasks to experiment with, so you can simply see it as a challenging computer came and work through them one by one, learning something about the logical connectives and how they work as you go.

For the actual workshop, my plan is to let the students first try to solve the tasks of one session on their own, let them draw their own conclusions and come up with an idea of what they just did, and then deliver an explanation of the logical meaning of what they did.

The implementation is heavily influenced by Isabelle: The software does not know anything about, say, conjunction (∧) and implication (→). To the core, everything is but an untyped lambda expression, and when two blocks are connected, it does unification4 of the proposition present on either side. This general framework is then instantiated by specifying the basic rules (or axioms) in a descriptive manner. It is quite feasible to implement other logics or formal systems on top of this as well.

Another influence of Isabelle is the non-linear editing: You neither have to create the proof in a particular order nor have to manually manage a “proof focus”. Instead, you can edit any bit of the proof at any time, and the system checks all of it continuously.

As always, I am keen on feedback. Also, if you want to use this for your own teaching or experimenting needs, let me know. We have a mailing list for the project, the code is on GitHub, where you can also file bug reports and feature requests. Contributions are welcome! All aspects of the logic are implemented in Haskell and compiled to JavaScript using GHCJS, the UI is plain hand-written and messy JavaScript code, using JointJS to handle the graph interaction.

Obviously, there is still plenty that can be done to improve the machine. In particular, the ability to create your own proof blocks, such as proof by contradiction, prove them to be valid and then use them in further proofs, is currently being worked on. And while the page will store your current progress, including all proofs you create, in your browser, it needs better ways to save, load and share tasks, blocks and proofs. Also, we’d like to add some gamification, i.e. achievements (“First proof by contradiction”, “50 theorems proven”), statistics, maybe a “share theorem on twitter” button. As the UI becomes more complicated, I’d like to investigating moving more of it into Haskell world and use Functional Reactive Programming, i.e. Ryan Trickle’s reflex, to stay sane.

Customers who liked The Incredible Proof Machine might also like these artifacts, that I found while looking whether something like this exists:

  • Easyprove, an interactive tool to create textual proofs by clicking on rules.
  • Domino On Acid represents natural deduction rules in propositional logic with → and ⊥ as a game of dominoes.
  • Proofscape visualizes the dependencies between proofs as graphs, i.e. it operates on a higher level than The Incredible Proof Machine.
  • Proofmood is a nice interactive interface to conduct proofs in Fitch-style.
  • Proof-Game represents proofs trees in a sequent calculus with boxes with different shapes that have to match.
  • JAPE is an editor for proofs in a number of traditional proof styles. (Thanks to Alfio Martini for the pointer.)
  • Logitext, written by Edward Z. Yang, is an online tool to create proof trees in sequent style, with a slick interface, and is even backed by Coq! (Thanks to Lev Lamberov for the pointer.)
  • Carnap is similar in implementation to The Incredible Proof Machine (logical core in Haskell, generic unification-based solver). It currently lets you edit proof trees, but there are plans to create something more visual.
  • Clickable Proofs is a (non-free) iOS app that incorporates quite a few of the ideas that are behind The Incredible Proof Machine. It came out of a Bachelor’s thesis of Tim Selier and covers propositional logic.
  • Euclid the game by Kasper Peulen is a nice game to play with geometric constructions.

  1. Students with migration background supported by the START scholarship

  2. Does anyone know the reference?

  3. We almost named it “Proofcraft”, which would be a name our current Minecraft-wild youth would appreciate, but it is alreay taken by Gerwin Kleins blog. Also, the irony of a theorem prover being in-credible is worth something.

  4. Luckily, two decades ago, Tobias Nipkow published a nice implementation of higher order pattern unification as ML code, which I transliterated to Haskell for this project.

Quickest path to a local apt repository

Published 2015-08-22 in sections English, Debian.

As I’m writing this, DebConf 15 is coming to an end. I spend most of my time improving the situation of the Haskell Packages in Debian, by improving the tooling and upgrading our packages to match Stackage 3.0 and build against GHC 7.10. But that is mostly of special interest (see this mail for a partial summary), so I’d like to use this post to advertise a very small and simple package I just uploaded to Debian:

During one of the discussion here I noticed that it is rather tricky to make a locally built package available to apt-get. The latest version in unstable allows one to install a debian package simply by running apt-get install on it, but in some cases, e.g. when you want a convenient way to list all packages that you made available for local use, this is insufficient.

So the usual approach is to create a local apt repository with your packages. Which is non-trivial: You can use dpkg-scanpackage, apt-ftparchive or reprepro. You need to create the directories, run the commands, add the repository to your local sources. You need to worry about signing it or setting the right options to make apt-get accept it without signing.

It is precisely this work that my new package local-apt-repository automates for you: Once it is installed, you simply drop the .deb file into /srv/local-apt-repository/ and after the next apt-get update the package can be installed like any other package from the archive.

I chose to use the advanced features that systemd provides – namely activation upon path changes – so works best with systemd as the init system.

If you want to contribute, or test it before it passes the NEW queue, check out the git repository.

Running circle-packing in the Browser, now using GHCJS

Published 2015-06-20 in sections English, Haskell.

Quite a while ago, I wrote a small Haskell library called circle-packing to pack circles in a tight arrangement. Back then, I used the Haskell to JavaScript compiler fay to create a pretty online demo of that library, and shortly after, I create the identical demo using haste (another Haskell to JavaScript compiler).

The main competitor of these two compilers, and the most promising one, is GHCJS. Back then, it was too annoying to install. But after two years, things have changed, and it only takes a few simple commands to get GHCJS running, so I finally created the circle packing demo in a GHCJS variant.

Quick summary: Cabal integration is very good (like haste, but unline fay), interfacing JavaScript is nice and easy (like fay, but unlike haste), and a quick check seems to indicate that it is faster than either of these two. I should note that I did not update the other two demos, so they represent the state of fay and haste back then, respectively.

With GHCJS now available at my fingertips, maybe I will produce some more Haskell to be run in your browser. For example, I could port FrakView, a GUI program to render, expore and explain iterated function systems, from GTK to HTML.

Tiptoi auf der GPN 15

Published 2015-06-06 in sections Deutsch, Tiptoi.

Soeben findet in Karlsuhe die Gulaschprogrammiernacht statt, eine ein Chaos-Event mit Vorträgen, Workshops, allerlei Technikspielereien und, wie der Name sagt, auch Gulasch. Ich hab hier einen Vortrag zu (mal wieder) meinen Tiptoi-Basteleien gehalten. Entgegen meiner anfänglichen Sorgen war der Vortragssaal mit geschätzt 40 Leuten ganz ansehnlich gefüllt. In Anschluss habe ich noch einen Workshop angeboten, soll heißen, wer wollte macht seinen ersten Schritte mit dem tttool und ich helf über die ersten Hürden. Besonders gefreut hab ich mich über ein junges Mädchen, das ausführlich ihre Vorstellung von Rezepten mit Tiptoi-Unterstützung erläuterte.

Ansonsten hab ich von der GPN noch nicht viel mitbekommen, da ich gerade erst angekommen bin...

ZuriHac 2015

Published 2015-06-01 in sections English, Haskell.

Last weekend, I attended ZuriHac 2015, which was, as always, a pleasant event. I did not actually do a lot, besides some maintenance of Debian Haskell packages, but had some nice chats. It is always very motivating to hear that people read my blog, or that they found my talk (such as the Haskell Bytes talk at Galois) helpful.

My plan was to work on gipeda and I did not do much until an hour before I had to leave, when Lennard Kolmodin came around and I showed him the software. He liked it so far, so we quickly set up an instance of gipeda for the “binary” library. It is not finished yet, as more benchmarks need to be extracted from the build log. That was motivating, and I got further ideas to implement during the train ride back. If only that had happened earlier during the weekend...

Fifth place in Godingame World Cup

Published 2015-04-26 in sections English, Haskell.

Last evening, Codingame held a “Programming World Cup” titled “There is no Spoon”. The format is that within four hours, you get to write a program that solves a given task. Submissions are first rated by completeness (there are 13 test inputs that you can check your code again, and further hidden tests that will only be checked after submission) and then by time of submission. You can only submit your code once.

What I like about Codingame is that they support a great number of programming languages in their Web-“IDE”, including Haskell. I had nothing better to do yesterday, so I joined. I was aiming for a good position in the Haskell-specific ranking.

After nearly two hours my code completed all the visible test cases and I submitted. I figured that this was a reasonable time to do so, as it was half-time and there are supposed to be two challenges. I turned out that the first, quite small task, which felt like a warm-up or qualification puzzle, was the first of those two, and that therefore I was done, and indeed the 5th fastest to complete a 100% solution! With only less than 5 minutes difference to the 3rd, money-winning place – if I had known I had such a chance, I had started on time...

Having submitted the highest ranked Haskell code, I will get a T-Shirt. I also defended Haskell’s reputation as an efficient programming language, ranked third in the contest, after C++ (rank 1) and Java (rank 2), but before PHP (9), C# (10) and Python (11), listing only those that had a 100% solution.

The task, solving a Bridges puzzle, did not feel like a great fit for Haskell at first. I was juggling Data.Maps around where otherwise I’d simple attach attributes to object, and a recursive function simulated nothing but a plain loop. But it played off the moment I had to implement guessing parts of the solution, trying what happens and backtracking when it did not work: With all state in parameters and pure code it was very simple to get a complete solution.

My code is of course not very polished, and having the main loop live in the IO monad just to be able to print diagnostic commands is a bit ugly.

The next, Lord of the Ring-themed world cup will be on June 27th. Maybe we will see more than 18 Haskell entries then?

Talk and Article on Monads for Reverse Engineering

Published 2015-04-15 in sections English, Haskell.

In a recent project of mine, a tool to analyze and create files for the Ravensburger Tiptoi pen, I used two interesting Monads with good results:

  • A parser monad that, while parsing, remembers what part of the file were used for what and provides, for example, an annotated hex dump.
  • A binary writer monad that allows you to reference and write out offsets to positions in the file that are only determined “later” in the monad, using MonadFix.

As that’s quite neat, I write a blog post for the German blog about it, and also held a talk at the Karlsruhe functional programmers group. If you know some German, enjoy; if not, wait until I have a reason to hold the talk in English. (As a matter of fact, I did hold the talk in English, but only spontaneously, so the text is in German only so far.)

An academic birthday present

Published 2015-03-28 in sections English, Haskell.

Yesterday, which happened to be my 30th birthday, a small package got delivered to my office: The printed proceedings of last year's “Trends in Functional Programming” conference, where I published a paper on Call Arity (preprint). Although I doubt the usefulness of printed proceedings, it was a nicely timed birthday present.

Looking at the rather short table of contents – only 8 papers, after 27 presented and 22 submitted – I thought that this might mean that, with some luck, I might have chances to get the “Best student paper award”, which I presumed to be announced at the next iteration of the conference.

For no particular reason I was leisurely browsing through the book, and started to read the preface. And what do I read there?

Among the papers selected for these proceedings, two papers stood out. The award for Best Student Paper went to Joachim Breitner for his paper entitled Call Arity, and the award for Best Paper Overall went to Edwin Brady for his paper entitled Resource-dependent Algebraic Effects. Congratulations!

Now, that is a real nice birthday present! Not sure if I even would have found out about it, had I not have thrown a quick glance at page V...

I hope that it is a good omen for my related ICFP'15 submission.

Tiptoi-Artikel in der c't

Published 2015-03-21 in sections Deutsch, Tiptoi.

Gestern erschien Ausgabe 08/15 der c't, und darin ein Artikel von Carsten Podszun und mir: „Stiftzauber – Eigene Bücher und Spiele für den Tiptoi vertonen“. Dies ist meine erste Veröffentlichung in einem derart populärem Magazin (Auflage etwa 270.000)! Ich bin gespannt ob das Tiptoi-Bastel-Projekt: jetzt einen neuen Aktivitätsschub bekommt und freue mich auf viele Fragen und Berichte auf der tiptoi-Mailingliste.

Ich habe ja schon ein paar mal in kleineren Magazinen veröffentlicht (3× im Linux-Magazin, Auflage 26.000; 2× in FreeX), und der Prozess war schon recht unterschiedlich. Beim Linux-Magazin bekommt man Autorenrichtlinien, die z.B. auch festlegen, mit welchen Tags man die Formatierung (Überschriften, Inline-Code) festlegt. Ich dann den Artikel geschrieben, es gab vielleicht noch etwas Feedback, und er wurde im großen und ganzen so gedruckt wie eingereicht – Tippfehler wurden eventuell noch behoben.

Der Wichtel, der den Artikel ziert

Der Wichtel, der den Artikel ziert

Bei der c't wurde ich als Autor deutlich intensiver betreut. Ende Oktober reichten wir einen erstes Konzept und Mitte November einen Rohentwurf (als Textdatei) ein – wir hofften noch in eine Ausgabe vor oder zu Weihnachten zu kommen, da um diese Zeit viele neue Tiptoi-Stifte in die Haushalte kommen und Eltern die Zeit zum Basteln haben. Dann war allerdings erst mal Funkstille bis Anfang Januar. Ich schätze dass unser Artikel in der Warteschlange von höher priorisierten Texten überholt wurde...

Mitte Januar bekamen wir dann von der uns betreuenden Redakteurin den Rohentwurf in überarbeiteter Form und als RTF-Datei zurück. Da waren dann auch die Heise-spezifischen Tags für Zwischenüberschriften o.ä. drin. Die Verzögerung hatte allerdings ihr gutes: Das tttool hat sich bis dahin deutlich weiterentwickelt und insgesamt wurde der Prozess deutlich einfacher. Ich bin also nochmal ran und habe den Text entsprechend aktualisiert und am 1. Februar wieder in die Redaktion geschickt, jetzt als RTF-Datei. Nach drei Wochen gab es dann wieder Feedback und die Aussicht auf ein Erscheinen in c't 8. Ich hab das Feedback eingearbeitet und am nächsten Tag zurück geschickt. Nach einer Woche ohne Aktivität hatte ich noch weitere kleine Verbesserungen hinterhergeschickt.

Weitere zwei Wochen ruhe und plötzlich lag uns vorletzten Mittwoch eine PDF-Datei mit einem fertig gelayouteten Artikel vor. In dem Text fehlten aber manche Änderungen aus meinen letzten beiden Mails. Ich verglich die beiden Versionen Satz für Satz um herauszufinden, was fehlt, und stellte fest dass jeder zweite Satz umformuliert oder zumindest leicht umgestellt wurde. Mein Bruder hat sich schon gewundert und gefragt ob der Text wirklich von mir geschrieben wurde...

Wir hatten nun plötzlich eine harte Deadline von 48h für letzte Änderungen – auf einmal muss also alles schnell gehen. Ich meldete daher gleich die übersehenen Passagen aus meinen letzten Mails.

Am Donnerstag kam dann die vorerst letzte Version, in der ich noch ein paar kleine sachliche Ungenauigkeiten1, Tippfehler und sprachliche Unschönheiten bemängelte. Leider kamen diese Änderungen wegen einem Problem mit meinem Mailserver (Debian-Bug 780256 mit 780578) erst Freitag Nachmittag an und konnten nicht mehr berücksichtigt werden – schade! Ich hab die finale Version jetzt noch gar nicht gesehen; vielleicht wurden sie ja im Lektorat noch behoben.

In dieser letzten Version war dann auch der Aufmacher, also das Bild oben auf der ersten Seite zu sehen. Auf die Gestaltung, die auf der Tiptoi-Mailingliste schon verwundert kommentiert wurde, hatten wir als Autoren keinen Einfluss.

Anders als beim Linux-Magazin entsteht so ein c't-Artikel also in einem recht intensiveren Dialog mit einem Redakteur, der zum Beispiel darauf achtet, dass der Artikel zur Zielgruppe passt, dass alles wichtige erklärt wird und der sprachlich nochmal drübergeht. Das ist natürlich sinnvoll und die Voraussetzung für gute Qualität.

Andererseits hat der Prozess auch große Nachteile. Die Gesamtdauer – mehr als 5 Monate vom ersten Kontakt bis zum Erscheinen mit langen Phasen des Stillstandes – ist etwas demotivierend. Zusätzlich ist die Interaktion nicht besonders wohldefiniert: Nachdem ich einen überarbeiteten Entwurf geschickt habe war mir nicht klar, ob und in welcher Form ich weitere Verbesserungen nachreichen kann. Da die Texte als RTF-Dateien rumgeschickt wurden, habe ich daraus geschlossen, dass sie nicht vernünftig versioniert werden, wie etwa Textdateien in einem Git-Repo, und eventuell manuell zusammengeführt werden müssen. Eine Lektorin in einem Buchverlag erzählte mir, dass es dort ein Token-System gibt, und immer klar ist ob der Redakteur oder der Autor jetzt den Text weiter entwickeln darf. Das hätte Missverständnisse vermieden. Noch schöner fände ich allerdings ein von Redaktion und Autor gemeinsam genutztes Etherpad, Git-Repository o.ä., was mir auch ermöglicht hätte, die Änderungen der Redaktion besser nachzuvollziehen. Bei einem technischen Verlag wie Heise sollte das doch vielen Autoren entgegen kommen.

Ich hoffe das war nicht meine letzte Veröffentlichung in einem Magazin wie der c't und weiß jetzt dass ich da das nächste Mal besser darauf achten muss, dass so Missverständnisse vermieden werden können.

An der Stelle nochmal vielen Dank an Rebecca Schwerdt für die Zeichnung, mit der wir den Artikel illustriert haben.

  1. Da steht z.B. „..., wo [der OID-Code] für das menschliche Auge nicht erkennbar ist“. Der Satz wurde von der Redaktion dazugeschrieben, ist aber falsch: Richtig wäre allenfalls „...kaum erkennbar ist.“

Sim Serim geschenkt bekommen

Published 2015-03-17 in sections Deutsch.

Vor gut einem Jahr habe ich das Brettspiel „Sim Serim“ unter dem Namen „Sum Serum“ als Browserspiel implementiert. Da ich das Spiel nicht selber besitze und mir die Regeln nur kurz in der Karlsruher Spielepyramide erklärt wurden, hatte ich etwas übersehen: Die Zahl der Steine pro Spieler ist eigentlich begrenzt, worauf mich kürzlich Ulrich Roth auf BoardGameGeek aufmerksam gemacht hat. Darauf hin habe ich das noch korrigiert und dabei die Grafik des Spiels (ein klein wenig) aufgehübscht.

Dass muss Heinrich Glumpler, der Autor von Sim Serim, mitbekommen haben, denn er hat meine Implementierung nicht nur ausgiebig gelobt, sondern mir tatsächlich einfach ein Exemplar des „echten“ Sim Serims geschenkt! Das freut mich natürlich sehr! (Und ist deutlich angemeher als die Reaktion von Brian Hersch auf meine Java-ME-Version von Tabu damals vor 9 Jahren...)