Thursday, May 28, 2015

On the fine-structure of regular algebra by Foster and Struth (review)

This review of On the fine-structure of regular algebra by Simon Foster and Georg Struth (Journal of Automated Reasoning 54 (2): 165-197, 2015) was first published in Computing Reviews.

Although it is dangerous to generalize from a single example, it’s instructive to look at Foster and Struth’s paper as giving us a snapshot of the state of the art in automating ordinary reasoning. First, let’s look at the particular subject of the paper.

Regular expressions and finite automata are fundamental to the practice of computer science, but they are a fertile topic for research, too. A key question is identity: when do two regular expressions (or two finite automata) behave identically? The answer is “when they describe the same set of strings,” but that’s less useful computationally than it first looks, since it requires that we test sets, which potentially are infinite, for equality. So, how else to judge identity? By setting out a collection of laws, or axioms, that encapsulate identity. Foster and Struth’s paper sets out the various attempts by a number of authors, including Boffa, Conway, Kozen, and Salomaa, to provide axioms that are sound (don’t prove any false negatives) and complete (can prove all identities).

The “fine structure” of the title is a detailed study of the interrelationships of these sets of axioms: showing when one set implies another (a process of deduction) and when one set is strictly stronger than another, which is shown by giving a counterexample that meets one set and not the other. The process of both deduction and finding counterexamples is computer assisted, and this provides the main contribution of the paper.

How does the automation directly contribute to the mathematics? It means that a number of loose ends could be tidied up: one set of axiomatizations was simplified, some missing axioms were found in the statement of a particular axiom set, and a gap was found in an existing, well-known proof. So it increased assurance in the work, but probably does not constitute a substantial advance in itself.

On the other hand, the work is indicative of real progress in the facilities available to support online proof and counterexample development. Advances have come in a number of ways. Most important is the way in which different approaches have come together: it used to be that the proof was either done manually, with a proof assistant, or in an entirely automated way, using some kind of decision procedure. The work under review uses the Isabelle proof assistant [1], which now supports the Sledgehammer tool [2], to apply a number of external automated theorem provers for first-order logic; in cases where this fails, Isabelle has its own simplification and proving systems. This has the effect of allowing users to concentrate their attention on shaping the higher-level architecture of the theories, rather than having to deduce the results proof step by (painful) proof step. Where this reaches its limit is when proofs go beyond the purely algebraic and contemplate rather more mathematical structure (for example, sets) as provided by a higher-order logic.

Although most mathematicians don’t use theorem-proving technology in their day-to-day practice, as opposed to the wide take-up of computer algebra systems in various areas of mathematics and engineering, it has taken real hold in the area of mechanized metatheory of programming languages, as witnessed by the POPLmark challenge (http://www.seas.upenn.edu/~plclub/poplmark/). It may well be because this is an area where the scale of proofs can be such that the usual social process of proof checking has been shown to be less than ideal, that value that accrues from formalization. In conclusion, it is interesting to speculate on how long it will take for the practicing mathematician to reach for a theorem-proving system as a part of his or her daily work.

[1] Isabelle home page. https://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html (05/13/2015).
[2] Blanchette, J. C.; B√∂hme, S.; Paulson, L. C. Extending Sledgehammer with SMT solvers. In Proc. of the 23rd Int. Conf. on Automated Deduction: CADE-23. Springer, 

Wednesday, May 13, 2015

Erlang MOOC pilot, day 3

We’re at day 3 of our MOOC pilot on functional programming in Erlang: so how are things going?

MOOCs aren’t synchronous, and so people can begin and progress in their own time. So far half of those who signed up in advance have started to use the MOOC, and half of them have progressed a good way through the first week’s material. We have people taking an active part from (in no particular order) the Netherlands, Spain, Russia, the USA, Mexico, Denmark, Italy, France, Argentina, Chile, Japan, the Czech republic, New Zealand, China, Canada, the UK amongst others.

We’re also finding our way in working out the best ways of interacting. Our forums are split “by activity” and while this keeps each one on topic, it leaves no space for general discussions, so we’ve added a “common room” for those discussions. We also wanted to share with everyone some of the responses to points being made in the feedback form, so we have added a (growing) FAQ page to hold those questions and answers. Luckily we’re able to sort quite a few things out, but some others – like making videos downloadable – are going to take more time, and internal university discussions, to resolve.

We’re also beginning to see discussion and feedback on programming homework assignments. Part of the MOOC ethos is to involve everyone in giving feedback about others’ work and problems, so we have a fully meshed network rather than spoke to hub with the Kent staff providing feedback and so on. It’s still early days, but discussions are beginning. We also had a request for acceptance tests for the homeworks, but again for the purposes of the trial we’re encouraging participants themselves to develop and share these too. We might come back to this as the pilot progresses …

So far Moodle seems to be coping … there would be clear advantages to going with a fully-featured MOOC platform, such as providing transcripts of the videos for accessibility reasons, but Moodle seems to be managing so far. We’re also able to see how people are progressing in quite some detail, so there will be number crunching going on over the course of the pilot, and hopefully some useful data analysis as an outcome.

Monday, coincidentally, we were part of a tea party to celebrate the Beacon Projects at Kent, and as part of that we got a lot of encouragement and interest in what we’re doing. It can only help with developing a case to argue to the university about the multi-faceted value of MOOCs, online lectures and blended learning to our staff, students and public reach.

Monday, May 11, 2015

“Functional Programming in Erlang” MOOC pilot

It’s all very peculiar.

We’ve been working flat out to get the pilot MOOC on Functional Programming in Erlang up and running at Kent, we have signed up over 500 participants, and it just went live 20 minutes ago. Rather like sending a book manuscript off to the publishers, it has all gone quiet, and we're waiting to see what's going to happen. I should tell you who the “we” are: apart from me, there’s Mark O'Connor, who is Distance Learning Technologist for the university, and Stephen Adams, who is TA for the course and who is a PhD student in computer science here.

This pilot is part of a bigger plan, which includes supporting our face-to-face teaching of Erlang at Kent, as well as putting out a set of Master Classes in Erlang by Joe Armstrong, one of the inventors of Erlang, Francesco Cesarini, founder of Erlang Solutions Ltd, and me. These will be coming shortly. This K-MOOCs project is being supported by the University of Kent as part of its Beacon Projects initiative, which is in celebration of the University’s fiftieth anniversary.

We recorded the master classes in a studio with green screen etc, to try that out, and these are in the final stages of production, but the majority of the MOOC lectures are more “home made” and were recorded on my MacBook Pro, using the built in audio and video facilities, and Kent’s lecture recording facilities that are powered by Panopto . Given that “available tech” approach, we’ve been pleased with the results (but our participants may choose to differ!).

In getting the MOOC planned and executed, Mark has been tireless in providing infrastructure, in getting me to plan, in editing and in feeding back on all the activities. We’ve also really benefitted from advice and help from Mike McCracken of Georgia Tech, who has pioneered their online CS courses and MOOCs. Without Mike’s advice about how to script the course in advance, implementation would have been so much more difficult.

As it is, we’ve got the course in place. I’ll be adding a few finishing touches – more quizzes! – today, but really we’re waiting to see how people get on with what’s there. I’ll aim to blog some more as the pilot runs, and we see how it all works out.