Feit, Thompson – og Microsoft

20121014-104320.jpg

For snart en del år siden havde jeg et kort besøg af Douglas Bridges fra Canterbury University i New Zealand, og han gav et spændende seminar om konstruktiv matematik. Det pudsige var, at de mange matematikere, der var til stede, ikke kendte til denne retning. Alle, der beskæftiger sig med matematik, ved at der er forskel på konstruktive og ikke-konstruktive beviser. Konstruktive beviser kræver at man beviser eksistentielle påstande (“Der findes en x således at…”) ved en konstruktion (dvs. som del af beviset konstruere dette x).men for det meste bliver det ved dét.

Intuitionistisk matematik er den gren af konstruktiv matematik, der er baseret på L.E.J. Brouwers matematikfilosofi. En helt cental indsigt her er forbindelsen til den typede lambda-kalkyle. Denne forbindelse gør bl.a. at bevistjek (dsv. undersøgelse af om bevisreglerne i et formelt bevis er anvendt korrekt) præcist svarer til typetjek, og en konstruktion svarer til en term i den typede lambda-kalkyle. dvs. til et program. Derfor blev intuitionisme interessant for teoretisk datalogi og for knap 30 år siden, da man var godt i gang med at forstå hvordan typede lambdakalkyler kan bruges som basis for funktionsorienterede programmeringssprog (med ML som tidligt eksempel) gik jagten ind på at lave software, der baseret på intuitionistisk typeteori kan formalisere og tjekke matematiske teorier. Blandt de vigtige bedrifter er det arbejde, Thierry Coquand m.fl. har udført med bevisassistenten Coq, der er baseret på typeteorien Calculus of Constructions. En hel masse klassiske resultater er allerede blevet tjekket – så matematikstuderende på bachelorniveau kan tage det roligt. Men også beviset for den berømte firefarvesætning fra grafteori er blevet tjekket, og dette imponerende resultat skyldes Georges Gonthier fra INRIA Microsoft Research i Cambridge (et samarbejde mellem det franske forskningslaboratorium INRIA og Bill Gates & Co.). Det er Gonthier, man ser på billedet ovenfor.

Nævnes skal også det arbejde, der pågår med at bruge bevisassistenten Isabelle. En af mine gamle specialestuderende Palle Raabjerg gør dette som helt central del af sit PhD-arbejde om nominelle proceskalkyler. Min egen fornemmelse er at beviser inden for teoretisk datalogi går mod at blive systematisk tjekket med sådanne bevisassistenter (og jeg lover, at jeg selv nok skal begynde på det en dag…)

I dag kom så det seneste resultat. Igen var det Georges Gonthier der var på banen. Han har denne gang sammen med sin forskningsgruppe og kolleger andre steder formaliseret beviset for Feit-Thompsons sætning. Det tog dem seks år.

Denne sætning siger at enhver endelig simpel gruppe af ulige orden er løsbar. Med G løsbar menes, at der findes en følge af undergrupper

1 \leq G_1 \leq \ldots G_k = G

(hvor 1 er den trivielle gruppe) således at \leq er undergruppe-ordningen og så G_{i-1} er normal i G_i og G_{i+1}/G_{i} er abelsk for alle 1 \leq i < k[/latex]. Sætningen var vigtig i jagten på et bevis for Burnsides formodning, nemlig at enhver ikke-abelsk endelig simpel gruppe vil være af lige orden. Vi har mao. at gøre med klassifikationen af de endelige simple grupper, der er et fascinerende emne inden for det 20. århundredes matematik. De simple grupper er gruppeteoriens "primtalsbegreb" – en gruppe er simpel, hvis dens eneste normale undergrupper er gruppen selv eller [latex]1[/latex]. For dem, der beskæftiger sig med formalisering af matematiske teorier, er Feit-Thompsons sætning interessant, fordi dens bevis er så stort og besværligt. Det fyldte faktisk en hel udgave af Pacific Journal of Mathematics, startende på side 775 og sluttende på side 1029. Derfor er det en udfordring for formaliseringen at forstå bevisets struktur og selvfølgelig også at debugge det.

Se mere på http://www.msr-inria.inria.fr/Projects/math-components/feit-thompson.

De mange resultater inden for formaliseret matematik viser, at konstruktiv matematik ikke er nogen tosset tilgang, Nogle synes at der er tale om at lave matematik med den ene hånd bundet på ryggen, når man f.eks. ikke kan bruge indirekte beviser, men fordelene i form af muligheden for systematiske bevistjek er tydelige.

Beviset er også interessant, fordi det er med til at vise forbindelsen mellem matematisk aktivitet og softwareudvikling — det store stykke Coq-kode (ca. 170.000 linjer) er jo et stykke software —og måske dermed også være med til at gøre noget ved den fornemmelse, mange lægfolk (og en del studerende) har af at matematik (og vel forskningsaktiviteter i det hele taget) er noget, der foregår “pr. øjemål”. For sådan er det ikke — der er tværtimod tale om en blanding af nødvendige aha-oplevelser og forudsigelige, men lige så nødvendige systematiske skridt.

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

4 kommentarer til “Feit, Thompson – og Microsoft”

Skriv et svar