A Classical Sequent Calculus with Dependent Types étienne Miquey.pdf

该【A Classical Sequent Calculus with Dependent Types étienne Miquey 】是由【周瑞】上传分享，文档一共【47】页，该文档可以免费在线阅读，需要了解更多关于【A Classical Sequent Calculus with Dependent Types étienne Miquey 】的内容，可以使用淘豆网的站内搜索功能，选择自己适合的文档，以下文字是截取该文章内的部分文字，如需要获得完整电子版，请下载此文档到您的设备，方便您编辑和打印。:..AClassicalSequentCalculuswithDependentTypeséTIENNEMIQUEY,INRIA,te8DependenttypesareakeyfeatureoftheproofassistantsbasedontheCurry-,theyareknowntomisbehaveinthepresenceofdependenttypes,unlessdepen-,whilesequentcalculinaturallysupportcontinuation-passing-styleinterpretations,-by-valuelanguagewithacontroloperatoranddependenttypes,andtojustifyitssoundnessthroughacontinuation-passing--by-valueversionoftheλμμ?--tencybymeansofacontinuation-passing-,:?putation→Controlprimitives;Typetheory;Operationalsemantics;Prooftheory;AdditionalKeyWordsandPhrases:Dependenttypes,sequentcalculus,classicallogic,controloperators,call-by-value,delimitedcontinuations,continuation-passing-styletranslation,valuerestrictionACMReferenceformat:é,2,Article8(March2019),:///,-gramming,dependenttypesprovidemoreprecisetypes—andthusmoreprecisespeciications—,,twoofthemostac--typetheories:thecalculusofinductiveconstructionsforCoq[6]andMartin-L?f’stypetheoryforAgda[24].Yet,bothsystemslacksupportforclassicallogicandmoregenerallyforsideefects,’addresses:é.Miquey,LS2N-LaboratoiredesSciencesduNumériquedeNantes,FacultédesSciencesetTech-niques,2ChemindelaHoussinière,Batiment34,44322Nantes;email:etienne.******@(s),orrepublish,topostonserversortoredistributetolists,requirespriorspeciicpermissionand/orafee.******@.?2019Copyrightheldbytheowner/author(s).-0925/2019/03-ART8$:///,,,:March2019.:..8:2é.MiqueyInpractice,esstolow-levelcontrol(.,tothewaytheprogramisexecutedontheavailablehardware)andmakesomealgorithmsmonefects,suchastheexplicitmanipulationofmemory,thegenera-tionofrandomnumbers,andinput/outputfacilities,areavailableinmostpracticalprogramminglanguages(.,OCaml,C++,Python,Java).In1990,(shortforcallwithcurrentcontinua-tion)couldbetypedbyPeirce’slaw((A→B)→A)→A)[15],thusextendingtheformulas-as-,Peirce’slawisknowntoimply,inanintuitionisticframework,alltheotherformsofclassicalreasoning(excludedmiddle,reductioadabsurdum,doublenegationelimination,etc.).putationalinterpretationofclassicalproofs,,forexample,Parigot’sλμ-calculus[31],BarbaneraandBerardi’ssymmetricλ-calculus[3],Krivine’sλc-calculus[21],andCurienandHerbelin’sλμˉμ?-calculus[7].Nevertheless,dependenttypesareknowntomisbehaveinthepresenceofcontroloperatorsandleadtologicalinconsistencies[17].Sincethesameproblemariseswithawiderclassofef-fects,itseemsthatwearefacingthefollowingdilemma:eitherwechooseanefectfullanguage(allowingustowritemoreprograms)eptingthelackofdependenttypesorwechooseadependentlytypedlanguage(allowingustowriteinerspeciications)-putationalefects(.,divergence,I/O,localreferences,exceptions).Amongotherworks,al.[1],byVákár[35,36],orbyPédrotandTabareau,whoproposedasystematicalwaytoaddefectstotypetheory[33].Sideefects—putationsinfunctionalprogramming—,controloperatorscanbeinterpretedsimi-larlythroughthecontinuationmonad,,theproblempletelysatisfy-[18]andLepigre[22]proposedsomerestrictionsonpatiblewithaclassicalproofsystem,whileBlot[5]-by-ValueandValueRestrictionInlanguagesenjoyingtheChurch-Rosserproperty(liketheλ-calculusorCoq),theorderofevaluationisirrelevant,-ular,thecall-by-nameandcall-by-,,considerthesimplecaseofafunctionappliedtoatermproducingsomesideefects(.,increasingareference).Incall-by-name,putationoftheargumentisdelayedtothetimeofitsefectiveuse,whileincall-by-value,,forinstance,thefunctionneverusesitsargument,thecall-by-nameevaluationwillnotgenerateanysideefect,andifitusesittwice,urtwice(andthereferencewillhaveits1Asidefromstrictlylogicalconsiderationsasin[18],,forinstance,theininitetapelemmathatstatesthatfromanyininitesequenceofnaturalnumbers,,andthecorrespondingprogram(which,givenasinputastreamofintegers,returnsastreamthatconsistseitheronlyofoddintegersoronlyofevenones)[23,],,,:March2019.:..AClassicalSequentCalculuswithDependentTypes8:3valueincreasedbytwo).Onthecontrary,inbothcases,thecall-by-valueevaluationgeneratesthesideefectexactlyonce(andthereferencehasitsvalueincreasedbyone).Inthisarticle,wepresentalanguagefollowingthecall-by-valuereductionstrategy,,whenconsideringalanguagewithcontroloperators(orotherkindsofsideefects),soundnessoftenturnsouttobesubtletopreserveincall-by--by-valueinthepresenceofsideefectswererelatedtoref-erences[39]andpolymorphism[16].Inbothcases,asimplesolution(butoftenunnecessarilyrestrictiveinpractice[14,22])tosolvetheinconsistenciesconsistsoftheintroductionofavalueases,,Lepigrepre-sentedaproofsystemprovidingdependenttypesandacontroloperator[22],,,therestrictionthatarisesnaturallycoincideswiththenegative-elimination-freefragmentofHerbelin’sdPAωsystem[18].-by-valuelanguagewithclassicalcontrolanddependenttypes,andtojustifyitssoundnessthroughacontinuation-passing-?-calculus[7],suchacalculusisclosetoanabstractmachine,which-pilation[8].Asamatteroffact,theoriginalmotivationforthisworkwasthedesignofaprogramtranslationforHerbelin’sdPAωsystem(passescontroloperatorsanddepen-denttypes),thiscalculuswaspresentedinanaturaldeductionstyle,-passing-,aseofacalculuswithclassicallogic,,theusualcall-by-valuestrategyoftheλμμ?-calculuscausessubjectreductiontofail,whichwouldal-,thesystemwedevelopmightbeairststepto-wardtheadaptionofthewell-understoodcontinuation-passing-styletranslationsforMLtodesigna(dependently),,presentedinSection2,,itisnotsuitableforobtainingacontinuation-passing-[2],whichareusedtoforcethepurityneededfordependenttypesinanotherwisenonpurely2Inthesenseofaformulas-as-typesinterpretationofasequentcalculusàlaHilbert(asCurien-Herbelin’sλμμ?-calculus[7]orMunch-agnoni’ssystemL[29]),,,,:March2019.:..8:4é.?--initionofthenegative-elimination-freefragment(Section3).Inaddition,itallowsforthedesign,inSection4,ofacontinuation-passing-styletranslationthatpreservesdependenttypesandper-,italsoprovidesuswithawaytoembedourcalculusintoLepigre’scalculus[22],:?binedependenttypesandcontroloperatorsbymeansofasyntacticre-strictiontothenegative-elimination-freefragment.?Wegiveasequentcalculuspresentationandsolvethetype-soundnessissuesitraisesintwodiferentways.?Ourirstsolutionsimplyreliesonalistofdependenciesthatareaddedtothetypesystem.?OursecondsolutionusesdelimitedcontinuationstoensureconsistencywithdependenttypesandprovidesuswithaCPStranslation(carryingdependenttypes)toacalculuswith-outacontroloperator.?WerelateoursystemtoLepigre’scalculus,[26].?-CalculusWerecallherethespiritoftheλμμ?-calculus;forfurtherdetailsandreferencespleaserefertotheoriginalarticle[7].Thesyntaxandreductionrules(parameterizedoverasubsetofproofsVandasubsetofevaluationcontextsE)aregiveninFigure1,whereμa?.ccanbereadasacontextleta=[]p||ecanbeunderstoodasastateofanabstractmachine,representingtheevaluationofaproofp(theprogram)againstacoproofe(thestack),,,