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 log2 n) time and O(n) space, where is n the input size. This result improves upon the O(n log2 n) time and O(n2) 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]
A. Andreev and S. Soloviev. A deciding algorithm for linear isomorphism of types with complexity O(n log2n). Lecture Notes in Computer Science, 1290:197ff, 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]
D. A. Basin. Equality of terms containing associative-commutative functions and commutative binding operators is isomorphism complete. In 10th International Conference on Automated Deduction, pages 251--260. Springer-Verlag New York, Inc., 1990.
[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 and G. Longo. Provable isomorphisms and domain equations in models of typed languages. In Proc. of the 7th annual ACM symposium on Theory of computing, pages 263--272. ACM Press, May 1985.
[7]
J. Considine. Deciding isomorphisms of simple types in polynomial time. Technical report, CS Department, Boston University, April 2000.
[8]
R. D. Cosmo. Type isomorphisms in a type-assignment framework. In Proc. of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 200--210. ACM Press, 1992.
[9]
R. Di Cosmo. Isomorphisms of types: from λ-calculus to information retrieval and language design. Birkhauser, 1995. ISBN-0-8176-3763-X.
[10]
M. Fiore, R. D. Cosmo, and V. Balat. Remarks on isomorphisms in typed lambda calculi with empty and sum types. In Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS'02), July 2002.
[11]
J. Y. Gil. Subtyping arithmetical types. In 27th Symposium on Principles of Programming Languages, POPL'01, pages 276--289, London, England, Jan.17--19 2001. ACM SIGPLAN --- SIGACT, ACM Press.
[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]
S. Jha, J. Palsberg, and T. Zhao. Efficient type matching. In Proc. of the 5th Foundations of Software Science and Computation Structures, Grenoble, France, April 2002.
[15]
J. Palsberg and T. Zhao. Efficient and flexible matching of recursive types. In Proc. of LICS'00, 15th Annual IEEE Symposium on Logic in Computer Science, June 2000.
[16]
M. Rittri. Using types as search keys in function libraries. Journal of Functional Programming, 1(1), 1989.
[17]
M. Rittri. Retrieving library identifiers via equational matching of types. In 10th International Conference on Automated Deduction, pages 603--617, 1990.
[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
- Efficient algorithms for isomorphisms of simple types
Recommendations
Efficient algorithms for isomorphisms of simple types
POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThe 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 ...
Efficient algorithms for isomorphisms of simple types
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 ...
Randomised algorithms for isomorphisms of simple types
We give the first linear time (randomised) algorithm for the first order isomorphism problem, that is, the isomorphism of non-recursive types involving product-and function-type constructors, under the axioms of commutativity and associativity of products, ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2003308 pages
Copyright © 2003 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 15 January 2003
Published in SIGPLAN Volume 38, Issue 1
Check for updates
Author Tags
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations9Total Citations
- 475Total Downloads
- Downloads (Last 12 months)6
- Downloads (Last 6 weeks)0
Reflects downloads up to 27 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in