Efficient algorithms for isomorphisms of simple types

ABSTRACT

The first order isomorphism problem is to decide whether two non-recursive types using product- and function-type constructors, are isomorphic under the axioms of commutative and associative products, and currying and distributivity of functions over products. We show that this problem can be solved in O(n log² n) time and O(n) space, where is n the input size. This result improves upon the O(n log² n) time and O(n²) space bounds of the best previous algorithm. We also describe an O(n) time algorithm for the linear isomorphism problem, which does not include the distributive axiom, whereby improving upon the O(n log n) time of the best previous algorithm for this problem.

REFERENCES

• 1: Alexander E. Andreev , Sergei Soloviev, A Deciding Algorithm for Linear Isomorphism of Types with Complexity O (n log2(n)), Proceedings of the 7th International Conference on Category Theory and Computer Science, p.197-209, September 04-06, 1997
• 2: J. Auerbach, C. Barton, and M. Raghavachary. Type isomorphisms with recursive types. Technical Report RC 21247, IBM Research Division, Yorktown Heights, New York, August 1998.
• 3: J. Auerbach and M. C. Chu-Carroll. The mockingbird system: A compiler-based approach to maximally interoperable distributed programming. Technical Report RC 20178, IBM Research Division, Yorktown Heights, New York, February 1997.
• 4: David A. Basin, Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete, Proceedings of the tenth international conference on Automated deduction, p.251-260, July 1990, Kaiserslautern, Germany
• 5: K. B. Bruce, R. D. Cosmo, and G. Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science, 1:1--20, 1991.
• 6: K B Bruce , G Longo, Provable isomorphisms and domain equations in models of typed languages, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.263-272, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22175]
• 7: Jeffrey Considine, Deciding Isomorphisms of Simple Types in Polynomial Time, Boston University, Boston, MA, 2000
• 8: Robero Di Cosmo, Type isomorphisms in a type-assignment framework, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.200-210, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143208]
• 9: Roberto Di Cosmo, Isomorphisms of types: from &lgr;-calculus to information retrieval and language design, Birkhauser Verlag, Basel, Switzerland, 1995
• 10: Marcelo P. Fiore , Roberto Di Cosmo , Vincent Balat, Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.147, July 22-25, 2002
• 11: Joseph (Yossi) Gil, Subtyping arithmetical types, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.276-289, January 2001, London, United Kingdom
• 12: R. GureviΗ. Equational theory of positive numbers with exponentiation. American Mathmatical Society, 94(1):135--141, May 1985.
• 13: W. A. Howard. The formulaes-as-types notion of construction. In J. R. Hindley and J. P. Seldin, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479--490. Academic Press, 1980.
• 14: Somesh Jha , Jens Palsberg , Tian Zhao, Efficient Type Matching, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.187-204, April 08-12, 2002
• 15: Jens Palsberg , Tian Zhao, Efficient and Flexible Matching of Recursive Types, Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, p.388, June 26-29, 2000
• 16: M. Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1), 1989.
• 17: Mikael Rittri, Retrieving library identifiers via equational matching of types, Proceedings of the tenth international conference on Automated deduction, p.603-617, July 1990, Kaiserslautern, Germany
• 18: S. V. Soloviev. The category of finite sets and cartesian closed categories. Journal of Soviet Mathematics, 22(3):1387--1400, 1983.
• 19: A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley, CA, 2nd edition, 1951.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Lambda calculus and related systems

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

  G. Mathematics of Computing
  G.4 MATHEMATICAL SOFTWARE

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
first order isomorphism, linear isomorphism, non-recursive types, simple types, type signature