标签: interaction-nets

我正在为交互网编译lambda演算术语,以便使用Lamping的抽象算法来评估它们.为了测试我的实现,我使用了这个教堂号码除法功能:

div = (? a b c d . (b (? e . (e d)) (a (b (? e f g . (e (? h . (f h g)))) (? e . e) (? e f . (f (c e)))) (b (? e f . e) (? e . e) (? e . e)))))

除以4(即(? k . (div k k)) (? f x . (f (f (f (f x)))))),我得到这个网:

(抱歉可怕的渲染.?是一个lambda,R是root,D是粉丝,e是橡皮擦.) …

在这篇论文中，作者建议在 lambda 术语之间进行翻译：

data Term = Zero | Succ Term | App Term Term | Lam Term

和交互网络：

data Net = -- if I understood correctly
    Apply Net Net Net 
    | Abstract Net Net Net
    | Delete Net Net Int
    | Duplicate Net Net Net Int
    | Erase Net

不幸的是我无法理解他的编译算法。似乎缺少实际的算法，我不知道他对第三页上的图像是什么意思。我已经尝试通过查看已发布的源代码来理解它，但是作者使用他自己的图形重写 DSL 来定义它，所以我必须先学习它。翻译是如何作为普通 Haskell 函数实现的？