introduction to linear logic - t. brauner

《introduction to linear logic - t. brauner》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、BRICSBRICSLS-96-6T.BraBasicResearchinComputerScience¨uner:IntroductiontoLinearLogicIntroductiontoLinearLogicTorbenBrauner¨BRICSLectureSeriesLS-96-6ISSN1395-2048December1996Copyrightc1996,BRICS,DepartmentofComputerScienceUniversityofAarhus.Allrightsreserved.Repr

2、oductionofallorpartofthisworkispermittedforeducationalorresearchuseonconditionthatthiscopyrightnoticeisincludedinanycopy.SeebackinnerpageforalistofrecentpublicationsintheBRICSLectureSeries.Copiesmaybeobtainedbycontacting:BRICSDepartmentofComputerScienceUniversi

3、tyofAarhusNyMunkegade,building540DK-8000AarhusCDenmarkTelephone:+4589423360Telefax:+4589423255Internet:BRICS@brics.dkBRICSpublicationsareingeneralaccessiblethroughWorldWideWebandanonymousFTP:http://www.brics.dk/ftp://ftp.brics.dk/ThisdocumentinsubdirectoryLS/96

4、/6/IntroductiontoLinearLogicTorbenBrauner¨TorbenBra¨unerBRICS1DepartmentofComputerScienceUniversityofAarhusNyMunkegadeDK-8000AarhusC,Denmark1BasicResearchInComputerScience,CentreoftheDanishNationalResearchFoundation.PrefaceThemainconcernofthisreportistogiveanin

5、troductiontoLinearLogic.ForpedagogicalpurposesweshallalsohavealookatClassicalLogicaswellasIntuitionisticLogic.LinearLogicwasintroducedbyJ.-Y.Girardin1987andithasattractedmuchattentionfromcomputerscientists,asitisalogicalwayofcopingwithresourcesandresourcecontro

6、l.Thefocusofthistechnicalreportwillbeonproof-theoryandcomputationalinterpretationofproofs,thatis,wewillfocusonthequestionofhowtointerpretproofsasprogramsandreduction(cut-elimination)asevaluation.WerstintroduceClassicalLogic.Thisisthefundamentalideaoftheproofs-

7、as-programsparadigm.Cut-eliminationforClassicalLogicishighlynon-deterministic;itisshownhowthiscanberemediedeitherbymovingtoIntuitionisticLogicortoLinearLogic.InthecaseonLinearLogicweconsiderIntuitionisticLinearLogicaswellasClassicalLinearLogic.Furthermore,wetak

8、ealookattheGirardTranslationtranslatingIntuitionisticLogicintoIntuitionisticLinearLogic.Also,wegiveabriefintroductiontosomeconcretemodelsofIntuitionisticLinearLogic.Noproofs