Horn clause logic with external procedures : towards a theoretical framework

Sammanfattning:

Horn clause logic has certain properties which limit its usefulness as a programming language. In this thesis we concentrate on three such limitations: (1) Horn clause logic is not intended for the implementation of algorithms. Thus, if a problem has an efficient algorithmic solution it may be difficult to express this within the Horn clause formalism. (2) To work with a predefined structure like integer arithmetic, one has to axiomatize it by a Horn clause program. Thus functions of the structure are to be represented as predicates of the program. (3) Instead of re-implement existing software modules, it is clearly better to re-use them. To this end, a support for combining Horn clause logic with other programming languages is needed.

When extending the Horn clause formalism, there is always a trade-off between general applicability and purity of the resulting system. There have been many suggestions for solving some of problems (1) to (3). Most of them use one of the following strategies: (a) To allow new operational features, such as access to low-level constructs of other languages. (b) To introduce new language constructs, and to support them by a clean declarative semantics and a complete operational semantics.

In this thesis a solution to problems (1) to (3) is suggested. It combines the strategies of (a) and (b) by limiting their generality: We allow Horn clause programs to call procedures written in arbitrary languages. It is assumed however that these procedures are either functional or relational. The functional procedures yield a ground term as output whenever given ground terms as input. Similarly, the relational procedures either succeed or fail whenever applied to ground terms. Under these assumptions the resulting language has a clean declarative semantics.

For the operational semantics, an extended but incomplete unification algorithm, called S-unify is developed. By using properties of this algorithm we characterize classes of goals for which our interpreter is complete. It is also formally proved that (a slightly extended version of) S-unify is as complete as possible under the adopted assumptions.