(TMC58) The Pointfree Transform

March 31st, 2009

At today’s TMC, we commenced the study of the paper “Transforming data by Calculation” by Jose N. Oliveira. After reviewing the content of the paper, we examined the JNO’s proof that the no-confusion principle was equivalent to the kernel of R being contained in id. In Eric’s attempt to flesh out JNO’s proof, he appealed to


\langle\forall x :: f.x \Rightarrow C\rangle \equiv \langle\forall x :: f.x\rangle \Rightarrow C.

Joao tried to prove this, eventually showing that it was not a theorem. On the way there, however, he demonstrated that


\langle\forall x :: f.x \Rightarrow C\rangle \equiv  \langle\exists x :: f.x\rangle \Rightarrow C,

which turned out to be exactly what was needed! (Joao’s proof used the golden rule. Two days later, Eric used a different method, see below).

Next we delved into the first exercise, which was to provide a pointfree version of the no-loss principle. Eric proved that \langle\forall a :: \langle\exists c :: cRa\rangle\rangle equals id \subseteq ker. R. Though Joao agreed that each step was motivated, he preferred going from the pointfree to pointwise version, especially as his intuition would have led him to the pointfree formulation instantly.

The final exercise of the afternoon was Jose’s third exercise: Given a function f :: B \leftarrow A, calculate the pointwise version of ker.f and show that img.f is the coreflexive associated to predicate p, defined by p.b = \langle\exists a ::  b = f.a\rangle . Joao constructed the bulk of the proof, though it there still felt like there was a little something missing. While Eric was running onto the train back to Birmingham, Joao found the theorem


b\,(\phi.p)\,a ~~=~~ (b=a)~\wedge~p.a

which was what was needed to complete the proof!

(TMC21) A Clique Problem (IMO 2007, Problem 3)

October 25th, 2007

Today we have solved the following problem from the 2007 International Mathematics Olympiad:

In a mathematical competition some competitors are friends. Friendship is always mutual. Call a group of competitors a clique if each two of them are friends. (In particular, any group of fewer than two competitors is a clique.) The number of members of a clique is called its size. Given that, in this competition, the largest size of a clique is even, prove that the competitors can be arranged in two rooms such that the largest size of a clique contained in one room is the same as the largest size of a clique contained in the other room.

We invite you to solve the problem and then compare your solution with ours!

Click here to download our solution!

Update (07/12/2007): an error in our solution to the clique problem has been pointed out to us by Dmitri Davydok — to whom we give our thanks — and so we have removed the paper.

(TMC19) Moessner’s theorem, revisited

October 12th, 2007

Today we have seen a possible formalization of the algorithm behind Moessner’s theorem (see (TMC16) Moessner’s Theorem). In “The Art of Computer Programming”, Donald Knuth presents the following theorem:

\begin{mpdisplay}{0.2em}{8.5mm}{2mm}{3} $\langle\Sigma{}n\ms{2}{:}\ms{2}n\ms{1}\mathsf{mod}\ms{1}m\ms{1}{=}\ms{1}r\ms{2}{:}\ms{2}f{.}n\ms{1}{\times}\ms{1}z^{n}\rangle$\push\-\\     $=$\+\pop\\ ${\displaystyle\frac{1}{m}}{\times}\langle\Sigma{}c\ms{2}{:}\ms{2}0\ms{1}{\leq}\ms{1}c\ms{1}{<}\ms{1}m\ms{2}{:}\ms{2}w^{{-}c\ms{1}{\times}\ms{1}r}\ms{1}{\times}\ms{1}F{.}(w^{c}{\times}z)\rangle~~.$ \end{mpdisplay}

An easy generalization is:

\begin{mpdisplay}{0.2em}{8.5mm}{2mm}{3} $\langle\Sigma{}n\ms{2}{:}\ms{2}\langle\exists{}b\ms{2}{:}\ms{2}0\ms{1}{\leq}\ms{1}b\ms{1}{<}\ms{1}r\ms{2}{:}\ms{2}n\ms{1}\mathsf{mod}\ms{1}m\ms{1}{=}\ms{1}b\rangle\ms{2}{:}\ms{2}f{.}n\ms{1}{\times}\ms{1}z^{n}\rangle$\push\-\\     $=$ \>  \>$\{$  \>\+\+\+range disjunction\-\-$~~~ \}$\pop\\ $\langle\Sigma{}b\ms{1}{:}\ms{1}0\ms{1}{\leq}\ms{1}b\ms{1}{<}\ms{1}r\ms{1}{:}\ms{1}\langle\Sigma{}n\ms{2}{:}\ms{2}n\ms{1}\mathsf{mod}\ms{1}m\ms{1}{=}\ms{1}b\ms{2}{:}\ms{2}f{.}n\ms{1}{\times}\ms{1}z^{n}\rangle\rangle$\push\-\\     $=$ \>  \>$\{$  \>\+\+\+Knuth\-\-$~~~ \}$\pop\\ $\langle\Sigma{}b\ms{1}{:}\ms{1}0\ms{1}{\leq}\ms{1}b\ms{1}{<}\ms{1}r\ms{1}{:}\ms{1}{\displaystyle\frac{1}{m}}{\times}\langle\Sigma{}c\ms{2}{:}\ms{2}0\ms{1}{\leq}\ms{1}c\ms{1}{<}\ms{1}m\ms{2}{:}\ms{2}w^{{-}c\ms{1}{\times}\ms{1}b}\ms{1}{\times}\ms{1}F{.}(w^{c}{\times}z)\rangle\rangle$\push\-\\     $=$ \>  \>$\{$  \>\+\+\+nesting and distributivity\-\-$~~~ \}$\pop\\ ${\displaystyle\frac{1}{m}}{\times}\langle\Sigma{}b,c\ms{2}{:}\ms{2}0\ms{1}{\leq}\ms{1}b\ms{1}{<}\ms{1}r\ms{1}{\wedge}\ms{1}0\ms{1}{\leq}\ms{1}c\ms{1}{<}\ms{1}m\ms{2}{:}\ms{2}w^{{-}c\ms{1}{\times}\ms{1}b}\ms{1}{\times}\ms{1}F{.}(w^{c}{\times}z)\rangle~~.$ \end{mpdisplay}

Naming this new generating function as cross.F.r.m and observing that the generating function for the positive natural numbers is

\begin{displaymath}{\displaystyle\frac{1}{(1\ms{2}{-}\ms{2}z)^{2}}}\mbox{\ \ \ ,}\end{displaymath}

and that the partial sums of a sequence denoted by a generating function F.z is

\begin{displaymath}{\displaystyle\frac{1}{1\ms{2}{-}\ms{2}z}}\ms{1}{\times}\ms{1}F{.}z\mbox{\ \ \ ,}\end{displaymath}

the algorithm behind Moessner’s theorem is:

\begin{mpdisplay}{0.2em}{8.5mm}{2mm}{3} $F{.}z\ms{1}:=\ms{1}{\displaystyle\frac{1}{(1\ms{2}{-}\ms{2}z)^{2}}}\ms{2};$\\     $j\ms{1}:=\ms{1}m\ms{2}{-}\ms{2}1\ms{2};$\\     \push$\{~~$\=\+\push\textbf{Invariant}:$~~~~$\=\+I\-\pop\-$ ~~\}$\pop\\ \push$\MPsf{do}\ms{2}$\=\+\push$j\ms{1}{\geq}\ms{1}1~~\MPsf{\rightarrow}~~$\=\+$~$\=\+$F{.}z\ms{2}:=\ms{2}{\displaystyle\frac{1}{1\ms{2}{-}\ms{2}z}}\ms{1}{\times}\ms{1}\mathit{cross\/}{.}F{.}j{.}m\ms{3};$\\     $j\ms{1}:=\ms{1}j\ms{2}{-}\ms{2}1$\-\-\pop\-\\     $\MPsf{od}$\pop\\ \push$\{~~$\=\+$\left[z^{n{\times}m}\right]\ms{1}F{.}z\ms{1}{=}\ms{1}(n\ms{2}{+}\ms{2}1)^{m}$\-$ ~~\}$\pop \end{mpdisplay}

We were not successful in finding and proving an invariant I for this algorithm, yet. If you have any idea, please let us know!

(TMC17) IFIP WG 2.1 meeting in September 2007

September 26th, 2007

Today Roland has spoken about the recent IFIP WG 2.1 meeting in Kyoto. In particular we have discussed the following probabilistic-game problem:

“Consider the following game. There are n players each of whom has a coin. A round of the game consists of all the players tossing their coins; the players who toss tails lose and take no further part in the game. The game consists of repeating rounds until either all players have lost or exactly one player remains. In the latter case, the remaining player is the winner (in the former case, there is no winner).”

The problem is to determine a tight lower bound on the probability that a play of the game results in there being a winner (assuming that we start with at least 1 player).

Click here to download our solution

(TMC16) Moessner’s theorem

September 4th, 2007

Today we have discussed Moessner’s theorem and we tried to solve it using generating functions. For those who don’t know Moessner’s theorem, we provide some information:

In 1951, Alfred Moessner conjectured that the natural mth powers can be generated in the following way: cross out every mth number from the sequence of positive natural numbers and compute the sequence of partial sums. From the resulting sequence, cross out every (m-1)st number and, again, form the sequence of partial sums. Again, cross out every (m-2)nd number from the resulting sequence and form the sequence of partial sums. Repeat the process m-1 times and the final sequence contains all natural mth powers.

For example, for m=4, we obtain

 \def\strike{\makebox[0pt][l]{/}}\[ \begin{array}{cccccccccccc} 1 & 2 & 3 & \strike 4 & 5 & 6 & 7 & \strike 8 & 9 & 10 & 11 & \strike 1 \strike 2  \cdots\\ 1 & 3 & \strike 6 & ~ & 11 & 17 & \strike 2 \strike 4 & ~ &  33 &  43  & \strike 5 \strike 4 &  ~~~ \cdots \\ 1 & \strike 4 &    &       &15 & \strike 3 \strike 2 &   &    &   65 & \strike 1 \strike 0 \strike 8 & & ~~~ \cdots \\ 1 &  &  &  & 16 &  &  &  & 81 &  &  & ~~~ \cdots\\ \end{array} \]

(TMC15) The Torch Problem revisited

July 24th, 2007

Today we have discussed Roland’s new solution to the Torch problem. If you want to read it, you can download Roland’s note named “The Capacity C Torch Problem“. We have also continued discussing the Chinese Remainder Theorem.

(TMC14) The Chinese Remainder Theorem, again

July 17th, 2007

Today we have continued discussing the Chinese Remainder Theorem and, after writing down the proof that a solution exists, Roland pointed out a way to extract the algorithm from the proof.

Roland also introduced his new solution to the Torch Problem.

If you are interested in learning more about what we did regarding the Chinese Remainder Theorem, you can read a working document written by Arjan and Joao.

(TMC13) The Chinese Remainder Theorem and the Celebrity Clique Problem

July 3rd, 2007

Today we have discussed the Chinese Remainder Theorem and a possible derivation for the algorithm. We have started with its formal derivation, which is:
\begin{mpdisplay}{0.2em}{5.5mm}{2mm}{3}\push$\{~~$\=\+$m\ms{1}{>}\ms{1}0\ms{1}{\wedge}\ms{1}n\ms{1}{>}\ms{1}0\ms{1}{\wedge}\ms{1}\langle\exists{}x{:}{:}\ms{3}x\ms{1}{=}\ms{1}a\ms{2}(\textsf{mod}~~ m)\ms{3}{\wedge}\ms{3}x\ms{1}{=}\ms{1}b\ms{2}(\textsf{mod}~~ n)\rangle$\-$ ~~\}$\pop\\         $S$\\        \push$\{~~$\=\+$x\ms{1}{=}\ms{1}a\ms{2}(\textsf{mod}~~ m)\ms{3}{\wedge}\ms{3}x\ms{1}{=}\ms{1}b\ms{2}(\textsf{mod}~~ n)$\-$ ~~\}$\pop$~~.$\end{mpdisplay}

We then derived the algorithm that is usually presented in textbooks, but we are not happy with the lack of motivation of our solution.

In the last 15 minutes, Arjan presented a solution to a simplified version of the “celebrity cliques” problem.

(TMC12) Generating Functions, continued

June 12th, 2007

Today we’ve continued discussing generating functions. In particular:

  • we’ve briefly discussed the paper Objects of Categories as Complex Numbers, written by Marcelo Fiore and Tom Leinster;
  • we’ve seen how we can use generating functions to calculate closed formulae for recurrences;

(TMC11) Generating Functions

June 5th, 2007

Today we’ve discussed generating functions. We’ve seen how they can be used to discover/prove identities, to solve counting problems and how to find datatypes that satisfy certain equations.

For instance, is there any datatype S.z that satisfies the equation?

$S.z + S.z \times z \times z \cong 1 + Bool \times z \times S.z$~~~.

Using arithmetic (on complex numbers), we get

$S.z = \frac{1}{(1-z)^2} = \frac{1}{(1-z)} \times \frac{1}{(1-z)}$~~~,

which denotes the type “Pair of Lists”. We’ve decided to investigate on related work to see under which conditions these kind of manipulations hold. Next week we continue with the discussion.