将 Dup, Elide, Erase, Nothing 改为内置规则

[Wybxc]

Questions

• 是否区分 Dup/Elide, Erase/Nothing？
  • 类型擦除后，Dup/Elide 是同一个 Agent
  • 不再使用 Elide/Nothing，下同
• 如何处理 Dup-Elide 规约的行为？
  • 可能的两种规约方式：annihilate/commute（参考：HVM）

[Wybxc]

可能的解决方法：引入 Elide'，用于区分 annihilate / commute 两种规约

Lambda(@x, #y) >> Dup(@u, @v) =>
    @x -> Elide'(#x1, #x2)       /* 如果 @x 是 Lambda-like 的参数 */
    #y -> Dup(@y1, @y2)
    @u <- Lambda(@x1, #y1)
    @v <- Lambda(@x2, #y2)

Elide'(#x, #y) >> Dup(@u, @v) => #x -> @u, #y -> @v
Elide(#x, #y) >> Dup(@u, @v) =>
    #x -> Dup(@x1, @x2),
    #y -> Dup(@y1, @y2),
    @u <- Elide(#x1, #y1),
    @v <- Elide(#x2, #y2)

Lambda-like 参数指签名为 out Func(out x, in ...) 中的 out 参数，遇到 Lambda-like 参数时，构造 Elide'，否则构造 Elide

正确性待证明

跑了一下发现会导致规约无限膨胀，可能还需要再研究研究

[Wybxc]

演算了一下，发现即使去掉 lambda-like 函数，语言的表达能力也不会减弱

对于每个函数，可以额外定义一个 boxed agent，让 boxed agent 与 beta-reduction 的交互中生成 function agent，这样可以模拟 lambda 的效果

如果去掉 lambda-like 的函数，那么 Elide 与 Nothing 就不必要存在了