Termination Of Narrowing Revisited PDF Free Download

1y ago

26 Views

1 Downloads

6.89 MB

37 Pages

Report/dmca

Download PDF

Transcription

Termination of Narrowing RevisitedMarı́a AlpuenteDepartmento de Sistemas Informáticos y Computación (DSIC)Technical University of Valencia (UPV)Valencia, SpainPisa - October 23th, 2009M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20091 / 34

Our motivation(1991) Ph.D. on Equational Constraint Satisfaction via NarrowingSupervisors: Giorgio Levi and Isidro RamosNarrowingGeneralization of rewriting with unification and logic variablesProblem: Termination of narrowing was an issueNaı̈ve solution: Incremental constraint solving approachM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20092 / 34

Our motivationFor 20 years a recurrent problem in many narrowing nal model of functional–logic languagesEquational unificationAnalysis and certification of security policiesSymbolic reachabilityType-checking of dependently typed languagesCompact approximations of program semanticsAutomated proofs of termination for rewritingModel-checkingNarrowing-driven partial evaluationDeclarative debuggingM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20093 / 34

Our GoalsDespite the great number of narrowing-fueled tools, surprisinglytermination of narrowing has received little attention (less thancompleteness)The main goalsInvestigate the (mostly unexplored) problem of narrowing terminationDevelop a practical tool (previously lacking): an automated narrowingtermination proverM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20094 / 34

DefinitionsRewriting s p,R t s[r σ]p if there is a position p of s a matcher σ s.t. s p lσa rule (l r ) in R Narrowing s;p,R,σ t (s[r ]p )σ if there isM. Alpuente, S. Escobar, J. Iborra (UPV) a nonvariable position p of s a unifier σ s.t. s p σ lσ[σ mgu(s p , l)]a rule (l r ) in RTermination of Narrowing RevisitedPisa - October 23th, 20095 / 34

An example Standard definitionof addition (TRS)R add nadd(0, Y ) Yadd(s(X ), Y ) s(add(X , Y ))With rewriting: add(s(0), 0) R s(add(0, 0)) R s(0)With narrowing: add(s(0), 0) ;R s(add(0, 0)) ;R s(0)butalso: add(Z , Y )s(add(X , Y ))“instantiate”#:tttttttt R“instantiate”ttadd(s(X ), Y ) {{{{{{ R{{s(Y ) (rnf )s(add(0, Y ))with computed answer substitution {Z /s(0)}M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20096 / 34

An example Standard definitionof addition (TRS)R add nadd(0, Y ) Yadd(s(X ), Y ) s(add(X , Y ))With rewriting: add(s(0), 0) R s(add(0, 0)) R s(0)With narrowing: add(s(0), 0) ;R s(add(0, 0)) ;R s(0)butalso: add(Z , Y ) /o /o /o /o /o /o /o /o /o / s(add(X , Y )) /o /o /o /o /o /o /o /o / s(Y ) (rnf ):{X /Y }tt{ tt{{t{t{{ Rtt R“instantiate”tt {{{Z /s(X )}“instantiate”#add(s(X ), Y )s(add(0, Y ))with computed answer substitution {Z /s(0)}M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20096 / 34

An exampleInfinitely many narrowing derivations exist for the input calladd(Z , Y) ;{Z /0} Y.add(Z , Y) ; {Z /s n (0)} sn (Y)since there is a loop in the call graph (via unification)M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20097 / 34

Narrowing termination matters!Narrowing is extremely non–terminating, but there are many practicalsituations where narrowing termination matters, and besides it can beproven!Example Narrowing does notterminate in R id dueto uncontrolledrecursionR id id(X ) Xnid(0) 0 id(s(X )) s(id(X )) id(X ) 0 ;id X 0 ;{X /0} trueid(X ) 0 ;{X /s(X 0 )} s(id(X 0 )) 0 ;{X 0 /s(X 00 )} s(s(id(X 00 ))) 0 . . .M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20098 / 34

Narrowing termination matters!In bottom-up program analysis, often we consider semantics alsoexpressed by rulesit can be important that narrowing terminates in the denotationsE.g., in order to apply an immediate consequences operatorWe need to narrow expressions in theTR (I ) : zip{lθ 7 u l r R, r ; I ,θ u} interpretation IThe good news are that the rhs’s of semantic rules have more limitedrecursion, making narrowing terminate!Example S(R id ) {id(X ) 7 X }M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 20099 / 34

.running calls in the semanticsWhich Semantics forLogic Languages?Giorgio LeviDipartimento di InformaticaUniversità di PisaValencia, October 1989M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200910 / 34

Completeness and TerminationPrevious termination results were obtained as a by-product of addressingthe completeness of narrowing-based procedures for equational unificationHullot (1980) (unification–completeness)In canonical theories (also called “complete”), narrowing is complete as anequational unification algorithm.Example.We have seen that narrowing is able to compute the solutions for X , Y , Z s.t. add(X , Y ) E ZM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200911 / 34

Completeness and TerminationGeneral problem of symbolic reachability in non–confluent TRSs(that is, to find “more general” solutions σ such that sσ R tσ)Meseguer and Thati (2007) (reachability–completeness)Without assuming canonicity, narrowing is complete as a procedure tosolve reachability problems Example.R R add n key 0key s(0)Narrowing is still able to compute the solutions for X , Y , Z s.t. add(X , Y ) R ZThat is, we can get rid of canonicity if we are not interested in equational unification.This extends narrowing capabilities to the analysis of concurrent systems.M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200912 / 34

Completeness and TerminationIn our own work, we are interested in classes of TRSs where narrowingterminates and is strongly reachability–complete (i.e., w.r.t.non–normalized solutions)Meseguer and Thati (2007) (strong reachability–completeness)Without assuming canonicity, narrowing is strongly complete as aprocedure to solve reachability problems for two classes of TRSs:1topmost2right-linear (for linear goals)unification-completeness reachability-completenessM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200913 / 34

1Classical termination of narrowing: Christian and Hullot2Extending Hullot’s termination criterion3Getting rid of canonicity and linearity4The Narradar Termination ToolM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200914 / 34

Classical termination of narrowing:Christian and HullotThe only positive termination result was proved by J. ChristianTheorem [Christian, 1992]Narrowing terminates in left-flat TRS (lhs’s arguments are variables orground terms) that are compatible with a termination ordering Example (Non–flat rules cause echoing) R {f(f(X )) X } (f(X ), X ) ;{X/f(X0 )} (X 0 , f(X 0 )) ;{X0 /f(X00 )} (f(X 00 ), X 00 ) ; . . .M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200915 / 34

Classical termination of narrowing:Christian and HullotThe starting point for our work, a popular (but faulty!) termination resultTheorem [Hullot, 1980]Narrowing terminates in canonical TRSs if all basic narrowing derivationsissuing from the rhs’s of the rules terminate (i.e., derivations which do notreduce some blocked positions).ExampleRemind that Christian’s TRS {f(f(X )) X } is canonical and triviallysatisfies the condition on the rhs XM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200916 / 34

Classical termination of narrowing:Christian and Hullot(Faulty) Theorem [Hullot, 1980]Narrowing terminates in canonical TRSs if all basic narrowing derivationsissuing from the rhs’s of the rules terminate.(Downgraded) b.n. Theorem [Hullot’s PhD. Thesis, 1981]Basic narrowing terminates in canonical TRSs if all basic narrowingderivations issuing from the rhs’s of the rules terminate.M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200917 / 34

Classical termination of narrowing:Christian and HullotA naı̈ve generalization of Hullot’s criterion does not hold:Narrowing terminates in canonical TRSs if all basic narrowing derivationsissuing from the rhs’s of the rules terminateCounter-exampleChristian’s TRS R {f(f(X )) X } does satisfy the stronger conditionas well.M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200918 / 34

DefinitionsNarrowing s ;p,R,σ (s[r ]p )σ if a nonvariable position p of sa rule (l r ) in Ra unifier σ. s p σ lσ[σ mgu(s p , l)] Basic narrowingThe idea is to avoid narrowing phs, ρi ;σ,R hs[r ]p , ρσi if M. Alpuente, S. Escobar, J. Iborra (UPV)steps on subterms introduced by instantiationa nonvariable position p of sa rule (l r ) in Ra unifier σ. s p ρσ lσ[σ mgu(s p ρ, l)]Termination of Narrowing RevisitedPisa - October 23th, 200920 / 34

Basic narrowing terminates more oftenExample. f(f(X )) XBasic narrowing blocks the derivation of Christian’s example at the firststep (because echoing is not produced any more):6h (f(X ), X ), idi ;{X /f(X 0 )} h (X 0 , X ), {X /f(X 0 )}i ;whereas ordinary narrowing ran in a loop: (f(X ), X ) ;{X/f(X0 )} (X 0 , f(X 0 )) ;{X0 /f(X00 )} (f(X 00 ), X 00 ) ; . . .M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200921 / 34

How to get the extension?By just considering a class of TRSs identified by Réty where, for each narrowingderivation there is an commuted b. n. derivation.(Generalized) Hullot’s TheoremNarrowing terminates in TRSs that satisfy Réty’s maximal commutationproperty if basic narrowing terminates.(Réty, 1987) The TRS R satisfies the maximal commutation property if1) it is right–linear, and either left–linear or conservative (Var (l) Var (r )), and2) narrowing only produces normalized substitutions in R (this holds in left-linear CSs)M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200922 / 34

Getting rid of canonicityCanonicity is required but superfluous in Hullot’s b.n. termination result(required for deriving termination & unification–completeness in one go).(Downgraded and purged) Hullot’s b.n. TheoremBasic narrowing terminates (in canonical TRSs) if all basic narrowingderivations issuing from the rhs’s of the rules terminate.Termination CorollaryNarrowing terminates if R satisfies Réty’s maximal commutation propertyand all basic narrowing derivations issuing from the rhs’s of the rulesterminate.M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200924 / 34

Getting rid of left-linearityFrom the above corollary, we distill a practical termination criterion in twostepsFirst, we get rid of left–linearity by generalizing the class of TRSs whereRéty’s normalization condition holdsDefinitionA TRS is rnf-based if the arguments of the lhs’s of all rules are rigidnormal forms (i.e., unnarrowable)The class of rnf-based TRSs subsume (typical functional programs):left-linear CSsalmost orthogonal TRSsM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200925 / 34

Getting rid of right-linearitySecond, we get rid of right–linearity by generalizing together the rnf-basedTRSs and left–flat TRSsDefinitionleft-plain TRSs: every non-ground strict subterm of the lhs’s is a rnfright-rnf TRSs: all rhs’s are rigid normal forms (i.e., unnarrowable)reachability–complete TRSs: those where narrowing is stronglyreachability–complete(the inspiration for naming this class comes from the “complete TRSs”, asynonymous for canonical TRSs because narrowing is unification-complete inthem)M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200926 / 34

Corollary [Termination of narrowing for right-rnf TRSs]Narrowing terminates in any right-rnf TRS which is either1right-linear,2confluent and left–plain, or3topmost** in case (1), for linear input termsThis––––result is very handy sinceit is (almost) syntactical, and does not resort to termination orderingsit dispenses with linearity in some casesit applies to TRSs that are not purely left-flat or rnf-basedit ensures reachability completeness as wellM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200927 / 34

Some final examplesExampleNote that R add satisfies all the criteria, except for right-rnfAlso note that Christian’s example is right-rnf and right linear (butthe input call was not linear)ExampleExponentiation function (used as a primitive operation for key exchange inthe Diffie-Hellman key agreement protocol) where * and g are constructorsexp(exp(g,y),z) exp(g, y * z)This rule satisfies both criteria (1) and (2), hence narrowing terminatesM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200928 / 34

The Narradar Termination Tool. Enjoy!http://safe-tools.dsic.upv.es/narradarM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200930 / 34

Additional resultsNarradar is also based on additional results regarding modularity andmechanization of termination proofs by using dependency pairs.Alpuente, M., Escobar, S., and Iborra, J. (2008a).Modular Termination of Basic Narrowing.In Proc. RTA 2008, Springer LNCS 5117:1–16.Alpuente, M., Escobar, S., and Iborra, J. (2008b).Termination of Narrowing using Dependency Pairs.In Proc. ICLP 2008, Springer LNCS 5366: 317-33.M. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200931 / 34

Wrap upRestrictions on RLF cTRL (LL or Co) NC R–bnTR-rnf L rnf–BRL R-rnf ( linear term)LP RC R-rnfR-rnf LP CR-rnf TpRL (LL or Co) NC StReference(Christian, 1992)(Hullot’s result generalized)e.g. R-rnf L CSe.g. R-rnf (either aO or CS C)using (Nieuwenhuis, nstructor eft–flatLlinearaOalmost Orthogonalbasic narrowing terminatesNCRety’s normalization conditionall basic narrowing derivations starting from rule rhs’s terminatestandard theories saturated by basic paramodulationcompatible with a termination orderingFigure: Summary of criteria for narrowing terminationM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200932 / 34

ConclusionMain resultsi We extend to narrowing Hullot’s b.n. theorem and drop canonicityii By considering the class of strongly reachability-complete TRSs, weprove termination in a number of TRSs where neither canonicity norlinearity are assumed.iii We developed an automated termination prover that is publiclyavailableOne plus: some of our results are based (and hence preserve) reachabilitycompleteness, besides ensuring terminationM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200933 / 34

Thank you!The Valencian School of Giorgio LeviM. Alpuente, S. Escobar, J. Iborra (UPV)Termination of Narrowing RevisitedPisa - October 23th, 200934 / 34

Termination of Narrowing Revisited Mar a Alpuente Departmento de Sistemas Inform aticos y Computaci on (DSIC) Technical University of Valencia (UPV)