资源描述：
《FULLY ABSTRACT SEMANTICS FORO BSERVABLY SEQUENTIAL LANGUAGES》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、FULLYABSTRACTSEMANTICSFOROBSERVABLYSEQUENTIALLANGUAGESRobertCartwrightPierre-LouisCurienMatthiasFelleisenDepartmentofComputerScienceRiceUniversityHouston,TX77251-1892AlsoappearedinInformationandComputation1994RiceUniversityTechnicalReport#93-219Minorrevisions:July2003FULLYABSTRACTSEMANTIC
2、SFOROBSERVABLYSEQUENTIALLANGUAGESRobertCartwright∗DepartmentofComputerScience,RiceUniversity,Houston,TX77005Pierre-LouisCurien†EcoleNormaleSup´erieure,LIENS-CNRS,45rued’Ulm,75230Paris,FranceMatthiasFelleisen‡DepartmentofComputerScience,RiceUniversity,Houston,TX77005AbstractOneofthemajorch
3、allengesindenotationalsemanticsistheconstructionofafullyabstractsemanticsforahigher-ordersequentialprogramminglanguage.Forthepastfifteenyears,researchonthisproblemhasfocusedondevelopingasemanticsforPCF,anidealizedfunctionalprogramminglanguagebasedonthetypedλ-calculus.Unlikemostpracticallan
4、guages,PCFhasnofacilitiesforobservingandexploitingtheevalu-ationorderofargumentstoprocedures.Sincewebelievethatthesefacilitiesplayacrucialroleinsequentialcomputation,thispaperfocusesonasequentialextensionofPCF,calledSPCF,thatincludestwoclassesofcontroloperators:apossiblyemptysetoferrorgen
5、eratorsandacollectionofcatchandthrowconstructs.Foreachsetoferrorgenerators,thepaperpresentsafullyabstractsemanticsforSPCF.Ifthesetofer-rorgeneratorsisempty,thesemanticsinterpretsallproceduresincludingcatchandthrowasBerry-Curiensequentialalgorithms.Ifthelanguagecontainserrorgenerators,proc
6、eduresdenotemanifestlysequentialfunctions.ThemanifestlysequentialfunctionsformaScottdomainthatisisomorphictoadomainofdecisiontrees,whichisthenat-uralextensionoftheBerry-Curiendomainofsequentialalgorithmsinthepresenceoferrors.1FullAbstractionandSequentialityAdenotationalsemanticsforaprogra
7、mminglanguagedeterminestwonaturalequiva-lencerelationsonprogramphrases.Thefirstrelation,denotationalequivalence,equatestwophrasesifandonlyiftheyhavethesamemeaning(denotation).Thesecondrelation,ob-servationalequivalence,equatestwophrasesifandonlyiftheyhavethesameobser
