The competition is about solving solitaire-like games played on a Turing tape (a one-dimensional tape divided into squares as used in Turing machines). We think the games are very appropriate to celebrating Turing’s legacy because they combine mathematics (polynomial arithmetic) with algorithmics (finding the most effective way to solve the games).

The competition has a number of rounds. Round 0 (familiarisation) began on April 1. It will be followed by 5 practice rounds which continue until July. During the practice rounds we will be publishing top scores so that participants can compare their solutions with those obtained by others. The final begins at the end of August and lasts for 3 weeks. It’s possible to join in the competition at any time.

There are 4 categories of participant: pre-university, undergraduate, postgraduate and other. The games are challenging to solve but are feasible for all categories. The current (round 0) top-scorer is an undergraduate from Ningbo.

Students registered at a UK educational institution are eligible to compete for cash and other prizes. All competitors (whether or not a UK student) will be entitled to a discount of 20 per cent on the purchase price of the book Algorithmic Problem Solving by Roland Backhouse, courtesy of the publishers John Wiley & Sons, Inc.

The final begins on 26th August, 2012 and ends on 16th September, 2012. Winners will be announced on 30th September, 2012.

A few days ago I found a video on YouTube explaining how to use CoqIde, the IDE for the Coq proof assistant. The proof that was used to illustrate the IDE was the equivalence between Peirce’s law and the excluded middle law, that is, the equivalence between the two following laws:

After watching the video, I wrote a goal-oriented, calculational proof of the equivalence between (0) and (1). In this short note, I describe the design of my proof.

A calculational proof

A useful rule of thumb is to start with the most complicated side, for it is usually easier to simplify expressions than to complicate them. With this in mind, let us try to manipulate (0) so that it becomes (1).

Looking at the shapes of (0) and (1), we immediately see that $q$ occurs in (0), but not in (1). So, if we start with (0), we will have to eliminate the occurence of $q$. This suggests that we have to use laws that involve the elimination of variables. Two elementary rules that are of this kind are the so-called absorption rules for conjunction and disjunction:

$\mleq{(2)}{(p \wedge q) \vee p ~\equiv~ p}$

$\mleq{(3)}{(p \vee q) \wedge p ~\equiv~ p}$

At a first sight, these rules may not seem very useful, because they involve only conjunction and disjunction and we want to eliminate a variable from a formula involving implication. But we know that implication can be written in terms of negation and disjunction:

These observations, together with the De Morgan rule, allow us to write a goal-oriented, calculational proof of the equivalence between (0) and (1):

\[
\beginproof
\pexp{((p{\Rightarrow}q){\Rightarrow}p)\Rightarrow p}
\hint{=}{rewrite the two leftmost $\Rightarrow$ using (4)}
\pexp{{\neg{(\neg{p} \vee q)} \vee p} ~\Rightarrow~ p}
\hint{=}{De Morgan rule, that is, $\neg{(\neg{p} \vee q)} ~\equiv~ (p \wedge \neg{q})$}
\pexp{{(p \wedge \neg{q}) \vee p} ~\Rightarrow~ p}
\hint{=}{absorption (2)}
\pexp{p{\Rightarrow}p}
\hint{=}{rewrite $\Rightarrow$ using (4)}
\pexp{\neg{p} \vee p ~~.}
\endproof
\]

The video

The video that I mentioned is shown below. It would be unfair to compare the proofs, since the main goal of the video is to illustrate Coq’s IDE and not to show how to design proofs. Nevertheless, I would like to invite the reader to comment on the use of automated/interactive theorem provers to design proofs. Thanks for reading.

I am currently in Salamanca (Spain), attending the conference Tools for Teaching Logic III. My talk was on teaching logic through algorithmic problem solving and it went quite well, I think. In particular, it seems that the audience enjoyed the examples that I have used and the teaching scenarios that I have shown. As a result, I have promised that I would upload my PhD thesis into this website. Since the thesis can also be useful for other people, I have decided to write a new blog post. I hope you enjoy!

Abstract

Algorithmic problem solving provides a radically new way of approaching and solving problems in general by using the advances that have been made in the basic principles of correct-by-construction algorithm design. The aim of this thesis is to provide educational material that shows how these advances can be used to support the teaching of mathematics and computing.

We rewrite material on elementary number theory and we show how the focus on the algorithmic content of the theory allows the systematisation of existing proofs and, more importantly, the construction of new knowledge in a practical and elegant way. For example, based on Euclid’s algorithm, we derive a new and efficient algorithm to enumerate the positive rational numbers in two different ways, and we develop a new and constructive proof of the two-squares theorem.

Because the teaching of any subject can only be effective if the teacher has access to abundant and sufficiently varied educational material, we also include a catalogue of teaching scenarios. Teaching scenarios are fully worked out solutions to algorithmic problems together with detailed guidelines on the principles captured by the problem, how the problem is tackled, and how it is solved. Most of the scenarios have a recreational flavour and are designed to promote self-discovery by the students.

Based on the material developed, we are convinced that goal-oriented, calculational algorithmic skills can be used to enrich and reinvigorate the teaching of mathematics and computing.

Suppose you write a program and you send the source code to two of your friends, ${\cal A}$ and ${\cal B}$. Your two friends read the code and when they finish, $A$ errors are detected by ${\cal A}$, $B$ errors are detected by ${\cal B}$, and $C$ errors are detected by both. So, in total, $A+B-C$ errors are detected and can now be eliminated. We wish to estimate the number of errors that remain unnoticed and uncorrected.

The original version of this problem concerns manuscripts and proofreaders, instead of source code and programmers. It was posed and solved by George Polya and published in 1976 on The American Mathematical Monthly under the name of Probabilities in Proofreading. Because the problem is interesting and Polya’s solution is short and elegant, I have decided to record and share it. Also, since code sharing and reading is a frequent activity in the software development world, estimating the desired value can be helpful for some readers of this blog.

Estimating the number of unnoticed errors

Let $E$ be the number of all errors, noticed and unnoticed, in the source code. Our goal is to estimate the value of $E-(A+B-C)$. Let $p$ be the probability that friend ${\cal A}$ notices any given error and $q$ the analogous probability for friend ${\cal B}$. The expected number of errors that may be detected by ${\cal A}$ is $E{\cdot}p$ and by ${\cal B}$ is $E{\cdot}q$. Assuming that these probabilities are independent, the expected number of errors that may be mutually detected by both friends is $E{\cdot}p{\cdot}q$.

Because we are interested in an estimate, we can safely assume that the expected numbers are approximately equal to the number of errors detected, that is, $E{\cdot}p \sim A$, $E{\cdot}q \sim B$, and $E{\cdot}p{\cdot}q \sim C$. (We use the notation $\sim$ to denote that two numbers are approximately equal.)

We now have all the ingredients to conclude the solution. Recall that our goal is to estimate the value of $E-(A+B-C)$. We calculate:

\[
\beginproof
\pexp{E-(A+B-C)}
\hint{=}{we rewrite $E$ to prepare the introduction of $A$, $B$, and $C$}
\pexp{\frac{E{\cdot}p{\cdot}E{\cdot}q}{E{\cdot}p{\cdot}q} - (A+B-C)}
\hint{\sim}{assumption on estimates}
\pexp{\frac{A{\cdot}B}{C} - (A+B-C)}
\hint{=}{arithmetic}
\pexp{\frac{(A-C){\cdot}(B-C)}{C}~~.}
\endproof
\]

Some time ago, I have installed and configured ThinkFinger, a driver for the fingerprint-readers found in most IBM/Lenovo Thinkpads, including my Lenovo X61 Tablet. Although it worked well, it was very slow! I had to wait 5 to 10 seconds for the prompt to show, then a bit more before I could swipe my finger or write my password, and then a bit more for the password to be accepted.

To make my world a better place to live, I have downloaded the development version of the driver and tried to figure out why it was being so slow. It turns out that in the library that is used to communicate with the fingerprint-reader, there was a call to the function usb_bulk_read that was taking too long. I have tried to find some official documentation about this function, but all I could find was how not to document a function (seriously, what is the role of the parameter timeout? and is it measured in seconds? milliseconds?).

Anyway, I have changed the value of the USB_TIMEOUT constant from 5000 to 5 and the fingerprint-reader is much, much better! In detail, here is the patch:

I am not sure why this works and what are the implications, but all the tests I did were satisfactory. If you know more about this problem, please let me know! I would be more than happy to understand why the USB_TIMEOUT constant seems to be acting as a time-wait delay, rather than as a timeout in the following call (line 324, libthinkfinger/libthinkfinger.c):

(I think it is strange that I haven’t found anyone complaining about the same problem. Nevertheless, I’ve decided to publish this post anyway, in case someone runs into the same problem.)

Update (2009/07/31): I’ve upload a patched SRC RPM: thinkfinger-0.3-9.jff.src.rpm. Please note that I have added the patch to Fedora’s SRC RPM.