《Improving dependency pairs》由会员分享，可在线阅读，更多相关《Improving dependency pairs（15页珍藏版）》请在金锄头文库上搜索。
1、Improving Dependency PairsJ urgen Giesl, Ren e Thiemann, Peter Schneider-Kamp, Stephan FalkeLuFG Informatik II, RWTH Aachen, Ahornstr. 55, 52074 Aachen, Germanyfgiesl|thiemannginformatik.rwth-aachen.defnowonder|spfgi2.informatik.rwth-aachen.deAbstract. The dependency pair approach is one of the most
2、 powerfultechniques for termination and innermost termination proofs of term re-write systems (TRSs). For any TRS, it generates inequality constraintsthat have to be satis ed by weakly monotonic well-founded orders. Weimprove the dependency pair approach by considerably reducing thenumber of constra
3、ints produced for (innermost) termination proofs.Moreover, we extend transformation techniques to manipulate depen-dency pairs which simplify (innermost) termination proofs signi cantly.In order to fully automate the dependency pair approach, we show howtransformation techniques and the search for s
4、uitable orders can be mech-anized e ciently. We implemented our results in the automated termina-tion prover AProVE and evaluated them on large collections of examples.1 IntroductionMost traditional methods to prove termination of TRSs (automatically) usesimpli cation orders 7,24, where a term is gr
5、eater than its proper subterms.However, there are numerous important TRSs which are not simply terminating,i.e., their termination cannot be shown by simpli cation orders. Therefore, thedependency pair approach 2,11,12 was developed which allows the applicationof simpli cation orders to non-simply t
6、erminating TRSs. In this way, the classof systems where termination is provable mechanically increases signi cantly.Example 1. The following TRS from 2 is not simply terminating, since in thelast quot-rule, the left-hand side is embedded in the right-hand side if y is instan-tiated with s(x). Thus,
7、classical approaches for automated termination proofsfail on this example, while it is easy to handle with dependency pairs.minus(x;0)!x quot(0;s(y)!0minus(s(x);s(y)!minus(x;y) quot(s(x);s(y)!s(quot(minus(x;y);s(y)In Sect. 2, we recapitulate the dependency pair approach for termination andinnermost
8、termination proofs. Then we show that the approach can be improvedsigni cantly by reducing the constraints for termination (Sect. 3) and innermosttermination (Sect. 4). Sect. 5 introduces new conditions for transforming depen-dency pairs in order to simplify (innermost) termination proofs further.Fo
9、r automated (innermost) termination proofs, the constraints generated bythe dependency pair approach are pre-processed by an argument ltering andafterwards, one tries to solve them by standard simpli cation orders. We presentan algorithm to generate argument lterings in our improved dependency paira
10、pproach (Sect. 6) and discuss heuristics to increase e ciency in Sect. 7.Our improvements and algorithms are implemented in our termination proverAProVE. We give empirical results which show that they are extremely successfulin practice. Thus, our contributions are also very helpful for other tools
11、based ondependency pairs (1, CiME 6, TTT 16) and we conjecture that they can alsobe used in other recent approaches for termination of TRSs 5,10 which haveseveral aspects in common with dependency pairs. Finally, dependency pairs canbe combined with other termination techniques (e.g., in 25 we integ
12、rated depen-dency pairs and the size-change principle from termination analysis of functional19 and logic programs 9). Moreover, the system TALP 22 uses dependencypairs for termination proofs of logic programs. Thus, improving dependency pairsis also useful for termination analysis of other kinds of
13、 programming languages.All proofs and details on our experiments can be found in 13.2 Dependency PairsWe brie y present the dependency pair approach of Arts and Giesl and referto 2,11,12 for re nements and motivations. We assume familiarity with termrewriting (see, e.g., 4). For a TRS R over a signa
14、ture F, the de ned symbolsD are the root symbols of the left-hand sides of rules and the constructors areC =FnD. We restrict ourselves to nite signatures and TRSs. Let F =ffjf2Dgbe a set of tuple symbols, where f has the same arity as f and we oftenwrite F for f, etc. If t = g(t1;:;tm) with g2D, we
15、write t for g(t1;:;tm).De nition 2 (Dependency Pair). If l!r2R and t is a subterm of r withde ned root symbol, then the rewrite rule l!t is called a dependency pair ofR. The set of all dependency pairs of R is denoted by DP(R).So the dependency pairs of the TRS in Ex. 1 areMINUS(s(x);s(y)!MINUS(x;y)
16、 (1) QUOT(s(x);s(y)!MINUS(x;y) (2)QUOT(s(x);s(y)!QUOT(minus(x;y);s(y) (3)To use dependency pairs for (innermost) termination proofs, we need the no-tion of (innermost) chains. We always assume that di erent occurrences of de-pendency pairs are variable disjoint and we always consider substitutions whosedomains may be in nite. Here, i!R denotes innermost reductions.De nition 3 (R-Chain). A sequence of dependency pairs s1!t1, s2!t2;:is a
