就这么多！

为什么？

考虑具有对的传统 Lambda 演算，它有两个计算规则

• Lambda 应用： (λx body) arg

• 成对投影： let {a b} = {fst snd} in cont

当将Lambda演算编译到交互组合子时

• lams和apps可以表示为构造节点（γ）

• pars和lets可以表示为复制节点（δ）

因此，lambda应用和成对投影仅仅是湮灭

      Lambda Application                 Pair Projection
                                                                   
      (λx body) arg                      let {a b} = {fst snd} in cont 
      ----------------                   -----------------------------
      x <- arg                           a <- fst                  
      body                               b <- snd                  
                                         cont                      
                                                                   
    ret  arg    ret  arg                  a   b       a    b       
     |   |       |    |                   |   |       |    |       
     |___|       |    |                   |___|       |    |       
 app  \ /         \  /                let  \#/         \  /        
       |    ==>    \/                       |    ==>    \/         
       |           /\                       |           /\         
 lam  /_\         /  \               pair  /#\         /  \        
     |   |       |    |                   |   |       |    |       
     |   |       |    |                   |   |       |    |       
     x  body     x   body                fst snd    fst   snd      
                                                                   
 "The application of a lambda        "The projection of a pair just 
 substitutes the lambda's var        substitutes the projected vars
 by the application's arg, and       by each element of the pair, and
 returns the lambda body."           returns the continuation."

但湮灭只发生在相同节点交互时。在交互网上，不同节点可以交互，这会触发另一个规则，即交换规则。该规则可以视为处理以下表达式

• Lambda投影： let {a b} = (λx body) in cont

• 成对应用： ({fst snd} arg)

但是，我们如何“投影”一个lambda或“应用”一个pair？在Lambda演算中，这些情况是未定义的并且会陷入停滞，应该是类型错误。然而，通过从交互组合子的角度解释交换规则的效果，我们可以为这些lambda表达式提出一种合理的归约

   Lambda Application                         Pair Application
                                                                  
   let {a b} = (λx body) in cont             ({fst snd} arg)   
   ------------------------------             ---------------
   a <- (λx0 b0)                             let {x0 x1} = arg in
   b <- (λx1 b1)                             {(fst x0) (snd x1)}
   x <- {x0 x1}
   let {b0 b1} = body in
   cont                   
       
    ret  arg         ret  arg            ret  arg         ret  arg  
     |   |            |    |              |   |            |    |   
     |___|            |    |              |___|            |    |   
 let  \#/            /_\  /_\         app  \ /            /#\  /#\  
       |      ==>    |  \/  |               |      ==>    |  \/  |  
       |             |_ /\ _|               |             |_ /\ _|  
 lam  /_\            \#/  \#/        pair  /#\            \ /  \ /  
     |   |            |    |              |   |            |    |   
     |   |            |    |              |   |            |    |   
     x  body          x   body           var body         var  body 

 "The projection of a lambda         "The application of a pair is a pair
 substitutes the projected vars      of the first element and the second
 by a copies of the lambda that      element applied to projections of the
 return its projected body, with     application argument."
 the bound variable substituted
 by the new lambda vars paired."

这，从某种意义上说，完成了lambda演算；也就是说，以前“停滞”的表达式现在有了有意义的计算。该系统按现在的写法是图灵完备的，然而，它非常有限，因为它不能复制pair，也不能复制复制的lambda。不过，有一种简单的方法可以极大地提高其表达能力：通过给lets加上标签，并将成对投影规则升级为

let #i{a,b} = #j{fst,snd} in cont
---------------------------------
if #i == #j:
  a <- fst
  b <- snd
  cont
else:
  a <- #j{a0,a1}
  b <- #j{b0,b1} 
  let #i{a0,a1} = fst in
  let #i{b0,b1} = snd in
  cont

也就是说，它可能对应于交互组合子的湮灭或交换，这取决于标签#i和#j的值。这使得IC能够复制pair，复制复制的lambda，计算嵌套循环，执行指数运算的Church编码，表达任意递归函数，如Y组合子等。换句话说，通过这种简单的扩展，IC变得非常强大和表达力强，为我们提供了

1. 一个新的计算模型，它与lambda演算类似，但可以最优归约。

2. 一个通用、高阶的“核心语言”，它比lambda演算更轻便、更快。

3. 交互组合子的项视图，使推理它们的图更容易。

话虽如此，请记住，IC与Lambda演算不等价。它是一个不同的模型。有一些λ项是IC无法计算的，反之亦然。例如，Lambda演算可以执行church-nats的自乘方，如λx (x x)，这在IC上是不可能的。然而，在IC上，我们可以有call/cc，直接O(1)队列和完全线性的HOAS，这在Lambda演算上是不可能的。

λu λv dup {a b} = {(λx x) (λy y)}; {(a u) (b v)}
------------------------------------------------ superposition-projection
λu λv {((λx x) u) ((λy y) v)}
----------------------------- lambda-application
λu λv {((λx x) u) v}
-------------------- lambda-application
λu λv {u v}

dup {a b} = λx λy λz y; {a b}
----------------------------- lambda-projection
dup {a b} = λy λz y; {(λx0 a) (λx1 b)}
-------------------------------------- lambda-projection
dup {a b} = λz {y0 y1}; {(λx0 λy0 a) (λx1 λy1 b)}
------------------------------------------------- lambda-projection
dup {a b} = {y0 y1}; {(λx0 λy0 λz0 a) (λx1 λy1 λz1 b)}
------------------------------------------------------ superposition-projection
{(λx0 λy0 λz0 y0) (λx1 λy1 λz1 y1)}

{{(λx x) (λy y)} (λt t)}
------------------------ superposition-application
dup {a0 a1} = λt t; {((λx x) a0) ((λy y) a1)}
--------------------------------------------- lambda-projection
dup {a0 a1} = {t0 t1}; {((λx x) (λt0 a0)) ((λy y) (λt1 a1))}
------------------------------------------------------------ superposition-projection
{((λx x) (λt0 t0)) ((λy y) (λt1 t1))}
------------------------------------- lambda-application
{((λx x) (λt0 t0)) (λt1 t1)}
---------------------------- lambda-application
{(λt0 t0) (λt1 t1)}

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))