Unification of Simply Typed Lambda Terms as Logic Programming

Published by

Niveau: Supérieur
Unification of Simply Typed Lambda-Terms as Logic Programming Dale Miller? Laboratory for the Foundation of Computer Science University of Edinburgh, and Computer Science Department University of Pennsylvania March 1991 Abstract The unification of simply typed ?-terms modulo the rules of ?- and ?-conversions is often called “higher-order” unification because of the possible presence of variables of functional type. This kind of unification is undecidable in general and if unifiers exist, most general unifiers may not exist. In this paper, we show that such unification problems can be coded as a query of the logic programming language L? in a natural and clear fashion. In a sense, the translation only involves explicitly axiomatizing in L? the notions of equality and substitution of the simply typed ?-calculus: the rest of the unification process can be viewed as simply an interpreter of L? searching for proofs using those axioms. 1 Introduction Various recent computer systems require typed ?-terms to be unified. For example, the theorem proving systems TPS [1] and Isabelle [14] and the logic programming language ?Prolog [13] all require unification of simply typed ?-terms. The logic programming language Elf [15], based on the type system LF [5], requires a similar operation for dependent typed ?-terms. Flexible implementations of type systems will probably need to employ various aspects of such unification.

  • binary equality predicates

  • terms

  • avoid variable

  • higher order

  • used adjective

  • order horn

  • clause

  • terms modulo

  • ?0


Published : Wednesday, June 20, 2012
Reading/s : 18
Tags :
Origin : lix.polytechnique.fr
Number of pages: 12
See more See less
UnificationofSimplyTypedLambda-TermsasLogicProgrammingDaleMillerLaboratoryfortheFoundationofComputerScienceUniversityofEdinburgh,andComputerScienceDepartmentUniversityofPennsylvaniaMarch1991AbstractTheunificationofsimplytypedλ-termsmodulotherulesofβ-andη-conversionsisoftencalled“higher-order”unificationbecauseofthepossiblepresenceofvariablesoffunctionaltype.Thiskindofunificationisundecidableingeneralandifunifiersexist,mostgeneralunifiersmaynotexist.Inthispaper,weshowthatsuchunificationproblemscanbecodedasaqueryofthelogicprogramminglanguageLλinanaturalandclearfashion.Inasense,thetranslationonlyinvolvesexplicitlyaxiomatizinginLλthenotionsofequalityandsubstitutionofthesimplytypedλ-calculus:therestoftheunificationprocesscanbeviewedassimplyaninterpreterofLλsearchingforproofsusingthoseaxioms.1IntroductionVariousrecentcomputersystemsrequiretypedλ-termstobeunified.Forexample,thetheoremprovingsystemsTPS[1]andIsabelle[14]andthelogicprogramminglanguageλProlog[13]allrequireunificationofsimplytypedλ-terms.ThelogicprogramminglanguageElf[15],basedonthetypesystemLF[5],requiresasimilaroperationfordependenttypedλ-terms.Flexibleimplementationsoftypesystemswillprobablyneedtoemployvariousaspectsofsuchunification.Inordertoavoidusingtheveryvagueandoverusedadjective“higher-order,”weshallrefertotheproblemofunifyingsimplytypedλ-termsmoduloβ-andη-conversionasβη-unification.Therehavebeenseveralpresentationsofβη-unification.OneofthefirsttohavebeenimplementedinnumeroussystemswasgivenbyHuetin[7].SnyderandGallierin[16]andtheauthorin[11]followHuet’spresentationcloselyexceptthatdetailsofthesearchforunifiersaremademoredeclarativeusingnotionssimilartothetransitionsystemsfoundin[8].Thepresentationgivenherewilldepartsignificantlyfromthosefoundintheseotherpapers,althoughinterestingconnectionsbetweenthesepresentationscanbemade.ThemostsignificantdepartureisthatthelogicprogramminglanguageLλ[10]isemployedtoassistinspecifyingAppearsintheProceedingsofthe1991InternationalConferenceonLogicProgramming,editedbyKoichiFurukawa,June1991.1
βη-unification.Toacertainextent,thetransitionsystemsusedin[8,11,16]couldbeformalizedusingfirst-orderHornclauses.ThelogicLλismoreexpressivethanHornclausesbecauseitcontainsconstructsforthescopedintroductionofprogramclausesandlocalconstants.Thesescopingconstructsareusedtoaddressproblemsinhandlingthescopesandnamesofboundvariablesinλ-terms.ThelogicLλisaweaksubsetofthelogicunderlyingλProlog:itisweakerinthatanimplementationofLλwouldonlyneedtocontainakindoffirst-orderunificationwhileλPrologneedsfullhigher-orderunification.Thispaperisanattempttounderstandexactlythisgapandtoshowthatthegapcanbebridgedcompletelywithintheweakerlanguageinaverydirectanddeclarativeway.Thispaperisdividedintothefollowingsections.Thenextsectionmotivatesastyleofspecificationusedthroughoutthepaper.Section3describessomebasicaspectsofthesimplytypedλ-calculusandSection4presentstwologicprogramminglanguages,hhωandLλ,thatweuseforspecification.EqualityandsubstitutionaregivenanLλspecificationinSection5.Thenon-deterministicspecificationofβη-unificationiscompletedinSection6.SomeconsiderationsforproducingadeterministicimplementationofthisspecificationaregiveninSection7.WebrieflyconcludeinSection8.2MotivationsConsiderasimple,multi-sortedfirst-orderlogicthatconsistsoftheprimitivetypes(sorts)S={i,j}andsignature(i.e.,thesetofconstants)Σ0={a:i,b:j,f:ij,g:jii}.Forexample,theterm(g(fa)(gba))isaclosed,first-ordertermsoftypeioverΣ0.Letcopyiandcopyjbethebinaryequalitypredicatesforthesetwotypes(thereasonforchosingtherootword“copy”insteadof,say,“equal”willbeapparentlater).Theprovableinstancesofequalityfortypesiandjcanbeaxiomatizedusingthetwoclausesix.copyixx,jx.copyjxx.(Thesubscriptonaquantifierindicatesthetypethequantifiedvariableassumesinitsscope.)Ofcourse,thisdescriptionofequalitydoesnotprovideanyinformationabouthowequalityischecked.Itisaconvenientspecification,however,sinceitisactuallyindependentofthesigna-tureusedtobuildtermsofthesetwosorts.AmoredetailedspecificationforthesepredicatesgiventhesignatureabovewouldbetheclausesC0listedbelow:copyiaa,copyjbb,ixiu(copyixucopyj(fx)(fu)),jxju(copyjxu⊃∀iyiv(copyiyvcopyi(gxy)(guv))).Itisasimplemattertoprovethatiftandsaretwoclosedterms,thencopyitsisprovablefromtheseformulasifandonlyiftandsareequaltermsoftypeioverthesignatureΣ0.AlltheclausesinC0areessentiallyfirst-orderHornclauses.Giventhisformulationofequality,itisverysimpletospecifysubstitutioninthefollowingfashion.Letx:ibea“new”constant(chosensoasnottobeinΣ0),lettbesomeclosedtermoftypeioverΣ0,andletsbesometermoverΣ0∪{x:i}.Thenitisagainaneasymatterto2
showthattheatomcopyisrisprovablefromC0augmentedwiththeclausecopyixtifandonlyifristheresultofsubstitutingtforxins;thatis,C0∪{copyixt}`copyisrifandonlyifr=[x7→t]s.Thissimpledeviceofaugmentingequalityprogramswillbeusedfrequentlytoencodesubstitution.Sincecopywillsometimesindicateequalityandsometimessubstitution,dependingonthecontext,itwasnamedforamoreoperationalandneutralconcept.Finally,noticethatthestructureofthesignatureofΣ0givesriseimmediatelytothestruc-tureoftheprogramclausesinC0.Thus,foreachfunctionalarrowinthetypeofaconstant,therecorrespondstwouniversalquantifiersandanimplicationintheprogram.Followingthisobservation,itseemsclearhowtoincorporateaconstantofsecondordertypeintothespecifi-cationofequality.Forexample,letΣ10∪{h:(ij)i}.Theλ-termh(λw.f(gbw)),forexample,isaΣ1-termoftypei.Followingtheexampleabove,theclausefordescribingequalityfortermscontaininghshouldbewrittenasijxiju(iyiv(copyiyvcopyj(xy)(uv))copyj(hx)(hu)).AsweshallseelaterinSection5,thisisthecorrectaxiomatizationofequalitywithrespecttotheconstanth.Thisclause,however,isclearlynotafirst-orderHornclausesinceitcontainsanimplicationanduniversalquantifierinitsbodyandbecauseitusesquantificationofthesecond-ordervariablesxandu.Thematerialinthenexttwosectionsprovideaformalbackgroundbywhichtheaboveobservationscanbemadepreciseandgeneralized.3SimplyTypedλ-CalculusLetSbeafixed,finitesetofprimitivetypes(alsocalledsorts).Thesetoftypesisthesmallestsetofexpressionsthatcontainstheprimitivetypesandisclosedundertheconstructionoffunctiontypes,usingthebinary,infixsymbol.TheGreeklettersτandσareusedassyntacticvariablesrangingovertypes.Thetypeconstructorassociatestotheright:readτ1τ2τ3asτ1(τ2τ3).Letτbethetypeτ1→∙∙∙→τnτ0whereτ0Sandn0.(Byconvention,ifn=0thenτissimplythetypeτ0.)Thetypesτ1,...,τnaretheargumenttypesofτwhilethetypeτ0isthetargettypeofτ.Theorderofatypeτisdefinedasfollows:IfτSthenτhasorder0;otherwise,theorderofτisonegreaterthanthemaximumorderoftheargumenttypesofτ.Thus,τhasorder1exactlywhenτisoftheformτ1→∙∙∙→τnτ0wheren1and{τ01,...,τn}⊆S.Foreachtypeτ,weassumethattherearedenumerablymanyconstantsandvariablesofthattype.Constantsandvariablesdonotoverlap,andiftwoconstants(orvariables)havedifferenttypes,theyaredifferentconstants(orvariables).Asignature(overS)isafinitesetΣofconstants.Weoftenenumeratesignaturesbylistingtheirmembersaspairs,writtena:τ,whereaisaconstantoftypeτ.Althoughattachingatypeinthiswayisredundant,itmakesreadingsignatureseasier.Aconstantorvariableoftypeτisatermoftypeτ.Iftisatermoftypeτσandsisatermoftypeτ,thentheapplication(ts)isatermoftypeσ.Applicationassociatestotheleft;thatis,theexpression(t1t2t3)isreadas((t1t2)t3).Finally,ifxisavariableoftypeτandtisatermoftypeσ,thentheabstractionλxtisatermoftypeτσ.IfΣisasignatureandtisaclosedtermallofwhoseconstantsaremembersofΣ,thentisaΣ-term.Ifxandsaretermsofthesametypethen[x7→s]denotestheoperationofsubstitutingsforallfreeoccurrencesofx,systematicallychangingboundvariablesinordertoavoidvariablecapture.3
Termsarerelatedtoothertermsbythefollowingconversionrules.Theterm-convertstotheterms0ifscontainsasubformulaoccurrenceoftheformλxtands0arisesfromreplacingthatsubformulaoccurrencewithλy[x7→y]t,providedyisnotfreeint.Theterm-convertstotheterms0ifscontainsasubformulaoccurrenceoftheform(λxt)t0ands0arisesfromreplacingthatsubformulaoccurrencewith[x7→t0]t.Theterm-convertstos0ifscontainsasubformulaoccurrenceoftheformλx(tx),wherexisnotfreeint,ands0arisesfromreplacingthatsubformulaoccurrencewitht.Thebinaryrelationofλ-conversionisdefinedsothat-convertstosifthereisalistoftermst1,...,tn,withn1,tequaltot1,sequaltotn,andfori=1,...,n1,eitherticonvertstoti+1orti+1convertstotibyα,β,orη.Expressionsoftheformλx(tx)arecalledη-redexes(providedxisnotfreeint)whileexpressionsoftheform(λxt)sarecalledβ-redexes.Atermisinλ-normalformifitcontainsnoβ-orη-redexes.Everytermcanbeconvertedtoaλ-normalterm,andthatnormaltermisuniqueuptothenameofboundvariables.Theexpressionλnorm(t)denotestheλ-normalformoft.See[6]forafullerdiscussionofthesebasicpropertiesofthesimplytypedλ-calculus.Todeneformulas,weshallnowconsiderthefollowingextensiontoterms.Letobethetypeofpropositions,whereoisassumednottobeamemberofS.Aconstantoftypeτ1→∙∙∙→τnowillbeusedtodenotepredicates;thatis,apredicateisdenotedbyafunc-tionalexpressionthattakesitsargumentstoaproposition.Thelogicalconstantsaregiventhefollowingtypes:,,arealloftypeooo;andτandτareoftype(τo)o,foralltypesτ.Weshallruleoutquantificationoverpredicatesbyrestrictingthetypeτinτandτnottocontainthetypesymbolo.Weshallassumethatthelogicalconstantsarenotmembersofanysignature.Aformulaisatermoftypeo.Thelogicalconstants,,arewritteninthefamiliarinfixform.Theexpressionsτ(λzt)andτ(λzt)arewrittensimplyasτztandτzt.AclosedformulaisaΣ-formulaifallofitsnon-logicalconstantsaremembersofΣ.Thesubstitutionoperationandconversionrelationsontermsimmediatelyextendtoformulas.4TwoLogicProgrammingLanguages4.1HereditaryHarropformulas:hhωOurfirstlogicprogramminglanguage,calledhhω,isbasedontwosetsofclosed,λ-normalformulas:D,whichcanbeusedasprogramclauses,andG,whichcanbeusedasgoalsorqueries.TheformulasinD,denotedbythesyntacticvariableD,arethosethatdonothaveanypositiveoccurrenceofadisjunctionorexistentialquantifier,whileformulasinG,denotedbythesyntacticvariableG,aretheirdual;thatis,formulasinGcannothaveanynegativeoccurrenceofadisjunctionorexistentialquantifier.Inordertoformalizeanotionofbackchainingoverclausesofthisgeneralform,weneedthefollowingdefinition.LetPbeafinitesubsetofD.Thesetofpairs|P|ΣisdefinedtobethesmallestsetsuchthatifD∈Pthenh∅,Di∈|P|Σ,ifhΓ,D1D2i∈|P|ΣthenhΓ,D1iandhΓ,D2iaremembersof|P|Σ,4
ifhΓ,GDi∈|P|ΣthenhΓ∪{G},Di∈|P|Σ,andifhΓ,τxDi∈|P|ΣandtisaΣ-term,thenhΓnorm([x7→t]D)i∈|P|Σ.Thefollowingpropositionhasbeenusedelsewheretojustifycallinghhωalogicprogramminglanguage[9,12].Proposition1LetΣbeasignature,letPbeafinitesubsetofD,let{G1,G2,τx.G,τx.G}⊆G,andletD∈D.Thenthefollowingholdsforintuitionisticprovability`.(WhenwewriteΣ;P`GweassumethatP∪{G}isasetofΣ-formulas.)Σ;P`G1G2ifandonlyifΣ;P`G1andΣ;P`G2.Σ;P`G1G2ifandonlyifΣ;P`G1orΣ;P`G2.Σ;P`∃τxGifandonlyifthereisaΣ-termtoftypeτsuchthatΣ;P`λnorm([x7→t]G).Σ;P`DG1ifandonlyifΣ;P∪{D}`G1.Σ;P`∀τx.GifandonlyifΣ∪{c:τ};P`[x7→c]G,wherecisaconstantoftypeτthatisnotinΣ.IfAisatomic,thenΣ;P`AifandonlyifforsomeΓ,hΓ,Ai∈|P|ΣandforeveryGΓ,Σ;P`G.Thispropositioninfactdescribesanon-deterministicinterpreterforhhω.Movingfromthispropositiontoanactualdeterministicinterpreterforhhωisadifficulttask.Variousaspectsofimplementingalanguagelikehhωhavebeenconsideredin[3,13].WementionacoupleaspectsinSection7.Inordertomotivateintroducingthenextlogicprogramminglanguage,itisimportanttomentionherethataninterpreterforhhωwillneedtoperformβ-reductionswhilelookingforproofs.Thatis,althoughprogramsandgoalsstartoutinλ-normalform,substitutionsmaycausethemtobecomenon-normal.Thus,referencestotheλnorm()functioninProposition1andinthedefinitionof|P|Σarenecessaryingeneral.Itisbecauseβ-conversioncancausesignificantchangestoatermthatunificationinthissettingisveryhard.Thenextlanguageweintroducewillberestrictedinsuchawaythatonlyaverysimplefragmentofgeneralβ-conversionisrequiredintheinterpreter.Asaresult,unificationinthatlanguagewillbeparticularlysimple.4.2Thesublanguage:LλAboundvariableoccurrenceinaformulaG∈Gisessentiallyuniversalifitisboundbyapositiveoccurrenceofauniversalquantifierorbya(term-level)λ-abstractioninG;itisessentiallyexistentialifitisboundbyeitherapositiveexistentialoranegativeuniversalquantifierinG.Dually:aboundvariableoccurrenceinaformulaD∈DisessentiallyexistentialifitisboundbyapositiveoccurrenceofauniversalornegativeoccurrenceofanexistentialquantifierinD;itisessentiallyuniversalifitisboundbyanegativeuniversalquantifierora(term-level)λ-abstractioninD.Intherunningofthenon-deterministicinterpreterdescribedabove,theessentiallyexistentialvariablescangetinstantiatedwithgeneralterms;itisviasubstitutionsforthesevariablesthatnewβ-redexescanappear.Oursecondlogicprogramminglanguage,calledLλ,isbasedontwosetsofλ-normalformulas:D0⊆D,whichcanbeusedasprogramclauses,andG0⊆G,whichcanbeusedasgoalsorqueries.5
Therestrictiontodeterminethesubsetsintendedisthefollowinginbothcases:wheneveranyformulainthesesetshasanessentiallyexistentialboundvariableoccurrence,sayx,appearingastheheadofanexpressionoftheform(xt1...tn)(n1)thent1,...,tnisalistofdistinctvariablesthatareessentiallyuniversallyquantifiedwithinthescopeofthebindingforx.Forexample,ifpredicatephastypejothentheformulaijxiy(p(xy)p(fy))isanexampleofbothagoalandprogramclauseforhhω;itisonlyalegalgoalinLλ.AsaclauseofLλ,ithasasubtermoccurrence(xy)wherebothxandyareessentiallyexistential.Suchasubtermisnotpremitted.AlltheformulasinSection2areinLλ.Ofcourse,first-orderHornclausesarebothgoalsandclausesinLλ.Giventhisrestrictiontothesyntaxofprogramclausesandgoals,theonlyβ-redexesthatmustbecomputedfromwithinaninterpreterforLλarethoseoftheform(λx.M)ywhereyisaboundvariablethatisnotfreeinλx.M.Suchβ-redexesareverysimpletoreduce:justchangefreeoccurrencesofxinMtoy.Giventhatα-conversionisavailable,thiscanbestatedevenmoresimply:atermtisrelatedtosbyβ0-conversionifoneisgottenfromtheotherbyreplacingaβ0-redex(λx.M)xinonewithMintheother.IftheinterpreterforhhωisgivenaprogramandgoaloftherestrictedlanguageLλ,theonlyβ-redexesthatneedtobereducedareβ0-redexes.Itisprovedin[10]thattheunificationproblemsthatarisefromwritinganinterpreterforLλ,sayβ0η-unificationproblems,aredecidableandmostgeneralunifiersexistswhenunifiersexist.ItisarguedinthatpaperthattheunificationneededforLλistheweakestextensionstofirst-orderunificationthattreatsboundvariablesdirectly.5SpecifyingEqualityandSubstitutionLettandsbetwoλ-normaltermsoftypeσ.Definethefollowingfunctionbyinductiononthestructureofsimpletypes.½λnorm(copyσts)ifσisprimitive[t,s:σ]=σ1xσ1u([x,u:σ1][(tx),(su):σ2])ifσisσ1σ2.(Thisrecursivedefinitionissimilartothatusedin[4]tocodeadependenttypedλ-calculusintohhω.)Forexample,theexpression[h,λx.(g(xa)a):(ij)i]yieldstheformulaijxiju(iyiv[copyiyvcopyj(xy)(uv)]copyi(hx)(g(ua)a)).NoticethattheclausesgiveninSection2areexactlytheclauses[a,a:i],[b,b:j],[f,f:ij],[g,g:jii],[h,h:(ij)i]ItisaneasymattertoshowthatsuchaformulaisalwaysbothagoalandaclauseforLλandthattheformula[t,s:σ]isaHornclauseifandonlyifσisoforder0or1.Thefollowingpropositionisstatedherewithoutproof.Itsproofisastraightforwardinductiononthestructureofproofs(whichmirrorsthestructureofβη-longnormalforms[6]).Proposition2LetΣcontainatleastthedistinctconstantsc1:σ1,...,cn:σn(n0).Lett1,...,tnbeΣ-termsoftypeσ1,...,σn,respectively,andletCbetheset{[ci,ti:σi]|i=1,...,n}.Finally,letMandNbeΣ-termsoftypeτ.ThenΣ;C`[M,N:τ]ifandonlyifMisa{c1,...,cn}-termand(λc1...λcn.M)t1...tnβη-convertstoN.6
Fromthisproposition,thefollowingcorollaryfollowsimmediately.Corollary1LetΣbeasignatureandletCΣbetheset{[c,c:σ]|c:σΣ}.IfMandNareΣ-termsoftypeτ,thenΣ;CΣ`[M,N:τ]ifandonlyifMβη-converts.NotIfMandNareΣ-termsoftypeστandτ,respectively,thenΣ;CΣ`∀σx([x,t:σ][Mx,N:τ])ifandonlyif(Mt)βη-convertstoN.Thus,itispossibletousetheformulas[c,c:σ]tohelpspecifybothequality(thatis,βη-conversion)andsubstitution.Toillustratehowsubstitutioncanbeaxiomatized,considerthefollowingLλclauseix(copyixTcopyi(Mx)S)substiiMTS.(Here,weshallstartadoptingthe(familiarProlog)conventionthatessentiallyexistentialvari-ableswillbecapitalizedlettersandthatifanyvariableisnotexplicitlyquantified,itisas-sumedtobeuniversallyquantifiedorexistentiallyquantifiedwithoutermostscopedependingonwhetherornottheformulaisintendedtobeaprogramclauseoragoal.)Thetypeofsubstiiis(ii)iio.AssumeforthemomentthatwehaveaProlog-likeinterpreterforLλ,andconsiderat-temptingtofindasubstitutiontermforthe(essentiallyexistential)variableFsothatthegoalsubstiiFa(gba)isprovablefromthisclauseandtheclausesinSection1.Backchainingwouldcausethisgoaltobereducedtoix(copyixacopyi(Fx)(gba)).Thisgoalisthenreducedbyintroducinganewconstant,sayc:i,andthenaddingtheclausecopyicatotheprogrambeforeattemptingtoprovethegoalcopyi(Fc)(gba).Noticethatsincecwasintroducedafterthe“logic”variableFwasintroduced,acorrectinterpreterforLλwouldneedtomakecertainthatFisnotinstantiatedwithatermthatcontainsc.Thereisonlyoneclause,namely[g,g:jii],onwhichtobackchaintoprovethisgoal.DoingsoreducesthisgoaltothetwogoalscopyjF1bandcopyiF2a,wherethedisagreementpairFc=gF1F2muststillbesolved.Thefirstofthesetwogoalshasexactlyonesolution,namelyF17→b,gottenbybackchainingoncopyjbb.Thesecondgoal,however,canbeprovedtwodifferentways:bybackchainingovereithercopyiaa,yieldingF27→aorcopyicayieldingF27→c.Puttingthesesubstitutionsbacktogether,wegettwodifferentsolutionstotheoriginalgoal:namelyF7→λw.(gba)bysolvingthedisagreementpairFc=gba,andF7→λw.(gbw)bysolvingthedisagreementpairFc=gbc.(ThepossiblesolutionF7→λw.gbcisruledoutsincecisnotpermittedtooccurfreeinthesubstitutiontermofF.)Notice,thatthesetwosubstitutionsareexactlythetwosolutionstotheβη-unificationproblemiiF.Fa=gba.Substitutioncanbeaxiomatizedinageneralfashionbyextendingtheexampleabove.As-sumethatwehavethepredicatessubstτσ:(τσ)τσoforeachpairoftypesτandσ.Thesepredicatesarethenaxiomatizedbythefollowingclausescheme:τx([x,T:τ][(Mx),S:σ])substτσMTS.7
Itfollowsimmediatelyfromthecorollaryabove,that,whenusedinconjunctionwiththeclauses{[c,c:σ]|c:σΣ},theseclausesprove(substτσMTS)ifandonlyif(MT)isβη-convertibletoS.NowassumethatMisoftheformλx.M0.Thecomputationoftheλ-normalformof(MT)happensintwosteps.First,TissubstitutedforfreeoccurrencesofxinM0.Itisthisstepthatthelogicalstructureofthesubstclausemakesexplicit.Thesecondsteprequiresanynewlyintroducedβ-redexestobereduced.Thisstepisnotmadeexplicitinthecodeabove:ifitneedstohappen,themeta-levelproofoperationmustperformthosereductions.Thus,thesubst-clausescannotgenerallybeLλprogramclauses.Forexample,theclausespecifyingsubstitutionattype(ij)iisijx(iYiV(copyiYVcopyj(xY)(TV))copyi(Mx)S)subst(ij)iMTS.ThisclauseisnotanLλprogramclausebecausetheessentiallyexistentialvariableThasanoccurrence(TV)whereitisappliedtoanotheressentiallyexistentialvariable.Newβ-redexes(whicharenotβ0-redexes)canbeintroducedatthispoint.Indefiningsubstτσ,ifthetypeτisprimitive,thennonewβ-redexeswillappearandthecorrespondingsubstclauseis,infact,inLλ(seetheaxiomatizationofsubstiiabove).ItispossibletoaxiomatizesubstcompletelyinLλ.Sinceitcanbedeterminedstaticallywhereβ-reductionswillneedtobeperformedwithinthecomputationofasubstgoal,itispossibletoreplacetheβ-redexwithanexplicitcalltosubst,thistimeatalowertype.Inparticular,ifτisfunctional,thensubstτσwillneedtocallsubstτ.Forexample,thefollowingisanLλspecificationofsubst(ij)i:ijx(iYiV(copyiYV⊃∀jU[substijTVUcopyj(xY)U])copyi(Mx)S)subst(ij)iMTS.Here,thepositivelyoccurringatomcopyj(xY)(TV)isreplacedwithjU[substijTVUcopyj(xY)U]:theβ-reductionneededtosimplify(TV)ismadeexplicitbythecalltosubstij.Thetwoimplementationsofsubstprovethesamegoals.Inthisfashion,weshallassumethatthepredicatessubstτσareallaxiomatizedcompletelyinLλ.ThetranslationofaclauseofhhωintoaclauseinLλgivenbythisexamplecanbegeneralized.Wepresentageneraltranslationinthenextsection.6TransforminghhωGoalsintoLλGoalsItispossibletosystematicallytranslateagoalinhhωintoagoalinLλsothattheproofsofthegoalinhhωdifferfromtheproofsinLλonlyinthatadditionalsubstandcopygoalsneedtobeestablished.Otherwise,allsubstitutionsmadeintheseproofsareidentical.SinceΣ;{D1,...,Dn}`GisequivalenttoΣ;∅`D1⊃∙∙∙⊃DnG,itisenoughtorestrictthistranslationtogoalformulasonly:itdualizesimmediatelyforprogramclauses.Forconvenience,weaxiomatizethepredicatesnsubstτ1→∙∙∙→τnσ:(τ1→∙∙∙→τnσ)τ1→∙∙∙→τnσotodoann-foldsubstitutioninthefollowingway:τ1x1([x1,T1:τ1]⊃∙∙∙⊃∀τnxn([xn,Tn:τn][Mx1∙∙∙xn,S:σ])...)substnMT1...TnS.8
Asbefore,theseclausescanbeadjustedsothattheyareactuallyLλprogramclauses.AsubtermofagoalformulaGwillbecalledanon-Lλsubtermifitisoftheform(Xt1∙∙∙tn)wheren1,XisessentiallyexistentialinG,andthetermst1,...,tndonotsatisfytherestrictionsdefiningLλ.ThetranslationfromhhωgoalstoLλgoalsisbyinductiononthenumberofnon-Lλsubtermoccurrences.LetG∈G.IfGisnotanLλgoal,thenthereisanoccurrenceofanatomicformulaAinGwhichhasasubtermoftheform(Xt1∙∙∙tn)wheren,Xandt1,...,tnareasabove.Lety1,...,ym(m0)bethelistofessentiallyuniversalvariablesthatareboundinthescopeofX’sbindingoccurrenceandthatalsocontain(Xt1∙∙∙tn)intheirscope.Letσ1,...,σmbethetypesofy1,...,ym,respectively.LetHbeavariablenotoccurringfreeinAandletA0betheresultofreplacingtheoccurrenceof(Xt1∙∙∙tn)with(Hy1...ym).LetG0betheresultofreplacingAwitheithertheexpressionH([σ1y1([y1,y1:σ1]⊃∙∙∙⊃∀σmym([ym,ym:σm]substnXt1...tn(Hy1...ym))∙∙∙)]A0)ifAoccursnegativelyinG,orH([σ1y1([y1,y1:σ1]⊃∙∙∙⊃∀σmym([ym,ym:σm]substnXt1∙∙∙tn(Hy1...ym))...)]A0)ifAoccurspositivelyinG.Theresultingformulanowhasonefewernon-Lλsubterms.Ifwerepeatthisprocessuntilallsuchsubtermsareremoved,theresultwillbeanLλgoalformula.Thefollowingpropositionestablishesasimplecorrectnesspropertyforthistranslation.Proposition3LetΣbeasignature,letCΣbetheset{[c,c:σ]|c:σΣ},andletGbeanhhωgoalformulathatdoesnotcontainoccurrencesofanycopyorsubstpredicates.LetG00betheLλgoalthatresultsfromperformingtheabovementionedtranslationstothehhωgoalformulaG.ThenΣ;∅`GifandonlyifΣ;CΣ`G00.Furthermore,ifGisoftheformτX.HthenG00isoftheformτX.H00,andforallΣ-termstoftypeτ,Σ;∅`λnorm([X7→t]H)ifandonlyifΣ;CΣ`λnorm([X7→t]H00).Inotherwords,answerssubstitutionsarethesamebetweenthesetwogoals.Considertheβη-unificationproblemiiX[k(λv(m(Xv)))=k(λy(X(my)))],overthesignature{m:ii,k:(ii)i}.ThiscanbewrittenasthehhωgoaliZ(eqZZ)⊃∃iiX[eq(k(λv(m(Xv))))(k(λy(X(my))))].Thisqueryhasonenon-Lλsubterm,namely,(X(my)).Usingtheabovementionedtransfor-mationleadstotheLλgoaliZ(eqZZ)⊃∃iiXiiH[iy(copyiyysubstiiX(my)(Hy))eq(k(λv(m(Xv))))(k(λy(Hy)))].Solvingthisqueryusingthecopy-clausesfortheconstantsmandk,wefindthatthereareaninfinitenumberofproofs,yieldingasequenceofsubstitutiontermsforX,namely,λw.w,λw.(fw),λw.(f(fw)),etc.Thesearethustheunifiersfortheoriginalβη-unificationproblem.9
Be the first to leave a comment!!

12/1000 maximum characters.