Logic Programming with Linear Logic

LogicProgrammingwithLinearLogicMichaelDavidWinikoff1997SubmittedintotalfulfilmentoftherequirementsofthedegreeofDoctorofPhilosophyDepartmentofComputerScienceSchoolofElectricalEngineeringandComputerScienceTheUniversityofMelbourneParkville,Victoria3052AUSTRALIAiiAbstractProgramminglanguagesarethebasictoolsofcomputerscience.Thedesignofagoodprogramminglanguageisatrade-offbetweenmanyfactors.Perhapsthemostimpor-tantanddifficulttrade-offisbetweenexecutionefficiencyandprogrammerefficiency.Higherlevellanguagesreducetheamountofworktheprogrammerhastodo;howevertheyhave,todate,beenlessefficientthanlowerlevellanguages.Thatlowerlevellan-guagesarenecessarilymoreefficientisapieceoffolklorewhichisunderattack–higherlevellanguagesareconstantlycomingclosertotheperformanceofthelowerlevellan-guages.Aconsequenceofthisconstantlyclosingperformancegapisthattheabstractionlevelofprogramminglanguagesisslowlybutinevitablyrising.Aclassofprogramminglanguageswhichhasbeendescribedas“veryhighlevel”isdeclarativeprogramminglanguages.Declarativeprogramminglanguageshavesimpleformalsemanticsandareeasiertoreasonaboutandtoconstructtoolsforthanmoretra-ditionalprogramminglanguages.Howevertheselanguagesdosufferfromanumberofproblems.Theyareweakatexpressingsideeffectsandconcurrency.SideeffectsaregenerallyusedtoperformI/OandasaresultdeclarativelanguageshavebeenweakatexpressingI/O.Declarativelanguagesarealsoweakatexpressingconcurrencywithoutcompromisingtheirsemanticpurityandasaresulttendtobeweakatexpressinggraph-icaluserinterfaces.Girard’slinearlogicpromisessolutionstosomeoftheseproblems–linearlogiciscapableofmodellingupdates,ithasinspiredlineartypeswhichenablesideeffectstobesafelyintroducedforefficiencyreasons,andlinearlogiccanmodelconcurrentbehaviorcleanly.Thisthesisfocusesonthederivationofalogicprogramminglanguagebasedonlin-iiiear(ratherthanclassical)logic.Ourhypothesisisthatitispossibletoderivealogicpro-gramminglanguagefromlinearlogic.Thislanguagecanbeeffectivelyimplementedandisanexpressivelanguage,allowingupdates,concurrencyandotheridiomstobecleanlyexpressed.Weinvestigatethesystematicderivationoflogicprogramminglanguagesfromlogicsandproposeataxonomyof“litmustests”whichcandeterminewhetherasubsetofalogiccanbeviewedasalogicprogramminglanguage.Oneofthetestsdevelopedisappliedinordertoderivealogicprogramminglanguagebasedonthefullmultipleconclusionlinearlogic.ThelanguageisnamedLygon.Wederiveanefficientsetofrulesformanagingresourcesinlinearlogicproofsandil-lustratehowtheselectionofagoalformulacanbemademoredeterministicusingheuris-ticsderivedfromknownpropertiesoflinearlogicproofs.FinallyweinvestigateprogrammingidiomsinLygonandpresentarangeofprogramswhichillustratethelanguage’sexpressiveness.ivAcknowledgementsIwouldliketothankmytwosupervisors–JamesHarlandandHaraldSøndergaard,fortheirsupportandguidance.Withouttheirfastandaccurateproof-readingthisthesiswouldundoubtedlyhavetheodd(additional)inconsistencyortwo.TheotherhalfoftheoriginalLygonduo,DavidPym,hascontinuedtooffercom-mentsfromafar.IwouldalsoliketothankDavidforinterestingandstimulatingdiscus-sion.InthelastfewyearstheLygonteamhasgrownatRMITandincludedanumberofstudentswhoseworkhasadvancedthecauseofLygon.Inparticular,theLygondebugger[153]istheworkofYiXiaoXu.YiXiaoisalsotheauthorofprograms14and15.Iwouldliketothankananonymousreferee(ofapaperbasedonchapter4)forpoint-ingustoHodas’thesisandforsuggestinganencodingofLygoninLolli.Iwouldliketothanktheexaminersofthisthesisfortheircarefulreadingandusefulcomments.Inparticular,chapter3benefitedfromthedetailedcritiqueprovided.ThankgototheAustralianResearchCouncil,theCollaborativeInformationTechnol-ogyResearchInstitute,theCentreforIntelligentDecisionSystems,theMachineIntelli-genceProject,theDepartmentofComputerScienceandtheSchoolofGraduateStudiesforfinancialsupport.ThanksalsogototheadministrativeandsystemsupportstaffattheDepartmentofComputerScienceforprovidingaworkingenvironmentandinvisi-blykeepingthingsworkingbehindthescenes.Lastbutnotleast,Iwouldliketothankmyfamily:Myparentsforcountlesssmallandmanylargethings,myfianc´e,LeanneVeitch,forsupportaboveandbeyondthecallofdutythroughthelastfewweeks,andmysister,Yael,fornoapparentreason(shewantedtobehere!).vThankstoyouall!viDedicationTothememoryofmygrandfather,PaulFeher(3.1.1907-8.10.1995).viiviiiContents1Introduction12Background52.1SequentCalculus:::::::::::::::::::::::::::::52.2IntuitionisticLogic::::::::::::::::::::::::::::152.3LinearLogic:::::::::::::::::::::::::::::::152.4Permutabilities::::::::::::::::::::::::::::::182.5LinearLogicProgrammingLanguages:::::::::::::::::233DerivingLogicProgrammingLanguages273.1ProblemswithUniformity::::::::::::::::::::::::303.2WhatIsLogicProgramming?::::::::::::::::::::::363.3TheSingleConclusionCase:::::::::::::::::::::::383.3.1ExtendingUniformitytoDealwithAtomicGoals::::::::443.4Examples::::::::::::::::::::::::::::::::503.4.1PureProlog:::::::::::::::::::::::::::513.4.2Lolli:::::::::::::::::::::::::::::::533.5TheMultipleConclusionedCase::::::::::::::::::::573.5.1GeneralisingUniformitytotheMultipleConclusionCa