A mixed linear and non-linear logic proofs, terms

AMixedLinearandNon-LinearLogi:Proofs,TermsandModels(PreliminaryReport)P.N.BentonyUniversityofCambridgeAbstratIntuitionistilinearlogiregainstheexpressivepowerofintuitionistilogithroughthe!(‘ofourse’)modality.Benton,Bierman,HylandanddePaivahavegivenatermassignmentsystemforILLandanassoiatednotionofategorialmodelinwhihthe!modalityismodelledbyaomonadsatisfyingertainextraonditions.Ordinaryintuitionistilogiisthenmodelledinaartesianlosedategorywhiharisesasafullsubategoryoftheategoryofoalgebrasfortheomonad.ThispaperattemptstoexplaintheonnetionbetweenILLandILmorediretlyandsymmetriallybygivingalogi,termalulusandategorialmodelforasysteminwhihthelinearandnon-linearworldsexistonanequalfooting,withoperationsallowingonetopassinbothdiretions.WestartfromtheategorialmodelofILLgivenbyBenton,Bierman,HylandanddePaivaandshowthatthisisequivalenttohavingasymmetrimonoidaladjuntionbetweenasymmetrimonoidallosedategoryandaartesianlosedategory.Wethenderivebothasequentalulusandanaturaldedutionpresentationofthelogiorrespondingtothenewnotionofmodel.Ashorterversionofthispaperistobepresentedat,andsubmittedtotheproeedingsof,the1994AnnualConfereneoftheEuropeanAssoiationforComputerSieneLogi,Kazimierz,Poland.yAuthor’saddress:UniversityofCambridge,ComputerLaboratory,NewMuseumsSite,PembrokeStreet,CambridgeCB23QG,UnitedKingdom.Email:Nik.Bentonl.am.a.uk.ResearhsupportedbyaSERCFellowshipandtheEUEspritprojetLOMAPS.2CONTENTS3Contents1Introdution51.1Bakground::::::::::::::::::::::::::::::::::::51.2Motivation::::::::::::::::::::::::::::::::::::51.2.1FuntionalProgramming::::::::::::::::::::::::51.2.2Logi:::::::::::::::::::::::::::::::::::61.2.3Semantis:::::::::::::::::::::::::::::::::71.3Overview:::::::::::::::::::::::::::::::::::::72TheCategorialPiture92.1AnIsomorphism:::::::::::::::::::::::::::::::::132.2TheComonadandComparisonwithLinearCategories::::::::::::152.2.1LNLmodelImpliesLinearCategory::::::::::::::::::162.2.2LinearCategoryImpliesLNLmodel::::::::::::::::::222.2.3AdditivesandtheSeelyIsomorphisms:::::::::::::::::252.3TheMonadandComparisonwithLet-CCCs:::::::::::::::::272.3.1StrongMonads::::::::::::::::::::::::::::::272.4Examples:::::::::::::::::::::::::::::::::::::292.4.1!-ompletePartialOrders::::::::::::::::::::::::292.4.2AbelianGroups::::::::::::::::::::::::::::::293LNLLogi313.1SequentCalulus:::::::::::::::::::::::::::::::::313.1.1TheFirstWrongWay::::::::::::::::::::::::::323.1.2TheSeondWrongWay:::::::::::::::::::::::::333.1.3AWell-BehavedSequentCalulus:::::::::::::::::::343.1.4CutElimination:::::::::::::::::::::::::::::353.1.5CutEliminationandSemantiEquality::::::::::::::::423.1.6Variations:IntroduingAdditiveNon-LinearContexts::::::::433.1.7Variations:AParsimoniousPresentation:::::::::::::::453.2NaturalDedutionandLNLTerms:::::::::::::::::::::::473.2.1TheNaturalDedutionRules::::::::::::::::::::::473.2.2TermAssignment:::::::::::::::::::::::::::::503.2.3NormalisationandRedution::::::::::::::::::::::513.3Translations::::::::::::::::::::::::::::::::::::563.3.1ILLtoLNLLogi::::::::::::::::::::::::::::573.3.2LNLLogitoILL::::::::::::::::::::::::::::583.3.3FurtherResultsontheTranslations::::::::::::::::::604ConlusionsandFurtherWork625Aknowledgements634CONTENTS51Introdution1.1BakgroundThispaperonernsavariantoftheintuitionistifragmentofGirard’slinearlogi[Gir87℄.Asiswell-known,linearlogidoesnotontainthestruturalrulesofweakeningandontration,butthesearereintroduedinaontrolledwayviaaunaryoperator,written!andpronouned‘ofourse’,‘bang’or‘shriek’.Thesequentalulusrulesfor!arethefollowing:!‘APromotion!‘!A;A‘BDerelition;!A‘B;!A;!A‘BContration;!A‘B‘BWeakening;!A‘BTherulesaboveallowordinaryintuitionistilogitobeinterpretedwithinintuition-isitilinearlogivia(forexample)theso-alled‘Girardtranslation’.In[BBHdP92,BBHdP93b,BBHdP93a℄,Benton,Bierman,HylandanddePaivaformulatedanaturaldedutionpresentationofthemultipliative/exponentialfragmentofILL,togetherwithatermalulus(extendingthepropositionsastypesanalogytolinearlogi)andaat-egorialmodel(alinearategory).Inthatwork,themultipliative(i.e.,Æ)partofthelogiismodelledinasymmetrimonoidallosedategory(SMCC).Thatmuhisstandardandwell-understood.The!modalityisthenmodelledbyamonoidalomonadontheSMCCwhihisrequiredtosatisfyertainextra(andnon-trivial)onditions.TheseextraonditionsaresuÆienttoensurethattheategoryofoalgebrasfortheomonadontainsafullsubategorywhihisartesianlosedandthusmodelstheinterpretationofILinILL.Whilsttheviewthatlinearlogiisprimaryandthatordinarylogiismerelyapartoflinearlogiisappealing(partiularlyifonetakesseriouslythelaimsoflinearlogitobe\thelogibehindlogi),itisnotneessarilyalwaysthebestwayofseeingthesituation.ThispapertriestopresentamoresymmetriviewoftherelationshipbetweenILandILL,startingfromamodel-theoretiperspetive,anditseemsworthtryingtogivesomemotivationforwhythismightbeworthdoing.1.2Motivation1.2.1FuntionalProgrammingFromapratialpointofview,thereareanumberofreasonswhythestandardlineartermalulus(LTC)of[BBHdP92℄mightbeonsideredunsuitableasthebasisofalinearfuntionalprogramminglanguage.Firstly,linearfuntionalpr