paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Functional Meaning for Parallel Streaming

并行流式计算的函数式语义
PLDI 9(PLDI)2025匹配度 2/10 · 该论文属于纯程序语言形式语义与确定性并行/分布式计算的理论工作,讨论 λ∨、流序、域理论和 Datalog 式单调性;与用户的 PL↔AI、静态分析、浮点程序分析、贝叶斯程序分析及 LLM/Agent 交叉方向基本无关。仅在广义 PL 理论基础上有很弱的关联。引用 1 inbox
Nick Rioux, Steve Zdancewic
crossref: 2026-09-10

AI 速览

一句话:提出核心语言 λ∨,用流序统一函数式编程与确定性分布式计算的基础。

并行与分布式编程中的竞态和消息重排会引入非确定性。LVars、CRDT 等通过共享状态上的偏序来刻画状态演化,使单调程序具有确定性;Datalog 风格语言虽将单调性一等化,却并非通用语言。本文提出 λ∨,一个面向确定性并行的核心语言:值可依据“流序”随时间增长,所有计算对该序单调。该流序与 Scott 语义中的近似序一致,从而把函数式编程的基础与确定性分布式计算的基础统一起来。λ∨ 具有基于域理论的计算充分模型,既保留函数式编程的组合性与抽象能力,又具备 Datalog 的声明式特征。

问题
并行与分布式编程因竞态和消息重排产生非确定性,如何设计既通用、表达自然又具有坚实形式基础的确定性并行语言。
方法
提出核心语言 λ∨,以流序约束值随时间增长并要求所有计算单调;该流序与 Scott 语义的近似序一致,据此建立域理论语义。
评估
通过域理论模型与计算充分性证明语义的合理性;摘要未报告实现或实验评估。
原文摘要(Abstract)

Nondeterminism introduced by race conditions and message reorderings makes parallel and distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address this problem by introducing a partial order structure on shared state that describes how the state evolves over time. Monotone programs that respect the order are deterministic. Datalog-inspired languages incorporate this idea of monotonicity in a first-class way but they are not general-purpose. We would like parallel and distributed languages to be as natural to use as any functional language, without sacrificing expressivity, and with a formal basis of study as appealing as the lambda calculus. This paper presents λ ∨ , a core language for deterministic parallelism that embodies the ideas above. In λ ∨ , values may increase over time according to a streaming order and all computations are monotone with respect to that order. The streaming order coincides with the approximation order found in Scott semantics and so unifies the foundations of functional programming with the foundations of deterministic distributed computation. The resulting lambda calculus has a computationally adequate model rooted in domain theory. It integrates the compositionality and power of abstraction characteristic of functional programming with the declarative nature of Datalog.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot3078,
  title = {Functional Meaning for Parallel Streaming},
  author = {Nick Rioux and Steve Zdancewic},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  year = {2025},
  doi = {10.1145/3729299}
}