På jakt efter buggar i datorprogram

Jacopo Emmenegger, som disputerade i matematik vid Stockholms universitet 2019, har erhållit en postdoktoral tjänst hos professor Giuseppe Rosolini, vid Università di Genova, Genua, Italien.

När vi numera alltmer förlitar oss på datorerna, hur ska vi kunna bedöma om deras mjukvara är korrekt? För att kunna verifiera datorprogrammen håller nya verktyg på att utvecklas inom den matematiska logiken. Ett system för att säkerställa att datorprogrammet gör vad det är meningen att det ska göra är Beroende typteori, som introducerades på 1970-talet av den svenska logikern Per Martin-Löf. 

Den första typteorin utvecklades långt före datorernas tid, i början av 1900-talet av den brittiska matematikern och filosofen Bertrand Russell. I sina försök att skapa gemensamma grundvalar för all matematik stötte han på paradoxer, bland andra den berömda Russellparadoxen; i en klassisk version av den säger en man från Kreta att alla från Kreta alltid ljuger. 

Senare utvecklades typteorierna till strikt formella system användbara till att bland annat studera programmeringsspråk. Beroende typteori är dock ganska invecklad att handskas med. Ett steg att underlätta hanteringen togs för cirka tio år sedan, då den framstående matematikern Vladimir Voevodsky utökade den beroende typteorin med en ny princip – univalensaxiomet. För att detta axiom ska vara användbart till att verifiera datorprogram måste dess beräkningsmässiga innehåll kunna undersökas. 

Jacopo Emmenegger kommer i sitt projekt att testa i vilken mån univalensaxiomet är beräkningsbart med hjälp av så kallade realiserbarhetsmodeller. Modellerna bygger på en abstrakt version av Turingmaskiner, de tidigaste och mest studerade beräkningsmodellerna. Turingmaskiner kan ses som en samling instruktioner för att läsa och skriva ettor och nollor på en remsa, och på så sätt är de en abstrakt version av moderna datorprogram. För att kunna fastställa om det går att genomföra beräkningar med den beroende typteorin som utökats med univalensaxiomet behöver man hitta en realiserbarhetsmodell där varje term i typteorin svarar mot en Turingmaskin. Projektet förenar på så sätt två av de viktigaste metoderna inom dataprogrammering: typteori och realiserbarhet.

Foto: Ota de Leonardis