La lecture en ligne est gratuite
Read Download

Share this publication

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