Proof for Functional Programming

ProofforFunctionalProgrammingToappearin:ParallelFunctionalProgrammingSimonThompsonDraft2{August19981IntroductionInthischapterweexaminewaysinwhichfunctionalprogramscanbeprovedcorrect.Foranumberofreasonsthisiseasierforfunctionalthanforimpera-tiveprograms.Inthesimplestcasesfunctionalprogramsareequations,sothelanguagedocumentsitself,asitwere.Beyondthisweoftenhaveahigher-levelexpressionofproperties,bymeansofequationsbetweenfunctionsratherthanvalues.Wecanalsoexpresspropertieswhichcannotsimplybediscussedforimperativeprograms,usingnotationsforlistsandotheralgebraicdatatypes,forinstance.Apartfromthegeneralobservationthatproofscarryoverdirectlytoim-plicitlyparallelfunctionalsystems,whatistheparticularrelevanceofprooftoparallelfunctionalprogramming?Twoparticularpointsareemphasisedinthischapter.Lazyevaluationgivesinniteandpartialdatastructures,whichcanbeviewedasdescribingthedataowingarounddeterministicnetworksofprocessesCross-referencetoLoogen’sSection3.3.1here.Sec-tion8.3givesaproofthataprocessnetworkproducesthelistoffactorials;thebisimulationmethodusedhereformsalinkwithvericationtechniquesforprocessalgebras,whichgiveadeclarativetreatmentofparallelismandnon-determinismandwhicharesurveyedinSection8.4.Thereisanimportantthreadinthedevelopmentoffunctionalprogram-ming,goingbackatleasttoBackus’FP[2],whicharguesthatitisbesttoeschewexplicitrecursionandtoprogramusingaxedsetofhigher-order,polymorphiccombinators,whicharerelatedtoprogrammingskeletonscross-referencetoskeletons.Thepropertiesofthesecombinatorscanbeseenaslogicallawsinanalgebraofprogramming[4].Theselawscanalsobeseentohaveintensionalcontent,withatransformationfromleft-toright-handsiderepresentingachangeinthecostofanoperation,orintheparallelismimplicittherecross-referencetocostmodelling.ThistopicisexaminedfurtherinSection9.3.1Theequationalmodel,exploredinSection2,givesthespiritoffunctionalprogramverication,butitneedstobemodiedandstrengthenedinvariouswaysinordertoapplytoafullfunctionallanguage.Thepatternofthechapterwillbetogiveasuccessionofrenementsofthelogicasfurtherfeaturesareaddedtothelanguage.Thesewelookatnow.Thedeningformsoflanguagesaremorecomplexthansimpleequations.Section3looksatconditionaldenitions(using‘guards’),patternmatchingandlocaldenitions(inletandwhereclauses)eachofwhichaddscomplications,notleastwhenthefeaturesinteract.Reasoningcannotbecompletelyequational.Weneedtobeabletoreasonbycases,andingeneraltobeabletoprovepropertiesoffunctionsdenedbyrecursion;structuralinductionisthemechanism,anditisdiscussedinSection4andillustratedbyacorrectnessproofforaminiaturecompilerinSection5.Withgeneralrecursion,examinedinSection6andwhichisafeatureofalllanguagesinthecurrentmainstream,comesthepossibilityofnon-terminationofevaluation.Inalazylanguagegeneralrecursionhasthemoreprofoundeectofintroducinginniteandpartiallistsandotherdatastructures.Inbothlazyandstrictlanguagesthispossibilitymeansinturnthatinin-terpretingthemeaningofprogramsweareforcedtointroduceextravaluesateachtype.Thisplainlyaectsthewayinwhichthelogicisexpressed,anditsrelationtofamiliarpropertiesof,say,theintegers.ThebackgroundtothisisexploredinSection7.Section8givesanoverviewofthetwoprincipalapproachestogivingmean-ingstoprograms{denotationalsemanticsandoperationalsemantics{andtheirimplicationsforprogramverication.Aproofofcorrectnessforafunctiondenedbygeneralrecursionexempliesthedenotationalapproach,whilstop-erationalsemanticsunderpinsaproofthatalazyprocessnetworkgeneratesthelistoffactorials.Thislastproofformsalinkwiththeprocessalgebraapproachtoparallelism,whichisalsodiscussedinthissection.Becauseofthecomplicationswhichnon-terminationbrings,therehasbeenrecentinterestinterminatinglanguagesandtheseareintroducedinSection9.OfparticularrelevancehereisthetransformationalapproachofBackus,Birdandothers.Afully-edgedlanguagewillallowuserstointeractwiththeenvironmentinvariousways,butatitssimplestbyreadinginputandwritingoutput.Thisissupportedinavarietyofways,includingtheside-eectingfunctionsofStandardMLandthemonadsofHaskell1.4.SMLalsoallowsmutablereferencesandexceptions.Inthischapterwecoveronlythepurepartsoflanguages,butreferreadersto[6]foraperspicaciousdiscussionofprogramvericationforvariousformsofinput/outputincludingmonadicIO.RecentworkonmodellingSML-stylereferencescanbefoundin[15].Thischapterdoesnottrytoaddressalltheworkonvericationofparallelimperativeprograms:Sections8.9and8.10oftheexhaustivesurvey[5]morethandojusticetothistopic,andputitinthecontextofimperativeprogramver-icationingeneral.Ontheotherhand,linkswithprocessalgebraareexaminedinSection8.4.22Thebasisoffunctionalprogramming:equa-tionsInthissectionweexaminethebasisoffunctionalprogrammingandshowhowthedenitionsofasimplefunctionalprogramcanbeinterpretedaslogicalequations.Anexaminationofhowthisapproachcanbemodiedandextendedtoworkingeneralformsthemainpartofthechapter.Afunctionalprogramconsistsofacollectionofdenitionsoffunctionsandothervalues.AnexampleprogramusingthenotationoftheHaskelllanguage[14]istest::Integertest=42id::a-aidx=xplusOne::Inte