1 Ahigher-orderimplementationofrewriting LawrencePaulson ComputerLaboratory UniversityofCambridge CornExchangeStreet CambridgeCB23QG England Abstract Manyautomatictheorem-proversrelyonrewriting.Usingtheoremsasrewriteruleshelpsto simplifythesubgoalsthatariseduringaproof. LCFisaninteractivetheorem-proverintendedforreasoningaboutcomputation.Its implementationofrewritingispresentedindetail.LCFprovidesafamilyofrewritingfunctions, andoperatorstocombinethem.Asuccessionoffunctionsisdescribed,frompatternmatching primitivestotherewritingtoolthatperformsmostinferencesinLCFproofs. Thedesignishighlymodular.Eachfunctionperformsabasic,specifictask,suchas recognizingacertainformoftautology.Eachoperatorimplementsonemethodofbuildinga rewritingfunctionfromsimplerones.Thesepiecescanbeputtogetherinnumerousways, yieldingavarietyofrewritingstrategies. Theapproachinvolvesprogrammingwithhigher-orderfunctions.Rewritingfunctionsare datavalues,producedbycomputationonotherrewritingfunctions.Thecodeisindailyuseat Cambridge,demonstratingthepracticaluseoffunctionalprogramming.

2 1.Introductiontorewriting Whentryingtoproveatheorem,oneapproachistosimplifyitbyapplyingleft-to-right rewriterules.Forexample,considertheproofthatadditionofnaturalnumbersisassociative. Wecantakethenaturalnumberstohavetheform0,SUCC(0),SUCC(SUCC(0)),...,anddefine additionusingtheaxioms 0+n=n SUCC(m)+n=SUCC(m+n) Associativityofadditioncanbestated (m+n)+k=m+(n+k) Inductiononmreducestheproblemtoprovingthetwogoals: (0+n)+k=0+(n+k) (basecase) (SUCC(m)+n)+k=SUCC(m)+(n+k)(stepcase) withinductionhypothesis (m+n)+k=m+(n+k) Whenconductingsuchaproofbyhand,wewouldnotevenwritedownanexpressionlike 0+(n+k),butwouldcrossoutthe0immediately,provingthebasecase.Forthestepcase,we wouldexpandoutbothsides,writing leftside: (SUCC(m)+n)+k=(bydefinitionofaddition) SUCC(m+n)+k=(bydefinitionofaddition) SUCC((m+n)+k)=(byinductionhypothesis) SUCC(m+(n+k)) rightside: SUCC(m)+(n+k)=(bydefinitionofaddition) SUCC(m+(n+k)) QED Notethatthecancellingofthe0in0+(n+k)canberegardedastherewritingof0+(n+k), usingthefirstaxiomofadditionasarewriterule.Theotheradditionaxiom,andtheinduction hypothesis,arealsousedasrewriterulesintheproof. Rewritingisfundamentaltomostresearchonprovingtheoremsbycomputer [$boyer79,$cohn83,$paulson83a].Manytheoremscanbeprovedbyinductionandrewriting,or evenbyrewritingalone.Fortheorieswhereallaxiomsareequations,itissometimespossibleto proveadditionalequationsandachieveacompletesetofrewriterules,capableofrewritingany 3 termintocanonicalform[$huet80].Thisprovidesadecisionprocedurefortestingthevalidityof anyequationofthetheory. Thereisawidevarietyofrewritingstrategies,asKuechlin[$kuechlin82]thoroughly discusses.Inwhatordershouldrewriterulesbeconsideredifmorethanoneapplies?What aboutloopingrewritessuchasm+n=n+m?Shouldatermberewrittenagainandagainuntilno rulesapply,oronlyaboundednumberoftimes?Shouldatermbetraversedtop-downorbottom-up,left-to-rightorright-to-left?Andhowcanwemakeuseofrewritesthathavepre-conditions, suchas ifmisnotzerothen(m*n)/m=n? Thispaperpresentsafamilyofrewritingprimitives,andoperatorstocombinethem.It proceedsinstages,frompattern-matchingprimitives,toinstantiationfunctions,termandformula rewritingfunctions,tautologysolvers,finallydiscussingtherewritingtheorem-proverthatis providedintheLCFsystem[$paulson83a].Thefunctionsateachstageareconstructedfrom thoseofthepreviousstagebyfunctionaloperatorsthatexpresssimplecomputationalintuitions suchassequencing,alternation,andrepetition. Mostfunctiondefinitionsarebriefanddirectlyexpressthedesigndecisionssuchastraversal order.Eventhetheorem-provingfunctionisonlytwelvelines,whichformareadablesummaryof itsrewritingstrategy.Ifyoudislikethestandardstrategy,youcaneasilyimplementanother. Thismodularityisinsharpconstrasttolarge,monolithicimplementationsofrewriting,suchas LCF’spreviousone. Higher-orderfunctionsplayavitalrole.Therewritingprimitivesarefunctions,the operatorsarefunctionals.ThemethodisimplementedintheprogramminglanguageML [$gordon79,$gordon82].ItcannotbeimplementedinBackus’sFPlanguage[$backus78],which allowsonlyfirst-orderfunctions. 2.TheLCFproofassistant LCFisaninteractivetheorem-proverforDanaScott’sLogicforComputableFunctions [$gordon79].Thislogic,calledPPLAMBDA,providesthe"undefined"elementUUandthe associatedpartialordering;itallowsreasoningaboutdenotationalsemantics,programsthat manipulateunboundedstreams,etc.LCFletsyoudeclareconstantsandtypes,assertaxioms, andprovetheorems;itrecordsallthisinformationinatheoryfile.Youcanbuildatheoryontop ofothertheories,inheritingtheconstants,axioms,etc.oftheothertheories.Amajorverification projectmightinvolveatheoryhierarchycontainingtheoriesoflists,naturalnumbers,sets, specializeddatastructures,andtheoriesofincreasinglycomplexfunctionsoperatingonthese types. LCFliesmid-waybetweenastep-by-stepproofchecker,andanautomatictheorem-prover. Whenconductingaproof,youareresponsibleforperformingeachlogicalinference.Youmay automatepartsofthistaskbywritingprogramsinthemeta-language,ML.Thestandard theorem-provingtools,suchastherewritingfunctions,arewritteninML.MLtreatstheterms andformulasofPPLAMBDAasdatavalues,providingfunctionstobuildthemandtakethem apart.Theoremsarealsodatavalues.

4 PPLAMBDAisanaturaldeductionlogic[$manna74]:theoremsareprovedrelativetoaset ofassumptions.Atheorem[A1;...;An]|-BmeansthattheconclusionBholdswheneverthe assumptionsA1,...,Anhold.(Theconclusionandassumptionsareformulas.)InML,atheorem isavalueoftheabstracttypethm,representedbyapair([A1;...;An],B).Suchapairis traditionallycalledasequent. MLprovidesfunctionstodecomposeatheoremintoitsconclusionandassumptions,butnot toconstructanarbitrarytheorem.Theoremsmustbeprovedbyapplyinginferencerulesto axioms.LCFusestypicalintroduction/eliminationinferencerules,implementedasfunctions whoseargumentsandresultshavetypethm.Type-checkingguaranteesthatinferencerulesare onlyappliedtotheorems. Mostproofsareconductedbackwards,startingfromthedesiredgoal(expressedasa sequent).Thegoalisreducedtosimplersubgoals,andthosereducedtofurthersubgoals,untilall thesubgoalshavebeenreducedtotautologies.Backwardsproofusestactics.Atacticisa functionthatmapsagoaltoalistofsubgoals,pairedwithaninferencerule.Theinferencerule justifiesthechoiceofsubgoals.Giventheoremsthatassertthesubgoals,itproducesatheorem thatassertsthegoal. Tacticscorrespondtosimplereasoningmethods.Forinstance,theconjunctiontactic CONJTACreducesanygoaloftheformA/\BtothetwosubgoalsAandB;thedischargetactic DISCHTACreducesanygoaloftheformA==>BtothesubgoalofprovingBunderthe assumptionA.Ifyouapplyatactictoagoalthatitcannothandle,thenitwillfailviaML’s exceptionmechanism(describedbelow). ItwouldbetediousindeedtoprovetheoremsinsuchtinystepsasCONJTACand DISCHTAC.Mostinteractiveproofsrelyonmorepowerfultactics,constructedfromthe primitiveonesusingfunctionscalledtacticals.ThebasiconesareTHEN,ORELSE,and REPEAT. tac1THENtac2 appliestac1,thenappliestac2toallresultingsubgoals tac1ORELSEtac2 appliestac1,ifitfailsthenappliestac2 REPEATtac appliestacrecursivelyonthegoalandtheresultingsubgoals, returningthesubgoalsforwhichtacfails Youmaybesurprisedtoseetheimperativenotionsofsequencing,alternation,and repetitionembodiedinhigher-orderfunctionsthatmanipulateproofstrategies.Thispaperwill showthatthesamenotionsapplytorewriting.

5 3.ReferencesummaryofML ThissectiondescribesjustenoughofMLtoenableyoutofollowtherestofthepaper.For instance,ML’spolymorphictypesystemisnotdiscussedbecausemostofthefunctionsinthis paperarestronglytyped.Gordon[$gordon82]givesagoodintroductiontoMLanditsusein theorem-proving.TheEdinburghLCFManual[$gordon79]alsocontainsanintroductiontoML, andishelpfultohaveathandifyouintendtostudythepaperindetail. Note:thispaperconcernsCambridgeLCF,arevisedversionofEdinburghLCF.Mostof thechangesinvolvethelogicPPLAMBDA[$paulson83c].Despiteincompatibilities, documentationonEdinburghLCFisstilluseful. 3.1.Values ValuesofthelanguageMLinclude *theintegers0,1,2,...,withoperators+,-,*,/,etc. *thebooleanstrueandfalse,withoperators&,or,not,alongwiththeconditionalexpression: ifbthenxelsey *tokens,whicharecharacterstringssuchas‘NOCONV‘or‘HiDaddy‘ *pairssuchas0,true--whichmaybeiteratedtoformtuples:‘manny‘,‘moe‘,‘jack‘ *lists[x1;...;xn],suchas[(0,true);(1,false)] *functions,whichmaybepassedasvalues,retainingtheiroriginalvariablebindingseven outsideofthescopewheretheywerecreated *terms,formulas,theoremsofthelogicPPLAMBDA 3.2.Types Typesinclude int(integers) bool(booleans) tok(tokens) a#b(pairswithcomponentsofthetypesaandb) alist(listswithelementsoftypea) a->b(functionsfromatob) term(PPLAMBDAterms) form(PPLAMBDAformulas) thm(PPLAMBDAtheorems)

6 3.3.Declarations Typedattoplevel,thedeclaration letx=3;; causesxtodenote3fortherestoftheterminalsession.Insideaprogram,thedeclaration letx=3inx+x causesxtodenote3onlyintheexpressionx+x.Alocaldeclarationsupersedesanyglobalone, usingstaticscoperules. Declarationsinclude letx=3(values) letdoublek=k+k(functions) lettimesxy=x*y(curriedfunctions) letrecfactn=(recursivefunctions) ifn=0then1 elsetimesn(fact(n-1)) Notethatparenthesesarenotrequiredaroundargumentstofunctions.Thusdoublek meansthesameasdouble(k). 3.4.Trappingfailures Anattempttoperformanillegaloperation,suchasdivisionbyzero,causesMLtosignal failure.Eachfailurehasanassociatederrormessage,orfailuretoken.Aprogramcansignal failureviatheexpression failwith‘myerror‘ Afailurehaltsexecutionunlessitistrapped.Evaluatingtheexpressionx?ycomputesthe valueofx;ifxfails,thenitcomputesthevalueofy. Somepeopleobjecttofailuretrapping,comparingittoagotostatement.Theypreferto useconditionalexpressionstopreventfailuresfromoccurring.Thisisimpracticalforcombining proofstrategies,wheresuccessorfailureisdifficulttopredict.Thoughimplementedasagoto, failurecanbeunderstoodasanerrorvaluethatispassedalonguntilitistestedfor.Acommon useoffailureistorejectinputsthatdonotmatchanexpectedpattern.

7 3.5.Standardfunctionsandoperators Infixoperatorsinclude .--"conses"anelementtothefrontofalist x.[y1;...;yn]--->[x;y1;...;yn] @--appendstwolists [x1;...;xm]@[y1;...;yn]--->[x1;...;xm;y1;...yn] o--composestwofunctions (fog)x--->f(gx) Functionsinclude map--appliesafunctiontoeachelementofalist mapf[x1;...;xn]--->[fx1;...;fxn] mapfilter--likemapbutdoesnotpropagatefailure;ignoresany listelementsforwhichffails flat--flattensalistoflistsintoalist flat[l1;...;ln]--->l1@...@ln itlist--iteratesdownalist,accumulatingaresult itlistf[x1;...;xn]y--->fx1(f...(fxny)) fst,snd--selectcomponentsofpairs fst(x,y)--->x snd(x,y)--->y 3.6.ManipulatingPPLAMBDAabstractsyntax ThetermsofPPLAMBDA,whichdenotecomputablevalues,areelementsoftheMLtype term.Termshavefourabstractsyntaxclasses: C(constant,whereCisaconstantsymbol) x(variable) \x.t(lambda-abstraction) tu(combination,orfunctionapplication) Thereissyntacticsugarforcertaincommonexpressions: p=>t|u(conditionalexpression,actually"CONDptu") t,u(pair,actually"PAIRtu")

8 Youmaydeclareconstantsymbols;thestandardonesinclude UU(bottom,orundefinedelement) TT(true,acomputabletruthvalue) FF(false) FST(aselectorfunction,likefstinML) SND(likesndinML) Note:thoughnotdiscussedhere,PPLAMBDAtermsobeyapolymorphictypesystem similartoML’s. TheformulasofPPLAMBDA,whichdenotelogicalstatements,areelementsoftheMLtype form.Formulashavesevenabstactsyntaxclasses: !x.A(universalquantifier) ?x.A(existentialquantifier) A/\B(conjunction) A\/B(disjunction) A==>B(implication) A<=>B(if-and-only-if) Pt(predicate,wherePisapredicatesymbol) Standardformulasinclude TRUTH()(standardtautologypredicate) FALSITY()(standardcontradictionpredicate) t==u(equivalenceoftandu,actually"equiv(t,u)") t<<u(Scottinequivalenceoftandu,actually"inequiv(t,u)") ˜ A(negation,actually"A==>FALSITY()") Note:theformulat==uexpressesequivalenceratherthanequality.Roughlyspeaking,t anduareequivalentiftheyarebothundefined,orbothdefinedandequal. TheMLexpressionforconstructingaPPLAMBDAobject(termorformula)consistsofthat objectenclosedinquotationmarks.Thesearesyntaxtrees,notcharacterstrings!MLprovides destructorfunctionsfortakingapartPPLAMBDAobjects. destcomb"fx"--->"f","x" destequiv"t==u"--->"t","u" destconj"A/\B"--->"A","B" destimp"A==>B"--->"A","B" etc. ThetheoremsofPPLAMBDA,whichdenoteprovedformulas,areelementsoftheMLtype thm.Inferencerulesareprovidedasfunctionsthatproducetheorems.Forinstance,thefunction MPimplementsModusPonens.

9 MP"|-A==>B""|-A"--->"|-B" Note:thisexample,andothersbelow,showtheoremsinquotationmarks.Thesedepict valuesratherthanexpressions.MLdoesnotallowquotedtheoremsasexpressions,sincethey wouldconstructtheoremswithoutproof.InferenceruleslikeMPmustbeappliedtoidentifiersor otherexpressionsoftypethm. Thefunctionconclreturnstheconclusionofatheorem. concl"[A1;...;An]|-B"--->"B" 4.Patternmatchingprimitives NowwearereadytoexamineLCF’srewritingfunctions,startingwithprimitivesand workingupwards.TheMLprogramsbelowomitmostPPLAMBDAinferences,aswellascodefor optimizationanddebugging.Themostfrequentlyusedinferencesare"wiredin"asadditional primitives,toavoidderivingthemrepeatedly.However,theprogramsrunninginLCFare essentiallyasdescribedhere. Aquantifiedtheoremsuchas|-!x.Astandsforaninfinityoftheorems,oneforeachx.Ina proof,youarelikelytoneedsomeoftheseinstances,ratherthanthegeneralform.LCF’spattern matchingprimitivesrelieveyouofthetediumofinstantiatingtheorems. 4.1.Matchingtermsandformulas Mostrewritingfunctionsdependonthematchingfunctionstermmatchandformmatch.If patternandobjectareterms,thecall termmatchpatternobject returnsalistof(term,variable)pairs.Thisexpressestheobjectasaninstanceofthepattern (allowingforrenamingofboundvariables).Ifnomatchexists,termmatchfails.Theanalogous functionforformulasisformmatch. Letuslookataterminalsessionusingthesefunctions.Thelinesbeginningwith#denote inputtoLCF,andtheotherlinesdenotetheresponse. Webindacomplexterm,aconditional,totheMLidentifiertmobj.MLrespondsby printingthevalueanditstype. #lettmobj="TT=>(FF,TT)|(TT,FF)";; tmobj="(TT=>(FF,TT)|(TT,FF))":term 10 Avariablecanbematchedtotheterm.(Theresultingmatchincludesalistfor PPLAMBDAtypessuchas":*",whichweignoreforsimplicity.) #termmatch"x"tmobj;; ["(TT=>(FF,TT)|(TT,FF))","x"], [":tr#tr",":*"] :((term#term)list#(type#type)list) Thetermcanbematchedagainstaconditional,breakingitintoparts. #termmatch"p=>x|y"tmobj;; ["TT,FF","y";"FF,TT","x";"TT","p"], [":tr#tr",":*"] :((term#term)list#(type#type)list) Since"p=>x|y"ismerelysyntacticsugarfor"CONDpxy",wecanalsomatchtheterm againstacombination. #termmatch"fx"tmobj;; ["TT,FF","x";"CONDTT(FF,TT)","f"], [":tr#tr",":**";":tr#tr",":*"] :((term#term)list#(type#type)list) Wecannotmatchthetermagainstsomethingofadifferentform.Ifwetry,termmatch fails. #termmatch"p=>FF|y"tmobj;; evaluationfailedtermmatch #termmatch"\p.p"tmobj;; evaluationfailedtermmatch Wecanconductasimilarsessionusingformmatch. #letfmobj="!x.(x,TT)==UU";; fmobj="!x.(x,TT)==UU":form #formmatch"!y.(x,y)==UU"fmobj;; evaluationfailedformmatch #formmatch"?x.(x,TT)==UU"fmobj;; evaluationfailedformmatch #formmatch"!y.(y,z)==UU"fmobj;; ["TT","z"], [":tr",":**"] :((term#term)list#(type#type)list)

11 4.2.Instantiatingtheoremsbymatching Thefunctionstermmatchandformmatcharetooprimitiveformostapplications.Their mainpurposeistoimplementthenextlevelofabstraction,whichprovidesfunctionsfor instantiatingtheorems.Calling PARTTMATCHpartfnAt matchesthetermttosomepartofthetheoremAobtainedbythefunctionpartfn,andreturnsA withitstypesandvariablesinstantiated.Thepartfniscomposedfromdestructorfunctionssuch asfst,destcomb,anddestequiv.Itisappliedtotheconclusionofthetheoremafterremoving outeruniversalquantifiers. PARTTMATCHmakesiteasytodefineinferencerulesthatinvolvematching.For instance,PPLAMBDAincludesanaxiomstatingthatthebottomelementissmallerthanany otherelement. MINIMAL|-!x.UU<<x InstantiatingMINIMALisinconvenient(notonlyx,butPPLAMBDAtypesmustbe instantiated),soLCFprovidesaninferenceruleMINthatmapsanytermttothetheorem |-UU<<t.ThisrulecanbeexpressedusingPARTTMATCHandthefunction (sndodestinequiv): letMIN=PARTTMATCH(sndodestinequiv)MINIMAL;; LetusseehowPARTTMATCHdetermineswhatpartofMINIMALtomatchagainst. Thiscomputationtakesplacebeforeatermtisapplied,sincePARTTMATCHisacurried function. (sndodestinequiv)(concl"|-UU<<x") snd(destinequiv"UU<<x") snd("UU","x")

"x"

SoMINmatchesatermtagainsttheright-hand-side,x,returningtheinstance|-UU<<tof MINIMAL. ThefunctionPARTFMATCHisanalogous,butmatchessomesubformulaofthetheorem ratherthanasubterm.Oneofitsapplicationsisasimpleresolutionrule,MATCHMP.Thisisa ModusPonensthatmatchesanimplicationtoanantecedent. letMATCHMPimpth= letmatch=PARTFMATCH(fstodestimp)impth in \th.MP(match(conclth))th;; 12 CallingMATCHMP"|-!x1...xn.A==>B""|-A’",whereA’isaninstanceofA,returns thecorrespondinginstanceofB.Byconvention,letuswritethisinstance|-B’.Thecomposite function(fstodestimp)takesthefirstpartofanimplication,whichistheantecedent.Oneof myproofs[$paulson83a]involvesatotalfunctionVARSOFandatheoryofstrictlists.The functionMAP,whichmapsanyfunctionfoveralist,producesatotalfunctioniffistotal.The ruleMATCHMPcanprovethatthefunction(MAPVARSOF)istotal. Firstweload,fromtheoryfiles,twotheoremsabouttotality. #letVARSOFTOTAL=theorem‘VARSOF‘‘VARSOFTOTAL‘;; VARSOFTOTAL="|-!t.˜ t==UU==>˜ VARSOFt==UU":thm #letMAPTOTAL=theorem‘listfun‘‘MAPTOTAL‘;; MAPTOTAL= "|-!f. (!x.˜ x==UU==>˜ fx==UU)==> (!l.˜ l==UU==>˜ MAPfl==UU)" :thm UsingMATCHMP,wegeneratemoretotalitytheorems. #letTOTAL1=MATCHMPMAPTOTALVARSOFTOTAL;; TOTAL1="|-!l.˜ l==UU==>˜ MAPVARSOFl==UU":thm #letTOTAL2=MATCHMPMAPTOTALTOTAL1;; TOTAL2="|-!l.˜ l==UU==>˜ MAP(MAPVARSOF)l==UU":thm #letTOTAL3=MATCHMPMAPTOTALTOTAL2;; TOTAL3="|-!l.˜ l==UU==>˜ MAP(MAP(MAPVARSOF))l==UU":thm 5.Termconversions Thepurposeofrewritingistoconvertanytermtintoatermuthatissomehowsimpler. Furthermore,umustbeprovedequivalenttot.Mosttheorem-proverstakeforgrantedthattheir rewritingfunctionsarereliable,buttheLCFmethodologydemandsthateveryrewritingstepbe justifiedbyatheorem. LCF’srewritingfunctionsarecalledconversions.Atermconversionisanyfunctionthat mapsatermttoatheorem|-t==u.Thisconvertsthetermttoanothertermu,andprovesthe twoequivalent.SinceMLallowsustotaketheoremsapart,wecanextractthenewtermufrom thetheorem|-t==u. LetusbindsomeMLidentifierstotermsforuseinlaterterminalsessions.(This simultaneousdeclarationresemblesLisp’s"destructuringlet".)

13 #let[abs1;abs2;condu;condt;condf;condfst]=exampleterms;; abs1="(\fun.(fun(TT,FF)=>x|y))FST":term abs2="(\t.(\u.t,u)FF)TT":term condu="(UU=>(TT,FF,p)|(q,TT,q))":term condt="(TT=>x|y)":term condf="(FF=>fx|fy)":term condfst="(FST(TT,FF)=>x|y)":term 5.1.Basicconversions Betaconversion,BETACONV,isstandardinLCF.Ifxisavariable,andu,vareterms, andu[v/x]denotesthesubstitutionofvforxinu,then BETACONV"(\x.u)v"--->"|-(\x.u)v==u[v/x]" ThissessiondemonstratesthatBETACONVperformsexactlyonebeta-conversion,nottwo orzero. #BETACONVabs1;; "|-(\fun.(fun(TT,FF)=>x|y))FST==(FST(TT,FF)=>x|y)":thm #BETACONVabs2;; "|-(\t.(\u.t,u)FF)TT==(\u.TT,u)FF":thm #BETACONVcondt;; evaluationfailedBETACONV Anotherbasicconversionistorewriteaccordingtoatheoremthatstatesanequivalence. Suchtheoremsarecalledrewritesortermrewrites. REWRITECONV"|-!x1...xn.t==u" Thisconversiontakesanyinstanceoft,suchast’,andinstantiatesthevariablesx1...xn,to returnthetheorem|-t’==u’.ItisimplementedusingthematchingfunctionPARTTMATCH: letREWRITECONV=PARTTMATCH(fstodestequiv);; LetusexploreREWRITECONV.FirstwebindsomePPLAMBDAaxiomstoidentifiers, foruseinlatersessions.

14 #let[CONDUU;CONDTT;CONDFF; #MINCOMB;MINABS; #MKPAIR;FSTPAIR;SNDPAIR] #=examplerewrites;; CONDUU="|-(UU=>x|y)==UU":thm CONDTT="|-(TT=>x|y)==x":thm CONDFF="|-(FF=>x|y)==y":thm MINCOMB="|-UUx==UU":thm MINABS="|-\x.UU==UU":thm MKPAIR="|-FSTx,SNDx==x":thm FSTPAIR="|-FST(x,y)==x":thm SNDPAIR="|-SND(x,y)==y":thm WebuildaconversionfromFSTPAIR.ItcansimplifytermsbeginningwithFST,butnot thosebeginningwithSND. #letFSTCONV=REWRITECONVFSTPAIR;; FSTCONV=-:conv #FSTCONV"FST(TT,FF)";; "|-FST(TT,FF)==TT":thm #FSTCONV"SND(TT,FF)";; evaluationfailedtermmatch WebuildaconversionfromCONDTTanduseittosimplifyaterm. #letCONDTTCONV=REWRITECONVCONDTT;; CONDTTCONV=-:conv #CONDTTCONVcondt;; "|-(TT=>x|y)==x":thm ThisconversioninsiststhattheconditionbeTT,notnoticingthatFST(TT,FF)hasthe samevalue. #CONDTTCONVcondfst;; evaluationfailedtermmatch 5.2.Combiningconversions Wehaveoperators,similartotacticals,forcombiningBETACONVandREWRITECONV intomorepowerfulconversions. TheoperatorORELSECprovidesthenotionofalternation.Forconversionsconv1and conv2,andtermt,theconversion 15 (conv1ORELSECconv2)t--->conv1t?conv2t Ittriesconv1;ifthatfails,thenittriesconv2. UsingORELSEC,wecanimplementaconversionforconditionalsthathandlesbothTTand FF,thoughstillnotFST(TT,FF). #letCONDTFCONV= #(REWRITECONVCONDTT)ORELSEC #(REWRITECONVCONDFF);; CONDTFCONV=-:conv #CONDTFCONVcondt;; "|-(TT=>x|y)==x":thm #CONDTFCONVcondf;; "|-(FF=>fx|fy)==fy":thm #CONDTFCONVcondfst;; evaluationfailedtermmatch Wecanalsoimplementthenotionofsequencing,defininganoperatorTHENC.For conversionsconv1andconv2,theconversion (conv1THENCconv2)t derives |-t==t1(byconv1) |-t1==t2(byconv2) andreturns |-t==t2(bytransitivity,failingifconv1orconv2does) NotethatTHENCjustifiesitsresultusingthejustificationsproducedbyconv1andconv2. UsingTHENC,wecanimplementadoublebeta-conversion,whichfailsifonlyonebeta-conversionispossible. #letBETABETACONV=BETACONVTHENCBETACONV;; BETABETACONV=-:conv #BETABETACONVabs1;; evaluationfailedBETACONV #BETABETACONVabs2;; "|-(\t.(\u.t,u)FF)TT==TT,FF":thm 16 BothORELSECandTHENChaveidentityelements.TheconversionNOCONVappliesto noterms;italwaysfails.TheconversionALLCONVappliestoall;itmapsanytermttothe theorem|-t==t. #NOCONVcondt;; evaluationfailedNOCONV #ALLCONVcondfst;; "|-(FST(TT,FF)=>x|y)==(FST(TT,FF)=>x|y)":thm Forcombiningseveralconversionsintoamulti-waychoice,useFIRSTCONV.Itisdefined usingitlist,ORELSEC,andNOCONV. FIRSTCONV[conv1;...;convn]---> conv1ORELSEC...ORELSECconvn UsingFIRSTCONV,wecanimplementaconversionforconditionalsthathandlesthe conditionsUU,FF,andTT. #letCONDCONV= #FIRSTCONV(mapREWRITECONV[CONDTT;CONDFF;CONDUU]);; CONDCONV=-:conv #CONDCONVcondu;; "|-(UU=>(TT,FF,p)|(q,TT,q))==UU":thm #CONDCONVcondf;; "|-(FF=>fx|fy)==fy":thm #CONDCONVcondt;; "|-(TT=>x|y)==x":thm #CONDCONVcondfst;; evaluationfailedFIRSTCONV Theseoperatorsresembletacticals.THENCandTHENbothexpresssequencing; ORELSECandORELSEbothexpressalternation.ThetacticALLTAC,whichpassesonits goalunchanged,istheidentityforTHEN.(ALLTACiscalledIDTACinEdinburghLCF.)The tacticNOTAC,whichfailsonallgoals,istheidentityforORELSE.ORELSECandNOCONV areimplementedlikeORELSEandNOTAC,usingfailure.Mostremarkably,wecandefine repetitionforconversionsexactlyasitisdefinedfortactics. letrecREPEATCconvt= ((convTHENC(REPEATCconv))ORELSECALLCONV)t;; Afinepoint:Withouttheabstractionovert,REPEATCwouldalwaysloop,becauseML usesapplicativeorder(eager)evaluationratherthannormalorder(lazy)evaluation.

17 UsingREPEATC,wecanimplementafunctionthatperformsasmanytop-levelbeta-conversionsaspossible. #letBETANCONV=REPEATCBETACONV;; BETANCONV=-:conv #BETANCONVabs1;; "|-(\fun.(fun(TT,FF)=>x|y))FST==(FST(TT,FF)=>x|y)":thm #BETANCONVabs2;; "|-(\t.(\u.t,u)FF)TT==TT,FF":thm #BETANCONVcondt;; "|-(TT=>x|y)==(TT=>x|y)":thm 5.3.Depthconversions Nowwestepbeyondtheanalogywithtacticals,andexamineconversionsthattraverseterms recursively.LCFprovidesfunctionsforconvertingsubterms:COMBCONVhandles combinations,whileABSCONVhandlesabstractions.Theyfailontermsthatdonothavethe correspondingform. Theconversion(COMBCONVconv"ft")derives |-f==g(byconv) |-t==u(byconv) andreturns |-ft==gu(bysubstitution) Theconversion(ABSCONVconv"\x.t")derives |-t==u(byconv) andreturns |-\x.t==\x.u(byextensionality,possiblyrenamingx) LetuscombineCOMBCONVandABSCONVintoaconversionforaterm’stop-level subterms.Recallthatatermcanbeaconstant,variable,abstraction,orcombination.Constants andvariablesareleftunchanged,usingALLCONV: letSUBCONVconv= FIRSTCONV[COMBCONVconv;ABSCONVconv;ALLCONV];; NowitissimpletowriteaconversionDEPTHCONVthatrecursivelyrewritesallsubterms ofaterm,indepth-firstorder.

18 letrecDEPTHCONVconvt= (SUBCONV(DEPTHCONVconv)THENC(REPEATCconv))t;; TotryDEPTHCONVout,wefirstmakeatop-levelconversionthatincludesbeta-conversionandallourrewrites. #letMANYCONV= #FIRSTCONV(mapREWRITECONVrewrites)ORELSEC #BETACONV;; MANYCONV=-:conv NowwemakeadepthconversionfromMANYCONVandtryitonsomeexamples. #letDCONV=DEPTHCONVMANYCONV;; DCONV=-:conv #DCONVabs2;; "|-(\t.(\u.t,u)FF)TT==TT,FF":thm #DCONVcondfst;; "|-(FST(TT,FF)=>x|y)==x":thm #DCONVabs1;; "|-(\fun.(fun(TT,FF)=>x|y))FST==(FST(TT,FF)=>x|y)":thm Wehavefinallymanagedtosimplifycondfst,butwhathappenedwithabs1?Clearlyits resultcanbesimplifiedfurther.Weneedamoresophisticatedconversion,whichresimplifiesthe resultofeverysuccessfulconversion. letrecREDEPTHCONVconvt= (SUBCONV(REDEPTHCONVconv)THENC ((convTHENC(REDEPTHCONVconv))ORELSECALLCONV)) t;; HereweseethatREDEPTHCONVcansimplifyabs1completely. #letRDCONV=REDEPTHCONVMANYCONV;; RDCONV=-:conv #RDCONVabs1;; "|-(\fun.(fun(TT,FF)=>x|y))FST==x":thm DEPTHCONVandREDEPTHCONVrewritesubtermsbeforerewritingthetop-level term.YoumaypreferTOPDEPTHCONV,whichtriestorewritethetermbeforeitssubterms. Thiscanbequicker,convertingFST(x,y)toxwithoutwastingtimeony.Itcanalsobeslower, converting(\x.Fxx)tto(Ftt)andthenconvertingttwice.

19 letrecTOPDEPTHCONVconvt= (REPEATCconvTHENC (SUBCONV(TOPDEPTHCONVconv))THENC ((convTHENC(TOPDEPTHCONVconv))ORELSECALLCONV)) t;; 6.Interlude Thoughwehavepassedovernumerousprogramsandexamples,weareonlyhalf-way throughCambridgeLCF’simplementationofrewriting.Letuspauseandreflectonwhatwehave seensofar. Inonesense,thereisnothingremarkableaboutanyoftheprogramsabove.Pattern matchingandrewritinghavebeenaroundfordecades.TheoldsimplifierinEdinburghLCF [$gordon79]isaspowerfulasTOPDEPTHCONV,andotherimplementationsofrewritingare considerablymoreelaborate[$kuechlin82]. Myapproachdiffersinitsmodularprogrammingstyle,whichprovidesbothflexibilityand readability.Theconversionsandtheiroperatorsformalanguageforexpressingrewriting strategies.Forinstance, REPEATC(BETACONVTHENCBETACONV) evidentlyperformsanevennumberofbeta-conversions.Conversionsweredevelopedinorderto escapetherigidityofthetheoldLCFsimplifier;nowseveralLCFusersareusingconversionsto suittheirparticularneeds. Eachdepthconversionexpressesanabstractstrategyforthetraversalofterms,independent fromtheconversiontobeappliedateachsubterm.ThecodeforTOPDEPTHCONVisa paraphraseofitseffect."Repeatedlyapplytheconversionconvtothetermtaslongaspossible; thenconvertrecursivelythesubterms;iftheresultcanstillbeconverted,thenconvertrecursively again." Conversionsmaybeamenabletoalgebraicreasoning,sincetheyobeycertainidentity, associative,anddistributivelaws.Considertheequations 0+a=a+0=a (a+b)+c=a+(b+c) a+b=b+a a+a=a 1.a=a.1=a (a.b).c=a.(b.c) 0.a=a.0=0 a.(b+c)=a.b+b.c (b+c).a=b.a+c.a 20 Researchers[$lehmann77]havebeguntostudymathematicalstructuressuchassemirings andregularalgebras,whichsatisfyvarioussubsetsoftheseequations.PuttingORELSEC, THENC,NOCONV,ALLCONVfor+,.,0,1,itappearsthatconversionssatisfymostofthem. Themainexceptionisa+b=b+a;theoperatorORELSECisnotsymmetric,butalwaystriesits leftoperandfirst.Also,theseconddistributivelawfails.Theforgoingalsoappliestotactics. Mostoftheresearchonsemiringsconcernspath-findingingraphs.Onecanimagineagraph wherethenodesaretermsandthearcsareconversions.Whetherornotthishasanypractical application,itisimportantthatconversionscanbeunderstoodthroughmathematicaltheories thathaveariseninunrelatedbranchesofcomputerscience. Backus’sTuringAwardlecture[$backus78]hasattractedsomuchattentionthatmany peoplenowequatefunctionalprogrammingwithhisFPsystems.Indeed,conversionsexemplify "changeableparts","combiningforms",and"algebraofprograms",whichBackusclaimsas advantagesofhistechnique.However,FPsystemsallowonlyfirst-orderprogramming.FPdoes notregardfunctionsasdataobjects;forinstance,youcannotbuildalistoffunctions. Conversions,andmanyotherpartsofLCF,relyheavilyonhigher-orderfunctions.FPprovides onlyafixedsetoffunctionals("combiningforms");aprogrammercannotintroducenewonessuch asTOPDEPTHCONV.FPdoesnotallowthetrappingoffailures,whichLCFrequiresfor combiningtacticsandconversions.ItisvitaltorecognizethattheFPstyleofprogramming differsfundamentallyfromtheMLstyle. 7.Formulaconversions NowweresumetheexaminationofLCF’srewritingtools.Theideasbehindterm conversionsapplyequallywelltotherewritingofformulas.Letaformulaconversionbeany functionthatmapsaformulaAtoatheorem|-A<=>B.ThisconvertsAtoBandprovesthe twoequivalent.LCFprovidesafamilyofformulaconversions,andoperatorstocombinethem,as fortermconversions. 7.1.Analogsoftermconversions Wecanrewriteaformulawithatheoremthatstatesalogicalequivalence,byinvokingthe formulaconversion REWRITEFCONV"|-!x1...xn.A<=>B" Suchtheoremsarecalledformularewrites.Theconversionisimplementedlike REWRITECONV,usingtheinstantiationfunctionPARTFMATCH: letREWRITEFCONV=PARTFMATCH(fstodestiff);; Thisisusefulforexpandingoutthedefinitionofapredicate,suchas 21 |-!rel.TRANSITIVErel<=> !xyz.relxy==TT/\relyz==TT==>relxz==TT LCFprovidestheidentityconversionsNOFCONV,whichalwaysfails,andALLFCONV, whichmapsanyformulaAto|-A<=>A.Forsequencing,theconversion(fconv1THENFC fconv2)isdefinedintermsofModusPonens.TheoperatorsORELSEFC,REPEATFC,and FIRSTFCONVareimplementedliketheirtermcounterparts. Wecanalsoconvertsubtermsandsubformulas.IfPisapredicate,then PREDFCONVconv"P(t)" isaformulaconversionthatconvertstheargumentt,deriving "|-t==u"(byconv) "|-P(t)==>P(u)"(bysubstitution) "|-P(u)==>P(t)"(bysymmetryandsubstitution) andreturns "|-P(t)<=>P(u)"(bydefinitionof<=>) TotestPREDFCONV,weapplyittothedepthconversionRDCONV,fromaprevious session.TheconvertedformulaconsistsofthepredicatePappliedtothetermsabs2andcondfst. #PREDFCONVRDCONV"P(ˆ abs2,ˆ condfst)";; "|-P((\t.(\u.t,u)FF)TT,(FST(TT,FF)=>x|y))<=>P((TT,FF),x)":thm PPLAMBDA’sinferencerulesallowustoimplementconversionoperatorsforthequantifiers andlogicalconnectives.TheconversionSUBFCONVappliesaconversiontoalltop-levelterms andformulasofaformula: letSUBFCONVconvfconv= FIRSTFCONV[ CONJFCONVfconv; DISJFCONVfconv; IMPFCONVfconv; IFFFCONVfconv; FORALLFCONVfconv; EXISTSFCONVfconv; PREDFCONVconv];; Formappingaconversionoverallsubformulasofaformula,theconversions DEPTHFCONV,REDEPTHFCONV,andTOPDEPTHFCONVaredefinedliketheirterm analogs.Forexample:

22 letrecDEPTHFCONVconvfconvfm= (SUBFCONVconv(DEPTHFCONVconvfconv)THENFC (REPEATFCfconv)) fm;; Letusbindsomeformularewritesandtestformulasforlatersessions. #let[PQ;LESSUU]=examplefrewrites;; PQ="|-!x.P(x,x)<=>Qx":thm LESSUU="|-!x.x<<UU<=>x==UU":thm #let[imp1;conj1;equiv1]=exampleforms;; imp1= "!xy.P((TT=>y|z),SND(y,y))==>Q((\p.(p=>v|y))FF)":form conj1="?x.x<<UUTT\/SND(x,TT)==(UU=>TT|FF)":form equiv1= "!x.?p.(FST(p,p)=>x|UU)==(p=>(\z.SND(x,z))x|(\r.r)UU)" :form Wemakeaconversiontouseourformularewrites,makeadepthconversionfromthisand thetermconversionRDCONV,andtryitonourtestdata. #letMANYFCONV= FIRSTFCONV(mapREWRITEFCONV[PQ;LESSUU]);; MANYFCONV=-:fconv #letDFCONV=DEPTHFCONVRDCONVMANYFCONV;; DFCONV=-:fconv #DFCONVimp1;; "|-(!xy.P((TT=>y|z),SND(y,y))==>Q(\p.(p=>v|y))FF)<=> (!xy.Qy==>Qy)" :thm #DFCONVconj1;; "|-(?x.x<<UUTT\/SND(x,TT)==(UU=>TT|FF))<=> (?x.x==UU\/TT==UU)" :thm #DFCONVequiv1;; "|-(!x.?p.(FST(p,p)=>x|UU)==(p=>(\z.SND(x,z))x|(\r.r)UU))<=> (!x.?p.(p=>x|UU)==(p=>x|UU))" :thm Theseformulasarenotfullysimplified.Thenextsectionshowshowtoeliminate subformulas,suchasTT==UU,thatareobviouslytrueorfalse.

23 7.2.Eliminatingpropositionaltautologies LCFincludesconversionsthatrecognizepropositionaltautologies.Forinstance, TAUTCONJFCONVcanderive TRUTH()/\A<=>A A/\TRUTH()<=>A FALSITY()/\A<=>FALSITY() A/\FALSITY()<=>FALSITY() Mostofthetautologyconversionfunctionsarehand-codedtotreataparticularclassof formulas.Butonesforquantifiersareimplementedintermsofformulaconversions.LCFhas storedthetheorems FORALLTRUTH|-(!x.TRUTH())<=>TRUTH() FORALLFALSITY|-(!x.FALSITY())<=>FALSITY() Usingthese,the"forall"tautologyconversioncansimplify!x.TRUTH()and!x.FALSITY(). ItsMLdefinitionis letTAUTFORALLFCONV= (REWRITEFCONVFORALLTRUTH) ORELSEFC (REWRITEFCONVFORALLFALSITY);; Thefamilyofconversionsismodular.Toimprovethetautologytest,writeabetterversion ofTAUTFORALLFCONV.Perhapsitshouldsimplify!x.AtoAforanyformulaAthatdoes notcontainx. LCFprovidestheconversionBASICTAUTFCONV,whichtriesallthetautologytestsin turn,failingifnoneapply. letBASICTAUTFCONV= FIRSTFCONV[ TAUTCONJFCONV; TAUTDISJFCONV; TAUTIMPFCONV; TAUTIFFFCONV; TAUTFORALLFCONV; TAUTEXISTSFCONV; TAUTPREDFCONV];; Therearemanywaysofbuildingsimplifiersfromtheseconversions.Thestandardone, BASICFCONV,usesTOPDEPTHCONVtosimplifyterms,TOPDEPTHFCONVto simplifyformulas,andBASICTAUTFCONVtofindtautologiesintheresultingformulas. Manyfactorsplayaroleintailoringasimplifiertoaspecificproblem.Forinstance,the 24 REDEPTHconversionsareslowerbutmorethoroughthantheDEPTHones.ForcurrentLCF applications,theTOPDEPTHconversionsseemtoofferthebestcompromiseofspeedand generality. letBASICFCONVconvfconv= TOPDEPTHFCONV(TOPDEPTHCONVconv)(fconvORELSEFCBASICTAUTFCONV);; ThefollowingsessionshowshowBASICFCONVcombinesourtop-levelconversions, MANYCONVandMANYFCONV.Theresultingformulaconversionsolvesthetautologiesthat weremissedbefore. #letBFCONV=BASICFCONVMANYCONVMANYFCONV;; BFCONV=-:fconv #BFCONVimp1;; "|-(!xy.P((TT=>y|z),SND(y,y))==>Q(\p.(p=>v|y))FF)<=> TRUTH()" :thm #BFCONVconj1;; "|-(?x.x<<UUTT\/SND(x,TT)==(UU=>TT|FF))<=> (?x.x==UU)" :thm #BFCONVequiv1;; "|-(!x.?p.(FST(p,p)=>x|UU)==(p=>(\z.SND(x,z))x|(\r.r)UU))<=> TRUTH()" :thm 8.Anatomyofarewritingtactic Instudyingtheserewritingfunctions,letusremainawareoftheiroriginalpurpose:toprove theorems.NowwewillstudytheLCFtacticREWRITETAC,whichsimplifiesagoalby rewritingitandremovingtautologies.Thistacticisevolvingovertime.Thoughtheversion describedhereisnotthelatest,itsstructureillustratesthepracticaluseofconversionsand higher-orderfunctions. 8.1.Implicativerewrites ThefunctionsREWRITECONVandREWRITEFCONVacceptrewritingtheoremsofthe form|-t==uor|-A<=>B.However,therearemanyequivalencesthatonlyholdundercertain conditions.ConsideratheoryoflistswithstrictCONSandMAPfunctions.Thefollowing theoremholdsonlybyvirtueoftheantecedentforcingxtobedefinedintheequivalence: ˜ x==UU==>MAPf(CONSxl)==CONS(fx)(MAPfl) IfxisUU,lisNIL,andfistheconstantfunction\y.TT,thentheequivalencedoesnothold:

25 MAP(\y.TT)(CONSUUNIL)==CONS((\y.TT)UU)(MAP(\y.TT)NIL) <=> (bystrictnessofCONS,definitionofMAP) MAP(\y.TT)UU==CONS((\y.TT)UU)NIL <=> (bybeta-conversion,strictnessofMAP) UU==CONSTTNIL <=> (bytotalityofCONS) FALSITY() Ingeneral,theseimplicativerewritesmaydependonmorethanoneantecedent.LCF presumesthemtohavetheform,fornon-negativen, A1==>(...(An==>t==u)...) A1==>(...(An==>(B<=>C))...) Howcanaconversionusesuchatheorem,givenaninstancet’ofthelefthandtermt?Ifit canprovetheinstancesoftheantecedents,A’1,...,A’n,then,byModusPonens,itcanreturnthe theorem|-t’==u’.Howshouldittrytoprovetheantecedents?ThesimplifiersinbothEdinburgh LCFandtheBoyer/MooreTheoremProver[$boyer79]solveantecedentsbyrecursivelyinvoking thesimplifier.However,thereisnoneedtocommitourselves;wecanpassanyprooftacticasan argument.Conversionsthatattempttoproveinstancesoftheantecedentsusingatactictacare IMPREWCONVtac"|-A1==>(...(An==>t==u)...)" IMPREWFCONVtac"|-A1==>(...(An==>(B<=>C))...)" 8.2.Backwardschaining AlthoughthelatestversionofREWRITETACinvokesitselftoprovetheantecedentsof implicativerewrites,wewillexamineanearlier,simplerversion.Itusesbackwardschaining--a proofsearchthatresemblestheexecutionofPPLAMBDAimplicationsasaPROLOGprogram [$clocksin81].ItisimplementedusingPARTFMATCHtomatchtheconsequentofan implication. Letusseehowbackwardschainingcansolveantecedentsofimplicativerewrites.Typically, anantecedentwillrequirethatalistlbedefined:˜ l==UU.Considerafirst-ordertheoryoflists, withNIL,astrictCONS,andaninfixoperatorAPPtoappendlists.Thetheoryincludes theoremsassertingthattheseconstantscreatedefinedlists: NILDEFINED|-˜ NIL==UU CONSDEFINED|-˜ a==UU==>(˜ l==UU==>˜ CONSal==UU) APPDEFINED|-˜ l1==UU==>(˜ l2==UU==>˜ l1APPl2==UU)

26 ThetacticIMPSEARCHTACperformsadepth-firstsearchusingalistofsuchtheorems. Itsearchesthelistforatheoremwhoseconsequentmatchesthegoal,failingifthereisnone. Supposethereisatheorem |-A1==>...==>An==>B, andthatthegoalisaninstanceB’ofB.Thetacticcallsitselfrecursivelytoprovetheinstances oftheantecedents,A’1...A’n,andprovesthegoalB’byModusPonens.Forthesearchto terminatesuccessfully,theremustbetheoremswithnoantecedents(n=0).Atheoremsuchas |-A==>Awillcauseinfiniteregress. Inthisexample,itestablishesthatacomplexlistisdefined,becauseitisconstructedfrom theconstantsNIL,CONS,APP.Thevariablest,u,andlareallassumedtobedefined.The goaltreeshowshowtheinitialgoalisreducedtosimplersubgoals,untiltheleavesarealltrue: ˜ (CONStl)APP(CONSt(CONSuNIL)))==UU ˜ CONStl==UU˜ CONSt(CONSuNIL)==UU ˜ t==UU˜ l==UU˜ t==UU˜ CONSuNIL==UU ˜ u==UU˜ NIL==UU 8.3.Canonicalforms ApredicatelogicsuchasPPLAMBDAallowsmanydifferentwaysofsayingthesamething. Forinstance,(A/\B)==>CislogicallyequivalenttoA==>(B==>C),though IMPREWCONVandIMPSEARCHTACexpectthelatter.EdinburghLCFaddressesthis problembyforcingeveryformulaintoastandardcanonicalform.CambridgeLCF,described here,takesamoreflexibleapproach.Itprovidesfunctionsforputtingtheoremsintocanonical form;theusermayinvoketheseorimplementdifferentonesinML.Thesefunctionsareinference rules.Theydonotsimplymanipulatedatastructures,butprovetheiroutputtheoremsfrom theirinputtheorems. ThefunctionIMPCANONconvertsatheoremintoalistofimplications.Thisformis usefulinmanyLCFsituations.(Note:boundvariablesmayberenamed;assumptionsoftheinput theoremarepassedtotheoutput.) IMPCANON"|-A/\B"--->(IMPCANON"|-A")@(IMPCANON"|-B") IMPCANON"|-(?x.A)==>B"--->IMPCANON"|-A[y/x]==>B" IMPCANON"|-!x.A"--->IMPCANON"|-A[y/x]" IMPCANON"|-(A/\B)==>C"--->IMPCANON"|-A==>(B==>C)" IMPCANON"|-(A\/B)==>C"--->(IMPCANON"|-A==>C")@(IMPCANON"|-B==>C")

27 Ifthecasesabovedonotapply,andtheargumentisanimplication|-A==>B,then IMPCANONcallsitselfontheequivalenttheorem,A|-B.ThisbreaksBintoalist [A|-B1;...;A|-Bn]oftheoremsthatassumeA.ItdischargesAfromeachofthese,toreturn [A==>B1;...;A==>Bn].Atheoremthatsatisfiesnocases,suchas|-A\/B,passesthrough unchanged. Inthissession,weseeIMPCANONconvertingseveralslightlydifferenttheoremsintothe sameone. #IMPCANON(ASSUME"!x.˜ x==UU==>!y.˜ y==UU==>˜ fxy==UU");; [.|-"˜ x==UU==>˜ y==UU==>˜ fxy==UU"]:thmlist #IMPCANON(ASSUME"!xy.˜ x==UU==>˜ y==UU==>˜ fxy==UU");; [.|-"˜ x==UU==>˜ y==UU==>˜ fxy==UU"]:thmlist #IMPCANON(ASSUME"(˜ x==UU/\˜ y==UU)==>˜ fxy==UU");; [.|-"˜ x==UU==>˜ y==UU==>˜ fxy==UU"]:thmlist #IMPCANON(ASSUME"(˜ x==UU/\˜ y==UU)==> #!fg.˜ fxy==UU/\˜ gxy==UU");; [.|-"˜ x==UU==>˜ y==UU==>˜ fxy==UU"; .|-"˜ x==UU==>˜ y==UU==>˜ gxy==UU"] :thmlist SuchimplicationsarefineforIMPREWCONVandIMPSEARCHTAC,but IMPREWFCONVexpectstheoremsoftheuncommonformC<=>D.Theinferencerule FCONVCANONalterstheconsequentofcertainimplicationsintologicalequivalences: P(x)--->P(x)<=>TRUTH()(Papredicatesymbol) ˜ P(x)--->P(x)<=>FALSITY() C<=>D--->unchanged elsefail ThusFCONVCANONproveslogicalequivalencesthatrewritepredicatestoTRUTH()and negatedpredicatestoFALSITY().Itpassesonanyformularewritesitencounters.Forinstance, thetheoremsNILDEFINED,CONSDEFINED,andAPPDEFINEDbecomeimplicative formularewrites.(Recallthattheformulat==uisshorthandforthepredicateequiv(t,u).) |-NIL==UU<=>FALSITY |-˜ a==UU==>(˜ l==UU==>(CONSal==UU<=>FALSITY())) |-˜ l1==UU==>(˜ l2==UU==>(l1APPl2==UU<=>FALSITY())) Thesetheoremscansolvetheantecedentsofimplicativerewritesusingrewritinginsteadof backwardschaining.Theeffectissimilartothederivationtreeshownattheendoftheprevious section.TOPDEPTHFCONVtriestheseformularewritesbeforedescendingintotheantecedent toapplytermrewrites. Thus,iftheantecedentcanbesolvedbybackwardschaining,itcanalsobesolvedby rewriting,withcomparableefficiency.Rewritingcansolvemanymoreantecedentsthan 28 backwardschainingcan.Itsmaindrawbackisagreaterdangerofinfiniteregress,tryingto rewritetheantecedentoftheantecedentofthe....Anyimplicativerewrite|-A(t)==>t==u cancausesuchregress,invokingitselfintheattempttoproveitsownantecedent.Againwesee thatmanyconsiderationsguidetheselectionofcomponentswhenbuildingasimplifier. 8.4.Theprimitiveconversiontactic Thoughtherearemanywaystobuildaconversion,thereisonlyoneobviouswaytoreduce agoalusingaconversion.Thetactic(FCONVTACfconv)usesfconvtoconvertagoalAtoa subgoalB,leavingitsassumptionsunchanged.IfBisjustTRUTH(),thenFCONVTAChas achievedthegoalA,andreturnsanemptysubgoallist. 8.5.Therewritingtactic ThetacticREWRITETACrequiresalltheabovepieces.Itacceptsalistoftheorems,and putsthemintocanonicalformusingIMPCANONandFCONVCANON.Ithandlesimplicative rewritesusingIMPREWCONVandIMPREWFCONV,whichfailonunacceptabletheorems. Thefunctionmapfiltergathersthesuccessfulconversions;these,alongwithBETACONV,are combinedusingFIRSTCONV,FIRSTFCONV,andBASICFCONV.REWRITETACsolves antecedentsofimplicativerewritesbybackwardschaining,usingthetacticIMPSEARCHTAC. Tosolvetrivialsubgoalsinchaining,itaugmentsthelistoftheoremswithLCF’sreflexivity axiom: EQREFL|-!x.x==x ThetacticASMREWRITETACcallsREWRITETAC,usingthetacticalASSUMLIST toappendthegoal’sassumptionstotheinputlistoftheorems.Mostproofsrelyon ASMREWRITETACforrewriting,inordertotakeadvantageoftheassumptions.

29 letREWRITETACthl= letthms=flat(mapIMPCANONthl)in letchaintac=IMPSEARCHTAC(EQREFL.thms)in letconv= FIRSTCONV(mapfilter(IMPREWCONVchaintac)thms) ORELSECBETACONV in letfconv= FIRSTFCONV (mapfilter((IMPREWFCONVchaintac)oFCONVCANON)thms) in FCONVTAC(BASICFCONVconvfconv);; letASMREWRITETACthl= ASSUMLIST(\asl.REWRITETAC(asl@thl));; 9.Examplesofsolvinggoalsbyrewriting ToseeASMREWRITETACinuse,considerarecentproofofmine[$paulson83a].Ituses adatastructureforexpressionscomposedofconstants,variables,andcombinationsofother expressions.ItconcernsinfixfunctionsOCCSandOCCSEQ;thesearerelationsbecausethey returnatruth-valuedresult.Therelation"tOCCSu"searchesuforanoccurrenceoft, returningTTifitfindsone.TherelationOCCSEQisthereflexiveclosureofOCCS.Theyare definedintermsofabooleanoperatorOR,andacomputableequalityrelation=. letOCCSEQ= newaxiom(‘OCCSEQ‘, "!tu.tOCCSEQu==(t=u)OR(tOCCSu)");; letOCCSCLAUSES= newaxiom(‘OCCSCLAUSES‘, "!t.tOCCSUU==UU /\ (!c.˜ c==UU==> tOCCS(CONSTc)==FF) /\ (!v.˜ v==UU==> tOCCS(VARv)==FF) /\ (!t1t2.˜ t1==UU==>˜ t2==UU==> tOCCS(COMBt1t2)==(tOCCSEQt1)OR(tOCCSEQt2))");; WewillseehowASMREWRITETAChelpstoprovethattherelationOCCSistransitive:

30 !t.˜ t==UU==> !u.tOCCSu==TT==> !u’.uOCCSu’==TT==>tOCCSu’==TT Inductingonthevariableu’yieldsfoursubgoals. #expand(TERMTAC"u’");; OK.. 4subgoals "uOCCS(COMBt1t2)==TT==>tOCCS(COMBt1t2)==TT" ["˜ t==UU"] ["tOCCSu==TT"] ["uOCCSt1==TT==>tOCCSt1==TT"] ["uOCCSt2==TT==>tOCCSt2==TT"] ["˜ t1==UU"] ["˜ t2==UU"] "uOCCS(VARv)==TT==>tOCCS(VARv)==TT" ["˜ t==UU"] ["tOCCSu==TT"] ["˜ v==UU"] "uOCCS(CONSTc)==TT==>tOCCS(CONSTc)==TT" ["˜ t==UU"] ["tOCCSu==TT"] ["˜ c==UU"] "uOCCSUU==TT==>tOCCSUU==TT" ["˜ t==UU"] ["tOCCSu==TT"] ComparethesewiththeaxiomOCCSCLAUSES;threeofthemcontradicttheantecedent, uOCCSu’==TT.UsingtheaxiomsOCCSCLAUSESandOCCSEQ,thetactic ASMREWRITETACsolvesthethreeeasygoals.Duringinitialization,itsplits OCCSCLAUSESintoUU,CONST,VAR,andCOMBclauses,eachanimplicativerewrite. WhilerewritingthegoalinvolvingCONST,itnoticestheassumption˜ c==UU,andrewrites uOCCS(CONSTc)toFF.ThenitrewritestheantecedentFF==TTtoFALSITY().Similarly, itrewritestheconsequenttoFALSITY(),yieldingthetrivialgoalFALSITY()==>FALSITY(). ASMREWRITETACsolvesthegoalsinvolvingUUandVARinthesameway.Thefourthgoal isdifficult,butthetacticadvancesitconsiderably:

31 "((u=t1)OR(uOCCSt1))OR ((u=t2)OR(uOCCSt2))==TT ==> ((t=t1)OR(tOCCSt1))OR ((t=t2)OR(tOCCSt2))==TT" ["˜ t==UU"] ["tOCCSu==TT"] ["uOCCSt1==TT==>tOCCSt1==TT"] ["uOCCSt2==TT==>tOCCSt2==TT"] ["˜ t1==UU"] ["˜ t2==UU"] Mypaper[$paulson83a]describestherestoftheproof,involvingacasesplitfollowedbya furthercalltoASMREWRITETAC. 9.1.RecentimprovementstoREWRITETAC REWRITETAChasevolvedsincethispaperwasfirstwritten.Theversionpresented aboveissimplerthanthelatestone.Nowweexamine,inlessdetail,therecentimprovements. Thefirstimplementationcontainedlotsofmessycode;Ilaterrealizedhowtoexpressthisina modularstyle,usingconversions. Themaininnovationistouselocalassumptionsduringrewriting.IntheformulasA/\Band A==>B,itislegitimatetoassumeAwhenrewritingB.Informally,thetruthvalueofBis irrelevantunlessAholds.Amoreconvincingjustificationisthefollowingderivedinferencerule, implementedinMLusingtheprimitiverules: A<=>A2 [A;A2]B<=>B2 ------------------------------------ (A/\B)<=>(A2/\B2) (A==>B)<=>(A2==>B2) ThisruleallowsustoconverttheformulaAtoA2,thenassumethesewhileconvertingBtoB2, withouttheseassumptionsappearingintheresultingtheorems. Localassumptionsfacilitatemanyproofs.Theolderrewritingtacticcouldreturnagoal containingtheformula p==TT==>p=>x|y==x Rewritingtheconditionalwiththelocalassumptionp==TTsimplifiestheformulatoTRUTH(). Iftherewritingtacticcannotmakelocalassumptions,thentheusermustmanipulatethe antecedentp==TTintoaglobalposition.Thesemanipulationsobscuretheproof.Theyreflect thecontextoftheformula,yettheformulaistrueinanycontext.

32 Itisnotobvioushowtheconversion(IMPFCONVfconv)canmakelocalassumptions. Somehowtheassumptionp==TTmustbeincorporatedintofconv,itselfbuiltfromother operators.Mysolutionistosupplyanadditionalargument,fconvfun,whichmapsaformulato aconversion.ThelocalversionofIMPFCONVis LOCALIMPFCONVfconvfconvfun WhenconvertinganimplicationA==>B,itusesfconvtoconvertAtoA2,appliesfconvfunto A2toproduceanewconversion,andconvertsBusingthat.Likewisethereisa LOCALCONJFCONV.Combiningtheseconversionswiththosefortheotherconnectivesyields aLOCALSUBFCONV,aLOCALTOPDEPTHFCONV,andaLOCALBASICFCONV. Theselocalconversionsresembletheirpredecessors,buttaketheadditionalargumentfconvfun. ThenewREWRITETACisimplementedintermsofahighlyrecursiveformulaconversion. Forsolvingimplicativerewrites,thisconversionusesacalltoitselfratherthan IMPSEARCHTAC.Itpassesanotherrecursivecallasthefconvfunargumentof LOCALSUBFCONV.Forfastpatternmatching,itstoresrewritesindiscriminationnets [$charniak80]insteadoflists. Aseparateimprovementistoexpandoutdisjunctionsduringrewriting,causingautomatic casesplits.TheconversionEXPANDDISJFCONVderives (A\/B)==>C<=>(A==>C)/\(B==>C) (A\/B)/\C<=>(A/\C)\/(B/\C) C/\(A\/B)<=>(C/\A)\/(C/\B) Thisisappliedatthesamepointasthetautologyconversions.Existentialquantifiersare similarlyexpanded.ExpansionofdisjunctionsisespeciallyeffectivewhenAandB,aslocal assumptions,helptorewriteC. 10.Conclusions Youmaybethinking,"Conversionsseeminteresting,butmustbehopelesslyinefficient." ConversionsareheavilyusedinCambridgeLCF,wheretheyareefficientenoughtoprovedifficult theorems.RuntimerangesfromtensecondstoseveralminutesonaVAX750computer. ItishardtoimprovetheefficiencyintheLCFframework.Anysimplifiermustproducea theoremtojustifyitsresult.Itmustcoexistwithothertheorem-provingtools,andwithML. Thisprecludessomeoptimizations,suchasreducingthenumberofsubstitutionsbymaintaininga globalenvironmentofvariablebindings[$boyer79].ThecurrentMLcompilergeneratespoor code,thoughefficientimplementationsarebeingdeveloped[$cardelli83]. ConversionfunctionshavemanyadvantagesoverEdinburghLCF’ssimplifier,alargeand inscrutableMLprogram.TheoperatorsPARTFMATCH,REWRITECONV, TAUTCONJCONV,IMPCANON,etc.,carryoutsmall,well-definedtasks.Theyhavesimple specificationsandimplementations.Togethertheyexpresstherewritingtactic,REWRITETAC, 33 inonlyadozenlines. REWRITETACperformsthevastmajorityofinferencesinLCFproofs.Itslimitations andabilitiesareeasytograsp,thankstoitsmodularstructure.Thishelpstheusertoplan interactivesessions,andtoreadtacticalproofslikeasummaryofthehundredsofformal inferences. Conversionsillustratethepowerofhigher-orderfunctions.BecauseMLtreatsfunctionsas first-classdata,wecanimplementrewritingtoolsasfunctionsandwriteoperatorstocombine them.Prooftacticsarefunctionstoo;theconversionIMPREWCONVgeneratesandproves subgoalsusingatacticpassedtoitasanargument.TheinstantiationfunctionPARTTMATCH acceptsafunctionargumentthattellsitwhatpartofatheoremtomatch.Thisprogramming stylediffersgreatlyfromthestylethatBackus[$backus78]recommends,whereonlyfirst-order functionsareallowed. LCFisusednotonlyforperformingparticularproofs,butalsoforresearchintoproof techniques.TheprogramminglanguageMLprovidestheflexibilityneededforthisresearch.The discoveryoftheoperatorsTHEN,ORELSE,andREPEAT,forcombiningtactics,wasa breakthroughinthedevelopmentofEdinburghLCF.Soitisexcitingtofindsimilaroperatorsfor combiningconversions,especiallysincetacticsandconversionshavelittleelseincommon.This callsforaninquiryintootherinstancesofthisprogrammingstyle. Acknowlegements.IwouldliketothankJ.Fairbairn,M.Gordon,D.Matthews,andthereferees fortheirdetailedcommentsonthepaper.D.Bensonintroducedmetosemirings.Thisresearch issupportedbytheScienceResearchCouncilofGreatBritain.

34 References [$backus78] J.Backus,CanprogrammingbeliberatedfromthevonNeumannstyle?Afunctionalstyle anditsalgebraofprograms,CommunicationsoftheACM21(August1978)pages613-641. [$boyer79] R.BoyerandJ.Moore,AComputationalLogic(AcademicPress,1979). [$cardelli83] L.Cardelli,Thefunctionalabstractmachine,Polymorphism:theML/LCF/HOPE Newsletter(BellLaboratories,MurrayHill,NewJersey,January1983). [$charniak80] E.Charniak,C.Riesbeck,andD.McDermott,ArtificialIntelligenceProgramming (LawrenceErlbaumAssociates,1980). [$clocksin81] W.ClocksinandC.Mellish,ProgramminginProlog(Springer-Verlag,1981). [$cohn83] A.Cohn,Theequivalenceoftwosemanticdefinitions:acasestudyinLCF,SIAMJournal ofComputing12(May1983)pages267-285. [$gordon79] M.Gordon,R.Milner,andC.Wadsworth,EdinburghLCF(Springer-Verlag,1979). [$gordon82] M.Gordon,RepresentingalogicintheLCFmetalanguage,in:D.Neel,editor,Toolsand NotionsforProgramConstruction(CambridgeUniversityPress,1982)pages163-185. [$huet80] G.HuetandD.Oppen,Equationsandrewriterules:asurvey,in:R.Book,Editor,Formal LanguageTheory:PerspectivesandOpenProblems(AcademicPress,1980)pages349-406. [$kuechlin82] W.Kuechlin,AnimplementationandinvestigationoftheKnuth-Bendixcompletion procedure,ReportNo.17/82,InstitutfuerInformatikI,UniversityofKarlsruhe(1982). [$lehmann77] D.J.Lehmann,Algebraicstructuresfortransitiveclosure,TheoreticalComputerScience4 (1977)pages59-76. [$manna74] Z.Manna,MathematicalTheoryofComputation(McGraw-Hill,1974).

35 [$paulson83a] L.Paulson,RecentdevelopmentsinLCF:examplesofstructuralinduction,ReportNo.34, ComputerLaboratory,UniversityofCambridge(1983). [$paulson83c] L.Paulson,TherevisedlogicPPLAMBDA:areferencemanual,ReportNo.36,Computer Laboratory,UniversityofCambridge(1983).