Logic programming, as exemplified by datalog, defines the meaning of a program as the canonical smallest model derived from deductive closure over its inference rules. However, many problems call for an enumeration of models that vary along some set of choices while maintaining structural and logical constraints -- there is no single canonical model. The notion of stable models has successfully captured programmer intuition about the set of valid solutions for such problems, giving rise to a family of programming languages and associated solvers collectively known as answer set programming. Unfortunately, the definition of a stable model is frustratingly indirect, especially in the presence of rules containing free variables. We propose a new formalism, called finite-choice logic programing, for which the set of stable models can be characterized as the least fixed point of an immediate consequence operator. Our formalism allows straightforward expression of common idioms in both datalog and answer set programming, gives meaning to a new and useful class of programs, enjoys a constructive and direct operational semantics, and admits a predictive cost semantics, which we demonstrate through our implementation.

翻译：以datalog为例的逻辑程序设计，将程序的意义定义为从其推理规则的演绎闭包导出的规范最小模型。然而，许多问题需要枚举在保持结构和逻辑约束的同时沿某些选择集变化的模型——不存在单一的规范模型。稳定模型的概念已成功捕捉了程序员对此类问题有效解集的直觉，催生了一系列编程语言及相关求解器，统称为回答集程序设计。遗憾的是，稳定模型的定义令人沮丧地间接，尤其是在包含自由变量的规则存在时。我们提出一种称为有限选择逻辑程序设计的新形式体系，其稳定模型集合可被刻画为立即后果算子的最小不动点。我们的形式体系能直接表达datalog和回答集程序设计中的常见范式，赋予一类新颖且有用的程序以意义，具备构造性且直接的操作语义，并允许可预测的成本语义——我们通过实现对此进行了展示。