Rank 3 Inhabitation of Intersection Types Revisited (Extended Version)

TL;DR

This paper strengthens the undecidability results of rank 3 intersection type inhabitation by showing it remains undecidable at order 3 and clarifies the principles needed for simulating Turing machines directly, offering a more concise construction.

Contribution

It proves that intersection type inhabitation is undecidable for types of rank 3 and order 3, and provides a clearer, more direct simulation of Turing machine computation.

Findings

Undecidability of rank 3 intersection type inhabitation at order 3

A more concise construction for simulating Turing machines

Insights into the expressiveness of intersection type inhabitation

Abstract

We revisit the undecidability result of rank 3 intersection type inhabitation (Urzyczyn 2009) in pursuit of two goals. First, we strengthen the previous result by showing that intersection type inhabitation is undecidable for types of rank 3 and order 3, i.e. it is not necessary to introduce new functional dependencies (new instructions) during proof search. Second, we pinpoint the principles necessary to simulate Turing machine computation directly, whereas previous constructions used a highly parallel and non-deterministic computation model. Since our construction is more concise than existing approaches taking no detours, we believe that it is valuable for a better understanding of the expressiveness of intersection type inhabitation.

Equations

$$\mathrm{rank}(\tau )$$

$$\mathrm{rank}(\sigma \cap \tau )$$

$$\mathrm{rank}(\sigma \to \tau )$$

$$\mathrm{order}(a)$$

$$\mathrm{order}(\sigma \cap \tau )$$

$$\mathrm{order}(\sigma \to \tau )$$

$$\mathbb{A}=\Sigma \dot{\cup }\{l,r,\bullet \}\dot{\cup }\{⟨q,a⟩\mid q\in Q,a\in \Sigma \}\dot{\cup }\{\circ ,\ast ,\#,\$\}$$

$${\sigma }_f=$$

$$\text{ for each }t=$$

$${\sigma }_t=$$

$$\text{ for each }t=$$

$${\sigma }_t=$$

$${\Gamma }_i⊢M_C^{C^{\prime }}:a_i\to a_i\text{ for }i\in [1,n]\setminus \{p,p+1\}$$

$$\text{and }{\Gamma }_p⊢M_C^{C^{\prime }}:c^{\prime }\to ⟨q,a_p⟩\text{ and }{\Gamma }_{p+1}⊢M_C^{C^{\prime }}:⟨q^{\prime },a_{p+1}⟩\to a_{p+1}$$

$${\Gamma }_i⊢M_C^{C^{\prime }}:a_i\to a_i\text{ for }i\in [1,n]\setminus \{p-1,p\}$$

$$\text{and }{\Gamma }_p⊢M_C^{C^{\prime }}:c^{\prime }\to ⟨q,a_p⟩\text{ and }{\Gamma }_{p-1}⊢M_C^{C^{\prime }}:⟨q^{\prime },a_{p-1}⟩\to a_{p-1}$$

$${\Gamma }_p⊢M:⟨q,a_p⟩$$

$$⟹$$

$$\text{and }{\Gamma }_p⊢N:c^{\prime }\text{ and }{\Gamma }_{p+1}⊢N:⟨q^{\prime },a_{p+1}⟩$$

$${\Gamma }_p⊢M:⟨q,a_p⟩$$

$$⟹$$

$$\text{and }{\Gamma }_p⊢N:c^{\prime }\text{ and }{\Gamma }_{p-1}⊢N:⟨q^{\prime },a_{p-1}⟩$$

$${\sigma }_{\ast }=$$

$${\sigma }_0=$$

$${\tau }_{\star }=$$

$$\text{where }\delta =\{t_1,\dots ,t_k\}$$

$${\sigma }_{\ast }$$

$${\sigma }_0$$

$${\sigma }_1$$

$${\sigma }_{ab\Rightarrow cd}$$

$${\tau }_{\star }$$

$$\text{where }R=\{t_1,\dots ,t_k\}$$

Full text

0.1 Introduction

Intersection types capture deep semantic properties of $\lambda$-terms such as normalization and were subject to extensive study for decades [1]. Due to their expressive power, intersection type inhabitation (given a type, does there exist a term having the type?) is undecidable in standard intersection type systems [2].

Urzyczyn showed in 2009 [5] that restricted to rank 2 intersection type inhabitation is exponential space complete and is undecidable for rank 3 and up. Later, Salvati et al. discovered the equivalence of intersection type inhabitation and $\lambda$-definability [4], which further improved our understanding of the expressiveness of intersection types.

One can take several routes in order to show undecidability of intersection type inhabitation (abbreviated by IHP, resp. IHP3 for rank 3). In [1] the following reduction is performed: EQA $\leq$ ETW $\leq$ WTG $\leq$ IHP, where EQA is the emptiness problem for queue automata, ETW is the emptiness problem for typewriter automata and WTG is the problem of determining whether one can win a tree game. A different route taken in [5] performs the following reduction: ELBA $\leq$ SSTS1 $\leq$ HETM $\leq$ IHP3, where ELBA is the emptiness problem for linear bounded automata, SSTS1 is the problem of deciding whether there is a word that can be rewritten to 1s in a simple semi-Thue system and HETM is the halting problem for expanding tape machines. Alternatively, following the route of [4] via semantics, the following reduction can be performed: WSTS $\leq$ LDF $\leq$ IHP3, where WSTS is the word problem in semi-Thue systems and LDF is the $\lambda$-definability problem. Each of these routes introduces its own machinery that may distract from the initial question. As a result, it is challenging to even give examples of particularly hard inhabitation problem instances, or distinguish necessary properties on a finer scale than the rank restriction.

In this work (cf. Section 0.3), we reduce the halting problem for Turing machines to intersection type inhabitation directly. In particular, we show how arbitrary Turing machine computations can be directly simulated using proof search. Additionally (Section 0.4), we outline the simplest construction (to date) to show undecidability of rank 3 inhabitation using simple semi-Thue systems. The main benefit of presented approaches is their corresponding accessibility and simplicity.

0.2 Preliminaries

We briefly assemble the necessary prerequisites in order to discuss inhabitation in the intersection type system. $\lambda$-terms (cf. Definition 1) are denoted by $M,N,L$ and intersection types (cf. Definition 2) are denoted by $\sigma,\tau$, while type atoms are denoted by $a,b,c$ and drawn from the denumerable set $\mathbb{A}$. The intersection operator $\cap$ binds stronger than $\to$ and is assumed to be idempotent, commutative and associative. The rules of the considered intersection type system (also used in [5]) are given in Definition 3.

Definition 1** ($\lambda$-Terms).**

$M,N,L::=x\mid(\lambda x.M)\mid(M\,N)$**

Definition 2** (Intersection Types).**

$\sigma,\tau::=a\mid\sigma\to\tau\mid\sigma\cap\tau\text{ where }a\in\mathbb{A}$**

Definition 3** (Intersection Type System).**

[TABLE]

After Leivant [3] we define the rank and the order of a type.

Definition 4** (Rank).**

[TABLE]

Definition 5** (Order).**

[TABLE]

Example 1**.**

Let $\tau=\bigcap_{i=1}^{n}(((d_{i}\to c_{i})\to b_{i})\to a_{i})\to a$. We have $\operatorname{rank}(\tau)=2$ and $\operatorname{order}(\tau)=4$. Note that types that are similar to $\tau$ are used in [5] to encode expanding tape machine switches.

Problem 1** (Intersection Type Inhabitation).**

Given a type $\tau$, is there a $\lambda$-term $M$ such that $\vdash M:\tau$?

0.3 Turing Machine Simulation

The undecidability proof in [5] reduces emptiness of linear bounded automata to a word existence problem in simple semi-Thue systemd to halting of expanding tape machines to inhabitation of an intersection type $\tau$ with $\operatorname{rank}(\tau)=3$ and $\operatorname{order}(\tau)=4$. In [5] order of $4$ is necessary to hide and restore a word on the tape of the machine by introducing new instructions. In this section, we reduce the halting problem to inhabitation of an intersection type $\tau_{\star}$ with $\operatorname{rank}(\tau_{\star})=\operatorname{order}(\tau_{\star})=3$. For this purpose, fix a Turing machine $T=(\Sigma,Q,q_{0},q_{f},\delta)$, where

• •

$\Sigma$ is the finite, non-empty set of tape symbols

• •

$Q$ is the finite, non-empty set of states

• •

$q_{0}\in Q$ is the initial state

• •

$q_{f}\in Q$ is the final state

• •

$\delta:(Q\setminus\{q_{f}\})\times\Sigma\to Q\times\Sigma\times\{+1,-1\}$ is the transition function

Let $\dot{\cup}$ denote disjoint union. We define the set of type atoms

[TABLE]

In the first part of our construction, we capture computation of $T$ using the following types:

[TABLE]

Intuitively, the defined types are used to achieve following goals

• •

$\langle q,a\rangle$ represents that $T$ is at the position containing $a$ in state $q$

• •

$l,r$ (left, right) mark neighboring cells while other cells are marked by $\bullet$

• •

$\sigma_{f}$ recognizes whether an accepting state is reached

• •

$\sigma_{t}$ transforms the state according to $\delta$

Let us abbreviate $[i,j]:=\{i,i+1,\ldots,j\}$.

Lemma 1**.**

Given $q\in Q$, $s=a_{1}\ldots a_{n}\in\Sigma^{n}$ and $p\in[1,n]$ we have $(q,p,s)$ is accepting in $T$ using at most $n$ tape cells iff there exists a term $e$ such that $\Gamma_{p}\vdash e:\langle q,a_{p}\rangle$ and $\Gamma_{i}\vdash e:a_{i}$ for $i\in[1,n]\setminus\{p\}$, where

• •

$\Gamma=\{x_{f}:\sigma_{f}\}\cup\{x_{t}:\sigma_{t}\mid t\in\delta\}$**

• •

$\Gamma_{1}=\Gamma\cup\{y_{1}:l\}\cup\{y_{j}:\bullet\mid j\in[2,n-1]\}$**

• •

$\Gamma_{i}=\Gamma\cup\{y_{i-1}:r,y_{i}:l\}\cup\{y_{j}:\bullet\mid j\in[1,n-1]\setminus\{i-1,i\}\}$* for $i\in[2,n-1]$*

• •

$\Gamma_{n}=\Gamma\cup\{y_{n-1}:r\}\cup\{y_{j}:\bullet\mid j\in[1,n-2]\}$**

Proof.

By construction $(y_{i}:l)\in\Gamma_{i}$ and $(y_{i}:r)\in\Gamma_{i+1}$ for $i\in[1,n-1]$. Intuitively, this property is used to identify “neighboring” contexts.

“$\Rightarrow$”****: Assume $(q,p,a_{1}\ldots a_{n})$ is accepting in $T$ using at most $n$ tape cells. If $q=q_{f}$, then $\Gamma_{i}\vdash x_{f}:a_{i}$ for $i\in[1,n]\setminus\{p\}$ and $\Gamma_{p}\vdash x_{f}:\langle q,a_{p}\rangle$. To capture computation, we represent the transition $C\stackrel{{\scriptstyle t\in\delta}}{{\leadsto}}C^{\prime}$ with $C=(q,p,a_{1}\ldots a_{p}\ldots a_{n})$ and $C^{\prime}=(q^{\prime},p+1,a_{1}\ldots a_{p-1},c^{\prime},a_{p+1}\ldots a_{n})$ by the term $M_{C}^{C^{\prime}}=x_{t}\,y_{p}$ with

[TABLE]

Similarly, we represent the transition $C\stackrel{{\scriptstyle t\in\delta}}{{\leadsto}}C^{\prime}$ with $C=(q,p,a_{1}\ldots a_{p}\ldots a_{n})$ and $C^{\prime}=(q^{\prime},p-1,a_{1}\ldots a_{p-1},c^{\prime},a_{p+1}\ldots a_{n})$ by the term $M_{C}^{C^{\prime}}=x_{t}\,y_{p-1}$ with

[TABLE]

Given a sequence of configurations $(q,p,s)=C_{1}\leadsto\ldots\leadsto C_{m}=(q_{f},p^{\prime},s^{\prime})$ for some $p^{\prime}\leq n$ and $s^{\prime}\in\Sigma^{n}$ let $M=M_{C_{1}}^{C_{2}}(M_{C_{2}}^{C_{3}}(\ldots(M_{C_{m-1}}^{C_{m}}\,x_{f})\ldots))$. By induction on $m$ we have $\Gamma_{i}\vdash M:a_{i}$ for $i\in[1,n]\setminus\{p\}$ and $\Gamma_{p}\vdash M:\langle q,a_{p}\rangle$.

“$\Leftarrow$”****: Assume $\Gamma_{i}\vdash M:a_{i}$ for $i\in[1,n]\setminus\{p\}$ and $\Gamma_{p}\vdash M:\langle q,a_{p}\rangle$ for some term $M$ in beta normal form (cf. [2]). We show that $(q,p,s)$ is accepting by induction on the structure of $M$. Due to $\Gamma_{p}\vdash M:\langle q,a_{p}\rangle$, we have three possible cases:

Case 1:

$M=x_{f}$. Therefore, $q=q_{f}$ and $(q,p,s)$ is accepting.

Case 2:

$M=x_{t}\,L\,N$ with $t=(q,a_{p})\mapsto(q^{\prime},c^{\prime},+1)$. We have

[TABLE]

By the induction hypothesis $(q^{\prime},p+1,a_{1}\ldots a_{p-1}c^{\prime}a_{p+1}\ldots a_{n})$ is accepting in $T$ using at most $n$ tape cells. Therefore, $(q,p,s)$ is accepting in $T$ using at most $n$ tape cells.

Case 3:

$M=x_{t}\,L\,N$ with $t=(q,a_{p})\mapsto(q^{\prime},c^{\prime},-1)$. We have

[TABLE]

By the induction hypothesis $(q^{\prime},p-1,a_{1}\ldots a_{p-1}c^{\prime}a_{p+1}\ldots a_{n})$ is accepting in $T$ using at most $n$ tape cells. Therefore, $(q,p,s)$ is accepting in $T$ using at most $n$ tape cells.

∎

In the second part of our construction we create the particular inhabitation problem to apply Lemma 1. The main idea is to use a technique similar to the encoding of expansion in expanding tape machines [5]. However, instead of introducing new functional dependencies (new machine instructions in the sense of [5]) it is sufficient to introduce type atoms that link neighboring judgements. We define the following types:

[TABLE]

Note that $\text{\textvisiblespace}\in\Sigma$ is the space symbol. Again, let us develop an intuition for the defined types:

• •

$\circ$ marks the first, \$$ the last, #$the second last and$*$ all other cells during tape expansion

• •

$\sigma_{*}$ is used for tape expansion at its end

• •

$\sigma_{0}$ initializes $T$ to the state $q_{0}$ and the empty tape replacing $\circ,*,#,$$ marks

Observe that $\operatorname{rank}(\tau_{\star})=\operatorname{order}(\tau_{\star})=3$.

Lemma 2**.**

There exists a term $M$ such that $\vdash M:\tau_{\star}$ iff there exists an $n\in\mathbb{N}$ and a term $N$ such that $\Gamma_{1}\vdash N:\langle q_{0},\text{\textvisiblespace}\rangle$ and $\Gamma_{i}\vdash N:\text{\textvisiblespace}$ for $i\in[2,n]$ where

• •

$\Gamma=\{x_{*}:\sigma_{*},x_{0}:\sigma_{0},x_{f}:\sigma_{f}\}\cup\{x_{t}:\sigma_{t}\mid t\in\delta\}$**

• •

$\Gamma_{1}=\Gamma\cup\{y_{1}:l\}\cup\{y_{j}:\bullet\mid j\in[2,n-1]\}$**

• •

$\Gamma_{i}=\Gamma\cup\{y_{i-1}:r,y_{i}:l\}\cup\{y_{j}:\bullet\mid j\in[1,n-1]\setminus\{i-1,i\}\}$* for $i\in[2,n-1]$*

• •

$\Gamma_{n}=\Gamma\cup\{y_{n-1}:r\}\cup\{y_{j}:\bullet\mid j\in[1,n-2]\}$**

Proof.

To improve accessibility of the proof, we visualize necessary/sufficient steps (according to the inhabitation algorithm given in [5]) to prove $\vdash M:\tau_{\star}$. A node $\sigma$ states that $\sigma$ is inhabited in the context described by the union of edge labels along the path from $\sigma$ to the root. Additionally, at each level of the tree the shape of inhabitants (which have to be identical due to the nature of $\cap$) is ascribed on the left. The inhabitant is therefore the composition of the ascriptions.

{\lambda(\Gamma).(\_):}$${\tau_{\star}}$${\lambda y_{1}.(\_):}$${(l\to\circ)\cap(r\to\#)\cap(\bullet\to\)}${x_{*}\,(\_):}${\circ}${\#}${$}${\lambda y_{2}.(\_):}${\bullet\to\circ}${l\to*}${(r\to#)\cap(\bullet\to$)}${x_{*}\,(\_):}${\circ}${*}${#}${\$}${\lambda y_{3}.(_):}${\bullet\to\circ}${\bullet\to*}${l\to*}${(r\to#)\cap(\bullet\to$)}${x_{*}\,(\_):}${\circ}${*}${*}${\#}${$}${\ldots}${\ldots}${\ldots}${\ldots}${\ldots}${\ldots}$\Gamma$y_{1}:l$y_{1}:r$y_{1}:\bullet$y_{2}:\bullet$y_{2}:l$y_{2}:r$y_{2}:\bullet$y_{3}:\bullet$y_{3}:\bullet$y_{3}:l$y_{3}:r$$y_{3}:\bullet$

First, the variables in $\Gamma$ and $y_{1}$ are abstracted. Next follows an arbitrary number of $x_{*}$ applications in combination with an abstraction, that increments the current width of the tree. Intuitively, $\circ$ is used to mark the first context; \$$ is used to mark the last context; #$is used to introduce consecutive$y_{i}:r$and$y_{i+1}:l$.

{x_{0}\,(\_):}$${\circ}$${*}$${\ldots}$${*}$${\#}$${\}${\lambda y_{n-1}.(\_):}${\bullet\to\langle q_{0},\text{\textvisiblespace}\rangle}${\bullet\to\text{\textvisiblespace}}${\ldots}${\bullet\to\text{\textvisiblespace}}${l\to\text{\textvisiblespace}}${r\to\text{\textvisiblespace}}${N:}{\langle q_{0},\text{\textvisiblespace}\rangle}$␣${\ldots}$␣␣␣$y_{n-1}:\bullety_{n-1}:\bullet$y_{n-1}:\bullet$y_{n-1}:l$$y_{n-1}:r$

Finally, an application of $x_{0}$ in combination with one abstraction of $y_{n-1}$, where $n$ is the current width of the tree, produces exactly $\Gamma_{1}\vdash N:\langle q_{0},\text{\textvisiblespace}\rangle$ and $\Gamma_{i}\vdash N:\text{\textvisiblespace}$ for $i\in[2,n]$, that can be verified inductively reading the edge labels along the path to the root.

Using the presented tree, we sketch the proof as follows.

“$\Rightarrow$”****: If $\tau_{\star}$ is inhabited, then we can read the tree from the root to the leaves to get necessary conditions $\Gamma_{1}\vdash N:\langle q_{0},\text{\textvisiblespace}\rangle$ and $\Gamma_{i}\vdash N:\text{\textvisiblespace}$ for $i\in[2,n]$ for some term $N$.

“$\Leftarrow$”****: If $\Gamma_{1}\vdash N:\langle q_{0},\text{\textvisiblespace}\rangle$ and $\Gamma_{i}\vdash N:\text{\textvisiblespace}$ for $i\in[2,n]$, then we can read the tree from leaves to the root to get the sufficient condition, namely the inhabitant $M$, such that $\vdash M:\tau_{\star}$. ∎

Theorem 1**.**

Intersection type inhabitation (Problem 1) is undecidable in rank $3$ and order $3$.

Proof.

Adding $x_{*}:\sigma_{*}$ and $x_{0}:\sigma_{0}$ to all contexts does not invalidate Lemma 1 because $\sigma_{*}$ and $\sigma_{0}$ work on the special atoms $\circ,*,\#$ and \$$. Therefore, by Lemma [2](#Thmlemma2) and Lemma [1](#Thmlemma1) we have that \tau_{\star}$is inhabited iff$T$ accepts the empty word. ∎

0.4 Simple Semi-Thue System Simulation

The undecidability result in Section 0.3 is of didactic interest because it shows how Turing machine computation can be simulated by proof search directly. If one is only interested in minimal requirements for undecidability, then it is helpful to consider simple semi-Thue systems.

Definition 6** (Simple Semi-Thue System).**

A semi-Thue system over an alphabet $\Sigma$, where each rule has the form $ab\Rightarrow cd$, for some $a,b,c,d\in\Sigma$, is called a simple semi-Thue system.

Problem 2**.**

Given a simple semi-Thue system $R$, is there an $n\in\mathbb{N}$ such that $0^{n}\twoheadrightarrow_{R}1^{n}$?

Lemma 3**.**

Problem 2 is undecidable.

Proof.

Reduction from the empty word halting problem for Turing machines. Turing machine computation requires at each step the modification of two neighboring cells. The unknown parameter $n$ corresponds to the required tape length. ∎

Given a simple semi-Thue system $R$ over an alphabet $\Sigma$ with \bullet,*,\#,\,l,r\not\in\Sigmawe (similarly to Section [0.3](#Ch0.S3)) construct the following types of rank and order at most3$:

[TABLE]

Lemma 4**.**

The type $\tau_{\star}$ is inhabited iff there exists an $n\in\mathbb{N}$ such that $0^{n}\twoheadrightarrow_{R}1^{n}$.

Proof.

The argumentation is the same as in the proofs of Lemma 2 and Lemma 1. The type $\sigma_{*}$ is used for initial expansion; $\sigma_{0}$ is used for initialization; $\sigma_{t}$ for transition for $t\in R$; and $\sigma_{1}$ for termination. ∎