Simple SubTypes of Intersection Types

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.

---

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