A Decision Algorithm for Linear Isomorphism of Types with Complexity Cn(log2(n))

It is known that ordinary isomorphisms (associativity and commutativity<br />of "times", isomorphisms for "times" unit and currying)<br />provide a complete axiomatisation for linear isomorphism of types.<br />One of the reasons to consider linear isomorphism of types instead of<br />ordinary isomorphism was that better complexity could be expected.<br />Meanwhile, no upper bounds reasonably close to linear were obtained.<br />We describe an algorithm deciding if two types are linearly isomorphic<br />with complexity Cn(log2(n)).