资源描述：
《FULLY ABSTRACT SEMANTICS FORO BSERVABLY SEQUENTIAL LANGUAGES》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、FULLYABSTRACTSEMANTICSFOROBSERVABLYSEQUENTIALLANGUAGESRobertCartwrightPierre-LouisCurienMatthiasFelleisenDepartmentofComputerScienceRiceUniversityHouston,TX77251-1892AlsoappearedinInformationandComputation1994RiceUniversityTechnicalReport#93-219Minorrevisions:J
2、uly2003FULLYABSTRACTSEMANTICSFOROBSERVABLYSEQUENTIALLANGUAGESRobertCartwright∗DepartmentofComputerScience,RiceUniversity,Houston,TX77005Pierre-LouisCurien†EcoleNormaleSup´erieure,LIENS-CNRS,45rued’Ulm,75230Paris,FranceMatthiasFelleisen‡DepartmentofComputerScien
3、ce,RiceUniversity,Houston,TX77005AbstractOneofthemajorchallengesindenotationalsemanticsistheconstructionofafullyabstractsemanticsforahigher-ordersequentialprogramminglanguage.Forthepastfifteenyears,researchonthisproblemhasfocusedondevelopingasemanticsforPCF,anid
4、ealizedfunctionalprogramminglanguagebasedonthetypedλ-calculus.Unlikemostpracticallanguages,PCFhasnofacilitiesforobservingandexploitingtheevalu-ationorderofargumentstoprocedures.Sincewebelievethatthesefacilitiesplayacrucialroleinsequentialcomputation,thispaperfo
5、cusesonasequentialextensionofPCF,calledSPCF,thatincludestwoclassesofcontroloperators:apossiblyemptysetoferrorgeneratorsandacollectionofcatchandthrowconstructs.Foreachsetoferrorgenerators,thepaperpresentsafullyabstractsemanticsforSPCF.Ifthesetofer-rorgeneratorsi
6、sempty,thesemanticsinterpretsallproceduresincludingcatchandthrowasBerry-Curiensequentialalgorithms.Ifthelanguagecontainserrorgenerators,proceduresdenotemanifestlysequentialfunctions.ThemanifestlysequentialfunctionsformaScottdomainthatisisomorphictoadomainofdeci
7、siontrees,whichisthenat-uralextensionoftheBerry-Curiendomainofsequentialalgorithmsinthepresenceoferrors.1FullAbstractionandSequentialityAdenotationalsemanticsforaprogramminglanguagedeterminestwonaturalequiva-lencerelationsonprogramphrases.Thefirstrelation,denota
8、tionalequivalence,equatestwophrasesifandonlyiftheyhavethesamemeaning(denotation).Thesecondrelation,ob-servationalequivalence,equatestwophrasesifandonlyiftheyhavethesameobser
