Undecidability of Intersection Type Inhabitation at Rank 3 and its Formalization

Issue title: Types, terms and reductions: A special issue dedicated to Paweł Urzyczyn for his 65th birthday

Guest editors: Thorsten Altenkirch and Aleksy Schubert

Article type: Research Article

Authors: Dudenhefner, Andrej^{; *} | Rehof, Jakob

Affiliations: Department of Computer Science, TU Dortmund University, Dortmund, Germany. andrej.dudenhefner@cs.tu-dortmund.de, jakob.rehof@cs.tu-dortmund.de

Correspondence: [*] Address for correspondence: Department of Computer Science, TU Dortmund University, Dortmund, Otto-Hahn-Str. 14, 44227 Dortmund , Germany

Abstract: 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”.

DOI: 10.3233/FI-2019-1856

Journal: Fundamenta Informaticae, vol. 170, no. 1-3, pp. 93-110, 2019