Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization

• Autorzy: Dudenhefner Andrej , Rehof Jacob

Identyfikatory

DOI

10.3233/FI-2019-1856

• Języki publikacji: EN

Abstrakty

EN

We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we simplify the existing proof, reducing simple semi-Thue systems to intersection type inhabitation in the original Coppo-Dezani type assignment system. Additionally, we outline a direct reduction from the Turing machine halting problem to intersection type inhabitation. Second, we formalize soundness and completeness of the reduction in the Coq proof assistant under the banner of “type theory inside type theory”.

Słowa kluczowe

EN

turing machines; evidence

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 93--110
• Opis fizyczny: Bibliogr. 41 poz., rys.

Twórcy

autor

Dudenhefner Andrej

• Department of Computer Science, TU Dortmund University, Dortmund, Germany

autor

Rehof Jacob

• Department of Computer Science, TU Dortmund University, Dortmund, Germany

Bibliografia

• [1] Coppo M, Dezani-Ciancaglini M. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 1980. 21(4):685-693. doi:10.1305/ndjfl/1093883253.
• [2] Pottinger G. A Type Assignment for the Strongly Normalizable Lambda-Terms. In: Hindley J, Seldin J (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561-577. Academic Press, 1980.
• [3] Barendregt HP, Dekkers W, Statman R. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press, 2013. ISBN: 978-0-521-76614-2.
• [4] Urzyczyn P. The Emptiness Problem for Intersection Types. In: Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS ’94), Paris, France, July 4-7, 1994. 1994 pp. 300-309. doi:10.1109/LICS.1994.316059.
• [5] Urzyczyn P. The Emptiness Problem for Intersection Types. Journal of Symbolic Logic, 1999. 64(3):1195-1215. doi:10.2307/2586625.
• [6] Barendregt HP, Coppo M, Dezani-Ciancaglini M. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic, 1983. 48(4):931-940. doi:10.2307/2273659.
• [7] Salvati S. Recognizability in the Simply Typed Lambda-Calculus. In: Ono H, Kanazawa M, de Queiroz RJGB (eds.), WoLLIC 2009, Proceedings of Workshop on Logic, Language, Information and Computation, volume 5514 of LNCS. Springer, 2009 pp. 48-60. doi:10.1007/978-3-642-02261-6_5.
• [8] Salvati S, Manzonetto G, Gehrke M, Barendregt HP. Urzyczyn and Loader are logically related. In: ICALP 2012, Proceedings of Automata, Languages, and Programming - 39th International Colloquium, volume 7392 of LNCS. Springer, 2012 pp. 364-376. doi:10.1007/978-3-642-31585-5_34.
• [9] Plotkin G. Lambda definability and logical relations. Technical Report Memorandum SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, 1973.
• [10] Loader R. The undecidability of lambda definability. Logic, Meaning and Computation: Essays in Memory of Alonzo Church, 2001. pp. 331-342.
• [11] Leivant D. Polymorphic Type Inference. In: POPL 1983, Proceedings of the 10th ACM Symposium on Principles of Programming Languages. 1983 pp. 88-98. doi:10.1145/567067.567077.
• [12] Urzyczyn P. Inhabitation of Low-Rank Intersection Types. In: TLCA 2009, Proceedings of Typed Lambda Calculus and Applications, volume 5608 of LNCS. Springer, 2009 pp. 356-370. doi:10.1007/978-3-642-02273-9_26.
• [13] Kuśmierek D. The Inhabitation Problem for Rank Two Intersection Types. In: TLCA 2007, Proceedings of Typed Lambda Calculus and Applications, volume 4583 of LNCS. Springer, 2007 pp. 240-254. doi:10.1007/978-3-540-73228-0_18.
• [14] Chandra AK, Kozen DC, Stockmeyer LJ. Alternation. Journal of the ACM, 1981. 28(1):114-133. doi:10.1145/322234.322243.
• [15] Rehof J, Urzyczyn P. The Complexity of Inhabitation with Explicit Intersection. In: Constable RL, Silva A (eds.), Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, volume 7230 of LNCS. Springer, 2012 pp. 256-270. doi:10.1007/978-3-642-29485-3_16.
• [16] Kurata T, Takahashi M. Decidable properties of intersection type systems. In: TLCA 1995, Proceedings of Typed Lambda Calculus and Applications, volume 902 of LNCS. Springer, 1995 pp. 297-311. doi:10.1007/BFb0014060.
• [17] Schubert A, Urzyczyn P, Zdanowski K. On the Mints Hierarchy in First-Order Intuitionistic Logic. Logical Methods in Computer Science, 2016. 12(4). doi:10.2168/LMCS-12(4:11)2016.
• [18] Schubert A, Urzyczyn P, Zdanowski K. On the Mints Hierarchy in First-Order Intuitionistic Logic. In: Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015. Proceedings. 2015 pp. 451-465. doi:10.1007/978-3-662-46678-0_29.
• [19] Hindley JR. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42, Cambridge University Press, 2008.
• [20] Sørensen M, Urzyczyn P. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. ISBN:0444520775.
• [21] Urzyczyn P. Inhabitation in Typed Lambda-Calculi (A Syntactic Approach). In: TLCA’97, Typed Lambda Calculi and Applications, Proceedings, volume 1210 of LNCS. Springer, 1997 pp. 373-389. doi:10.1007/3-540-62688-3_47.
• [22] Statman R. Intuitionistic Propositional Logic is Polynomial-space Complete. Theoretical Computer Science, 1979. 9:67-72. doi:10.1016/0304-3975(79)90006-9.
• [23] Dudenhefner A, Rehof J. Rank 3 Inhabitation of Intersection Types Revisited (Extended Version). CoRR, 2017. abs/1705.06070. 1705.06070, URL http://arxiv.org/abs/1705.06070.
• [24] Dudenhefner A, Rehof J. Intersection Type Calculi of Bounded Dimension. In: POPL 2017, Proceedings of the 44th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Paris, France, January. 2017. doi:10.1145/3009837.3009862.
• [25] Dudenhefner A, Rehof J. Typability in Bounded Dimension. In: LICS 2017, Proceedings of the 32nd ACM/IEEE Symposium on Logic in Computer Science, Reykjavik, Iceland, June. 2017. doi:10.1109/LICS.2017.8005127.
• [26] Dudenhefner A, Rehof J. Principality and approximation under dimensional bound. PACMPL, 2019. 3(POPL):8:1-8:29. URL https://dl.acm.org/citation.cfm?id=3290321.
• [27] Rehof J. Towards Combinatory Logic Synthesis. In: BEAT 2013, 1st International Workshop on Behavioural Types. ACM, 2013.
• [28] Düdder B, Martens M, Rehof J. Staged Composition Synthesis. In: ESOP 2014, Proceedings of European Symposium on Programming, Grenoble, France 2014, volume 8410 of LNCS. Springer, 2014 pp. 67-86. doi:10.1007/978-3-642-54833-8_5.
• [29] Rehof J, Urzyczyn P. Finite Combinatory Logic with Intersection Types. In: TLCA 2011, Proceedings of Typed Lambda Calculus and Applications, volume 6690 of LNCS. Springer, 2011 pp. 169-183. doi:10.1007/978-3-642-21691-6_15.
• [30] Düdder B, Martens M, Rehof J, Urzyczyn P. Bounded Combinatory Logic. In: CSL 2012, Proceedings of Computer Science Logic, volume 16 of LIPIcs. Schloss Dagstuhl, 2012 pp. 243-258. doi:10.4230/LIPIcs. CSL.2012.243.
• [31] Linial S, Post EL. Recursive Unsolvability of the Deducibility, Tarski’s Completeness and Independence of Axioms Problems of Propositional Calculus. Bulletin of the American Mathematical Society, 1949. 55:50. MR 10514.
• [32] Dudenhefner A, Rehof J. Lower End of the Linial-Post Spectrum. In: TYPES 2017, 23rd International Conference on Types for Proofs and Programs, Budapest, Hungary, 29 May - 1 June 2017. 2017 doi:10.4230/LIPIcs.TYPES.2017.2.
• [33] Düdder B, Martens M, Rehof J. Staged Composition Synthesis. In: ESOP 2014, Proceedings. 2014 pp. 67-86. doi:10.1007/978-3-642-54833-8_5.
• [34] Heineman GT, Hoxha A, Düdder B, Rehof J. Towards Migrating Object-Oriented Frameworks to Enable Synthesis of Product Line Members. In: Proceedings of the 19th International Conference on Software Product Line, SPLC 2015, Nashville, TN, USA, July 20-24, 2015. 2015 pp. 56-60. doi:10.1145/2791060.2791076.
• [35] Bessai J, Dudenhefner A, Düdder B, Martens M, Rehof J. Combinatory Process Synthesis. In: Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I. 2016 pp. 266-281. doi:10.1007/978-3-319-47166-2_19.
• [36] Bessai J, Chen T, Dudenhefner A, Düdder B, de’Liguoro U, Rehof J. Mixin Composition Synthesis based on Intersection Types. Logical Methods in Computer Science, 2018. 14(1). doi:10.23638/LMCS-14(1:18)2018.
• [37] Coppo M, Dezani-Ciancaglini M. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 1980. 21(4):685-693. doi:10.1305/ndjfl/1093883253.
• [38] van Bakel S. Strict Intersection Types for the Lambda Calculus. ACM Computing Surveys, 2011. 43(3). doi:10.1145/1922649.1922657.
• [39] van Bakel S. Complete Restrictions of the Intersection Type Discipline. Theor. Comput. Sci., 1992. 102(1):135-163. doi:10.1016/0304-3975(92)90297-S.
• [40] Dudenhefner A. Reduction from simple semi-Thue system rewriting to inhabitation in the Coppo-Dezani type assignment system. https://github.com/mrhaandi/lambda-cap. Accessed: 2018-09-13.
• [41] Forster Y, Heiter E, Smolka G. Verification of PCP-Related Computational Reductions in Coq. In: Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings. 2018 pp. 253-269. doi:10.1007/978-3-319-94821-8_15.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).