Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Logic-Based Program Synthesis and Transformation

LOPSTR 2015: Logic-Based Program Synthesis and Transformation pp 73–88Cite as

From Boolean Equalities to Constraints

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9527))

Abstract

Although functional as well as logic languages use equality to discriminate between logically different cases, the operational meaning of equality is different in such languages. Functional languages reduce equational expressions to their Boolean values, True or False, logic languages use unification to check the validity only and fail otherwise. Consequently, the language Curry, which amalgamates functional and logic programming features, offers two kinds of equational expressions so that the programmer has to distinguish between these uses. We show that this distinction can be avoided by providing an analysis and transformation method that automatically selects the appropriate operation. Without this distinction in source programs, the language design can be simplified and the execution of programs can be optimized. As a consequence, we show that one kind of equational expressions is sufficient and unification is nothing else than an optimization of Boolean equality.

This material is based in part upon work supported by the National Science Foundation under Grant No. 1317249.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    We use the syntax of Haskell [24] for functional programs.

  2. 2.

    Note that Curry requires the explicit declaration of free variables, as x in the rule of last, to ensure checkable redundancy, but we omit them in this paper for the sake of simplicity.

  3. 3.

    Note that we omit the type Success, as proposed in [6]. Hence, equational constraints as well as rule conditions are of type Bool rather than Success, in contrast to the current definition of Curry [21].

  4. 4.

    Since we do not discuss residuation and concurrent computations, we also omit the difference between rigid and flexible case expressions [18].

  5. 5.

    The latter equality could also be improved if disequality constraints [7, 22] are available in the target language, but since this is not the case for standard implementations of Curry, we do not consider them in this paper.

  6. 6.

    A logic programmer might wonder about the low number of equational constraints even in larger functional logic programs. This is mainly due to the fact that functional logic programming supports nested expressions (where Prolog programmers have to use auxiliary variables and unification to connect the result from an inner computation to an outer one). Moreover, predicates delivering multiple results can also be expressed as non-deterministic functions.

References

  1. Albert, E., Hanus, M., Huch, F., Oliver, J., Vidal, G.: Operational semantics for declarative multi-paradigm languages. J. Symb. Comput. 40(1), 795–829 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  2. Alpuente, M., Comini, M., Escobar, S., Falaschi, M., Lucas, S.: Abstract diagnosis of functional programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  3. Antoy, S.: Constructor-based conditional narrowing. In: Procedings of the 3rd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), pp. 199–206. ACM Press (2001)

    Google Scholar 

  4. Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  5. Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74–85 (2010)

    Article  Google Scholar 

  6. Antoy, S., Hanus, M.: Curry without Success. In: Proceedings of the 23rd International Workshop on Functional and (Constraint) Logic Programming (WFLP 2014), CEUR Workshop Proceedings, vol. 1335, pp. 140–154. CEUR-WS.org, (2014)

    Google Scholar 

  7. Arenas-Sánchez, P., Gil-Luezas, A., López-Fraguas, F.J.: Combining lazy narrowing with disequality constraints. In: Penjam, J. (ed.) PLILP 1994. LNCS, vol. 844. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  8. Bert, D., Echahed, R.: Abstraction of conditional term rewriting systems. In: Proceedings of the 1995 International Logic Programming Symposium, pp. 147–161. MIT Press (1995)

    Google Scholar 

  9. Bert, D., Echahed, R., Østvold, M.: Abstract rewriting. In: Cousot, P., Filé, G., Falaschi, M., Rauzy, A. (eds.) WSA 1993. LNCS, vol. 724. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  10. Braßel, B., Hanus, M., Peemöller, B., Reck, F.: KiCS2: A new compiler from curry to haskell. In: Kuchen, H. (ed.) WFLP 2011. LNCS, vol. 6816, pp. 1–18. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Braßel, B., Hanus, M., Peemöller, B., Reck, F.: Implementing equational constraints in a functional language. In: Sagonas, K. (ed.) PADL 2013. LNCS, vol. 7752, pp. 125–140. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  12. Cousot, P.: Types as abstract interpretations. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (Paris), pp. 316–331 (1997)

    Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction of approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)

    Google Scholar 

  14. Damas, L., Milner, R.: Principal type-schemes for functional programs. In: Proceedings 9th Annual Symposium on Principles of Programming Languages, pp. 207–212 (1982)

    Google Scholar 

  15. Hanus, M.: Teaching functional and logic programming with a single computation model. In: Hartel, P.H., Kuchen, H. (eds.) PLILP 1997. LNCS, vol. 1292. Springer, Heidelberg (1997)

    Google Scholar 

  16. Hanus, M.: High-Level Server Side Web Scripting in Curry. In: Ramakrishnan, I.V. (ed.) PADL 2001. LNCS, vol. 1990, pp. 76–92. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  17. Hanus, M.: Putting declarative programming into the web: translating curry to JavaScript. In: Proceedings of the 9th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2007), pp. 155–166. ACM Press (2007)

    Google Scholar 

  18. Hanus, M.: Functional logic programming: from theory to curry. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 123–168. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  19. Hanus, M., Antoy, S., Braßel, B., Engelke, M., Höppner, K., Koj, J., Niederau, P., Sadre, R., Steiner, F.: PAKCS: The portland aachen kiel curry system (2015). http://www.informatik.uni-kiel.de/pakcs/

  20. Hanus, M., Skrlac, F.: A modular and generic analysis server system for functional logic programs. In: Proceedings ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM 2014), pp. 181–188. ACM Press (2014)

    Google Scholar 

  21. Hanus, M.: Curry: an integrated functional logic language (vers. 0.8.3). http://www.curry-language.org, 2012

  22. Kuchen, H., López-Fraguas, F.J., Moreno-Navarro, J.J., Rodríguez-Artalejo, M.: Implementing a lazy functional logic language with disequality constraints. In: Proceedings of the 1992 Joint International Conference and Symposium on Logic Programming. MIT Press (1992)

    Google Scholar 

  23. Mycroft, A.: The theory and practice of transforming call-by-need into call-by-value. In: Robinet, B. (ed.) International Symposium on Programming. Lecture Notes in Computer Science, vol. 83, pp. 269–281. Springer, Heidelberg (1980)

    Chapter  Google Scholar 

  24. Peyton Jones, S.: Haskell 98 Language and Libraries-The Revised Report. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  25. Reddy, U.S.: Narrowing as the operational semantics of functional languages. In: Proceedings of IEEE International Symposium on Logic Programming, pp. 138–151, Boston (1985)

    Google Scholar 

  26. Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference, pp. 717–740. ACM Press (1972)

    Google Scholar 

  27. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  28. Slagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity, and associativity. J. ACM 21(4), 622–642 (1974)

    Article  MathSciNet  MATH  Google Scholar 

  29. Warren, D.H.D.: Higher-order extensions to Prolog: are they needed? Mach. Intell. 10, 441–454 (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Portland State University, Portland, OR, USA

    Sergio Antoy

  2. Institut Für Informatik, CAU Kiel, 24098, Kiel, Germany

    Michael Hanus

Authors
  1. Sergio Antoy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Michael Hanus
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Michael Hanus .

Editor information

Editors and Affiliations

  1. Università di Siena, Siena, Italy

    Moreno Falaschi

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Antoy, S., Hanus, M. (2015). From Boolean Equalities to Constraints. In: Falaschi, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2015. Lecture Notes in Computer Science(), vol 9527. Springer, Cham. https://doi.org/10.1007/978-3-319-27436-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-27436-2_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-27435-5

  • Online ISBN: 978-3-319-27436-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation