Exception Handling in Logic Programming

Introduction

One problem on logic programming is to treat the extra-logical primitive in a high-level way. The progress of logic programming has enriched the theory of Horn clauses with higher-order programming, mutual exclusion [1], etc. Never the less exception handling could not be dealt with elegantly.

In this paper, we propose a purely logical solution to this problem. It involves the direct employment of linear logic and game semantics (or computability logic [2, 3] to allow for goals with exception handling capability. A prioritizedchoice disjunctive (PCD) goal – is of the form $G0 \oplus *G1$ where G0, G1 are goals. We assume here G0 has higher priority. Executing this goal with respect to a program $D - ex(D, G0 \oplus *G1)$ – has the following intended semantics:
Sequentially choose the first successful one between $ex(D, G0), ex(D, G1)$.

An illustration of this aspect is provided by the following definition of the relation sort(X, Y) which holds if Y is a sorted list of X:

$$Sort(X, Y) : -heap sort(X, Y) \oplus *quick sort(X, Y)$$

The body of the definition above contains a PCD goal. As a particular example, solving the query sort ([3, 100, 40, 2], Y) would result in selecting and executing the first goal heap sort ([3, 100, 40, 2], Y). If the heap sort module is available in the program, then the given goal will succeed, producing solutions for Y. If the execution fails, the machine tries the plan B, i.e., the quicksort module.

The operator $\oplus$ is, in fact, indispensable to logic programming, as it is a logic-programming equivalent of the if-then-else in imperative languages. To see this, consider the following example:

$$Max(X, Y, Z) : -(X \geq Y \land Z = X) \oplus *(Z = Y).$$

Of course, we can specify PCD goals using cut in Prolog, but it is well-known that cuts complicates the declarative meaning of the program [4].

As seen from the example above, PCD goals of the form $A \oplus *B$ can be used to specify a task A, together with the failure-handling routine B.

The exact meaning of $A \oplus *B$ can be explained by translating it to

$$A \oplus (\neg A \land B)$$

Here, dealing with ¬A, we rely on closed world assumption.

This paper proposes Prolog⊕*, an extension of Prolog with PCD operators in goal formulas. The remainder of this paper is structured as follows. We describe Prolog⊕* in the next section. In Section 3, we present some examples of Prolog⊕*.

The Language

The language is a version of Horn clauses with PCD goals. It is described by G- and D-formulas given by the syntax rules below:

$$G := A | G \wedge G | \exists x G | G \oplus *G$$
$$D := A | G \supset A | \forall x D | D \wedge D$$

In the rules above, A represents an atomic formula. A D-formula is called a Horn clause with PCD goals.

We will present a proof procedure for this language as a set of rules. These rules in fact depend on the top-level constructor in the expression, a property known as uniform provability [5, 6, 7, 8]. Note that proof search alternates between two phases: the goal-reduction phase and the back chaining phase. In the goal-reduction phase (denoted by $pv(D, G)$), the machine tries to solve a goal G from a clause D by simplifying G. The rule (6)-(8) are related to this phase. If G becomes an atom, the machine switches to the back chaining mode. This is encoded in the rule (5). In the back chaining mode (denoted by $bc(D1, D, A)$), the machine tries to solve an atomic goal A by first reducing a Horn clause D1 to simpler forms (via rule (3) and (4)) and then back chaining on the resulting clause (via rule (1) and (2)).