Hostname: page-component-7b7567c8c-7pwfn Total loading time: 0 Render date: 2026-11-12T22:39:47.625Z Has data issue: false hasContentIssue false
  • English
  • Français

On the building of affine retractions

Published online by Cambridge University Press:  01 August 2008

ALEKSY SCHUBERT
ALEKSY SCHUBERT*
Affiliation:
Institute of Informatics, University of Warsaw, ul. Banacha 2, 02-097 Warsaw, Poland Email: alx@mimuw.edu.pl
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

A simple type σ is retractable to a simple type τ if there are two terms Cσ→τ and Dτ→σ such that D ○ C λx.x. The retractability of types is affine if the terms C and D are affine, that is, when every bound variable occurs in them at most once in the scope of its declaration. This paper presents a system that derives affine retractability for simple types. It also studies the complexity of constructing these affine retractions. The problem of affine retractability is NP-complete even for the class of types over a single type atom and having limited functional order. In addition, a polynomial algorithm for types of orders less than three is presented.

References

Barendregt, H. P. (1992) Lambda calculi with types. In: Gabbay, S. A. D. and Maibaum, T. (eds.) Handbook of Logic in Computer Science 2, Oxford Science Publications 117–309.Google Scholar
Bono, V. and Tiuryn, J. (2002) Products and polymorphic subtypes. Fundamenta Informaticae 51 (1)13–41.Google Scholar
Bruce, K. and Longo, G. (1985) Provable isomorphisms and domain equations in models of typed languages. In: ACM Symposium on Theory of Computing (STOC'85).Google Scholar
Considine, J. (2000) Deciding isomorphisms of simple types in polynomial time. Technical report, Boston University, Boston, MA, USA.Google Scholar
Cormen, T. H., Leiserson, C. E. and Rivest, R. L. (1990) Introduction to Algorithms, MIT Press.Google Scholar
de'Liguoro, U., Piperno, A. and Statman, R. (1992) Retracts in Simply Typed λβη-Calculus. In: Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science 461–469.Google Scholar
Dezani-Ciancaglini, M. (1976) Characterization of normal forms possessing inverse in the lambda-beta-mu-calculus. Theoretical Computer Science 2 (3)323–337.CrossRefGoogle Scholar
Di Cosmo, R. (1995) Isomorphisms of types: from lambda-calculus to information retrieval and language design, Birkhauser.Google Scholar
Dowek, G. (1993) A unification algorithm for second-order linear terms. Manuscript available at http://coq.inria.fr/dowek.Google Scholar
Fiore, M. P., Cosmo, R. D. and Balat, V. (2002) Remarks on isomorphisms in typed lambda calculi with empty and sum types. In: LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society 147.CrossRefGoogle Scholar
Levy, J., Schmidt-Schauß, M. and Villaret, M. (2006) Bounded second-order unification is NP-complete. In: Term Rewriting and Applications (RTA-17). Springer-Verlag Lecture Notes in Computer Science 4098 400–414.CrossRefGoogle Scholar
Lincoln, P. and Mitchell, J. C. (1992) Algorithmic aspects of type inference with subtypes. In: POPL '92: Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press 293–304.Google Scholar
McAdam, B. J. (2002) Repairing Type Errors in Functional Programs, Ph.D. thesis, University of Edinburgh. (Available at http://hdl.handle.net/1842/368.)Google Scholar
Mitchell, J. C. (1988) Polymorphic type inference and containment. Information and Computation 76 (2-3)211–249.Google Scholar
Padovani, V. (2001) Retracts in simple types. In: Proceedings of Typed Lambda Calculi and Applications, 5th International Conference, TLCA 2001. Springer-Verlag Lecture Notes in Computer Science 2044 376–384.Google Scholar
Palsberg, J. and Zhao, T. (2001) Efficient and flexible matching of recursive types. Information and Computation 171 (2)364–387.CrossRefGoogle Scholar
Regnier, L. and Urzyczyn, P. (2001) Retractions of types with many atoms. Technical report, Institute of Informatics, Warsaw University. (Available at http://arxiv.org/abs/cs.LO/0212005.)Google Scholar
Rittri, M. (1991) Using types as search keys in function libraries. Journal of Functional Programming 1 (1)71–89.Google Scholar
Schmidt-Schauß, M. (2004) Decidability of bounded second order unification. Information and Computation 188 (2)143–178.Google Scholar
Schubert, A. (2004) On the building of affine retractions. In: Marcinkowski, J. and Tarlecki, A. (eds.) Proceedings of Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL. Springer-Verlag Lecture Notes in Computer Science 3210 205–219.Google Scholar
Spławski, Z. and Urzyczyn, P. (1999) Type fixpoints: Iteration vs. recursion. In: Proceedings of 4th International Conference on Functional Programming, ACM Press 102–113.Google Scholar
Stirling, C. (2006) A game-theoretic approach to deciding higher-order matching. In: Bugliesi, M., Preneel, B., Sassone, V. and Wegener, I. (eds.) Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Proceedings, Part II. Springer-Verlag Lecture Notes in Computer Science 4052 348–359.Google Scholar
Vorobyov, S. (1997) The “Hardest” Natural Decidable Theory. In: Proceedings of the Twelfth Annual IEEE Symposium on Logic in Computer Science 294–305.Google Scholar
Wierzbicki, T. and Dougherty, D. (2002) A Decidable Variant of Higher Order Matching. In: Tison, S. (ed.) Proc. 13th Conf. on Rewriting Techniques and Applications, RTA'02. Springer-Verlag Lecture Notes in Computer Science 2378 340–351.Google Scholar
Zibin, Y., Gil, J. Y. and Considine, J. (2003) Efficient algorithms for isomorphisms of simple types. In: POPL '03: Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press 160–171.CrossRefGoogle Scholar