$\mleq{(0)}
{((p{\Rightarrow}q){\Rightarrow}p)\Rightarrow p}
$

and
$\mleq{(1)}
{\neg{p} \vee p}
$

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:

$\mleq{(4)}
{{p{\Rightarrow}q} ~\equiv~ {\neg{p} \vee q}}
$

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.

In June, Jeremy Weissmann read my proof and he proposed a different development. His argument was well structured, but it wasn’t as goal-oriented as I’d hoped for. Gladly, after a brief discussion, we realised that we were missing a great opportunity to use the trading rule (details below)!

I was so pleased with the final outcome that I decided to record and share the new proof.

Problem statement

In graph theory, the degree of a vertex $A$, $\fapp{d}{A}$, is the number of edges incident with the vertex $A$, counting loops twice. So, considering Graph 0 below, we have $\fapp{d}{A}=3$, $\fapp{d}{B}=3$, $\fapp{d}{C}=1$, $\fapp{d}{D}=3$, and $\fapp{d}{E}=2$.

Graph 0: Example of an undirected graph with five vertices

A well-known property is that every undirected graph contains an even number of vertices with odd degree. The result first appeared in Euler’s 1736 paper on the Seven Bridges of Königsberg and is also known as the handshaking lemma (that’s because another way of formulating the property is that the number of people that have shaken hands an odd number of times is even).

As we can easily verify, Graph 0 satisfies this property. There are four vertices with odd degree ($A$,$B$, $C$, and $D$), and 4, of course, is an even number.

Although the proof of this property is simple, all the conventional proofs that I know of are not goal-oriented. My goal is to show you a development of a goal-oriented proof. Also, my proof is completely guided by the shape of the formulae involved, which helps reducing the amount of guessing involved.

Notations that I use

Before we start, let me explain the notations that I use. I assume the existence of two predicates, $even$ and $odd$, that test the parity of numbers. For example, $\fapp{even}{8}$ and $\fapp{odd}{3}$ are both true, and $\fapp{even}{5}$ and $\fapp{odd}{6}$ are both false. Also, I use the so-called Eindhoven notation for quantifiers; for example, to express the sum of all natural even numbers less than 50 I write $\quantifier{\Sigma}{n}{0{\leq}n{<}50~\wedge~\fapp{even}{n}}{n}$, and instead of writing $\fapp{even}{0}{\equiv}\fapp{even}{1}{\equiv}{\cdots}{\equiv}\fapp{even}{50}$, I write $\quantifier{\equiv}{n}{0{\leq}n{\leq}50}{\fapp{even}{n}}$.

An advantage of using a systematic notation for quantifiers is that we can write the rules that manipulate quantifiers in a very general way. For example, suppose that the quantifier $\bigoplus$ generalises the binary operator $\oplus$. Moreover, let us assume that $1_{\oplus}$ is the unit of $\oplus$, that is, for all $n$, we have:

\[
n{\oplus}1_{\oplus} = 1_{\oplus}{\oplus}n = n ~~.
\]

Then, the so-called trading rule is valid:

\[
\beginproof
\pexp{\quantifier{\bigoplus}{n}{P \wedge Q}{T}}
\equiv & \\
\pexp{\quantifier{\bigoplus}{n}{P}{{\sf if~~} Q \rightarrow T~~\Box~~\neg{Q} \rightarrow 1_{\oplus} {~~\sf fi}} ~.}
\endproof
\]

This rule applies to all quantifiers that generalise operators with units. For example, because true is the unit of $\equiv$, we have

\[
\beginproof
\pexp{\quantifier{\equiv}{n}{P \wedge Q}{T}}
\equiv & \\
\pexp{\quantifier{\equiv}{n}{P}{{\sf if~~} Q \rightarrow T~~\Box~~\neg{Q} \rightarrow true {~~\sf fi}} ~,}
\endproof
\]

which is the same as

\[
\quantifier{\equiv}{n}{P \wedge Q}{T} \equiv
\quantifier{\equiv}{n}{P}{Q \Rightarrow T} ~~.
\]

Calculating a solution to the handshaking lemma

Now, the first step in any goal-oriented solution is to express the goal. In other words, what do we want to prove or calculate? Using the notation just described and assuming that the variable $v$ ranges over the set of all vertices, our goal is to determine the value of the following expression:

\[
\fapp{even}
{
\quantifier{\Sigma}{v}
{\fapp{odd}{(\fapp{d}{v})}}
{1}
}~~~.
\]
Note that we are adding 1 (counting) for each vertex $v$ with an odd degree. We then apply the predicate $even$ to the result. If the result is true, there is an even number of vertices with odd degree; otherwise, there is an odd number. Our goal is thus to determine its value. (We know that it must evaluate to true, because the property is well-known. However, in general, when doing mathematics, we don’t know what is the final value; that is why goal-oriented and calculational proofs are important.)

We know that the predicate $even$ distributes over addition, so we calculate:

\[
\beginproof
\pexp{\fapp{even}{\quantifier{\Sigma}{v}{\fapp{odd}{(\fapp{d}{v})}}{1}}}
\hint{=}{$even$ distributes over addition}
\pexp{\quantifier{\equiv}{v}{\fapp{odd}{(\fapp{d}{v})}}{\fapp{even}{1}}}
\hint{=}{$\fapp{even}{1}\equiv false$}
\pexp{\quantifier{\equiv}{v}{\fapp{odd}{(\fapp{d}{v})}}{false}}
\hint{=}{trading rule (see above)}
\pexp{\quantifier{\equiv}{v}{\!}{\fapp{odd}{(\fapp{d}{v})} \Rightarrow false}}
\hint{=}{${\fapp{odd}{n}\Rightarrow{false}} ~\equiv~ {\fapp{even}{n}}$}
\pexp{\quantifier{\equiv}{v}{\!}{\fapp{even}{(\fapp{d}{v})}}}
\hint{=}{$even$ distributes over addition}
\pexp{\fapp{even}{\quantifier{\Sigma}{v}{\!}{\fapp{d}{v}}}}
\endproof
\]

This calculation shows that the parity of the number of vertices with odd degree is the same as the parity of the sum of all the degrees. But because each edge has two ends, the sum of all the degrees is simply twice the total number of edges. We thus have:

\[
\beginproof
\pexp{\fapp{even}{\quantifier{\Sigma}{v}{\fapp{odd}{(\fapp{d}{v})}}{1}}}
\hint{=}{calculation above}
\pexp{\fapp{even}{\quantifier{\Sigma}{v}{\!}{\fapp{d}{v})}}}
\hintf{=}{the sum of all the degrees is twice the}
\hintl{number of edges, i.e., an even number}
\pexp{true~~.}
\endproof
\]

And so we can conclude that every undirected graph contains an even number of vertices with odd degree.

What is wrong with conventional solutions?

Conventional solutions for this problem are usually very similar to the following one, taken from the book “Ingenuity in Mathematics” (p. 8), by Ross Honsberger:

The proof in general is simple. We denote by T the total of all the local degrees:

(1) T = d(A) + d(B) + d(C) + … + d(K) .

In evaluating T we count the number of edges running into A, the number into B, etc., and add. Because each edge has two ends, T is simply twice the number of edges; hence T is even.

Now the values d(P) on the right-hand side of (1) which are even add up to a sub-total which is also even. The remaining values d(P) each of which is odd, must also add up to an even sub-total (since T is even). This shows that there is an even number of odd d(P)’s (it takes an even number of odd numbers to give an even sum). Thus there must be an even number of vertices with odd local degree.

There is nothing wrong with this solution in the sense that it shows why the property holds. However, it is clearly oriented to verification: it starts by introducing the total sum of all the local degrees, observing that its value is even; then it analyses that sum to conclude the property. The question is: how can we teach students to come with the total sum of all the local degrees? In general, how can we teach students to come with seemingly unrelated concepts that will be crucial in the development of their arguments? I don’t think we can.

On the other hand, if we look at the goal-oriented proof, we see that the goal is simple to express. Furthermore, with some training, most students would write it correctly and would be able to calculate that the parity of the number of vertices with odd degree is the same as the parity of the sum of all the degrees. And then (and only then) the introduction of the total sum of all the degrees would make sense. In a way, goal-oriented calculations are like that famous masked magician that reveals magic’s biggest secrets, for they reveal how the rabbit got into the hat.

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.

Download the PDF

Principles and Applications of Algorithmic Problem Solving (PhD Thesis, João F. Ferreira, 345 pages)

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
\]

This is the desired estimate!

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:

Index: libthinkfinger/libthinkfinger.c
===================================================================
--- libthinkfinger/libthinkfinger.c     (revision 118)
+++ libthinkfinger/libthinkfinger.c     (working copy)
@@ -35,7 +35,7 @@

 #define USB_VENDOR_ID     0x0483
 #define USB_PRODUCT_ID    0x2016
-#define USB_TIMEOUT       5000
+#define USB_TIMEOUT       5
 #define USB_WR_EP         0x02
 #define USB_RD_EP         0x81
 #define DEFAULT_BULK_SIZE 0x40

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):

usb_retval = usb_bulk_read (tf->usb_dev_handle, USB_RD_EP, bytes,
                            size, USB_TIMEOUT);

(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.

I expect the future to be as wonderful as the past has been. There’s still an enormous amount of interesting work to do. As far as the fundamental science is concerned, we still certainly do not know how to prove programs correct. We need a lot of steady progress in this area, which one can foresee, and a lot of breakthroughs where people suddenly find there’s a simple way to do something that everybody hitherto has thought to be far too difficult.

In graph theory, the degree of a vertex $A$, $\fapp{d}{A}$, is the number of edges incident with the vertex $A$, counting loops twice. So, considering Graph 0 below, we have $\fapp{d}{A}=3$, $\fapp{d}{B}=3$, $\fapp{d}{C}=1$, $\fapp{d}{D}=3$, and $\fapp{d}{E}=2$.

Graph 0: Example of an undirected graph with five nodes

A well-known property is that every undirected graph contains an even number of vertices with odd degree. The result first appeared in Euler’s 1736 paper on the Seven Bridges of Königsberg and is also known as the handshaking lemma (that’s because another way of formulating the property is that the number of people that have shaken hands an odd number of times is even).

As we can easily verify, Graph 0 satisfies this property. There are four vertices with odd degree ($A$,$B$, $C$, and $D$), and 4, of course, is an even number.

Although the proof of this property is simple, I have never seen it proved in a calculational and goal-oriented way. My aim with this post is to show you a development of a goal-oriented proof.

Before we start, let me explain the notations that I use. I assume the existence of two predicates, $even$ and $odd$, that test the parity of numbers. For example, $\fapp{even}{8}$ and $\fapp{odd}{3}$ are both true, and $\fapp{even}{5}$ and $\fapp{odd}{6}$ are both false. Also, I use the so-called Eindhoven notation for quantifiers; for example, to express the sum of all natural even numbers less than 50 I write $\quantifier{\Sigma}{n}{0{\leq}n{<}50~\wedge~\fapp{even}{n}}{n}$, and instead of writing $\fapp{even}{0}{\equiv}\fapp{even}{1}{\equiv}{\cdots}{\equiv}\fapp{even}{50}$, I write $\quantifier{\equiv}{n}{0{\leq}n{\leq}50}{\fapp{even}{n}}$.

Now, the first step in any goal-oriented solution is to express the goal. In other words, what do we want to prove or calculate? Using the notation just described and assuming that $V$ is the set of all vertices, our goal is to determine the value of the following expression:

\[
\fapp{even}
{
\quantifier{\Sigma}{a}
{a{\in}V{\wedge}\fapp{odd}{(\fapp{d}{a})}}
{1}
}~~~.
\]
Note that we are adding 1 (counting) for each node $a$ in $V$ with an odd degree. We then apply the predicate $even$ to the result. If the result is true, there is an even number of vertices with odd degree; otherwise, there is an odd number. Our goal is thus to determine its value. (We know that it must evaluate to true, because the property is well-known. However, in general, when doing mathematics, we don't know what is the final value; that is why goal-oriented and calculational proofs are important.)

We know that the predicate $even$ distributes over addition, so we calculate:

\[
\beginproof
\pexp{\fapp{even}{\quantifier{\Sigma}{a}{a{\in}V\,{\wedge}\,\fapp{odd}{(\fapp{d}{a})}}{1}}}
\hint{=}{$even$ distributes over addition}
\pexp{\quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{odd}{(\fapp{d}{a})}}{\fapp{even}{1}}}
\hintf{=}{the most reasonable thing to do is to simplify the}
\hintm{range; this step prepares that simplification, because}
\hintm{$\quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{even}{(\fapp{d}{a})}}{true}$ is true and $\equiv$ is reflexive.}
\hintl{Also, $\fapp{even}{1}{\equiv}false$.}
\pexp{\quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{odd}{(\fapp{d}{a})}}{false} \equiv \quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{even}{(\fapp{d}{a})}}{true}}
\hint{=}{we make the terms equal, using the information in the range}
\pexp{\quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{odd}{(\fapp{d}{a})}}{\fapp{even}{(\fapp{d}{a})}} \equiv \quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{even}{(\fapp{d}{a})}}{\fapp{even}{(\fapp{d}{a})}}}
\hint{=}{range splitting}
\pexp{\quantifier{\equiv}{a}{a{\in}V}{\fapp{even}{(\fapp{d}{a})}}}
\hint{=}{$even$ distributes over addition}
\pexp{\fapp{even}{\quantifier{\Sigma}{a}{a{\in}V}{\fapp{d}{a})}}~~.}
\endproof
\]

This calculation shows that the parity of the number of vertices with odd degree is the same as the parity of the sum of all the degrees. But because each edge has two ends, the sum of all the degrees is simply twice the total number of edges. We thus have:

\[
\beginproof
\pexp{\quantifier{\equiv}{a}{a{\in}V\,{\wedge}\,\fapp{odd}{(\fapp{d}{a})}}{\fapp{even}{1}}}
\hint{=}{calculation above}
\pexp{\fapp{even}{\quantifier{\Sigma}{a}{a{\in}V}{\fapp{d}{a})}}}
\hintf{=}{the sum of all the degrees is twice the}
\hintl{number of edges, i.e., an even number}
\pexp{true~~.}
\endproof
\]

And so we can conclude that every undirected graph contains an even number of vertices with odd degree.

What is wrong with conventional solutions?

Conventional solutions for this problem are usually very similar to the following one, taken from the book “Ingenuity in Mathematics” (p. 8), by Ross Honsberger:

The proof in general is simple. We denote by T the total of all the local degrees:

(1) T = d(A) + d(B) + d(C) + … + d(K) .

In evaluating T we count the number of edges running into A, the number into B, etc., and add. Because each edge has two ends, T is simply twice the number of edges; hence T is even.

Now the values d(P) on the right-hand side of (1) which are even add up to a sub-total which is also even. The remaining values d(P) each of which is odd, must also add up to an even sub-total (since T is even). This shows that there is an even number of odd d(P)’s (it takes an even number of odd numbers to give an even sum). Thus there must be an even number of vertices with odd local degree.

There is nothing seriously wrong with this solution. It clearly shows why the property holds. However, it is, in my view, oriented to verification: it starts by introducing the total sum of all the local degrees, observing that its value is even; then it analyses that sum to conclude the property. My question is: how can we teach students to come with the total sum of all the local degrees? In general, how can we teach students to come with seemingly unrelated concepts that will be crucial in the development of their arguments? I don’t think we can.

On the other hand, if we look at the goal-oriented proof, we see that the goal is simple to express. Furthermore, with some training, most students would write it correctly and would be able to calculate that the parity of the number of vertices with odd degree is the same as the parity of the sum of all the degrees. And then (and only then) the introduction of the total sum of all the degrees would make sense. In a way, goal-oriented calculations are like that famous masked magician that reveals magic’s biggest secrets, for they reveal how the rabbit got into the hat.

I found the following problem on K. Rustan M. Leino’s puzzles page:

[Carroll Morgan told me this puzzle.]

Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence.

More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n). Prove that for any positive K and natural n, F(n*K) is a multiple of F(K).

This problem caught my attention, because it looks like a good example for using a result that I have derived last year. My result gives a reasonable sufficient condition for showing that a function distributes over the greatest common divisor and shows that the Fibonacci function satisfies the condition.

In fact, using the property that the Fibonacci function distributes over the greatest common divisor, we can solve this problem very easily. Using $\fapp{fib}{n}$ to denote the Fibonacci number $n$, $m{\nabla}n$ to denote the greatest common divisor of $m$ and $n$, and $\setminus$ to denote the division relation, a possible proof is:

\[
\beginproof
\pexp{\text{$\fapp{fib}{(n{\times}k)}$ is a multiple of $\fapp{fib}{k}$}}
\hint{=}{definition}
\pexp{\fapp{fib}{k} \setminus \fapp{fib}{(n{\times}k)}}
\hint{=}{rewrite in terms of $\nabla$}
\pexp{\fapp{fib}{k} ~\nabla~ \fapp{fib}{(n{\times}k)} ~=~ \fapp{fib}{k}}
\hint{=}{$fib$ distributes over $\nabla$}
\pexp{\fapp{fib}{(k{\nabla}(n{\times}k))} = \fapp{fib}{k}}
\hint{=}{$k{\nabla}(n{\times}k) = k$}
\pexp{\fapp{fib}{k} = \fapp{fib}{k}}
\hint{=}{reflexivity}
\pexp{true~~.}
\endproof
\]

The crucial step is clearly the one where we apply the distributivity property. Distributivity properties are very important, because they allow us to rewrite expressions in a way that prioritizes the function that has the most relevant properties. In the example above we could not simplify $\fapp{fib}{k}$ nor $\fapp{fib}{(n{\times}k)}$, but applying the distributivity property prioritised the $\nabla$ operator — and we know how to simplify $k{\nabla}(n{\times}k)$. Furthermore, in practice, distributivity properties reduce to simple syntactic manipulations, thus reducing the introduction of error and simplifying the verification of our arguments.

(Now that I think about it, perhaps it would be a good idea to write a note on distributivity properties, summarizing their importance and their relation with symbol dynamics.)

If you have any corrections, questions, or alternative proofs, please leave a comment!

The new and official URL of this website is now shorter and r’s-free: joaoff.com .

If you don’t like it and prefer the old one, please let me know!

Inside, there was a check for a correction I sent him some months ago. In fact, it was not really a correction; it was more like a comment. And it was so obvious (he even said that) that he just sent $\$$0.32, instead of the usual $\$$2.56. But hey, who cares? I’ve got Knuth’s autograph now

Perhaps I should set as one of my goals to find a proper error, so that I can receive a $\$$2.56 check By the way, the errata of the Concrete Mathematics is available online and this particular omission is documented as follows:

page 338, line 2 from the bottom
change “for $z$” to “for $z$ and multiplying by $a$”