一句话：基于 call-by-push-value 重构函数逻辑编程核心演算，并以 lower powerdomain 给出与抽象机完全抽象的域论语义。
函数逻辑编程（FLP）在高阶函数式编程之上引入非确定性选择、逻辑变量与等式约束。本文观察到这些构造可呈现为代数效应，据此理性重构了一个基于 call-by-push-value 的 FLP 核心演算，支持高阶函数与递归。作者给出一个实现 narrowing 的抽象机来执行该演算的程序，并基于 lower powerdomain 建立域论语义，证明该语义相对于抽象机是可靠的（sound）、充分的（adequate）且完全抽象的（fully abstract）。这一结果同时引发对域论在刻画 FLP 时局限性的探讨，为理解非确定性与约束求解的语义基础提供了新的视角。
Functional Logic Programming (FLP) is a paradigm that extends higher-order functional programming with nondeterministic choice, logical variables, and equational constraints. Starting from the observation that these constructs can be presented as algebraic effects, we rationally reconstruct a core calculus for FLP that is based on call-by-push-value, and supports higher-order functions and recursion. We show how to execute its programs through an abstract machine that implements narrowing. Finally, we present a domain-theoretic semantics based on the lower powerdomain, which we prove to be sound, adequate, and fully abstract with respect to the machine. This leads to an exploration of the limitations of domain theory in modelling FLP.
@article{JonesMLMK26,
title = {Domain-Theoretic Semantics for Functional Logic Programming},
author = {Eddie Jones and Samson Main and Celia Mengyue Li and Jonathan Marriott and G. A. Kavvos},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776699}
}