Abstract
Narrowing extends rewriting with logic capabilities by allowing logic variables in terms and replacing matching with unification. Narrowing has been widely used in different contexts, ranging from theorem proving to language design. Surprisingly, the termination of narrowing has been mostly overlooked. In this paper, we present a new approach for analyzing the termination of narrowing in left-linear constructor systems|a widely accepted class of systems|that allows us to reuse existing methods in the literature on termination of rewriting.
This work has been partially supported by the EU (FEDER) and the Spanish MEC under grants TIN2005-09207-C03-02 and Acción Integrada HA2006-0008.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Albert, E., Vidal, G.: The Narrowing-Driven Approach to Functional Logic Program Specialization. New Generation Computing 20(1), 3–26 (2002)
Alpuente, M., Falaschi, M., Ramis, M.J., Vidal, G.: Narrowing Approximations as an Optimization for Equational Logic Programs. In: Penjam, J., Bruynooghe, M. (eds.) PLILP 1993. LNCS, vol. 714, pp. 391–409. Springer, Heidelberg (1993)
Antoy, S.: Optimal non-deterministic functional logic computations. In: Hanus, M., Heering, J., Meinke, K. (eds.) ALP 1997 and HOA 1997. LNCS, vol. 1298, pp. 16–30. Springer, Heidelberg (1997)
Antoy, S., Ariola, Z.: Narrowing the Narrowing Space. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292, pp. 1–15. Springer, Heidelberg (1997)
Antoy, S., Echahed, R., Hanus, M.: A Needed Narrowing Strategy. Journal of the ACM 47(4), 776–822 (2000)
Antoy, S., Hanus, M.: Overlapping Rules and Logic Variables in Functional Logic Programs. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 87–101. Springer, Heidelberg (2006)
Arroyo, G., Ramos, J.G., Silva, J., Vidal, G.: Improving Offline Narrowing-Driven Partial Evaluation using Size-Change Graphs. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 60–76. Springer, Heidelberg (2007)
Arts, T., Giesl, J.: Termination of Term Rewriting Using Dependency Pairs. Theoretical Computer Science 236(1-2), 133–178 (2000)
Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)
Chabin, J., Réty, P.: Narrowing Directed by a Graph of Terms. In: Book, R.V. (ed.) RTA 1991. LNCS, vol. 488, pp. 112–123. Springer, Heidelberg (1991)
Christian, J.: Some Termination Criteria for Narrowing and E-narrowing. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 582–588. Springer, Heidelberg (1992)
de Dios-Castro, J., López-Fraguas, F.: Extra Variables Can Be Eliminated from Functional Logic Programs. In: Proc. of the 6th Spanish Conf. on Programming and Languages (PROLE 2006), ENTCS, vol. 188, pp. 3–19. (2007)
Dershowitz, N.: Termination of Rewriting. Journal of Symbolic Computation 3(1&2), 69–115 (1987)
Dershowitz, N., Sivakumar, G.: Goal-Directed Equation Solving. In: Proc. of 7th National Conf. on Artificial Intelligence, pp. 166–170. Morgan Kaufmann, San Francisco (1988)
Hanus, M. (ed.): Curry: An Integrated Functional Logic Language, http://www.informatik.uni-kiel.de/~mh/curry/
Escobar, S., Meadows, C., Meseguer, J.: A Rewriting-Based Inference System for the NRL Protocol Analyzer and its Meta-Logical Properties. Theoretical Computer Science 367(1-2), 162–202 (2006)
Escobar, S., Meseguer, J.: Symbolic Model Checking of Infinite-State Systems Using Narrowing. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 153–168. Springer, Heidelberg (2007)
Giesl, J., Middeldorp, A.: Eliminating Dummy Elimination. In: McAllester, D. (ed.) CADE 2000. LNCS, vol. 1831, pp. 309–323. Springer, Heidelberg (2000)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Giesl, J., Thiemann, R., Schneider-Kamp, P., Falke, S.: Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning 37(3), 155–203 (2006)
Hanus, M.: The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming 19&20, 583–628 (1994)
Hölldobler, S. (ed.): Foundations of Equational Logic Programming. LNCS, vol. 353. Springer, Heidelberg (1989)
Hullot, J.M.: Canonical Forms and Unification. In: Bibel, W. (ed.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall, Englewood Cliffs (1993)
Klop, J.W.: Term Rewriting Systems: A Tutorial. Bulletin of the European Association for Theoretical Computer Science 32, 143–183 (1987)
Kusakari, K., Nakamura, M., Toyama, Y.: Argument Filtering Transformation. In: Nadathur, G. (ed.) PPDP 1999. LNCS, vol. 1702, pp. 48–62. Springer, Heidelberg (1999)
López-Fraguas, F., Sánchez-Hernández, J.: TOY: A Multiparadigm Declarative System. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol. 1631, pp. 244–247. Springer, Heidelberg (1999)
Meseguer, J., Thati, P.: Symbolic Reachability Analysis Using Narrowing and its Application to Verification of Cryptographic Protocols. Electronic Notes in Theoretical Computer Science 117, 153–182 (2005)
Moreno-Navarro, J.J., Kuchen, H., Loogen, R., Rodriguez-Artalejo, M.: Lazy Narrowing in a Graph Machine. In: Kirchner, H., Wechler, W. (eds.) ALP 1990. LNCS, vol. 463, pp. 298–317. Springer, Heidelberg (1990)
Nishida, N., Miura, K.: Dependency Graph Method for Proving Termination of Narrowing. In: Proc. of WST 2006, pp. 12–16 (2006)
Nishida, N., Sakai, M., Sakabe, T.: Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables. ENTCS, 86(3) (2003)
Ramos, J.G., Silva, J., Vidal, G.: Fast Narrowing-Driven Partial Evaluation for Inductively Sequential Systems. In: Proc. of the 10th ACM SIGPLAN Int’l Conf. on Functional Programming (ICFP 2005), pp. 228–239. ACM Press, New York (2005)
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated Termination Analysis for Logic Programs by Term Rewriting. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 177–193. Springer, Heidelberg (2007)
Sheard, T.: Type-Level Computation Using Narrowing in Ωmega. In: In Proc. of PLPV 2006. ENTCS, vol. 174, pp. 105–128 (2007)
Slagle, J.R.: Automated Theorem-Proving for Theories with Simplifiers, Commutativity and Associativity. Journal of the ACM 21(4), 622–642 (1974)
Vidal, G.: Termination of Narrowing in Left-Linear Constructor Systems. Technical report, DSIC, Technical University of Valencia (2007), http://www.dsic.upv.es/~gvidal/german/papers.html#tnt
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vidal, G. (2008). Termination of Narrowing in Left-Linear Constructor Systems. In: Garrigue, J., Hermenegildo, M.V. (eds) Functional and Logic Programming. FLOPS 2008. Lecture Notes in Computer Science, vol 4989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78969-7_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-78969-7_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78968-0
Online ISBN: 978-3-540-78969-7
eBook Packages: Computer ScienceComputer Science (R0)