The Intricacies of Three-Valued Extensional Semantics for Higher-Order Logic Programs

1 Introduction

Recent research [Wadge, 1991; Bezem, 1999; 2001; Charalambidis et al., 2013; 2017; 2018; Rondogiannis and Symeonidou, 2018] has investigated the possibility of providing extensional semantics to higher-order logic programming (HOLP). Extensionality facilitates the use of standard set theory in order to reason about programs, at the price of a relatively restricted syntax.

There exist two research directions for providing extensional semantics to higher-order logic programs. The first one [Wadge, 1991; Charalambidis et al., 2013; 2014; 2018] has been developed using domain-theoretic tools. The second approach [Bezem, 1999; 2001; Rondogiannis and Symeonidou, 2018] is based on processing the ground instantiation of the program. The two research directions are not unrelated: it has been shown by Charalambidis et al. [2017] that for a broad class of positive programs, the two approaches coincide.

In this paper we focus on the second approach, initially proposed by Bezem [1999; 2001] for positive higher-order logic programs. Recently, it was demonstrated by Rondogiannis and Symeonidou [2018] that by combining the technique of Bezem with the infinite-valued semantics of Rondogiannis and Wadge [2005], we obtain an extensional semantics for higher-order logic programs with negation. At the same time, a negative result was also established: by combining the technique of Bezem with the stable model semantics [Gelfond and Lifschitz, 1988], we get a semantics that is not necessarily extensional! It remained as an open problem of Rondogiannis and Symeonidou [2018] whether the combination of the technique of Bezem with the well-founded approach [Gelder et al., 1991] leads to an extensional semantics. It is exactly this problem that we undertake to solve in the present paper, the main contributions of which can be summarized as follows:

∗This paper is an abridged version of a paper with the same tile, that won a best-paper award at the ICLP-2017 conference.

• We demonstrate that the well-founded adaptation of Bezem's technique, does not in general lead to an extensional model. This indicates that the addition of negation to higher-order logic programming is not such a straightforward task as it was possibly initially anticipated.
• Despite the above negative result, we prove that the wellfounded adaptation of Bezem's technique gives an extensional two-valued model in the case of stratified programs. This result affirms the importance and the wellbehaved nature of stratified programs, which was, until now, only known for the first-order case.
• We study the more general question of the possible existence of an alternative extensional three-valued semantics for higher-order logic programs with negation. We indicate that in order to achieve such a semantics, one has to make some strong assumptions regarding the behaviour of negation in higher-order logic programs.

The next two sections motivate in an intuitive way the proposed approach. The remaining sections develop the material in a formal way. The proofs of all results can be found in the original paper [Rondogiannis and Symeonidou, 2017].

2 Extensional HOLP

W. W. Wadge [1991] suggested that if we appropriately restrict the syntax of HOLP, then we can obtain a denotational semantics in which predicates denote sets, much like the traditional semantics of higher-order functional programming. The most crucial syntactic restriction imposed by Wadge (and later independently by M. Bezem [1999; 2001]), is the following:

The extensionality syntactic restriction: In the head of every rule in a program, each argument of predicate type must be a variable, and all such variables must be distinct.

Example 1 The following is a legitimate program that defines the union of two relations P, Q (for the moment we use ad-hoc Prolog-like syntax):

union(P,Q)(X):-P(X). union(P,Q)(X):-Q(X).

However, each of these clauses violates Wadge's restriction:

Under the extensional approach, predicates can be understood declaratively in terms of extensional notions. For example, the program:

can be understood in a similar way as the well-known map function of Haskell. Moreover, since under the extensional approach predicates denote sets, two predicates that are true of the same arguments, are considered indistinguishable. So, for example, if we define two sorting predicates merge sort and quick sort it is guaranteed that any higher-order predicate will have the same behaviour whether it is given merge sort or quick sort as an argument. As mentioned by Wadge [1991] "extensionality means exactly that predicates are used as black boxes - and the "black box" concept is central to all kinds of engineering".

Another important advantage of this declarative approach to higher-order logic programming is that many techniques and ideas that have been successfully developed in the functional programming world (such as program transformations, optimizations, techniques for proving program correctness, and so on), could be transferred to the higher-order logic programming domain, opening in this way promising new research directions for logic programming as a whole.

3 An Intuitive Introduction

In this section we give an intuitive description of the semantic technique for positive higher-order logic programs proposed by Bezem [1999; 2001] and we outline how we use it when negation is added to programs. Given a positive program, the starting idea behind Bezem's approach is to take its "ground instantiation", in which we replace variables with well-typed terms constructed from syntactic entities that appear in the program. For example, consider the higher-order program:

q(a). q(b). p(Q):-Q(a). id(R)(X):-R(X).

In order to obtain the ground instantiation of this program, we consider each clause and replace each variable of the clause with a ground term that has the same type as the variable under consideration (the formal definition of this procedure will be given in Definition 9):

q(a). q(b). p(q):-q(a). id(q)(a):-q(a). id(q)(b):-q(b). p(id(q)):-id(q)(a). · · ·

One can now treat the new program as an infinite propositional one (i.e., each ground atom can be seen as a propositional variable). This implies that we can use the standard least fixed-point construction of classical logic programming in order to compute the set of atoms that should be taken as "true".

Bezem demonstrated that the least fixed-point semantics of the ground instantiation of every positive higher-order logic program of the language considered in [Bezem, 1999; 2001], is extensional in a sense that can be explained as follows. In our example, q and id(q) are equal since they are both true of exactly the constants a and b. Therefore, we expect that if p(q) is true then p(id(q)) is also true, because q and id(q) should be considered as indistinguishable.

We use the same idea with programs that include negation: the ground instantiation of such a program can be seen as a (possibly infinite) propositional program with negation. Therefore, we can compute its semantics in any standard way that exists for obtaining the meaning of such programs and then proceed to examine whether the chosen model is extensional in the sense of Bezem [1999; 2001]. As we are going to see in the subsequent sections, when the ground instantiation of the program is interpreted under the well-founded semantics, the semantics we obtain is not always extensional.

4 The Syntax of H

In this section we define the syntax of our language H. H uses a simple type systemwith two base types: o, the boolean domain, and ι, the domain of data objects. The composite types are partitioned into three classes: functional (assigned to function symbols), predicate (assigned to predicate symbols) and argument (assigned to parameters of predicates).

Definition 1 A type can either be functional, predicate, or argument, denoted by σ, π and ρ respectively and defined as:

We will use τ to denote an arbitrary type. The binary operator → is right-associative. It can be easily seen that every predicate type π can be written in the form ρ1 → · · · → ρn → o, n ≥ 0 (for n = 0 we assume that π = o).

Definition 2 The alphabet of H consists of the following: predicate variables of every predicate type π (denoted by capital letters such as Q, R, S, . . .); individual variables of type ι (denoted by capital letters such as X, Y, Z, . . .); predicate constants of every predicate type π (denoted by lowercase letters such as p, q, r, . . .); individual constants of type ι (denoted by lowercase letters such as a, b, c, . . .); function symbols of every functional type σ ̸= ι (denoted by lowercase letters such as f, g, h, . . .); the inverse implication constant ←; the negation constant ∼; the comma; and the left and right parentheses.

Arbitrary variables will usually be denoted by V and its subscripted versions.

Definition 3 The set of terms of H is defined as follows: every predicate variable (resp., predicate constant) of type π is a term of type π; every individual variable (resp., individual constant) of type ι is a term of type ι; if f is an n-ary function symbol and E1, . . . , En are terms of type ι then (f E1 · · · En) is a term of type ι; if E1 is a term of type ρ → π and E2 a term of type ρ then (E1 E2) is a term of type π.

Definition 4 The set of expressions of H is defined as follows: a term of type ρ is an expression of type ρ; if E is a term of type o then (∼E) is an expression of type o.

We will omit parentheses when no confusion arises. To denote that an expression E has type ρ we will often write E : ρ. We will write vars(E) to denote the set of all the variables in E. Expressions (respectively, terms) that have no variables will be referred to as ground expressions (respectively, ground terms). Terms of type o will be referred to as atoms and expressions of type o will be referred to as literals.

Definition 5 A clause of H is a formula p E1 · · · En ← L1, . . . , Lm, where p is a predicate constant of type ρ1 → · · · → ρn → o, E1, . . . , En are terms of types ρ1, . . . , ρn respectively, so that all Ei with ρi ̸= ι are distinct variables, and L1, . . . , Lm are literals. The term p E1 · · · En is called the head of the clause and the conjunction L1, . . . , Lm is its body. A program P of H is a finite set of clauses.

Example 2 The program below defines the subset relation over unary predicates:

subset S1 S2 ← ∼(nonsubset S1 S2) nonsubset S1 S2 ← (S1 X), ∼(S2 X)

The ground instantiation of a program is described by the following definitions:

Definition 6 A substitution θ is a finite set of the form {V1/E1, . . . , Vn/En} where the Vi's are different variables and each Ei is a term having the same type as Vi. The domain {V1, . . . , Vn} of θ is denoted by dom(θ). If all the terms E1, . . . , En are ground, θ is called a ground substitution.

Definition 7 Let θ be a substitution and E be an expression. Then, Eθ is an expression obtained from E as follows: Eθ = E if E is a predicate constant or individual constant; Vθ = θ(V) if V ∈ dom(θ), otherwise Vθ = V; (f E1 · · · En)θ = (f E1θ · · · Enθ); (E1 E2)θ = (E1θ E2θ); (∼E)θ = (∼Eθ). If θ is a ground substitution with vars(E) ⊆ dom(θ), then the ground expression Eθ is called a ground instance of E.

Definition 8 For a program P, we define the Herbrand universe for every argument type ρ, denoted by UP,ρ to be the set of all ground terms of type ρ that can be formed out of the individual constants, function symbols, and predicate constants in the program.

Definition 9 Let P be a program. A ground instance of a clause p E1 · · · En ← L1, . . . , Lm of P is a formula (p E1 · · · En)θ ← L1θ, . . . , Lmθ, where θ is a ground substitution whose domain is the set of all variables that appear in the clause, such that for every V ∈ dom(θ) with V : ρ, θ(V) ∈ UP,ρ. The ground instantiation of a program P, denoted by Gr(P), is the (possibly infinite) set that contains all the ground instances of the clauses of P.

5 The Semantics of H

In [Bezem, 1999; 2001] M. Bezem developed a semantics for higher-order logic programs that is a generalization of the familiar Herbrand-model semantics of classical (first-order) logic programs. As such, the approach proposes that the meaning of predicates and data objects is fixed across all (Herbrand) interpretations. Because of this, the following simplified definition of a higher-order interpretation is possible:

Definition 10 A (higher-order) Herbrand interpretation I of a program P is a function which assigns to each ground atom of UP,o, an element in a specified domain of truth values.

The truth domain used in [Bezem, 1999; 2001] is the traditional two-valued one, as only positive programs are studied. In our attempt to extend the well-founded semantics, in this paper we consider Herbrand interpretations with a threevalued truth domain, i.e. {false, 0, true}.

The concept of "Herbrand model" of a higher-order program can be defined as in classical logic programming.

Definition 11 Let P be a program and I be a Herbrand interpretation of P. We say I is a model of P if I(A) ≥ min{I(L1), . . . , I(Ln)} holds for every ground instance A ← L1, . . . , Lm of a clause of P.

Bezem's semantics is based on the observation that, given a positive higher-order program, the minimum model of its ground instantiation serves as a Herbrand interpretation for the program itself. We follow the same idea for programs with negation: we can use as an interpretation of a given higher-order program P, the model defined by any semantic approach that applies to its ground instantiation. It is trivial to see that any such model is also a Herbrand model of P.

In the following sections we investigate if the well-founded model [Gelder et al., 1991] enjoys the extensionality property, formally defined by Bezem [1999; 2001] through relations ∼=I,ρ over the set of ground expressions of a given type ρ and under a given interpretation I. These relations intuitively express extensional equality of type ρ, in the sense discussed in Section 3. The formal definition is as follows:

Definition 12 Let I be a Herbrand interpretation for a given program P. For every argument type ρ we define the relations ∼=I,ρ on UP,ρ as follows. Let E, E′ ∈ UP,ρ; then E ∼=I,ρ E′ if and only if: ρ = ι and E = E′ ; or ρ = o and I(E) = I(E′ ); or ρ = ρ′ → π and ED ∼=I,π E′ D′ for all D,D′ ∈ UP,ρ′ , such that D ∼=I,ρ′ D′ .

Generally, such relations are symmetric and transitive [Bezem, 1999; 2001] (i.e., partial equivalences). Whether they are moreover reflexive (i.e., full equivalences), depends on the specific interpretation, which leads to the notion of extensional interpretation:

Definition 13 Let P be a program and let I be a Herbrand interpretation of P. We say I is extensional if for all argument types ρ, ∼=I,ρ is reflexive, i.e. for all E ∈ UP,ρ, E ∼=I,ρ E.

For a more thorough and formal presentation of the notions discussed in this section, the reader may refer to the full version of the present paper [Rondogiannis and Symeonidou, 2017].

6 Non-Extensionality of theWell-Founded Model

In this section we demonstrate that the adaptation of Bezem's technique under the well-founded semantics does not in general preserve extensionality. In particular, we exhibit below a program that has a non-extensional well-founded model.

Example 3 Consider the higher-order program P:

w R ← ∼R

where the predicate variable Q is of type o → o and the predicate variable R is of type o. It is not hard to see that the predicates p : o → o and q : o → o represent the same relation, namely {(v, v) | v ∈ {false, 0, true}}.

Consider the predicate s : (o → o) → o. By taking the ground instances of the clauses involved, it is easy to see that the atom (s p), under the well-founded semantics, will be assigned the value false. On the other hand, (s q) is assigned the value 0, under the well-founded semantics, since the ground instances of the relevant clauses form a circular definition involving negation. In other words, p and q are extensionally equal, but (s p) and (s q) have different truth values.

The above discussion is based on intuitive arguments, but it is not hard to formalize it and obtain the following lemma:

Lemma 1 The well-founded model MP of the program of Example 3, is not extensional.

A question that arises is whether there exists a broad class of programs that are extensional under the well-founded semantics. The next section answers exactly this question.

7 Extensionality of Stratified Programs

In this section we argue that the well-founded model of a stratified higher-order program [Rondogiannis and Symeonidou, 2018] enjoys the extensionality property. In the following definition, a predicate type π is understood to be greater than a second predicate type π′ , if π is of the form ρ1 → · · · → ρn → π′ , where n ≥ 1.

Definition 14 A program P is called stratified if and only if it is possible to decompose the set of all predicate constants that appear in P into a finite number r of disjoint sets (called strata) S1, S2, . . . , Sr, such that for every clause H ← A1, . . . , Am,∼B1, . . . ,∼Bn in P, where the predicate constant of H is p, we have:

1. for every i ≤ m, if Ai is a term that starts with a predicate constant q, then stratum(q) ≤ stratum(p);
2. for every i ≤ m, if Ai is a term that starts with a predicate variable Q, then for all predicate constants q that appear in P, such that the type of q is greater than or equal to the type of Q, it holds stratum(q) ≤ stratum(p);
3. for every i ≤ n, if Bi starts with a predicate constant q, then stratum(q) < stratum(p);
4. for every i ≤ n, if Bi starts with a predicate variable Q, then for all predicate constants q that appear in P, such that the type of q is greater than or equal to the type of Q, it holds stratum(q) < stratum(p);

where stratum(r) = i if r belongs to Si.

Evidently, the stratification for classical logic programs [Apt et al., 1988] is a special case of the above definition.

Example 4 It is straightforward to see that the program:

is stratified. However, it is easy to check that the program:

is not stratified because if the term (q a) is substituted for Q we get a circularity through negation. The type of q is ι → ι → o and it is greater than the type of Q which is ι → o.

As it turns out, stratified higher-order logic programs have an extensional two-valued well-founded model.

Theorem 1 The well-founded model MP of a stratified program P is extensional and does not assign the value 0.

Despite the above result, we have not yet been able to clarify whether the class of locally stratified higher-order logic programs (see Rondogiannis and Symeonidou [2018]) is well-behaved with respect to extensionality, or not.

8 The Restrictions of 3-Valued Approaches

In this section we indicate that in order to achieve an extensional three-valued semantics for higher-order logic programs with negation, one has to make some strong assumptions regarding the behaviour of negation in such programs.

Consider again the program of Section 6. Under the infinite-valued adaptation of Bezem's approach by Rondogiannis and Symeonidou [2018] and also under the domain-theoretic infinite-valued approach by Charalambidis et al. [2014], the semantics of that program is extensional. Both approaches differentiate the meaning of p from the meaning of q, which correspond to different infinite-valued relations. Therefore, it is not a surprise that in both cases, the atoms (s p) and (s q) have different truth values.

Assume now that we want to devise an (alternative to the one presented in this paper) extensional three-valued semantics for H programs. Under such a semantics, it seems reasonable to assume that p and q would correspond to the same three-valued relation, namely {(v, v) | v ∈ {false, 0, true}}.

Notice however that p and q are expected to have a different operational behaviour. In particular, given the program:

we expect the atom (s p) to have the value false (due to the circularity that occurs when we try to evaluate it), while given the program:

w R ← ∼R

we expect the atom (s q) to have the value 0 due to the circularity through negation. At first sight, the above discussion seems to suggest that a three-valued extensional semantics for all higher-order logic programs with negation is not possible.

However, the above discussion is based mainly on our experience regarding the behaviour of first-order logic programs with negation. One could advocate a semantics under which (s q) will also return the value false, arguing that the definition of q uses two negations which cancel each other. This cancellation of double negations is not an entirely new idea; for example, for certain extended propositional programs, the semantics based on approximation fixpoint theory has the same effect (see for example Denecker et al. [2012][page 185, Example 1]). We have recently developed such an extensional three-valued semantics for higher-order logic programs with negation, using an approach based on approximation fixpoint theory in Charalambidis et al. [2018]. It is an interesting project for future research to evaluate the merits of each approach and the relationships between them.