{'fraction_non_alphanumeric': 0.056046983758700694, 'fraction_numerical': 0.011492169373549884, 'mean_word_length': 3.929324517512509, 'pattern_counts': {'":': 0, '<': 16, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 46, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Intricacies of 3-Valued Extensional Semantics for Higher-Order Logic Programs

In (Bezem 1999; Bezem 2001), M. Bezem defined an extensional semantics for positive higher-order logic programs. Recently, it was demonstrated in (Rondogiannis and Symeonidou 2016) that Bezem's technique can be extended to higher-order logic programs with negation, retaining its extensional properties, provided that it is interpreted under a logic with an infinite number of truth values. In (Rondogiannis and Symeonidou 2017) it was also demonstrated that Bezem's technique, when extended under the stable model semantics, does not in general lead to extensional stable models. In this paper we consider the problem of extending Bezem's technique under the well-founded semantics. We demonstrate that the well-founded extension fails to retain extensionality in the general case. On the positive side, we demonstrate that for stratified higher-order logic programs, extensionality is indeed achieved. We analyze the reasons of the failure of extensionality in the general case, arguing that a three-valued setting can not distinguish between certain predicates that appear to have a different behaviour inside a program context, but which happen to be identical as three-valued relations. The paper is under consideration for acceptance in TPLP.


Introduction
Recent research (Wadge 1991;Bezem 1999;Bezem 2001;Kountouriotis et al. 2005;Charalambidis et al. 2013;Rondogiannis and Symeonidou 2016;Charalambidis et al. 2017) has investigated the possibility of providing extensional semantics to higher-order logic programming. Under an extensional semantics, predicates denote sets, and therefore one can use standard set theory in order to understand programs and reason about them. Of course, extensionality comes with a price: to obtain an extensional semantics, one usually has to consider higher-order logic programs with a relatively restricted syntax. Actually this is a main difference between the extensional and the more traditional intensional approaches to higher-order logic programming such as (Miller and Nadathur 2012;Chen et al. 1993): the latter languages have a richer syntax and expressive capabilities but they are not usually amenable to a standard set-theoretic semantics.
There exist two main research directions for providing extensional semantics to higherorder logic programs. The first one (Wadge 1991;Kountouriotis et al. 2005;Charalambidis et al. 2013;Charalambidis et al. 2014) has been developed using domain-theoretic tools, and resembles the techniques for assigning denotational semantics to functional languages. The second approach (Bezem 1999;Bezem 2001; Rondogiannis and Symeonidou 2016) relies on the syntactic entities that exist in a program, and is based on processing the ground instantiation of the program. The two research directions are not unrelated: it has recently been shown (Charalambidis et al. 2017) that for a broad class of positive programs, the two approaches coincide with respect to ground atoms.
In this paper we focus exclusively on the second extensional approach. This approach was initially proposed in (Bezem 1999;Bezem 2001) for positive (i.e., negationless) higherorder logic programs. Recently, it was demonstrated in (Rondogiannis and Symeonidou 2016) that by combining the technique of (Bezem 1999;Bezem 2001) with the infinitevalued semantics of (Rondogiannis and Wadge 2005), we obtain an extensional semantics for higher-order logic programs with negation. In the extended version (Rondogiannis and Symeonidou 2017) of the paper (Rondogiannis and Symeonidou 2016) a negative and unexpected result is established: by combining the technique of (Bezem 1999;Bezem 2001) 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 2016) whether the combination of the technique of (Bezem 1999;Bezem 2001) 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.
We demonstrate that the well-founded extension of Bezem's technique fails to retain extensionality in the general case. On the positive side, we prove that for stratified higher-order logic programs, extensionality is indeed achieved. We analyze the reasons of the failure of extensionality in the general case, and claim that this is not an inherent shortcoming of Bezem's approach but a more general phenomenon. In particular we argue that restricting attention to three-valued logic appears to "throw away too much information" and makes predicates that are expected to have different behaviours, appear as identical three-valued relations. The main contributions of the present paper can be summarized as follows: • We demonstrate that the well-founded adaptation of Bezem's technique, does not in general lead to an extensional model. In particular, we exhibit a program with a non-extensional well-founded model. This result, despite its negative flavor, indicates that the addition of negation to higher-order logic programming is not such a straightforward task as it was possibly initially anticipated. Notice that, as it was recently demonstrated in (Rondogiannis and Symeonidou 2017), the stable model adaptation of Bezem's technique is also non-extensional in general. • Despite the above negative result, we prove that the well-founded adaptation of Bezem's technique gives an extensional two-valued model in the case of stratified programs. This result affirms the importance and the well-behaved 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 (arguably) non-standard assumptions regarding the behaviour of negation.
The rest of the paper is organized as follows. Section 2 introduces the basic notions and the advantages of the extensional approach to the semantics of higher-order logic programming. Section 3 presents in an intuitive way the main concepts and results of the paper. Section 4 introduces the syntax and Section 5 the semantics of our source language. Section 6 demonstrates that Bezem's approach is not extensional under the well-founded semantics. In Section 7 it is established that stratified programs have an extensional, two-valued, well-founded semantics. Section 8 concludes by discussing the restrictions that any reasonable three-valued semantics would have with respect to extensionality. The proofs of all results are given in the corresponding appendices.

Extensional Higher-Order Logic Programming
In (Wadge 1991) W. W. Wadge suggested that if we appropriately restrict the syntax of higher-order logic programming, then we can obtain languages that can be assigned a standard denotational semantics in which predicates denote sets. In other words, for such syntactically restricted languages one can apply traditional domain-theoretic notions and tools that have been used extensively in higher-order functional programming. The most crucial syntactic restriction imposed by Wadge (and also later independently by M. Bezem (Bezem 1999)), 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, the following program does not satisfy Wadge's restriction: q(a). r(q).
because the predicate constant q appears as an argument in the head of a rule. Similarly, the program: is problematic because the predicate variable Q is used twice in the head of the rule.
The advantages of extensionality were identified by Wadge and Bezem in their respective papers. First of all, under the extensional approach, program 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 that have the same type, say τ , and that perform the same task (possibly with different efficiency), it is guaranteed that any predicate which operates on relations of type τ will have the same behaviour whether it is given merge sort or quick sort as an argument. As mentioned in (Wadge 1991) "extensionality means exactly that predicates are used as black boxes -and the "black box" concept is central to all kinds of engineering". It is this property that makes extensional languages so appealing (and is actually one of the greatest assets of traditional functional programming).
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 higherorder logic programming domain, opening in this way promising new research directions for logic programming as a whole.

An Intuitive Overview of the Proposed Approach
In this paper we consider the semantic technique for positive higher-order logic programs proposed in (Bezem 1999;Bezem 2001) and we investigate whether it can be applied in order to provide an extensional well-founded semantics for higher-order logic programs with negation in clause bodies. In this section we give an intuitive description of Bezem's idea and we outline how we use it when negation is added to programs.
Given a positive higher-order logic program, the starting idea behind Bezem's approach is to take its "ground instantiation", in which we replace variables with well-typed terms that can be created using syntactic entities that appear in the program. For example, consider the higher-order program below: 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 8). In this way we obtain the following infinite program: 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 (see for example (Lloyd 1987)) in order to compute the set of atoms that should be taken as "true". In our example, the least fixed-point will contain atoms such as q(a), q(b), p(q), id(q)(a), id(q)(b), p(id(q)), and so on.
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;Bezem 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 (for example) if p(q) is true then p(id(q)) is also true, because q and id(q) should be considered as indistinguishable. This property of "indistinguishability" is formally defined in (Bezem 1999;Bezem 2001) and it is demonstrated that it holds in the least fixed-point of the immediate consequence operator of the ground instantiation of every program that abides to the simple extensionality syntactic restriction given in the previous section (and formally described by Definition 5 later in the paper).
The key idea behind extending Bezem's semantics in order to apply to higher-order logic programs with negation, is straightforward to state: given such a program, we first take its ground instantiation. The resulting program is a (possibly infinite) propositional program with negation and therefore we can compute its semantics in any standard way that exists for obtaining the meaning of such programs. For example, one could use the well-founded semantics (Gelder et al. 1991), the stable model semantics (Gelfond and Lifschitz 1988), or the infinite-valued semantics (Rondogiannis and Wadge 2005), and then proceed to examine whether the well-founded model (respectively, each stable model, or the minimum infinite-valued model) is extensional in the sense of (Bezem 1999;Bezem 2001

) (informally described above).
An open problem posed in (Rondogiannis and Symeonidou 2017) was whether Bezem's technique, under the well-founded semantics, always leads to an extensional well-founded model. As we are going to see in the subsequent sections, this is not the case. In particular, we exhibit a program containing three predicates s, p and q, such that p and q are extensionally equal under the well-founded semantics, but s(p) and s(q) have a different truth value. On the positive side, we prove that every stratified higher-order logic program with negation has an extensional well-founded model. In this sense, we identify a broad class of programs that are well-behaved in terms of extensionality.

The Syntax of H
In this section we define the syntax of the language H that we use throughout the paper. H is based on a simple type system with 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 (either functional, predicate, or argument). As usual, the binary operator → is right-associative. A functional type that is different than ι will often be written in the form ι n → ι, n ≥ 1. Moreover, 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). We proceed by defining the syntax of H:

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; the left and right parentheses; and the equality constant ≈ for comparing terms of type ι.
Arbitrary variables will be usually denoted by V and its subscripted versions.

Definition 3
The set of terms of H is defined as follows: every predicate variable (respectively, predicate constant) of type π is a term of type π; every individual variable (respectively, individual constant) of type ι is a term of type ι; if f is an n-ary function symbol and E 1 , . . . , E n are terms of type ι then (f E 1 · · · E n ) is a term of type ι; if E 1 is a term of type ρ → π and E 2 a term of type ρ then (E 1 E 2 ) 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; if E 1 and E 2 are terms of type ι, then (E 1 ≈ E 2 ) 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. Expressions of type o that do not contain negation, i.e. expressions of the form (E 1 ≈ E 2 ) or atoms, will be called positive literals, while expressions of the form (∼E) will be called negative literals. A literal is either a positive literal or a negative literal.

Definition 5
. . , V n are distinct variables of types ρ 1 , . . . , ρ n respectively and L 1 , . . . , L m are literals. The term p V 1 · · · V n is called the head of the clause, the variables V 1 , . . . , V n are the formal parameters of the clause and the conjunction L 1 , . . . , L m is its body. A program P of H is a finite set of clauses.

Example 3
For a more "real-life" higher-order logic program with negation, assume that we have a unary predicate movie M and a binary predicate ranking M R which returns the ranking R of a given movie M. Consider also the following first-order predicate that defines a preference over movies based on their ranking: prefer M1 M2 ← movie M1, movie M2, ranking M1 R1, ranking M2 R2, R1>R2.
The following higher-order predicate winnow (see for example (Chomicki 2003)) can be used to select all the "best" tuples T out of a given relation R based on a preference relation P: winnow P R T ← R T, ∼(bypassed P R T). bypassed P R T ← R T1, P T1 T. Intuitively, winnow returns all the tuples T of the relation R such that there does not exist any tuple T1 in the relation R that is better from T with respect to the preference relation P. For example, if we ask the query ?-winnow prefer movie T. we expect as answers all those movies that have the highest possible ranking. Notice that since winnow is a higher-order predicate, it can be invoked with different arguments; for example, it can be used to select out of a book relation, all those books that have the lowest possible price, or out of a flight relation all those flights that go to London, and so on.
The ground instantiation of a program is described by the following definitions:

Definition 6
A substitution θ is a finite set of the form {V 1 /E 1 , . . . , V n /E n } where the V i 's are different variables and each E i is a term having the same type as V i . We write dom(θ) to denote the domain {V 1 , . . . , V n } of θ. If all the terms E 1 , . . . , E n 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: If θ is a ground substitution such that vars(E) ⊆ dom(θ), then the ground expression Eθ is called a ground instance of E.

Definition 8
Let P be a program. A ground instance of a clause p V 1 · · · V n ← L 1 , . . . , L m of P is a formula (p V 1 · · · V n )θ ← L 1 θ, . . . , L m θ, 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) is a ground term of type ρ that has been formed with predicate constants, function symbols, and individual constants that appear in P. 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.

The Semantics of H
In (Bezem 1999;Bezem 2001) M. Bezem developed a semantics for higher-order logic programs which generalizes the familiar Herbrand-model semantics of classical (firstorder) logic programs. In this section we extend Bezem's semantics to the case of higherorder logic programs with negation.
In order to interpret the programs of H, we need to specify the semantic domains in which the expressions of each type τ are assigned their meanings. The following definition is a slightly modified version of the corresponding definition of (Bezem 1999;Bezem 2001) and it implies that the expressions of predicate types should be understood as representing functions. We use [S 1 → S 2 ] to denote the set of (possibly partial) functions from a set S 1 to a set S 2 . The possibility to have a partial function arises due to a technicality which is explained in the remark just above Definition 11.

Definition 9
A functional type structure S for H consists of two non-empty sets D and A together with an assignment τ to each type τ of H, so that the following are satisfied: Given a functional type structure S, any function v : o → {false, 0, true} will be called a three-valued valuation function (or simply valuation function) for S. We will use the term two-valued valuation functions to distinguish the subset of valuation functions which do not assign the value 0 to any element of o , i.e. the functions v : o → {false, true}.
It is customary in the study of the semantics of logic programming languages to restrict attention to Herbrand interpretations. Given a program P, a Hebrand interpretation is one that has as its underlying universe the so-called Herbrand universe of P:

Definition 10
For a program P, we define the Herbrand universe for every argument type ρ, denoted by U P,ρ 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. Moreover, we define U + P,o to be the set of all ground expressions of type o, that can be formed out of the above symbols, i.e. the set U + (Bezem 1999;Bezem 2001), we take D and A in Definition 9 to be equal to U P,ι and U + P,o respectively. Then, for each predicate type ρ → π, each element of U P,ρ→π can be perceived as a function mapping elements of ρ to elements of π , through syntactic application mapping. That is, E ∈ U P,ρ→π can be viewed as the function mapping each term E ′ ∈ U P,ρ to the term (E E ′ ) ∈ U P,π . Similarly, every n-ary function symbol f appearing in P can be viewed as the function mapping each element (E 1 , . . . , E n ) ∈ U n P,ι to the term (f E 1 · · · E n ) ∈ U P,ι .
Remark: There is a small technicality here which we need to clarify. In the case where ρ = o, E ∈ U P,o→π is a partial function because it maps elements of U P,o (and not of U + P,o ) to elements of U P,π ; this is due to the fact that our syntax does not allow an expression of type o → π to take as argument an expression of the form (E 1 ≈ E 2 ) nor of the form (∼E). In all other cases (i.e., when ρ = o), E represents a total function.

Definition 11
A (three-valued) Herbrand interpretation I of a program P consists of: 1. the functional type structure S P , such that D = U P,ι , A = U + P,o and ρ → π = U P,ρ→π for every predicate type ρ → π, called the Herbrand type structure of P; 2. the assignment to each individual constant c in P, of the element I(c) = c; to each predicate constant p in P, of the element I(p) = p; to each function symbol f in P, of the element I(f) = f; 3. a valuation function v I (·) for S P , assigning to each element of U + P,o an element in {false, 0, true}, while satisfying the following: We call v I (·) the valuation function of I and omit the reference to S P , since the latter is common to all Herbrand interpretations of a program. In fact, individual Herbrand interpretations are only set apart by their valuation functions. If the valuation function v I (·) is two-valued, then I will also be called a two-valued Herbrand interpretation.

Definition 12
A Herbrand state (or simply state) s of a program P is a function that assigns to each variable V of type ρ an element of U P,ρ .
Given a Herbrand interpretation I and state s, we can define the semantics of expressions with respect to I and s.

Definition 13
Let P be a program. Also, let I be a Herbrand interpretation and s a Herbrand state of P. Then the semantics of expressions with respect to I and s is defined as follows: • c I,s = I(c) = c, for every individual constant c; • p I,s = I(p) = p, for every predicate constant p; It is easy to see that the semantic function · is well defined, in the sense that, for every Herbrand state s and every expression E of every argument type ρ, we have E I,s ∈ ρ . Note that this makes E I,s a ground expression of the language. Also note, that if E is a ground expression then E I,s = E; therefore, if E is a ground literal, we can write v I (E) instead of v I ( E I,s ). Stretching this abuse of notation a little further, we can extend a valuation function to assign truth values to ground conjunctions of literals; this allows us to define the concept of Herbrand models for our higher-order programs in the same way as in classical logic programming.

Definition 14
Let P be a program and I be a Herbrand interpretation of P. We define v I (L 1 , . . . , L n ) = min{v I (L 1 ), . . . , v I (L n )} for all L 1 , . . . , L n ∈ U + P,o . Moreover, we say I is a model of P if v I ( A I,s ) ≥ v I ( L 1 I,s , . . . , L m I,s ) holds for every clause A ← L 1 , . . . , L m and every Herbrand state s of P.
Bezem's semantics is based on the observation that, given a positive higher-order program, we can use the minimum model of its ground instantiation as a (two-valued) valuation function defining a Herbrand interpretation for the initial program itself. We follow the same idea but now for programs with negation: we can use as the valuation function of a given H program, the Herbrand model defined by any semantic approach that applies to its ground instantiation. Actually, we demonstrate (see Theorem 1 below) that any interpretation I of the higher-order program P will be a minimal model of P, if its chosen valuation function is a minimal model of Gr(P).
We consider two different notions of minimality, based on the truth ordering ≤ and the Fitting ordering of truth values, respectively. Recall that ≤ is the partial order defined by false ≤ 0 ≤ true, while is the partial order defined by 0 false and 0 true.

Definition 15
If I and J are two Herbrand interpretations of a higher-order program P, we say I ≤ J (respectively, If M is a model of P then we say it is ≤-minimal (resp., -minimal) if there does not exist a different model N of P, such that N ≤ M (resp., N M ).

Theorem 1
Let P be a program and let Gr(P) be its ground instantiation. Also let M be a partial interpretation 1 of Gr(P) and let M be the Herbrand interpretation of P, such that v M (A) = M (A) for every A ∈ U P,o . Then, M is a Herbrand model of P if and only if M is a model of Gr(P). Moreover, M is ≤-minimal (respectively, -minimal) if and only if M is ≤-minimal (respectively, -minimal).
As an application of the above developments we define two special Herbrand interpretations of higher-order programs, employing the well-known perfect model (Apt et al. 1988;Gelder 1989) and well-founded model (Gelder et al. 1991) of the ground instantiation of a program, as valuation functions.

Definition 16
Let P be a program and let Gr(P) be the ground instantiation of P. Also, let N Gr(P) be the perfect model 1 (if this exists) and M Gr(P) be the well-founded model 1 of Gr(P). We define N P to be the two-valued Herbrand interpretation of P such that v N P (A) = N Gr(P) (A) for every A ∈ U P,o . Similarly, we define M P to be the three-valued Herbrand interpretation of P such that v M P (A) = M Gr(P) (A) for every A ∈ U P,o .
Clearly, by Theorem 1, N P (if it exists) is a two-valued minimal model and M P is a three-valued minimal model of P. In the following sections we investigate their suitability for providing extensional semantics for H programs. In particular, we examine if each of them enjoys the extensionality property, formally defined (Bezem 1999;Bezem 2001) through relations ∼ =v,τ over the set of expressions of a given type τ and under a given valuation function v. These relations intuitively express extensional equality of type τ , in the sense discussed in Section 3. For the purposes of this paper only extensional equality of argument types will be needed, for which the formal definition is as follows:

Definition 17
Let S be a functional type structure and v be a valuation function for S. For every argument type ρ we define the relations ∼ =v,ρ on ρ as follows: Let d, d ′ ∈ ρ ; then d ∼ =v,ρ d ′ if and only if 1. ρ = ι and d = d ′ , or 2. ρ = o and v(d) = v(d ′ ), or 3. ρ = ρ ′ → π and d e ∼ =v,π d ′ e ′ for all e, e ′ ∈ ρ ′ , such that e ∼ =v,ρ ′ e ′ and d e, d ′ e ′ are both defined.
The above discussion leads to the notion of extensional interpretation:

Definition 18
Let P be a program and let I be a Herbrand interpretation of P with valuation function v I . We say I is extensional if for all argument types ρ the relations ∼ =v I ,ρ are reflexive, i.e. for all E ∈ ρ , it holds that E ∼ =v I ,ρ E.
The above notion will be extensively used in the following two sections.

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

Example 4
Consider the higher-order program P: where the predicate variable Q is of type o → o and the predicate variable R is of type o. Before stating formally the non-extensionality result, certain explanations at an intuitive level are in order. Consider first the predicate p of type o → o. One can view p as representing the identity relation on truth values, i.e., as the relation It is not hard to see that the predicate q of type o → o, represents exactly the same relation. However, the definition of q involves two applications of negation, while p is defined directly (without the use of negation). Consider now the predicate s of type (o → o) → o which can take as a parameter either p or q. When s takes p as a parameter, we get the following two clauses (by substituting p for Q and (s p) for R in the above program): A recursive definition of this form assigns to (s p), under the well-founded semantics, the value false. Consider on the other hand the case where s takes q as a parameter. Then, by doing analogous substitutions, we get the following three clauses: Under the well-founded semantics, (s q) is assigned the value 0. In other words, despite the fact that p and q are extensionally equal (see also below), (s p) and (s q) have different truth values. In conclusion, the adaptation of the well-founded semantics under Bezem's technique does not lead to an extensional model in all cases.
Of course, the above discussion is based on intuitive arguments, but it is not hard to formalize it. The main difficulty lies in establishing that p and q are extensionally equal because the above program has an infinite ground instantiation Gr(P) (see Appendix B). The following lemma, whose detailed proof is given in Appendix B, suggests that M P , i.e. the Herbrand interpretation of our example program P defined by using the well-founded model M Gr(P) of Gr(P) as the valuation function, is not extensional.

Lemma 1
The Herbrand interpretation M P of the program of Example 4 is not extensional.
The consequences that the above lemma has for the investigation of alternative extensional three-valued semantics for higher-order logic programs with negation, will be discussed in Section 8.
A natural question that arises is whether there exists a broad and useful class of programs that are extensional under the well-founded semantics. The next section answers exactly this question.

Extensionality of Stratified Programs
In this section we present the notion of stratified higher-order programs, originally introduced in (Rondogiannis and Symeonidou 2016), and argue that the well-founded model of such a program enjoys the extensionality property defined in Section 5. 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 19 The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP 13
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) S 1 , S 2 , . . . , S r , such that for every clause H ← A 1 , . . . , A m , ∼B 1 , . . . , ∼B n in P, where the predicate constant of H is p, we have: 1. for every i ≤ m, if A i is a term that starts with a predicate constant q, then stratum(q) ≤ stratum(p); 2. for every i ≤ m, if A i 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 B i starts with a predicate constant q, then stratum(q) < stratum(p); 4. for every i ≤ n, if B i 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 the predicate constant r belongs to S i .
One may easily see that the stratification for classical logic programs (Apt et al. 1988;Gelder 1989) is a special case of the above definition.

Example 5
It is straightforward to see that the program: is stratified. However, it can easily be checked that the program: is not stratified because if the term (q a) is substituted for Q we get a circularity through negation. Notice that 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 well-founded model. The proof of the following theorem can be found in Appendix C.

Theorem 2
The well-founded model M P of a stratified program P is extensional.
Despite the fact that stratified programs lead to an extensional well-founded model, we have not been able to verify that the same property holds for locally stratified higherorder logic programs (for a formal definition of the notion of local stratification for H programs, please see (Rondogiannis and Symeonidou 2016)). On the other hand, our attempts to find a locally stratified program with a non-extensional well-founded model have also been unsuccessful, and therefore it is not at present clear to us whether this class of programs is well-behaved with respect to extensionality, or not.

The Restrictions of Three-Valued Approaches
In this section we re-examine the counterexample of Section 6 but now from a broader perspective. In particular, we indicate that in order to achieve an extensional threevalued semantics for higher-order logic programs with negation, one has to make some (arguably) non-standard assumptions regarding the behaviour of negation in such programs. On the other hand, a logic with an infinite number of truth values appears to be a more appropriate vehicle for achieving extensionality. In the following discussion, we assume some basic familiarity with the main intuition behind the approaches described in (Rondogiannis and Symeonidou 2016) and in (Charalambidis et al. 2014).
Consider again the program of Section 6. Under the infinite-valued adaptation of Bezem's approach given in (Rondogiannis and Symeonidou 2016) and also under the domain-theoretic infinite-valued approach of (Charalambidis et al. 2014), the semantics of that program is extensional. The reason is that both of these approaches differentiate the meaning of p from the meaning of q. The truth domain in both approaches is the set: where F α and T α represent different degrees of truth and falsity, and Ω is the first uncountable ordinal. Under this truth domain, predicate p (intuitively) corresponds to the infinite-valued relation: while predicate q corresponds to the relation: Obviously, the relations p and q are different as sets and therefore it is not a surprise that under both the semantics of (Rondogiannis and Symeonidou 2016) and (Charalambidis et al. 2014), the atoms (s p) and (s q) have different truth values. Notice, however, that if we collapse p and q in three-valued logic (i.e., if we map each F α to false, each T α to true, and 0 to 0), the collapsed relations become identical.
Assume now that 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 from a logic programming perspective, p and q are expected to have a different operational behaviour when they appear inside a program. In particular, given the program: we expect the atom (s p) to have the value false (due to the circularity that occurs if we try to evaluate it), while given the program: we expect the atom (s q) to have the value 0 due to the circularity through negation.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP 15
At first sight, the above discussion seems to suggest that there is no way we can have a three-valued extensional semantics for all higher-order logic programs with negation.
However, the above discussion is based mainly on our experience regarding the behaviour of first-order logic programs with negation. One could argue that we could devise a semantics under which (s q) will also return the value false. One possible justification for such a semantics would be that the definition of q uses two negations which cancel each other, and therefore we should actually expect q to behave exactly like p when it appears inside a program. Despite the fact that such a proposal seems somewhat unintuitive to us, we can not exclude it as a possibility. It is worth noting that such cancellations of double negations appear in certain semantic approaches to negation. For example, for certain extended propositional programs, the semantics based on approximation fixpoint theory has the effect of canceling double negations (see for example (Denecker et al. 2012)[page 185, Example 1]). It is possible that higher-order logic programs with negation behave similarly to extended propositional programs, and it is conceivable that one could construct an extensional three-valued semantics for all higher-order logic programs with negation, using an approach based on approximation fixpoint theory. This research direction certainly deserves further investigation.
It is our belief however that the most rigorous approach to extensionality for higherorder logic programs with negation, is through the use of the infinite-valued approach. It is worth noting that recently, some advantages of the infinite-valued approach versus the well-founded one, were identified in a different context. More specifically, as it was recently demonstrated in (Ésik 2015; Carayol andÉsik 2016), the infinite-valued approach satisfies all identities of iteration theories (Bloom andÉsik 1993), while the well-founded semantics does not. Since iteration theories (intuitively) provide an abstract framework for the evaluation of the merits of various semantic approaches for languages that involve recursion, the results just mentioned give an extra incentive for the further study and use of the infinite-valued approach.
L i are called literals, negative if they have negation and positive otherwise. As hinted in Section 3, we need to consider propositional programs with a possibly countably infinite number of clauses, as this is the case with the ground instantiation of a higher-order program. Moreover, we must allow a positive literal L i to also be one of the constants true and false. The reason for this is that in the ground instantiation of an H program, there may exist ground expressions of the form (E 1 ≈ E 2 ) in the bodies of clauses. These have specific meanings under the semantics of Section 5 and can not be treated as propositional variables. In the case where the two expressions E 1 and E 2 are syntactically identical, the expression (E 1 ≈ E 2 ) will be treated as the constant true (i.e., it is assumed that I((E 1 ≈ E 2 )) = true for every interpretation I of the ground instantiation), and otherwise as the constant false.
We use, throughout all sections of the Appendix, the standard representation of partial interpretations of propositional programs by T, F , where T and F are disjoint subsets of the Herbrand base B P of a propositional program P (i.e., the set of propositional variables appearing in P) denoting the sets of propositional variables considered to be true and false, respectively, in the interpretation. Naturally, T, F is a total interpretation if The truth ordering ≤ and Fitting ordering of interpretations can be defined in two equivalent ways:

Definition 20
If I = T, F and I ′ = T ′ , F ′ are two partial interpretations of a propositional program P then we say that I ≤ I ′ if T ⊆ T ′ and F ′ ⊆ F , or, equivalently, if I(p) ≤ I ′ (p) for every propositional variable p of P. Moreover, we say that I I ′ if T ⊆ T ′ and F ⊆ F ′ , or, equivalently, if I(p) I ′ (p) for every propositional variable p of P.
A model M of a propositional program is as usual considered to be ≤-minimal (respectively, -minimal) if there does not exist a different model N of P, such that N ≤ M (respectively, N M ).

Theorem 1
Let P be a program and let Gr(P) be its ground instantiation. Also let M be a partial interpretation of Gr(P) and let M be the Herbrand interpretation of P, such that v M (A) = M (A) for every A ∈ U P,o . Then, M is a Herbrand model of P if and only if M is a model of Gr(P). Moreover, M is ≤-minimal (respectively, -minimal) if and only if M is ≤minimal (respectively, -minimal).

Proof
Step 1 M is a model of Gr(P) ⇒ M is a Herbrand model of P: For every Herbrand state s of P there exists a ground substitution θ such that θ(V) = s(V), and therefore s(V) = θ(V) M,s ′ , for all states s ′ and variables V in P. Also, for every clause A ← L 1 , . . . , L m in P there exists a respective ground instance Aθ ← L 1 θ, . . . , L m θ in Gr(P).
As M is a model of Gr ( Step 2 M is a Herbrand model of P ⇒ M is a model of Gr(P): Every clause in Gr(P) is a ground instance of a clause A ← L 1 , . . . , L m in P and is therefore of the form Aθ ← L 1 θ, . . . , L m θ for some ground substitution θ. Consider a Herbrand state s, such that s(V) = θ(V) for every variable V in P. Because M is a model of P Step 3 M is minimal ⇒ M is minimal: Assume there exists a model N of P, distinct from M, such that N ≤ M (respectively, N M). Then we can construct an interpretation N for Gr(P) such that for every ground atom A, for at least one ground atom B. As we showed in Step 2, the fact that N is a model of P implies that N is a model of Gr(P), which is of course a contradiction, since M is a ≤-minimal (respectively, -minimal) model of Gr(P). Therefore, M must be a ≤-minimal (respectively, -minimal) model of P.
Step 4 M is minimal ⇒ M is minimal: By the reverse of the argument used in Step 1, the fact that N is a model of Gr(P) implies that N is a model of P, which is of course a contradiction, since M is a ≤-minimal (respectively, -minimal) model of P. Therefore, M must be a ≤-minimal (respectively, -minimal) model of Gr(P).

Appendix B Proof of Lemma 1
For the proof of Lemma 1, which we present in this appendix, we rely on the method of (Przymusinska and Przymusinski 1990) for the construction of the well-founded model. We first give the necessary definitions from (Przymusinska and Przymusinski 1990).

Definition 21
Let P be a propositional program and let J be an interpretation of P. The operator Θ J (·) on the set of interpretations of P is defined as follows: for every interpretation I and every propositional variable p of P, M Gr(P) (s p) = M Gr(P) (s q) and this should be obvious to the reader who is familiar with the well-founded model semantics; however, for reasons of completeness, we present a formal argument in the second part of this proof. In the same sections, we claimed that this is despite the fact that p ∼ =M Gr(P) ,o→o q, which we will immediately proceed to prove. Of course, by Definitions 17 and 18, the facts that M Gr(P) (s p) = M Gr(P) (s q) and p ∼ =M Gr(P) ,o→o q, render M P not extensional. First, we show that p ∼ =M Gr(P) ,o→o q, i.e. that for all A, A ′ ∈ U P,o such that A ∼ =M Gr(P) ,o A ′ , p A ∼ =M Gr(P) ,o q A ′ holds. By definition M Gr(P) is a fixed-point of the operator Θ M Gr(P) (·), therefore for any ground atom B we have that M Gr(P) (B) equals to true, if there exists a clause B ← L 1 , . . . , L n in Gr(P), such that M Gr(P) (L i ) = true for all i ≤ n; it equals to false if for every clause B ← L 1 , . . . , L n in Gr(P), we have that M Gr(P) (L i ) = false for at least one i ≤ n; and it equals to 0 otherwise. Observe that there exists only one clause in Gr(P) such that p A is the head of the clause, in particular it is the ground instance p A ← A of the clause p R ← R of P. This suggests that M Gr(P) (p A) = M Gr(P) (A) (1). Similarly, the ground instance q A ′ ← ∼(w A ′ ) of the clause q R ← ∼(w R) is the only clause in Gr(P) with q A ′ as its head atom and from this we can infer that M Gr(P) (q A ′ ) = M Gr(P) (∼(w A ′ )) = ¬M Gr(P) (w A ′ ) (2). Finally, the only clause in Gr(P), such that w A ′ is the head of the clause, is the ground instance w A ′ ← ∼A ′ of the clause w R ← ∼R of P, which implies that M Gr(P) (w A ′ ) = M Gr(P) (∼A ′ ) = ¬M Gr(P) (A ′ ) (3). By (2) and (3) we have M Gr(P) (q A ′ ) = M Gr(P) (A ′ ), and, in conjunction with (1), that M Gr(P) (p A) = M Gr(P) (q A ′ ), because A ∼ =M Gr(P) ,o A ′ implies, by Definition 17, that M Gr(P) (A) = M Gr(P) (A ′ ). Therefore, we also have p A ∼ =M Gr(P) ,o q A ′ and, in consequence, p ∼ =M Gr(P) ,o→o q.
For the second part, we show that M Gr(P) (s p) = M Gr(P) (s q). We do this in two steps; first we show that M Gr(P) (s p) = false and then that M Gr(P) (s q) = 0.
For the first step, it suffices to show that M 1 (s p) = Θ ↑ω M0 (s p) = false. For this, we prove that Θ ↑n M0 (s p) = false and Θ ↑n M0 (p (s p)) = false, for all n < ω, by an induction on n. The basis case is trivial, as Θ ↑0 M0 = ∅, U P,o , assigns the value false to every atom. For the induction step, we show the statement for n + 1 assuming that it holds for n. We see that there exists only one clause in Gr(P) such that s p is the head of the clause; this is the ground instance s p ← p (s p) of the clause s Q ← Q (s Q) of P. By the induction hypothesis, we have that Θ ↑n M0 (p (s p)) = false, therefore Θ Similarly, the only clause in Gr(P) with p (s p) as the head of the clause is the ground instance p (s p) ← (s p) of the clause p R ← R of P. By the induction hypothesis, we have that Θ ↑n M0 (s p) = false, therefore Θ (p (s p)) = false. For the second step, we perform an induction on α, during which we simultaneously show that M α (s q) = 0, M α (q (s q)) = 0 and M α (w (s q)) = 0, for all countable ordinals α. The basis case is trivial, as M 0 = ∅, ∅ assigns the value 0 to all atoms. For the induction step, we first prove the statement for a successor ordinal α+1, assuming that it holds for all countable ordinals up to α. Indeed, there exists exactly one clause in Gr(P) with w (s q) as its head atom, in particular the ground instance w (s q) ← ∼(s q) of the clause q R ← ∼(w R). As ∼(s q) is a negative literal, for every n < ω the value of Θ ↑(n+1) Mα (w (s q)) is defined by M α (∼(s q)). By the induction hypothesis, we have M α (s q) = M α (∼(s q)) = 0, therefore it follows that Θ ↑(n+1) Mα (w (s q)) = 0 and, because this holds for every n < ω, that M α+1 (w (s q)) = 0. Moreover, the ground instance q (s q) ← ∼(w (s q)) of the clause q R ← ∼(w R) is the only clause in Gr(P) with q (s q) as its head atom. Again, ∼(w (s q)) is a negative literal and so for every n < ω the value of Θ ↑(n+1) Mα (q (s q)) only depends on M α (∼(w (s q))). By the induction hypothesis, we have M α (w (s q)) = M α (∼(w (s q))) = 0, therefore it follows that Θ ↑(n+1) Mα (q (s q)) = 0. Since this holds for every n < ω, we also have that M α+1 (q (s q)) = 0. Finally, there exists only one clause in Gr(P) such that s q is the head of the clause, in particular the ground instance s q ← q (s q) of the clause s Q ← Q (s Q) of P. We have already shown that Θ ↑(n+1) Mα (q (s q)) = 0 for all n < ω; moreover, by the induction hypothesis, M α (q (s q)) = 0. Consequently, for all n < ω, Θ ↑(n+2) Mα (s q) = 0 and thus M α+1 (s q) = 0. It remains to show M α (s q) = 0, M α (q (s q)) = 0 and M α (w (s q)) = 0 for a limit ordinal α. In this case, we have that M α = β<α T β , β<α F β . By the induction hypothesis, M β (s q) = 0 for all β < α, which means that s q ∈ T β and s q ∈ F β . In other words, s q ∈ β<α T β and s q ∈ β<α F β , therefore M α (s q) = 0. In the same way we can show that M α (q (s q)) = 0 and M α (w (s q)) = 0. This concludes the induction and so we have proven that M Gr(P) (s q) = 0.

Appendix C Proof of Theorem 2
Before we proceed with the proof of Theorem 2, we recall some necessary definitions. Note that the proof makes use of a fixed-point characterization of the perfect model semantics given in (Przymusinska and Przymusinski 1990), rather than the more traditional definition of (Przymusinski 1988). The following definition of the local stratification of possibly infinite propositional programs is adapted to allow for the presence of expressions of the form (E 1 ≈ E 2 ).

Definition 23
A propositional program P is called locally stratified if and only if it is possible to decompose the Herbrand base B P of P into disjoint sets (called strata) S 1 , S 2 , . . . , S α , . . . , α < γ, where γ is a countable ordinal, such that for every clause H ← A 1 , . . . , A m , ∼B 1 , . . . , ∼B n in P, we have that for every i ≤ m, stratum(A i ) ≤ stratum(H) and for every i ≤ n, stratum(B i ) < stratum(H), where stratum is a function such that stratum(C) = β, if the propositional variable C ∈ B P belongs to S β and stratum(C) = 0, if C ∈ B P and is a constant (equivalently, of the form (E 1 ≈ E 2 )). Any decomposition of the described form is called a local stratification of P.
In (Przymusinska and Przymusinski 1990), for any interpretation J, the operator Ψ J is defined and shown to have a unique least fixed-point given by Ψ ↑ω J of the next definition. This is then used to give an iterated fixed-point characterization of the perfect model of a locally stratified program.

Definition 24
Let P be a propositional program and let J be an interpretation of P. The operator Ψ J : 2 B P → 2 B P is defined as follows: for every I ⊆ B P , Ψ J (I) = {p ∈ B P | there exists a clause p ← L 1 , . . . , L n in P such that, for all i ≤ n, either J(L i ) = true or
The next lemma and its following corollary are the basis for our proof of Theorem 2.

Lemma 2
Let P be an H program. If P is stratified then the ground instantiation Gr(P) of P is locally stratified.

Proof
Consider a decomposition S 1 , . . . , S r of the set of predicate constants of P such that the requirements of Definition 19 are satisfied. This defines a decomposition S ′ 1 , . . . , S ′ r of U P,o , which is also the Herbrand base of Gr(P), as follows: S ′ i = {A ∈ U P,o | the leftmost predicate constant of A belongs to S i } It is easy to check that S ′ 1 , . . . , S ′ r corresponds to a local stratification of Gr(P).
An immediate result of the above lemma is that the model N P can be defined for every stratified program of H:

Corollary 1
Let P be an H program. If P is stratified, then the perfect model N P of P exists and coincides with its well-founded model M P .

Proof
By Lemma 2, if P is stratified then Gr(P) is locally stratified. Therefore the unique perfect model N Gr(P) of Gr(P) exists (Przymusinski 1988) and N P is defined. Moreover, the perfect model of a locally stratified propositional program, which is the valuation function of N P , coincides with its well-founded model M Gr(P) (Przymusinski 1988), i.e. the valuation function of M P . In other words, in this case N P and M P coincide, because they have the same valuation function.

Theorem 2
The well-founded model M P of a stratified program P is extensional.

Proof
By Corollary 1, if P is stratified then M P coincides with N P . Therefore, it suffices to show that N P is extensional and for this we rely upon the constructive definition of N Gr(P) from (Przymusinska and Przymusinski 1990) presented above. Consider a stratification S 1 , . . . , S r of the set of predicate constants of P. As argued in the proof of Lemma 2, the following decomposition S ′ 1 , . . . , S ′ r of U P,o : S ′ i = {A ∈ U P,o | the leftmost predicate constant of A belongs to S i } corresponds to a local stratification of Gr(P). Therefore, whenever a ground atom A begins with a predicate constant p, we will have stratum(A) = stratum(p). Moreover, by Theorem 3, N Gr(P) = N r .
Since the valuation function of N P is N Gr(P) , essentially we need to show that E ∼ =N Gr(P) ,ρ E, for every ground expression E of every argument type ρ. We perform an induction on the structure of ρ. For the base types ι and o the statement holds by definition. For the induction step, we prove the statement for a predicate type π = ρ 1 → · · · → ρ m → o, assuming that it holds for all types simpler than π (i.e., for the types ρ 1 , . . . , ρ m , o and, recursively, the types that are simpler than ρ 1 , . . . , ρ m ). Let A be any atom of the following form: A is headed by a predicate constant p and all variables in vars(A) are of types simpler than π. Let θ, θ ′ be ground substitutions, such that vars(A) ⊆ dom(θ), dom(θ ′ ) and θ(V) ∼ =N Gr(P) ,ρ θ ′ (V) for any V : ρ in vars(A). We claim it suffices to show the following two properties P 1 (α) and P 2 (α), for all finite ordinals (i.e., natural numbers) α: P 1 (α): If N α (Aθ) = true then N Gr(P) (Aθ ′ ) = true. P 2 (α): If N α (Aθ) = false then N Gr(P) (Aθ ′ ) = false.
To see why proving the above properties is enough to establish that E ∼ =N Gr(P) ,π E, observe the following: first of all, we assumed that π is of the form ρ 1 → · · · → ρ m → o, so if V 1 : ρ 1 , . . . , V m : ρ m are variables, then E V 1 · · · V m is an atom of the form described above. As N Gr(P) = N r , if N Gr(P) (E θ(V 1 ) · · · θ(V m )) = N r (E θ(V 1 ) · · · θ(V m )) = true and property P 1 (r) holds, then we can infer that N Gr(P) (E θ ′ (V 1 ) · · · θ ′ (V m )) = true. Because the relations ∼ =N Gr(P) ,ρi are symmetric, θ and θ ′ are interchangeable. Therefore the same argument can be used to infer the reverse implication, i.e. N Gr(P) (E θ ′ (V 1 ) · · · θ ′ (V m )) = true ⇒ N Gr(P) (E θ(V 1 ) · · · θ(V m )) = true, thus resulting to an equivalence. If P 2 (r) holds, the analogous equivalence can be shown for the value false in the same way and so it follows that E ∼ =N Gr(P) ,π E. Finally, r is determined by the stratification of the higher-order