Hvad gør du, hvis du skal være sikker på, at din kode virker?

Kernespørgsmålet i det felt jeg arbejdede med, afhængig typeteori, er som følger: Hvad gør du, hvis du skal være sikker på, at din kode virker? Ikke sikker i specifikke scenarier, men matematisk sikker på at for alle mulige inputs til programmet produceres et output, som følger kravspecifikationen. Et muligt svar i den situation er at benytte afhængig typeteori.

Typeteori er et logisk sprog, som kan bruges både som fundament for matematik og et programmeringssprog. Specifikt svarer en typeteori til et funktionelt sprog med stærke typer, der kommer med en række automatiske garantier om programmer skrevet i sproget. Udover disse indbyggede garantier kan man med afhængig typeteori skrive specifikationer af programmer i typeteorien selv, ved at benytte sig af det som logisk sprog. Man kan så matematisk bevise, at et program implementerer en specifikation med både program, bevis og specifikation skrevet i det samme sprog.

Afhængig typeteori har to begrænsninger: den ene som logik og den anden som programmeringssprog. Det logiske problem kan løses med Cubical Type Theory (CTT), og problemet på programmeringssiden kan løses med Clocked Type Theory (CloTT). I artiklen kombineres de til Clocked Cubical Type Theory (CCTT), som med Højere Induktive Typer (HITs) bliver et ekspressivt programmeringssprog med en hensigtsmæssig logik.

Rum

Den logiske begrænsning i afhængig typeteori er dens håndtering af lighed, hvilket må siges at være kernen i enhver logik. Hvis vi eksempelvis tænker på hvilke funktioner, der skal være lig hinanden, er der en beslutning at tage. Vil vi gøre det muligt at skelne funktioner, som er defineret på forskellige måder, men producerer det samme output? Måske er vi interesserede i en logik, hvor funktioner der tager lige lang tid at køre altid er lig hinanden, uanset input og output, så vi kan bruge den til at beskrive ressourceforbrug i et system. Et udbredt valg er ikke at skelne mellem funktioner, som giver det samme output for alle inputs. Dette valg, funktionel ekstensionalitet, er kritisk, når man bruger typeteorien som logik til at ræsonnere om funktioner på kravspecifikationsniveauet. Her er vi nemlig udelukkende interesserede i, hvad vores program rent faktisk gør. Lighedsbegrebet er altså en central del af en logik, som afgør hvilke situationer, en logik kan beskrive.

Afhængig typeteori i sin moderne form låner fra det matematiske felt homotopi teori. Lighed i homotopi teori har en geometrisk fortolkning: De objekter man arbejder med er, løst sagt, geometriske objekter og to punkter i en form siges at være lig hinanden, hvis man kan tegne en linje fra det ene punkt til det andet indenfor formen. Det kan umiddelbart virke ret abstrakt, at man skal tænke på for eksempel typen af programmer, der producerer et tal som en geometrisk form. At bruge geometriske stier som lighedsbegreb har dog mange gode konsekvenser. Udover at opfylde de ting man normalt kræver af lighed, kan man for eksempel bevise, at den understøtter funktionel ekstensionalitet.

Tid

For de fleste indeholder definitionen af ’programmeringssprog’ Turing-komplethed, hvilket løst sagt betyder ’alt hvad en computer kan’. Typeteori som programmeringssprog er ikke som udgangspunkt Turing-komplet, da det mangler generel rekursion, altså muligheden for at definere en funktion som kalder sig selv. Grunden til at dette ikke er en del af standardpakken for typeteori er, at generel rekursion giver mulighed for at bevise alle udsagn i logikken, og dermed forhindrer os i at bruge teorien som en matematisk logik.

Guarded recursion er en måde at tillade rekursive definitioner uden at muliggøre de patologiske beviser af logiske udsagn. Her bruges et redskab fra modal logik for at beskrive rekursion ved at tilføje en eksplicit markering i sproget af, at det rekursive kald skal ske ’senere’. Dette tilføjer en måde for sproget at holde styr på hvilken rækkefølge forskellige opgaver bliver udført, og det kan dermed forhindre at en udregning skal bruge resultatet fra et program, som først bliver kørt senere.

Verifikation af kritisk software

Guarded recursion og CTT eksisterede før mit arbejde, og de har endda været kombineret før på forskellige måder. Forskellen på de eksisterende systemer, og det der er beskrevet i artiklen, er den konkrete behandling af koinduktive typer. Det er nemmest at forstå forskellen i et eksempel.

Den ærketypiske koinduktive type er en strøm af input – for eksempel en temperaturmåling fra en atomreaktor hvert sekund. For at forstå programmer som afhænger af en sådan strøm af inputs, bruger vi en koinduktiv strøm af tal. De koinduktive programmer kommer automatisk til at være produktive. Det er groft sagt en garanti for, at programmet altid vil producere sit output baseret på en temperaturmåling i endelig tid.

Der hvor koinduktion bliver vigtigt, er i specifikationsprocessen. Tidligere systemer havde andre og strengere begrænsninger på, hvilke informationer de havde adgang til om deres programmer. Specifikt var det ikke muligt at sammenligne programmer, som opdaterer efter hver temperaturmåling, og dem der aggregerer data fra for dagens forløb, på trods af at de kan være funktionelt ens.

Udover dette har vi udvidet systemet med de såkaldte HITs. Et simpelt eksempel på en induktiv type er lister. I typeteori tænker man på lister som være bygget op fra en tom liste ved at tilføje elementer. Vi har altså to måder at lave en liste. Enten kan vi tage den tomme liste, eller også kan vi tilføje et element til en eksisterende liste. Sæt nu at vi ikke bekymrede os om rækkefølgen på de objekter, vi har i vores liste. Vi mener altså, at i logikken skal man se [a,b] og [b,a] som ens, hvilket for os betyder, at der skal være en sti mellem de to lister. Det er der ikke nogen måde at gøre i den induktive type af lister, men med en højere induktiv type kan en sådan sti indsættes manuelt. Situationen ville så være, at man havde tre måder at lave en liste på: den tomme, sammensætninger som før og nu en liste som befinder sig på stien mellem [a,b] og [b,a].

Perspektivernes grundforskning er lange, og vi er nogle år fra at have et implementeret programmeringssprog baseret på CCTT, men artiklen har givet en retning at arbejde i.

Det brede perspektiv i artiklens indhold er, at vi nu tilføjer en af de vigtigste egenskaber ved typeteori til systemet: Evnen til at definere nye typeformere on-the-fly. Hvis du har et problem som kan løses matematisk med koinduktion, kan det formentlig beskrives i artiklens system, og dermed retfærdiggøres matematisk.


Læs den fulde artikel her.