交互网络通常会留下一堆冗余的粉丝吗？ [英] Is it usual for interaction nets to leave piles of redundant fans?

问题描述

我正在为交互网络编译lambda微积分术语，以便使用Lamping的抽象算法对它们进行评估。为了测试我的实现，我使用了这个教会号码分割功能：

  div =（λabcd。（b（λ （e（f））（e（f））（e（f））（e（f（e））。 e）（λe。e）（λe。e）））））
  

4（即，（λk。（div kk））（λfx。（f（f（fx）））））/ code>），我得到这个网络：

（抱歉，糟糕的渲染。 λ是一个lambda， R 是root， D 是一个粉丝， e 是橡皮擦。）

读回这个词，我得到1号教堂。但是这个网络非常膨胀：它有很多粉丝和橡皮擦没有明显的目的。划分更大的数字更糟糕。这是 div 32 32 ：

这又读回为一个，但在这里我们可以看到冗余风扇节点的尾部更长。我的问题是：这是减少特定术语时交互需求的预期行为，还是这是我实施时可能出现的错误？如果这不是bug，是否有解决方法？

解决方案

是的，以减少它的存在）



从交互式网络实现的一些细节中抽象出
，并从您对<$ $的抽象算法的可靠性假设进行抽象c $ c> div ，
一切看起来都很好。

• 否除了 chi 的声明之外，进一步的互动可以应用于您展示的输出，因为没有一对 De 可以通过它们的主要端口进行交互。




• 这种减少规则（这是IN框架）可能会提高效率，在某些特定情况下也是合理的。
  基本上，所涉及的粉丝不得有任何双胞胎，即在网络中不得存在 D'，这样最终消灭 D-D'可能会发生。
  有关更多详细信息，请参阅功能性编程语言的最佳实现，章节安全节点（可在线获取！），或者在原来的论文中找到：
  
  

  
  Asperti，Andrea和Juliusz Chroboczek。 安全操作员：永远关闭括号，优化最佳λ微积分实现。 适用于工程，通信和计算的代数 8.6（1997）：437-468。 最后，回读程序的目的不是为了减少程序的某种外部成本，而是作为计算重复和擦除的延期成本。
  正如您注意到的那样，这样的成本几乎可以忽略不计，所以如果您想在真实世界的场景中测试效率，总是总结减少共享和回读减少的结果。

b $ b

I'm compiling lambda calculus terms to interaction nets in order to evaluate them using Lamping's abstract algorithm. In order to test my implementation, I used this church-number division function:

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

Dividing 4 by 4 (that is, (λ k . (div k k)) (λ f x . (f (f (f (f x)))))), I get this net:

(Sorry for the awful rendering. λ is a lambda, R is root, D is a fan, e is eraser.)

Reading this term back, I get the church number 1, as expected. But this net is very inflated: it has a lot of fans and erasers that serve no obvious purpose. Dividing bigger numbers is even worse. Here is div 32 32:

This again reads back as one, but here we can see an even longer tail of redundant fan nodes. My question is: is this an expected behavior of interaction needs when reducing that particular term or is this a possible bug on my implementation? If this isn't a bug, is there any way around that?

解决方案

Yes, it is usual (but there are techniques to lessen its presence)

Abstracting from some details of your implementation with Interaction Nets, and also from your hypothesis of soundness of the abstract algorithm for your div, everything seems just fine to me.

• No further interaction can be applied to the output you show, in spite of chi's claim, because none of the pairs D-e can interact through their principal port.

• This latter kind of reduction rule (that is not allowed by IN framework) may improve efficiency and it is also sound in some particular cases. Basically, the involved fan must not have any "twin", i.e. there must exists no D' in the net such that eventually the annihilation D-D' can happen. For more details, look at The optimal implementation of functional programming language, chapter Safe nodes (which is available online!), or at the original paper from which that came:

  Asperti, Andrea, and Juliusz Chroboczek. "Safe Operators: Brackets Closed Forever Optimizing Optimal λ-Calculus Implementations." Applicable Algebra in Engineering, Communication and Computing 8.6 (1997): 437-468.

• Finally, the read-back procedure must be intended not as some sort of external cost for your reduction precedure, but rather as a deferred cost of computing duplication and erasure. As you notice, such a cost is rarely negligible, so if you want to test efficiency in a real-world scenario, always sum up both sharing reduction and read-back reduction.

这篇关于交互网络通常会留下一堆冗余的粉丝吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！