Strikthetsanalys

Inom datavetenskap hänvisar strikthetsanalys till varje algoritm som används för att bevisa att en funktion i ett icke-strikt funktionellt programmeringsspråk är strikt i ett eller flera av sina argument. Denna information är användbar för kompilatorer eftersom strikta funktioner kan kompileras mer effektivt. Således, om en funktion visar sig vara strikt (med användning av strikthetsanalys) vid kompilering, kan den kompileras för att använda en mer effektiv anropskonvention utan att ändra innebörden av det omslutande programmet.

Observera att en funktion f sägs divergera om den returnerar $\{\bot \}$ : operativt skulle det innebära att f antingen orsakar onormal avslutning av det omslutande programmet (t.ex. fel med ett felmeddelande) eller att den loopar oändligt. Begreppet "divergens" är signifikant eftersom en strikt funktion är en som alltid divergerar när den ges ett argument som divergerar, medan en lat (eller icke-strikt) funktion är en som kan eller inte kan divergera när den ges ett sådant argument. Strikthetsanalys försöker bestämma "divergensegenskaper" för funktioner, vilket således identifierar vissa funktioner som är strikta.

Tillvägagångssätt för strikthetsanalys

Framåt abstrakt tolkning

Strikthetsanalys kan karakteriseras som en framåtriktad abstrakt tolkning som approximerar varje funktion i programmet med en funktion som avbildar argumentens divergensegenskaper till resultatens divergensegenskaper. I det klassiska tillvägagångssättet som var banbrytande av Alan Mycroft använde den abstrakta tolkningen en tvåpunktsdomän där 0 betecknar mängden $\{\bot \}$ betraktad som en delmängd av argumentet eller returtypen, och 1 betecknar mängden alla värden i typen.

Efterfrågeanalys

Glasgow Haskell Compiler (GHC) använder en bakåtriktad abstrakt tolkning som kallas efterfrågeanalys för att utföra strikthetsanalys såväl som andra programanalyser. I efterfrågeanalys modelleras varje funktion av en funktion från värdekrav på resultatet till värdekrav på argumenten. En funktion är strikt i ett argument om ett krav på dess resultat leder till ett krav på det argumentet.

Projektionsbaserad strikthetsanalys

Projektionsbaserad strikthetsanalys, introducerad av Philip Wadler och RJM Hughes , använder strikthetsprojektioner för att modellera mer subtila former av strikthet, såsom huvudstrikthet i ett listargument. (Däremot kan GHC:s efterfrågeanalys bara modellera strikthet inom produkttyper, dvs. datatyper som bara har en enda konstruktor .) En funktion $f$ anses vara strikt om $f= f\circ \pi$ , där $\pi$ är projektionen som huvudutvärderar dess listargument.

Det fanns en stor mängd forskning om strikthetsanalys på 1980-talet.