An Intuitionistic Logic for Sequential Control

pages

English

Documents

Écrit par
C Liang

Publié par
chaeh

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

chaeh

Nombre de lectures

Langue

English

Niveau: Supérieur
An Intuitionistic Logic for Sequential Control Chuck Liang1 and Dale Miller2 1 Department of Computer Science, Hofstra University, Hempstead, NY, US 2 INRIA Saclay & LIX/Ecole Polytechnique, Palaiseau, France Abstract We introduce a propositional logic ICL, which adds to intuitionistic logic elements of classical reasoning without collapsing it into classical logic. This logic includes a new constant for false, which augments false in intuitionistic logic and in minimal logic. We define Kripke models for ICL and show how they translate to several other forms of semantics. We define a sequent calculus and prove cut-elimination. We then formulate a natural deduction proof system with a term calculus that gives a direct, computational in- terpretation of contraction. This calculus shows that ICL is fully capable of typing programming language control operators such as call/cc while maintaining intuitionistic implication as a genuine connective. 1 Introduction It is now well known that the Curry-Howard correspondence can be extended beyond intuitionis- tic logic. Since Griffin ([7]) showed the relationship between certain classical axioms and control operators, several constructive classical systems have been formulated, including Girard's LC proof system [5] and Parigot's deduction system, from which is derived ?µ-calculus [14] and its variants. However, the isomorphism between ?-abstraction and intuitionistic implication is a very strong one.

logic into

since neither

without ?

intuitionistic logic

within icl

models can

Voir

Publié par

chaeh

Nombre de lectures

Langue

English

AnIntuitionisticLogicforSequentialControlChuckLiang1andDaleMiller21DepartmentofComputerScience,HofstraUniversity,Hempstead,NY,USchuck.c.liang@hofstra.edu2INRIASaclay&LIX/EcolePolytechnique,Palaiseau,Francedale.miller@inria.frAbstractWeintroduceapropositionallogicICL,whichaddstointuitionisticlogicelementsofclassicalreasoningwithoutcollapsingitintoclassicallogic.Thislogicincludesanewconstantforfalse,whichaugmentsfalseinintuitionisticlogicandinminimallogic.WedeﬁneKripkemodelsforICLandshowhowtheytranslatetoseveralotherformsofsemantics.Wedeﬁneasequentcalculusandprovecut-elimination.Wethenformulateanaturaldeductionproofsystemwithatermcalculusthatgivesadirect,computationalin-terpretationofcontraction.ThiscalculusshowsthatICLisfullycapableoftypingprogramminglanguagecontroloperatorssuchascall/ccwhilemaintainingintuitionisticimplicationasagenuineconnective.1IntroductionItisnowwellknownthattheCurry-Howardcorrespondencecanbeextendedbeyondintuitionis-ticlogic.SinceGrifﬁn([7])showedtherelationshipbetweencertainclassicalaxiomsandcontroloperators,severalconstructiveclassicalsystemshavebeenformulated,includingGirard’sLCproofsystem[5]andParigot’sdeductionsystem,fromwhichisderivedλµ-calculus[14]anditsvariants.However,theisomorphismbetweenλ-abstractionandintuitionisticimplicationisaverystrongone.Ifonecollapsesintuitionisticlogicintoclassicallogicaltogetherandconsidersthewholearenaofclassicalproofs,thenoneisconfrontedwiththefactthatclassicalimplicationdoesnothavethesamestrengthasitsintuitionisticcounterpart.Forexample,intuitionisticimplicationcorrespondstotheprogrammingnotionoflocalizedscope.Inclassicallogic,however,(A⇒B)∨CisequivalenttoB∨(A⇒C),whichmeansthattheassumptionAisnotlocalizedtotheleftdisjunct.Thecon-structivemeaningofclassicallogicisdependentonhowwechoosetointerpretclassicalimplication:forexample,¬A∨Band¬(A∧¬B)conveydifferentkindsofproceduralinformation.Ontheotherhand,ifweembedclassicallogicintointuitionisticlogicviaadouble-negationtranslation,thentheconstructivemeaningofclassicalproofsisalsochanged,forwecanonlyexpectλ-termsfromsuchatranslation,andnotλµ-terms.Weproposeanewlogicthatisanamalgamationofintuitionisticandclassicallogics,onethatdoesnotcollapseoneintotheother.WerefertothislogicasIntuitionisticControlLogic(ICL).Incontrasttointermediatelogics,wedonotaddnewaxiomstointuitionisticlogicbutanewlogicalconstantforfalse.Wedistinguishbetweentwosymbols:0and⊥.Theconstant0isfalseinintu-itionisticlogic.Thetwoconstantswillallowustodeﬁnetwoformsofnegation:∼Aand¬A.Forexample,A∨¬AwillbeprovablebutnotA∨∼A.Ontheotherhand,neitherformofnegationisinvolutivebecausebothnegationsaredeﬁnedbyintuitionisticimplication(A⊃0andA⊃⊥).ICLcanalsobedescribedasintuitionisticlogicplusaversionofPeirce’slaw.However,thatdescriptionaloneisunsatisfactory:wedesireclearsemanticsandproofsystemswithcut-eliminationproceduresthatmakecomputingpossible.Wedeﬁneseveralformsofsemantics,includingversionsofKripkemodelsandcartesianclosedcategories.TheseintuitionisticstructuresdonotbecomedegenerateinICL.Thecut-eliminationprocedureswedeﬁnewillincludeaformofstructuralre-ductionasfoundinλµcalculus,therebyshowingthatcontroloperatorscanbeobtainedwithoutacompletecollapseintoclassicallogic.LeibnizInternationalProceedingsinInformaticsSchlossDagstuhl–Leibniz-ZentrumfürInformatik,DagstuhlPublishing,Germany

Voir