- -

Context-sensitive Rewriting

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

Compartir/Enviar a

Citas

Estadísticas

  • Estadisticas de Uso

Context-sensitive Rewriting

Mostrar el registro sencillo del ítem

Ficheros en el ítem

[Cerrado]
Nombre: Lucas - Context-s ...
Tamaño: 881.5Kb
Formato: PDF
Descripción: Versión editorial
Solicitar una copia al autor
dc.contributor.author Lucas Alba, Salvador es_ES
dc.date.accessioned 2021-05-20T03:33:28Z
dc.date.available 2021-05-20T03:33:28Z
dc.date.issued 2020-09 es_ES
dc.identifier.issn 0360-0300 es_ES
dc.identifier.uri http://hdl.handle.net/10251/166526
dc.description.abstract [EN] The appropriate selection of the arguments of functions that can be evaluated in function calls is often useful to improve efficiency, speed, termination behavior, and so on. This is essential, e.g., in the conditional if - then - else operator. We can specify this by associating a set mu( f) of indices of evaluable arguments to each function symbol f. With mu(if-then-else) = {1}, only the Boolean argument b in calls if b then e else e' is evaluated. In the realm of term rewriting, this is called context-sensitive rewriting. It has been proven useful to improve the termination behavior of rewriting computations while it is still able to compute (or approximate) canonical forms like head-normal forms, (infinite) values, and (infinite) normal forms by requiring a few reasonable conditions. This article provides an overview of basic results to use context-sensitive rewriting in practice. es_ES
dc.description.sponsorship Supported by the EU (FEDER) and projects RTI2018-094403-B-C32, PROMETEO/2019/098, and SP20180225. es_ES
dc.language Inglés es_ES
dc.publisher Association for Computing Machinery es_ES
dc.relation.ispartof ACM Computing Surveys es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Programming languages es_ES
dc.subject Term rewriting es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Context-sensitive Rewriting es_ES
dc.type Artículo es_ES
dc.identifier.doi 10.1145/3397677 es_ES
dc.relation.projectID info:eu-repo/grantAgreement/GVA//PROMETEO%2F2019%2F098/ES/DeepTrust: Deep Logic Technology for Software Trustworthiness/ 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.rights.accessRights Cerrado 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. (2020). Context-sensitive Rewriting. ACM Computing Surveys. 53(4):1-36. https://doi.org/10.1145/3397677 es_ES
dc.description.accrualMethod S es_ES
dc.relation.publisherversion https://doi.org/10.1145/3397677 es_ES
dc.description.upvformatpinicio 1 es_ES
dc.description.upvformatpfin 36 es_ES
dc.type.version info:eu-repo/semantics/publishedVersion es_ES
dc.description.volume 53 es_ES
dc.description.issue 4 es_ES
dc.relation.pasarela S\423953 es_ES
dc.contributor.funder Generalitat Valenciana es_ES
dc.contributor.funder Agencia Estatal de Investigación es_ES
dc.description.references Alarcón, B., Gutiérrez, R., & Lucas, S. (2010). Context-sensitive dependency pairs. Information and Computation, 208(8), 922-968. doi:10.1016/j.ic.2010.03.003 es_ES
dc.description.references Alpuente, M., Escobar, S., & Lucas, S. (2004). Correct and Complete (Positive) Strategy Annotations for OBJ. Electronic Notes in Theoretical Computer Science, 71, 70-89. doi:10.1016/s1571-0661(05)82529-0 es_ES
dc.description.references Andrianarivelo, N., & Réty, P. (2015). Over-Approximating Terms Reachable by Context-Sensitive Rewriting. Reachability Problems, 128-139. doi:10.1007/978-3-319-24537-9_12 es_ES
dc.description.references Borralleras, C., Ferreira, M., & Rubio, A. (2000). Complete Monotonic Semantic Path Orderings. Lecture Notes in Computer Science, 346-364. doi:10.1007/10721959_27 es_ES
dc.description.references Borralleras, C., Lucas, S., & Rubio, A. (2002). Recursive Path Orderings Can Be Context-Sensitive. Lecture Notes in Computer Science, 314-331. doi:10.1007/3-540-45620-1_27 es_ES
dc.description.references Gérard Boudol. 1985. Computational semantics of term rewriting systems. Algebr. Methods Semant. (1985) 169--236. Gérard Boudol. 1985. Computational semantics of term rewriting systems. Algebr. Methods Semant. (1985) 169--236. es_ES
dc.description.references Bruni, R., & Meseguer, J. (2006). Semantic foundations for generalized rewrite theories. Theoretical Computer Science, 360(1-3), 386-414. doi:10.1016/j.tcs.2006.04.012 es_ES
dc.description.references Clavel, M., Durán, F., Eker, S., Lincoln, P., Martı́-Oliet, N., Meseguer, J., & Quesada, J. F. (2002). Maude: specification and programming in rewriting logic. Theoretical Computer Science, 285(2), 187-243. doi:10.1016/s0304-3975(01)00359-0 es_ES
dc.description.references Clavel, M., Eker, S., Lincoln, P., & Meseguer, J. (1996). Principles of Maude. Electronic Notes in Theoretical Computer Science, 4, 65-89. doi:10.1016/s1571-0661(04)00034-9 es_ES
dc.description.references Courcelle, B. (1983). Fundamental properties of infinite trees. Theoretical Computer Science, 25(2), 95-169. doi:10.1016/0304-3975(83)90059-2 es_ES
dc.description.references Dershowitz, N. (1979). A note on simplification orderings. Information Processing Letters, 9(5), 212-215. doi:10.1016/0020-0190(79)90071-1 es_ES
dc.description.references Dershowitz, N., Kaplan, S., & Plaisted, D. A. (1991). Rewrite, rewrite, rewrite, rewrite, rewrite, …. Theoretical Computer Science, 83(1), 71-96. doi:10.1016/0304-3975(91)90040-9 es_ES
dc.description.references Eker, S. (1998). Term Rewriting with Operator Evaluation Strategies. Electronic Notes in Theoretical Computer Science, 15, 311-330. doi:10.1016/s1571-0661(05)80019-2 es_ES
dc.description.references Jörg Endrullis . 2009. Jambox. ( 2009 ). Retrieved from http://joerg.endrullis.de/jambox.html. Jörg Endrullis. 2009. Jambox. (2009). Retrieved from http://joerg.endrullis.de/jambox.html. es_ES
dc.description.references Endrullis, J., & Hendriks, D. (2011). Lazy productivity via termination. Theoretical Computer Science, 412(28), 3203-3225. doi:10.1016/j.tcs.2011.03.024 es_ES
dc.description.references Futatsugi, K., Goguen, J. A., Jouannaud, J.-P., & Meseguer, J. (1985). Principles of OBJ2. Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL ’85. doi:10.1145/318593.318610 es_ES
dc.description.references Futatsugi, K., & Nakagawa, A. (s. f.). An overview of CAFE specification environment-an algebraic approach for creating, verifying, and maintaining formal specifications over networks. Proceedings First IEEE International Conference on Formal Engineering Methods. doi:10.1109/icfem.1997.630424 es_ES
dc.description.references Giesl, J. (2001). Journal of Automated Reasoning, 26(1), 1-49. doi:10.1023/a:1006408829523 es_ES
dc.description.references GIESL, J., & MIDDELDORP, A. (2004). Transformation techniques for context-sensitive rewrite systems. Journal of Functional Programming, 14(4), 379-427. doi:10.1017/s0956796803004945 es_ES
dc.description.references Jürgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics Held as Part of ETAPS’19 Part III Dirk Beyer Marieke Huisman Fabrice Kordon and Bernhard Steffen (Eds.) Lecture Notes in Computer Science Vol. 11429. Springer 156--166. DOI:https://doi.org/10.1007/978-3-030-17502-3_10 Jürgen Giesl Albert Rubio Christian Sternagel Johannes Waldmann and Akihisa Yamada. 2019. The termination and complexity competition. In Tools and Algorithms for the Construction and Analysis of Systems—25 Years of TACAS: TOOLympics Held as Part of ETAPS’19 Part III Dirk Beyer Marieke Huisman Fabrice Kordon and Bernhard Steffen (Eds.) Lecture Notes in Computer Science Vol. 11429. Springer 156--166. DOI:https://doi.org/10.1007/978-3-030-17502-3_10 es_ES
dc.description.references Giesl, J., Thiemann, R., Schneider-Kamp, P., & Falke, S. (2007). Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning, 37(3), 155-203. doi:10.1007/s10817-006-9057-7 es_ES
dc.description.references Goguen, J., & Malcolm, G. (Eds.). (2000). Software Engineering with OBJ. Advances in Formal Methods. doi:10.1007/978-1-4757-6541-0 es_ES
dc.description.references Gramlich, B., & Lucas, S. (2002). Simple termination of context-sensitive rewriting. Proceedings of the 2002 ACM SIGPLAN workshop on Rule-based programming - RULE ’02. doi:10.1145/570186.570189 es_ES
dc.description.references Gramlich, B., & Lucas, S. (2006). Generalizing Newman’s Lemma for Left-Linear Rewrite Systems. Term Rewriting and Applications, 66-80. doi:10.1007/11805618_6 es_ES
dc.description.references Gutiérrez, R., & Lucas, S. (2010). Proving Termination in the Context-Sensitive Dependency Pair Framework. Lecture Notes in Computer Science, 18-34. doi:10.1007/978-3-642-16310-4_3 es_ES
dc.description.references Raúl Gutiérrez and Salvador Lucas. 2015. Function calls at frozen positions in termination of context-sensitive rewriting See Martí-Oliet et al. [2015] 311--330. DOI:https://doi.org/10.1007/978-3-319-23165-5_15 Raúl Gutiérrez and Salvador Lucas. 2015. Function calls at frozen positions in termination of context-sensitive rewriting See Martí-Oliet et al. [2015] 311--330. DOI:https://doi.org/10.1007/978-3-319-23165-5_15 es_ES
dc.description.references Gutiérrez, R., & Lucas, S. (2020). Automatically Proving and Disproving Feasibility Conditions. Lecture Notes in Computer Science, 416-435. doi:10.1007/978-3-030-51054-1_27 es_ES
dc.description.references Hirokawa, N., & Moser, G. (2014). Automated Complexity Analysis Based on Context-Sensitive Rewriting. Rewriting and Typed Lambda Calculi, 257-271. doi:10.1007/978-3-319-08918-8_18 es_ES
dc.description.references Hirokawa, N., Nagele, J., & Middeldorp, A. (2018). Cops and CoCoWeb: Infrastructure for Confluence Tools. Lecture Notes in Computer Science, 346-353. doi:10.1007/978-3-319-94205-6_23 es_ES
dc.description.references Hudak, P. (1989). Conception, evolution, and application of functional programming languages. ACM Computing Surveys, 21(3), 359-411. doi:10.1145/72551.72554 es_ES
dc.description.references Hudak, P., Peyton Jones, S., Wadler, P., Boutel, B., Fairbairn, J., Fasel, J., … Peterson, J. (1992). Report on the programming language Haskell. ACM SIGPLAN Notices, 27(5), 1-164. doi:10.1145/130697.130699 es_ES
dc.description.references J. F. Th. Kamperman and H. R. Walters . 1995 . Lazy rewriting and eager machinery. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA’95) Jieh Hsiang (Ed.) Lecture Notes in Computer Science Vol. 914 . Springer 147--162. DOI:https://doi.org/10.1007/3-540-59200-8_54 J. F. Th. Kamperman and H. R. Walters. 1995. Lazy rewriting and eager machinery. In Proceedings of the 6th International Conference on Rewriting Techniques and Applications (RTA’95) Jieh Hsiang (Ed.) Lecture Notes in Computer Science Vol. 914. Springer 147--162. DOI:https://doi.org/10.1007/3-540-59200-8_54 es_ES
dc.description.references Kennaway, R., Klop, J. W., Sleep, R., & Devries, F. J. (1995). Transfinite Reductions in Orthogonal Term Rewriting Systems. Information and Computation, 119(1), 18-38. doi:10.1006/inco.1995.1075 es_ES
dc.description.references Kojima, Y., & Sakai, M. (s. f.). Innermost Reachability and Context Sensitive Reachability Properties Are Decidable for Linear Right-Shallow Term Rewriting Systems. Lecture Notes in Computer Science, 187-201. doi:10.1007/978-3-540-70590-1_13 es_ES
dc.description.references Kojima, Y., Sakai, M., Nishida, N., Kusakari, K., & Sakabe, T. (2011). Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems. IPSJ Online Transactions, 4, 193-216. doi:10.2197/ipsjtrans.4.193 es_ES
dc.description.references Lucas, S. (2001). Transfinite Rewriting Semantics for Term Rewriting Systems. Lecture Notes in Computer Science, 216-230. doi:10.1007/3-540-45127-7_17 es_ES
dc.description.references Lucas, S. (2002). Context-Sensitive Rewriting Strategies. Information and Computation, 178(1), 294-343. doi:10.1016/s0890-5401(02)93176-7 es_ES
dc.description.references Lucas, S. (2002). Termination of (Canonical) Context-Sensitive Rewriting. Lecture Notes in Computer Science, 296-310. doi:10.1007/3-540-45610-4_21 es_ES
dc.description.references Lucas, S. (2006). Proving termination of context-sensitive rewriting by transformation. Information and Computation, 204(12), 1782-1846. doi:10.1016/j.ic.2006.07.001 es_ES
dc.description.references Salvador Lucas. 2020. Applications of context-sensitive rewriting. (submitted). Salvador Lucas. 2020. Applications of context-sensitive rewriting. (submitted). es_ES
dc.description.references Maranget, L. (1991). Optimal derivations in weak lambda-calculi and in orthogonal term rewriting systems. Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’91. doi:10.1145/99583.99618 es_ES
dc.description.references McCarthy, J. (1960). Recursive functions of symbolic expressions and their computation by machine, Part I. Communications of the ACM, 3(4), 184-195. doi:10.1145/367177.367199 es_ES
dc.description.references Meseguer, J. (2012). Twenty years of rewriting logic. The Journal of Logic and Algebraic Programming, 81(7-8), 721-781. doi:10.1016/j.jlap.2012.06.003 es_ES
dc.description.references Middeldorp, A. (1997). Call by need computations to root-stable form. Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ’97. doi:10.1145/263699.263711 es_ES
dc.description.references Nagele, J., Felgenhauer, B., & Middeldorp, A. (2017). CSI: New Evidence – A Progress Report. Lecture Notes in Computer Science, 385-397. doi:10.1007/978-3-319-63046-5_24 es_ES
dc.description.references Nagele, J., Thiemann, R., & Winkler, S. (2014). Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations. Lecture Notes in Computer Science, 216-232. doi:10.1007/978-3-319-12154-3_14 es_ES
dc.description.references Dag Prawitz. 1965. Natural Deduction. A Proof Theoretical Study. Almqvist 8 Wiksell. Dag Prawitz. 1965. Natural Deduction. A Proof Theoretical Study. Almqvist 8 Wiksell. es_ES
dc.description.references Raffelsieper, M., & Zantema, H. (2009). A Transformational Approach to Prove Outermost Termination Automatically. Electronic Notes in Theoretical Computer Science, 237, 3-21. doi:10.1016/j.entcs.2009.03.032 es_ES
dc.description.references Rapp, F., & Middeldorp, A. (2018). FORT 2.0. Lecture Notes in Computer Science, 81-88. doi:10.1007/978-3-319-94205-6_6 es_ES
dc.description.references Schernhammer, F., & Gramlich, B. (2009). VMTL–A Modular Termination Laboratory. Lecture Notes in Computer Science, 285-294. doi:10.1007/978-3-642-02348-4_20 es_ES
dc.description.references Thiemann, R., & Sternagel, C. (2009). Certification of Termination Proofs Using CeTA. Theorem Proving in Higher Order Logics, 452-468. doi:10.1007/978-3-642-03359-9_31 es_ES
dc.description.references Thiemann, R., & Sternagel, C. (2009). Loops under Strategies. Lecture Notes in Computer Science, 17-31. doi:10.1007/978-3-642-02348-4_2 es_ES
dc.description.references Uchiyama, K., Sakai, M., & Sakabe, T. (2008). Decidability of Innermost Termination and Context-Sensitive Termination for Semi-Constructor Term Rewriting Systems. Electronic Notes in Theoretical Computer Science, 204, 21-34. doi:10.1016/j.entcs.2008.03.051 es_ES
dc.description.references Zantema, H. (1997). Termination of context-sensitive rewriting. Lecture Notes in Computer Science, 172-186. doi: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