Research Article
Incorporating First-Order Unification into Functional Language via First-Class Environments
@INPROCEEDINGS{10.1007/978-3-319-11629-7_3, author={Shin-ya Nishizaki}, title={Incorporating First-Order Unification into Functional Language via First-Class Environments}, proceedings={Signal Processing and Information Technology. Second International Joint Conference, SPIT 2012, Dubai, UAE, September 20-21, 2012, Revised Selected Papers}, proceedings_a={SPIT}, year={2014}, month={11}, keywords={functional programming language first-order unification first-class environment unification}, doi={10.1007/978-3-319-11629-7_3} }- Shin-ya Nishizaki
Year: 2014
Incorporating First-Order Unification into Functional Language via First-Class Environments
SPIT
Springer
DOI: 10.1007/978-3-319-11629-7_3
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.
