Abstract
The expressive power of logic programming may be achieved within a functional programming framework by extending the functional language with the ability to evaluate absolute set abstractions. By absolute set abstraction, logical variables are introduced into functional languages as first class objects. Their set-valued interpretations are implicitly defined by the constraining equations. Narrowing and unification can be used to solve these constraining equations to produce the satisfying instantiations of the logic variables. In this paper, we study an execution mechanism for evaluating absolute set abstraction in a first order (non-strict) functional programming setting. First, we investigate the semantics of absolute set abstraction. It is shown that absolute set abstraction is no more than a setvalued expression involving the evaluation of function inversion. Functional equality is defined coinciding with the semantics of the continuous and strict equality function in functional programming. This new equality means that the well known techniques for equation solving can be adopted as a proper mechanism for solving the constraining equations which are the key to the evaluation of absolute set abstraction. The main result of this paper lies in the study of a particular narrowing strategy, called lazy pattern driven narrowing, which is proved to be complete and optimal for evaluating absolute set abstraction in the sense that a complete set of minimal solutions of the constraining equations can be generated by a semantic unification procedure based on this narrowing strategy. This indicates that a mechanism for equation solving can be developed within a functional programming context, producing a more expressive language.
On leave from Dept. of Computer Science, Tsinghua University, Beijing, PRC.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Bellia,M. and Giorgio, L. "The Relation Between Logic and Functional Language: A Survey" The Journal of Logic Programming 3, Oct. 1986.
Burstall R. et.al. "Hope: an experimental applicative language" Proc. Lisp Conf. Stanford. 1980.
Darlington, J. Field, A.J. and Pull, H. "The unification of Functional and Logic languages" in Logic Programming: Functions, Relations and Equations, ed. Doug Degroot and G. Lindstrom, Prentice-Hall, 1986.
Darlington, J. et.al. "A Functional Programming Environment Supporting Execution, Partial Execution and Transformation" To appear.
Dershowitz, N. and Plaisted, D.A. "Equational programming" in Machine Intelligence, D.Michie, J.E. Hayes and J. Richards, eds., 1986.
Darlington, J, Yi-ke Guo "Narrowing and unification in Functional Programming" Research Report, FPS, DoC, Imperial College, Oct. 1988.
Darlington, J, Yi-ke Guo "On Constraint Functional Programming" To appear.
Van Emden, Maarten. H. and Yukawa, K. "Logic Programming with Equations" Journal of Logic Programming 4, 1986.
Fay, M.J., "First-order Unification in an Equational Theory" in 4th Workshop on Automated Deduction, 1979.
Fribourg, L., "SLOG: A logic programming language interpreter based on clausal superposition and rewriting" in Proc. 1985 Symposium on Logic Programming, Boston, Mass.
Gallier, J.H. and Snyder, W. "A general Complete E-unification procedure", in Proc. of RTA87, LNCS 256,1987
E. Giovannetti, G. Levi, C. Moiso and C.Palamidessi, Kernel LEAF: An experimental logic plus functional language-its syntax, semantics and computational model, ESPRIT Project 415, Second year report 1986.
Hullot, J. M., "Canonical Forms and Unification, "in Proc. 5th conference on Automated Deduction, LNCS 80, 1980.
Huet, G. Levy, L.L. "Computations in Nonambiguous Linear Rewriting Systems" Research Report. INRIA. 1979.
Huet,G. and Oppen, D.C., "Equations and Rewrite Rules: A Survey" TR-CSL-111, SRI, Jan, 1980.
Hussmann, H, "Nichtdeterministische Algebraische Spezifikationen (in German), Ph.D. thesis, Univ. of Passau, 1988.
Jaffar, J., Lassez, J. and Maher, M. "Constraint Logic Programming" in Proc. of. 14th ACM symp. POPL. 1987.
Jayaraman, B. and Silberman,F., "Equations, Sets and Reduction Semantics for Functional and Logic Programming" in Proc. of. ACM Confs on LISP and Functional Programming, Aug. 1986.
Martelli, A. et,al "An algorithm for unification in equational theories", in Proc. 1986 International Symposium on Logic Programming, Salt Lake City, Utah, 1986.
Reddy, U.S. "Narrowing as the Operational Semantics of Functional Languages" Proc. of the 1985 Symp. on Logic Programming, July, 1985.
Reynolds, J.C. "Transformational Systems and the Algebraic Structure of Atomic Formulas." Machine Intelligence 5. ed. Michie, D. Edinburgh Univ. Press, 1970.
You, Jia-Huai "Unification Modulo an Equality Theory for Embedding Functional Programming into Prolog" Extended Abstract, Dept. of Computing Science, Univ.of Alberta, Canada, May, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1989 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Darlington, J., Guo, Yk. (1989). Narrowing and unification in functional programming —An evaluation mechanism for absolute set abstraction. In: Dershowitz, N. (eds) Rewriting Techniques and Applications. RTA 1989. Lecture Notes in Computer Science, vol 355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-51081-8_102
Download citation
DOI: https://doi.org/10.1007/3-540-51081-8_102
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-51081-9
Online ISBN: 978-3-540-46149-4
eBook Packages: Springer Book Archive