-
Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs
Authors:
Angelos Charalambidis,
Panos Rondogiannis,
Ioanna Symeonidou
Abstract:
We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first memb…
▽ More
We define a novel, extensional, three-valued semantics for higher-order logic programs with negation. The new semantics is based on interpreting the types of the source language as three-valued Fitting-monotonic functions at all levels of the type hierarchy. We prove that there exists a bijection between such Fitting-monotonic functions and pairs of two-valued-result functions where the first member of the pair is monotone-antimonotone and the second member is antimonotone-monotone. By deriving an extension of consistent approximation fixpoint theory (Denecker et al. 2004) and utilizing the above bijection, we define an iterative procedure that produces for any given higher-order logic program a distinguished extensional model. We demonstrate that this model is actually a minimal one. Moreover, we prove that our construction generalizes the familiar well-founded semantics for classical logic programs, making in this way our proposal an appealing formulation for capturing the well-founded semantics for higher-order logic programs. This paper is under consideration for acceptance in TPLP.
△ Less
Submitted 23 April, 2018;
originally announced April 2018.
-
The Intricacies of 3-Valued Extensional Semantics for Higher-Order Logic Programs
Authors:
Panos Rondogiannis,
Ioanna Symeonidou
Abstract:
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 (Rondo…
▽ More
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.
△ Less
Submitted 15 July, 2017;
originally announced July 2017.
-
Extensional Semantics for Higher-Order Logic Programs with Negation
Authors:
Panos Rondogiannis,
Ioanna Symeonidou
Abstract:
We develop an extensional semantics for higher-order logic programs with negation, generalizing the technique that was introduced in [Bezem99,Bezem01] for positive higher-order programs. In this way we provide an alternative extensional semantics for higher-order logic programs with negation to the one proposed in [CharalambidisER14]. As an immediate useful consequence of our developments, we defi…
▽ More
We develop an extensional semantics for higher-order logic programs with negation, generalizing the technique that was introduced in [Bezem99,Bezem01] for positive higher-order programs. In this way we provide an alternative extensional semantics for higher-order logic programs with negation to the one proposed in [CharalambidisER14]. As an immediate useful consequence of our developments, we define for the language we consider the notions of stratification and local stratification, which generalize the familiar such notions from classical logic programming. We demonstrate that for stratified and locally stratified higher-order logic programs, the proposed semantics never assigns the unknown truth value. We conclude the paper by providing a negative result: we demonstrate that the well-known stable model semantics of classical logic programming, if extended according to the technique of [Bezem99,Bezem01] to higher-order logic programs, does not in general lead to extensional stable models.
△ Less
Submitted 28 June, 2018; v1 submitted 30 January, 2017;
originally announced January 2017.
-
Equivalence of two Fixed-Point Semantics for Definitional Higher-Order Logic Programs
Authors:
Angelos Charalambidis,
Panos Rondogiannis,
Ioanna Symeonidou
Abstract:
Two distinct research approaches have been proposed for assigning a purely extensional semantics to higher-order logic programming. The former approach uses classical domain theoretic tools while the latter builds on a fixed-point construction defined on a syntactic instantiation of the source program. The relationships between these two approaches had not been investigated until now. In this pape…
▽ More
Two distinct research approaches have been proposed for assigning a purely extensional semantics to higher-order logic programming. The former approach uses classical domain theoretic tools while the latter builds on a fixed-point construction defined on a syntactic instantiation of the source program. The relationships between these two approaches had not been investigated until now. In this paper we demonstrate that for a very broad class of programs, namely the class of definitional programs introduced by W. W. Wadge, the two approaches coincide (with respect to ground atoms that involve symbols of the program). On the other hand, we argue that if existential higher-order variables are allowed to appear in the bodies of program rules, the two approaches are in general different. The results of the paper contribute to a better understanding of the semantics of higher-order logic programming.
△ Less
Submitted 10 September, 2015;
originally announced September 2015.
