Static termination analysis for prolog using term rewriting and SAT solving [Elektronische Ressource] / vorgelegt von Jan Peter Schneider-Kamp. [Hrsg.: Fachgruppe Informatik, RWTH Aachen University]

Description

AachenDepartment of Computer ScienceTechnical ReportStatic Termination Analysis for Prologusing Term Rewriting and SAT SolvingPeter Schneider-KampISSN 0935{3232 Aachener Informatik Berichte AIB-2008-17RWTH Aachen Department of Computer Science December 2008The publications of the Department of Computer Science of RWTH Aachen (AachenUniversity of Technology) are in general accessible through the World Wide Web.http://aib.informatik.rwth-aachen.de/Static Termination Analysis for Prologusing Term Rewriting and SAT SolvingVon der Fakult at fur Mathematik, Informatik undNaturwissenschaften der RWTH Aachen University zurErlangung des akademischen Grades eines Doktors derNaturwissenschaften genehmigte Dissertationvorgelegt vonDiplom-InformatikerJan Peter Schneider-KampausGeldernBerichter: Prof. Dr. Jurgen GieslProf. Michael CodishTag der mundlic hen Prufung: 8. Dezember 2008Diese Dissertation ist auf den Internetseiten der Hochschulbibliothek online verfugbar.Jan Peter Schneider-KampLehr- und Forschungsgebiet Informatik [e-mail] Informatik Bericht AIB-2008-17Herausgeber: Fachgruppe InformatikRWTH Aachen UniversityAhornstr. 5552074 AachenGERMANYISSN 0935-3232AbstractThe most fundamental decision problem in computer science is the halting problem, i.e.,given a description of a program and an input, decide whether the program terminatesafter nitely many steps or runs forever on that input.

Sujets

• Informatik

Informations

• Publié par: rheinisch-westfalischen_technischen_hochschule_-rwth-_aachen
• Publié le: 01 janvier 2008
• Nombre de lectures: 30
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

The

publications

University

of

of

the

tDepartmen

)gychnoloeT

are

in

of

general

Computer

accessible

Science

roughth

of

the

WTHR

orldW

aachen.de/http://aib.informatik.rwth-

henAac

Wide

(

achenA

eb.W

usingStaticTTermerminationRewritingAnalandysisSATforSolvingProlog

VonderFakult¨atf¨urMathematik,Informatikund

NaturwissenschaftenderRWTHAachenUniversityzur

ErlangungdesakademischenGradeseinesDoktorsder

DissertationgenehmigtehaftenNaturwissensc

vorgelegtvon

erDiplom-Informatik

hneider-KampSceterPJan

hneider-KampSc

aus

Geldern

Berichter:Prof.Dr.J¨urgenGiesl

haelMicProf.dishCo

Tagderm¨undlichenPr¨ufung:8.Dezember2008

DieseDissertationistaufdenInternetseitenderHochschulbibliothekonlineverf¨ugbar.

hneider-KampSc

eterP

Jan

2

Informatik

bietungsgehorscF

undLehr-

[e-mail]

ISSN

0935-3232

er:Herausgeb

GERMANY

henAac52074

Ahornstr.

55

ikInformat

hgruppacFe

henAacWTHR

yersitUniv

AIB-2008-17

thBeric

Informatik

Aachener

Abstract

Themostfundamentaldecisionproblemincomputerscienceisthehaltingproblem,i.e.,
givenadescriptionofaprogramandaninput,decidewhethertheprogramterminates
afterfinitelymanystepsorrunsforeveronthatinput.WhileTuringshowedthisproblem
tobeundecidableingeneral,developingstaticanalysistechniquesthatcanautomatically
proveterminationformanypairsofprogramsandinputsisofgreatpracticalinterest.
Thisistrueinparticularforlogicprogramming,astheinherentlackofdirectioninthe
computationvirtuallyguaranteesthatanynon-trivialprogramterminatesonlyforcertain
classesofinputs.Thus,terminationoflogicprogramsiswidelystudiedandsignificant
advanceshavebeenmadeduringthelastdecades.Nowadays,therearefully-automated
toolsthattrytoproveterminationofagivenlogicprogramw.r.t.agivenclassofinputs.
Nevertheless,therestillremainmanylogicprogramsthatcannotbehandledbyany
currentterminationtechniqueforlogicprogramsthatisamenabletoautomation.
Anotherareawhereterminationhasbeenstudiedevenmoreintensivelyistermrewrit-
ing.Thisbasiccomputationprincipleunderliestheevaluationmechanismofmanypro-
gramminglanguages.Significantadvancestowardspowerfulautomatabletermination
techniquesduringthelastdecadehaveyieldedaplethoraofpowerfultoolsforproving
.automaticallyterminationInthisthesis,weshowthattechniquesdevelopedforprovingterminationoftermrewrit-
ingcansuccessfullybeadaptedandappliedtoanalyzelogicprograms.Thenewtechniques
developedsignificantlyextendtheapplicabilityandthepowerofautomatedtermination
analysisforlogicprograms.Theworkpresentedhererangesfromadaptingtechniques
toworkdirectlyonlogicprogramstotransformationsfromlogicprogramstoaspecial-
izedversionoftermrewriting.Onthelogicprogrammingsidewealsopresentanew
pre-processingapproachtohandlelogicprogramswithcuts.Onthetermrewritingside
weshowhowtosearchforcertainpopularclassesofwell-foundedordersontermsmore
efficientlybyencodingthesearchintosatisfiabilityproblemsofpropositionallogic.
Thecontributionsdevelopedinthisthesisareimplementedintoolsforautomatedter-
minationanalysis–mostlyinourfullyautomatedterminationproverAProVE.Thesig-
nificanceofourresultsisdemonstratedbythefactthatAProVEhasreachedthehighest
scorebothfortermrewritingandlogicprogrammingattheannualinternationalTermi-
nationCompetitionsinallyearssince2004,wheretheleadingautomatedtoolstryto
analyzeterminationofprogramsfromdifferentareasofcomputerscience.

edgmentslwAckno

FirstandforemostIwouldliketothankJ¨urgenGieslforbeingachallengingandde-
mandingandatthesametimetrustingandsupportivesupervisor,employer,colleague,
andmentor.Hisdoorwasalwaysopen,therewasalwaystimefordiscussion,andhis
optimismalwayskeptmeonthetrack.
IamequallythankfultowardsmycolleagueandfriendRene´Thiemann.Hisintuition
andcraftsmanshipinformalproofsgaverisetocountlessfruitfuldiscussions,somefrus-
trating,mostveryproductive,butallmutuallyrewarding.Itwasmygreatestpleasure
toworkinateamwithhimandJ¨urgen.
ManythanksgotoMikeCodishforagreeingtobethesecondsupervisorofmythesis
andformanyverysatisfyingdiscussions–rangingfromfacetofaceoverabeertolong
Skypesessionswherehemademeawarethatbirdnoiseisactuallynice.Withouthis
initiativeinearly2006,therewouldbenosecondpartofthisthesis.
IamgratefultoAlexanderSerebrenikforintroducingmetotheworldoflogicprogram-
ming.TheideaswescribbledonapapernapkinoutsideaValenciancafe´backin2003
havebeenthestartingpointforafruitfulcooperationthathasinspiredmostofthefirst
thesis.thisofpartMythanksbelongtomyofficemateStephanSwiderskiforexchangingallthoseideas
andprovidingmewithhissometimesunconventionalbutoftenenlighteningperspective,
andtomycolleagueCarstenFuhsforco-developingtheSATframeworkand,givena
sufficientsupplyofcoffee,findingthemostobscureofmistakes.
SpecialthanksgotoThomasStr¨oderforgreatworkonthelogicprogrammingimple-
mentation,andtoCarstenFuhs,CarstenOtto,Rene´Thiemann,StephanSwiderski,and
Erika´Abrah´amforproof-readingpreliminaryversionsofthisthesis.
Sincerethanksgotoallotherco-authorsofjointpapersforfruitfulcooperations,to
alltheothermembersoftheAProVEteamforalltheircontributionsandmanyadark
Guinness,andtothecolleaguesoftheMOVESgroupforaniceatmospherebeforeand
after2pm.Ialsoenjoyedthepresenceofandthecooperationwithourinternational
guestsManhThangNguyen,Ra´ulGuti´errez,andBeatrizAlarc´on.
Lastbutnotleast,IammuchobligedtomyparentsandSilke,whohadtoputupwith
longandirregularworkhours,frequenttravels,andincomprehensibleresearchtopics,yet
stillsupportedmeinsomanyways.

Schneider-KampPeter

Contents

ductionIntro1.

Prelimina2.ries

I.TerminationAnalysisofLogicPrograms

1

7

11

3.TransformationalApproach13
3.1.Preliminaries..................................17
3.2.TransformingLogicProgramsintoTermRewriteSystems..........19
3.3.TerminationofInfinitaryConstructorRewriting...............24
3.4.RefiningtheArgumentFilter.........................31
3.5.FormalComparisonoftheTransformationalApproaches..........53
3.6.ExperimentsandDiscussion..........................57
3.7.Summary....................................62

63roachAppDirect4.4.1.Preliminaries..................................65
4.2.DependencyTripleFramework.........................66
4.3.DependencyTripleProcessors.........................69
4.4.Summary....................................76

5.LogicProgramswithCuts79
5.1.Preliminaries..................................81
5.2.ConcreteDerivations..............................82
5.3.AbstractDerivations..............................86
5.4.TerminationGraph...............................100
5.5.TerminationGraphtoLogicProgram.....................111
5.6.Summary....................................119

II

II.AutomatingSearchbyEncodingtoSAT

Contsten

121

6.RecursivePathOrder123
6.1.Preliminaries..................................125
6.2.EncodingRPOproblems............................128
6.3.ImplementationandExperiments.......................133
6.4.Summary....................................134

135FiltersArgument7.7.1.Preliminaries..................................136
7.2.EncodingRPOwithArgumentFilters....................140
7.3.ArgumentFiltersandUsableRules......................145
7.4.ImplementationandExperiments.......................148
7.5.Summary....................................149

Conclusion8.

Bibliography

Index

151

155

165

ionuctdIntro1.

Themostfundamentaldecisionproblemincomputerscienceisthehaltingproblem,i.e.,
givenaprogramandaninput,decidewhethertheprogramterminatesafterfinitelymany
stepsorwhetheritrunsforeveronthatinput.While[Tur36]showedthisproblemtobe
undecidableingeneral,developingstaticanalysistechniquesthatcanautomaticallyprove
terminationformanypairsofprogramsandinputsisofgreatpracticalinterest.
Provingterminationisessentialforanumberofverificationtechniques.Forexample,
boththeoremproving[BM79]andKnuth-Bendixcompletion[KB70]requirefrequentter-
minationproofsfortheircorrectoperation(see[MV06,WSW06,BKN07]forrecentwork
onapplyingterminationanalysisintheseareas).Inprocessverification,livenessprob-
lemscanoftenbereducedtoterminationproblems[GZ03],andMicrosoftusestermination
analysistostaticallyverifytheirdevicedrivers[CPR05].
Terminationanalysisisofparticularinterestinlogicprogrammingastheinherentlack
ofdirectioninthecomputationvirtuallyguaranteesthatanynon-trivialprogramter-
minatesonlyforcertainclassesofinputs.Thus,terminationoflogicprogramsiswidely
studied(see[DD94]foranoverviewand[BCG+07,CLS05,CLSS06,DS02,LMS03,MR03,
MS07,ND05,ND07,NGSD08,SD05a,Sma04]formorerecentwork)andsignificantad-
vanceshavebeenmadeduringthelastdecades.Nowadays,therearefully-automated
tools[LSS97,MB05,TGC02,SD03a,GST06,ND07,OCM00]thattrytoprovetermina-
tionofagivenlogicprogramw.r.t.agivenclassofinputs.Nevertheless,therestillremain
manynaturallogicprogramsthatcannotbeshownterminatingbyanyofthesetools.
Anotherareawhereterminationhasbeenstudiedevenmoreintensivelyistermrewrit-
ing(seeforexample[Der87,Zan95,AG00,GTSF06,EWZ06]).Thisbasiccomputation
principleunderliestheevaluationmechanismofmanyprogramminglanguagesand,in-
deed,transformationsfromfunctional