28.5 Undecidability of Full F:

---

28.5 Undecidability of Full F_<:

We established in the previous section that the algorithmic subtyping rules for full F_<: are sound and complete—that is, that the smallest relation closed under these rules contains the same statements as the smallest relation closed under the original declarative rules. This leaves the question of whether an algorithm implementing these rules terminates on all inputs. Unfortunately—and, to many people at the time this was discovered, quite surprisingly—it does not.

28.5.1 Exercise [⋆]:

If the algorithmic rules for full F_<: do not define an algorithm that always terminates, then clearly the proof of termination for the kernel F_<: algorithm cannot be carried over to the rules for the full system. Precisely where does it break down?

Here is an example, due to Ghelli (1995), that makes the subtyping algorithm diverge. We first define the following abbreviation:

The crucial property of the ¬ operator is that it allows the left-and right-hand sides of subtyping statements to be swapped.

28.5.2 Fact:

Г ⊢ ¬S <: ¬T iff Г ⊢ T <: S.

Proof: EXERCISE [⋆⋆ ↛].

Now, define a type T as follows:

   T  =  "X<:Top. ¬("Y<:X.¬Y). 

If we use the algorithmic subtyping rules bottom-to-top to attempt to construct a subtyping derivation for the statement

we end up in an infinite regress of larger and larger subgoals:

The renaming steps necessary to maintain the well-formedness of the context when new variables are added are performed tacitly here, choosing new names so as to clarify the pattern of regress. The crucial trick is the "re-bounding" that occurs, for instance, between the second and third lines, where the bound of X₁ on the left-hand side changes from Top in line 2 to X₀ in line 3. Since the whole left-hand side in line 2 is itself the upper-bound of X₀, this re-bounding creates a cyclic pattern where longer and longer chains of variables in the context must be traversed on each loop. (The reader is cautioned not to look for semantic intuitions behind this example; in particular, ¬T is a negation only in a syntactic sense.)

Worse yet, not only does this particular algorithm fail to terminate on some inputs, it can be shown (Pierce, 1994) that there is no algorithm that is sound and complete for the original full F_<: subtype relation and that terminates on all inputs. The proof of this fact is too large for this book. However, to get a sense of its flavor, let's look at one more example.

28.5.3 Definition:

The positive and negative occurrences in a type T are defined as follows. T itself is a positive occurrence in T. If T₁→T₂ is a positive (respectively, negative) occurrence, then T₁ is a negative (resp. positive) occurrence and T₂ is a positive (negative) occurrence. If "X<:T₁.T₂ is a positive (respectively, negative) occurrence, then T₁ is a negative (resp. positive) occurrence and T₂ is a positive (negative) occurrence. The positive and negative occurrences in a subtyping statement Г ⊢ S <: T are defined as follows: the type S and the bounds of type variables in Г are negative occurrences. The type T is a positive occurrence.

The words "positive" and "negative" come from logic. According to the well-known Curry-Howard correspondence between propositions and types (§9.4), the type S→T corresponds to the logical proposition S ⇒ T, which, by the definition of logical implication, is equivalent to ¬S V T. The subproposition S here is obviously in a "negative" position—that is, inside of an odd number of negations—if and only if the whole implication appears inside an even number of negations. Note that a positive occurrence in T corresponds to a negative occurrence in ¬T.

28.5.4 Fact:

If X occurs only positively in S and negatively in T, then X<:U ⊢ S <: T iff ⊢ [X ↦ U]S <: [X ↦ U]T.

Proof: EXERCISE [⋆⋆ ↛].

Now, let T be the following type

   T  =  forall;X0<:Top. "X1<:Top. "X2<:Top.                   ¬("Y0<:X0."Y1<:X1."Y2<:X2.¬X0) 

and consider the subtyping statement

   ⊢  T  <:   "X0<:T."X1<:P."X2<:Q.               ¬("Y0<:Top."Y1<:Top."Y2<:Top.                ¬("Z0<:Y0."Z1<:Y2."Z2<:Y1.U)). 

We can think of this statement as a description of the state of a simple computer. The variables X₁ and X₂ are the "registers" of this machine. Their current contents are the types P and Q. The "instruction stream" of the machine is the third line: the first instruction is encoded in the bounds (Y₂ and Y₁—note their order) of the variables Z₁ and Z₂, and the unspecified type U is the remaining instructions in the program. The type T, the nested negations, and the bound variables X₀ and Y₀ here play much the same role as their counterparts in the simpler example above: they allow us to "turn the crank" and get back to a subgoal of the same shape as the original goal. One turn of the crank will correspond to one cycle of our machine.

In this example, the instruction at the front of the instruction stream encodes the command "switch the contents of registers 1 and 2." To see this, we use the two facts stated above to calculate as follows. (The values P and Q in the two registers are highlighted, to make them easier to follow.)

         ⊢   T         <:   "X0<:T."X1<:P."X2<:Q.              ¬("Y0<:Top."Y1<:Top."Y2<:Top.               ¬("Z0<:Y0."Z1<:Y2."Z2<:Y1.U))    iff  ⊢   ¬("Y0<:T."Y1<:P ."Y2<:Q.¬T)         <:  ¬("Y0<:Top."Y1<:Top."Y2<:Top.        by Fact 28.5.4              ¬("Z0<:Y0."Z1<:Y2."Z2<:Y1. U))    iff  ⊢   ("Y0<:Top."Y1<:Top."Y2<:Top.              ¬("Z0<:Y0."Z1<:Y2<:"Z2<:Y1. U))         <:  ("Y0<:T."Y1<:P ."Y2<:Q.¬T)           by Fact 28.5.2    iff  ⊢   ¬("Z0<:T."Z1<:Q."Z2<:P. U))         <:  ¬T                                   by Fact 28.5.4    iff  ⊢   T         <:  ("Z0<:T."Z1<:Q."Z2<:P.U))            by Fact 28.5.2 

Note that, at the end of the derivation, not only have the values P and Q switched places, but the instruction that caused this to happen has been used up in the process, leaving U at the front of the instruction stream to be "executed" next. By choosing a value of U that begins in the same way as the instruction we just executed

   U  =  ¬("Y0<:Top. "Y1<:Top. "Y2<:Top.          ¬("Z0<:Y0. "Z1<:Y2. "Z2<:Y1.U')) 

we can perform another swap and return the registers to their original state before continuing with U′. Alternatively, we can choose other values for U that cause different sorts of behavior. For example, if

   U  =  ¬("Y0<:Top. "Y1<:Top. "Y2<:Top.          ¬("Z0<:Y0. "Z1<:Y1. "Z2<:Y2. Y1)) 

then, on the next cycle of the machine, the current value of register 1, i.e., Q, will appear in the position of U—in effect, performing an "indirect branch" through register 1 to the stream of instructions represented by Q. Conditional constructs and arithmetic (successor, predecessor, and zero-test) can be encoded using a generalization of this trick.

Putting all of this together, we arrive at a proof of undecidability via a reduction from two-counter machines—a simple variant on ordinary Turing machines, consisting of a finite control and two counters, each holding a natural number—to subtyping statements.

28.5.5 Theorem [Pierce, 1994]:

For each two-counter machine M, there exists a subtyping statement S(M) such that S(M) is derivable in full F_<: iff the execution of M halts.

Thus, if we could decide whether any subtype statement is provable, then we could also decide whether any given two-counter machine will eventually halt. Since the halting problem for two-counter machines is undecidable (cf. Hopcroft and Ullman, 1979), so is the subtyping problem for full F_<:.

We should emphasize, again, that the undecidability of the subtype relation does not imply that the semi-algorithm for subtyping developed in §28.4 is either unsound or incomplete. If the statement Г ⊢ S <: T is provable according to the declarative subtyping rules, then the algorithm will definitely terminate and yield true. If Г ⊢ S <: T is not provable according to the declarative subtyping rules, then the algorithm will either diverge or yield false. The point is that a given subtyping statement may fail to be provable from the algorithmic rules in two different ways: either by generating an infinite sequence of subgoals (meaning that there is no finite derivation with this conclusion) or else by leading to an obvious inconsistency like Top <: S→T. The subtyping algorithm can detect one of these cases, but not the other.

Does the undecidability of full F_<:: mean that the system is useless in practice? Actually, it is generally held that the undecidability of F_<:: is not, per se, a terribly serious deficiency. For one thing, it has been shown (Ghelli, 1995) that, in order to cause the subtype checker to diverge, we must present it with a goal with three quite special properties, each one of which is difficult to imagine programmers creating by accident. Also, there are a number of popular languages whose typechecking or type reconstruction problems are, in principle, either extremely expensive—like ML and Haskell, as we saw in §22.7—or even undecidable, like C++ and λProlog (Felty, Gunter, Hannan, Miller, Nadathur, and Scedrov, 1988). In fact, experience has shown the lack of joins and meets mentioned in the following section (cf. Exercise 28.6.3) to be a significantly more problematic shortcoming of full F_<::than its undecidability.

28.5.6 Exercise [⋆⋆⋆⋆]:

(1) Define a variant of full F_<: with no Top type but with both X<:T and X bindings for variables (i.e., with both bounded and unbounded quantification); this variant is called completely bounded quantification. (2) Show that the subtype relation for this system is decidable. (3) Does this restriction offer a satisfactory solution to the basic problems raised in this section? In particular, does it work for languages with additional features such as numbers, records, variants, etc.?

---