Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 8/2020

16.01.2020

The 2D Dependency Pair Framework for Conditional Rewrite Systems—Part II: Advanced Processors and Implementation Techniques

verfasst von: Salvador Lucas, José Meseguer, Raúl Gutiérrez

Erschienen in: Journal of Automated Reasoning | Ausgabe 8/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Proving termination of programs in ‘real-life’ rewriting-based languages like CafeOBJ, Haskell, Maude, etc., is an important subject of research. To advance this goal, faithfully capturing the impact in the termination behavior of the main language features (e.g., conditions in program rules) is essential. In Part I of this work, we have introduced a 2D Dependency Pair Framework for automatically proving termination properties of Conditional Term Rewriting Systems. Our framework relies on the notion of processor as the main practical device to deal with proofs of termination properties of conditional rewrite systems. Processors are used to decompose and simplify the proofs in a divide and conquer approach. With the basic proof framework defined in Part I, here we introduce new processors to further improve the ability of the 2D Dependency Pair Framework to deal with proofs of termination properties of conditional rewrite systems. We also discuss relevant implementation techniques to use such processors in practice.
Vorheriger Artikel Theorem Proving for Pointwise Metric Temporal Logic Over the Naturals via Translations
Nächster Artikel Loop-Type Sequent Calculi for Temporal Logic

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
1
In the following, iff abbreviates if and only if.
 
2
Schernhammer and Gramlich considered this implementation of integer division as an example of a ‘careless’ definition of a program where detecting operational nontermination “points to a flaw in the specification of R allowing division by zero” [30, p. 675]. However, they could not provide an automatic proof of operational nontermination.
 
3
A k-ary symbol f is defined in a CTRS \(\mathcal{R}\) if there is a rule \(f(\ell _1,\ldots ,\ell _k)\rightarrow r\Leftarrow c\) in \(\mathcal{R}\).
 
4
Note that the inference rules are schematic in the sense that each inference rule \(\frac{B_1~\cdots ~B_n}{A}\) can be used under any instance \(\frac{\sigma (B_1)~\cdots ~\sigma (B_n)}{\sigma (A)}\) of the rule by a substitution \(\sigma \).
 
5
Our definition of operational termination depends on the (reasonable, but discretional) use of well-formed proof trees; see [18, Sect. 3.1] for a discussion about the impact of this decision in the analysis of the termination behavior of computational systems.
 
6
In [24], three notions of chain of dependency pairs, namely, H-, V-, and O-chains, were introduced and applied to prove termination, V-termination, and operational termination, respectively. H-chains, though, use dependency pairs that we do not consider here.
 
7
Actually, the cycle could also be dismissed by using the satisfiability approach in [20, Sect. 4.5]. This would immediately lead to an operational termination proof. However, we use the simpler (syntactic) approximation described in [27, Sect. 7.1.1] and delay the final proof to provide an application of our next processor in Sect. 4.3.
 
8
See [18, Sect. 5.5.1] for details about its practical use in proofs of termination by satisfiability.
 
9
By a definite Horn theory we mean a set of universally quantified clauses \(\lnot A_1\vee \cdots \vee \lnot A_n\vee B\) (or \(A_1\wedge \cdots \wedge A_n \Rightarrow B\) in implication form), where \(A_1,\ldots ,A_n,B\) are atoms for some \(n\ge 0\).
 
10
A TRS is said to be innermost terminating if the (one-step) innermost rewriting relation \(\rightarrow _i\), which rewrites terms only if they contain no other redex, is terminating.
 
11
A ‘normalized instance’ of a term t is an instance \(\sigma (t)\) by a substitution \(\sigma \) such that \(\sigma (x)\) is a normal form for all variables \(x\in \mathcal{V}ar(t)\).
 
12
In a reduction pair \((\succsim ,\succ )\) consists of a reflexive, transitive, monotonic (closed under contexts) and stable (closed under substitutions) relation \(\succsim \), and a stable well-founded ordering \(\succ \) such that \(\succsim \circ \succ \,\subseteq \,\succ \) or \(\succ \circ \succsim \,\subseteq \,\succ \) [12, Sect. 2.3].
 
15
The use of \({\textsf {P}}_{{ NC }}\) in [26, Sect. 6.2] with the CTRS in Example 15 would lead to a wrong proof of operational termination. The corrected version of \({\textsf {P}}_{{ NC }}\) which is presented in this paper, though, is the one implemented in the Termination Competition version of mu-term.
 
Literatur
1.
Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000)MathSciNetCrossRef
2.
Alarcón, B., Gutiérrez, R., Lucas, S., Navarro-Marset, R.: Proving termination properties with MU-TERM. In: Proceedings of AMAST’10, LNCS, vol. 6486, pp. 201–208 (2011)
3.
Baader, F., Nipkow, T.: Term Rewriting and all That. Cambridge University Press, Cambridge (1998)CrossRef
4.
Barwise, J.: An introduction to first-order logic. In: Barwise, J. (ed.) Handbook of Mathematical Logic. North-Holland, Amsterdam (1977)
5.
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude—A High-Performance Logical Framework. LNCS 4350, Springer, New York (2007)
6.
Contejean, E., Marché, C., Tomás, A.-P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2006)MathSciNetCrossRef
7.
8.
Durán, F., Lucas, S., Meseguer, J.: MTT: the Maude termination tool (system description). In: Proceedings of IJCAR’08, LNAI, vol. 5195, pp. 313–319 (2008)
9.
Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008)MathSciNetCrossRef
10.
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic Termination proofs in the dependency pair framework. In: Proceeding of IJCAR’06, LNAI, vol. 4130, pp. 281–286 (2006)
11.
Giesl, J., Thiemann, R., Schneider-Kamp, P.: The dependency pair framework: combining techniques for automated termination proofs. In: Proceedings of LPAR’04, LNAI, vol. 3452, pp. 301–331 (2004)
12.
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006)MathSciNetCrossRef
13.
Goguen, J., Meseguer, J.: Models and equality for logical programming. In: Proceedings of TAPSOFT’87, LNCS, vol. 250, pp. 1–22 (1987)
14.
15.
Hirokawa, N., Middeldorp, A.: Dependency pairs revisited. In: Proceedings of RTA’04, LNCS, vol. 3091, pp. 249–268 (2004)
16.
Hodges, W.: Elementary predicate logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 1, pp. 1–131. Reidel Publishing Company, Dordrecht (1983)
17.
Lankford, D.S.: On proving term rewriting systems are noetherian. Technical Report, Louisiana Technological University, Ruston, LA (1979)
18.
19.
Lucas, S., Gutiérrez, R.: Automatic synthesis of logical models for order-sorted first-order theories. J. Autom. Reason. 60(4), 465–501 (2018)MathSciNetCrossRef
20.
Lucas, S., Gutiérrez, R.: Use of logical models for proving infeasibility in term rewriting. Inf. Process. Lett. 136, 90–95 (2018)MathSciNetCrossRef
21.
Lucas, S., Marché, C., Meseguer, J.: Operational termination of conditional term rewriting systems. Inf. Process. Lett. 95, 446–453 (2005)MathSciNetCrossRef
22.
Lucas, S., Meseguer, J.: Models for logics and conditional constraints in automated proofs of termination. In: Proceedings of AISC’14, LNAI, vol. 8884, pp. 9–20 (2014)
23.
Lucas, S., Meseguer, J.: 2D Dependency pairs for proving operational termination of CTRSs. In: Escobar, S., (ed) Proceedings of the 10th International Workshop on Rewriting Logic and its Applications, WRLA’14, LNCS, vol. 8663, pp. 195–212 (2014)
24.
Lucas, S., Meseguer, J.: Dependency pairs for proving termination properties of conditional term rewriting systems. J. Log. Algebr. Methods Program. 86, 236–268 (2017)MathSciNetCrossRef
25.
Lucas, S., Meseguer, J.: Normal forms and normal theories in conditional rewriting. J. Log. Algebr. Methods Program. 85(1), 67–97 (2016)MathSciNetCrossRef
26.
Lucas, S., Meseguer, J., Gutiérrez, R.: Extending the 2D DP framework for conditional term rewriting systems. In: Selected Papers from LOPSTR’14, LNCS, vol. 8981, pp. 113–130 (2015)
27.
Lucas, S., Meseguer, J., Gutiérrez, R.: The 2D dependency pair framework for conditional rewrite systems. Part I: Definition and basic processors. J. Comput. Syst. Sci. 96, 74–106 (2018)MathSciNetCrossRef
28.
29.
Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer, New York (2002)CrossRef
30.
Schernhammer, F., Gramlich, B.: Characterizing and proving operational termination of deterministic conditional term rewriting systems. J. Log. Algebr. Program. 79, 659–688 (2010)MathSciNetCrossRef
31.
Sternagel, T., Middeldorp, A.: Conditional confluence (system description). In: Proceedings of RTA-TLCA’14, LNCS, vol. f8560, pp. 456–465 (2014)
32.
Sternagel, T., Middeldorp, A.: Infeasible conditional critical pairs. In: Proceedings of IWC’15, pp. 13–18 (2014)
33.
Thiemann, R.: The DP Framework for Proving Termination of Term Rewriting. PhD Thesis, RWTH Aachen, Technical Report AIB-2007-17 (2007)
34.
Thiemann, R., Giesl, J., Schneider-Kamp, P.: Improved modular termination proofs using dependency pairs. In: Proceedings of IJCAR’04, LNAI, vol. 3097, pp. 75–90 (2004)
35.
Metadaten
Titel
The 2D Dependency Pair Framework for Conditional Rewrite Systems—Part II: Advanced Processors and Implementation Techniques
verfasst von
Salvador Lucas
José Meseguer
Raúl Gutiérrez
Publikationsdatum
16.01.2020
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 8/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-020-09542-3