M. Alpuente
M. Falaschi
G. Vidal
Skip Abstract Section
Abstract
Partial evaluation is a method for program specialization based on fold/unfold transformations [8, 25]. Partial evaluation of pure functional programs uses mainly static values of given data to specialize the program [15, 44]. In logic programming, the so-called static/dynamic distinction is hardly present, whereas considerations of determinacy and choice points are far more important for control [12]. We discuss these issues in the context of a (lazy) functional logic language. We formalize a two-phase specialization method for a non-strict, first order, integrated language which makes use of lazy narrowing to specialize the program w.r. t. a goal. The basic algorithm (first phase) is formalized as an instance of the framework for the partial evaluation of functional logic programs of [2, 3], using lazy narrowing. However, the results inherited by [2, 3] mainly regard the termination of the PE method, while the (strong) soundness and completeness results must be restated for the lazy strategy. A post-processing renaming scheme (second phase) is necessary which we describe and illustrate on the well-known matching example. This phase is essential also for other non-lazy narrowing strategies, like innermost narrowing, and our method can be easily extended to these strategies. We show that our method preserves the lazy narrowing semantics and that the inclusion of simplification steps in narrowing derivations can improve control during specialization.
- 1 M. Alpuente, M. Falaschi, P. Juli~in, and G. Vidal. Callby-Name Partial Evaluation of Functional Logic Programs. TR DSIC-II/34/96, U.P. Valencia, 1996. Google Scholar
Digital Library
- 2 M. Alpuente, M. Falaschi, and G. Vidal. Narrowingdriven Partial Evaluation of Functional Logic Programs. In H. Riis Nielson, editor, Proc. of the 6th European Syrup. on Programming, ESOP'96, pages 45-61. Springer LNCS 1058, 1996. Google ScholarDigital Library
- 3 M. Alpuente, M. Falaschi, and G. Vidal. Narrowingdriven Specialization of Functional Logic Programs. TR DSIC-II/33/96, U.P. Valencia. Extended and revised version of {2}. Available from URL htt.p://www.dsic.upv.es/users/elp/papers.html, 1996. Google ScholarDigital Library
- 4 S. Antoy, R. Echahed, and M. Hanus. A Needed Narrowing Strategy. In Proc. 21st ACM Syrup. o~ Principles of Programming Langttages, Portland, pages 268- 279, 1994. Google ScholarDigital Library
- 5 K. Benkerimi and P.M. Hill. Supporting Transformations for the Partial Evaluation of Logic Programs. Journal of Logic and Computation, 3(5):469-486, 1993.Google Scholar
- 6 J.A. Bergstra and J.W. Klop. Conditional Rewrite Rules: confluence and termination. Journal of Computer and System Sciences, 32:323-362, 1986. Google ScholarDigital Library
- 7 D. Bert and R. Echahed. Design and implementation of a generic, logic and functional programming language. In Proc. of First European Symp. on Programming, ESOP'86, pages 119-132. Springer LNCS 213, 1986. Google ScholarDigital Library
- 8 R.M. Burstall and J. Darlington. A Transformation System for Developing Recursive Programs. Journal of the ACM, 24(1):44-67, 1977. Google ScholarDigital Library
- 9 W. Chin. Towards an Automated Tupfing Strategy. In Proc. of Partial Evaluation and Semantics-Based Pro. 9ram Manipulation, Copenhagen, Denmark, June 1993, pages 119-132. ACM, New York, 1993. Google ScholarDigital Library
- 10 N. Dershowitz and J.-P. Jouannaud. Rewrite Systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics, pages 243-320. Elsevier, Amsterdam, 1990. Google ScholarDigital Library
- 11 L. Fribourg. SLOG: a logic programming language interpreter based on clausal superposition and rewriting. In Proc. of Second IEEE lnt'l Syrup. on Logic Programming, pages 172-185. IEEE, New York, 1985.Google Scholar
- 12 J. Gallagher. TutoriM on Specialisation of Logic Programs. In Proc. of Partial Evaluation and Semantics- Based Program Manipulation, Copenhagen, Denmark, June 1993, pages 88-98. ACM, New York, 1993. Google ScholarDigital Library
- 13 J. Gallagher and M. Bruynooghe. Sonde Low-Level Source Transformations for Logic Programs. In M. Bruynooghe, editor, Proc. of 2nd Workshop on Meta-Programmin9 ir~ Logic, pages 229-246. Department of Computer Science, K U Leuven, Belgium, 1990.Google Scholar
- 14 E. Giovannetti, G. Levi, C. Moiso, and C. Palamidessi. Kernel Leaf: A Logic plus Functional Language. Journal of Computer and System Sciences, 42, 1991. Google ScholarDigital Library
- 15 R. Gliick and M.H. S~rensen. Partial Deduction and Driving are Equivalent. In P~vc. lnt7 Syrup. on Programming Language Implementation and Logic Programming, PLILP'94. pages 165-181. Springer LNCS 844, 1994. Google ScholarDigital Library
- 16 M. Hanus. Compiling Logic Programs with Equality. In Proc. of 2nd lnt'l Workshop on Programming Language implementation and Logic Programming, pages 387-401. Springer LNCS 456, 1990. Google ScholarDigital Library
- 17 M. Hanus. Combining Lazy Narrowing with Simpfification. In Proc. of 6th lnt'l Syrup. on Programming Language Implementation and Logic P~vyramming, pages 370-384. Springer LNCS 844, 1994. Google ScholarDigital Library
- 18 M. Hanus. The Integration of Functions into Logic Progtamming: From Theory to Practice. Journal of Logic Programming, 19&20:583-628, 1994.Google Scholar
- 19 M. Hanus. On Extra Variables in (.Equational) Logic Programming. In Proc. o} 20th Int'l Conf. on Logic Pro- 9ramming, pages 665-678. The MIT Press, Cambridge, MA, 1995.Google Scholar
- 20 M. Hanus, H. Kuchen, and J.J. Moreno-Navarro. Curry: A Truly Functional Logic Language. In Proc. ILPS'95 Workshop on Visions }or the Future of Logic Programming, pages 95-107, 1995.Google Scholar
- 21 S. HSlldobler. Foundations of Equational Logic Pro- 9ramming. Springer LNAI 353, 1989. Google ScholarDigital Library
- 22 J.M. Hullot. Canonical Forms and Unification. In Proc of 5th Int'l Conj. on Automated Deduction, pages 318- 334. Springer LNCS 87, 1980. Google ScholarDigital Library
- 23 H. Hussman. Unification in Conditional-Equational Theories. in Proc. European Conf. on Computer Algebra EUROCAL'85, pages 543-553. Springer LNCS 204, 1985. Google ScholarDigital Library
- 24 N.D. Jones. The Essence of Program Transformation by Partial Evaluation and Driving. In N.D. Jones, M. Hagiya, and M. Sato, editors, Logic, Language and Computation, pages 206-224. Springer LNCS 792, 1994.Google Scholar
- 25 N.D. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Prentice- Hall, Englewood Cliffs, N J, 1993. Google ScholarDigital Library
- 26 J.W. Klop. Term Rewriting Systems. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science, volume I, pages 1-112. Oxford University Press, 1992. Google ScholarDigital Library
- 27 D.E. Knuth, J.H. Morris, and V.R. Pratt. Fast Pattern Matching in Strings. SlAM Journal o} Computation, 6(2):323-350, 1977.Google ScholarCross Ref
- 28 J. B. Kruskal. The Theory of Well-Quasi-Ordering: A Frequently Discovered Concept. Journal of Combinatorial Theory, A(13):297-305, 1972.Google Scholar
- 29 H. Kuchen, R. Loogen, J.J. Moreno-Navarro, and M. Rodriguez-Artalejo. Lazy Narrowing in a Graph Machine. In Proc. of the lnt'l Con}. on Algebraic and Logic Programming, volume 463 of Lecture Notes in Computer Science, pages 298-317, 1990. Google ScholarDigital Library
- 30 J.-L. Lassez, M. J. Maher, and K. Marriott. Unification Revisited. In J. Minker, editor, Foundations o} Deductive Databases and Logic Programming, pages 587-625. Morgan K~ufmann, Los Altos, Ca., 1988. Google ScholarDigital Library
- 31 M. Leuschel and B. Martens. Global Control for Partial Deduction through Characteristic Atoms and Global Trees. Technical Report CW-220, Department of Computer Science, K.U. Leuven, Belgium, December 1995.Google Scholar
- 32 M. Leuschel, D. De Schreye, and A. de Waal. A Conceptual Embedding of Folding into Partial Deduction: Towards a Maximal Integration. In M. Maher, editor, Proc. o} the Joint International Conference and Symposium on Logic Programming JICSLP'96, pages 319- 332. The MIT Press, Cambridge, MA, 1996.Google Scholar
- 33 M. Leuschel and M.H. S~rensen. Redundant Argument Filtering of Logic Programs. In Proc. of Int'l Workshop on Logic Programming Synthesis and Transformation, LOPSTR'96. To appear in Springer LNCS, 1996. Google ScholarDigital Library
- 34 J.W. Lloyd and J.C. Shepherdson. Partial Evaluation in Logic Programming. Journal of Logic Programming, 11'217-242, 1991. Google ScholarDigital Library
- 35 R. Loogen, F. L6pez-Fraguas, and M. Rodriguez- Artalejo. A Demand Driven Computation Strategy for Lazy Narrowing. In J. Penjam and M. Bruynooghe, editors, Proc. of PLILP'93, Tallinn (Estonia), pages 184-200. Springer LNCS 714, 1993. Google ScholarDigital Library
- 36 B. Martens and J. Gallagher. Ensuring Global Termination of Partial Deduction while Allowing Flexible Polyvariance. In L. Sterling, editor, Proc. of ICLP'95, pages 597-611. MIT Press, 1995.Google Scholar
- 37 A. Middeldorp and E. Hamoen. Completeness Results for Basic Narrowing. Applicable Algebra in Engineering, Communication and Computing, 5:213-253, 1994.Google ScholarCross Ref
- 38 A. Middeldorp and S. Okui. A Deterministic Lazy Narrowing Calculus. In Proc. o} the Fuji Int'l Workshop on Functional and Logic Programming, pages 104-118. World Scientific, 1995.Google Scholar
- 39 J.J. Moreno-Navarro and M. Rodriguez-Artalejo. Logic Programming with Functions and Predicates: The language Babel. Journal o,f Logic Programming, 12(3):191- 224, 1992. Google ScholarDigital Library
- 40 U.S. {teddy. Narrowing as the Operational Semantics of Functional Languages. In Proc. of Second 1EEE Int'l Syrup. on Logic Programming, pages 138-151. IEEE, New York, 1985.Google Scholar
- 41 P. R~ty. Improving basic narrowing techniques. In Proc. of the Conf. on Rewriting Techniques and Applications, pages 228-241. Springer LNCS 256, 1987. Google ScholarDigital Library
- 42 M.H. Sorensen. Turchin's Supercompiler Revisited: An Operational Theory of Positive Information Propagation. Technical Report 94/7, Master's Thesis, DIKU, University of Copenhagen, Denmark, 1994.Google Scholar
- 43 M.H. Sorensen and R. Gltick. An Algorithm of Generalization in Positive Supercompilation. In J.W. Lloyd, editor, Proc. of ILPS'95, pages 465-479. The MIT Press, Cambridge, MA, 1995.Google Scholar
- 44 M.H. S0rensen, R. Giiick, and N.D. Jones. A Positive Supercompiler. Journal of Functional Programming, 1996. To ~ppear.Google Scholar
- 45 V.F. Turchin. Program Transformation by Supercompilation. In H. Ganzinger and N.D.}ones, editors, Programs as Data Objects, 1985, pages 257-281. Springer LNCS 217, 1986. Google ScholarDigital Library
- 46 V.F. Turchin. The Algorithm of Generalization in the Supercompiler. In D. Bjorner, A.P. Ershov, and N.D. Jones, editors, Proc. of the lnt7 Workshop on Partial Evaluation and Mixed Computation, pages 531-549. North-Holland, Amsterdam, 1988.Google Scholar
- 47 P.L. Wadler. Deforestation: transforming programs to eliminate trees. In Proc of the European Syrup. on Programming, ESOP'S& pages 344-358. Springer LNCS 300, 1988. Google ScholarDigital Library
Index Terms
- Specialization of lazy functional logic programs
Recommendations
Specialization of lazy functional logic programs
PEPM '97: Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulationPartial evaluation is a method for program specialization based on fold/unfold transformations [8, 25]. Partial evaluation of pure functional programs uses mainly static values of given data to specialize the program [15, 44]. In logic programming, the ...
Partial evaluation of functional logic programs
Languages that integrate functional and logic programming with a complete operational semantics are based on narrowing, a unification-based goal-solving mechanism which subsumes the reduction principle of functional languages and the resolution ...
A general framework for lazy functional logic programming with algebraic polymorphic types
We propose a general framework for first-order functional logic programming, supporting lazy functions, non-determinism and polymorphic datatypes whose data constructors obey a set 𝒞 of equational axioms. On top of a given 𝒞, we specify a program as a ...
Comments