A Fully Abstract Semantics for a First-Order Functional Language with Logic Variables

Abstract

There is much interest in combining the functional and logic programming paradigms � in particular, there have been several proposals for adding logic variables to functional languages, since that permits incremental construction of data structures through constraint intersection. While it is straight-forward to give an abstract semantics for functional languages and for logic languages, it has proven surprisingly di cult to give a proper semantic account of functional languages with logic variables. In this paper, we present a rst-order functional language with logic variables and give its meaning using a structural operational semantics. We also give it a denotational semantics, using a novel technique involving closure operators on a Scott domain. Finally, we show that these two semantics correspond in the strongest possible way|weshow that the denotational semantics is fully abstract with respect to the operational semantics. The techniques developed in this paper are quite general, and can be used to give semantics to any constraint-based logic programming languages. Our results can also be interpreted as a generalization of Kahn semantics for data ow networks in which processes not only exchange messages, but have access to a shared global address space in which variables are bound through constraint intersection. Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Functional Programming � D.3.1 [Programming Languages]: Formal De nitions and Theory- semantics � D.3.2 [Programming Languages]: Data ow Languages � F.3.2 [Theory of Computation]: Semantics of Programming Languages- denotational semantics � F.4.1 [Theory of Computation]: Mathematical Logic- logic programming