Simple SubTypes of Intersection Types

• Autorzy: Statman Rick

Identyfikatory

DOI

10.3233/FI-2019-1864

• Języki publikacji: EN

Abstrakty

EN

Solving the Entscheidungsproblem was a challenge first posed by David Hilbert in 1928, and solutions to decision problems are perhaps the most prized posessions in logic. Pawel Urzyczyn has a number of these, one of which I will discuss below. However, let me remind you of Michael Rabin describing his time with Dana Scott at IBM prior to their Turing award winning paper Finite automata and their decision problems “So we both went, in 1957 to IBM and the location was the so-called Lamb Estate [Robert S. Lamb estate], a wonderful place, while the Princeton Laboratory, designed by Sarason, the Watson Laboratory was in stages of construction. The Lamb Estate, very appropriately, used to be, before that, an Insane Asylum. All those buildings were building where kooks were housed...” [1]. This is what IBM thought of decision problems. In this note we give a new proof of the undecidability of the inhabitation problem for intersection types.

Słowa kluczowe

EN

statistical decision making; finite state machine; scaffolding; lambs

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 307--324
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Statman Rick

• Carnegie Mellon University, Department of Mathematical Sciences, Pittsburgh, PA 15213, USA

Bibliografia

• [1] Harel D. An Interview with Michael Rabin, Interviewed by David Harel. Jerusalem: ACM A.M. Turing Award. November 12, 2015.
• [2] Urzyczyn P. The Emptiness Problem for Intersection Types. J. Symb. Log. 64(3): 1195-1215 (1999), doi:10.2307/2586625.
• [3] Dudenhefner A, Rehof J. Rank 3 Inhabitation of Intersection Types Revisited (Extended Version). CoRR abs/1705.06070 (2017), (unpublished).
• [4] Statman R. On sets of terms with a given intersection type. CoRR, abs/1809.08169, 2018.
• [5] Loader R. The undecidability of λ-definability, Logic, Meaning and Computation: Essays in Memory of Alonzo Church, C. Anthony Anderson and Michael Zelëny eds., 2001, 331-342, doi:10.1007/978-94-010-0526-5_15.
• [6] Salvati S, Manzonetto G, Gehrke M, Barendregt H. Loader and Urzyczyn Are Logically Related. Automata, Languages, and Programming - 39th International Colloquium, ICALP 2012, Warwick, UK, July 9-13, 2012, Proceedings, Part II: 364-376, doi:10.1007/978-3-642-31585-5_34.
• [7] Barendregt HP, Dekkers W, Statman R. Lambda Calculus with Types. Perspectives in logic, Cambridge University Press 2013, ISBN 978-0-521-76614-2, pp. I-XXII, 1-833, doi:10.1017/CBO9781139032636.001.
• [8] Wikipedia contributors, Fitch notation. Wikipedia, The Free Encyclopedia. Feb. 25, 2018, 16:16 UTC. Available at: https://en.wikipedia.org/w/index.php?title=Fitch_notation&oldid=827587308. Accessed March 13, 2019.
• [9] Wikipedia contributors. Semilattice. Wikipedia, The Free Encyclopedia. Feb. 14, 2019, 16:55 UTC. Available at: https://en.wikipedia.org/w/index.php?title=Semilattice&oldid=883313539. Accessed March 14, 2019.
• [10] Coppo M, Giannini P. Principal Types and Unification for a Simple Intersection Type System. Inf. Comput. 122(1): 70-96 (1995), doi:10.1006/inco.1995.1141.
• [11] Coppo M, Giannini P. A Complete Type Inference Algorithm for Simple Intersection Types. CAAP ’92, 17th Colloquium on Trees in Algebra and Programming, Rennes, France, February 26-28, 1992, Proceedings: 102-123, doi:10.1007/3-540-55251-0_6.
• [12] Kfoury AJ, Wells JB. Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci. 311(1-3): 1-70 (2004), doi:10.1016/j.tcs.2003.10.032.

Uwagi

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