zbMATH — the first resource for mathematics

From Boolean equalities to constraints. (English) Zbl 1362.68033
Falaschi, Moreno (ed.), Logic-based program synthesis and transformation. 25th international symposium, LOPSTR 2015, Siena, Italy, July 13–15, 2015. Revised selected papers. Cham: Springer (ISBN 978-3-319-27435-5/pbk; 978-3-319-27436-2/ebook). Lecture Notes in Computer Science 9527, 73-88 (2015).
Summary: 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.
For the entire collection see [Zbl 1326.68017].
68N17 Logic programming
68N18 Functional programming and lambda calculus
Curry; Haskell; KiCS2; PAKCS
Full Text: DOI
[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) · Zbl 1129.68042 · doi:10.1016/j.jsc.2004.01.001
[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) · Zbl 1278.68056
[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) · doi:10.1145/773184.773205
[4] Antoy, S., Echahed, R., Hanus, M.: A needed narrowing strategy. J. ACM 47(4), 776–822 (2000) · Zbl 1327.68141 · doi:10.1145/347476.347484
[5] Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74–85 (2010) · Zbl 05748176 · doi:10.1145/1721654.1721675
[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)
[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)
[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)
[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)
[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) · Zbl 05934426 · doi:10.1007/978-3-642-22531-4_1
[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) · Zbl 06314916 · doi:10.1007/978-3-642-45284-0_9
[12] Cousot, P.: Types as abstract interpretations. In: Proceedings of the 24th ACM Symposium on Principles of Programming Languages (Paris), pp. 316–331 (1997) · doi:10.1145/263699.263744
[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) · doi:10.1145/512950.512973
[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) · doi:10.1145/582153.582176
[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) · Zbl 0871.00033 · doi:10.1007/BFb0026998
[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) · doi:10.1007/3-540-45241-9_6
[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) · doi:10.1145/1273920.1273942
[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) · Zbl 1383.68017 · doi:10.1007/978-3-642-37651-1_6
[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) · doi:10.1145/2543728.2543744
[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)
[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) · Zbl 0435.68015 · doi:10.1007/3-540-09981-6_19
[24] Peyton Jones, S.: Haskell 98 Language and Libraries-The Revised Report. Cambridge University Press, Cambridge (2003) · Zbl 1067.68041
[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)
[26] Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of the ACM Annual Conference, pp. 717–740. ACM Press (1972) · doi:10.1145/800194.805852
[27] Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965) · Zbl 0139.12303 · doi:10.1145/321250.321253
[28] Slagle, J.R.: Automated theorem-proving for theories with simplifiers, commutativity, and associativity. J. ACM 21(4), 622–642 (1974) · Zbl 0296.68092 · doi:10.1145/321850.321859
[29] Warren, D.H.D.: Higher-order extensions to Prolog: are they needed? Mach. Intell. 10, 441–454 (1982)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.