Abstract semantics for a higher-order functional language with logic variables

Abstract

Although there is considerable experience in using languages that combine the functional and logic programming paradigms, the problem of providing an adequate semantic foundation for such languages has remained open. In an earlier paper, we solved this problem for first-order languages by reducing the problem to that of solving simultaneous fixpoint equations involving closure operators over a Scott domain and showing that the resulting semantics was fully abstract with respect to the operational semantics. These results showed that the first-order fragment could be viewed as a language of incremental definition of data structures through constraint intersection. The problem for higher-order languages remained open, in part because higher-order functions can interact with logic variables in complicated ways to give rise to behavior reminiscent of own variables in Algol-60. We solve this problem in this paper. We show that in the presence of logic variables, higher-order functions may be modeled extensionally as closure operators on function graphs ordered in a way reminiscent of the ordering on extensible records in studies of inheritance. We then extend the equation solving semantics of the first-order subset to the full language, and prove the usual soundness and adequacy theorems for this semantics. These results show that a higher-order functional language with logic variables can be viewed as a language of incremental definition of functions.