×

zbMATH — the first resource for mathematics

Operational semantics for declarative multi-paradigm languages. (English) Zbl 1129.68042
Summary: Declarative multi-paradigm languages combine the most important features of functional, logic and concurrent programming. The computational model of such integrated languages is usually based on a combination of two different operational principles: narrowing and residuation. This work is motivated by the fact that a precise definition of an operational semantics including all aspects of modern multi-paradigm languages like laziness, sharing, non-determinism, equational constraints, external functions and concurrency does not exist. Therefore, in this article, we present the first rigorous operational description covering all the aforementioned features in a precise and understandable manner. We develop our operational semantics in several steps. First, we define a natural (big-step) semantics covering laziness, sharing and non-determinism. We also present an equivalent small-step semantics which additionally includes a number of practical features like equational constraints and external functions. Then, we introduce a deterministic version of the small-step semantics which makes the search strategy explicit; this is essential for profiling, tracing, debugging etc. Finally, the deterministic semantics is extended in order to cover the concurrent facilities of modern declarative multi-paradigm languages. The semantics developed provides an appropriate foundation for modeling actual declarative multi-paradigm languages like Curry. The complete operational semantics has been implemented and used with various programming tools.

MSC:
68Q55 Semantics in the theory of computing
68N17 Logic programming
68N18 Functional programming and lambda calculus
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aït-Kaci, H.; Lincoln, P.; Nasr, R., Le fun: logic, equations, and functions, (), 17-23
[2] Albert, E.; Antoy, S.; Vidal, G., Measuring the effectiveness of partial evaluation in functional logic languages, (), 103-124 · Zbl 1018.68500
[3] Albert, E.; Hanus, M.; Huch, F.; Oliver, J.; Vidal, G., An operational semantics for declarative multi-paradigm languages, () · Zbl 1129.68042
[4] Albert, E.; Hanus, M.; Huch, F.; Oliver, J.; Vidal, G., Operational semantics for functional logic languages, ()
[5] Albert, E.; Hanus, M.; Vidal, G., A practical partial evaluation scheme for multi-paradigm declarative languages, Journal of functional and logic programming, 1, (2002) · Zbl 1037.68011
[6] Albert, E.; Vidal, G., The narrowing-driven approach to functional logic program specialization, New generation computing, 20, 1, 3-26, (2001) · Zbl 1016.68024
[7] Albert, E.; Vidal, G., Symbolic profiling of multi-paradigm declarative languages, (), 148-167 · Zbl 1073.68545
[8] Antoy, S., Constructor-based conditional narrowing, (), 199-206
[9] Antoy, S.; Echahed, R.; Hanus, M., A needed narrowing strategy, Journal of the ACM, 47, 4, 776-822, (2000) · Zbl 1327.68141
[10] Antoy, S.; Hanus, M., Compiling multi-paradigm declarative programs into prolog, (), 171-185 · Zbl 0969.68667
[11] Armstrong, J.; Williams, M.; Wikstrom, C.; Virding, R., Concurrent programming in Erlang, (1996), Prentice Hall
[12] Barendregt, H., The lambda calculus—its syntax and semantics, (1984), Elsevier · Zbl 0551.03007
[13] Börger, E., A logical operational semantics of full prolog. part I: selection core and control, (), 36-64 · Zbl 0925.68301
[14] Börger, E., A logical operational semantics of full prolog. part II: built-in predicates for database manipulations, (), 1-14 · Zbl 0796.68140
[15] Börger, E.; López-Fraguas, F.; Rodríguez-Artalejo, M., A model for mathematical analysis of functional logic languages and their implementations, (), 410-415
[16] Börger, E.; Rosenzweig, D., A mathematical definition of full prolog, Science of computer programming, 24, 3, 249-286, (1995) · Zbl 0832.68022
[17] Börger, E.; Rosenzweig, D., The WAM—definition and compiler correctness, (), 20-90 · Zbl 0832.68024
[18] Braßel, B., Hanus, M., Huch, F., Silva, J., Vidal, G., 2004a. Run-time profiling of functional logic programs. In: Pre-Proceedings of the Int’l Symposium on Logic-based Program Synthesis and Transformation. LOPSTR. 2004 · Zbl 1134.68329
[19] Braßel, B.; Hanus, M.; Huch, F.; Vidal, G., A semantics for tracing declarative multi-paradigm programs, () · Zbl 1134.68329
[20] Chakravarty, M.; Guo, Y.; Köhler, M.; Lock, H., Goffin — higher-order functions meet concurrent constraints, Science of computer programming, 30, 1-2, 157-199, (1998) · Zbl 0891.68016
[21] Damas, L.; Milner, R., Principal type-schemes for functional programs, (), 207-212
[22] Debbabi, M.; Bolignano, D., A semantic theory for ML higher-order concurrency primitives, (), 145-184
[23] Debray, S.; Mishra, P., Denotational and operational semantics for prolog, Journal of logic programming, 5, 61-91, (1988) · Zbl 0632.68020
[24] Echahed, R.; Janodet, J., Admissible graph rewriting and narrowing, (), 325-340 · Zbl 0949.68081
[25] Giovannetti, E.; Levi, G.; Moiso, C.; Palamidessi, C., Kernel leaf: A logic plus functional language, Journal of computer and system sciences, 42, 363-377, (1991) · Zbl 0717.68013
[26] González-Moreno, J.; Hortalá-González, M.; López-Fraguas, F.; Rodríguez-Artalejo, M., An approach to declarative programming based on a rewriting logic, Journal of logic programming, 40, 47-87, (1999) · Zbl 0942.68060
[27] Gurevich, Y., Sequential abstract state machines capture sequential algorithms, ACM transactions on computational logic, 1, 1, 77-111, (2000) · Zbl 1365.68258
[28] Habel, A.; Plump, D., Term graph narrowing, Mathematical structures in computer science, 6, 6, 649-676, (1996) · Zbl 0864.68073
[29] Hanus, M., Parametric order-sorted types in logic programming, (), 181-200 · Zbl 0967.68508
[30] Hanus, M., The integration of functions into logic programming: from theory to practice, Journal of logic programming, 19&20, 583-628, (1994) · Zbl 0942.68526
[31] Hanus, M., A unified computation model for functional and logic programming, (), 80-93
[32] Hanus, M., 2003. Curry: An integrated functional logic language. Available at:http://www.informatik.uni-kiel.de/ curry/
[33] Hanus, M.; Koj, J., An integrated development environment for declarative multi-paradigm programming, (), 1-14, also available from the Computing Research Repository (CoRR) at http://arXiv.org/abs/cs.PL/0111039
[34] Hanus, M.; Prehofer, C., Higher-order narrowing with definitional trees, Journal of functional programming, 9, 1, 33-75, (1999) · Zbl 0926.68028
[35] Haridi, S.; Janson, S.; Palamidessi, C., Structural operational semantics for AKL, Journal of future generation computer systems, 8, 409-421, (1992)
[36] Hortalá-González, T.; Ullán, E., An abstract machine based system for a lazy narrowing calculus, (), 216-232 · Zbl 0987.68855
[37] Huber, M., Varsek, I., 1987. Extended Prolog with order-sorted resolution. In: Proc. of the 4th IEEE Int’l Symposium on Logic Programming. San Francisco, pp. 34-43
[38] Janson, S.; Haridi, S., Programming paradigms of the andorra kernel language, (), 167-183
[39] Jones, N., Mycroft, A., 1984. Stepwise development of operational and denotational semantics for Prolog. In: Proc. of the 2nd Int’l Conf. on Logic Programming. ICLP’84, pp. 281-288
[40] Launchbury, J., A natural semantics for lazy evaluation, (), 144-154
[41] Lloyd, J., Foundations of logic programming, (1987), Springer-Verlag Berlin · Zbl 0668.68004
[42] Lloyd, J., Programming in an integrated functional and logic language, Journal of functional and logic programming, 3, 1-49, (1999)
[43] López-Fraguas, F.; Sánchez-Hernández, J., TOY: A multiparadigm declarative system, (), 244-247
[44] Moreno-Navarro, J.; Rodríguez-Artalejo, M., Logic programming with functions and predicates: the language babel, Journal of logic programming, 12, 3, 191-224, (1992) · Zbl 0754.68031
[45] Panangaden, P.; Reppy, J., The essence of concurrent ML, (), 5-29
[46] Haskell 98 language and libraries—the revised report, () · Zbl 1067.68041
[47] Peyton Jones, S.; Gordon, A.; Finne, S., Concurrent Haskell, (), 295-308
[48] Podelski, A.; Smolka, G., Operational semantics of constraint logic programs with coroutining, (), 449-463
[49] Sansom, P.; Peyton-Jones, S., Formally based profiling for higher-order functional languages, ACM transactions on programming languages and systems, 19, 2, 334-385, (1997)
[50] Saraswat, V.; Rinard, M.; Panangaden, P., Semantic foundation of concurrent constraint programming, (), 333-352
[51] Schulte, C.; Smolka, G., Encapsulated search for higher-order concurrent constraint programming, (), 505-520
[52] Sestoft, P., Deriving a lazy abstract machine, Journal of functional programming, 7, 3, 231-264, (1997) · Zbl 0881.68049
[53] Slagle, J., Automated theorem-proving for theories with simplifiers, commutativity and associativity, Journal of the ACM, 21, 4, 622-642, (1974) · Zbl 0296.68092
[54] Smolka, G., Logic programming with polymorphically order-sorted types, (), 53-70 · Zbl 0708.68016
[55] Smolka, G., A foundation for higher-order concurrent constraint programming, (), 50-72
[56] Vidal, G., Cost-augmented partial evaluation of functional logic programs, Higher-order and symbolic computation, 17, 1-2, 7-46, (2004) · Zbl 1075.68010
[57] Wadler, P.; Blott, S., How to make ad-hoc polymorphism less ad hoc, (), 60-76
[58] Wallace, M., Chitil, O., Brehm, T., Runciman, C., 2001. Multiple-view tracing for Haskell: a new Hat. In: Proc. of the 2001 ACM SIGPLAN Haskell Workshop. Universiteit Utrecht UU-CS-2001-23
[59] Warren, D., 1983. An abstract Prolog instruction set. Technical note 309, SRI International, Stanford
[60] Warren, D.H.D., Higher-order extensions to prolog — are they needed?, ()
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.