欢迎来到天天文库
浏览记录
ID:40881304
大小:1.75 MB
页数:18页
时间:2019-08-09
《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
此文档下载收益归作者所有