- -

Derivational Complexity and Context-Sensitive Rewriting

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

  • Estadisticas de Uso

Derivational Complexity and Context-Sensitive Rewriting

Show full item record

Lucas Alba, S. (2021). Derivational Complexity and Context-Sensitive Rewriting. Journal of Automated Reasoning. 65(8):1191-1229. https://doi.org/10.1007/s10817-021-09603-1

Por favor, use este identificador para citar o enlazar este ítem: http://hdl.handle.net/10251/183402

Files in this item

Item Metadata

Title: Derivational Complexity and Context-Sensitive Rewriting
Author: Lucas Alba, Salvador
UPV Unit: Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació
Issued date:
Abstract:
[EN] Context-sensitive rewriting is a restriction of rewriting where reduction steps are allowed on specific arguments mu(f) subset of {1, ..., k} of k-ary function symbols f only. Terms which cannot be further rewritten ...[+]
Subjects: Derivational complexity , Term rewriting , Termination
Copyrigths: Reserva de todos los derechos
Source:
Journal of Automated Reasoning. (issn: 0168-7433 )
DOI: 10.1007/s10817-021-09603-1
Publisher:
Springer-Verlag
Publisher version: https://doi.org/10.1007/s10817-021-09603-1
Project ID:
info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C32/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/
info:eu-repo/grantAgreement/GENERALITAT VALENCIANA//PROMETEO%2F2019%2F098//DEEPTRUST/
Thanks:
Partially supported by the EU (FEDER), and projects RTI2018-094403-B-C32 and PROMETEO/2019/098.
Type: Artículo

References

Alarcón, B., Lucas, S., Navarro-Marset, R.: Proving termination with matrix interpretations over the reals. In: Geser, A., Waldmann, J. (eds.). Proceedings of the 10th International Workshop on Termination, WST 2009), HTWK Leipzig, pp. 12–15 (2009a)

Alarcón, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Lucio, P., Moreno, G., Peña, R. (eds.). Actas de las IX Jornadas de Programación y Lenguajes (PROLE 2009), SISTEDES, pp. 268–2–77 (2009b)

Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8 [+]
Alarcón, B., Lucas, S., Navarro-Marset, R.: Proving termination with matrix interpretations over the reals. In: Geser, A., Waldmann, J. (eds.). Proceedings of the 10th International Workshop on Termination, WST 2009), HTWK Leipzig, pp. 12–15 (2009a)

Alarcón, B., Lucas, S., Navarro-Marset, R.: Using matrix interpretations over the reals in proofs of termination. In: Lucio, P., Moreno, G., Peña, R. (eds.). Actas de las IX Jornadas de Programación y Lenguajes (PROLE 2009), SISTEDES, pp. 268–2–77 (2009b)

Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theor. Comput. Sci. 236(1–2), 133–178 (2000). https://doi.org/10.1016/S0304-3975(99)00207-8

Arts, T., Giesl, J.: A collection of examples for termination of term rewriting using dependency pairs. Tech. Rep. AIB-2001-09, RWTH Aachen, Germany (2001)

Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J.W., Nijman, A.J., Treleaven, P.C. (eds.). PARLE (2), Springer, Lecture Notes in Computer Science, vol. 259, pp. 141–158 (1987)

Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Complexity classes and rewrite systems with polynomial interpretation. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.). Computer Science Logic, 12th International Workshop, CSL ’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24–28, 1998, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1584, pp. 372–384, (1998) https://doi.org/10.1007/10703163_25

Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Prog. 11(1), 33–53 (2001)

Cichon, A., Lescanne, P.: Polynomial interpretations and the complexity of algorithms. In: Kapur, D. (ed.). Automated Deduction: CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15–18, 1992, Proceedings, Springer, Lecture Notes in Computer Science, vol. 607, pp. 139–147, (1992) https://doi.org/10.1007/3-540-55602-8_161

Cichon, E.: Termination orderings and complexity characterizations. In: Aczell, S., Wainer (eds.). Proof Theory: a selection of papers from the Leeds Proof Theory Programme, 1990, Cambridge University Press, Lecture Notes in Computer Science, vol. 607, pp. 171–194 (1992)

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: All About Maude: A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007). https://doi.org/10.1007/978-3-540-71999-1

Contejean, E., Marché, C., Tomás, A.P., Urbain, X.: Mechanically proving termination using polynomial interpretations. J. Autom. Reason. 34(4), 325–363 (2005). https://doi.org/10.1007/s10817-005-9022-x

Courcelle, B.: Recursive applicative program schemes. In: van Leeuwen, J. (ed.). Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, Elsevier and MIT Press, pp. 459–492 (1990) https://doi.org/10.1016/b978-0-444-88074-1.50014-7

Dershowitz, N.: A note on simplification orderings. Inf. Process. Lett. 9(5), 212–215 (1979). https://doi.org/10.1016/0020-0190(79)90071-1

Dershowitz, N.: 33 examples of termination. In: Comon, H., Jouannaud, J. (eds.). Term Rewriting, French Spring School of Theoretical Computer Science, Font Romeux, France, May 17–21, 1993, Advanced Course, Springer, Lecture Notes in Computer Science, vol. 909, pp. 16–26, (1993) https://doi.org/10.1007/3-540-59340-3_2

Durán, F., Escobar, S., Lucas, S.: New Evaluation Commands for Maude Within Full Maude. In: Martí-Oliet, N. (ed.). Proceedings of the Fifth International Workshop on Rewriting Logic and Its Applications, WRLA 2004, Barcelona, Spain, March 27–28, 2004, Elsevier, Electronic Notes in Theoretical Computer Science, vol. 117, pp. 263–284, (2004) https://doi.org/10.1016/j.entcs.2004.06.014

Durán, F., Eker, S., Escobar, S., Martí-Oliet, N., Meseguer, J., Rubio, R., Talcott, C.L.: Programming and symbolic computation in Maude. J. Log. Algebra Method Prog. (2020). https://doi.org/10.1016/j.jlamp.2019.100497

Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008)

Fasel, J.H., Hudak, P., Jones, S.L.P., Wadler, P.: SIGPLAN notices special issue on the functional programming language haskell. ACM SIGPLAN Not. 27(5), 1 (1992)

Futatsugi, K., Nakagawa, A.T.: An overview of CAFE specification environment: an algebraic approach for creating, verifying, and maintaining formal specifications over networks. In: First IEEE International Conference on Formal Engineering Methods, ICFEM 1997, Hiroshima, Japan, November 12–14, 1997, Proceedings, IEEE Computer Society, pp. 170–182, (1997) https://doi.org/10.1109/ICFEM.1997.630424

Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and improving dependency pairs. J. Autom. Reason. 37(3), 155–203 (2006). https://doi.org/10.1007/s10817-006-9057-7

Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Analyzing Program Termination and Complexity Automatically with AProVE. J. Autom. Reason. 58(1), 3–31 (2017). https://doi.org/10.1007/s10817-016-9388-y

Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamada, A.: The termination and complexity competition. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.). Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III, Springer, Lecture Notes in Computer Science, vol. 11429, pp. 156–166, (2019) https://doi.org/10.1007/978-3-030-17502-3_10

Goguen, J.A., Winkler, T., Meseguer, J., Futatsugi, K., Jouannaud, J.P.: Introducing obj Software Engineering with OBJ: algebraic specification in action:169–236 (2000)

Gramlich, B., Lucas, S.: Modular termination of context-sensitive rewriting. In: Proceedings of the 4th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, October 6-8, 2002, Pittsburgh, PA, USA (Affiliated with PLI 2002), ACM, pp. 50–61, (2002a) https://doi.org/10.1145/571157.571163

Gramlich, B., Lucas, S.: Simple termination of context-sensitive rewriting. In: Fischer, B., Visser, E. (eds.). Proceedings of the 2002 ACM SIGPLAN Workshop on Rule-Based Programming, Pittsburgh, Pennsylvania, USA, 2002, ACM, pp. 29–42, (2002b) https://doi.org/10.1145/570186.570189

Grzegorczyk, A.: Some classes of recursive functions. J. Symbol. Logic 20(1), 71–72 (1955). https://doi.org/10.2307/2268082

Gutiérrez, R., Lucas, S.: mu-term: Verify termination properties automatically (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.). Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, Springer, Lecture Notes in Computer Science, vol. 12167, pp. 436–447, (2020) https://doi.org/10.1007/978-3-030-51054-1_28

Hirokawa, N., Moser, G.: Automated complexity analysis based on the dependency pair method. In: Armando, A., Baumgartner, P., Dowek, G. (eds.). Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12–15, 2008, Proceedings, Springer, Lecture Notes in Computer Science, vol. 5195, pp. 364–379, (2008) https://doi.org/10.1007/978-3-540-71070-7_32

Hirokawa, N., Moser, G.: Automated complexity analysis based on context-sensitive rewriting. In: Dowek, G. (ed.). Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings, Springer, Lecture Notes in Computer Science, vol. 8560, pp. 257–271, (2014) https://doi.org/10.1007/978-3-319-08918-8_18

Hirokawa, N., Nagele, J., Middeldorp, A.: Cops and CoCoWeb: Infrastructure for Confluence Tools. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.). Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Springer, Lecture Notes in Computer Science, vol. 10900, pp. 346–353, (2018) https://doi.org/10.1007/978-3-319-94205-6_23

Hofbauer, D.: Termination proofs by multiset path orderings imply primitive recursive derivation lengths. Theor. Comput. Sci. 105(1), 129–140 (1992). https://doi.org/10.1016/0304-3975(92)90289-R

Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations (preliminary version). In: Dershowitz, N. (ed.). Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3–5, 1989, Proceedings, Springer, Lecture Notes in Computer Science, vol. 355, pp. 167–177, (1989) https://doi.org/10.1007/3-540-51081-8_107

Knuth, D.E., Bendix, P.E.: Simple word problems in universal algebra. In: Leech, J. (ed.). Computational Problems in Abstract Algebra, Pergamon Press, pp. 263–297 (1970)

Lankford, D.S.: On proving term rewriting systems are noetherian. Louisiana Technological University, Ruston, LA, Tech. rep (1979)

Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002a). https://doi.org/10.1006/inco.2002.3176

Lucas, S.: Termination of (canonical) context-sensitive rewriting. In: Tison, S. (ed.). RTA, Springer, Lecture Notes in Computer Science, vol. 2378, pp. 296–310 (2002b)

Lucas, S.: A note on completeness of conditional context-sensitive rewriting. In: 5th International Workshop on Reduction Strategies in Rewriting and Programming, pp. 3–15. University of Kyoto, WRS (2005a)

Lucas, S.: Polynomials over the reals in proofs of termination: from theory to practice. ITA 39(3), 547–586 (2005b). https://doi.org/10.1051/ita:2005029

Lucas, S.: Context-sensitive rewriting. ACM Comput. Surv. 53(4), 78:1–78:36 (2020). https://doi.org/10.1145/3397677

Lucas, S.: Applications and extensions of context-sensitive rewriting. J. Logical Algebraic Methods Prog. 121, 100680 (2021). https://doi.org/10.1016/j.jlamp.2021.100680

Manna, Z., Ness, S.: On the termination of Markov algorithms. In: Proceedings of the Third Hawaii International Conference on System Science, pp. 789–792 (1970)

McCarthy, J.: Towards a mathematical science of computation. In: Information Processing, Proceedings of the 2nd IFIP Congress 1962, Munich, Germany, August 27–September 1, 1962, North-Holland, pp. 21–28 (1962)

Middeldorp, A.: Call by need computations to root-stable form. In: Lee, P., Henglein, F., Jones, N.D. (eds.). Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium, Paris, France, 15–17 January 1997, ACM Press, pp. 94–105 (1997) https://doi.org/10.1145/263699.263711

Moser, G., Schnabl, A.: The derivational complexity induced by the dependency pair method. Logical Methods Comput. Sci. (2011). https://doi.org/10.2168/LMCS-7(3:1)2011

Moser, G., Schnabl, A., Waldmann, J.: Complexity analysis of term rewriting based on matrix and context dependent interpretations. In: Hariharan, R., Mukund, M., Vinay, V. (eds.). IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9–11, 2008, Bangalore, India, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 2, pp. 304–315 (2008). https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1762

Neurauter, F., Middeldorp, A.: Revisiting matrix interpretations for proving termination of term rewriting. In: Schmidt-Schauß, M. (ed.). Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30–June 1, 2011, Novi Sad, Serbia, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 10, pp. 251–266 (2011), https://doi.org/10.4230/LIPIcs.RTA.2011.251

Neurauter, F., Zankl, H., Middeldorp, A.: Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In: Fermüller, C.G., Voronkov, A. (eds.). Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings, Springer, Lecture Notes in Computer Science, vol. 6397, pp. 550–564 (2010), https://doi.org/10.1007/978-3-642-16242-8_39

Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reason. 51(1), 27–56 (2013). https://doi.org/10.1007/s10817-013-9277-6

Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002)

Péchoux, R.: Synthesis of sup-interpretations: a survey. Theor. Comput. Sci. 467, 30–52 (2013). https://doi.org/10.1016/j.tcs.2012.11.003

Rapp, F., Middeldorp, A.: FORT 2.0. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.). Automated Reasoning: 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14–17, 2018, Proceedings, Springer, Lecture Notes in Computer Science, vol. 10900, pp. 81–88 (2018), https://doi.org/10.1007/978-3-319-94205-6_6

Ritchie, R.W.: Classes of predictably computable functions. Trans. Am. Math. Soc. 106, 139–173 (1963)

Rubio, R., Martí-Oliet, N., Pita, I., Verdejo, A.: Parameterized Strategies Specification in Maude. In: Fiadeiro, J.L., Tutu, I. (eds.). Recent Trends in Algebraic Development Techniques: 24th IFIP WG 1.3 International Workshop, WADT 2018, Egham, UK, July 2-5, 2018, Revised Selected Papers, Springer, Lecture Notes in Computer Science, vol. 11563, pp. 27–44 (2018), https://doi.org/10.1007/978-3-030-23220-7_2

Steinbach, J.: Proving polynomials positive. In: Shyamasundar, R.K. (ed.). Foundations of Software Technology and Theoretical Computer Science, 12th Conference, New Delhi, India, December 18–20, 1992, Proceedings, Springer, Lecture Notes in Computer Science, vol. 652, pp. 191–202 (1992), https://doi.org/10.1007/3-540-56287-7_105

Sternagel, C., Thiemann, R.: Signature extensions preserve termination: an alternative proof via dependency pairs. In: Dawar, A., Veith, H. (eds.). Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23–27, 2010. Proceedings, Springer, Lecture Notes in Computer Science, vol. 6247, pp. 514–528 (2010), https://doi.org/10.1007/978-3-642-15205-4_39

Terese.: Term Rewriting Systems, Cambridge tracts in theoretical computer science, vol. 55. Cambridge University Press (2003)

Waldmann, J.: Polynomially bounded matrix interpretations. In: Lynch, C. (ed.). Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11–13, 2010, Edinburgh, Scottland, UK, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, LIPIcs, vol. 6, pp. 357–372 (2010), https://doi.org/10.4230/LIPIcs.RTA.2010.357

Weiermann, A.: Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths. Theor. Comput.Sci. 139(1 & 2), 355–362 (1995). https://doi.org/10.1016/0304-3975(94)00135-6

Zantema, H.: Termination of term rewriting: interpretation and type elimination. J. Symb. Comput. 17(1), 23–50 (1994). https://doi.org/10.1006/jsco.1994.1003

Zantema, H.: Termination of context-sensitive rewriting. In: Comon, H. (ed.). Rewriting Techniques and Applications, 8th International Conference, RTA-97, Sitges, Spain, June 2–5, 1997, Proceedings, Springer, Lecture Notes in Computer Science, vol. 1232, pp. 172–186 (1997), https://doi.org/10.1007/3-540-62950-5_69

[-]

recommendations

 

This item appears in the following Collection(s)

Show full item record