Precise and expressive mode systems for typed logi

PreciseandExpressiveModeSystemsforTypedLogicProgrammingLanguagesDavidOvertonSubmittedintotalfulfilmentoftherequirementsofthedegreeofDoctorofPhilosophyDecember2003DepartmentofComputerScienceandSoftwareEngineeringTheUniversityofMelbourneVictoria3010,AustraliaAbstractInthisthesiswelookatmodeanalysisoflogicprograms.Beingbasedonthemathematicalformalismofpredicatelogic,logicprogramshavenoapriorinotionofdataflow—asinglelogicprogrammayruninmultiplemodeswhereeachmodedescribes,orprescribes,apatternofdataflow.Amodesystemprovidesanabstractdomainfordescribingtheflowofdatainlogicprograms,andanalgorithmforanalysingprogramstoinferthemodesofaprogramortocheckthecorrect-nessofmodedeclarationsgivenbytheprogrammer.Suchananalysiscanprovidemuchusefulinformationtothecompilerforoptimisingtheprogram.Inaprescriptivemodesystem,modeanalysisisalsoanimportantpartofthesemanticanalysisphaseofcompilation(muchliketypeanalysis)andcaninformtheprogrammerofmanyerrorsorpotentialerrorsintheprogramatcompiletime.Wethereforebelieveitisanessentialcomponentofanyindustrialstrengthlogicprogrammingsystem.Ouraimistodevelopastrongandprescriptivemodesystemthatisbothaspreciseandexpressiveaspossible.WebelievethisrequiresastronglytypedandpurelydeclarativelanguageandsowefocusonthelanguageMercury.ThefirstcontributionofourworkistogiveadetaileddescriptionofMercury’sexistingmodesystem,whichisbasedonabstractinterpretation.Althoughmostofthissystemhasbeenaroundforseveralyears,thisisthefirsttimeithasbeendescribedinthislevelofdetail.Thisisalsothefirsttimetherelationshipofthemodesystemtotheformalismofabstractinterpretationhasbeenmadeclear.Followingthat,welookatwaysofextendingthemodesystemtoprovidefurtherprecisionandexpressiveness,andtoovercomesomeofthelimitationsofthecurrentsystem.Thefirstoftheseextensionsistosupportaformofconstrainedparametricpolymorphismformodes.Thisisanalogoustoconstrainedparametricpolymorphictypesystemssuchastypeclasses,andaddsasomewhatsimilardegreeofexpressivenesstothemodesystem.Nextwelookatamethodforincreasingtheprecisionofthemodeanalysisbykeepingtrackofaliasesbetweenvariables.Theincreasedprecisionwegainfromthisallowsanincreaseinexpressivenessbyallowingtheuseofpartiallyinstantiateddatastructuresandmorecomplexuniquenessannotationsonmodes.ThefinalareawelookatisanalternativeapproachtomodeanalysisusingBooleanconstraints.Thisallowsustodesignamodesystemthatcancapturecomplexmodeconstraintsbetweenvariablesandmoreclearlyseparatesthevarioustasksrequiredformodeanalysis.Webelievethatthisconstraint-basedsystemprovidesagoodplatformforfurtherextensionoftheMercurymodeiiiAbstractsystem.TheworkwedescribehasallbeenimplementedintheMelbourneMercurycompiler,althoughonlyconstrainedparametricpolymorphismhassofarbecomepartofanofficialcompilerrelease.DeclarationThisistocertifythat(i)thethesiscomprisesonlymyoriginalworktowardsthePhDexceptwhereindicatedinthePreface,(ii)dueacknowledgementhasbeenmadeinthetexttoallothermaterialused,(iii)thethesisislessthan100,000wordsinlength,exclusiveoftables,maps,bibliographiesandappendices.DavidOvertonDecember2003iiiivDeclarationPrefaceThisthesiscomprises7chapters,includinganintroductionandconclusion.Followingtheintro-duction,Chapter2providesthebackgroundandnotationnecessarytounderstandtherestofthethesis.Chapter3presentsthemodeanalysissystemasitiscurrentlyimplementedintheMelbourneMercurycompiler.Chapter4presentsextensionstothemodesystemtoallowmodepolymorphism.Chapter5describesanextensiontothemodesystemtokeeptrackofdefinitealiases.Chapter6presentsanewapproachtomodeanalysisusingBooleanconstraints.Finally,Chapter7containssomeconcludingremarks.ThemodesystemdescribedinChapter3wasdesignedandimplementedbyFergusHendersonandothers,howeverthenotationfortheformalisationofthesystemwhichispresentedinthisthesisisentirelymyownwork.Section5.3isbasedonresearchpartofwhichwascarriedoutjointlywithAndrewBromage.Ithasnotpreviouslybeenpublished.Section5.4isbasedonpartofRoss,Overton,andSomogyi[117].Chapter6isbasedonOverton,Somogyi,andStuckey[111],howevermostofthematerialdescribingtheimplementationisnew.vviPrefaceAcknowledgementsThisresearchhasbeenmadepossiblebythefinancialsupportoftheCommonwealthofAustraliaintheformofanAustralianPostgraduateAward.Iwouldliketothankmysupervisor,ZoltanSomogyi,andtheothermembersofmyadvisorycommittee,LeeNaishandHaraldSøndergaard,fortheiradviceandsupportthroughoutmyPhDcandidature.ThankyoualsotoAndrewBromage,PeterRossandPeterStuckeywithwhomIhavecollaboratedonvariouscomponentsoftheresearchpresentedhere.ThankyoutoPeterSchachteforprovidingtheROBDDpackagewhichIusedforimplementingtheworkofChapter6.ThankyoutomyverygoodfriendTomConway,withoutwhoseencouragementIneverwouldhavegotinvolvedintheMercuryprojectorstartedaPhD(don’tworry,Tom,I’veforgivenyou).ThankyoutoFergusHendersonwhoseextremelythoroughcodereviewshelpedgreatlytoimproveboththisresearchanditsimplementation.TotherestoftheMercuryteam,RalphBecket,MarkBrown,SimonTaylor,DavidJefferyandTysonDowd,ithasbeengreatworkingwithallofyou.Ihavelearntagreatdealaboutlogicprogramming,languagedesignandsoftwareengineeringinm