Applications and extensions of context-sensitive rewriting. (English) Zbl 1518.68157
Summary: Context-sensitive rewriting is a restriction of term rewriting which is obtained by imposing replacement restrictions on the arguments of function symbols. It has proven useful to analyze computational properties of programs written in sophisticated rewriting-based programming languages such as CafeOBJ, Haskell, Maude, OBJ*, etc. Also, a number of extensions (e.g., to conditional rewriting or constrained equational systems) and generalizations (e.g., controlled rewriting or forbidden patterns) of context-sensitive rewriting have been proposed. In this paper, we provide an overview of these applications and related issues.
References:
| [1] | Alarcón, B.; Emmes, F.; Fuhs, C.; Giesl, J.; Gutiérrez, R.; Lucas, S.; Schneider-Kamp, P.; Thiemann, R., Improving context-sensitive dependency pairs, (Cervesato, I.; Veith, H.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings (2008), Springer), 636-651 · Zbl 1182.68092 |
| [2] | Alarcón, B.; Gutiérrez, R.; Lucas, S., Context-sensitive dependency pairs, Inf. Comput., 208, 922-968 (2010) · Zbl 1206.68158 |
| [3] | Alarcón, B.; Lucas, S., Using context-sensitive rewriting for proving innermost termination of rewriting, Electron. Notes Theor. Comput. Sci., 248, 3-17 (2009) · Zbl 1337.68147 |
| [4] | Alarcón, B.; Lucas, S.; Meseguer, J., A dependency pair framework for a OR C-termination, (Ölveczky, P. C., Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers (2010), Springer), 35-51 · Zbl 1306.68060 |
| [5] | Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S., Improving on-demand strategy annotations, (Baaz, M.; Voronkov, A., LPAR (2002), Springer), 1-18 · Zbl 1023.03530 |
| [6] | Alpuente, M.; Escobar, S.; Gramlich, B.; Lucas, S., On-demand strategy annotations revisited: an improved on-demand evaluation strategy, Theor. Comput. Sci., 411, 504-541 (2010) · Zbl 1186.68092 |
| [7] | Andrianarivelo, N.; Pelletier, V.; Réty, P., Transforming prefix-constrained or controlled rewrite systems, (Mosbah, M.; Rusinowitch, M., SCSS 2017, the 8th International Symposium on Symbolic Computation in Software. SCSS 2017, the 8th International Symposium on Symbolic Computation in Software, Science 2017, April 6-9, 2017, Gammarth, Tunisia (2017), EasyChair), 49-62 |
| [8] | Andrianarivelo, N.; Réty, P., Confluence of prefix-constrained rewrite systems, (Kirchner, H., 3rd International Conference on Formal Structures for Computation and Deduction. 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018, July 9-12, 2018, Oxford, UK (2018), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 6:1-6:15 · Zbl 1462.68087 |
| [9] | Antoy, S., Definitional trees, (Kirchner, H.; Levi, G., Algebraic and Logic Programming, Third International Conference. Algebraic and Logic Programming, Third International Conference, Volterra, Italy, September 2-4, 1992, Proceedings (1992), Springer), 143-157 · Zbl 0856.68013 |
| [10] | Antoy, S.; Hanus, M., Functional logic programming, Commun. ACM, 53, 74-85 (2010) |
| [11] | Arts, T.; Giesl, J., Termination of term rewriting using dependency pairs, Theor. Comput. Sci., 236, 133-178 (2000) · Zbl 0938.68051 |
| [12] | Baader, F.; Nipkow, T., Term Rewriting and All That (1998), Cambridge University Press |
| [13] | Bergstra, J. A.; Klop, J. W., Conditional rewrite rules: confluence and termination, J. Comput. Syst. Sci., 32, 323-362 (1986) · Zbl 0658.68031 |
| [14] | Bonfante, G.; Cichon, A.; Marion, J.; Touzet, H., Complexity classes and rewrite systems with polynomial interpretation, (Gottlob, G.; Grandjean, E.; Seyr, K., Computer Science Logic, 12th International Workshop, CSL ’98, Annual Conference of the EACSL. Computer Science Logic, 12th International Workshop, CSL ’98, Annual Conference of the EACSL, Brno, Czech Republic, August 24-28, 1998, Proceedings (1998), Springer), 372-384 · Zbl 0934.03052 |
| [15] | Bonfante, G.; Cichon, A.; Marion, J.; Touzet, H., Algorithms with polynomial interpretation termination proof, J. Funct. Program., 11, 33-53 (2001) · Zbl 0987.68042 |
| [16] | Bruni, R.; Meseguer, J., Generalized rewrite theories, (Baeten, J. C.M.; Lenstra, J. K.; Parrow, J.; Woeginger, G. J., Automata, Languages and Programming, 30th International Colloquium. Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, the Netherlands, June 30 - July 4, 2003. Proceedings (2003), Springer), 252-266 · Zbl 1039.03020 |
| [17] | Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 386-414 (2006) · Zbl 1097.68051 |
| [18] | Cichon, A.; Lescanne, P., Polynomial interpretations and the complexity of algorithms, (Kapur, D., Automated Deduction - CADE-11, 11th International Conference on Automated Deduction. Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings (1992), Springer), 139-147 · Zbl 0925.68266 |
| [19] | 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 (2007), Springer · Zbl 1115.68046 |
| [20] | Courcelle, B., Fundamental properties of infinite trees, Theor. Comput. Sci., 25, 95-169 (1983) · Zbl 0521.68013 |
| [21] | Dershowitz, N.; Okada, M.; Sivakumar, G., Canonical conditional rewrite systems, (Lusk, E. L.; Overbeek, R. A., 9th International Conference on Automated Deduction. 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings (1988), Springer), 538-549 · Zbl 0667.68043 |
| [22] | 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. Algebraic Methods Program., 110 (2020) · Zbl 1494.68109 |
| [23] | Durán, F.; Lucas, S.; Marché, C.; Meseguer, J.; Urbain, X., Proving operational termination of membership equational programs, High.-Order Symb. Comput., 21, 59-88 (2008) · Zbl 1192.68154 |
| [24] | Durán, F.; Lucas, S.; Meseguer, J., MTT: the Maude termination tool (system description), (Armando, A.; Baumgartner, P.; Dowek, G., Automated Reasoning, 4th International Joint Conference. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings (2008), Springer), 313-319 · Zbl 1165.68360 |
| [25] | Durán, F.; Lucas, S.; Meseguer, J., Methods for proving termination of rewriting-based programming languages by transformation, Electron. Notes Theor. Comput. Sci., 248, 93-113 (2009) · Zbl 1337.68067 |
| [26] | Durán, F.; Lucas, S.; Meseguer, J.; Marché, C.; Urbain, X., Proving termination of membership equational programs, (Heintze, N.; Sestoft, P., Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 2004. Proceedings of the 2004 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation, 2004, Verona, Italy, August 24-25, 2004 (2004), ACM), 147-158 |
| [27] | Durán, F.; Meseguer, J., On the Church-Rosser and coherence properties of conditional order-sorted rewrite theories, J. Log. Algebraic Methods Program., 81, 816-850 (2012) · Zbl 1272.03139 |
| [28] | Eker, S., Term rewriting with operator evaluation strategies, (Kirchner, C.; Kirchner, H., 1998 International Workshop on Rewriting Logic and Its Applications, WRLA 1998, Abbaye des Prémontrés at Pont-à-Mousson. 1998 International Workshop on Rewriting Logic and Its Applications, WRLA 1998, Abbaye des Prémontrés at Pont-à-Mousson, France, September 1998 (1998), Elsevier), 311-330 · Zbl 0917.68113 |
| [29] | Endrullis, J.; Grabmayer, C.; Hendriks, D., Data-oblivious stream productivity, (Cervesato, I.; Veith, H.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008, Proceedings (2008), Springer), 79-96 · Zbl 1182.68117 |
| [30] | Endrullis, J.; Grabmayer, C.; Hendriks, D.; Isihara, A.; Klop, J. W., Productivity of stream definitions, (Csuhaj-Varjú, E.; Ésik, Z., Fundamentals of Computation Theory, 16th International Symposium. Fundamentals of Computation Theory, 16th International Symposium, FCT 2007, Budapest, Hungary, August 27-30, 2007, Proceedings (2007), Springer), 274-287 · Zbl 1135.68471 |
| [31] | Endrullis, J.; Grabmayer, C.; Hendriks, D.; Isihara, A.; Klop, J. W., Productivity of stream definitions, Theor. Comput. Sci., 411, 765-782 (2010) · Zbl 1183.68162 |
| [32] | Endrullis, J.; Hendriks, D., From outermost to context-sensitive rewriting, (Treinen, R., Rewriting Techniques and Applications, 20th International Conference. Rewriting Techniques and Applications, 20th International Conference, RTA 2009, Brasília, Brazil, June 29 - July 1, 2009, Proceedings (2009), Springer), 305-319 · Zbl 1242.68129 |
| [33] | Endrullis, J.; Hendriks, D., Transforming outermost into context-sensitive rewriting, Log. Methods Comput. Sci., 6 (2010) · Zbl 1191.68362 |
| [34] | Endrullis, J.; Hendriks, D., Lazy productivity via termination, Theor. Comput. Sci., 412, 3203-3225 (2011) · Zbl 1216.68136 |
| [35] | Endrullis, J.; Waldmann, J.; Zantema, H., Matrix interpretations for proving termination of term rewriting, J. Autom. Reason., 40, 195-220 (2008) · Zbl 1139.68049 |
| [36] | Falke, S., Term Rewriting with Built-in Numbers and Collection Data Structures (2009), The University of New Mexico: The University of New Mexico Albuquerque, New Mexico, Ph.D. thesis |
| [37] | Falke, S.; Kapur, D., Dependency pairs for rewriting with built-in numbers and semantic data structures, (Voronkov, A., Rewriting Techniques and Applications, 19th International Conference. Rewriting Techniques and Applications, 19th International Conference, RTA 2008, Hagenberg, Austria, July 15-17, 2008, Proceedings (2008), Springer), 94-109 · Zbl 1145.68445 |
| [38] | Falke, S.; Kapur, D., Termination of context-sensitive rewriting with built-in numbers and collection data structures, (Escobar, S., Functional and Constraint Logic Programming, 18th International Workshop. Functional and Constraint Logic Programming, 18th International Workshop, WFLP 2009, Brasilia, Brazil, June 28, 2009, Revised Selected Papers (2009), Springer), 44-61 · Zbl 1274.68149 |
| [39] | Fernández, M., Relaxing monotonicity for innermost termination, Inf. Process. Lett., 93, 117-123 (2005) · Zbl 1173.68543 |
| [40] | Ferreira, M. C.F.; Ribeiro, A. L., Context-sensitive AC-rewriting, (Narendran, P.; Rusinowitch, M., Rewriting Techniques and Applications, 10th International Conference. Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings (1999), Springer), 286-300 · Zbl 0946.68068 |
| [41] | Fissore, O.; Gnaedig, I.; Kirchner, H., Induction for termination with local strategies, Electron. Notes Theor. Comput. Sci., 58, 155-188 (2001) · Zbl 1268.68146 |
| [42] | Fissore, O.; Gnaedig, I.; Kirchner, H., Simplification and termination of strategies in rule-based languages, (Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 27-29 August 2003, Uppsala, Sweden (2003), ACM), 124-135 |
| [43] | Fokkink, W.; Kamperman, J.; Walters, P., Lazy rewriting on eager machinery, ACM Trans. Program. Lang. Syst., 22, 45-86 (2000) |
| [44] | Friedman, D. P.; Wise, D. S., CONS should not evaluate its arguments, (Michaelson, S.; Milner, R., Third International Colloquium on Automata, Languages and Programming. Third International Colloquium on Automata, Languages and Programming, University of Edinburgh, UK, July 20-23, 1976 (1976), Edinburgh University Press), 257-284 · Zbl 0461.68023 |
| [45] | Fuhs, C., Transforming derivational complexity of term rewriting to runtime complexity, (Herzig, A.; Popescu, A., Frontiers of Combining Systems - 12th International Symposium. Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings (2019), Springer), 348-364 · Zbl 1435.68132 |
| [46] | Giesl, J.; Arts, T., Verification of Erlang processes by dependency pairs, Appl. Algebra Eng. Commun. Comput., 12, 39-72 (2001) · Zbl 0973.68101 |
| [47] | 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 approve, J. Autom. Reason., 58, 3-31 (2017) · Zbl 1409.68255 |
| [48] | Giesl, J.; Middeldorp, A., Transforming context-sensitive rewrite systems, (Narendran, P.; Rusinowitch, M., Rewriting Techniques and Applications, 10th International Conference. Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Proceedings (1999), Springer), 271-287 |
| [49] | Giesl, J.; Middeldorp, A., Transformation techniques for context-sensitive rewrite systems, J. Funct. Program., 14, 379-427 (2004) · Zbl 1104.68056 |
| [50] | Giesl, J.; Thiemann, R.; Schneider-Kamp, P.; Falke, S., Mechanizing and improving dependency pairs, J. Autom. Reason., 37, 155-203 (2006) · Zbl 1113.68088 |
| [51] | Gnaedig, I.; Kirchner, H., Termination of rewriting under strategies, ACM Trans. Comput. Log., 10 (2009) · Zbl 1351.68129 |
| [52] | Goguen, J. A.; Meseguer, J., Order-sorted algebra I: equational deduction for multiple inheritance, overloading, exceptions and partial operations, Theor. Comput. Sci., 105, 217-273 (1992) · Zbl 0778.68056 |
| [53] | 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) |
| [54] | Gramlich, B., Abstract relations between restricted termination and confluence properties of rewrite systems, Fundam. Inform., 24, 2-23 (1995) · Zbl 0839.68047 |
| [55] | Gramlich, B.; Schernhammer, F., Extending context-sensitivity in term rewriting, (Fernández, M., 9th International Workshop on Reduction Strategies in Rewriting and Programming. 9th International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009 (2009)), 56-68 |
| [56] | Gramlich, B.; Schernhammer, F., Termination of rewriting with and automated synthesis of forbidden patterns, (Kirchner, H.; Muñoz, C., Strategies in Rewriting, Proving, and Programming. Strategies in Rewriting, Proving, and Programming, IWS 2010 (2010)), 35-50 |
| [57] | Gutiérrez, R.; Lucas, S., Proving termination in the context-sensitive dependency pair framework, (Ölveczky, P. C., Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010. Rewriting Logic and Its Applications - 8th International Workshop, WRLA 2010, Held as a Satellite Event of ETAPS 2010, Paphos, Cyprus, March 20-21, 2010, Revised Selected Papers (2010), Springer), 18-34 · Zbl 1306.68072 |
| [58] | Gutiérrez, R.; Lucas, S., Automatically proving and disproving feasibility conditions, (Peltier, N.; Sofronie-Stokkermans, V., Automated Reasoning - 10th International Joint Conference. Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II (2020), Springer), 416-435 · Zbl 07614688 |
| [59] | Gutiérrez, R.; Lucas, S., Mu-term: verify termination properties automatically (system description), (Peltier, N.; Sofronie-Stokkermans, V., Automated Reasoning - 10th International Joint Conference. Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II (2020), Springer), 436-447 · Zbl 07614689 |
| [60] | Hanus, M., The integration of functions into logic programming: from theory to practice, J. Log. Program., 19/20, 583-628 (1994) · Zbl 0942.68526 |
| [61] | Hanus, M., Functional logic languages: combine search and efficient evaluation (panel abstract), (Lloyd, J. W., ILPS (1995), MIT Press), 625-626 |
| [62] | Hendrix, J.; Meseguer, J., On the completeness of context-sensitive order-sorted specifications, (Baader, F., RTA (2007), Springer), 229-245 · Zbl 1203.68098 |
| [63] | Hirokawa, N.; Moser, G., Automated complexity analysis based on the dependency pair method, (Armando, A.; Baumgartner, P.; Dowek, G., Automated Reasoning, 4th International Joint Conference. Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings (2008), Springer), 364-379 · Zbl 1165.68390 |
| [64] | Hirokawa, N.; Moser, G., Automated complexity analysis based on context-sensitive rewriting, (Dowek, G., Rewriting and Typed Lambda Calculi - Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic. 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 (2014), Springer), 257-271 · Zbl 1416.68092 |
| [65] | Hirokawa, N.; Nagele, J.; Middeldorp, A., Cops and CoCoWeb: infrastructure for confluence tools, (Galmiche, D.; Schulz, S.; Sebastiani, R., Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference. 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 (2018), Springer), 346-353 |
| [66] | Hofbauer, D., Termination proofs by multiset path orderings imply primitive recursive derivation lengths, Theor. Comput. Sci., 105, 129-140 (1992) · Zbl 0759.68045 |
| [67] | Hofbauer, D.; Lautemann, C., Termination proofs and the length of derivations (preliminary version), (Dershowitz, N., Rewriting Techniques and Applications, 3rd International Conference. Rewriting Techniques and Applications, 3rd International Conference, RTA-89, Chapel Hill, North Carolina, USA, April 3-5, 1989, Proceedings (1989), Springer), 167-177 · Zbl 1503.68116 |
| [68] | Hudak, P.; Peyton Jones, S. L.; Wadler, P.; Boutel, B.; Fairbairn, J.; Fasel, J. H.; Guzmán, M. M.; Hammond, K.; Hughes, J.; Johnsson, T.; Kieburtz, R. B.; Nikhil, R. S.; Partain, W.; Peterson, J., Report on the programming language Haskell, a non-strict, purely functional language, SIGPLAN Not., 27, 1 (1992) |
| [69] | Jacquemard, F.; Kojima, Y.; Sakai, M., Controlled term rewriting, (Tinelli, C.; Sofronie-Stokkermans, V., Frontiers of Combining Systems, 8th International Symposium. Frontiers of Combining Systems, 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings (2011), Springer), 179-194 · Zbl 1348.68083 |
| [70] | Jacquemard, F.; Kojima, Y.; Sakai, M., Term rewriting with prefix context constraints and bottom-up strategies, (Felty, A. P.; Middeldorp, A., Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction. Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings (2015), Springer), 137-151 · Zbl 1465.68121 |
| [71] | Jouannaud, J.; Waldmann, B., Reductive conditional term rewriting systems, (Wirsing, M., Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts - III. Formal Description of Programming Concepts - III: Proceedings of the IFIP TC 2/WG 2.2 Working Conference on Formal Description of Programming Concepts - III, Ebberup, Denmark, 25-28 August 1986 (1987), North-Holland), 223-244 |
| [72] | Kamperman, J. F.T.; Walters, H. R., Lazy rewriting and eager machinery, (Hsiang, J., Rewriting Techniques and Applications, 6th International Conference. Rewriting Techniques and Applications, 6th International Conference, RTA-95, Kaiserslautern, Germany, April 5-7, 1995, Proceedings (1995), Springer), 147-162 · Zbl 1503.68121 |
| [73] | Kaplan, S., Simplifying conditional term rewriting systems: unification, termination and confluence, J. Symb. Comput., 4, 295-334 (1987) · Zbl 0641.68046 |
| [74] | Kapur, D.; Narendran, P.; Zhang, H., On sufficient-completeness and related properties of term rewriting systems, Acta Inform., 24, 395-415 (1987) · Zbl 0594.68035 |
| [75] | Kop, C.; Middeldorp, A.; Sternagel, T., Complexity of conditional term rewriting, Log. Methods Comput. Sci., 13 (2017) · Zbl 1398.68275 |
| [76] | Lucas, S., Context-sensitive computations in confluent programs, (Kuchen, H.; Swierstra, S. D., PLILP (1996), Springer), 408-422 |
| [77] | Lucas, S., Computational properties of term rewriting with replacement restrictions, (Falaschi, M.; Navarro, M.; Policriti, A., 1997 Joint Conf. on Declarative Programming. 1997 Joint Conf. on Declarative Programming, APPIA-GULP-PRODE’97, Grado, Italy, June 16-19, 1997 (1997)), 393-404 |
| [78] | Lucas, S., Context-sensitive computations in functional and functional logic programs, J. Funct. Logic Program. (1998) · Zbl 0924.68106 |
| [79] | Lucas, S., Termination of on-demand rewriting and termination of OBJ programs, (Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming. Proceedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 5-7, 2001, Florence, Italy (2001), ACM), 82-93 · Zbl 1282.68038 |
| [80] | Lucas, S., Termination of rewriting with strategy annotations, (Nieuwenhuis, R.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings (2001), Springer), 669-684 · Zbl 1275.68084 |
| [81] | Lucas, S., Context-sensitive rewriting strategies, Inf. Comput., 178, 294-343 (2002) · Zbl 1012.68095 |
| [82] | Lucas, S., Lazy rewriting and context-sensitive rewriting, Electron. Notes Theor. Comput. Sci., 64, 234-254 (2002) · Zbl 1268.68100 |
| [83] | Lucas, S., A note on completeness of conditional context-sensitive rewriting, (5th International Workshop on Reduction Strategies in Rewriting and Programming. 5th International Workshop on Reduction Strategies in Rewriting and Programming, WRS (2005), University of Kyoto), 3-15 |
| [84] | Lucas, S., Termination of canonical context-sensitive rewriting and productivity of rewrite systems, (Navarro, M., Proceedings XV Jornadas Sobre Programación Y Lenguajes. Proceedings XV Jornadas Sobre Programación Y Lenguajes, PROLE 2015, Santander, Spain, 15-17th September 2015 (2015)), 18-31 |
| [85] | Lucas, S., Context-sensitive rewriting, ACM Comput. Surv., 53, 78:1-78:36 (2020) |
| [86] | Lucas, S.; Marché, C.; Meseguer, J., Operational termination of conditional term rewriting systems, Inf. Process. Lett., 95, 446-453 (2005) · Zbl 1185.68374 |
| [87] | Lucas, S.; Meseguer, J., Operational termination of membership equational programs: the order-sorted way, Electron. Notes Theor. Comput. Sci., 238, 207-225 (2009) · Zbl 1347.68198 |
| [88] | Lucas, S.; Meseguer, J., Normal forms and normal theories in conditional rewriting, J. Log. Algebraic Methods Program., 85, 67-97 (2016) · Zbl 1356.68124 |
| [89] | Lucas, S.; Meseguer, J., Dependency pairs for proving termination properties of conditional term rewriting systems, J. Log. Algebraic Methods Program., 86, 236-268 (2017) · Zbl 1353.68155 |
| [90] | 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) · Zbl 1393.68088 |
| [91] | Lucas, S.; Meseguer, J.; Gutiérrez, R., The 2D dependency pair framework for conditional rewrite systems. Part II: advanced processors and implementation techniques, J. Autom. Reason., 64, 1611-1662 (2020) · Zbl 1459.68092 |
| [92] | Marchiori, M., Unravelings and ultra-properties, (Hanus, M.; Rodríguez-Artalejo, M., Algebraic and Logic Programming, 5th International Conference. Algebraic and Logic Programming, 5th International Conference, ALP’96, Aachen, Germany, September 25-27, 1996, Proceedings (1996), Springer), 107-121 · Zbl 1355.68142 |
| [93] | Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 73-155 (1992) · Zbl 0758.68043 |
| [94] | Meseguer, J., Twenty years of rewriting logic, J. Log. Algebraic Program., 81, 721-781 (2012) · Zbl 1267.03043 |
| [95] | Middeldorp, A., Call by need computations to root-stable form, (Lee, P.; Henglein, F.; Jones, N. D., Conference Record of POPL’97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Papers Presented at the Symposium. 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 (1997), ACM Press), 94-105 |
| [96] | Milner, R., The polyadic π-calculus: a tutorial, (Hamer, F. L.; Brauer, W.; Schwichtenberg, H., Logic and Algebra of Specifications (1991), Springer-Verlag) |
| [97] | Milner, R., Communicating and Mobile Systems - the Pi-Calculus (1999), Cambridge University Press · Zbl 0942.68002 |
| [98] | Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, I and II, Inf. Comput., 100, 1-77 (1992) · Zbl 0752.68037 |
| [99] | Moser, G.; Schnabl, A., The derivational complexity induced by the dependency pair method, Log. Methods Comput. Sci., 7 (2011) · Zbl 1237.68109 |
| [100] | Moser, G.; Schnabl, A.; Waldmann, J., Complexity analysis of term rewriting based on matrix and context dependent interpretations, (Hariharan, R.; Mukund, M.; Vinay, V., IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2008, December 9-11, 2008, Bangalore, India (2008), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 304-315 · Zbl 1248.68278 |
| [101] | Nagaya, T., Reduction Strategies for Term Rewriting Systems (1999), School of Information Science, Japan Advanced Institute of Science and Technology, Ph.D. thesis |
| [102] | Nakamura, M., Reduction Strategies for Term Rewriting Systems (2002), School of Information Science, Japan Advanced Institute of Science and Technology, Ph.D. thesis |
| [103] | Nakamura, M.; Ogata, K., The evaluation strategy for head normal form with and without on-demand flags, 36, 212-228 (2000) · Zbl 0962.68083 |
| [104] | Nakamura, M.; Ogata, K.; Futatsugi, K., Reducibility of operation symbols in term rewriting systems and its application to behavioral specifications, J. Symb. Comput., 45, 551-573 (2010) · Zbl 1192.68931 |
| [105] | Neurauter, F.; Zankl, H.; Middeldorp, A., Revisiting matrix interpretations for polynomial derivational complexity of term rewriting, (Fermüller, C. G.; Voronkov, A., Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference. Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings (2010), Springer), 550-564 · Zbl 1306.68083 |
| [106] | Nishida, N.; Kuroda, T.; Yanagisawa, M.; Gmeiner, K., CO3: a COnverter for proving COnfluence of COnditional TRSs, (4th International Workshop on Confluence. 4th International Workshop on Confluence, IWC 2015, August 2, 2015, Berlin, Germany (2015)), 42 |
| [107] | Nishida, N.; Mizutani, T.; Sakai, M., Transformation for refining unraveled conditional term rewriting systems, Electron. Notes Theor. Comput. Sci., 174, 75-95 (2007) · Zbl 1277.68107 |
| [108] | Nishida, N.; Sakai, M., Completion after program inversion of injective functions, Electron. Notes Theor. Comput. Sci., 237, 39-56 (2009) · Zbl 1294.68064 |
| [109] | Nishida, N.; Sakai, M.; Sakabe, T., Partial inversion of constructor term rewriting systems, (Giesl, J., Term Rewriting and Applications, 16th International Conference. Term Rewriting and Applications, 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005, Proceedings (2005), Springer), 264-278 · Zbl 1078.68662 |
| [110] | Nishida, N.; Sakai, M.; Sakabe, T., Soundness of unravelings for deterministic conditional term rewriting systems via ultra-properties related to linearity, (Schmidt-Schauß, M., Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, May 30 - June 1, 2011, Novi Sad, Serbia (2011), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 267-282 · Zbl 1236.68143 |
| [111] | Nishida, N.; Sakai, M.; Sakabe, T., Soundness of unravelings for conditional term rewriting systems via ultra-properties related to linearity, Log. Methods Comput. Sci., 8 (2012) · Zbl 1252.68161 |
| [112] | Nishida, N.; Yanagisawa, M.; Gmeiner, K., On proving confluence of conditional term rewriting systems via the computationally equivalent transformation, (3rd International Workshop on Confluence. 3rd International Workshop on Confluence, IWC 2014, July 13, 2014, Vienna, Austria (2014)), 42 |
| [113] | Ogata, K.; Futatsugi, K., Operational semantics of rewriting with the on-demand evaluation strategy, (Bryant, B. R.; Carroll, J. H.; Damiani, E.; Haddad, H.; Oppenheim, D., Applied Computing 2000, Proceedings of the 2000 ACM Symposium on Applied Computing. Applied Computing 2000, Proceedings of the 2000 ACM Symposium on Applied Computing, Villa Olmo, Via Cantoni 1, 22100 Como, Italy, March 19-21, 2000, vol. 2 (2000), ACM), 756-764 |
| [114] | Ohlebusch, E., Transforming conditional rewrite systems with extra variables into unconditional systems, (Ganzinger, H.; McAllester, D. A.; Voronkov, A., Logic Programming and Automated Reasoning, 6th International Conference. Logic Programming and Automated Reasoning, 6th International Conference, LPAR’99, Tbilisi, Georgia, September 6-10, 1999, Proceedings (1999), Springer), 111-130 · Zbl 0949.68084 |
| [115] | Ohlebusch, E., Advanced Topics in Term Rewriting (2002), Springer · Zbl 0999.68095 |
| [116] | Ölveczky, P. C.; Meseguer, J., Specification of real-time and hybrid systems in rewriting logic, Theor. Comput. Sci., 285, 359-405 (2002) · Zbl 1001.68061 |
| [117] | Ölveczky, P. C.; Meseguer, J., Real-time Maude 2.1, Electron. Notes Theor. Comput. Sci., 117, 285-314 (2004) |
| [118] | Péchoux, R., Synthesis of sup-interpretations: a survey, Theor. Comput. Sci., 467, 30-52 (2013) · Zbl 1282.68091 |
| [119] | Raffelsieper, M.; Zantema, H., A transformational approach to prove outermost termination automatically, Electron. Notes Theor. Comput. Sci., 237, 3-21 (2009) · Zbl 1294.68099 |
| [120] | Rubio, R.; Martí-Oliet, N.; Pita, I.; Verdejo, A., Parameterized strategies specification in Maude, (Fiadeiro, J. L.; Tutu, I., Recent Trends in Algebraic Development Techniques - 24th IFIP WG 1.3 International Workshop. Recent Trends in Algebraic Development Techniques - 24th IFIP WG 1.3 International Workshop, WADT 2018, Egham, UK, July 2-5, 2018, Revised Selected Papers (2018), Springer), 27-44 · Zbl 1444.68104 |
| [121] | Schernhammer, F.; Gramlich, B., Termination of lazy rewriting revisited, Electron. Notes Theor. Comput. Sci., 204, 35-51 (2008) · Zbl 1279.68120 |
| [122] | Schernhammer, F.; Gramlich, B., Characterizing and proving operational termination of deterministic conditional term rewriting systems, J. Log. Algebraic Methods Program., 79, 659-688 (2010) · Zbl 1206.68163 |
| [123] | Serbanuta, T.; Rosu, G., Computationally equivalent elimination of conditions, (Pfenning, F., Term Rewriting and Applications, 17th International Conference. Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings (2006), Springer), 19-34 · Zbl 1151.68438 |
| [124] | Sijtsma, B. A., On the productivity of recursive list definitions, ACM Trans. Program. Lang. Syst., 11, 633-649 (1989) |
| [125] | Slagle, J. R., Automated theorem-proving for theories with simplifiers commutativity, and associativity, J. ACM, 21, 622-642 (1974) · Zbl 0296.68092 |
| [126] | Thati, P.; Sen, K.; Martí-Oliet, N., An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0, Electron. Notes Theor. Comput. Sci., 71, 261-281 (2002) · Zbl 1272.68322 |
| [127] | Weiermann, A., Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths, Theor. Comput. Sci., 139, 355-362 (1995) · Zbl 0874.68156 |
| [128] | Yamada, A.; Sternagel, C.; Thiemann, R.; Kusakari, K., AC dependency pairs revisited, (Talbot, J.; Regnier, L., 25th EACSL Annual Conference on Computer Science Logic. 25th EACSL Annual Conference on Computer Science Logic, CSL 2016, August 29 - September 1, 2016, Marseille, France (2016), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 8:1-8:16 · Zbl 1369.68250 |
| [129] | Zantema, H., Termination of term rewriting by semantic labelling, Fundam. Inform., 24, 89-105 (1995) · Zbl 0839.68050 |
| [130] | Zantema, H.; Raffelsieper, M., Stream productivity by outermost termination, (Fernández, M., Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming. Proceedings Ninth International Workshop on Reduction Strategies in Rewriting and Programming, WRS 2009, Brasilia, Brazil, 28th June 2009 (2009)), 83-95 |
| [131] | Zantema, H.; Raffelsieper, M., Proving productivity in infinite data structures, (Lynch, C., Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK (2010), Schloss Dagstuhl - Leibniz-Zentrum für Informatik), 401-416 · Zbl 1236.68056 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
