View in EDS

Equivalence of two fixed-point semantics for definitional higher-order logic programs.

Saved in:
Bibliographic Details
Title: Equivalence of two fixed-point semantics for definitional higher-order logic programs.
Authors: Charalambidis, Angelos1 a.charalambidis@di.uoa.gr, Rondogiannis, Panos1 prondo@di.uoa.gr, Symeonidou, Ioanna1 i.symeonidou@di.uoa.gr
Source: Theoretical Computer Science. Mar2017, Vol. 668, p27-42. 16p.
Subjects: Mathematical equivalence, Fixed point theory, Semantics, Extension (Logic), Logic programming, Coincidence theory
Abstract: Two distinct research approaches have been proposed for assigning extensional semantics to higher-order logic programming. The former approach [11] uses classical domain-theoretic tools while the latter [1] 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. [ABSTRACT FROM AUTHOR]
Copyright of Theoretical Computer Science is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:Two distinct research approaches have been proposed for assigning extensional semantics to higher-order logic programming. The former approach [11] uses classical domain-theoretic tools while the latter [1] 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. [ABSTRACT FROM AUTHOR]
ISSN:03043975
DOI:10.1016/j.tcs.2017.01.005