A Decision Algorithm for Linear Isomorphism of Types with Complexity
![]() Alexander E. Andreev November 1996 |
Abstract:It is known that ordinary isomorphisms (associativity and
commutativity of ``times'', isomorphisms for ``times'' unit and currying)
provide a complete axiomatisation for linear isomorphism of types. One of the
reasons to consider linear isomorphism of types instead of ordinary
isomorphism was that better complexity could be expected. Meanwhile, no upper
bounds reasonably close to linear were obtained. We describe an algorithm
deciding if two types are linearly isomorphic with complexity
Available as PostScript, PDF, DVI. |