一句话：提出 Verse 演算（VC），为确定性函数式逻辑编程提供小步重写语义，并证明良行为项的重写系统合流。
函数式逻辑语言文献丰富，但为其提供令人满意的语义一直是个难题。本文提出 Verse 演算（VC），一种面向确定性函数式逻辑编程的新核心演算。核心贡献是为 VC 建立小步重写语义，从而可以像对待 lambda 演算一样，通过连续应用重写规则来推理 VC 程序。作者进一步证明，对于良行为的项，该重写系统是合流的，即不同重写顺序不会导致结果分歧。该工作为确定性函数式逻辑编程提供了简洁的操作语义基础，并支持基于重写的程序推理。
Functional logic languages have a rich literature, but it is tricky to give them a satisfying semantics. In this paper we describe the Verse calculus, VC, a new core calculus for deterministic functional logic programming. Our main contribution is to equip VC with a small-step rewrite semantics, so that we can reason about a VC program in the same way as one does with lambda calculus; that is, by applying successive rewrites to it. We also show that the rewrite system is confluent for well-behaved terms.
@article{paperbot1906,
title = {The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming},
author = {Lennart Augustsson and Joachim Breitner and Koen Claessen and Ranjit Jhala and Simon Peyton Jones and Olin Shivers and Guy L. Steele Jr. and Tim Sweeney},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {ICFP},
year = {2023},
doi = {10.1145/3607845}
}