Title: Approximation Fixpoint Theory and the Well-Founded Semantics of Higher-Order Logic Programs,
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 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.