互动网是否通常会留下成堆的冗余粉丝？

Question

我正在为交互网编译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是橡皮擦.)

读回这个词,我按照预期得到了1号教堂.但这个网络非常膨胀:它有很多粉丝和橡皮擦没有明显的用途.划分更大的数字甚至更糟.这是div 32 32:

这再次回读为one,但在这里我们可以看到更长的冗余风扇节点尾部.我的问题是:这是减少特定术语时预期的交互需求行为,还是我的实现可能出现的错误？如果这不是一个错误,那有什么办法吗？

Answer 1

是的,这是通常的(但有一些技术可以减少它的存在)

从使用Interaction Nets的实现的一些细节中抽象出来,以及从你的抽象算法的完整性的假设中抽象出来div,对我来说一切似乎都很好.

• 尽管chi声称,因此没有进一步的交互可以应用于您显示的输出,因为没有一对D-e可以通过其主要端口进行交互.

• 后一种减少规则(IN框架不允许)可以提高效率,并且在某些特定情况下也是合理的.基本上,涉及的粉丝一定不能有任何"双胞胎",即网中必定不存在D'最终湮灭的D-D'情况.有关更多详细信息,请查看函数式编程语言的最佳实现,安全节点一章(可在线获取!),或者从原始文件中获取:

  Asperti,Andrea和Juliusz Chroboczek."安全操作员:托架永远关闭优化最佳λ微积分实现." 适用于工程,通信和计算的代数 8.6(1997):437-468.

• 最后,回读程序的目的不应该是减少程序的某种外部成本,而是计算重复和擦除的延迟成本.正如您所注意到的,这样的成本很少可以忽略不计,因此如果您想在真实场景中测试效率,请始终总结共享减少和回读减少.