一句话：将函数式编排语言化简为核心 λχ，提出 semilenient 求值策略，把语义精简为十条规则并修正 Chorλ。
编排式编程允许用单个高层程序实现分布式交互并投影到各进程，但函数式编排语言的语义尚不清晰，已有 Chorλ 模型规则繁多且缺乏明确求值策略。本文从 Chorλ 出发剥离非本质特性，得到核心模型 λχ，发现其底层与非严格 λ 演算密切相关，并称之为 semilenient 求值。作者引入编排求值上下文与特殊 commute 规则，将 λχ 的语义精简到十条规则，同时发现先前 Chorλ 表述缺失的三条规则。额外结构还带来良好性质，可简化编排与投影之间的对应证明。该模型既是函数式编排语言的原则性基础，也适合作为入门切入点。
The past few years have seen a surge of interest in choreographic programming, a programming paradigm for concurrent and distributed systems. The paradigm allows programmers to implement a distributed interaction protocol with a single high-level program, called a choreography, and then mechanically project it into correct implementations of its participating processes. A choreography can be expressed as a λ -term parameterized by constructors for creating data “at” a process and for communicating data between processes. Through this lens, recent work has shown how one can add choreographies to mainstream languages like Java, or even embed choreographies as a DSL in languages like Haskell and Rust. These new choreographic languages allow programmers to write in applicative style (like in functional programming) and write higher-order choreographies for better modularity. But the semantics of functional choreographic languages is not well-understood. Whereas typical λ -calculi can have their operational semantics defined with just a few rules, existing models for choreographic λ -calculi have dozens of complex rules and no clear or agreed-upon evaluation strategy . We show that functional choreographic programming is simple. Beginning with the Chor λ model from previous work, we strip away inessential features to produce a “core” model called λ χ . We discover that underneath Chor λ ’s apparently ad-hoc semantics lies a close connection to non-strict λ -calculi; we call the resulting evaluation strategy semilenient . Then, inspired by previous non-strict calculi, we develop a notion of choreographic evaluation contexts and a special commute rule to simplify and explain the unusual semantics of functional choreographic languages. The extra structure leads us to a presentation of λ χ with just ten rules, and a discovery of three missing rules in previous presentations of Chor λ . We also show how the extra structure comes with nice properties, which we use to simplify the correspondence proof between choreographies and their projections. Our model serves as both a principled foundation for functional choreographic languages and a good entry point for newcomers.
@article{paperbot3038,
title = {Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)},
author = {Dan Plyukhin and Xueying Qin and Fabrizio Montesi},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {ICFP},
year = {2025},
doi = {10.1145/3747538}
}