一句话：提出函数式概率网络语言 PλωNK，以高阶抽象和 ωQBS 语义扩展 Probabilistic NetKAT。
本文提出 PλωNK，一种函数式概率网络编程语言，用于扩展 Probabilistic NetKAT（PNK）。PNK 通过概率选择与无限迭代支持网络行为的概率建模，但缺乏抽象与高阶函数，编程不便。PλωNK 在保留概率建模能力的同时引入函数式抽象与高阶函数，并用显式的 thunk 与顺序组合语法来刻画并行和概率选择等副作用。形式化面临两大挑战：函数式环境中多副作用需受控，且测度论不允许高阶函数；作者借助 ω-Quasi Borel Spaces（ωQBS）这一概率程序语言域论进展来解决。该工作不仅为 PNK 带来抽象，也为组合高阶函数、迭代与并行的概率语言发展了元理论。
This work presents PλωNK, a functional probabilistic network programming language that extends Probabilistic NetKAT (PNK). Like PNK, it enables probabilistic modelling of network behaviour, by providing probabilistic choice and infinite iteration (to simulate looping network packets). Yet, unlike PNK, it also offers abstraction and higher-order functions to make programming much more convenient. The formalisation of PλωNK is challenging for two reasons: Firstly, network programming induces multiple side effects (in particular, parallelism and probabilistic choice) which need to be carefully controlled in a functional setting. Our system uses an explicit syntax for thunks and sequencing which makes the interplay of these effects explicit. Secondly, measure theory, the standard domain for formalisations of (continuous) probablistic languages, does not admit higher-order functions. We address this by leveraging ω-Quasi Borel Spaces (ωQBSes), a recent advancement in the domain theory of probabilistic programming languages. We believe that our work is not only useful for bringing abstraction to PNK, but that—as part of our contribution—we have developed the meta-theory for a probabilistic language that combines advanced features like higher-order functions, iteration and parallelism, which may inform similar meta-theoretic efforts.