Polymorphic Subtyping Without Distributivity

Jacek Chrząszcz

10th March 1998

Abstract The subtyping relation in the polymorphic second-order λ-calculus was introduced by John C. Mitchell in 1988. It is known that this relation is undecidable, but all known proofs of this fact strongly depend on the distributivity axiom. Nevertheless it has been conjectured that this axiom does not influence the undecidability.

The present paper shows undecidability of subtyping when we remove distributivity from its definition. Furthermore, the full equational axiomatisation of the corresponding equivalence relation is given. Both results follow from an analysis of rewriting-style subtyping derivations.

1 Introduction

Polymorphism is one of the most important issues in modern programming. When we go beyond the limits of shallow polymorphism imposed by common functional languages like ML or Haskell, we encounter (among others) the following question: when can values of a given type σ replace values of type τ without a type clash, or, differently speaking, is σ a subtype of τ?

In the higher-order polymorphic functional language, system F, the subtyping relation is characterized by:

∀α_{1} … α_{n} σ ⊑_{F} ∀β_{1} … β_{m} σ{α_{1} ↦ ρ_{1}, …, α_{n} ↦ ρ_{n}}  (1)

where β_{1}, …, β_{m} are not free in ∀α_{1} … α_{n} σ, and ρ_{1}, …, ρ_{n} are arbitrary types. But this relation is not strong enough. One can see for example that when σ ⊑_{F} σ′ then terms of type τ → σ can very well replace those of type τ → σ′. Therefore John C. Mitchell in [Mit88] extended the notion of subtyping to a containment relation ⊑_{M}. It is defined by four axioms and three rules. The axioms are: reflexivity, quantifier instantiation, generalization (adding an empty quantifier), and quantifier distributivity over an arrow. The rules ensure transitivity and a particular closure by context. The particularity lies within the rule concerning the arrow symbol:

σ_{1} → τ_{1} ⊑_{M} σ_{2} → τ_{2} if σ_{2} ⊑_{M} σ_{1} and τ_{1} ⊑_{M} τ_{2}

Adding a subsumption rule for ⊑_{M}

\frac{E ⊢ M : σ σ ⊑_{M} τ}{E ⊢ M : τ}

properly extends System F. Unfortunately the resulting system F_{η} has all the bad undecidability properties of system F. Typability and type-checking are undecidable in both systems (see [Wel94] for F and [Wel96] for typability and [TU95] for type-checking in F_{η}) and so is Mitchell subtyping relation [TU95] (see also [Wel95] for alternative proof).

The solution for designers of functional languages with full polymorphism is to seek for non-trivial decidable subrelations of ⊑_{M}. And to do this it is essential to understand what exactly makes this relation undecidable.

The present paper analyses the subtyping relation when we remove distributivity from its definition. This axiom seems to be the least intuitive while the subtyping relation without it remains quite powerful and useful.

Both known undecidability proofs strongly depend on the distributivity axiom. Tiuryn and Urzyczyn [TU95] encode computations of a certain device called stack register machine with undecidable halting problem. The encoding is based on subtyping derivations in Longo-Milsted-Soloviev system [LMS95], which deeply incorporates the distributivity axiom.

Another approach is taken by Wells [Wel95], who reduces the well known semi-unification problem to subtyping. Having two pairs of types σ_{1}, τ_{1} and σ_{2}, τ_{2}, the author constructs a universal type Π(δ_{1}, ζ_{1}, δ_{2}, ζ_{2}) such that if γ⃗ are all variables in σ_{1}, τ_{1}, σ_{2}, τ_{2} then

∀β (Π(β, β, β, β) → ⊥) ⊑_{M} (∀γ⃗ Π(σ_{1}, τ_{1}, σ_{2}, τ_{2})) → ⊥

if and only if σ_{1}, τ_{1} and σ_{2}, τ_{2} are semi-unifiable. The distributivity axiom plays a crucial role in this proof. Intuitively after performing common substitution, it is the only way to separate quantifiers and therefore apply two separate substitutions yielding σ_{1}θθ_{1} = τ_{1}θ and σ_{2}θθ_{2} = τ_{2}θ.

Our work proves that removing distributivity does not suffice to obtain a decidable subtyping relation.

The undecidablility result is based on a reduction similar to that in the work of Tiuryn and Urzyczyn. Instead of using Longo-Milsted-Soloviev system we define a type rewriting system (like in [Tiu95]) which is a straightforward translation of original Mitchell axioms. Each rewriting step is an application of instantiation or generalisation axioms, some of them being applications backwards because of the symbol → which is anti-monotonic in the first argument.

The rewriting and its correspondence with the subtyping axiomatisation is given in Section 3. Then it is shown that rewriting derivations can be normalized, i.e. the steps can be rearranged so that all positive steps precede the negative ones. Using normal derivations we characterize in Section 6 the equivalence relation induced by the new subtyping preorder. Its equational axiomatization is given, similar to the one given by Tiuryn [Tiu95] for the full Mitchell subtyping relation.

Section 7 introduces yet another class of derivations, ordered ones, which are normal derivations where rewriting takes place from the root towards the leaves in the positive phase, and the other way in the negative ones. It is somewhat similar to Wells’s syntax-driven system [Wel95], but using rewriting helps keeping all proof information in one piece.

Ordered derivations constitute a very useful tool to prove subtyping properties necessary to encode computations of a stack register machine (Section 9). Finally, in Section 10 we conclude the paper with some sugestions on how else a decidable subtyping relation could be found.

2 Notation

We work with polymorphic types (like in system F), defined over the denumerable set of variables V by the following grammar:

T ::= V | ∀V T | T → T

Variables appearing in types are denoted by the initial Greek letters α, β, γ, sequences of quantified variables by δ⃗, ζ⃗, ϑ⃗, and types by other Greek letters like σ, τ, ρ… Often we abbreviate ∀α∀β τ as ∀αβ τ. We admit that quantifiers bind stronger than the operator →, and we use the symbol ⊥ to denote the type ∀α α.

The number of arrows appearing in a given type is called its weigth. The inductive definition follows:

weight(α) = 0
weight(∀α σ) = weight(σ)
weight(σ_{1} → σ_{2}) = weight(σ_{1}) + weight(σ_{2}) + 1

Because of quantifiers, variables occuring in a given type may be either bound or free, that is not bound by any quantifier. For a given type σ, the set of all free variables occuring in it is denoted by F V (σ). Formally we define:

F V (α) = {α}
F V (σ_{1} → σ_{2}) = F V (σ_{1}) ∪ F V (σ_{2})
F V (∀β σ) = F V (σ) \ {β}

Types which differ only in the names of bound variables are considered to be equal. Furthermore we assume that in each type the names of bound variables are distinct and different from the names of free ones.

A partial function of a finite domain from the set of variables V to the set of types T is called a substitution. It can be extended in a natural way to a function from T to T . Application of a substitution θ to a type σ is written in postfix notation as σθ. If θ assigns a type τ_{i} to variables α_{i} for all i and is undefined for other variables, we write θ = {α_{1} ↦ τ_{1}, …, α_{n} ↦ τ_{n}}. If necessary we rename bound variables in σ to ensure that free variables in the inserted types τ_{1}, …, τ_{n} remain free in σθ. In our notation substitutions bind stronger than quantifiers, so in the type ∀β σ{α ↦ ξ} the free occurences of β in the type ξ will be bound by the quantifier ∀β.

Polimorphic types may also be regarded as labelled trees. Leaves are labelled by variables, internal nodes by → symbols and each node is labelled by a finite sequence of quantifiers. The set of positions in such a tree can be identified with a finite set of finite chains over the alphabet {0, 1}. We define the sign of a given position p to be positive if p contains even number of zeros, and negative otherwise. The empty chain is denoted by ϵ, and given two chains p, r their concatenation is writen as pr.

Positions can be compared by two different partial orders. The prefix order is denoted ≤, and the notation p ≹ r means that p and r are not comparable. The other order is the lexicographic order ⪯ induced by 0 ≺ 1.

If σ is a type and p a position in the tree of σ, then we denote by σ|_{p} a subtree at the position p. If σ and ϱ are types and p is a position in the tree of σ then σ[ϱ]_{p} stands for σ with the subtree at position p replaced by ϱ. Unlike a substitution, this operation may make some free variables in ϱ bound by quantifiers in σ.

3 Subtyping relation

The relation of subtyping ⊑ is defined by 3 axioms and 3 rules:

(refl) σ ⊑ σ
(inst) ∀α σ ⊑ σ{α ↦ ρ}
(quant) σ ⊑ ∀α σ if α ∉ F V (σ)

Rules:

(→-context) \frac{σ_{2} ⊑ σ_{1} τ_{1} ⊑ τ_{2}}{σ_{1} → τ_{1} ⊑ σ_{2} → τ_{2}}
(∀-context) \frac{σ ⊑ τ}{∀α σ ⊑ ∀α τ}
(trans) \frac{σ ⊑ ρ ρ ⊑ τ}{σ ⊑ τ}

Our definiton differs from the original one introduced by Mitchell in [Mit88] in the lack of the distributivity axiom:

(distr) ∀α(σ → τ) ⊑_{M} σ → ∀α τ if α ∉ F V (σ)

4 Type rewriting

For technical reasons instead of the derivations in the above system we use type rewriting according to the following rules:

\begin{aligned}C^{+}[∀α σ]_{p} & =^{p} ⟹_{i}^{+} & C^{+}[σ\{α ↦ ρ\}]_{p} \\ C^{+}[σ]_{p} & =^{p} ⟹_{q}^{+} & C^{+}[∀α σ]_{p} \\ & & if α ∉ F V (σ) \end{aligned}  \begin{aligned}C^{−}[σ\{α ↦ ρ\}]_{r} & =^{r} ⟹_{i}^{−} & C^{−}[∀α σ]_{r} \\ C^{−}[∀α σ]_{r} & =^{r} ⟹_{q}^{−} & C^{−}[σ]_{r} \\ & & if α ∉ F V (σ) \end{aligned}

where C^{+}[ ]_{p} and C^{−}[ ]_{r} denote contexts with a hole at a positive position p and negative position r respectively. When we do not want to precise what step is considered, we omit the appropriate decoration and write for example ⟹_{i} or ⟹^{+}. Any finite number of steps may be denoted by a double arrow ⟹ ⟹. Given a derivation step σ → τ, the absolute value of the difference of weights of σ and τ is called the weight of this step. Intuitively, it is the number of arrows introduced (or removed) by this step.

The meaning of the introduced rewriting is expressed by the following lemma:

Lemma 4.1 For any types σ and τ we have:

σ ⊑ τ if and only if σ ⟹ ⟹ τ

Proof. Both implications can easily be proved by a routine induction. ■

5 Normal derivations

The goal of the present section is to show that every subtyping inequality can be proved by a normal derivation, that is a sequence of positive steps (which increase the weight of a type) followed by a sequence of negative steps.

Definition 5.1 (normal derivation)

A derivation σ ⟹ ⟹ τ is called normal, if it is of the form σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ for certain type ρ.

The weight of a normal derivation is the sum of weights of steps in it. It is easy to see that it is equal 2 × weight(ρ) − weight(σ) − weight(τ).

Before we show how to normalise a given derivation, we define the notion of safe steps.

Definition 5.2 (safe step) A rewriting step σ ⟹ τ is safe, if one of the following conditions is satisfied:

1. it is a ⟹_{q} step;

2. it is a ⟹_{i} step, in which the inserted type is ⊥;

3. it is a =^{p} ⟹_{i} step, in which the inserted type is a variable β bound at a position p′ ≤ p, of the same sign as the sign of p.

The second condition above covers particularly the instatiation of empty quantifiers, i.e. the steps C^{+}[∀α σ] ⟹_{i}^{+} C^{+}[σ] and respectively C^{−}[σ] ⟹_{i}^{−} C^{−}[∀α σ] for α ∉ F V (σ).

The last condition of the safe step definition expresses the following situations:

C^{+}[∀β C^{+}[∀α σ]] ⟹_{i}^{+} C^{+}[∀β C^{+}[σ{α ↦ β}]]
C^{−}[∀β C^{+}[σ{α ↦ β}]] ⟹_{i}^{−} C^{−}[∀β C^{+}[∀α σ]]

All safe steps have the weight 0. In addition, a safe step can be inserted in the derivation without changing its weight. The formal statement of this property, together with an example of a step of weight 0 which is not safe will be given by the end of the section.

The following lemma shows how to permute negative and positive steps,^{1} which is necessary to normalise a derivation.

Lemma 5.3 (permuting negative and positive steps)

Let σ and τ be types such that σ ⟹^{−} ρ ⟹^{+} τ. There exists a type ρ′ such that σ ⟹^{+} ρ′ ⟹^{−} τ. In addition if the step σ ⟹^{−} ρ is safe then after the permutation the step ρ′ ⟹^{−} τ will remain safe and similarily if ρ ⟹^{+} τ is a safe step then so will be σ ⟹^{+} ρ′.

Proof. Let σ =^{p} ⟹^{−} ρ =^{r} ⟹^{+}. Depending on p and r we have three possibilities to consider:

• p ≹ r — this case is easy;

• p < r, r = ps. If both steps are q-steps then it is obvious. If we have one q-step and one i-step, then it does not pose any problems either. The type inserted by the i-step is unchanged so safe steps remain safe.

If both steps are i-steps then we have

σ = σ[∀δ⃗ ϱ[∀ζ⃗β υ]_{s}{α ↦ ξ_{α}}]_{p}  =^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{s}]_{p}
=^{r} ⟹_{i}^{+} σ[∀δ⃗α ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{s}]_{p} = τ

We know that β ∉ F V (ξ_{α}), but α may occur in ξ_{β}. Assigning ϱ̄ = ϱ{α ↦ ξ_{α}} and ῡ = υ{α ↦ ξ_{α}}, we can swap these steps in the following way:

σ = σ[∀δ⃗ ϱ̄[∀ζ⃗β ῡ]_{s}]_{p}  =^{r} ⟹_{i}^{+} σ[∀δ⃗ ϱ̄[∀ζ⃗ ῡ{β ↦ ξ_{β}{α ↦ ξ_{α}}}]_{s}]_{p}
= σ[∀δ⃗ ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{s}{α ↦ ξ_{α}}]_{p}
=^{p} ⟹_{i}^{−} σ[∀δ⃗α ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{s}]_{p} = τ

the middle equality being a simple property of substitution. If the negative step was safe, it will remain safe since the type ξ_{α} does not change. If the positive step was safe, then ξ_{β} = ⊥ or ξ_{β} = γ for a variable γ bound at a positive position; in both cases α ∉ F V (ξ_{β}), so ξ_{β}{α ↦ ξ_{α}} = ξ_{β};

• p > r. This situation is dual to the previous one. Given the derivation σ =^{p} ⟹^{−} ρ =^{r} ⟹^{+} τ it suffices to consider

τ → ⊥ =^{0r} ⟹^{−} ρ → ⊥ =^{0p} ⟹^{+} σ → ⊥

where of course 0r < 0p. ■

Lemma 5.4 Given two types σ and τ such that σ ⊑ τ, there exists a normal derivation σ ⟹ ⟹^{+} ⟹ ⟹^{−} τ.

Proof. Since by Lemma 4.1 there exists a derivation σ ⟹ ⟹ τ, it suffices to use Lemma 5.3 appropriate numer of times in order to obtain a normal derivation. ■

After proving the above very important fact we can define the weight of an inequality.

Definition 5.5 (weight of inequality)

Weight of an inequality σ ⊑ τ is the minimal weight of its normal derivations σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ.

Now we can formally explain the meaning of the safe steps

Proposition 5.6 Let σ_{1} ⊑ τ and let σ_{0} ⟹ σ_{1} be a safe step. Then the weight of the inequality σ_{0} ⊑ τ is no greater than the weight of the inequality σ_{1} ⊑ τ.

Proof. This proposition is a straightforward consequence of Lemma 5.3. ■

Let us give an example of a rewriting step of weight 0, which is not safe. Consider the following one-step derivation of weight weight(ξ):

∀α (∀β (⊥ → β) → α) =^{ϵ} ⟹_{i}^{+} ∀β (⊥ → β) → ξ

If we precede it by the zero-weight step

∀α ((⊥ → α) → α) = ∀α ((⊥ → β){β ↦ α} → α) =^{0} ⟹_{i}^{−} ∀α (∀β (⊥ → β) → α)

we get the derivation which is not normal. The first step is not safe, because the variable α is bound at a positive position ϵ and not negative, like the variable β. After the permutation of these steps, according to Lemma 5.3, we get the derivation

∀α ((⊥ → α) → α) =^{ϵ} ⟹_{i}^{+} ((⊥ → ξ) → ξ) =^{0} ⟹_{i}^{−} ∀β (⊥ → β) → ξ

Its weight is equal 3 × weight(ξ), that is more than the weight of the primary positive step, if only weight(ξ) > 0.

6 Bicoercible types

Types σ and τ are called bicoercible if σ ⊑ τ and τ ⊑ σ. We show in the present section, that the bicoercibility relation may be identified with the least congruence containing the axioms

(B1) ∀α∀β σ ∼ ∀β∀α σ

(B2) ∀α σ ∼ σ{α ↦ ⊥} (if all occurences of α in σ are positive)

The equivalence relation induced by the original Mitchell system was characterized by Tiuryn in [Tiu95]. It is defined by axioms (B1), (B2) and the axiom

order of the steps ∀α α =^{ϵ} ⟹_{i}^{+} (β → β) → β =^{0} ⟹_{i}^{−} (∀α α) → β

1A permutation the other way is not always possible. One cannot for example change the

(B3) ∀α (σ_{1} → σ_{2}) ∼_{M} σ_{1} → ∀α σ_{2} (jeűli α ∉ F V (σ_{1}))

which is not true in our system.^{2} The rest of the present section is devoted to the proof that a relation ∼ defined as the least congruence containing axioms (B1) and (B2) is the equivalence relation induced by the quasi-order ⊑. To prove this we introduce the notion of reversible steps.

Definition 6.1 (reversible step)

A single rewriting step σ ⟹ τ is called reversible, if τ ⊑ σ.

Lemma 6.2 Let σ ⟹_{i}^{+} τ and let p and r be such that σ|_{pr} = ∀δ⃗ α, where α is bound at a positive position p. If the position pr in τ is not an occurence of a variable bound at a positive position, then the step σ ⟹_{i}^{+} τ is not reversible.

Proof. Suppose the step σ ⟹_{i}^{+} τ is reversible. Then there exists a normal derivation τ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ.

If τ|_{pr} = ∀ζ⃗ β, where β is free or bound at a negative position, then ρ|_{pr} = ∀ϑ⃗ β as well, because during the positive phase of a derivation negative variables are not instantiated, and free variables cannot be instantiated at all.

If τ|_{pr} = ∀ζ⃗ (ξ_{1} → ξ_{2}), for some ξ_{1}, ξ_{2}, then similarily ρ|_{pr} = ∀ϑ⃗ (ξ′_{1} → ξ′_{2}) (for some ξ′_{1}, ξ′_{2}), because during the positive phase the weight of types does not decrease.

In both cases ρ|_{pr} is not a variable bound at a positive position. It follows that neither is σ|_{pr}, because negative steps ⟹_{q}^{−} do not change variable bindings, and the steps ⟹_{i}^{−} do not create new variables bound at positive positions, a contradiction. ■

The next lemma uses the following notation. Let σ be a type such that a position s is an occurence of a variable α bound by a quantifier at a position p (of course p ≤ s). We denote by Π_{σ}(s) the set of positions of all occurences of the variable α (bound by the quantifier ∀α at position p) in the type σ. If the type is clear from the context, the index σ will be omitted.

Lemma 6.3 Let σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ be a normal derivation of the inequality σ ⊑ σ. Let p be a positive position and r such that pr is a negative position and σ|_{pr} = ∀ϑ⃗ α, where α is a variable bound at a positive position p. Then in every type in the derivation σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ, the position pr is an occurence of a variable bound by a quantifier at the position p and the set Π(pr) does not change.

Proof. All steps in the considered derivation σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} σ are of course reversible. The shape of type and the sign of variable bindings cannot be changed by positive steps, according to Lemma 6.2. By a similar argument neither can they be changed by negative steps, so they remain constant during the entire derivation.

Consider a the possible influence of a single positive step =^{s} ⟹_{i}^{+}, accepted by Lemma 6.2, on the binding position of the variable α and the set Π(pr)

2It is not true that ∀α (β → (α → β)) ∼ β → ∀α (α → β)

• if s ≹ p, the step does not have any influence on the variable α;

• if s ≤ p and the quantifier ∀α at position p lies within the range of the instantiated quantifier, then the instantiation has no influence on α;

• if s = p and ∀α is the instantiated quantifier, then the binding position can be changed into some positive p′ such that p = p′r′ for some r′

σ_{i}[∀δ⃗β ϱ[∀ζ⃗α υ]_{r′}]_{p′} =^{p} ⟹_{i}^{+} σ_{i}[∀δ⃗β ϱ[∀ζ⃗υ{α ↦ ∀ϑ⃗ β}]_{r′}]_{p′} = σ_{i+1}

• if s ≥ p and the instantiated quantifier lies within the range of ∀α, then the set Π(pr) can increase (we assume s = pr′′ for some r′′)

σ_{i}[∀ζ⃗α υ[∀δ⃗γ χ]_{r′′}]_{p} =^{s} ⟹_{i}^{+} σ_{i}[∀ζ⃗α υ[∀δ⃗ χ{γ ↦ ∀ϑ⃗ α}]_{r′′}]_{p} = σ_{i+1}

According to this, the set Π(pr) cannot be decreased nor can the binding position be turned into a bigger one in the prefix order. Since negative steps do not influence variables bound at positive positions, the binding position of α and the set Π(pr) remain unchanged. ■

Lemma 6.4 If σ ⟹ τ is a reversible step then the statement σ ∼ τ can be derived from the axioms (B1) and (B2).

Proof. If the step σ ⟹ τ is a q-step then it suffices to use the (B2) axiom. Otherwise it is an i-step. Assume it is a positive step

σ = σ[∀δ⃗α ϱ]_{p} =^{p} ⟹_{i}^{+} σ[∀δ⃗ϱ{α ↦ ξ}]_{p} = τ

If α ∉ F V (ϱ), we can use the (B2) axiom as above.

Let us suppose that α ∈ F V (ϱ). By Lemma 6.2 we obtain that ξ = ∀α_{1} … α_{n} β, where β is either one of the variables α_{1}, …, α_{n}, or another variable bound at a positive position.

If β = α_{i} for some i, then by Lemma 6.2 the variable α may have only positive occurences in ϱ. In this case we can use the axiom (B2) to put ⊥ in all occurences, and then add missing quantifiers, by the appropriate number of (B2) applications.

Otherwise β is another variable bound at a positive position p′, where p = p′r′ for some r′. By Lemma 6.3 either p′ = p and β ∉ F V (ϱ) or all occurences of α and β are positive. In the first case we have to permute quantifiers at a position p by multiple application of the (B1) axiom and then eliminate the unnecessary ∀β quantifier by (B2), yielding a type that needs only a renaming of α to β.

In the second case we first replace all occurences of the variables α and β with ⊥ by the (B2) axiom, and then by using the same axiom “the other way” we turn every inserted type ⊥ into a new variable γ quantified by a new quantifier ∀γ at a position p′. It remains to add missing empty quantifiers ∀α_{1} … α_{n} where necessary and finally change the name of the bound variable γ back to β.

Since the same reasoning can be repeated for negative reversible σ ⟹_{i}^{−} τ step, we conclude that for every reversible step σ ⟹ τ, we can prove σ ∼ τ using (B1) and (B2) axioms. ■

Lemma 6.5 If the statement σ ∼ τ can be proved by a single use of the axiom (B1) or (B2) then σ ⟹ ⟹ τ and τ ⟹ ⟹ σ. Moreover these derivations use only safe steps.

Proof. We have to consider four possibilities, depending on what axiom was used and what was the position sign. Since most of the reasoning is simple we will analyse only the case where the axiom (B2) was used at a positive position p

σ = σ[∀δ⃗α ϱ]_{p} ∼ σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p} = τ

The derivation from left to right can be done by a single i-step. Constructing a derivation from right to left is more complicated. Let r_{1}, …, r_{n} be all occurences of α in ϱ. For all i we have ϱ{α ↦ ⊥}|_{r_{i}} = ∀ζ⃗_{i}⊥ = ∀ζ⃗_{i}β β, so

σ[∀δ⃗ ϱ{α ↦ ⊥}]_{p}  =^{p} ⟹_{q}^{+} σ[∀δ⃗γ ϱ{α ↦ ⊥}]_{p}
=^{pr_{1}} ⟹_{i}^{+} σ[∀δ⃗γ ϱ{α ↦ ⊥}[∀ζ⃗_{1} γ]_{r_{1}}]_{p} ⋮
=^{pr_{n}} ⟹_{i}^{+} σ[∀δ⃗γ ϱ{α ↦ ⊥}[∀ζ⃗_{1} γ]_{r_{1}} ⋯ [∀ζ⃗_{n} γ]_{r_{n}}]_{p}
=  σ[∀δ⃗γ ϱ{α ↦ γ}]_{p}
≡  σ[∀δ⃗α ϱ]_{p}

where γ is fresh. All steps =^{pr_{i}} ⟹_{i}^{+} are correct and safe because every r_{i} is positive, and the inserted variable γ is bound at a positive position p.

The other cases are left to the reader. ■

Theorem 1 (characterization of bicoercibility)

Inequalities σ ⊑ τ and τ ⊑ σ are both true if and only if σ ∼ τ.

Proof. If both inequalities σ ⊑ τ and τ ⊑ σ are true, then there exists a normal derivation σ ⟹ ⟹^{+} ⟹ ⟹^{−} τ containing only reversible steps. By Lemma 6.4 we have σ ∼ τ.

The opposite implication is also elementary. If σ ∼ τ, then by Lemma 6.5 and transitivity of ⊑ we obtain σ ⊑ τ and τ ⊑ σ. ■

The property of bicoercible types, that will be used in consecutive sections is stated by the next proposition.

Proposition 6.6 If σ_{0} ∼ σ_{1} and σ_{1} ⊑ τ then the inequality σ_{0} ⊑ τ also holds and the weights of both inequalities are the same.

Proof. This proposition is an easy consequence of Lemma 6.5 and Proposition 5.6. ■

7 Ordered derivations

In order to show the properties of ⊑ which will be directly used in the undecidability proof, we will use the ordered version of normal derivations. Intuitively, positive rewriting steps will be ordred by their positions compared with the lexicographic ordering (induced by 0 ≺ 1). At one position, all q-steps will precede i-steps ordered from outermost to innermost. Negative steps will be ordered dually. The rewriting will then take place first at positive postion from the root towards the leaves, and then at negative positions, from the leaves upwards.

Definition 7.1 (ordered derivations)

A sequence of positive steps σ_{0} =^{p_{1}} ⟹^{+} ⋯ =^{p_{n}} ⟹^{+} σ_{n} is ordered if the following conditions are satisfied:

1. for all i, j if i < j then p_{i} ⪯ p_{j};

2. for any given p, =^{p} ⟹_{q}^{+} steps precede =^{p} ⟹_{i}^{+} steps;

3. there are no pairs of steps

σ_{j}[∀δ⃗ α ζ⃗β ϱ]_{p}  =^{p} ⟹_{i}^{+} σ_{j}[∀δ⃗ α ζ⃗ ϱ{β ↦ ξ_{β}}]_{p}
=^{p} ⟹_{i}^{+} σ_{j}[∀δ⃗ ζ⃗ ϱ{β ↦ ξ_{β}}{α ↦ ξ_{α}}]_{p}

A sequence of negative steps τ_{0} ⟹^{−} ⋯ ⟹^{−} τ_{n} is ordered, if the dual sequence of positive steps τ_{n} → γ ⟹^{+} ⋯ ⟹^{+} τ_{0} → γ (for γ fresh) is ordered.

A normal derivation σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ is called ordered if both sequences σ ⟹ ⟹^{+} ρ and ρ ⟹ ⟹^{−} τ are ordered.

We will prove now that all derivations may be ordered. We need the following key lemma.

Lemma 7.2 If a two-step sequence σ =^{p} ⟹^{+} ρ =^{p′} ⟹^{+} τ is not ordered, then there exists a type ρ′ such that the derivation σ ⟹^{+} ρ′ ⟹^{+} τ is ordered.

Proof. In most cases we can easily permute rewriting steps. The only difficulty arises when we have two i-steps and p′ is a prefix of p. Let r be such that pr = p′ (possibly r = ϵ). We have

σ = σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{r}]_{p′}  =^{p} ⟹_{i}^{+} σ[∀δ⃗α ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{r}]_{p′}
=^{p′} ⟹_{i}^{+} σ[∀δ⃗ ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{r}{α ↦ ξ_{α}}]_{p′} = τ

Using the fact that υ{β ↦ ξ_{β}}{α ↦ ξ_{α}} = υ{α ↦ ξ_{α}}{β ↦ ξ_{β}{α ↦ ξ_{α}}} and assigning \overline{ϱ} = ϱ\{α ↦ ξ_{α}\} and \overline{υ} = υ\{α ↦ ξ_{α}\} we can do the following

σ = σ[∀δ⃗α ϱ[∀ζ⃗β υ]_{r}]_{p′}  =^{p} ⟹_{i}^{+} σ[∀δ⃗ ϱ[∀ζ⃗β υ]_{r}{α ↦ ξ_{α}}]_{p′}
= σ[∀δ⃗ \overline{ϱ}[∀ζ⃗β \overline{υ}]_{r}]_{p′}
=^{p′} ⟹_{i}^{+} σ[∀δ⃗ \overline{ϱ}[∀ζ⃗ \overline{υ}\{β ↦ ξ_{β}\{α ↦ ξ_{α}\}\}]_{r}]_{p′}
= σ[∀δ⃗ ϱ[∀ζ⃗ υ{β ↦ ξ_{β}}]_{r}{α ↦ ξ_{α}}]_{p′} = τ
■

Lemma 7.3 (ordering derivations)

If σ ⊑ τ, then there exists an ordered derivation σ ⟹ ⟹^{+} ⟹ ⟹^{−} τ, of weight equal to the weight of the inequality.

Proof. According to Lemma 7.2, we conclude that any sequence of positive steps may be ordered. Using the dual method, we can order the negative steps as well.

Let σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ be a normal derivation of the inequality σ ⊑ τ of minimal weight. Ordering of positive and negative steps do not change the type ρ, so the weight of the derivation σ ⟹ ⟹^{+} ρ ⟹ ⟹^{−} τ equal 2 × weight(ρ) − weight(σ) − weight(τ) does not change. ■

8 Decomposing inequalities

The present section shows the properties of ⊑ that will be directly used in the proof of undecidability.

Lemma 8.1 Let σ ⊑ τ and let σ|_{p} = ϱ_{σ} and τ|_{p} = ϱ_{τ} be subterms such that no variable that is free in ϱ_{σ} (resp. in ϱ_{τ}) is bound in σ (resp. τ). If p is positive, then ϱ_{σ} ⊑ ϱ_{τ} and if p is negative then ϱ_{τ} ⊑ ϱ_{σ}.

Proof. Let σ = σ_{0} =^{p_{1}} ⟹^{+} ⋯ =^{p_{n}} ⟹^{+} σ_{n} = τ_{m} =^{q_{m}} ⟹^{−} ⋯ =^{q_{1}} ⟹^{−} τ_{0} = τ be an orderd

derivation of the inequality σ ⊑ τ. Suppose p is positive. Since the sequences p_{1}, …, p_{n} and q_{1}, …, q_{m} are lexicographically ordered, each phase of the derivation can be divided into three parts. Consider the positive phase.

First there come steps at positions p_{1}, …, p_{k−1} smaller then p. They do not influence the subterm at a positon p since no free variable of ϱ_{σ} is bound above. Then there come all steps at positions p_{k}, …, p_{k′} which have p as a prefix. They can be seen as a derivation issued from ϱ_{σ}. The only problem arises when some variable in an inserted type gets bound by a quantifier above p. But since this quantifier cannot be instantiated (the derivation is ordered) this variable has to be removed by some negative steps. Hence we can replace a bound variable by a free one, because in any case it will be removed.

The last sequence of steps, at positions p_{k′+1}, …, p_{n}, has no influence on the subtype at position p. An analogous partition can be done with the negative phase, so the middle parts of each phase form a desired derivation ϱ_{σ} ⟹ ⟹ ϱ_{τ} (or the other way if p is negative). ■

Lemma 8.2 The inequality σ′ → σ′′ ⊑ τ′ → τ′′ holds if and only if both inequalities σ′ ⊒ τ′ and σ′′ ⊑ τ′′ hold. Moreover, if all inequalities are true then the weight of the first one is equal to the sum of weights of the others.

Proof. The implication from left to right is an easy consequence of the rule (→-context) and from right to left — of the last lemma.

The second statement of the lemma is also easy. Having two normal deriva-

tions of minimal weight τ′ = τ′_{0} =^{t_{1}} ⟹^{+} ⋯ =^{t_{k}} ⟹^{+} τ′_{k} = σ′_{l} =^{u_{l}} ⟹^{−} ⋯ =^{u_{1}} ⟹^{−} σ′_{0} = σ′

and σ′′ = σ′′_{0} =^{p_{1}} ⟹^{+} ⋯ =^{p_{n}} ⟹^{+} σ′′_{n} = τ′′_{m} =^{q_{m}} ⟹^{−} ⋯ =^{q_{1}} ⟹^{−} τ′′_{0} = τ′′ we can combine

them (reversing the steps of the first one) into

\begin{aligned}& σ′_{0} → σ′′_{0} =^{0u_{1}} ⟹^{+} ⋯ =^{0u_{l}} ⟹^{+} σ′_{l} → σ′′_{0} =^{1p_{1}} ⟹^{+} ⋯ =^{1p_{n}} ⟹^{+} σ′_{l} → σ′′_{n} & = \\ = & τ′_{k} → τ′′_{m} =^{1q_{m}} ⟹^{−} ⋯ =^{1q_{1}} ⟹^{−} τ′_{k} → τ′′_{0} =^{0t_{k}} ⟹^{−} ⋯ =^{0t_{k}} ⟹^{−} τ′_{0} → τ′′_{0} \end{aligned} (2)

So the weight of the inequality σ′ → σ′′ ⊑ τ′ → τ′′ is no greater than the sum of weights of σ′ ⊒ τ′ and σ′′ ⊑ τ′′. We will now show that it cannot be smaller either.

Let us take an ordered derivation of minimal weight of the inequality σ′ → σ′′ ⊑ τ′ → τ′′. It starts with some =^{ϵ} ⟹^{+} steps, but an easy analysis proves that those steps are meaningless. So the rest of the derivation consist of steps either at a position 0p′ or 1r′, just like in the derivation (2). So it can be split into the component derivations the weights of which sum to the weight of the primary inequality. ■

Lemma 8.3 Let σ and τ be types. Assume that there exist two paths: positive p and negative r such that σ|_{p} = σ|_{r} = α and τ|_{p} = τ|_{r} = α for a free variable α. Suppose furthermore that τ is not of the form ∀γ τ′. Then

1. ∀α σ ⊑ τ{α ↦ ξ} if and only if σ{α ↦ ξ} ⊑ τ{α ↦ ξ};

2. if both inequalities hold then the weight of the latter is no smaller than the weight of the former;

3. moreover if weight(ξ) > 0 then the weight of the first inequality is strictly greater than the weight of the second.

Proof. If the inequality σ{α ↦ ξ} ⊑ τ{α ↦ ξ} holds, then since ∀α σ =^{ϵ} ⟹_{+}^{i} σ{α ↦ ξ}, we have the following wychodzi!

∀α σ ⊑ τ{α ↦ ξ}  (3)

In order to show the opposite implication suppose the latter inequality holds. Consider its ordered derivation of minimal weight. It begins with some meaningless =^{ϵ} ⟹^{+} steps. All they can do is to add some empty quantifiers after the initial ∀α. Now the latter must be instantiated:

∀α σ′ =^{ϵ} ⟹_{i}^{+} σ′{α ↦ χ}  (4)

where σ′ stands for ∀β_{1} … β_{n} σ, and β_{1}, …, β_{n} are the quantifiers added by first =^{ϵ} ⟹^{+} steps. Of course β_{1}, …, β_{n} ∉ F V (σ′{α ↦ χ}). By Lemma 8.1, ξ ∼ χ, so also σ{α ↦ ξ} ∼ σ′{α ↦ χ}. This yields the inequality

σ{α ↦ ξ} ⊑ τ{α ↦ ξ}

Its weight, by Proposition 6.6 is no greater than the weight of (3) minus the weight of (4), which is strictly positive, when weight(ξ) is so. Since weight(ξ) = weight(χ) we have the desired conclusion. ■

9 Encoding a machine

This section cempletes the proof of undecidability of the relation ⊑. After proving Lemmas 8.2 and 8.3, we know that ⊑ has all properties of the relation ⊑_{M} used in [TU95] to encode the halting problem of stack register machines. We show briefly the idea of this encoding.

A stack register machine M is a deterministinc computing device with two main registers V_{1} and V_{2} and a finite number of auxiliary registers v_{1}, …, v_{n}. The registers can hold nonempty words over the finite alphabet Σ, containing instruction labels with one special end label e. A machine step consists of taking the top label from the first main register, executing the assigned instruction on the auxiliary registers and finally switching the main ones. If the read label is the last one in V_{1}, we copy the contents of the first auxiliary register, before instruction execution. Machine instructions are parallel assignments of one registers to another, with pushing some new labels at the top. For a given label ℓ ≠ e we write

ℓ(r_{1}, …, r_{n}) = (w_{1}r_{i_{1}}, …, w_{n}r_{i_{n}}) where w_{i} ∈ Σ^{∗}

Given an instantaneous description — a tuple (V_{1}, V_{2}, v_{1}, …, v_{n}) of n + 2 words — a next step leads to the following configuration, depending on the contents of the first main register:

• if V_{1} = eV′_{1}, the machine halts;

• if V_{1} = ℓV′_{1}, where ℓ ≠ e and V_{1} ≠ ϵ, the next instantaneous description is (V_{2}, V′_{1}, v′_{1}, …, v′_{n}), for ℓ(v_{1}, …, v_{n}) = (v′_{1}, …, v′_{n});

• if V_{1} = ℓ, for ℓ ≠ e, the next configuration is (V_{2}, v_{1}, v′_{1}, …, v′_{n}), for v′_{1}, …, v′_{n} as above.

The encoding idea is the following. For each label ℓ ∈ Σ we construct a type σ_{ℓ} hiding the associated instruction. Then we give the word composition rules yielding from a given configuration the n + 2 types, σ_{V_{1}}, σ_{V_{2}}, σ_{v_{1}}, …, σ_{v_{n}}, containing one special free variable γ. The key to the undecidability proof is the following proposition:

Proposition 9.1 Given a stack register machine M, it halts for an instantaneous description (V_{1}, V_{2}, v_{1}, …, v_{n}) if and only if the encoding inequality holds

σ_{V_{1}} ⊑ (σ_{v_{1}} → σ_{v_{1}}) → ⋯ (σ_{v_{n}} → σ_{v_{n}}) → σ_{V_{2}} → γ  (5)

Proof sketch:^{3} The equivalence is based on the following properties of the encoding and the relation ⊑

• if (V_{1}, V_{2}, v_{1}, …, v_{n}) is an end configuration, i.e. V_{1} = eV′_{1}, then σ_{V_{1}} = ⊥; • if V_{1} = ℓV′_{1} for V′_{1} ≠ ϵ and ℓ(r_{1}, …, r_{n}) = (w_{1}r_{i_{1}}, …, w_{n}r_{i_{n}}), then we have

3For the details concerning the encoding and the proof of the proposition we refer the reader to [TU95]

σ_{V_{1}} = ∀α_{1} … α_{n} ((α_{1} → α_{1}) → … → (α_{n} → α_{n}) →
((σ_{w_{1}}[α_{i_{1}}] → σ_{w_{1}}[α_{i_{1}}]) → ⋯ → (σ_{w_{n}}[α_{i_{n}}] → σ_{w_{n}}[α_{i_{n}}]) →
σ_{V′_{1}} → γ) → γ)

If the encoding inequality (5) holds, then by using Lemma 8.3 n times, we know it is equivalent to the inequality

(σ_{v_{1}} → σ_{v_{1}}) → … → (σ_{v_{n}} → σ_{v_{n}}) → ((σ_{w_{1}}[σ_{v_{i_{1}}} ] → σ_{w_{1}}[σ_{v_{i_{1}}} ]) → … → (σ_{w_{n}}[σ_{v_{in}}] → σ_{w_{n}}[σ_{v_{in}}]) → σ_{V′_{1}} → γ) → γ

⊑ (σ_{v_{1}} → σ_{v_{1}}) → … → (σ_{v_{n}} → σ_{v_{n}}) → σ_{V_{2}} → γ

After application of Lemma 8.2 (n + 1) times, we obtain the equivalence with the encoding inequality after one step of the execution

σ_{V_{2}} ⊑ (σ_{w_{1}}[σ_{v_{i_{1}}} ] → σ_{w_{1}}[σ_{v_{i_{1}}} ]) → … → (σ_{w_{n}}[σ_{v_{in}}] → σ_{w_{n}}[σ_{v_{in}}]) → σ_{V′_{1}} → γ

The weight of the latter inequality is no greater then the weight of 5), and the difference becomes strictly positive if at least one type σ_{v_{1}}, …, σ_{v_{n}} was of a non-zero weight;

• similarily, if V_{1} = ℓ, for ℓ as above, we have

σ_{V_{1}} = ∀α_{1} … α_{n} ((α_{1} → α_{1}) → … → (α_{n} → α_{n}) →
((σ_{w_{1}}[α_{i_{1}}] → σ_{w_{1}}[α_{i_{1}}]) → ⋯ → (σ_{w_{n}}[α_{i_{n}}] → σ_{w_{n}}[α_{i_{n}}]) →
α_{1} → γ) → γ)

and by the analogous reasoning we obtain the equivalence of (5) with the inequality

σ_{V_{2}} ⊑ (σ_{w_{1}}[σ_{v_{i_{1}}} ] → σ_{w_{1}}[σ_{v_{i_{1}}} ]) → … → (σ_{w_{n}}[σ_{v_{in}}] → σ_{w_{n}}[σ_{v_{in}}]) → σ_{v_{1}} → γ

It is obvious that if the configuration (V_{1}, V_{2}, v_{1}, …, v_{n}) is an end one, the encoding inequality holds. Otherwise we have the equivalence

\begin{matrix}σ_{V_{1}} ⊑ (σ_{v_{1}} → σ_{v_{1}}) → ⋯ (σ_{v_{n}} → σ_{v_{n}}) → σ_{V_{2}} → γ \\ ⟺ σ_{U_{1}} ⊑ (σ_{u_{1}} → σ_{u_{1}}) → ⋯ (σ_{u_{n}} → σ_{u_{n}}) → σ_{U_{2}} → γ \end{matrix}

where (U_{1}, U_{2}, u_{1}, …, u_{n}) is the machine configuration after one step of the execution. Moreover the weight of the latter inequality is no greater then the weight of the former and if at least one of v_{1}, …, v_{n} does not start with e, the difference of the weights is strictly positive.

Of course if the machine halts, the encoding inequality holds for all configurations leading to the end one.

The proof of the other implication is slightly more difficult. If the encoding inequality holds then with each step the weight of the encoding inequality decreases or (if all auxiliary registers begin with the e label) the number of labels in the main registers decreases while the weight of the encoding inequality remains unchanged. When the first main register becomes empty, its contents is replaced by the word beginning with the end label which provides termination of the execution in the next step. ■

Theorem 2 The relation ⊑ of polymorphic subtyping without distributivity is undecidable.

Proof. The result follows from the our Propsition 9.1 and Lemma 16 from the paper of Tiuryn and Urzyczyn [TU95] that reduces the undecidable halting problem of deterministic two-counter automata to the halting problem of stack register machines. ■

10 Conclusions

The same proof would also be valid if we removed yet another axiom from the definition of subtyping — the axiom of generalization (quant). The only difference would emerge in Section 6, but Proposition 6.6 remains true which enables us to continue with the undecidability proof.

Another direction of searching for decidable subtyping relation is the predicative version of System F, presented by Daniel Leivant [Lei91]. Some work has already been done in this field (see [?]), but we believe that further investigation should lead to interesting results.

References

[Gir89] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[Jim95] T. Jim, “System F plus subsumption reduces to Mitchell’s subtyping relation”, Manuscript (1995).

[Lei91] D. Leivant, “Finitely stratified polymorphism”, Information and Computation, 93 (1), 1991, 93–113.

[LMS95] G. Longo, K. Milsted, and S. Soloviev, “A logic of subtyping”, Proc. 10-th IEEE Symp. Logic in Computer Science, San Diego (1995), pp. 292-299.

[Mit88] J.C. Mitchell, “Polymorphic type inference and containment”, Information and Computation, 76 (2-3), 1988, pp. 211–249.

[Tiu95] J. Tiuryn, “Equational Axiomatization of Bicoercibility for Polymorphic Types”, Proc. Conf. Foundations of Software Technology and Teoretical Computer Science’95, Bangalore, India; 18-20 Dec 1995. Lecture Notes in Computer Science 1026, pp. 166-179.

[TU95] J. Tiuryn and P. Urzyczyn, “The Subtyping Problem For Second-Order Types in Undecidable” Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp. 74-85, 27-30 July 1996.

[Wel94] J.B. Wells, “Typability and type checking in the second-order λcalculus calculus are equivalent and undecidable”, Proc. 9th LICS, IEEE, 1994, pp. 176–185.

[Wel95] J.B. Wells, “The Undecidabilility of Mitchell’s Subtyping Relationship”, Technical Report, Computer Science Department, Boston University, Number 95-019, December 10 1995.

[Wel96] J.B. Wells, “Typability is Undecidable for F+Eta” Technical Report, Computer Science Department, Boston University, Number 96-022, March 9 1996.