An Intuitionistic Logic for Sequential Control

C Liang

Description

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


• icl


• models can


• ¬a

Sujets

• Miller
• Leibniz
• École polytechnique
• Hofstra University
• Intuitionistic logic

Informations

• Publié par: chaeh
• Nombre de lectures: 8
• Langue: English

Extrait

AnIntuitionisticLogicforSequentialControl ChuckLiang 1 andDaleMiller 2 1DepartmentofComputerScience,HofstraUniversity,Hempstead,NY,US [e-mail] 2INRIASaclay&LIX/EcolePolytechnique,Palaiseau,France [e-mail] Abstract WeintroduceapropositionallogicICL,whichaddstointuitionisticlogicelementsofclassicalreasoning withoutcollapsingitintoclassicallogic.Thislogicincludesanewconstantforfalse,whichaugments falseinintuitionisticlogicandinminimallogic.WedefineKripkemodelsforICLandshowhowthey translatetoseveralotherformsofsemantics.Wedefineasequentcalculusandprovecut-elimination.We thenformulateanaturaldeductionproofsystemwithatermcalculusthatgivesadirect,computationalin- terpretationofcontraction.ThiscalculusshowsthatICLisfullycapableoftypingprogramminglanguage controloperatorssuchascall/ccwhilemaintainingintuitionisticimplicationasagenuineconnective. 1Introduction ItisnowwellknownthattheCurry-Howardcorrespondencecanbeextendedbeyondintuitionis- ticlogic.SinceGriffin([7])showedtherelationshipbetweencertainclassicalaxiomsandcontrol operators,severalconstructiveclassicalsystemshavebeenformulated,includingGirard’sLCproof system[5]andParigot’sdeductionsystem,fromwhichisderivedλµ-calculus[14]anditsvariants. However,theisomorphismbetweenλ-abstractionandintuitionisticimplicationisaverystrong one.Ifonecollapsesintuitionisticlogicintoclassicallogicaltogetherandconsidersthewholearena ofclassicalproofs,thenoneisconfrontedwiththefactthatclassicalimplicationdoesnothavethe samestrengthasitsintuitionisticcounterpart.Forexample,intuitionisticimplicationcorrespondsto theprogrammingnotionoflocalizedscope.Inclassicallogic,however,(A ⇒ B) ∨ Cisequivalent toB ∨ (A ⇒ C),whichmeansthattheassumptionAisnotlocalizedtotheleftdisjunct.Thecon- structivemeaningofclassicallogicisdependentonhowwechoosetointerpretclassicalimplication: forexample, ¬ A ∨ B and ¬ (A ∧¬ B) conveydifferentkindsofproceduralinformation. Ontheotherhand,ifweembedclassicallogicintointuitionisticlogicviaadouble-negation translation,thentheconstructivemeaningofclassicalproofsisalsochanged,forwecanonlyexpect λ-termsfromsuchatranslation,andnotλµ-terms. Weproposeanewlogicthatisanamalgamationofintuitionisticandclassicallogics,onethat doesnotcollapseoneintotheother.WerefertothislogicasIntuitionisticControlLogic(ICL).In contrasttointermediatelogics,wedonotaddnewaxiomstointuitionisticlogicbutanewlogical constantforfalse.Wedistinguishbetweentwosymbols:0and ⊥ .Theconstant0isfalseinintu- itionisticlogic.Thetwoconstantswillallowustodefinetwoformsofnegation: ∼ Aand ¬ A.For example, A ∨¬ A willbeprovablebutnot A ∨∼ A .Ontheotherhand,neitherformofnegationis involutivebecausebothnegationsaredefinedbyintuitionisticimplication( A ⊃ 0 and A ⊃⊥ ). ICLcanalsobedescribedasintuitionisticlogicplusaversionofPeirce’slaw.However,that descriptionaloneisunsatisfactory:wedesireclearsemanticsandproofsystemswithcut-elimination proceduresthatmakecomputingpossible.Wedefineseveralformsofsemantics,includingversions ofKripkemodelsandcartesianclosedcategories.Theseintuitionisticstructuresdonotbecome degenerateinICL.Thecut-eliminationprocedureswedefinewillincludeaformofstructuralre- duction asfoundinλµcalculus,therebyshowingthatcontroloperatorscanbeobtainedwithouta completecollapseintoclassicallogic. LeibnizInternationalProceedingsinInformatics SchlossDagstuhl–Leibniz-ZentrumfürInformatik,DagstuhlPublishing,Germany