Test-driven maths: convergent sequences

I want to show today that working in the paradigm of test-driven-development, we can develop a working definition of a convergent sequence. Metaphorically speaking, we want to develop a mathematical "program" that, given a sequence, says to us that this sequence is convergent in some useful sense.

I will start with an easy example (which will be our first test). We look at the sequence of numbers, which we will call

Test sequence 1

$$1, \frac{1}{2},  \frac{1}{3},  \frac{1}{4}, ...$$

or, in other, terms $\{\frac{1}{n}\}_n$

It is clear (by intuition) that the numbers in this sequence (in the following sequence 1) become smaller and smaller approaching, but never touching 0. For this reason we will use this as our first test case, and try to derive a formal definition of what is a sequence of numbers that converges to 0.

By looking at the sequence 2 things become apparent: 1) the numbers get smaller and smaller and 2) the  numbers always are positive. So we try our first defintion.

Convergent sequences, take 1

A sequence of positive numbers is said to be convergent to 0 if the numbers become smaller and smaller.

Let us try now to put it in more formal terms


Convergent sequences, take 2

A sequence of positive numbers $x_n\geq0$ is said to be convergent to 0 if $x_{n+1}< x_n$ for all $n$ index of the sequence.

Since now $\frac{1}{n+1}<\frac{1}{n}$, this definition seems to include our test tesequence 1, in the sense that according to this definition, our sequence converges to 0. Can we stop now? No. We have written a small test (checking whether the sequence 1 is converging) and a small piece of code (our take 2). But our mathematical insight is not yet satisfied, because our test does not cover many possible inputs (in form of test sequences of course). So, we have to extend our test.

In particular, it is maybe useful to have a sequence of which we know (always by intuition) that it does not converge to 0 so that we can check that our definition also fails when it must. The simplest thing to do is to consider the sequence 1 and add 1 to all members.


Test sequence 2

$$2, 1+\frac{1}{2},  1+\frac{1}{3},  1+\frac{1}{4}, ...$$

Now, since our sequence is composed of decreasing positive numbers, our tentative definition would call it convergent. Since we know that this sequence does not converge, that means that our program (take 2) does not pass the test. In fact the point is that our test sequence 2 is always at least 1 away from 0. So, let us add to our definition that the sequence cannot have a definite distance from 0.

Convergent sequences, take 3

A sequence of positive numbers $x_n\geq0$ is said to be convergent to 0 if $x_{n+1}< x_n$ for all $n$ index of the sequence and for any positive number $\epsilon$, it is not true that all numbers in the sequence are larger than $\epsilon$.

This looks good. Let us build some new test to check whether we are really there. Say, we take the sequence 2 and we put some 0 here and there. The resulting sequence should not converge according to our definition, since we are not getting closer and closer to 0 with all numbers!


Test sequence 3

$$2, 0, 1+\frac{1}{2},  0, 1+\frac{1}{3},  0, 1+\frac{1}{4}, ...$$

Now we have problem. The sequence is clearly non convergent: if we take the odd indexes, we go to 1, otherwise we go to 0. Since we have 0s over and over again in our sequence, we cannot find an $\epsilon$ such that all numbers are larger than that, so for that reason the sequence would be classified as convergent. But: since we inserted 0 over and over again, the numbers are not decreasing, and the sequence is classified as not convergent for that reason. This sounds weird. It looks that we pass the test, but for the wrong reason. Let us keep in mind that there is some problem with the decreasing property and let us correct the part regarding the distance from 0.


Convergent sequences, take 4

A sequence of positive numbers $x_n\geq0$ is said to be convergent to 0 if $x_{n+1}< x_n$ for all $n$ index of the sequence and for any positive number $\epsilon$, we can find some index $k$ (dependent on $\epsilon$) such that all numbers with index larger than $k$ are smaller than $\epsilon$.

Now we are on the safer side with the test sequences 2 and 3. Indeed, if I choose my $\epsilon = 0.9$ I am not able to find any index such that the numbers with larger index are smaller than 0.9, since I have over and over again some $1+\frac{1}{n}$ popping up in my sequence. Are we still on the safe side with sequence 1? Yes, since if I choose $k=\frac{1}{\epsilon}$, it is clear that for all larger index the numbers in the sequence are smaller than $\epsilon$ (this is undergraduate algebra, just try it). Note that now the test sequence 3 is classified as not convergent for both not being decreasing and for being not arbitrary small.

Now let us go back to the problem with the decreasing sequences.. If I have a sequence of numbers and scramble the order, I do not want that this scrambling changes whether we call the sequence convergent or not. So, we come with a second test sequences that has to converge.


Test sequence 4

$$\frac{1}{2},  1,  \frac{1}{4}, \frac{1}{3}, ...$$

We just switched the position of the neighbours. Now, this sequence is intuitevly convergent, but our take 4 says it is not, since the elements are not decreasing. So, what if we drop the assumption of having decreasing numbers?


Convergent sequences, take 5

A sequence of positive numbers $x_n\geq0$ is said to be convergent to 0 if for any positive number $\epsilon$, we can find some index $k$ (dependent on $\epsilon$) such that all numbers with index larger than $k$ are smaller than $\epsilon$.

This sounds familiar. Surprising as it is, real world mathematics really feel like that often: you start with some hypothesis of a theorem, try out some examples, until you are confident enough. Constructing the examples exactly gives you the boundaries of the hypothetical theorem. Can we build proofs by this method?

A test-driven revival

Since more than 1 year I left Freiburg and the BCF to start working in the development of MEMS with Bosch GmbH. For some complicated reasons connected to my work there, I've got involved in software engineering and in particular in test-driven development. But only today I realised why I've got involved there and why I like it.

In fact, test-driven development is a kind of "formalization" of how mathematicians actually work!

In particular, I found it complying with Gower's pedagogical principle.

Following this intuition, I will try in the next days (months?) to revive this blog, and to show that what computer scientists rediscovered in the middle of the of 90ies as test-driven development is nothing but what mathematicians are doing since centuries.

Appello: dimostrazione del teorema dei 4 colori

Qualcuno sa se questo articolo e' vero?

L'autore da' una dimostrazione senza computer del teorema dei 4 colori. Potrebbe essere possibile, soprattutto dato che l'autore (Ibrahim Cahit) sembra essere un professionista.

Per i non-addetti ai lavori: il teorema dei 4 colori afferma che e' possibile colorare ogni mappa (senza enclavi) con al massimo 4 colori differenti. E' stato provato alla fine degli anni '80 verificando ogni caso possibile, dopo aver ridotto il problema ad un numero finito (ma grande) di casi critici possibili.

Ovviamente fu quasi uno scandalo per la comunita' matematica, quindi sarebbe veramente interessante sapere se esiste una dimostrazione "umana".

Purtroppo non sono un esperto di teoria dei grafi, quindi non penso di poter verificare la dimostrazione di persona: qualcuno sa qualcosa?

Al Mercato Nero

Ho varie cose su cui vorrei scrivere nei prossimi giorni: spero di riuscire ad evaderle tutte prima che il semestre cominci: varie conferenze a cui sono stato nell'ultimo mese, un'altra che stiamo organizzandon con un collega, l'ultimo paper che ho messo su arXiv, il corso che terrò questo semestre.

Comincio con la bizzarra installazione teatrale a cui ho partecipato ieri. La compagnia teatrale del teatro cittadino di Friburgo ha realizzato un progetto con delle scuole, in cui gli studenti dovevano realizzare delle rappresentazioni teatrali che trattasero di alcuni temi neuroscientifici: stimulazione cerebrale profonda, interfaccia cervello-computer ed altre amenità.

Ieri hanno presentato questi spettacoli, insieme a conferenze e dibattiti diretti da alcuni specialisti del settore. La sera è stato organizzato dalla compagnia un mercato nero del sapere. 48 esperti hanno offerto delle conversazioni di 1/2 ora su un tema a loro scelta al pubblico. Il pubblico poteva scegliere l'espero, e per 1 euro, parlare con lui del tema proposto.

Il mio tema era "Conway's game of life: l'ultimo gioco dove l'uomo è ancora superiore alla macchina". La mia idea era di partire dalla notizia che da pochi mesi esistono programmi giocatori di go in grado di competere con giocatori professionisti. Questo è stata una grande soprpresa per me, perchè nell'ambiente dei giocatori di strategia si andava mormorando che, a differenza degli scacchi, il go era insolubile per i computer, perchè non è attaccabile in maniera brute force, e per altri motivi più profondi. Da quello che ho capito essenzialmente è difficile scrivere un algoritmo di valutazione.

Poi volevo introdurre il game of life: spiegarne le regole, e giocare alcune situazioni semplici, per far capire che è in teoria è possibile costruire un computer composto da automi cellulari.

L'idea era di poi passare a Turing, Gödel, e argomentare che il computer non può, a causa del teorema di Gödel, superare l'uomo nel game of life.

Cosa a cui non credo fino in fondo, a dire il vero. Ma tant'è: tutte e due le conversazioni sono andate benissimo, nonostante il primo ragazzo fosse uno scolaro di 17 anni e il secondo uno studente di storia al 3° anno.

Di più: certamente un'esperienza ispiratrice e che ripeterò, qualora ce ne sia ancora l'occasione.

L'alieno imbroglione

Ho finalmente risolto l'enigma presentato qua.

In questo racconto, un alieno raccoglie tutti i dati sulla terra; per memorizzarli, un computer incide su una barretta metallica una fessura. Lo sviluppo binario della posizione della fessura è esattamente il file contenente i dati raccolti sul pianeta terra.

Questo, in via teorica, permette di conservare una quantità di dati infinita tramite un oggetto semplice quale una barretta metallica: basta memorizzare in maniera analogica, in maniera da evitare di utilizzare l'inefficiente memoria di un computer digitale.

L'errore nel racconto è: i dati, prima di essere stampati sulla barretta metallica, devono essere presenti nel computer che manovra la macchina che esegue la fessura. Esso deve quindi avere una memoria digitale sufficiente!

Ovviamente, si può ovviare a questo problema utilizzando un computer esso stesso analogico, ma questo non c'è, nel racconto.

PS: sto leggendo questo libro: fino ad adesso posso solo consigliarlo

Un nuovo giocattolo

È python!

Per me che non ho mai programmato è una meraviglia: un linguaggio di programmazione semplice e meravigliosamente efficace.

In Ubuntu (una distribuzione Linux che vi consiglio di installare: ci riuscirete anche se fino ad ora avete usato solo Windows) è di solito preinstallato, altrimenti aprite l'applicazione synaptic e installate python e ipython.

Ne vedrete delle belle!