title: Is it usual for interaction nets to leave piles of redundant fans?
body: <p>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:</p>
  
  <pre><code>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)))))
  </code></pre>
  
  <p>Dividing 4 by 4 (that is, <code>(λ k . (div k k)) (λ f x . (f (f (f (f x)))))</code>), I get this net:</p>
  
  <p><a href="https://i.stack.imgur.com/SmPim.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/SmPim.png" alt="enter image description here"></a></p>
  
  <p>(Sorry for the awful rendering. <code>λ</code> is a lambda, <code>R</code> is root, <code>D</code> is a fan, <code>e</code> is eraser.) </p>
  
  <p>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 <code>div 32 32</code>:</p>
  
  <p><a href="https://i.stack.imgur.com/khhb8.png" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/khhb8.png" alt="enter image description here"></a></p>
  
  <p>This again reads back as <code>one</code>, but here we can see an even longer tail of redundant fan nodes. My question is: <strong>is this an expected behavior of interaction needs when reducing that particular term or is this a possible bug on my implementation</strong>? If this isn't a bug, is there any way around that?</p>