Operator-based semantics for choice programs: is choosing losing? (full version)
Jesse Heyninck
TL;DR
This work presents an operator-based semantics framework for logic programs with choice constructs in both heads and bodies, grounded in non-deterministic approximation fixpoint theory (AFT). It defines four non-deterministic approximating operators—GZ, LPST, MR, and U—to generate four-valued interpretations via IC^x_P(x,y), enabling a principled comparison of supported and stable semantics for choice programs. The paper introduces constructive stable fixpoints, develops a c-stable operator based on well-founded sequences, and shows how these semantics generalize and relate to existing approaches for both choice and disjunctive logic programs, including three-valued versions of Liu et al. and Gelfond & colleagues. It also proposes several groundedness postulates to compare semantics and demonstrates how disjunctive logic program semantics emerge as special cases under D2C translations. Overall, the framework provides a unified, extensible means to analyze and compare a broad spectrum of semantics for non-deterministic choice programs, with implications for principled solver design and theoretical understanding of grounding and self-justification.
Abstract
Choice constructs are an important part of the language of logic programming, yet the study of their semantics has been a challenging task. So far, only two-valued semantics have been studied, and the different proposals for such semantics have not been compared in a principled way. In this paper, an operator-based framework allow for the definition and comparison of different semantics in a principled way is proposed.