Semantics of negation in extensional higher-order logic programming

Abstract

We consider the two existing extensional approaches to the semantics of positive higher-order logic programming, originally introduced by W. W. Wadge and M. Bezem respectively. 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, while only Wadge's approach had been extended to apply to higher-order programs with negation.We show that Wadge's semantics and Bezem's semantics coincide for a broad and interesting class of programs, which do not include existentially quantified predicate variables in the bodies of clauses. We indicate that they also have profound differences, which surface when we extend our source language to allow existential predicate variables.In addition, we focus on the less developed research direction of the two, namely Bezem's semantics, and we adapt, for the first time, Bezem's technique to define an extensional semantics for higher-order logic programs with negation. For this purpose, we utilize the infinite-valued approach to negation-as-failure. On the other hand, we show that an adaptation of the technique under the well-founded or the stable model semantics does not in general lead to an extensional semantics. We analyse the reasons for this failure arguing that a three-valued setting cannot 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. As an application of our developments, we define for the first time the notions of stratification and local stratification for higher-order logic programs with negation. We prove that every stratified program has a distinguished extensional model which can be equivalently obtained through the well-founded, stable or infinite-valued model semantics. Furthermore, we show that this model does not assign the unknown truth value. These results affirm the importance and the well-behaved nature of stratified programs, which was, until now, only known for the first-order case.

Θεωρούμε τις δύο υπάρχουσες εκτατικές προσεγγίσεις στη σημασιολογία των θετικών λογικών προγραμμάτων ανώτερης τάξης, προταθείσες από τον W. W. Wadge και τον M. Bezem αντίστοιχα. Η πρώτη προσέγγιση χρησιμοποιεί κλασικά εργαλεία από τη θεωρία πεδίων ενώ η δεύτερη στηρίζεται στις συντακτικές οντότητες που εμφανίζονται στο πρόγραμμα και βασίζεται στην επεξεργασία του βασικού αναπτύγματος του προγράμματος. Οι σχέσεις μεταξύ των δύο προσεγγίσεων δεν είχαν ως τώρα διερευνηθεί, ενώ μόνο η προσέγγιση του Wadge είχε επεκταθεί ώστε να εφαρμοστεί σε προγράμματα ανώτερης τάξης με άρνηση. Δείχνουμε ότι οι σημασιολογίες του Wadge και του Bezem συμπίπτουν για μία ευρεία και ενδιαφέρουσα κλάση προγραμμάτων, τα οποία δεν περιλαμβάνουν υπαρξιακά ποσοτικοποιημένες μεταβλητές στα σώματα των προτάσεων. Σημειώνουμε ότι έχουν επίσης ουσιαστικές διαφορές, οι οποίες γίνονται εμφανείς όταν επεκτείνουμε την θεωρούμενη γλώσσα ώστε να επιτρέπονται υπαρξιακές μεταβλητές. Επιπλέον, εστιάζουμε στη λιγότερο ανεπτυγμένη ερευνητική κατεύθυνση εκ των δύο, δηλαδή τη σημασιολογία του Bezem, και προσαρμόζουμε για πρώτη φορά την τεχνική του Bezem ώστε να ορίσουμε μία εκτατική σημασιολογία για λογικά προγράμματα ανώτερης τάξης με άρνηση. Για τον σκοπό αυτό, αξιοποιούμε την απειρότιμη προσέγγιση στην άρνηση-μέσω-αποτυχίας. Από την άλλη, δείχνουμε ότι o συνδυασμός της τεχνικής με τη σημασιολογία σταθερού μοντέλου ή με την καλώς θεμελιωμένη σημασιολογία, αποτυγχάνει να παράξει εκτατικές σημασιολογίες, στη γενική περίπτωση. Αναλύουμε τις αιτίες αυτής της αποτυχίας και ισχυριζόμαστε ότι μία τρίτιμη λογική δεν μπορεί να διαχωρίσει μεταξύ τους ορισμένα κατηγορήματα, τα οποία έχουν διαφορετική συμπεριφορά μέσα σε ένα πρόγραμμα, αλλά τυγχάνει να εμφανίζονται ως πανομοιότυπες τρίτιμες σχέσεις. Τέλος, ορίζουμε για πρώτη φορά τις έννοιες της στρωματοποίησης και της τοπικής στρωματοποίησης για λογικά προγράμματα ανώτερης τάξης με άρνηση. Αποδεικνύουμε ότι κάθε στρωματοποιημένο πρόγραμμα έχει ένα διακριτό εκτατικό μοντέλο, το οποίο μπορεί να κατασκευαστεί ισοδύναμα μέσω της καλώς θεμελιωμένης, της σταθερής ή της απειρότιμης σημασιολογίας. Επιπλέον, δείχνουμε ότι αυτό το μοντέλο δεν αποδίδει ποτέ την άγνωστη τιμή αληθείας. Τα αποτελέσματα αυτά αναδεικνύουν τη σπουδαιότητα και την καλή φύση των στρωματοποιημένων προγραμμάτων, που ήταν ως τώρα γνωστή μόνο στην περίπτωση των λογικών προγραμμάτων πρώτης τάξης.