二元会话类型 | Codeboy's Blog

形式陈述

二元会话类型描述一对端点之间有先后次序的通信义务：下一步发送什么、接收什么、由谁选择分支，以及何时结束。本文给出一个有限、同步的教学演算，以线性类型约束端点所有权，以小步语义描述双方同时完成一次通信。不含递归、共享端点、端点传递、子类型或进程失败。

协议、进程与基本计算

基本类型为 $A::=\mathsf{Int}\mid\mathsf{Bool}$ 。整数取数学整数，故没有溢出；基本值为整数和布尔常量。会话类型为

S::=\mathsf{end}\mid {!A.S}\mid {?A.S} \mid\oplus\{\ell_i:S_i\}_{i\in I} \mid\&\{\ell_i:S_i\}_{i\in I},

其中 $I$ 有限非空、标签互异。 $!A.S$ 表示发送一个 $A$ 后遵循 $S$ ， $?A.S$ 表示接收； $\oplus$ 主动选择一个标签， $\&$ 准备接受所列的任一标签。 $\mathsf{end}$ 是惰性的完成状态，本文没有额外的关闭握手。

把基本表达式与值区分开，才能准确描述发送 $n+1$ ：

\begin{aligned} v&::=k\mid\mathsf{true}\mid\mathsf{false} &&(k\in\mathbb Z),\\ e&::=v\mid a\mid e+e,\\ P&::=0\mid x!e.P\mid x?(a).P\mid x\triangleleft\ell.P \mid x\triangleright\{\ell_i:P_i\}_{i\in I} \mid(P\mid P)\mid(\nu xy)P. \end{aligned}

最后一行中的 $P\mid P$ 是并行组合。 $x?(a).P$ 绑定基本变量 $a$ ； $(\nu xy)P$ 绑定一对新鲜、互相连接的端点 $x,y$ 。所有代换均避免变量捕获。基本上下文 $\Gamma$ 允许复制和丢弃变量，包含通常的常量、变量规则以及

\frac{\Gamma\vdash e_1:\mathsf{Int}\quad\Gamma\vdash e_2:\mathsf{Int}} {\Gamma\vdash e_1+e_2:\mathsf{Int}}.

对闭的良型表达式，求值 $e\Downarrow v$ 总是终止且结果唯一：常量求值为自身，两个整数子表达式分别求值后相加。运行中输入变量先由通信代换为值，因此实际发送时表达式是闭的。基本计算无副作用，也不能读取或携带端点。

对偶 $\overline S$ 交换双方的义务，而不改变基本消息类型：

\begin{aligned} \overline{\mathsf{end}}&=\mathsf{end},& \overline{!A.S}&=?A.\overline S,& \overline{?A.S}&=!A.\overline S,\\ \overline{\oplus\{\ell_i:S_i\}_{i\in I}} &=\&\{\ell_i:\overline{S_i}\}_{i\in I},&& \overline{\&\{\ell_i:S_i\}_{i\in I}} =\oplus\{\ell_i:\overline{S_i}\}_{i\in I}. \end{aligned}

结构归纳立即给出 $\overline{\overline S}=S$ ；特别地，对偶分支具有完全相同的标签集。

类型规则与同步归约

判断 $\Gamma;\Delta\vdash P$ 中， $\Delta$ 记录端点的当前剩余协议，端点名互异。记 $\operatorname{end}(\Delta)$ 表示其所有条目均为 $\mathsf{end}$ ；这些惰性条目可以保留或去掉。以下规则中的 $\Delta,x:S$ 要求 $x$ 不在 $\Delta$ 中：

\frac{\operatorname{end}(\Delta)}{\Gamma;\Delta\vdash0} \qquad \frac{\Gamma;\Delta_1\vdash P\quad\Gamma;\Delta_2\vdash Q} {\Gamma;\Delta_1\uplus\Delta_2\vdash P\mid Q} \qquad \frac{\Gamma;\Delta,x:S,y:\overline S\vdash P} {\Gamma;\Delta\vdash(\nu xy)P}.

不相交并 $\uplus$ 保证一个活跃端点只属于一个并行分量；限制规则要求两端当前类型互为对偶。发送与接收分别消耗当前通信义务：

\frac{\Gamma\vdash e:A\quad\Gamma;\Delta,x:S\vdash P} {\Gamma;\Delta,x:!A.S\vdash x!e.P} \qquad \frac{\Gamma,a:A;\Delta,x:S\vdash P} {\Gamma;\Delta,x:?A.S\vdash x?(a).P}.

接收规则的 $a$ 是新鲜变量。选择只检查实际选择的延续；提供分支则必须检查每一种可能：

\frac{j\in I\quad\Gamma;\Delta,x:S_j\vdash P} {\Gamma;\Delta,x:\oplus\{\ell_i:S_i\}_{i\in I} \vdash x\triangleleft\ell_j.P},

\frac{\bigl(\Gamma;\Delta,x:S_i\vdash P_i\bigr)_{i\in I}} {\Gamma;\Delta,x:\&\{\ell_i:S_i\}_{i\in I} \vdash x\triangleright\{\ell_i:P_i\}_{i\in I}}.

所有分支使用同一份其他端点上下文 $\Delta$ ，但一次执行只进入一个分支。这是互斥选择，不能将这些前提误读成并行复制资源。

归约规则为

\frac{e\Downarrow v} {(\nu xy)(x!e.P\mid y?(a).Q) \longrightarrow(\nu xy)(P\mid Q[v/a])},

(\nu xy)(x\triangleleft\ell_j.P\mid y\triangleright\{\ell_i:Q_i\}_{i\in I}) \longrightarrow(\nu xy)(P\mid Q_j),\qquad j\in I.

另有交换两端角色的规则。归约对并行组合和限制封闭，不进入尚未通信的前缀；允许 $\alpha$ 换名、并行的交换结合与 $0$ 单位律，以及不捕获自由名字的作用域外移。发送和接收在同一步完成，没有消息队列。

直觉

普通消息类型只说明“这里传整数”。会话类型还能说明“先传整数，再由客户端选择继续或取消；继续就必须收到一个整数”。对偶不是两边写同一份程序，而是发送对应接收、选择对应等待选择。两端协议一致，才可能在同一个通信位置对接。

线性纪律管理的是当前协议能力的唯一所有者，不是端点名字在源码中只能出现一次。 $x!41.x?(r).0$ 中的两个 $x$ 由顺序前缀连接：第一个动作结束后，同一绑定以剩余类型进入延续。函数式接口可以改用“消费旧句柄、返回新句柄”表达同一推进；这里直接在推导上下文中更新剩余协议。

基本值与端点的纪律不同。服务端收到的整数 $n$ 放入 $\Gamma$ ，可以反复参与计算，也可以在取消分支中不用；活跃端点放入 $\Delta$ ，不能在两个同时运行的线程之间复制，也不能在仍有通信义务时被 $0$ 丢弃。

例子与边界

从 41 到 42，或在分支处取消

令客户端与服务端类型分别为

\begin{aligned} S&=!\mathsf{Int}.\oplus\{\mathsf{inc}:?\mathsf{Int}.\mathsf{end}, \mathsf{cancel}:\mathsf{end}\},\\ \overline S&=?\mathsf{Int}.\&\{\mathsf{inc}:!\mathsf{Int}.\mathsf{end}, \mathsf{cancel}:\mathsf{end}\}. \end{aligned}

完整程序为

\begin{aligned} C&=x!41.x\triangleleft\mathsf{inc}.x?(r).0,\\ D&=y?(n).y\triangleright\{ \mathsf{inc}:y!(n+1).0,\ \mathsf{cancel}:0\}. \end{aligned}

客户端由 $r:\mathsf{Int};x:\mathsf{end}\vdash0$ 向上应用接收、选择和发送规则，得到 $\varnothing;x:S\vdash C$ 。服务端在 $\Gamma=n:\mathsf{Int}$ 下有 $n+1:\mathsf{Int}$ ，所以 $\Gamma;y:!\mathsf{Int}.\mathsf{end}\vdash y!(n+1).0$ ；取消分支则有 $\Gamma;y:\mathsf{end}\vdash0$ 。两分支共享空的其他端点上下文，经分支及接收规则得到 $\varnothing;y:\overline S\vdash D$ 。并行与限制规则最后给出闭判断 $\varnothing;\varnothing\vdash(\nu xy)(C\mid D)$ 。

记 $C_1=x\triangleleft\mathsf{inc}.x?(r).0$ ，完整运行是

\begin{aligned} (\nu xy)(C\mid D) &\longrightarrow(\nu xy)(C_1\mid y\triangleright\{\mathsf{inc}:y!(41+1).0,\mathsf{cancel}:0\})\\ &\longrightarrow(\nu xy)(x?(r).0\mid y!(41+1).0)\\ &\longrightarrow(\nu xy)(0\mid0). \end{aligned}

第一步发送 $41$ 并代换 $n$ ；第二步同步选择 $\mathsf{inc}$ ；第三步由 $41+1\Downarrow42$ 发送 $42$ ，再作代换 $[42/r]$ 。 $r$ 未用于后续计算，故结果仍为 $0$ 。三步后的内部端点类型依次为

\begin{array}{c|c|c} &x&y\\\hline 1&\oplus\{\mathsf{inc}:?\mathsf{Int}.\mathsf{end},\mathsf{cancel}:\mathsf{end}\} &\&\{\mathsf{inc}:!\mathsf{Int}.\mathsf{end},\mathsf{cancel}:\mathsf{end}\}\\ 2&?\mathsf{Int}.\mathsf{end}&!\mathsf{Int}.\mathsf{end}\\ 3&\mathsf{end}&\mathsf{end} \end{array}

发送 41 后，inc 分支经返回 42 推进到双方 end；cancel 分支直接推进到双方 end，每次通信同步更新两端剩余类型。

图中的 $T=\oplus\{\mathsf{inc}:?\mathsf{Int}.\mathsf{end},\mathsf{cancel}:\mathsf{end}\}$ ， $\overline T$ 是服务端的对应分支类型。每条消息箭头位于通信前后的两行状态之间；取消路径是第二次通信的另一种选择，不与 $\mathsf{inc}$ 同时执行。

若改用 $C_{\mathrm{cancel}}=x!41.x\triangleleft\mathsf{cancel}.0$ ，客户端仍有类型 $S$ 。第一步同样发送 $41$ ；第二步选择取消，直接留下 $(\nu xy)(0\mid0)$ ，无需发送回复。相反，发送布尔值不能满足最初的 $!\mathsf{Int}$ ；选择未声明标签违反 $j\in I$ ；选择 $\mathsf{inc}$ 后直接停机则无法用 $x:?\mathsf{Int}.\mathsf{end}$ 推导 $0$ 。

两条会话仍可形成死锁

考虑完全封闭、没有递归的网络

N=(\nu xy)(\nu zw) \bigl(x?(n).z!\mathsf{true}.0\mid w?(b).y!1.0\bigr).

左线程的推导从结束条目开始：

\begin{aligned} n:\mathsf{Int};x:\mathsf{end},z:\mathsf{end}&\vdash0,\\ n:\mathsf{Int};x:\mathsf{end},z:!\mathsf{Bool}.\mathsf{end} &\vdash z!\mathsf{true}.0,\\ \varnothing;x:?\mathsf{Int}.\mathsf{end},z:!\mathsf{Bool}.\mathsf{end} &\vdash x?(n).z!\mathsf{true}.0. \end{aligned}

右线程同理：

\begin{aligned} b:\mathsf{Bool};w:\mathsf{end},y:\mathsf{end}&\vdash0,\\ b:\mathsf{Bool};w:\mathsf{end},y:!\mathsf{Int}.\mathsf{end} &\vdash y!1.0,\\ \varnothing;w:?\mathsf{Bool}.\mathsf{end},y:!\mathsf{Int}.\mathsf{end} &\vdash w?(b).y!1.0. \end{aligned}

两个上下文不相交； $x,y$ 对偶， $z,w$ 也对偶。因此并行规则及两次限制规则得到 $\varnothing;\varnothing\vdash N$ 。但左边等待 $x$ 接收，右边等待 $w$ 接收；对应发送 $y!1$ 与 $z!\mathsf{true}$ 都藏在尚未完成的接收前缀之后。没有归约规则可用。线性所有权与逐对对偶均成立，跨会话的循环等待仍然存在。

推论与应用

保持的是成对推进的不变量

沿用进展与保持的证明方法，本演算满足：若 $\Gamma;\Delta\vdash P$ 且 $P\longrightarrow P'$ ，则 $\Gamma;\Delta\vdash P'$ 。这里外部接口 $\Delta$ 不变；发生通信的受限制端点，其内部类型同时从 $S,\overline S$ 推进到相应的对偶延续，不能把定理误读成“每个端点一直保持最初类型”。

证明先建立基本值代换引理：若 $\Gamma,a:A;\Delta\vdash Q$ 且 $\Gamma\vdash v:A$ ，则 $\Gamma;\Delta\vdash Q[v/a]$ 。对类型推导归纳即可； $v$ 不包含端点，所以代换既不改变线性上下文，也不复制端点。基本表达式求值另满足 $\Gamma\vdash e:A$ 且 $e\Downarrow v$ 蕴含 $\Gamma\vdash v:A$ ，由表达式结构归纳得到。

对一次发送归约，反演并行、限制和前缀规则，得到发送端 $x:!A.S$ 、接收端 $y:?A.\overline S$ ，以及两延续分别具有 $x:S$ 、 $y:\overline S$ 。求值与代换引理使接收延续保持良型，再用原先不相交的其他端点上下文合成并行，最后重新限制 $x,y$ 。唯一所有权确保没有第三个并行分量还握着此次被推进的活跃端点。

对标签归约，反演得到相同标签集及被选择的 $j$ 。分支规则已经检查 $Q_j$ ，其类型恰为选择端延续 $S_j$ 的对偶；重组并行与限制即可。上下文封闭的情形由归纳假设重建推导，结构同余由换名、上下文交换与作用域条件保持良型。因此示例从头到尾的外层判断都为空接口，内部状态却确实经历了三次变化。

单条会话何时保证下一步

限定为 $(\nu xy)(P\mid Q)$ ：只有两个顺序执行者，分别独占 $x$ 与 $y$ ；延续不含新的并行或限制，没有其他活跃信道；基本计算总是终止，且没有失败或外部交互。对这样良型、闭合的配置，若协议尚未结束，就存在下一步通信。

理由来自类型反演。若 $x$ 的类型为 $!A.S$ ，左执行者必以 $x!e$ 开头，右执行者由对偶类型必以 $y?(a)$ 开头；闭的 $e$ 可求值，所以发送规则可用。接收情形对称。选择情形中，一侧确定一个合法标签，另一侧已为该标签准备延续。到 $\mathsf{end}$ 时，两顺序执行者只能终止。有限协议每步严格减少剩余协议深度，所以持续执行可用归约的运行最终终止；这里没有对任意实际调度器作公平性承诺。

一旦允许每个线程持有多条活跃会话，上述反演只能确定“某条信道上的下一动作”，不能保证其对端此刻也在处理这条信道； $N$ 正好展示断裂之处。若要证明一般网络的无死锁，还须增加会话依赖顺序等全局约束，不能仅引用逐对对偶。

实际接口可用会话类型检查请求—响应、取消分支和分阶段资源交接。若改为带队列的异步通信，发送方可先推进而接收方尚未推进，当前局部类型不再逐步锁定为对偶；保持证明必须把队列内容计入不变量。本文的同步证明不直接覆盖这种语义，而上述两个线程均先接收的死锁例子在空队列下依然阻塞。

参考资料

Kohei Honda、Vasco T. Vasconcelos、Makoto Kubo，Language Primitives and Type Discipline for Structured Communication-Based Programming，ESOP 1998，LNCS 1381，122–138 页，§§2、5 与 §6.1；Theorem 5.4 讨论 subject reduction 与交互错误排除，§6.1 区分同步原语及异步实现。
Vasco T. Vasconcelos，Fundamentals of Session Types，2012 年 5 月 17 日作者预印本，对应 Information and Computation 217，52–70 页，§§2–3、6–7；第 9 页明确区分会话类型安全与进展，并展示良型死锁。本文只抽取有限、基本值通信的教学片段，规则与证明已在正文独立给出。
Frank Pfenning，Lecture 7: Preservation and Progress，2023 年 9 月 19 日，§§3–5、Theorems 2 与 4。其配置纪律加入提供者与客户端的次序约束，进展定理的前提强于本文任意不相交端点分配。

形式陈述 ​

协议、进程与基本计算 ​

类型规则与同步归约 ​

从 41 到 42，或在分支处取消 ​

两条会话仍可形成死锁 ​

保持的是成对推进的不变量 ​

单条会话何时保证下一步 ​

反向链接