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