A Finite Representation of the Narrowing Space

Vista sencilla de ítem
dc.contributor.authorNishida, Naokies_ES
dc.contributor.authorVidal, Germánes_ES
dc.date.accessioned2016-10-27T07:43:55Z
dc.date.available2016-10-27T07:43:55Z
dc.date.issued2013-09-18
dc.descriptionThe final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-14125-1_4es_ES
dc.description.abstractNarrowing basically extends rewriting by allowing free variables in terms and by replacing matching with unification. As a consequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still represents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (possibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.es_ES
dc.description.accrualMethodSes_ES
dc.description.bibliographicCitationNishida, N.; Vidal, G. (2013). A Finite Representation of the Narrowing Space. En Logic-Based Program Synthesis and Transformation. Springer. 54-71. doi:10.1007/978-3-319-14125-1_4es_ES
dc.description.referencesAlbert, E., Vidal, G.: The Narrowing-Driven Approach to Functional Logic Program Specialization. New Generation Computing 20(1), 3–26 (2002)es_ES
dc.description.referencesAlpuente, M., Falaschi, M., Vidal, G.: Partial Evaluation of Functional Logic Programs. ACM Transactions on Programming Languages and Systems 20(4), 768–844 (1998)es_ES
dc.description.referencesAlpuente, M., Falaschi, M., Vidal, G.: Compositional Analysis for Equational Horn Programs. In: Rodríguez-Artalejo, M., Levi, G. (eds.) ALP 1994. LNCS, vol. 850, pp. 77–94. Springer, Heidelberg (1994)es_ES
dc.description.referencesAntoy, 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)es_ES
dc.description.referencesArts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science 236(1–2), 133–178 (2000)es_ES
dc.description.referencesArts, T., Zantema, H.: Termination of Logic Programs Using Semantic Unification. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol. 1048, pp. 219–233. Springer, Heidelberg (1996)es_ES
dc.description.referencesBaader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)es_ES
dc.description.referencesBae, K., Escobar, S., Meseguer, J.: Abstract Logical Model Checking of Infinite-State Systems Using Narrowing. In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2013)es_ES
dc.description.referencesDe Schreye, D., Glück, R., Jørgensen, J., Leuschel, M., Martens, B., Sørensen, M.: Conjunctive partial deduction: foundations, control, algorihtms, and experiments. Journal of Logic Programming 41(2&3), 231–277 (1999)es_ES
dc.description.referencesEscobar, 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)es_ES
dc.description.referencesEscobar, 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)es_ES
dc.description.referencesFribourg, L.: SLOG: A Logic Programming Language Interpreter Based on Clausal Superposition and Rewriting. In: Proceedings of the Symposium on Logic Programming, pp. 172–185. IEEE Press (1985)es_ES
dc.description.referencesGnaedig, I., Kirchner, H.: Proving weak properties of rewriting. Theoretical Computer Science 412(34), 4405–4438 (2011)es_ES
dc.description.referencesHanus, M.: The integration of functions into logic programming: From theory to practice. Journal of Logic Programming 19&20, 583–628 (1994)es_ES
dc.description.referencesHanus, M. (ed.): Curry: An integrated functional logic language (vers. 0.8.3) (2012). http://www.curry-language.orges_ES
dc.description.referencesHermenegildo, M., Rossi, F.: On the Correctness and Efficiency of Independent And-Parallelism in Logic Programs. In: Lusk, E., Overbeck, R. (eds.) Proceedings of the 1989 North American Conf. on Logic Programming, pp. 369–389. The MIT Press, Cambridge (1989)es_ES
dc.description.referencesHölldobler, S. (ed.): Foundations of Equational Logic Programming. LNCS, vol. 353. Springer, Heidelberg (1989)es_ES
dc.description.referencesMeseguer, 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)es_ES
dc.description.referencesMiddeldorp, A., Okui, S.: A Deterministic Lazy Narrowing Calculus. Journal of Symbolic Computation 25(6), 733–757 (1998)es_ES
dc.description.referencesNishida, N., Sakai, M., Sakabe, T.: Generation of Inverse Computation Programs of Constructor Term Rewriting Systems. IEICE Transactions on Information and Systems J88–D–I(8), 1171–1183 (2005) (in Japanese)es_ES
dc.description.referencesNishida, N., Sakai, M., Sakabe, T.: Partial Inversion of Constructor Term Rewriting Systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 264–278. Springer, Heidelberg (2005)es_ES
dc.description.referencesNishida, N., Vidal, G.: Program inversion for tail recursive functions. In: Schmidt-Schauß, M. (ed.) Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. LIPIcs, vol. 10, pp. 283–298. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2011)es_ES
dc.description.referencesNishida, N., Vidal, G.: Computing More Specific Versions of Conditional Rewriting Systems. In: Albert, E. (ed.) LOPSTR 2012. LNCS, vol. 7844, pp. 137–154. Springer, Heidelberg (2013)es_ES
dc.description.referencesNutt, W., Réty, P., Smolka, G.: Basic Narrowing Revisited. Journal of Symbolic Computation 7(3/4), 295–317 (1989)es_ES
dc.description.referencesOhlebusch, E.: Advanced Topics in Term Rewriting. Springer, London, UK (2002)es_ES
dc.description.referencesPalamidessi, C.: Algebraic Properties of Idempotent Substitutions. In: Paterson, M. (ed.) ICALP 1990. LNCS, vol. 443, pp. 386–399. Springer, Heidelberg (1990)es_ES
dc.description.referencesRamos, J.G., Silva, J., Vidal, G.: Fast Narrowing-Driven Partial Evaluation for Inductively Sequential Systems. In: Danvy, O., Pierce, B.C. (eds.) Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, pp. 228–239. ACM Press (2005)es_ES
dc.description.referencesSlagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity and associativity. Journal of the ACM 21(4), 622–642 (1974)es_ES
dc.description.upvformatpfin71es_ES
dc.description.upvformatpinicio54es_ES
dc.format.extent17es_ES
dc.identifier.doi10.1007/978-3-319-14125-1_4
dc.identifier.isbn978-3-319-14124-4
dc.identifier.issn0302-9743
dc.identifier.urihttps://riunet.upv.es/handle/10251/72829
dc.languageIngléses_ES
dc.publisherSpringeres_ES
dc.relation.conferencedateSeptember 18-19, 2013es_ES
dc.relation.conferencename23rd International Symposium on Logic Based Program Synthesis and Transformation (LOPSTR 2013)es_ES
dc.relation.conferenceplaceMadrid, Spaines_ES
dc.relation.ispartofLogic-Based Program Synthesis and Transformationes_ES
dc.relation.ispartofseriesLecture Notes in Computer Science;8901
dc.relation.publisherversionhttp://link.springer.com/chapter/10.1007/978-3-319-14125-1_4es_ES
dc.relation.references10.1007/BF03037257es_ES
dc.relation.references10.1145/291891.291896es_ES
dc.relation.references10.1007/3-540-58431-5_8es_ES
dc.relation.references10.1007/BFb0033833es_ES
dc.relation.references10.1016/S0304-3975(99)00207-8es_ES
dc.relation.references10.1007/3-540-60939-3_17es_ES
dc.relation.references10.1017/CBO9781139172752es_ES
dc.relation.references10.1016/S0743-1066(99)00030-8es_ES
dc.relation.references10.1016/j.tcs.2006.08.035es_ES
dc.relation.references10.1007/978-3-540-73449-9_13es_ES
dc.relation.references10.1016/j.tcs.2011.04.028es_ES
dc.relation.references10.1016/0743-1066(94)90034-5es_ES
dc.relation.references10.1016/j.entcs.2004.06.024es_ES
dc.relation.references10.1006/jsco.1997.0197es_ES
dc.relation.references10.1007/978-3-540-32033-3_20es_ES
dc.relation.references10.1007/978-3-642-38197-3_10es_ES
dc.relation.references10.1016/S0747-7171(89)80014-8es_ES
dc.relation.references10.1007/978-1-4757-3661-8es_ES
dc.relation.references10.1007/BFb0032046es_ES
dc.relation.references10.1145/1090189.1086394es_ES
dc.relation.references10.1145/321850.321859es_ES
dc.relation.senia254715es_ES
dc.rightsReserva de todos los derechoses_ES
dc.rights.accessRightsAbiertoes_ES
dc.subject.classificationLENGUAJES Y SISTEMAS INFORMATICOSes_ES
dc.titleA Finite Representation of the Narrowing Spacees_ES
dc.typeCapítulo de libroes_ES
dc.typeComunicación en congresoes_ES
dc.type.versioninfo:eu-repo/semantics/publishedVersiones_ES
dspace.entity.typePublication
upv.uuid1002e1b0-308f-444f-8734-ade9ec632c8ees_ES

Archivos

Bloque original

Mostrando 1 - 2 de 2
Miniatura
Nombre:
paper.pdf
Tamaño:
305.25 KB
Formato:
Adobe Portable Document Format
Descripción:
Versión del Autor.
[object Object] Descargar
Miniatura
Nombre:
Nishida, Vidal_A Finite Representation of the Narrowing Space.pdf
Tamaño:
3.56 MB
Formato:
Adobe Portable Document Format
Descripción:
Versión editorial
Descargar

Colecciones

Artículos, conferencias, monografías