Fra endelighet til robust programvare

Datamaskiner styrer mye i dagens samfunn, og i noen tilfeller vil en "blåskjerm" være en katastrofe. Vi ønsker å være sikker på at programvaren som styrer en pacemaker eller et fly ikke slår seg av i tide og utide. For å bli virkelig sikker kan vi bevise matematisk at programvaren aldri slår seg av ukontrollert: at den kan fortsette i det uendelige.

Uheldigvis er det komplisert å bevise ting om programvare, så komplisert at vi trenger hjelp av et annet stykke programvare for å hjelpe oss med å holde styr på beviset. Men da trenger vi et begrep om endelighet og uendelighet som datamaskinen kan jobbe med.

Avhandlingen bruker konstruktiv matematikk for å undersøke forskjellige former for endelighet, avgjøre styrkeforhold mellom dem, og bevise nye egenskaper om de forskjellige konseptene.

Konstruktiv matematikk er en gren av matematikk hvor beviser korresponderer med algoritmer, og ved å studere konsepter som endelighet konstruktivt får vi resultater som vi kan tilbakeføre til datamaskinen.

Personalia:

Erik Parmann (1986) er født i Bergen og har en mastergrad fra Universitetet i Bergen (2011).