Ramsey og de andre

Ligesom rockmusikken har matematikken sine “unge døde”. De fleste kender Galois og Abel, men der er også bl.a. Ramsey. Frank Plumpton Ramsey (1903-1930) var en engelsk matematiker fra Cambridge, der interesserede sig for lidt af hvert – matematisk økonomi, filosofi og matematisk logik. I hans artikel “On a problem of formal logic”, der omhandler afgørbarheden af et fragment af første-ordens-logik, optræder et lille kombinatorisk lemma, som i dag kendes som Ramseys sætning og endte med at danne grundlaget for et område af grafteori, som i dag kendes som Ramsey-teori.

Én måde at formulere Ramseys sætning på er denne (vi antager at 0 ikke er et naturligt tal).

Lad n \in \mathbb{N} og c \in \mathbb{N}. Lad C = \{ 1,..,c \}. Betragt \mathbb{N}_n, mængden af alle delmængder af \mathbb{N} med n elementer. Betragt en vilkårlig farvningsfunktion f, der giver hver delmængde én af c mulige farver, dvs. f: \mathbb{N}_n \rightarrow C. Da findes der en uendelig delmængde \mathbb{M} \subseteq \mathbb{N} og en farve k således at for enhver S \in \mathbb{M} har vi at f(S) = k.

Sagt på mere jævnt dansk, uanset hvordan vi farver n-delmængderne af de naturlige tal med endeligt mange farver, kan vi altid udvælge en uendelig delmængde af de naturlige tal, således at alle dennes n-delmængder har samme farve.

Man kan vise, at den udgave af Ramseys sætning, som grafteoretikere kender, er en konsekvens af ovenstående. Se f.eks. Wikipedia for en gennemgang heraf.

Hvorfor så hele denne smøre? Jo, man kan faktisk bruge Ramseys sætning i datalogi til bl.a. at bevise at algoritmer terminerer. Der findes ingen generel strategi i form af en algoritme; det ved vi fra Turing. Men der er nogle bevistaktikker, der ofte dukker op. Ofte bruger man en strategi, hvor man definerer en velordning (\mathbb{O},\sqsubseteq), hvor punktmængden \mathbb{O} typisk er en mængde af tupler af variabelværdier. Derefter definerer man en funktion f : \mathbb{O} \rightarrow \mathbb{O} og viser at f(o) \sqsubset o efter hvert gennemløb af algoritmens hovedløkke. Da \sqsubseteq er en velordning, betyder det at der engang vil blive fundet en minimal o-værdi, og da terminerer løkken. Det bøvlede er her dels at finde frem til en god velordning, dels at finde en god f-kandidat.

Men Cook, Podelski og Rybachenko bruger altså Ramseys sætning til at bevise terminering. Læs deres artikel fra LICS (Logic in Computer Science) eller start med den korte introduktion, som Bill Gasarch har lavet – eller start med at læse indlægget herom på hans blog. Det gjorde jeg selv.

Ramsey nåede ikke at opleve noget som helst af alt dette. Han døde af gulsot få uger inden sin 27-års fødselsdag.

(Visited 102 times, 1 visits today)
Loading Facebook Comments ...

Skriv et svar