Definitions
DieterSpreen
FachbereichMathematik,TheoretischeInformatikUniversit¨at–GHSiegen,D–57068Siegen,Germany
Abstract
Wepresentapurelydomain-theoreticmodelofCoquandandHuet’sCalculusof
Construction[3],whichisoneofthemostpowerfultypesystemsproposedintheliterature.
Thewell-formedexpressionsofitslanguagearedividedintothreelevels:Terms,Types,andOrders.TermsaretheelementsofTypes,whiletheelementsofOrdersarecalledOperators.ThereisaspecialOrderconstantTypedenotingthecollectionofallTypes.Ordersareclosedunderboth,thedependentproductandthedependentsumofOrderfamiliesindexedoveranOrderoraType.Inthesameway,TypesareclosedunderthedependentproductaswellasthedependentsumofTypefamiliesindexedoveranOrderoraType.Inaddition,weallowrecursivedefinitionsatallthreelevels.
AsasubsystemthecalculuscontainsGirard-Reynold’spolymorphicλ-calculus[4,5,7].BuildinguponideasofGirard[6],Coquandetal.[2]presentedamodelofthissubcalculusinwhichTypesareinterpretedasdI-domains.
Itiswellknownthateachsuchdomaincanberepresentedasthestatesetofastableeventstructure[1].Inourmodel,weinterpretTypesasstableeventstructures,andinordernottohavetodealwithtoomanyisomorphiccopieswerestrictourselvestostableeventstructureswithonlynaturalnumbersaselements.Withrespecttoanaturalsubstructurerelation,thesetWofallsucheventstructuresturnsouttobealocallydistributivestableω-bifinitedomain.Here,locallydistributivemeansthateveryprincipalidealisdistributive.
Stablebifinitedomainsarealgebraicandcanthusbeobtained(uptoisomorphism)fromtheircompactelementsbyidealcompletion.WeinterpretOrdersaspartiallyorderedsetsthathaveonlynaturalnumbersaselementsandtheidealcompletionofwhichisalocallydistributivestableω-bifinitedomain.Again,anaturalsubstructurerelationcanbedefinedsothatthesetBofallsuchpartialordersisalocallydistributiveω-algebraicL-domainwhichsatisfiesBerry’saxiomI.
Expressionsofthecalculusareconstructedwithrespecttoanenvironment,calledcontext,inwhichthefreevariablesaredeclared.Itturnsoutthatcontextscanbeinterpretedbylocallydistributiveω-algebraicL-domainsthatsatisfyBerry’saxiomI.
ForastableeventstructureA∈WletS(A)beitsstatespaceandforapartialorderB∈BletR(B)beitsidealcompletion.Thenthemodelisasfollows:
•ATypeexpressionαwithfreevariablesdeclaredincontextΓisinterpretedasastablemapfrom[[Γ]]intoW.
1
•ATermexpressiontofTypeαwithfreevariablesdeclaredincontextΓisinter-pretedasastablefamily[[t]]with[[t]](x)∈S([[α]](x)),forx∈[[Γ]].•AnOrderexpressionσwithfreevariablesdeclaredincontextΓisinterpretedasastablemapfrom[[Γ]]intoB.•AnOperatorexpressionTofOrderσwithfreevariablesdeclaredincontextΓisinterpretedasastablefamily[[T]]with[[T]](x)∈R([[σ]](x)),forx∈[[Γ]].BythiswaywecanalsointerpretanextensionofthelanguagebydisjointsumsofTypesandOrders.
References
[1]R.AmadioandP.-L.Curien,DomainsandLambda-Calculi(CambridgeUniversity
Press,Cambridge,1997).[2]T.Coquand,C.Gunter,andG.Winskel,DI-domainsasamodelofpolymorphism,
in:M.Mainetal.,eds.,MathematicalFoundationsofProgrammingLanguageSemantics,NewOrleans,LA,1987,LectureNotesinComputerScience,Vol.298(Springer,Berlin,1987)344–363.[3]T.CoquandandG.Huet,Thecalculusofconstructions,Inform.andComput.76
(1988)95–120.[4]J.-Y.Girard,Uneextensiondel’interpr´etationfonctionelledeG¨odel`al’analyseet
sonapplication`al’´eliminationdescoupuresdansl’analyseetlath´eoriedestypes,in:J.F.Fenstad,ed.,Proceedings,2ndScandinavianLogicSymp.(North-Holland,Amsterdam,1971)63–92.[5]J.-Y.Girard,Interpretationfonctionelleet´eliminationdescoupuresdel’arithm´e-tiqued’ordresup´erieure,TheseD’Etat,Universit´eParisVII,1972.[6]J.-Y.Girard,ThesystemFofvariabletypes,fifteenyearslater,TheoreticalCom-puterScience45(1986)159–192.[7]J.C.Reynolds,Towardsatheoryoftypestructures,in:B.Robinet,ed.,Col-loquesurlaprogrammation,LectureNotesinComputerScience,Vol.19(Springer,
Berlin,1974)408–425.
E-mail:spreen@informatik.uni-siegen.de
2
因篇幅问题不能全部显示，请点此查看更多更全内容