- -

Derivational Complexity and Context-Sensitive Rewriting

RiuNet: Repositorio Institucional de la Universidad Politécnica de Valencia

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Derivational Complexity and Context-Sensitive Rewriting

Mostrar el registro sencillo del ítem

Ficheros en el ítem

Thumbnail
Nombre: Lucas - Derivational ...
Tamaño: 799.9Kb
Formato: PDF
Descripción: Versión editorial
Abrir
dc.contributor.author Lucas Alba, Salvador es_ES
dc.date.accessioned 2022-06-16T18:05:38Z
dc.date.available 2022-06-16T18:05:38Z
dc.date.issued 2021-12 es_ES
dc.identifier.issn 0168-7433 es_ES
dc.identifier.uri http://hdl.handle.net/10251/183402
dc.description.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 in this way are called mu-normal forms. For left-linear term rewriting systems (TRSs), the so-called normalization via mu-normalization procedure provides a systematic way to obtain normal forms by the stepwise computation and combination of intermediate mu-normal forms. In this paper, we show how to obtain bounds on the derivational complexity of computations using this procedure by using bounds on the derivational complexity of context-sensitive rewriting. Two main applications are envisaged: Normalization via mu-normalization can be used with non-terminating TRSs where the procedure still terminates; on the other hand, it can be used to improve on bounds of derivational complexity of terminating TRSs as it discards many rewritings. es_ES
dc.description.sponsorship Partially supported by the EU (FEDER), and projects RTI2018-094403-B-C32 and PROMETEO/2019/098. es_ES
dc.language Inglés es_ES
dc.publisher Springer-Verlag es_ES
dc.relation.ispartof Journal of Automated Reasoning es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Derivational complexity es_ES
dc.subject Term rewriting es_ES
dc.subject Termination es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Derivational Complexity and Context-Sensitive Rewriting es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1007/s10817-021-09603-1 es_ES
dc.relation.projectID 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/ es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GENERALITAT VALENCIANA//PROMETEO%2F2019%2F098//DEEPTRUST/ es_ES
dc.rights.accessRights Abierto es_ES
dc.contributor.affiliation Universitat Politècnica de València. Departamento de Sistemas Informáticos y Computación - Departament de Sistemes Informàtics i Computació es_ES
dc.description.bibliographicCitation 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 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1007/s10817-021-09603-1 es_ES
dc.description.upvformatpinicio 1191 es_ES
dc.description.upvformatpfin 1229 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 65 es_ES
dc.description.issue 8 es_ES
dc.relation.pasarela S\444864 es_ES
dc.contributor.funder GENERALITAT VALENCIANA es_ES
dc.contributor.funder AGENCIA ESTATAL DE INVESTIGACION es_ES
dc.description.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) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references Bonfante, G., Cichon, A., Marion, J., Touzet, H.: Algorithms with polynomial interpretation termination proof. J. Funct. Prog. 11(1), 33–53 (2001) es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references Endrullis, J., Waldmann, J., Zantema, H.: Matrix interpretations for proving termination of term rewriting. J. Autom. Reason. 40(2–3), 195–220 (2008) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references Grzegorczyk, A.: Some classes of recursive functions. J. Symbol. Logic 20(1), 71–72 (1955). https://doi.org/10.2307/2268082 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references Lankford, D.S.: On proving term rewriting systems are noetherian. Louisiana Technological University, Ruston, LA, Tech. rep (1979) es_ES
dc.description.references Lucas, S.: Context-sensitive rewriting strategies. Inf. Comput. 178(1), 294–343 (2002a). https://doi.org/10.1006/inco.2002.3176 es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references Lucas, S.: Context-sensitive rewriting. ACM Comput. Surv. 53(4), 78:1–78:36 (2020). https://doi.org/10.1145/3397677 es_ES
dc.description.references 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 es_ES
dc.description.references 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) es_ES
dc.description.references 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) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references Ohlebusch, E.: Advanced Topics in Term Rewriting. Springer (2002) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references Ritchie, R.W.: Classes of predictably computable functions. Trans. Am. Math. Soc. 106, 139–173 (1963) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references Terese.: Term Rewriting Systems, Cambridge tracts in theoretical computer science, vol. 55. Cambridge University Press (2003) es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES
dc.description.references 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 es_ES


Este ítem aparece en la(s) siguiente(s) colección(ones)

Mostrar el registro sencillo del ítem