article

A general framework for lazy functional logic programming with algebraic polymorphic types

Authors:

Puri Arenas-Sánchez,

Mario Rodríguez-ArtalejoAuthors Info & Claims

Theory and Practice of Logic Programming, Volume 1, Issue 2

Pages 185 - 245

Published: 01 March 2001 Publication History

Abstract

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 set ℛ of 𝒞-based conditional rewriting rules for defined functions. We argue that equational logic does not supply the proper semantics for such programs. Therefore, we present an alternative logic which includes 𝒞-based rewriting calculi and a notion of model. We get soundness and completeness for 𝒞-based rewriting w.r.t. models, existence of free models for all programs, and type preservation results. As operational semantics, we develop a sound and complete procedure for goal solving, which is based on the combination of lazy narrowing with unification modulo 𝒞. Our framework is quite expressive for many purposes, such as solving action and change problems, or realizing the GAMMA computation model.

References

[1]

Almendros-Jiménez, J. M. and Gil-Luezas, A. (1997) Lazy narrowing with parametric ordersorted types. Proc. Algebraic and Logic Programming (ALP'97). LNCS, vol. 1298, pp. 159- 173. Springer-Verlag.

[2]

Almendros-Jiménez, J. M., Gavilanes-Franco, A. and Gil-Luezas, A. (1996) Algebraic semantics for functional logic programming with polymorphic order-sorted types. Proc. Algebraic and Logic Programming (ALP'96). LNCS, vol. 1139, pp. 299-313. Springer-Verlag.

[3]

Antoy, S., Echahed, R. and Hanus, M. (1994) A needed narrowing strategy. Proc. of the ACM Symposium on Principles of Programming Languages (POPL'94), pp. 268-279. ACM Press.

[4]

Apt, K. R. (1990) Introduction to logic programming. In: van Leeuwen, J. (ed), Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp. 495-574. Elsevier & MIT Press.

[5]

Arenas-Sánchez, P. (1998) Programación declarativa con restricciones sobre tipos de datos algebraicos. PhD thesis, Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid.

[6]

Arenas-Sánchez, P. and Dovier, A. (1995) Minimal set unification. Proc. Programming Languages Implementation and Logic Programming (PLILP'95). LNCS, vol. 982, pp. 397- 414. Springer-Verlag.

[7]

Arenas-Sánchez, P. and Dovier, A. (1997) A minimality study for set unification. J. Logic and Functional Programming, 1997(7).

[8]

Arenas-Sánchez, P. and Rodríguez-Artalejo, M. (1997a) A lazy narrowing calculus for functional logic programming with algebraic polymorphic types. Proc. of the International Logic Programming Symposium (ILPS'97), pp. 53-68. MIT Press.

[9]

Arenas-Sánchez, P. and Rodríguez-Artalejo, M. (1997b) A semantic framework for functional logic programming with algebraic polymorphic types. Proc. Theory and Practice of Software Development (TAPSOFT'97). LNCS, vol. 1214, pp. 453-464. Springer-Verlag.

[10]

Arenas-Sánchez, P., López-Fraguas, F. J. and Rodríguez-Artalejo, M. (1998) Embedding multiset constraints into a lazy functional logic language. Proc. Programming Languages Implementation and Logic Programming (PLILP'98). LNCS, vol. 1490, pp. 429-444. Springer-Verlag.

[11]

Banâtre, J. P. and Métayer, D. Le. (1990) The gamma model and its discipline of programming. Science of Computer Programming, 15, 55-77.

Digital Library

[12]

Banâtre, J. P. and Métayer, D. Le. (1993) Programming by multiset transformation. Comm. ACM, 36:1, 98-111.

Digital Library

[13]

Bird, R. (1998) Introduction to functional programming using Haskell. Second edn. Computer Science. Prentice Hall.

[14]

Borovansky, P., Kirchner, C., Kirchner, H., Moreau, P. and Vittek, M. (1996) Elan: A logical framework based on computational systems. Rewriting Logic and its Applications, First International Workshop. Electronic Notes in Theoretical Computer Science, vol. 15, pp. 35-50. Elsevier.

[15]

Clavel, M., Eker, S., Lincoln, P. and Meseguer, J. (1996) Principles of Maude. Rewriting Logic and its Applications, First International Workshop. Electronic Notes in Theoretical Computer Science, vol. 4, pp. 95-116. Elsevier Science.

[16]

Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J. and Quesada, J. (1999) Maude: Specification and programming in rewriting logic. Technical report, Computer Science Laboratory, SRI International.

[17]

Damas, L. and Milner, R. (1982) Principal type-schemes for functional programs. Proc. of the ACM Symposium on Principles of Programming Languages (POPL'82), pp. 207-212. ACM Press.

Digital Library

[18]

Dershowitz, N. and Jouannaud, J.P. (1990) Rewrite systems. In: van Leeuwen, J. (ed), Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp. 243- 320. Elsevier & MIT Press.

[19]

Dershowitz, N. and Manna, Z. (1979) Proving termination with multiset ordering. Comm. ACM, 22(8), 465-476.

Digital Library

[20]

Dershowitz, N. and Okada, M. (1990) A rationale for conditional equational programming. Theoret. Comput. Sci., 75, 111-138.

Digital Library

[21]

Diaconescu, R., Futatsugi, K., Ishisone, M., Nagakawa, A. T. and Sawada, T. (1998) An overview of CafeOBJ. Rewriting Logic and its Applications, First International Workshop. Electronic Notes in Theoretical Computer Science, vol. 15, pp. 75-88. Elsevier Science.

[22]

Dovier, A. and Rossi, G. (1993) Embedding extensional finite sets in CLP. Proc. of the International Conference on Logic Programming (ICLP'93), pp. 540-556. MIT Press.

[23]

Dovier, A., Omodeo, E., Pontelli, E. and Rossi, G. (1991) {log}: A logic programming language with finite sets. Proc. of the International Conference on Logic Programming (ICLP'91), pp. 111-124. MIT Press.

[24]

Dovier, A., Policriti, A. and Rossi, G. (1996a) Integrating lists, multisets, and sets in a logic programming framework. Proc. International Workshop on Frontiers of Combining Systems (FROCOS'96), pp. 303-319. Kluwer.

[25]

Dovier, A., Omodeo, E., Pontelli, E. and Rossi, G. (1996b) {log}: A language for programming in logic with finite sets. J, Logic Programming, 28(1), 1-44.

[26]

Falaschi, M., Levi, G., Martelli, M. and Palamidessi, C. (1993) A model-theoretic reconstruction of the operational semantics of logic programs. Infor. & Computation, 102(1), 86-113.

Digital Library

[27]

Fay, M. J. (1979) First-order unification in an equational theory. Proc. of the 4th Workshop on Automated Deduction, pp. 161-167. Academic Press.

[28]

Giovannetti, E., Levi, G., Moiso, C. and Palamidessi, C. (1991) Kernel K-LEAF: A logic plus functional language. J. Comput. Syst. Sci., 42(2), 139-185.

Digital Library

[29]

Goguen, J. A. and Meseguer, J. (1987) Models and equality for logical programming. Proc. Theory and Practice of Software Development (TAPSOFT'87). LNCS, vol. 250 (II), pp. 1-22. Springer-Verlag.

[30]

González-Moreno, J. C., Hortalá -González, M. T., López-Fraguas, F. J. and Rodríguez-Artalejo, M. (1996) A rewriting logic for declarative programming. Proc. of the European Symposium on Programming (ESOP'96). LNCS, vol. 1058, pp. 156-172. Springer-Verlag.

[31]

González-Moreno, J. C., Hortalá-González, M. T., López-Fraguas, F. J. and Rodríguez-Artalejo, M. (1999) An approach to declarative programming based on a rewriting logic. J. Logic Programming, 40(1), 47-87.

[32]

González-Moreno, J. C., Hortalá-González, M. T. and Rodríguez-Artalejo, M. (1993) On the completeness of narrowing as the operational semantics of functional logic programming. Proc. Computer Science Logic (CSL'92). LNCS, vol. 702, pp. 216-230. Springer-Verlag.

[33]

González-Moreno, J. C., Hortalá-González, M. T. and Rodríquez-Artalejo, M. (1997) A higher order rewriting logic for functional logic programming. Proc. of the International Conference on Logic Programming (ICLP'97), pp. 53-167. MIT Press.

[34]

Große, G., Hölldobler, S., Schneeberger, J., Sigmund, U. and Thielscher, M. (1992) Equational logic programming, actions, and change. Proc. of the International Conference on Logic Programming (ICLP'92), pp. 177-191. The MIT Press.

[35]

Gunter, C. A. and Scott, D. S. (1990) Semantic domains. In: van Leeuwen, J. (ed), Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp. 633-674. Elsevier & MIT Press.

[36]

Hanus, M. (1990) A functional and logic language with polymorphic types (extended abstract). Proc. International Symposium on Design and Implementation of Symbolic Computation Systems. LNCS, vol. 429, pp. 215-224. Springer-Verlag.

[37]

Hanus, M. (1994) The integration of functions into logic programming. A survey. J. Logic Programming Special Issue "Ten Years of Logic Programming", (19 & 20), 583-628.

[38]

Hanus, M. (1997) Lazy narrowing with simplification. J. Comput. Languages, 23(2-4), 61-85.

Digital Library

[39]

Hölldobler, S. (1989) Foundations of equational logic programming. LNCS, vol. 353. Springer-Verlag.

[40]

Hölldobler, S. and Schneeberger, J. (1990) A new deductive approach to planning. New Generation Computing, 8, 225-244.

Digital Library

[41]

Huet, G. and Lévy, J. J. (1979) Call by need computations in nonambiguous linear term rewriting systems. Technical report 359, INRIA.

[42]

Huet, G. and Lévy, J.J. (1991) Computations in orthogonal term rewriting systems I, II. In: Lassez, J. L. and Plotkin, G. (eds), Computational Logic: Essays in Honour of J. Alan Robinson, pp. 395-414, 415-443. MIT Press.

[43]

Hullot, J. M. (1980) Canonical forms and unification. Proc. of the Conference on Automated Deduction (CADE'80). LNCS, vol. 204, pp. 318-334. Springer.

[44]

Hussmann, H. (1992) Non-deterministic algebraic specifications and nonconfluent term rewriting. J. Logic Programming, 12, 237-255.

Digital Library

[45]

Hussmann, H. (1993) Non-determinism in algebraic specifications and algebraic programs. Birkhäuser.

[46]

Jaffar, J., Lassez, J. L. and Maher, M. J. (1984) A theory of complete logic programs with equality. J. Logic Programming, 1, 211-223.

[47]

Jayaraman, B. (1992) Implementation of subset-equational programs. J. Logic Programming, 12, 299-324.

Digital Library

[48]

Jayaraman, B. and Plaisted, D. A. (1989) Programming with equations, subsets, and relations. Proc. of the International Conference on Logic Programming (ICLP'89), vol. 2, pp. 1051- 1068. MIT Press.

[49]

Jouannaud, J. P. and Kirchner, C. (1991) Equations in abstract algebras: A rule-based survey of unification. In: Lassez, J. L. and Plotkin, G. (eds), Computational Logic: Essays in Honour of J. Alan Robinson, pp. 257-321. MIT Press.

[50]

Kirchner, C., Kirchner, H. and Vittek, M. (1995) Designing constraint logic programming languages using computational systems. Proc. Principles and Practice of Constraint Programming (PPCP'95), pp. 133-160. MIT Press.

[51]

Legèard, B. (1994) Programmation en logique avec contraintes sur les ensembles, multiensembles et séquences. Utilisation en prototypage de logiciels. PhD thesis, Université de Franche-Comté.

[52]

Lloyd, J. W. (1999) Programming in an integrated functional and logic language. J. Logic and Functional Programming, 1999(3).

[53]

Loogen, R., López-Fraguas, F. J. and Rodríguez-Artalejo, M. (1993) A demand driven computation strategy for lazy narrowing. Proc. Programming Languages Implementation and Logic Programming (PLILP'93). LNCS, vol. 714, pp. 184-200. Springer.

[54]

Martí-Oliet, N. and Meseguer, J. (1995) Action and change in rewriting logic. In: Pareschi, R. and Fronhöfer, B. (eds), Theoretical Approaches to Dynamic Worlds in Computer Science and Artificial Intelligence. Cambridge M.P.

[55]

Meseguer, J. (1992) Multiparadigm logic programming (invited talk). Proc. Algebraic and Logic Programming (ALP'92). LNCS, vol. 632, pp. 158-200. Springer-Verlag.

[56]

Meseguer, J. (1993) A logical theory of concurrent objects and its realization in the Maude language. In: Agha, G., Wegner, P. and Yonezawa, A. (eds), Research Directions in Object-Based Concurrency, pp. 314-390. The MIT Press.

[57]

Middeldorp, A. and Hamoen, E. (1994) Completeness results for basic narrowing. Applicable Algebra in Engineering, Communication and Computation, 5, 213-253.

[58]

Middeldorp, A., Okui, S. and Ida, T. (1996) Lazy narrowing: Strong completeness and eager variable elimination. Theor. Comput. Sci., 167, 95-130.

Digital Library

[59]

Milner, R. (1978) A theory of type polymorphism in programming. J. Computer and Systems Sciences, 17, 348-375.

[60]

Molina, J. M. and Pimentel, E. (1997) Modularity in functional-logic programming. Proc. of the International Conference on Logic Programming (ICLP'97), pp. 183-197. MIT Press.

[61]

Möller, B. (1985) On the algebraic specification of infinite objects-ordered and continuous models of algebraic types. Acta Informatica, 22, 537-578.

Digital Library

[62]

Moreno-Navarro, J. J. and Rodríguez-Artalejo, M. (1992) Logic programming with functions and predicates: The language BABEL. J. Logic Programming, 12, 191-223.

Digital Library

[63]

Peterson, J. and Hammond, K. (1997) Report on the programming language Haskell. A nonstrict, purely functional language vs. 1.4. Technical report, Swedish Institute of Computer Science.

[64]

Pierce, B. J. (1991) Basic category theory for computer scientists. Foundations of Computer Science Series. MIT Press.

[65]

Reddy, U. (1985) Narrowing as the operational semantics of functional languages. Proc. Symposium on Logic Programming, pp. 138-151. IEEE Press.

[66]

Scott, D. S. (1982) Domains for denotational semantics. Proc. of the International Colloquium on Automata, Languages, and Programming (ICALP'82). LNCS, vol. 140, pp. 567-613. Springer-Verlag.

[67]

Smolka, G. (1989) Logic programming over polymorphically order-sorted types. PhD thesis, Fachbereich Informatik, Universität Kaiserslautern.

[68]

Socher-Ambrosius, R. (1994) A refined version of general E-unification. Proc. of the Conference on Automated Deduction (CADE-12). LNAI, pp. 665-677. Springer-Verlag.

[69]

Winskel, G. (1985) On powerdomains and modality. Theor. Comput. Sci., 36, 127-137.

[70]

You, J. H. (1989) Enumerating outer narrowing derivations for constructor-based term rewriting systems. J. Symbolic Computation, 7, 319-341.

Digital Library

Cited By

Palomino M(2007)A comparison between two logical formalisms for rewritingTheory and Practice of Logic Programming10.1017/S14710684060028457:1-2(183-213)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.1017/S1471068406002845
López Fraguas FRodríguez Artalejo MVírseda R(2007)A new generic scheme for functional logic programming with constraintsHigher-Order and Symbolic Computation10.1007/s10990-007-9002-420:1-2(73-122)Online publication date: 1-Jun-2007
https://dl.acm.org/doi/10.1007/s10990-007-9002-4
López-Fraguas FRodríguez-Artalejo Mdel Vado Vírseda R(2005)Constraint Functional Logic Programming RevisitedElectronic Notes in Theoretical Computer Science (ENTCS)10.5555/2773803.2773989117:C(5-50)Online publication date: 20-Jan-2005
https://dl.acm.org/doi/10.5555/2773803.2773989
Show More Cited By

A general framework for lazy functional logic programming with algebraic polymorphic types
1. Theory of computation

Recommendations

A lazy narrowing calculus for functional logic programming with algebraic polymorphic types
ILPS '97: Proceedings of the 1997 international symposium on Logic programming
Specialization of lazy functional logic programs

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 ...
Lazy narrowing with simplification

Languages that integrate functional and logic programming styles with a complete operational semantics are based on narrowing. In order to avoid useless computations, lazy narrowing strategies have been proposed in the past. This paper presents an ...

Comments

Information & Contributors

Information

Published In

cover image Theory and Practice of Logic Programming

Theory and Practice of Logic Programming Volume 1, Issue 2

March 2001

118 pages

ISSN:1471-0684

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 March 2001

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 03 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Palomino M(2007)A comparison between two logical formalisms for rewritingTheory and Practice of Logic Programming10.1017/S14710684060028457:1-2(183-213)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.1017/S1471068406002845
López Fraguas FRodríguez Artalejo MVírseda R(2007)A new generic scheme for functional logic programming with constraintsHigher-Order and Symbolic Computation10.1007/s10990-007-9002-420:1-2(73-122)Online publication date: 1-Jun-2007
https://dl.acm.org/doi/10.1007/s10990-007-9002-4
López-Fraguas FRodríguez-Artalejo Mdel Vado Vírseda R(2005)Constraint Functional Logic Programming RevisitedElectronic Notes in Theoretical Computer Science (ENTCS)10.5555/2773803.2773989117:C(5-50)Online publication date: 20-Jan-2005
https://dl.acm.org/doi/10.5555/2773803.2773989
Martín Sdel Vado Vírseda RAntoy SHanus M(2005)Designing an efficient computation strategy in CFLP(FD) using definitional treesProceedings of the 2005 ACM SIGPLAN workshop on Curry and functional logic programming10.1145/1085099.1085105(23-31)Online publication date: 29-Sep-2005
https://dl.acm.org/doi/10.1145/1085099.1085105
López-Fraguas FRodríguez-Artalejo Mdel Vado Vírseda RMoggi EWarren D(2004)A lazy narrowing calculus for declarative constraint programmingProceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming10.1145/1013963.1013972(43-54)Online publication date: 24-Aug-2004
https://dl.acm.org/doi/10.1145/1013963.1013972
López-Fraguas FSánchez-Hernández J(2004)A proof theoretic approach to failure in functional logic programmingTheory and Practice of Logic Programming10.1017/S14710684030017284:2(41-74)Online publication date: 1-Jan-2004
https://dl.acm.org/doi/10.1017/S1471068403001728
Palú ADovier APontelli ERossi GSagonas KMiller D(2003)Integrating finite domain constraints and CLP with setsProceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming10.1145/888251.888272(219-229)Online publication date: 27-Aug-2003
https://dl.acm.org/doi/10.1145/888251.888272

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents