Detta forskningsprojekt kommer att fördjupa vår matematiska förståelse av rekursion, det vill säga ett programs förmåga att upprepa sig under beräkning. Rekursion gör det möjligt för oss att lösa beräkningsuppgifter genom att bryta ner dem i enklare men liknande deluppgifter, en väsentlig källa till beräkningskraft i programmeringsspråk.
Att behärska rekursion är nyckeln till att lösa problem inom komplexitetsteorin, såsom det berömda P vs NP-problemet: är varje beräkningsuppgift med en effektivt verifierbar lösning också effektivt lösbar? Att närma sig svaret på denna fråga är inte bara av stor teoretisk betydelse, det skulle också direkt påverka många aspekter av det moderna digitala samhället. Säkerheten i dagens banksystem, till exempel, är avgörande beroende av den algoritmiska svårigheten att knäcka kommunikationsprotokoll med asymmetrisk kryptering.
Trots sin centrala roll har rekursion betraktats som en "magisk låda", en primitiv odelbar princip som inte kan analyseras ytterligare. Dessa begränsningar kan dock kringgås tack vare en nyligen utvecklad generalisering av matematiska bevis kallade "cykliska bevis", vilka kan uttrycka rekursion och själviteration genom cirkulär argumentation.
Baserat på sökandens preliminära forskningsresultat syftar det föreslagna projektet till att utveckla ett enhetligt ramverk för att undersöka rekursion genom cykliska bevis. Det föreslagna forskningsprogrammet spänner över många områden inom matematik och datavetenskap och syftar till att ytterligare stärka dess tvärvetenskapliga natur med tillämpningar av cykliska bevis inom programvaruutveckling och formell verifiering.
