The Inhabitation Problem for Rank Two Intersection Types

TL;DR

This paper demonstrates that determining whether a rank two intersection type can be inhabited is a decidable problem, but it is computationally hard, specifically EXPTIME-hard, due to a reduction from an acceptance problem for alternating Turing machines.

Contribution

It establishes the decidability of the inhabitation problem for rank two intersection types and proves its EXPTIME-hardness, challenging previous assumptions.

Findings

Inhabitation problem for rank two intersection types is decidable.

The problem is EXPTIME-hard, contrary to prior beliefs.

Reduction from alternating Turing machine acceptance problem proves hardness.

Abstract

We prove that the inhabitation problem for rank two intersection types is decidable, but (contrary to common belief) EXPTIME-hard. The exponential time hardness is shown by reduction from the in-place acceptance problem for alternating Turing machines.