抽象演算

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

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

2. 与图灵机类似，它可以通过简单、恒定时间的操作进行评估。

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

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

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

6. 与两者不同，它是内在并行的。

7. 它与 交互组合子 同构，这是一种美丽的计算模型。

语法

语法是通过简单地将 Lambda 演算扩展为 pairs 和 let 获得的。

term ::=
  | λx. term                 -- abstraction (affine function)
  | (term term)              -- application
  | (term,term)              -- superposition (pair)
  | let (p,q) = term in term -- definition (let)
  | 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：将 not 应用 8 次到 True 上。

完整归约。

这里是2^(2^2)的手写简化。