Notes on P-Algebra (4) Algebra over Process Struct

ISSN1361-6161ComputerScienceUniversityofManchesterNotesonP-Algebra(4):AlgebraoverProcessStructure,PartI.KoheiHondaDepartmentofComputerScienceUniversityofManchesterTechnicalReportSeriesUMCS-95-12-5NotesonP-Algebra(4):AlgebraoverProcessStructure,PartI.KoheiHondaDepartmentofComputerScienceUniversityofManchesterOxfordRoad,Manchester,[e-mail]17,1995Copyrightc1995.Allrightsreserved.Reproductionofallorpartofthisworkispermittedforeducationalorresearchpurposesonconditionthat(1)thiscopyrightnoticeisincluded,(2)properattributiontotheauthororauthorsismadeand(3)nocommercialgainisinvolved.RecenttechnicalreportsissuedbytheDepartmentofComputerScience,ManchesterUniversity,areavailablebyanonymousftpfromftp.cs.man.ac.ukinthedirectorypub/TR.ThelesarestoredasPostScript,incompressedform,withthereportnumberaslename.TheycanalsobeobtainedonRefereedby:CliJonesAbstractWedeveloptheoryofalgebraoverprocesses,basedonanabstracttreatmentofprocessstructure.Theabstractframeworkofprocessstructuresisdeveloped(PartI),and,onitsbasis,theoryofalgebraisdevelopedwherethebasicresultsincludingBirkho-likeVarietyTheoremareproved(PartII).Wealsodiscusspropertiesofsignicantconcreteexamplesofalgebras,takenfromextanttheoriesofconcurrency.PartIdevelopstheabstracttheoryofprocessstructureencompassingawiderangeofstructuresforprocesstheoryincludingconcretestructureswehavediscussedintheprecedingnotes.ThetheoryisusedasfoundationsofthealgebraicdevelopmentinPartII,andisinterestinginitsownright.1IntroductionTheaimofthepresentnotesistwo-fold.Therstaimistodevelopanotionofalgebraoverprocessstructurestogetherwithanappropriatesystemofnotations.Theabstractframeworkofthetheoryofalgebrafairlyfollowstheusualcategoricaltreatmentof\alge-brainacategorywiththecategoryofprocessstructureandp-mapsastheunderlyingcategory.Thenewpointshoweverlieintheconcreterepresentationofgeneralnotionslikehomomorphismsinthesettingofprocessstructure,aswellasbasicdierencesinseveralconstructionssuchasquotientandotherconstructions.Suchdierencesneces-sitateanewnotationforpresentingalgebraicnotions.Thetheory,whichtreatsstaticaspectofmanipulationofpureprocesses,willbecomethebasisoftreatmentofprocessdynamics,tobedevelopedinthesubsequentnotes.Thesecondaimconcernstheframeworkinwhichthesenotionsandresultsarepre-sented.WedeveloptheoryofalgebrainanabstractframeworkunlikeintheprecedingNotes[7,8,9].Thus,ratherthanrelyingonconcreteconstructionofpermutationgroupsandpartialinjectionsovernitesets,webaseourdevelopmentonapairofcategoriesconformingtocertainconditions,bywhichallessentialresultsandconstructionsoftheprecedingnotesareguaranteed.Forthedevelopmentoftheoryofalgebra,thisresultsinclarityofpresentationofthenotionsandtheproofs.Theapproachisalsoimpor-tantwhenweneedtoextendthenotionofprocessesbeyondwhathasbeenstudiedintheprecedingstudyofconcurrencysofar,cf.Examples2.19.Ourprimarypurposeinthispaperhoweverliesinexploitationoftheabstractframeworkforlucidpresentation,leavingdeeperstudyofsuchpossibilityelsewhere.Thenotesaredividedintotwoparts.PartIgivesabstracttheoryofprocessstructure,whichwillbeusedinPartIIandalsointhesubsequentNotes.Thetreatmentofthetheoryisself-contained.PartIIisdevotedtothedevelopmentofelementarytheoryofalgebra.IntherestofPartI,Section2presentsthefoundationalstructuresoftheab-stracttheorycalledConnectionDomains,whichgivesarelationalalgebraofconnectionsamongprocessesinacategoricalframework.Section3thenstudiesanabstracttheoryofprocessstructurebasedonconnectiondomains.Byvaryingtheunderlyingconnectiondomain,quitedierentkindsof\processstructuresarise(includingthefamiliarnotionofsetsthemselves),eachofwhichareshowntoinduceaset-liketheoryaswedeveloped1intheprecedingNotes.AllthemainresultsofNotes1and3areestablishedinthisabstractsetting,purelyrelyingontheabstractalgebraofconnections.Surprisingly,thegeneralityresultsinmuchshorterandmorelucidproofsthanthoseoftheprecedingNotes.Acknoweldgemensts.TheauthorthanksCliJonesforaseriesofenlighteningdis-cussionsandencouragement.HethanksPeterAczelforstimulatingdiscussionswhichdeepenedhisunderstandingonthesubject.TheauthorgratefullyacknowledgesthesupportofanEPSRCVisitingFellowship.2ConnectionDomainInfunctionsorrelationsoveraset,someelementsofasetarerelatedtosomeelementsofaset.Thewaytorelateanelementtoanotherelementisquitesimple:wejusttakeatupleoftwoelements.Inthetheoryofprocesses,thissimpleschemeisnolongervalid.Twoprocesses(correspondingtotwoelements)mayberelatedindiverseways,consideringhowinterfacepointsofprocessesareconnectedtoeachother.Thiswasimplicitinthestudyofprocessalgebra[11,6],embodiedinthenotionoffreenames,orstudyofcompositaanditsgeneralisations[2,3,13],embodiedinthenotionof\variables(of,say,openterms),andismadeexplicitbythestudyofprocessstructure[7],aswellasbysuchworksas[1,5,12].Specicallywhat[7]showedisthatacoherenttheoryofmapsandrel