Abstract
Unification is a useful process by which one attempts to find a substitute satisfying a given set of equations. Among several kinds of unification algorithms, the unification for equations between first-order terms is known to be decidable and to satisfy the completeness. A unification mechanism plays an important role in logic programming languages, such as Prolog. In this paper, we propose an approach to incorporating a unification mechanism into a functional programming language via first-class environments. The first-class environment is a reflective feature in a programming language, which enables us to reify environments, to handle them as first-class values such as integers and Boolean values, and to reflect the reified environment as an environment at a meta-level. By identifying resulting substitutions of unification problems as first-class environments, we can introduce unification into functional programming languages. In this paper, we first give the syntax of a simple functional language with unifications. Second, we give its operational semantics in the style of Kahn’s natural semantics. Finally, we introduce some related works and show the future direction of our works.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M., Cardelli, L., Curien, P.-L., Lévy, J.-J.: Explicit substitutions. Journal of Functional Programming 1(4), 375–416 (1991)
Baarer, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1999)
Baader, F., Snyder, W.: Unification theory. In: Robinson, J., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 447–533. Elsevier Science Publishers (2001)
Barendregt, H.P.: The Lambda Calculus. Elsevier (1984)
Curien, P.L.: An abstract framework for environment machines. Theor. Comput. Sci. 82, 389–402 (1991)
Curien, P.L., Hardin, T., Lévy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. J. ACM 43(2), 363–397 (1996)
Dowek, G., Hardin, T., Kirchner, C.: Higher-order unification via explicit substitutions, extended abstract. In: Proceedings of the Symposium on Logic in Computer Science, pp. 22–39. Springer (1987)
Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Wirsing, M., Vidal-Naquet, G. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)
Nishizaki, S.: Simply typed lambda calculus with first-class environments. Publications of Reseach Institute for Mathematical Sciences Kyoto University 30(6), 1055–1121 (1995)
Nishizaki, S.: Polymorphic environment calculus and its type inference algorithm. Higher-Order and Symbolic Computation 13(3), 239–278 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 ICST Institute for Computer Science, Social Informatics and Telecommunications Engineering
About this paper
Cite this paper
Nishizaki, Sy. (2014). Incorporating First-Order Unification into Functional Language via First-Class Environments. In: Das, V.V., Elkafrawy, P. (eds) Signal Processing and Information Technology. SPIT 2012. Lecture Notes of the Institute for Computer Sciences, Social Informatics and Telecommunications Engineering, vol 117. Springer, Cham. https://doi.org/10.1007/978-3-319-11629-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-11629-7_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11628-0
Online ISBN: 978-3-319-11629-7
eBook Packages: Computer ScienceComputer Science (R0)