Functional Logic Programming in Maude

  • Santiago Escobar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8373)


Functional logic programming languages combine the most important features of functional programming languages and logic programming languages. Functional logic programming applied to the Maude specification language would replace the functional viewpoint by an equational viewpoint while retaining the logic features. This paper tries to bridge the gap between functional logic languages and the current implementation of narrowing as symbolic reachability in Maude. It illustrates how many features available in modern functional logic languages are easily definable and simulated in Maude but also shows how Maude goes beyond standard practices in the functional logic area by using, e.g. equational properties such as associativity and commutativity or order-sorted information. As a practical application we use the Missionaries and Cannibals equational logic program given by Goguen and Meseguer for Eqlog in the eighties.


Logic Program Logic Programming Extra Variable Functional Logic Strict Equality 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alpuente, M., Ballis, D., Falaschi, M.: Transformation and debugging of functional logic programs. In: Dovier, A., Pontelli, E. (eds.) 25 Years of Logic Programming. LNCS, vol. 6125, pp. 271–299. Springer, Heidelberg (2010)Google Scholar
  2. 2.
    Antoy, S.: Evaluation strategies for functional logic programming. Journal of Symbolic Computation 40, 875–903 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Antoy, S.: Programming with narrowing: A tutorial. Journal of Symbolic Compututation 45(5), 501–522 (2010)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Antoy, S., Echahed, R., Hanus, M.: Parallel evaluation strategies for functional logic languages. In: Naish, L. (ed.) ICLP, pp. 138–152. MIT Press (1997)Google Scholar
  5. 5.
    Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74–85 (2010)CrossRefGoogle Scholar
  7. 7.
    Arts, 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)CrossRefGoogle Scholar
  8. 8.
    Bae, K., Escobar, S., Meseguer, J.: Abstract logical model checking of infinite-state systems using narrowing. In: van Raamsdonk, F. (ed.) RTA. LIPIcs, vol. 21, pp. 81–96. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2013)Google Scholar
  9. 9.
    Clavel, M., Durán, F., Eker, S., Escobar, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: Unification and narrowing in maude 2.4. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 380–390. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  10. 10.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)zbMATHGoogle Scholar
  11. 11.
    Dershowitz, N.: Goal Solving as Operational Semantics. In: International Logic Programming Symposium, Portland, OR, pp. 3–17. MIT Press, Cambridge (1995)Google Scholar
  12. 12.
    Durán, F., Eker, S., Escobar, S., Meseguer, J., Talcott, C.L.: Variants, unification, narrowing, and symbolic reachability in maude 2.6. In: Schmidt-Schauß, M. (ed.) RTA. LIPIcs, vol. 10, pp. 31–40. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2011)Google Scholar
  13. 13.
    Durán, F., Meseguer, J.: On the church-rosser and coherence properties of conditional order-sorted rewrite theories. J. Log. Algebr. Program. 81(7-8), 816–850 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Echahed, R., Peltier, N.: Narrowing data-structures with pointers. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 92–106. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Escobar, S.: Refining weakly outermost-needed rewriting and narrowing. In: PPDP, pp. 113–123. ACM Press, New York (2003)Google Scholar
  16. 16.
    Escobar, S.: Implementing natural rewriting and narrowing efficiently. In: Kameyama, Y., Stuckey, P.J. (eds.) FLOPS 2004. LNCS, vol. 2998, pp. 147–162. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    Escobar, S., Meseguer, J., Thati, P.: Natural narrowing for general term rewriting systems. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 279–293. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  19. 19.
    Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. Journal of Logic and Algebraic Programming 81(7-8), 898–928 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Fay, M.: First-order unification in an equational theory. In: Joyner, W.H. (ed.) Proceedings of the 4th Workshop on Automated Deduction, Austin, Texas, USA, pp. 161–167. Academic Press (1979)Google Scholar
  21. 21.
    Goguen, J., Meseguer, J.: Eqlog: Equality, Types and Generic Modules for Logic Programming. In: de Groot, D., Lindstrom, G. (eds.) Logic Programming, Functions, Relations and Equations, pp. 295–363. Prentice-Hall (1986)Google Scholar
  22. 22.
    Goguen, J.A., Meseguer, J.: Equality, types, modules, and (why not?) generics for logic programming. J. Log. Program. 1(2), 179–210 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Goguen, J.A., Meseguer, J.: Models and equality for logical programming. In: Ehrig, H., Levi, G., Montanari, U. (eds.) TAPSOFT 1987 and CFLP 1987. LNCS, vol. 250, pp. 1–22. Springer, Heidelberg (1987)Google Scholar
  24. 24.
    Hanus, M.: The Integration of Functions into Logic Programming: From Theory to Practice. Journal of Logic Programming 19&20, 583–628 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  25. 25.
    Hanus, M.: Multi-paradigm declarative languages. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 45–75. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  26. 26.
    Hanus, M.: Functional logic programming: From theory to curry. In: Voronkov, A., Weidenbach, C. (eds.) Ganzinger Festschrif. LNCS, vol. 7797, pp. 123–168. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  27. 27.
    Hölldobler, S.: Foundations of Equational Logic Programming. LNCS, vol. 353. Springer, Heidelberg (1989)CrossRefzbMATHGoogle Scholar
  28. 28.
    Hullot, J.-M.: Canonical forms and unification. In: Bibel, W., Kowalski, R.A. (eds.) CADE 1980. LNCS, vol. 87, pp. 318–334. Springer, Heidelberg (1980)Google Scholar
  29. 29.
    Jouannaud, J.-P., Kirchner, H.: Completion of a set of rules modulo a set of equations. SIAM J. Comput. 15(4), 1155–1194 (1986)MathSciNetCrossRefzbMATHGoogle Scholar
  30. 30.
    Lloyd, J.W.: Programming in an integrated functional and logic language. Journal of Functional and Logic Programming 1999(3) (1999)Google Scholar
  31. 31.
    Martelli, A., Montanari, U.: An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems 4, 258–282 (1982)CrossRefzbMATHGoogle Scholar
  32. 32.
    Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Meseguer, J.: Multiparadigm logic programming. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 158–200. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  34. 34.
    Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol. 1376, pp. 18–61. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  35. 35.
    Meseguer, J., Thati, P.: Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols. Higher-Order and Symbolic Computation 20(1-2), 123–160 (2007)CrossRefzbMATHGoogle Scholar
  36. 36.
    Moreno, J.C.G., Hortalá-González, M.T., López-Fraguas, F.J., Rodríguez-Artalejo, M.: An approach to declarative programming based on a rewriting logic. J. Log. Program. 40(1), 47–87 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 371–443. Elsevier and MIT Press (2001)Google Scholar
  38. 38.
    Plump, D.: Essentials of term graph rewriting. Electr. Notes Theor. Comput. Sci. 51, 277–289 (2001)CrossRefzbMATHGoogle Scholar
  39. 39.
    Reddy, U.S.: Narrowing as the Operational Semantics of Functional Languages. In: Proceedings of Second IEEE Int’l Symp. on Logic Programming, pp. 138–151. IEEE Computer Society Press (1985)Google Scholar
  40. 40.
    Riesco, A., Rodríguez-Hortalá, J.: Singular and plural functions for functional logic programming. CoRR, abs/1203.2431 (2012)Google Scholar
  41. 41.
    Slagle, J.R.: Automated theorem-proving for theories with simplifiers commutativity, and associativity. J. ACM 21(4), 622–642 (1974)MathSciNetCrossRefzbMATHGoogle Scholar
  42. 42.
    TeReSe (ed.): Term Rewriting Systems. Cambridge University Press, Cambridge (2003)Google Scholar
  43. 43.
    Vigneron, L.: Automated deduction techniques for studying rough algebras. Fundamenta Informaticae 33(1), 85–103 (1998)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Santiago Escobar
    • 1
  1. 1.DSIC-ELPUniversitat Politècnica de ValènciaSpain

Personalised recommendations