对称交互演算

对称交互演算是通过对 Lambda 演算进行轻微修改而获得的最小化编程语言和计算模型，以使其完美匹配 Lamping 的最优归约算法的抽象部分。特点

1. 与 Lambda 演算一样，它可以轻松表达代数数据类型和任意递归算法。

2. 与图灵机一样，它可以通过简单的、常数时间的操作进行评估。

3. 与 Lambda 演算（和 Rust）不同，它不需要垃圾回收。

4. 与 Lambda 演算不同，其最优归约的所有中间步骤都对应于项。

5. 与 Lambda 演算不同，项不仅可以最优归约，而且可以高效归约（即，没有或acles）。

6. 与两者都不同，它本质上是并行的。

7. 它与 对称交互算子 同构，这是一个美丽的计算模型。

语法

语法是通过简单地扩展 Lambda 演算来获得，增加了 pairs 和 let。

term ::=
  | λx. term                 -- abstraction
  | (term term)              -- application
  | (term,term)              -- pair
  | let (p,q) = term in term -- definition
  | x                        -- variable

除了变量只能出现一次，并且可以全局使用（为什么？）。

归约规则

共有 4 条归约规则。其中两条是常见的：应用 lambda 和对对子进行投影。其余两条处理先前未指定的案例：“应用对子”和“投影 lambda”。第一种执行并行应用，第二种执行增量复制。所有这些操作都是常数时间的。

-- Rule 0: lambda-application

((λx.f) a)
----------
f [x / a]

-- Rule 1: pair-projection

let (p,q) = (u,v) in t
----------------------
t [p / u] [q / v]

-- Rule 2: pair-application

((u,v) a)
----------------
let (x0,x1) = a 
in ((u x0),(v x1))

-- Rule 3: lambda-projection

let (p,q) = (λx.f) in t
-----------------------
let (p,q) = f in t
[p / λx0.p]
[q / λx1.q]
[x / (x0,x1)]

在这里，[a / b] 表示将 a 的出现替换为 b 的全局替换，而 x0 和 x1 是新变量。我使用额外的括号包围 lambda，以使阅读更清晰。

示例

示例 0：lambda 应用和对子投影（没有什么新东西）。

λu. λv. let (a,b) = (λx.x, λy.y) in (a u, b v)
----------------------------------------------  pair-projection
λu. λv. ((λx.x) u, (λy.y) v)
---------------------------- lambda-application
λu. λv. ((λx.x) u, v)
--------------------- lambda-application
λu. λv. (u, v)

示例 1：使用 lambda 投影复制一个函数。

let (a,b) = λx.λy.λz.y in (a,b)
------------------------------- lambda-projection
let (a,b) = λy.λz.y in (λx0.a, λx1.b)
--------------------------------------- lambda-projection
let (a,b) = λz. (y0,y1) in (λx0.λy0.a, λx1.λy1.b)
-------------------------------------------------- lambda-projection
let (a,b) = (y0,y1) in (λx0.λy0.λz0.a, λx1.λy1.λz1.b)
----------------------------------------------------- pair-projection
(λx0.λy0.λz0.y0, λx1.λy1.λz1.y1)

示例 2：演示对应用。

((λx.x, λy.y) λt.t) 
------------------- pair-application
let (a0,a1) = λt. t in ((λx.x) a0, (λy.y) a1)
--------------------------------------------- lambda-projection
let (a0,a1) = (t0,t1) in ((λx.x) λt0.a0, (λy.y) λt1.a1)
-------------------------------------------------------  pair-projection
((λx.x) λt0.t0, (λy.y) λt1.t1)
------------------------------- lambda-application
((λx.x) λt0.t0, λt1.t1)
----------------------- lambda-application
(λt0.t0, λt1.t1)

示例 3：2 + 3。

这相当于

data Nat = S Nat | Z

add : Nat -> Nat -> Nat
add (S n) m = S (add n m)
add Z     m = m

main : Nat
main = add (S (S (S Z))) (S (S Z))

完全归约。

示例 4：对 True 应用 not 8 次。

完全归约。

下面是 2^(2^2) 的手写归约。