π-演算中并行计算复杂度类型探究

### π - 演算中并行计算复杂度类型探究 #### 1. 定理与推论 有定理表明：设 $P$ 为一个带注释的进程，$m$ 是其全局并行复杂度。对于类型 $\varphi; \Phi; \Gamma \vdash P \triangleleft K$，有 $\varphi; \Phi \vDash K \geq m$。通过替换引理和并行组合规则可得到推论 1。 #### 2. 双调排序示例 双调排序是一种常见的并行算法，其并行复杂度为 $O(\log(n)^2)$。下面详细介绍其原理和实现。 - **双调序列**：双调序列有两种形式，一种是递增序列后接递减序列，如 $[2, 7, 23, 19, 8, 5]$；另一种是这种序列的循环旋转，如 $[8, 5, 2, 7, 23, 19]$。 - **主要函数**：该算法主要使用两个函数，$bmerge$ 和 $bsort$。 - **$bmerge$ 函数**：接收一个双调序列并递归排序。假设 $s = [a_0, \ldots, a_{n - 1}]$ 是双调序列，其中 $[a_0, \ldots, a_{n/2 - 1}]$ 递增，$[a_{n/2}, \ldots, a_{n - 1}]$ 递减，会生成 $s_1 = [\min(a_0, a_{n/2}), \min(a_1, a_{n/2 + 1}), \ldots, \min(a_{n/2 - 1}, a_{n - 1})]$ 和 $s_2 = [\max(a_0, a_{n/2}), \max(a_1, a_{n/2 + 1}), \ldots, \max(a_{n/2 - 1}, a_{n - 1})]$。$s_1$ 和 $s_2$ 也是双调序列，且 $\forall x \in s_1, \forall y \in s_2, x \leq y$。$bmerge$ 会递归应用于 $s_1$ 和 $s_2$ 以生成排序序列。 - **$bsort$ 函数**：接收一个序列并递归排序。先将序列分成两部分，然后分别对这两部分进行递增和递减排序，得到双调序列，最后使用 $bmerge$ 进行排序。 以下是双调排序在 $\pi$ - 演算中的代码实现： ``` !bcompare(l1 ,l2 ,a) . match(l1) { [ ] -> a⟨l1 ,l2⟩; ; x :: l′1 -> match(l2) { [ ] -> a⟨l1 ,l2⟩; ; y :: l′2 -> (νb)(νc)( bcompare⟨l′1 ,l′2 ,b⟩| tick.lessthan⟨x,y,c⟩ | b(lm ,lM ) .c(z) .if z then a⟨x :: lm ,y :: lM ⟩else a⟨y :: lm ,x :: lM ⟩ ) } } !bmerge(up, l ,a) . match( l ) { [ ] -> a⟨l ⟩; ; [y] -> a⟨l ⟩; ; -> let (l1 ,l2) = partition( l ) in (νb)(νc)(νd)( bcompare⟨l1 ,l2 ,b⟩| b(p1 ,p2) . (bmerge⟨up,p1 ,c⟩| bmerge⟨up,p2 ,d⟩) | c(q1) .d(q2) . if up then let l′ = q1 @ q2 in a⟨l′⟩ else let l′ = q2 @ q1 in a⟨l′⟩ ) } !bsort(up, l ,a) . match( l ) { [ ] -> a⟨l ⟩; ; [y] -> a⟨l ⟩; ; -> let (l1 ,l2) = partition( l ) in (νb)(νc)(νd)( bsort⟨tt,l1 ,b⟩| bsort⟨ff,l2 ,c⟩ | b(q1) .c(q2) .let q = q1 @ q2 in bmerge⟨up,q,d⟩| d(p) .a⟨p⟩ ) } ``` #### 3. 类型分析 - **$lessthan$ 服务器类型**：假设 $lessthan$ 具有服务器类型 $serv_0(B, B, ch_0(Bool))$，表示它是一个准备好被调用的服务器，接收一个用于返回布尔值的通道。 - **$bcompare$ 服务器类型**：可以给 $bcompare$ 赋予服务器类型 $\fo