Closures and fairness in the semantics of programming logic

《Closures and fairness in the semantics of programming logic》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、TheoreticalComputerScience29(1984)167-184167North-HollandCLOSURESANDFAIRNESSINTHESEMANTICSOFPROGRAMMIN~JLOGIC*J.-L.LASSEZANDM.J.MAHERDepartmwofComputerScience,UniversityofMelbourne,Parkville,Victoria,3052,AustraliaCommunicatedbyJ,.MannaReceivedNovember

2、1982RevisedMay1983Abstract.tVeusethenotionsofclosuresandfairchaoticiterationstogiveasemanticstologicprograms.Therelationshipsbetweenthesemanticsc;findividualrulesandthesemanticsofthewholeprogramareestablishedandanapplicationjtoparallelprocessingismenti

3、oncti.Achaoticfixedpointtheoremisgiven.whichcarriesthenon-determinisminherenttoresolution.Finally.veintroduceageneraldefinitionoffinitefailureandtheconceptoffairSLDresolution,andshowthatthisprocedureissoundandstronglycompletewithrespecttobothsuccessan

4、dfinitefailure.thusextendingaresultofAptandVanEmden(1982).Keywords.Logicpro~ram:iung,csemantics.chaoticiterations.SLDresolution.finitefailure,PROI.CX.1.IntroductionVanEmdenandKobvalski[IS]gaveveryelegantsimplefixedpointandmodel-theoreticsemanticsforlog

5、icprogramsindefiniteclausalform.AptandVanEmden[I]furtherexploitedfixedpointtechniquestoestablishthesoundnessandcomplzte-nessofSLDresolutionwithrespecttosuccessandtocharacterizeSLDfinitefailure.Thesetwopaperswhichgivetheformalsemanticsofwhatcouldbecalle

6、dpunIWXOC;havebeenwidelycitedintheliterature.P.CousotandR.Cousotinalongseriesofpapers(see[6]forabibliography)haveusedthenotionsofclosureandchaoticiterationstoestablish,inparticular,formalmodelsofglobaldataflowanaiysis.Takingaslightlydifferentapproachfr

7、omVanEmdenandKowalskisweconsideralogicprogramtoconsistonlyofinferencerules,theaxiomsbeingconsideredasinput.Thefunction[P]representingthesemanticsoftheprogramisthentheclosure(idempotent,increasing)ofthefunction[R]representingthesemanticsoftheiules.Thisc

8、losurepropertyallowsustousethetechniquesofCousotandCousot.Furtherclassicalfixedpointtheoremscanthenbeadaptedtoprovidesimplealgebraiccharacterizationsinthesemanticsoflogicprogramming.*ResearchsupportedbytheAustralianComputerResearchBoard