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

TL;DR

This paper investigates the extension of Bezem's extensional semantics for higher-order logic programs to three-valued logic, revealing limitations in general cases but success in stratified programs, and analyzing the reasons for these results.

Contribution

It extends Bezem's semantics to three-valued logic, analyzes its limitations, and identifies conditions under which extensionality is preserved in higher-order logic programs.

Findings

Extensionality fails in the general three-valued setting.

Extensionality holds for stratified higher-order logic programs.

Three-valued relations cannot distinguish certain predicate behaviors.

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 (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.