A Language for the Logical Specification of Proces

ALanguagefortheLogicalSpecicationofProcessesandRelationsLusCairesNovember1996TRUNL-DI-6/96(blankpage)ALanguagefortheLogicalSpecicationofProcessesandRelationsLusCairesDepartamentodeInformaticaUniversidadeNovadeLisboa2825MontedaCaparica,[e-mail]1996AbstractWepresentL,asimplelanguagethatcombinesinanuniformwaythere-ductionandstate-orientedstyleofspecicationexpectedfromaconcurrentprocesscalculus,withthemoredeclarativeandrelationalstyleofspeci-cationusualinlogicprogramming.FortheabstractoperationalsemanticsofLtwopresentationsareprovided,alinearlogicbasedproofsystemandalabelledtransitionsystemspecication.WewillarguethatthepresentformulationofLcancontributetoabetterunderstandingoftherelationbetweenproof-searchandconcurrency.WewillalsoshowthatLisanex-pressivelanguagebothasalogicprogrammingandasaprocessspecicationlanguage.Inparticular,Lcanencodethefullsynchronous-calculusandaversionofthehereditaryHarropformulas.1IntroductionDuetoitsabilitytohandleresourcesinanelycontrolledway,linearlogic[13]wasadoptedasaproof-theoreticfoundationofseverallogicprogrammingandspecicationlanguagesinwhichsomenotionsofstatecanbemodelled,forinstanceLolli[12],Forum[19],Lygon[11]andtheLinearLogicalFrameworkof[8].Besidesthese,someothersystemswerealsoproposedwiththemotivationofallowingthespecicationofconcurrentsystems,prominentexamplesbeingLO[4]andACL[14].Inthiscontext,severalauthors[17,15,14]noticedtheresemblancebetweenThisreportisanextendedandcorrectedversionof[5].1theformsofinteractionarisingamongagentsinprocesscalculilikeCCS[22]and-calculus[23]andthosethatoccuramonglogicalformulasduringbackwardproofconstructioninlinearlogicsequentcalculi.Forinstance,universalquanticationinduceshiding/namecreationandscopeextrusioninaformveryclosetotheoneavailableinthe-calculus,whiledisjunctionisusuallyrelatedtosomenotionofchoice.However,asremarkedin[18],systemslikeACLorLOincorporatesmallsub-setsoflinearlogicorhaveoperationalinterpretationsthatexcludethe\don’tknowsearchbehaviourexpectedfromalogicprogramminglanguage.Forin-stance,LOdoesnotsupportembeddedimplicationsoruniversalquanticationingoals,mechanismsthathavebeenprovenbyMiller(see[16,21],forinstance)tobeveryusefulinexecutablelogicalspecication(forinstance,inmanipulationsofabstractsyntax),whileACLismoreakintoacommittedchoicelanguagewithoutsequentialconjunctions.Ontheotherhand,systemsincorporatinglargersubsetsoflinearlogicorevenfulllinearlogicmustpaytheirexpressivenesswithagreateroperationalcomplexity,asisthecaseoftheForumspecicationlanguage.InthispaperwepresentL,asimplelanguagethatcombinesinauniformwaythereductionandstate-orientedstyleofspecicationexpectedfromaconcurrentprocesscalculuswiththemore\declarativeandrelationalstyleofspecicationusualinlogicprogramming.Accordingly,theabstractoperationalsemanticsofLcanbepresentedsimultaneouslybyalogicaldeductivesystemandbyalabelledtransitionsystemspecication.Thislastpresentationisverynaturalandconvinc-ingforaconcurrentcalculussincethemeaningassignedtothevariousconstructsistheonewewouldexpect;infactitcanbeimmediatelynotedbyinspectionthatLproperlycontainsa(value-passing)-calculus.Moreprecisely,Lcontainsavariantoftheasynchronous-calculus1(aspresentedinsay[2])enrichedwithalimitedformofmixedchoice.WewillshowthatLcandirectlyencodethefullsynchronous-calculuswithmixedchoiceof[23].NotethatPalamidessi[28]hasrecentlyshownthatthesynchronous-calculuswithchoiceisstrictlymoreex-pressivethantheusualversionsoftheasychronous-calculuseveninthepresenceofinputguardedchoice.Ontheotherhand,fromthelogicalviewpoint,thelan-guageofLisanexpressivesubsetoflinearlogic,sinceitcanencoderst-orderhereditaryHarropformulas(fohh)[21],thesubsetofintuitionisticrstorderlogicuponwhichthelanguageProlog[20]isbased.Inasense,Lcanbeseenastheminimalextensionoffohhforwhichanexpressiveconcurrentoperationalin-terpretationcanbeprovided,whereby\expressivewemeanincludingthebasicconstructsofCCSand-calculus.WewillalsoarguethatthepresentformulationofLcancontributetoabet-terunderstandingoftherelationbetweenuniformproof-searchandconcurrency,1Theasynchronous-calculusistherestrictionofthe-calculuswheretheoutputprexformxy:PisonlyallowedwhenPis0.Thismeansthatanagenthasnowaytosynchronisetheactivationofitscontinuationwiththeactualreceptionofamessageithasjustsent.2inparticularbydistinguishingstaticaspects(congruence)fromdynamics(reduc-tion)ofproof-search,andrevealingopportunitiesofparallelismnotonlyontheasynchronoussectionsofproofsbutalsoinbackchaining(focusing)steps.WealsobelievethataconcretelanguagebasedonLcanbegivenareasonablyecientimplementation,sincethecontrolofresourcesharing/acquisitionneededshouldbesimplerthantheI/Omodelsandimprovementsof[12,11,7]neededtohandleunrestrictedoccurrencesofthelinearlogicconjunctiveconnectives(multiplicative)and&(additive).Thestructureofthepaperisthefollowing.InSection2wewillmotivatethedesignofLbyaanalysisoftheprocessinterpretationofuniformproofsearch.InSection4wewillpresentanddiscussatransitionsystemsspecicatio