Document Open Access Logo

What’s Decidable About (Atomic) Polymorphism?

Authors Paolo Pistone, Luca Tranchini

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2021.27.pdf
  • Filesize: 0.9 MB
  • 23 pages

Document Identifiers

Author Details

Paolo Pistone
  • University of Bologna, Italy
Luca Tranchini
  • Eberhard Karls Universität Tübingen, Germany

Funding

  • Tranchini, Luca: DFG TR1112/4-1 "Falsity and Refutation. On the negative side of logic"

Cite AsGet BibTex

Paolo Pistone and Luca Tranchini. What’s Decidable About (Atomic) Polymorphism?. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 27:1-27:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.FSCD.2021.27

Abstract

Due to the undecidability of most type-related properties of System F like type inhabitation or type checking, restricted polymorphic systems have been widely investigated (the most well-known being ML-polymorphism). In this paper we investigate System Fat, or atomic System F, a very weak predicative fragment of System F whose typable terms coincide with the simply typable ones. We show that the type-checking problem for Fat is decidable and we propose an algorithm which sheds some new light on the source of undecidability in full System F. Moreover, we investigate free theorems and contextual equivalence in this fragment, and we show that the latter, unlike in the simply typed lambda-calculus, is undecidable.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Higher order logic
Keywords
  • Atomic System F
  • Predicative Polymorphism
  • ML-Polymorphism
  • Type-Checking
  • Contextual Equivalence
  • Free Theorems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Amal Ahmed, Dustin Jamner, Jeremy G. Siek, and Philip Wadler. Theorems for free for free: parametricity, with and without types. In Proceedings of the ACM on Programming Languages, volume 1 of ICFP, page Article No. 39, New York, 2017. Google Scholar
  2. Thorsten Altenkirch and Thierry Coquand. A finitary subsystem of the polymorphic λ-calculus. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, pages 22-28, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  3. E.S. Bainbridge, Peter J. Freyd, Andre Scedrov, and Philip J. Scott. Functorial polymorphism. Theoretical Computer Science, 70:35-64, 1990. Google Scholar
  4. Henk Barendregt. Lambda calculi with types. In Handbook of Logic in Computer Science, pages 117-309. Oxford University Press, 1992. Google Scholar
  5. Henk Barendregt, Wil Dekkers, and Richard Statman. Lambda calculus with types. Perspectives in Logic. Cambridge University Press, 2013. Google Scholar
  6. Norman Danner and Daniel Leivant. Stratified polymorphism and primitive recursion. Mathematical Structures in Computer Science, 9(4):507-522, 1999. Google Scholar
  7. Kosta Došen and Zoran Petrić. The typed Böhm theorem. Electronic Notes in Theoretical Computer Science, 50(2):117-129, 2001. Google Scholar
  8. Andrej Dudenhefner and Jakob Rehof. A simpler undecidability proof for system F inhabitation. In TYPES 2018, pages 2:1-2:11, 2018. Google Scholar
  9. José Espírito Santo and Gilda Ferreira. A refined interpretation of intuitionistic logic by means of atomic polymorphism. Studia Logica, 108(3):477-507, 2020. URL: https://doi.org/10.1007/s11225-019-09858-1.
  10. José Espírito Santo and Gilda Ferreira. The Russell-Prawitz embedding and the atomization of universal instantiation. Logic Journal of the IGPL, July 2020. jzaa025. Google Scholar
  11. Fernando Ferreira and Gilda Ferreira. Commuting conversions vs. the standard conversions of the "good" connectives. Studia Logica, 92(1):63-84, 2009. Google Scholar
  12. Fernando Ferreira and Gilda Ferreira. Atomic polymorphism. Journal of Symbolic Logic, 78(1):260-274, 2013. Google Scholar
  13. Fernando Ferreira and Gilda Ferreira. The faithfulness of Fat: a proof-theoretic proof. Studia Logica, 103(6):1303-1311, 2015. Google Scholar
  14. Gilda Ferreira. η-conversions of IPC implemented in atomic F. Logic Journal of the IGPL, 25(2):115-130, June 2016. Google Scholar
  15. Gilda Ferreira and Bruno Dinis. Instantiation overflow. Reports on Mathematical Logic, 51:15-33, 2016. Google Scholar
  16. Gilda Ferreira and Vasco T Vasconcelos. The computational content of atomic polymorphism. Logic Journal of the IGPL, 27(5):625-638, December 2018. Google Scholar
  17. Steven Fortune, Daniel Leivant, and Michael O'Donnell. The expressiveness of simple and second-order type structures. Journal of the ACM, 30(1):151-185, 1983. Google Scholar
  18. Ken-etsu Fujita and Aleksy Schubert. The undecidability of type related problems in the type-free style system F with finitely stratified polymorphic types. Information and Computation, 218:69-87, 2012. Google Scholar
  19. Dov M. Gabbay. Semantical Investigations in Heyting’s Intuitionistic Logic, volume 148. Springer Science + Business, Dordrecht, 1981. Google Scholar
  20. Jacques Garrigue and Didier Rémy. Extending ml with semi-explicit higher-order polymorphism. In Martín Abadi and Takayasu Ito, editors, Theoretical Aspects of Computer Software, pages 20-46, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  21. Paola Giannini and Simona Ronchi Della Rocca. Characterization of typings in polymorphic type discipline. In Proceedings of the 3-th Annual IEEE Symposium on Logic in Computer Science, pages 61-70, Edinburgh, 1988. Google Scholar
  22. Warren D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Computer Science, 13(2):225-230, 1981. Google Scholar
  23. Ryu Hasegawa. Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science, 4(1):71-109, 2009. Google Scholar
  24. Fritz Henglein. Polymorphic type inference and semi-unification. PhD thesis, The State University of New Jersey, 1989. Google Scholar
  25. Roger J. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29-60, 1069. Google Scholar
  26. Assaf J. Kfoury, Jerzy Tiuryn, and Paweł Urzyczyn. The undecidability of the semi-unification problem. Information and Computation, 102(1):83-101, 1993. Google Scholar
  27. Yves Lafont. The undecidability of second order linear logic without exponentials. The Journal of Symbolic Logic, 61(02):541-548, 1996. URL: https://doi.org/10.2307/2275674.
  28. Yves Lafont and Andre Scedrov. The Undecidability of Second Order Multiplicative Linear Logic. Information and Computation, 125(1):46-51, 1996. URL: https://doi.org/10.1006/inco.1996.0019.
  29. Joachim Lambek and Philip J. Scott. Introduction to higher order categorical logic. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1988. Google Scholar
  30. Didier Le Botlan and Didier Rémy. Mlf: Raising ml to the power of system f. In Proc. of the International Conference on Functional Programming (ICFP '03), pages 27-38, 2003. Google Scholar
  31. R. D. Lee. Decidable classes of recursive equations. PhD thesis, University of Leicester, 1969. Google Scholar
  32. Daniel Leivant. Stratified polymorphism. In LICS '89. Proceedings of the 4th Annual Symposium on Logic in Computer Science. IEEE, 1989. Google Scholar
  33. Daniel Leivant. Finitely stratified polymorphism. Information and Computation, 93(1):93-113, 1991. Google Scholar
  34. Daniel Leivant. A foundational delineation of Poly-time. Information and Computation, 110(2):391-420, 1994. Google Scholar
  35. Daniel Leivant. Peano’s lambda calculus: the functional abstraction implicit in arithmetic. In Logic, meaning and computation, Essays in Memory of Alonzo Church, volume 305 of Synthese Library, Studies in Epistemology, Logic, Methodology and Philosophy of Science, pages 313-329. Springer Netherlands, 2001. Google Scholar
  36. Jordi Levy. Decidable and undecidable second-order unification problems. In Tobias Nipkow, editor, Rewriting Techniques and Applications, pages 47-60, Berlin, Heidelberg, 1998. Springer Berlin Heidelberg. Google Scholar
  37. M. H. Löb. Embedding first order predicate logic in fragments of intuitionistic logic. Journal of Symbolic Logic, 41:705-718, 1976. Google Scholar
  38. Jan Małolepszy, Małgorzata Moczurad, and Marek Zaionc. Schwichtenberg-style lambda definability is undecidable. In Philippe de Groote and J. Roger Hindley, editors, Typed Lambda Calculi and Applications, pages 267-283, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  39. Paul-André Melliès and Noam Zeilberger. Functors are type refinement systems. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '15, pages 3-16, New York, NY, USA, 2015. Association for Computing Machinery. Google Scholar
  40. R. Milner and L. Damas. The principal type schemes for functional programs. In Symposium on Principles of Programming Languages, ACM, 1982. Google Scholar
  41. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Science, 17(3):248-375, 1978. Google Scholar
  42. Robin Milner. The standard ml core language. Polymorphism, 2(2), 1985. Google Scholar
  43. Le Than Dung Nguyen, Paolo Pistone, Thomas Seiller, and Lorenzo Tortora de Falco. Finite semantics of polymorphism, complexity and the expressive power of type fixpoints, 2019. URL: https://hal.archives-ouvertes.fr/hal-01979009.
  44. Vincent Padovani. Filtrage d'ordre supérieur. PhD thesis, Université Paris 7, 1996. Google Scholar
  45. Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1-2):185-199, 1993. Google Scholar
  46. Paolo Pistone. Proof nets and the instantiation overflow property, 2018. URL: http://arxiv.org/abs/1803.09297.
  47. Paolo Pistone and Luca Tranchini. The naturality of natural deduction II. some remarks on atomic polymorphism, 2020. URL: http://arxiv.org/abs/1908.11353.
  48. Paolo Pistone and Luca Tranchini. The Yoneda Reduction of Polymorphic Types (extended version), 2020. URL: http://arxiv.org/abs/1907.03481.
  49. Paolo Pistone and Luca Tranchini. The Yoneda Reduction of Polymorphic Types. In Christel Baier and Jean Goubault-Larrecq, editors, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), volume 183 of Leibniz International Proceedings in Informatics (LIPIcs), pages 35:1-35:22, Dagstuhl, Germany, 2021. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. Google Scholar
  50. Paolo Pistone and Luca Tranchini. What’s decidable about (atomic) polymorphism?, 2021. Available at URL: https://arxiv.org/abs/2105.00748.
  51. Gordon Plotkin and Martin Abadi. A logic for parametric polymorphism. In TLCA '93, International Conference on Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 361-375. Springer Berlin Heidelberg, 1993. Google Scholar
  52. M Clarence Protin. Type inhabitation of atomic polymorphism is undecidable. Journal of Logic and Computation, January 2021. exaa090. Google Scholar
  53. John C. Reynolds. Types, abstraction and parametric polymorphism. In R.E.A. Mason, editor, Information Processing '83, pages 513-523. North-Holland, 1983. Google Scholar
  54. Aleksy Schubert, Paweł Urzyczyn, and Konrad Zdanowski. On the Mints hierarchy in first-order intuitionistic logic. Logical Methods in Computer Science, 12(4:11):1-25, 2016. Google Scholar
  55. Helmut Schwichtenberg. Definierbare funktionen im λ-kalkül mit typen. Archiv für mathematische Logik und Grundlagenforschung, 17(3):113-114, 1975. Google Scholar
  56. S. K. Sobolev. The intuitionistic propositional calculus with quantifiers. Mathematical Notes of the Academy of Sciences of the USSR, 22(528-532), 1977. Google Scholar
  57. Morten Heine Sorensen and Pawel Urzyczyn. Lectures on the Curry-Howard isomorphism, volume 149 of Studies in logic and the foundations of mathematics. Elsevier Science, 2006. Google Scholar
  58. R. Statman. Completeness, invariance and λ-definability. The Journal of Symbolic Logic, 47(1):17-26, 1982. Google Scholar
  59. Richard Statman. intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9(1):67-72, 1979. Google Scholar
  60. Marin Sulzmann, Manuel M. T. Chakravarty, Simon Peyton Jones, and Kevin Donnelly. System f with type equality coercions. In TLDI '07 Proceedings of the 2007 ACM SIGPLAN Internatinal workshop in Types in languages design and implementation, pages 53-66. ACM New York, 2007. Google Scholar
  61. Luca Tranchini, Paolo Pistone, and Mattia Petrolo. The naturality of natural deduction. Studia Logica, https://doi.org/10.1007/s11225-017-9772-6, 2017.
  62. J. Voigtländer. Proving correctness via free theorems: the caser of the destroy/build-rule. In Proceedings of the ACM SIGPLAN symposium on Partial Evaluation and Semantics-Based Program Manipulation, pages 13-20, New York, 2008. ACM press. Google Scholar
  63. Philip Wadler. Theorems for free! In Proceedings of the fourth international conference on functinoal programming languages and computer architecture - FPCA '89, 1989. Google Scholar
  64. J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Annals of Pure and Applied Logic, 98:111-156, 1998. Google Scholar
  65. Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '99, pages 214-227, New York, NY, USA, 1999. Association for Computing Machinery. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact