Skip to main content
SpringerLink
Log in

Eliminating Irrelevant Non-determinism in Functional Logic Programs

  • Conference paper
  • First Online:
Practical Aspects of Declarative Languages (PADL 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10137))

Included in the following conference series:

Abstract

Functional logic programming languages support non-deterministic search and a flexible use of defined operations by applying them to unknown values. The use of these features has the risk that equal values might be computed several times or I/O computations could fail due to non-deterministic subcomputations. To detect such problems at compile time, we present a method to locate non-deterministic operations. If the non-determinism caused by some operation is semantically not relevant, the programmer can direct the compiler to produce only one result of a computation. If all the results of the computations are equal, this directive preserves the semantics and improves the operational behavior of programs. We define the declarative meaning of such annotations and propose both testing and verification techniques that respectively increase the confidence or formally prove that the non-determinism of an operation is irrelevant.

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

Access this chapter

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

Institutional subscriptions

Notes

  1. 1.

    The defining rules are inductively sequential if their patterns are just case distinctions on the constructors (see [2] for a precise definition). A consequence of this definition is that operations defined by functional patterns are NDD.

  2. 2.

    Note that this operation on value sets returns some value from the set and ignores the others, i.e., it implements “don’t care” non-determinism.

  3. 3.

    This behavior is specific to KiCS2. PAKCS suspends on this equation since it has a more restricted implementation of set functions.

  4. 4.

    http://www.informatik.uni-kiel.de/~mh/papers.

  5. 5.

    www.mercurylang.org.

References

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

    Article  MathSciNet  MATH  Google Scholar 

  2. Antoy, S.: Definitional trees. In: Kirchner, H., Levi, G. (eds.) ALP 1992. LNCS, vol. 632, pp. 143–157. Springer, Heidelberg (1992). doi:10.1007/BFb0013825

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  4. Antoy, S., Hanus, M.: Declarative programming with function patterns. In: Hill, P.M. (ed.) LOPSTR 2005. LNCS, vol. 3901, pp. 6–22. Springer, Heidelberg (2006). doi:10.1007/11680093_2

    Chapter  Google Scholar 

  5. Antoy, S., Hanus, M.: Overlapping rules and logic variables in functional logic programs. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 87–101. Springer, Heidelberg (2006). doi:10.1007/11799573_9

    Chapter  Google Scholar 

  6. Antoy, S., Hanus, M.: Set functions for functional logic programming. In: Proceedings of PPDP 2009, pp. 73–82. ACM Press (2009)

    Google Scholar 

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

    Article  Google Scholar 

  8. Antoy, S., Hanus, M.: Default rules for Curry. In: Gavanelli, M., Reppy, J. (eds.) PADL 2016. LNCS, vol. 9585, pp. 65–82. Springer, Cham (2016). doi:10.1007/978-3-319-28228-2_5

    Chapter  Google Scholar 

  9. Antoy, S., Hanus, M., Libby, S.: Proving non-deterministic computations in Agda. In: Proceedings of 24th International Workshop on Functional and Logic Programming (WFLP 2016), EPTCS (2016)

    Google Scholar 

  10. Braßel, B., Hanus, B., 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. Caballero, R., López-Fraguas, F.J.: Improving deterministic computations in lazy functional logic languages. J. Funct. Logic Program. 2003 (2003)

    Google Scholar 

  12. Christiansen, J., Fischer, S.: EasyCheck — test data for free. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 322–336. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78969-7_23

    Chapter  Google Scholar 

  13. Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: Proceedings of ICFP 2000, pp. 268–279. ACM Press (2000)

    Google Scholar 

  14. Cleva, J.M., Leach, J., López-Fraguas, F.J.: A logic programming approach to the verification of functional-logic programs. In: Proceedings of PPDP 2004, pp. 9–19. ACM Press (2004)

    Google Scholar 

  15. Fribourg, L.: Slog: a logic programming language interpreter based on clausal superposition and rewriting. In: Proceedings of IEEE International Symposium on Logic Programming, pp. 172–184 (1985)

    Google Scholar 

  16. González-Moreno, J.C., 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. Logic Program. 40, 47–87 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  17. Hanus, M.: Efficient implementation of narrowing and rewriting. In: Boley, H., Richter, M.M. (eds.) PDK 1991. LNCS, vol. 567, pp. 344–365. Springer, Heidelberg (1991). doi:10.1007/BFb0013543

    Chapter  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). doi:10.1007/978-3-642-37651-1_6

    Chapter  Google Scholar 

  19. Hanus, M., Skrlac, F.: A modular and generic analysis server system for functional logic programs. In: Proceedings of PEPM 2014, pp. 181–188. ACM Press (2014)

    Google Scholar 

  20. Hanus, M. et al.: PAKCS: The Portland Aachen Kiel Curry System (2016). http://www.informatik.uni-kiel.de/~pakcs/

  21. Loogen, R., Winkler, S.: Dynamic detection of determinism in functional logic languages. Theor. Comput. Sci. 142, 59–87 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  22. López-Fraguas, F.J., Rodríguez-Hortalá, J., Sánchez-Hernández, J.: A simple rewrite notion for call-time choice semantics. In: Proceedings of PPDP 2007, pp. 197–208. ACM Press (2007)

    Google Scholar 

  23. Stump, A.: Verified Functional Programming in Agda. ACM and Morgan & Claypool, New York (2016)

    Book  Google Scholar 

  24. TeReSe: Term Rewriting Systems, vol. 55 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2003)

    Google Scholar 

Download references

Acknowledgments

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

Author information

Authors and Affiliations

  1. Computer Science Department, Portland State University, Oregon, 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. University of Nebraska, Omaha, Nebraska, USA

    Yuliya Lierler

  2. Halmstad University, Halmstad, Sweden

    Walid Taha

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Antoy, S., Hanus, M. (2017). Eliminating Irrelevant Non-determinism in Functional Logic Programs. In: Lierler, Y., Taha, W. (eds) Practical Aspects of Declarative Languages. PADL 2017. Lecture Notes in Computer Science(), vol 10137. Springer, Cham. https://doi.org/10.1007/978-3-319-51676-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51676-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51675-2

  • Online ISBN: 978-3-319-51676-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation