Bisimulation in Functional Programming

ProvingCongruenceofBisimulationinFunctionalProgrammingLanguagesDouglasJ.HoweAT&TBellLaboratories600MountainAvenue,Room2B-438MurrayHill,NJ07974,[e-mail]&TBellLaboratories600MountainAvenue,Room2B-438MurrayHill,NJ07974,[e-mail]odforprovingcongruenceofbisimulation-likeequivalencesinfunc-tionalprogramminglanguages.Themethodappliestolanguagesthatcanbepresentedasasetofexpressionstogetherwithanevaluationrelation.WeusethismethodtoshowthatsomegeneralizationsofAbramsky’sapplicativebisimulationarecongruenceswheneverevaluationcanbespeciedbyacertainnaturalformofstructuredopera-tionalsemantics.Oneofthegeneralizationshandlesnondeterminismanddivergingcomputations.iiiProvingCongruenceofBisimulationinFunctionalProgrammingLanguagesDouglasJ.HoweAT&TBellLaboratories600MountainAvenue,Room2B-438MurrayHill,NJ07974,[e-mail]forprovingcongruenceofbisimulation-likeequivalencesinfunc-tionalprogramminglanguages.Themethodappliestolanguagesthatcanbepresentedasasetofexpressionstogetherwithanevaluationrelation.WeusethismethodtoshowthatsomegeneralizationsofAbramsky’sapplicativebisimulationarecongruenceswheneverevaluationcanbespeciedbyacertainnaturalformofstructuredopera-tionalsemantics.Oneofthegeneralizationshandlesnondeterminismanddivergingcomputations.1IntroductionOnewaytoviewafunctionalprogramminglanguageisasanevaluationsystem,whichwedenetobeasetoftermstogetherwithanevaluationrelation.Theintentionisthatatermaevaluatestoanothertermv,writtena)v,ifthereisacomputationstartingwithathatterminateswithresultv.Programequivalenceiscentraltoreasoningaboutfunctionalprograms.Thequestionarisesofwhentwoprogramsinanevaluationsystemaretobeconsideredequivalent.Therearetwopropertiesonemightexpectforareasonableequivalence,atleastwhencomputa-tionisdeterministic.First,iftwoprogramsareequivalentandevaluationofoneofthemterminates(thatis,producesavalue),thensoshouldevaluationoftheother,andthetworesultingvaluesshouldbeequivalent.Second,iftwovaluesvandv0areequivalent,thentheyshouldbothbethesamekindofvalue,and,furthermore,thecomponentsofvandv0shouldbeequivalent.Forexample,ifv=hv1;v2ithenv0shouldbeapairhv01;v02iwithv1equivalenttov01andv2equivalenttov02.Thecasewherevandv0arefunctionsislessclear.Supposev=x:bandv0=x:b0.Inthecaseofthelazy-calculus,itispossibleforacomputationinvolvingvorv0tosubstitute1anytermwhatsoeverforx.Thusifvandv0areequivalent,thenforalltermse,b[e=x]andb0[e=x]shouldbeequivalent.Ifthesepropertiesaretakenasadenitionofprogramequivalence,theninthecaseofthelazy-calculuswegettheapplicativebisimulationofAbramsky1990.Thelazy-calculuscanbeviewedasanevaluationsystemEbytakingthefollowingtworulesasaninductivedenitionofevaluation.f)x:bb[a=x])cf(a))cx:b)x:bApplicativebisimulationcannowbedenedasthesymmetricclosureofthelargestbinaryrelationoverclosedtermssuchthatifaa0anda)x:bthenthereisab0suchthata0)x:b0andforallclosede,b[e=x]b0[e=x].Anequivalentformulation,whichismoresuggestiveofthename\applicativebisimulation,isthefollowing.Saythataconvergesifthereisacsuchthata)c.Thenisthelargestrelationonclosedtermssuchthatifaa0andaconvergesthena0convergesandforallclosede,a(e)a0(e).Usingthisdenitionitistrivialtoverify,forexample,that(x:b)(a)b[a=x],sinceifonesideevaluatestosomevalue,thentheothersideevaluatestothesamevalue.However,inorderforbisimulationtobeausefulprogramequivalence,weneedtobeabletosubstituteequalsforequals.Wecandothisbecausebisimulationisacongruence:ifabandC[]isacontext(atermwithahole)thenC[a]C[b].ThiscanbeprovedusingatechniquefromBerry1981.Thebasicideaistoshowthattwotermsarebisimilarifandonlyiftheyareobservationallycongruent,inthesensethatreplacingonebytheotherinanycontextpreservesobservableresultsofevaluation.ForE,theobservableresultofevaluatingatermissimplythefactthatthetermhasavalue,andsoaandbareobservationallycongruentifandonlyifforallcontextsC[],C[a]convergesandonlyifC[b]does.SimilarproofshavebeendoneformorecomplicatedlanguagesthanE.Theproofsarenotparticularlydicult,buttheyarealldonefromrstprinciplesandinvolvedetailedanalysisofthereductionoftermsthatinvolvecontexts.See,forexample,Talcott1985,Bloom1990andJagadeesan1991.Thispapermakestwomaincontributions.Therstisasimplerandmoregeneralmethodforprovingcongruenceofbisimulation-likeequivalencesforevaluationsystems.Itismoregeneralbecauseitdoesnotrequirebisimulationtobethesameassomeformofobservationalcongruencetowhichtheknowntechniquescanbeapplied.Itissimplerbecauseiteliminatesreasoningaboutcontextsandbecausemostoftheworkinapplyingittoparticularevaluationsystemsandsimulationscanbefactoredoutandcapturedinsomesimpletechnicallemmas.Thesecondcontributionisaformalismforspecifyingevaluationrelationsthatguaranteesthatcertainbisimulation-likeequivalencesarecongruences.ThisformalismisinthegeneralspiritofPlotkin1981andthe\naturalsemanticsofKahn1987.Anevaluationsystemwhoseevaluationcanbedenedusingthisformalismiscalledastructuredevaluationsystem.Section2denes