Syntactic Metatheory of Higher-Order Subtyping

Andreas Abel and Dulma Rodriguez

Department of Computer Science, University of Munich Oettingenstr. 67, D-80538 München, Germany

                {andreas.abel|dulma.rodriguez}@ifi.lmu.de

Abstract. We present a new proof of decidability of higher-order subtyping in the presence of bounded quantification. The algorithm is formulated as a judgement which operates on beta-eta-normal forms. Transitivity and closure under application are proven directly and syntactically, without the need for a model construction or reasoning on longest beta-reduction sequences. The main technical tool is hereditary substitution, i.e., substitution of one normal form into another, resolving all freshly generated redexes on the fly. Hereditary substitutions are used to keep types in normal-form during execution of the subtyping algorithm. Termination of hereditary substitutions can be proven in an elementary way, by a lexicographic induction on the kind of the substituted variable and the size of the expression substituted into—this is what enables a purely syntactic metatheory. Keywords: Higher-order subtyping, bounded quantification, algorithmic subtyping, hereditary substitution.

1 Introduction

Higher-order subtyping with bounded quantification has been used to model aspects of object-oriented programming languages [Pie02, Ch. 32]. Decidability is non-trivial and has been studied extensively in the past. Both Compagnoni [Com95] and Pierce and Steffen [PS97] have provided an algorithm for deciding subtyping for Kernel System F_{<:}^{ω} and proven its completeness by establishing a strong normalization theorem, while Compagnoni and Goguen [CG03,CG06] have studied the more general system F_{≤}^{ω} and proved completeness by constructing a Kripke model.

The cited works are impressive, but the complexity of the proofs is a bit overwhelming when it comes to formalizing them in a theorem prover like Coq, Isabelle, or Twelf. The reason is that strong normalization theorems or models are laborious to mechanize and little is known about automating the involved proofs. However, recently there have been successes in formalizing purely syntactical developments of metatheory of programming languages, most notably SML [LCH07]. Such formalizations use only first-order inductive judgements over syntactical objects and proofs by induction over these judgements or simple arithmetical measures.

A modern technique to treat the metatheory of systems which rely on normalization is hereditary substitution [WC^{+}03]. Hereditary substitution provides an algorithm for bottom-up normalization whose termination can be proven by a simple lexicographic induction—provided the proof-theoretical strength of the language does not exceed that of the simply-typed lambda-calculus. The technique of hereditary substitution simplifies the metatheory considerably. Hereditary substitution has been successfully used for the normalization of the Concurrent Logical Framework [WC^{+}03], the Edinburgh LF [HL07], and the type language of SML [LCH07].

In this article, we present a purely syntactic metatheory of F_{<:}^{ω} using the technique of hereditary substitution, affirming that it is flexible enough to account for bounded quantification, which is similar to lazy let-binding or singleton types. The result is a major simplification of the metatheory of F_{<:}^{ω} and a proof structure that is ready for formalization in a proof assistant even with low prooftheoretical complexity such as Twelf.

Detailed proofs for the theorems of this paper can be found in the diploma thesis of the second author [Rod07].

Contents. In Section 2, we recapitulate System F_{<:}^{ω} with kinding, equality and declarative subtyping and present a subtyping algorithm which works on η-long β-normal type constructors. In Section 3 we present algorithms for hereditary substitution and normalization and prove their correctness; this section contains the main technical work. Afterwards, in Section 4, we show soundness, completeness, and termination of the subtyping algorithm, which is in essence a consequence of the results of Section 3. Finally, we discuss related and further work in the conclusions.

Judgements. In this article, the following judgements will be defined inductively:

Γ ⊢ F : κ  constructor F has kind κ in context Γ
Γ ⊢ F = F′ : κ F and F′ of kind κ are βη-equal
Γ ⊢ F ≤ F′ : κ F is a higher-order subtype of F′
Γ ⊢ V ⇑ κ  V is hereditarily normal of kind κ
Γ ⊢_{a} V ≤ V′ V is a subtype of V′, algorithmically

When we write D :: J, we mean that judgement J is established by derivation D. Then, |D| denotes the height of this derivation. We consider derivations ordered by their height: D_{1} ≤ D_{2} iff |D_{1}| ≤ |D_{2}|.

2 System F_{<:}^{ω}

This section introduces the syntax and the rules of kinding, equality, and subtyping of system F_{<:}^{ω}, a typed λ-calculus of polymorphic functions, subtyping, and type operators.

2.1 Constructors and Kinds

System F_{<:}^{ω} consists of terms (programs), type constructors and kinds. This article is dedicated to the decidability of subtyping alone, thus, we ignore terms and typing completely. Note, however, that decidability of typing follows from decidability of subtyping (via the concept of promotion [Pie02, Ch. 28.1] [PS97]).

Constructors are classified by their kind, i.e., as types, functions on types, etc. Kinds are given by the grammar:

κ ::= ∗ | κ_{1} → κ_{2}

Let κ → κ′ be an abbreviation for κ_{1} → κ_{2} → … → κ_{n} → κ′ where |κ| = n. Let |κ| ∈ ℕ denote a measure on kinds with |κ′| ≤ |κ → κ′| and |κ| < |κ → κ′|. An example of such a measure is the rank, which is defined recursively as rk(κ → ∗) = max{1 + rk(κ_{i}) | 1 ≤ i ≤ |κ|}. In particular, rk(∗) = 0.

Constructors are given by the following Church-style type-level λ-calculus. The meta-variable X ranges over a countable infinite set of constructor variables.

A, B, F, G ::= X | λX:κ. F | F G | A → B | ∀X ≤G:κ. A | ⊤

As usual, λX : κ. F binds variable X in F. We identify constructors up to αequivalence, i.e., up to renaming of bound variables. Sometimes, when we want to stress syntactic identity of constructors, we use ≡ for α-equivalence. The letters U, V, W denote β-normal constructors and A, B constructors of kind ∗ (types). We define ⊤_{κ→∗} = λY : κ. ⊤ (meaning λY_{1} : κ_{1}…. λY_{|Y |} : κ_{|κ|}. ⊤) where the lengths of Y and κ coincide. A vector notation is also used for application: F G means F G_{1} … G_{|G|}, where application associates to the left as usual.

Contexts follow the grammar Γ ::= ⋄ | Γ, X ≤ G: κ. We refer to G as the bound of X. We assume all variables bound in Γ to be distinct and define the notation Γ, X:κ as an abbreviation for Γ, X ≤⊤_{κ} : κ.

2.2 Kinding and Well-formed Contexts

Well-formed contexts Γ ⊢, defined mutually with the kinding judgement Γ ⊢ F : κ in Figure 1, are constructed from the empty context by adding well-kinded type variable declarations. Kinding is decidable and unique, since constructor variables are annotated with their kinds.

The extra assumption Γ ⊢ G : κ in rule (K-Var) is due to Pierce and Steffen [PS97] and simplifies the proof of Theorem 1, which entails termination of the subtyping algorithm.

We maintain the invariant that kinding statements are only derivable in wellformed contexts (see Lemma 1.1). Bounds do not matter for kinding, i.e., if a constructor F has kind κ in a context Γ , and Γ′ is the same context as Γ but with different, well-kinded bounds, then F has kind κ in context Γ′ as well.

Lemma 1 (Admissible rules for kinding).

1. Validity: If Γ ⊢ F : κ then Γ ⊢.

Γ ⊢

(C-Empty) \overline{⋄ ⊢}  (C-Bound) \frac{Γ ⊢  Γ ⊢ G : κ}{Γ, X ≤G:κ ⊢}

Γ ⊢ F : κ

(K-Var) \frac{(X ≤G:κ) ∈ Γ  Γ ⊢ G : κ}{Γ ⊢ X : κ}  (K-Top) \frac{Γ ⊢}{Γ ⊢ ⊤ : ∗}

(K-Abs) \frac{Γ, X:κ ⊢ F : κ′}{Γ ⊢ λX:κ. F : κ → κ′}  (K-App) \frac{Γ ⊢ F : κ → κ′  Γ ⊢ G : κ}{Γ ⊢ F G : κ′}

(K-Arr) \frac{Γ ⊢ A : ∗  Γ ⊢ B : ∗}{Γ ⊢ A → B : ∗}  (K-All) \frac{Γ ⊢ G : κ  Γ, X ≤G:κ ⊢ A : ∗}{Γ ⊢ ∀X ≤G:κ. A : ∗}

Γ ⊢ F = F′ : κ

(Eq-β) \frac{Γ, X:κ ⊢ F : κ′  Γ ⊢ G : κ}{Γ ⊢ (λX:κ. F) G = [G/X]F : κ′}  (Eq-η) \frac{Γ ⊢ F : κ → κ′  X ∉ FV(F)}{Γ ⊢ λX:κ. F X = F : κ → κ′}

(Eq-Var) \frac{(X ≤ G:κ) ∈ Γ  Γ ⊢ G : κ}{Γ ⊢ X = X : κ} (Eq-Abs) \frac{Γ, X:κ ⊢ F = F′ : κ′}{Γ ⊢ λX:κ. F = λX:κ. F′ : κ → κ′}

(Eq-App) \frac{Γ ⊢ F = F′ : κ → κ′  Γ ⊢ G = G′ : κ}{Γ ⊢ F G = F′ G′ : κ′}

(Eq-Top) \frac{Γ ⊢}{Γ ⊢ ⊤ = ⊤ : ∗}  (Eq-Arr) \frac{Γ ⊢ A = A′ : ∗  Γ ⊢ B = B′ : ∗}{Γ ⊢ A → B = A′ → B′ : ∗}

(Eq-All) \frac{Γ ⊢ G = G′:κ  Γ, X ≤ G:κ ⊢ A = A′ : ∗}{Γ ⊢ ∀X ≤ G:κ.A = ∀X ≤ G′:κ.A′ : ∗}

(Eq-Sym) \frac{Γ ⊢ F = F′ : κ}{Γ ⊢ F′ = F : κ}  (Eq-Trans) \frac{Γ ⊢ F_{1} = F_{2} : κ  Γ ⊢ F_{2} = F_{3} : κ}{Γ ⊢ F_{1} = F_{3} : κ}

Γ ⊢ F ≤ F′ : κ

(S-Var) \frac{Γ ⊢ G : κ  X ≤G:κ ∈ Γ}{Γ ⊢ X ≤ G : κ}  (S-App) \frac{Γ ⊢ F ≤ F′ : κ → κ′  Γ ⊢ H : κ}{Γ ⊢ F H ≤ F′H : κ′}

(S-Top) \frac{Γ ⊢ A : ∗}{Γ ⊢ A ≤ ⊤ : ∗}  (S-Abs) \frac{Γ, X:κ ⊢ F ≤ F′ : κ′}{Γ ⊢ λX:κ. F ≤ λX:κ. F′ : κ → κ′}

(S-Arr) \frac{Γ ⊢ A′ ≤ A : ∗  Γ ⊢ B ≤ B′ : ∗}{Γ ⊢ A → B ≤ A′ → B′ : ∗}

(S-All) \frac{Γ ⊢ G : κ  Γ, X ≤G:κ ⊢ A ≤ A′ : ∗}{Γ ⊢ ∀X ≤G:κ.A ≤ ∀X ≤G:κ.A′ : ∗}

(S-Eq) \frac{Γ ⊢ F = G : κ}{Γ ⊢ F ≤ G : κ}  (S-Trans) \frac{Γ ⊢ F ≤ G : κ  Γ ⊢ G ≤ H : κ}{Γ ⊢ F ≤ H : κ}

Fig. 1. Declarative presentation of F_{<:}^{ω}.

2. Weakening: If Γ, Γ′ ⊢ F : κ′ and Γ ⊢ G : κ then Γ, X ≤G:κ, Γ′ ⊢ F : κ′.

3. Substitution: If Γ, X ≤ H: κ, Γ′ ⊢ F : κ′ and Γ ⊢ G : κ then Γ, [G/X]Γ′ ⊢ [G/X]F : κ′.

Since bounds do not matter for kinding, we do not require Γ ⊢ G ≤ H : κ in the substitution property.

2.3 Equality

In contrast to previous presentations of System F_{<:}^{ω} [Pie02, Ch. 31], we consider constructors equivalent modulo β and η. Instead of an untyped equality we define an equality judgement Γ ⊢ F = F′ : κ, since this is more robust w. r. t. extensions, e. g., by polarities [Ste98,Abe06b]. The judgement is given by the axioms (Eq-β) and (Eq-η) plus congruence and equivalence rules (see Figure 1).

The equality judgement has the usual properties.

Lemma 2 (Admissible rules for equality).

1. Reflexivity: If Γ ⊢ F : κ then Γ ⊢ F = F : κ.

2. Validity: If Γ ⊢ G = G′ : κ then Γ ⊢ G : κ and Γ ⊢ G′ : κ.

3. Weakening: If Γ, Γ′ ⊢ F = F′ : κ and Γ ⊢ G : κ then Γ, X ≤ G: κ, Γ′ ⊢ F = F′ : κ.

4. Substitution: If Γ, X ≤ H : κ, Γ′ ⊢ F = F′ : κ′ and Γ ⊢ G : κ then Γ, [G/X]Γ′ ⊢ [G/X]F = [G/X]F′ : κ′.

Proof. Each by induction on the first derivation. In the proof of item 2, case (Eq-All), we use the fact that bounds do not matter for kinding. □

2.4 Subtyping

The F_{<:}^{ω} subtyping relation Γ ⊢ F ≤ F′ : κ (see Figure 1) extends the subtyping relation of system F_{≤} [CW85]. Subtyping for type operators of higher kind is defined pointwise, see (S-Abs) and (S-App).

Decidability requires using the Kernel-Fun rule (S-All). Full subtyping would allow a bound G′ ≤ G on the right hand side, losing decidability [Pie92]. We do not treat antisymmetry here. Reflexivity is inherited from equality.

Lemma 3 (Admissible rules for subtyping).

1. Validity: If Γ ⊢ F ≤ F′ : κ then Γ ⊢ F : κ and Γ ⊢ F′ : κ.

2. Weakening: If Γ, Γ′ ⊢ F ≤ F′ : κ and Γ ⊢ G : κ′ then Γ, X ≤ G: κ′, Γ′ ⊢ F ≤ F′ : κ.

3. Substitution: If Γ, X ≤ H : κ, Γ′ ⊢ F ≤ F′ : κ′ and Γ ⊢ G ≤ H : κ then Γ, [G/X]Γ′ ⊢ [G/X]F ≤ [G/X]F′ : κ′ (not needed in the following).

2.5 Algorithmic Subtyping

The declarative definition of subtyping contains two rules that correspond to a logical cut: on the level of constructors, the transitivity rule (S-Trans), if one views types as predicates and subtyping as predicate inclusion; and on the level of kinds, the application rule (S-App), if one views kinds as implicational propositions and constructors as their proofs.^{1} In an algorithmic version of subtyping, both kinds of cuts have to be eliminated [Com95,PS97]. Application is eliminated by considering constructors in normal form V only, in our case η-long β-normal form. Transitivity is incorporated into the variable rule (SA-Bound), which is a fusion of (S-Var), (S-App), (S-Eq), and (S-Trans). It looks up the bound U of the head X of a neutral constructor XV and recursively checks subtyping for U V . To keep everything in normal form, a normalizing application U @ V is employed which will be defined in Section 3.1.

The algorithm receives as input a context Γ and two η-long constructors V, V′ such that Γ ⊢ V : κ and Γ ⊢ V′ : κ and decides Γ ⊢ V ≤ V′ : κ.

Γ ⊢_{a} V ≤ V′

(SA-Top) \overline{Γ ⊢_{a} V ≤ ⊤}  (SA-Refl) \overline{Γ ⊢_{a} XV ≤ XV}

(SA-Bound) \frac{(X ≤U:κ → ∗) ∈ Γ  Γ ⊢_{a} U @ V ≤ W}{Γ ⊢_{a} XV ≤ W}

(SA-Arr) \frac{Γ ⊢_{a} W ≤ V : ∗  Γ ⊢_{a} V′ ≤ W′}{Γ ⊢_{a} V → V′ ≤ W → W′}

(SA-All) \frac{Γ, X ≤V :κ ⊢_{a} W ≤ W′}{Γ ⊢_{a} ∀X ≤V :κ.W ≤ ∀X ≤V :κ.W′}

(SA-Abs) \frac{Γ, X:κ ⊢_{a} V ≤ V′}{Γ ⊢_{a} λX:κ. V ≤ λX:κ. V′}

Observe that since we are dealing with η-long forms, the only constructors of higher kind are λ-abstractions (SA-Abs). The rules specify a deterministic algorithm if one checks applicability of rules earlier in the list prior to rules mentioned later. In particular, (SA-Top) is checked first, and (SA-Refl) before (SA-Bound).

Our algorithmic subtyping rules correspond to Compagnoni’s [Com95] and Pierce and Steffen’s [PS97]—except that they consider Church-style β-normal constructors, hence, their algorithm does not validate η-equality. Thus, one cannot claim our algorithm is new, but in the remainder of this article we will present a novel, very direct and concise correctness proof with purely syntactic methods, which has a realistic chance of being mechanized in a theorem prover such as Coq, Isabelle, or Twelf.

1 More precisely, (S-App) is the rule of modus ponens, but in unrestricted form it allows non-normal proofs.

3 Normalization of Constructors

In last section we have described a decision procedure for subtyping which works on η-long β-normal forms. In this section, we will describe a normalization algorithm nf_{−}(−) which is correct w. r. t. judgmental equality:

1. Sound: If Γ ⊢ F : κ then Γ ⊢ nf_{Γ} (F) = F : κ.

2. Complete: If Γ ⊢ F = F′ : κ then nf_{Γ} (F) ≡ nf_{Γ} (F′).

3.1 Hereditary Substitution

There are abundant strategies to compute β-normal forms; we use bottom-up normalization, because its termination can be shown directly in a simply-typed setting—in our case it is a simply-kinded setting.

The bottom-up strategy nf(H) normalizes the immediate subterms of H and then puts them back together. For an application H = F G, normalization nf(F) of the function part may yield an abstraction λY :κ. F′. In this case, a β-normal form can be recovered by substituting nf(G) for Y in F′. New redexes may be created in turn which are resolved immediately by another substitution etc. The iteration of this process, which we call hereditary substitution, terminates since the kind of the substituted variable decreases with each iteration.

Hereditary substitutions are implicit in combinatorial normalization proofs, e. g., Prawitz [Pra65], Levy [Lév76], Girard, Lafont, and Taylor [GLT89, Ch. 4], and Amadio and Curien [AC97, Thm. 2.2.9]. They were first made explicit by Watkins et. al. [WC^{+}03] and Adams [Ada05] for dependent types. We follow the presentation of the first author [Abe06a].

Hereditary substitution (see Figure 2) is given as a 4-ary function [G/X]^{κ}H, whose result F̂ is either just a constructor F or a constructor annotated with a kind, written F^{κ}. If G and H are β-normal (and well-kinded) then the result will also be β-normal (and well-kinded). Results can be coerced back to constructors via an erasure operation given by \underline{F^{κ}} = F and \underline{F} = F.

It is easy to see that if [G/X]^{κ}H = F^{κ_{2}} then |κ_{2}| ≤ |κ|. This invariant ensures the termination of hereditary substitution. For correctness we need to show that, modulo β-equality, hereditary substitution is conventional substitution. In the following, we leave the \underline{coercion} implicit.

Lemma 4 (Termination and soundness of hereditary substitutions). If D :: Γ, X : κ, Γ′ ⊢ F : κ′ and Γ ⊢ G : κ then Γ, [G/X]Γ′ ⊢ [G/X]F = [G/X]^{κ}F : κ′.

Proof. By lexicographical induction on (|κ|, D). The proof is a straightforward extension of the soundness proof in [Abe06a]. □

Corollary 1. If Γ ⊢ F : κ → κ′ and Γ ⊢ G : κ then Γ ⊢ F @ G = F G : κ′.

Lemma 5 (Commutativity of hereditary substitutions). Let Γ ⊢ U : κ and Γ, X:κ, Γ′ ⊢ V : κ′ with κ′ = κ → κ_{0}.

[G/X]^{κ}F

[G/X]^{κ}Y  := G^{κ}  if X = Y
Y  otherwise
[G/X]^{κ}(λY :κ′. F)  := λY :κ′. \underline{[G/X]^{κ}F}  where Y fresh for X, G
[G/X]^{κ}(F H)  := (\underline{[\underline{Ĥ}/Y]^{κ_{1}}F′})^{κ_{2}}  if F̂ = (λY :κ′_{1}. F′)^{κ_{1}→κ_{2}}
\underline{F̂} \underline{Ĥ}  otherwise
herein, \begin{aligned}F̂ & = & [G/X]^{κ}F \\ Ĥ & = & [G/X]^{κ}H \end{aligned}

[G/X]^{κ}(A → B)  := \underline{[G/X]^{κ}A} → \underline{[G/X]^{κ}B}
[G/X]^{κ}(∀Y ≤ H:κ.A) := ∀Y ≤ \underline{[G/X]^{κ}H}:κ.
\underline{[G/X]^{κ}A}  where Y fresh for X, G
[G/X]^{κ}⊤  := ⊤

F @ G

(λX:κ. F) @ G  := \underline{[G/X]^{κ}F}
F @ G  := F G  if F ≠ λX:κ. F′

F @ G

F @ G  := ((F @ G_{1}) @ G_{2} …) @ G_{|G|}

Fig. 2. Hereditary substitution.

1. If Γ, X:κ, Γ′ ⊢ W_{i} : κ_{i} for 1 ≤ i ≤ |κ| then

[U/X]^{κ}(V @ W) ≡ [U/X]^{κ}V @ [U/X]^{κ}W

2. If Γ, X:κ, Γ′, Y :κ′, Γ′′ ⊢ W : κ′′ then:

[U/X]^{κ}([V/Y]^{κ′}W) ≡ [[U/X]^{κ}V /Y]^{κ′}([U/X]^{κ}W)

Proof. Simultaneously by simultaneous induction^{2} on {κ, κ′}, first 1 and then 2. The proof of 2 proceeds by a local induction on W. □

3.2 Computing the Long Normal Form

Well-kinded constructors are β-normalizing, and we can compute their η-long βnormal form. First, let us define the η-expansion η_{κ}(N) of a neutral constructor N at kind κ by η_{∗}(N) = N and η_{κ→κ′}(N) = λX:κ. η_{κ′}(N η_{κ}(X)).

2 Simultaneous order is defined by {X, Y } < {X′, Y′} if X < X′ and Y ≤ Y′.

Lemma 6 (η-expansion is sound). If Γ ⊢ N : κ then Γ ⊢ N = η_{κ}(N) : κ.

Normalization is given by a partial function nf_{Γ} (F), defined by recursion on F.

nf_{Γ} (X)  := η_{κ}(X)  if (X ≤ :κ) ∈ Γ
nf_{Γ} (⊤)  := ⊤
nf_{Γ} (λX:κ. F) := λX:κ. nf_{Γ,X:κ}(F)
nf_{Γ} (A → B)  := nf_{Γ} (A) → nf_{Γ} (B)
nf_{Γ} (∀X ≤G:κ.A) := ∀X ≤nf_{Γ} (G):κ. nf_{Γ,X≤G:κ}(A)
nf_{Γ} (F G)  := nf_{Γ} (F) @ nf_{Γ} (G) where κ is the kind of G in Γ

The last line is the source of partiality: If Γ ⊬ F G : κ′, then there might be no kind of G. However, for well-kinded constructors Γ ⊢ F : κ, with which we explicitly deal, nf_{Γ} (F) is always well-defined. We omit the subscript Γ if clear from the context of discourse. The algorithm η-expands the variables, this way producing η-long β-normal constructors.

Normalization can be extended to contexts in the obvious way: nf(Γ) computes a context where all bounds have been normalized.

Lemma 7 (Soundness and termination of normalization). If Γ ⊢ F : κ then Γ ⊢ F = nf_{Γ} (F) : κ.

Proof. By induction on the kinding derivation, using Lemma 6 in the variable case, and Corollary 1 in the application case. □

3.3 Characterization of Long Normal Forms

We will now define a judgement Γ ⊢ V ⇑ κ, read “V is hereditarily normal of kind κ in context Γ ”, that classifies the β-normal constructor V as a possible input for the subtyping algorithm. In particular, V must be η-long, and new redexes which might be created by (SA-Bound) during the execution of the algorithm must be normalizable. We call such redexes hidden, an example is ∀X ≤(λY :∗. V):∗ → ∗. X W which contains the hidden redex (λY :∗. V) W.

Γ ⊢ V ⇑ κ

(LN-Bound) \frac{(X ≤U:κ → ∗) ∈ Γ  Γ ⊢ V_{i} ⇑ κ_{i}  Γ ⊢ U @ V ⇑ ∗ (⋆)}{Γ ⊢ X V ⇑ ∗}

(LN-Abs) \frac{Γ, X:κ ⊢ V ⇑ κ′}{Γ ⊢ λX:κ. V ⇑ κ → κ′}  (LN-Arr) \frac{Γ ⊢ V ⇑ ∗  Γ ⊢ W ⇑ ∗}{Γ ⊢ V → W ⇑ ∗}

(LN-All) \frac{Γ, X ≤U:κ ⊢ V ⇑ ∗}{Γ ⊢ ∀X ≤U:κ. V ⇑ ∗}  (LN-Top) \frac{Γ ⇑}{Γ ⊢ ⊤ ⇑ ∗}

Remark 1. The third hypothesis (⋆) in (LN-Bound) ensures normalization of hidden redexes, hence Γ ⊢ V ⇑ κ can be used as a termination measure for the algorithm. Even without (⋆) the judgement characterizes the η-long normal forms.

A context is normal, Γ ⇑, if all bounds in Γ are hereditarily normal. In the following, we establish that normalization is the identity on long normal forms. First we prove it for variables.

Lemma 8.

1. If Γ ⊢ V ⇑ κ then [V/X]^{κ}η_{κ}(X) ≡ V.

2. If D :: Γ, X:κ, Γ′ ⊢ W ⇑ κ′ then [η_{κ}(X)/X]^{κ}W ≡ W.

Proof. Simultaneously by induction on κ, and a local induction on D in 2. □

Lemma 9 (Idempotency of nf). If D :: Γ ⊢ U ⇑ κ then nf(U) ≡ U.

Proof. By induction on D, using Lemma 8 in the variable case. □

We now build up to a normalization theorem: we will show that nf produces a hereditarily normal form from each well-kinded constructor. The following lemma, which can be seen as the heart of our technical development, proves normalization of application.

Lemma 10 (Substitution and application for normal forms). Let E :: Γ ⊢ U ⇑ κ.

1. Assume D :: Γ, X:κ, Γ′ ⇑. Then Γ, [U/X]^{κ}Γ′ ⇑.

2. Assume D :: Γ, X:κ, Γ′ ⊢ V ⇑ κ′. Then Γ, [U/X]^{κ}Γ′ ⊢ [U/X]^{κ}V ⇑ κ′.

3. Assume D :: Γ ⊢ V ⇑ κ → κ′. Then Γ ⊢ V @ U ⇑ κ′.

Proof. Simultaneously by lexicographical induction on (|κ|, D). The interesting case of item 2 is (LN-Bound) with V ≡ XV , κ = κ → ∗.

\frac{Γ, X:κ, Γ′ ⊢ V_{i} ⇑ κ_{i} Γ, X:κ, Γ′ ⊢ ⊤_{κ} @ V ⇑ ∗}{Γ, X:κ, Γ′ ⊢ XV ⇑ ∗}

By induction hypothesis (2), we have D_{i} :: Γ, [U/X]^{κ}Γ′ ⊢ [U/X]^{κ}V_{i} ⇑ κ_{i} for i = 1..|κ|. Moreover, we have by induction hypothesis (3):

E_{1} :: Γ, [U/X]^{κ}Γ′ ⊢ U @ [U/X]^{κ}V_{1} ⇑ κ_{2} → … → κ_{n} → ∗

because (κ_{1}, E) < (κ, D). We again have by induction hypothesis (3):

E_{2} :: Γ, [U/X]^{κ}Γ′ ⊢ U @ ([U/X]^{κ}V_{1}) @ ([U/X]^{κ}V_{2}) ⇑ κ_{3} → … → κ_{n} → ∗

because (κ_{2}, E_{1}) < (κ, D). Continuing this schema, we get

E_{n} :: Γ, [U/X]^{κ}Γ′ ⊢ U @ [U/X]^{κ}V ⇑ ∗

which is equivalent to Γ, [U/X]^{κ}Γ′ ⊢ [U/X]^{κ}(X V ) ⇑ ∗ and we are finished. In case V ≡ Y V , with Y ≠ X, we use Lemma 5. □

Theorem 1 (Normalization).

1. If D :: Γ ⊢ then nf(Γ) ⇑.

2. If D :: Γ ⊢ F : κ then nf(Γ) ⊢ nf(F) ⇑ κ.

Proof. Simultaneously by induction on D, using the previous lemma in case of application. □

3.4 Completeness of Normalization

In this section, we prove completeness of the normalization function, i.e., that the normal forms of judgmentally equal constructors are identical.

Lemma 11. If D :: Γ, X : κ, Γ′ ⊢ F : κ′ and Γ ⊢ G : κ then nf([G/X]F) ≡ [nf(G)/X]^{κ}nf(F).

Proof. By induction on D. In the application case we use Lemma 5. □

Theorem 2 (Completeness of the normalization). If D :: Γ ⊢ F = F′ : κ then nf(F) ≡ nf(F′).

Proof. The proof is by induction on D, in case (Eq-η) we use the characterization of η-long β-normal forms (Theorem 1 and Lemma 9) and in case (Eq-β) we use the previous lemma. □

Corollary 2 (Uniqueness of normal forms). If Γ ⊢ V = V′ : κ and Γ ⊢ V, V′ ⇑ κ then V ≡ V′.

Proof. Directly, using Theorem 2 and Lemma 9. □

4 Verification of Algorithmic Subtyping

In this section, we show that the subtyping algorithm is sound and complete for the declarative rules in Section 2. The difficult part, namely establishing the necessary properties of hereditary substitution and normalization and constructing a termination measure Γ ⊢ V ⇑ κ, has been completed in the last section. The actual properties of algorithmic subtyping are now easy to verify.

Soundness of the algorithm is straightforward because the algorithmic rules are less permissive than the declarative ones.

Lemma 12. Let Γ ⊢ V, V′ : κ. If D :: Γ ⊢_{a} V ≤ V′, then Γ ⊢ V ≤ V′ : κ.

Proof. By induction on D. □

Theorem 3 (Soundness of algorithmic subtyping). Let Γ ⊢ F, F′ : κ. If D :: nf(Γ) ⊢_{a} nf(F) ≤ nf(F′), then Γ ⊢ F ≤ F′ : κ.

Proof. Combining lemmata 12 and 7. To account for normalization of Γ, we establish that declarative equality and subtyping remain valid if we replace bounds in the context by judgmentally equal ones. □

Completeness of the algorithm means that any derivable statement in the declarative system is also derivable in the algorithmic system. This is more difficult to show than soundness, because we have eliminated declarative rules like (S-Trans) or (S-App). Thus, we need to show that these rules are admissible in the algorithmic system.

Lemma 13 (Reflexivity). If V is β-normal then Γ ⊢_{a} V ≤ V.

Proof. By induction on V. □

Lemma 14 (Transitivity). D_{1} :: Γ ⊢_{a} V_{1} ≤ V_{2} and D_{2} :: Γ ⊢_{a} V_{2} ≤ V_{3} imply Γ ⊢_{a} V_{1} ≤ V_{3}.

Proof. By induction on D_{1}. □

The following substitution lemma is the key step in showing that algorithmic subtyping is closed under application, i.e., complete for rule (S-App).

Lemma 15 (Substitution). Let Γ, X : κ, Γ′ ⊢ V, V′ ⇑ κ′ and Γ ⊢ U ⇑ κ. If D :: Γ, X:κ, Γ′ ⊢_{a} V ≤ V′ then Γ, [U/X]^{κ}Γ′ ⊢_{a} [U/X]^{κ}V ≤ [U/X]^{κ}V′.

Proof. By induction on D. The interesting case is (SA-Bound) for V ≡ Y V with Y bound later in the context than X.

\frac{(Y ≤ U′:κ → ∗) ∈ Γ′ Γ, X:κ, Γ′ ⊢_{a} U′ @ V ≤ W}{Γ, X:κ, Γ′ ⊢_{a} Y V ≤ W}

By induction hypothesis we have

Γ, [U/X]^{κ}Γ′ ⊢_{a} [U/X]^{κ}(U′ @ V ) ≤ [U/X]^{κ}W

which by Lemma 5, part (1), is equivalent to

Γ, [U/X]^{κ}Γ′ ⊢_{a} [U/X]^{κ}U′ @ [U/X]^{κ}V ≤ [U/X]^{κ}W.

The goal Γ, [U/X]^{κ}Γ′ ⊢_{a} Y [U/X]^{κ}V ≤ [U/X]^{κ}W follows by (SA-Bound). □

Completeness can now be shown by induction on derivations, using the previous lemmas: reflexivity, transitivity and substitution.

Theorem 4 (Completeness). If D :: Γ ⊢ F ≤ F′ : κ then nf(Γ) ⊢_{a} nf(F) ≤ nf(F′).

Proof. By induction on D, using Lemma 15 in case (S-App). □

Termination of algorithmic subtyping is now proven via the inductive termination predicate Γ ⊢ V ⇑ κ (which by Theorem 1 holds for all normal forms of well-kinded constructors). It is a considerable simplification of Compagnoni’s [Com95] termination measure which features intersection types as well. It has to be investigated whether the simplicity of our measure can be kept in the presence of intersection types.

Theorem 5 (Termination of algorithmic subtyping). If D_{1} :: Γ ⊢ V ⇑ κ and D_{2} :: Γ ⊢ V′ ⇑ κ then the query Γ ⊢_{a} V ≤ V′ terminates.

Proof. By simultaneous induction on {D_{1}, D_{2}}. We detail the case that D_{1} ends with (LN-Bound).

\frac{(X ≤U:κ → ∗) ∈ Γ  Γ ⊢ V_{i} ⇑ κ_{i} for all i  Γ ⊢ U @ V ⇑ ∗}{Γ ⊢ XV ⇑ ∗}

In case V′ ≠ XV we apply the rule (SA-Bound)

\frac{(X ≤U:κ → ∗) ∈ Γ Γ ⊢_{a} U @ V ≤ V′}{Γ ⊢_{a} XV ≤ V′}

By the induction hypothesis, the query Γ ⊢_{a} U @ V ≤ V′ terminates, thus, the query Γ ⊢_{a} XV ≤ V′ terminates as well. □

Corollary 3 (Decidability). If Γ ⊢ F, F′ : κ then Γ ⊢ F ≤ F′ : κ is decidable.

Proof. By Theorem 2 nf(Γ) ⊢ nf(F), nf(F′) ⇑ κ. Hence, the query nf(Γ) ⊢_{a} nf(F) ≤ nf(F′) terminates by Theorem 5. If it succeeds then Γ ⊢ F ≤ F′ : κ by soundness (Theorem 3), if it fails then Γ ⊬ F ≤ F′ : κ by completeness (Theorem 4).

5 Conclusions and Related Work

In this article we have proven decidability of subtyping for F_{<:}^{ω} with βη-equality in a purely syntactical way, with only first-order inductive definitions and simple induction measures. The proofs have been organized with a formalization in mind and can be mechanized in proof assistants such as Coq, Isabelle, or Twelf.

Related work. Foundations of F_{<:}^{ω} and the type-theoretic investigation of objectoriented languages have been laid by Cardelli [Car88], Mitchell [Mit90], and Abadi and Cardelli [AC96].

Most similar to the present work is the one of Compagnoni [Com95] both in the design of the subtyping algorithm and the organization of the proofs of soundness, completeness, and termination. She also treats intersection types but not η-equality of constructors. The main differences in the proof are: She inserts the notion of normal subtyping between the declarative and the algorithmic one, which we do not require, she refers to strong normalization of reduction, which adds some complexity to the proof, and she has a complicated termination measure which involves the longest reduction sequences of constructors classified by a judgement similar to our hereditary normal forms. Our approach has allowed considerable simplifications in comparison with Compagnoni’s.

Pierce and Steffen [PS97] justify algorithmic subtyping using rewriting theory. They consider an extension of β-reductions by Γ -reduction, which replaces a head variable by its bound, and ⊤-reduction which witnesses that ⊤ is defined pointwise for higher kinds. The confluence and strong normalization theorems shed light on the combination of these notions of reduction, however, they are not the shortest path to the verification of the subtyping algorithm.

Compagnoni and Goguen [CG03] construct a Kripke model based on typed operational semantics to analyze the metatheory of F_{≤}^{ω}, an extension of F_{<:}^{ω} by bounded abstraction λX ≤ F. G. They use this model to prove anti-symmetry [CG06] of subtyping which allows replacing judgmental equality by bi-inclusion. Recently they have investigated Church-style subtyping [CG07], where each variable is annotated by its bound, hence, the complicated Kripke-model is replaced by a non-Kripke logical relation. Their subtyping algorithm works with weakhead normal forms, only the decision whether the bound-lookup rule (SA-Bound) should fire demands full normalization in some cases. The structure of their proof, with logical relation and strong normalization theorem, seems very robust w. r. t. extensions of the type language; however, it cannot compete with us in terms of proof economics.

The first author [Abe06b] considers F_{ω}, the higher-order polymorphic lambdacalculus with sized types and polarized subtyping, but without bounded quantification. His subtyping algorithm uses weak head normal forms and is proven complete purely syntactically as in this work. The lexicographic induction on kinds and constructors, which in this article justifies hereditary substitution, is used by the first author to prove a substitution property for algorithmic subtyping, which entails completeness. It remains open whether this argument scales to bounded quantification.

Future work. Steffen has extended his work to F_{<:}^{ω} with polarities, i. e., co-, contra-, and mixed-variant type constructors are distinguished. For this extension, only backtracking algorithms exist [Ste98, p. 102]; we would like to see whether our proof technique can simplify its metatheory as well. The same question arises for the extension F_{≤}^{ω} by bounded abstraction.

Acknowledgments. The research has been partially supported by the EU coordination action TYPES (510996).

References

[Abe06a] A. Abel. Implementing a normalizer using sized heterogeneous types. In C. McBride and T. Uustalu, eds., Wksh. on Mathematically Structured Functional Programming, MSFP 2006 . 2006.

[Abe06b] A. Abel. Polarized subtyping for sized types. In D. Grigoriev, J. Harrison, and E. A. Hirsch, eds., Proc. of the 1st Int. Computer Science Symposium in Russia, CSR 2006 , vol. 3967 of Lect. Notes in Comput. Sci., pp. 381–392. Springer-Verlag, 2006.

[AC96] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[AC97] R. Amadio and P.-L. Curien. Domains and Lambda Calculi. Cambridge University Press, 1997.

[Ada05] R. Adams. A Modular Hierarchy of Logical Frameworks. Ph.D. thesis, University of Manchester, 2005.

[Car88] L. Cardelli. Structural subtyping and the notion of power type. In Proc. of the 15th ACM Symp. on Principles of Programming Languages, POPL’88 , pp. 70–79. 1988.

[CG03] A. B. Compagnoni and H. Goguen. Typed operational semantics for higherorder subtyping. Inf. Comput., 184(2):242–297, 2003.

[CG06] A. Compagnoni and H. Goguen. Anti-symmetry of higher-order subtyping and equality by subtyping. Math. Struct. in Comput. Sci., 16:41–65, 2006.

[CG07] A. Compagnoni and H. Goguen. Subtyping à la Church. In E. Barendsen, V. Capretta, H. Geuvers, and M. Niqui, eds., Reflections on Type Theory, λcalculus, and the Mind. Essays dedicated to Henk Barendregt on the Occasion of his 60th Birthday. Radboud University Nijmegen, 2007.

[Com95] A. B. Compagnoni. Decidability of higher-order subtyping with intersection types. In L. Pacholski and J. Tiuryn, eds., Computer Science Logic, 8th Int. Wksh., CSL ’94 , vol. 933 of Lect. Notes in Comput. Sci., pp. 46–60. Springer-Verlag, 1995.

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys, 17(4):471–522, 1985.

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

[HL07] R. Harper and D. Licata. Mechanizing metatheory in a logical framework. J. Func. Program., 17(4–5):613–673, 2007.

[LCH07] D. K. Lee, K. Crary, and R. Harper. Towards a mechanized metatheory of Standard ML. In M. Hofmann and M. Felleisen, eds., Proc. of the 34th ACM Symp. on Principles of Programming Languages, POPL 2007 , pp. 173–184. ACM Press, 2007.

[Lév76] J.-J. Lévy. An algebraic interpretation of the λβK-calculus; and an applica-

tion of a labelled λ-calculus. Theor. Comput. Sci., 2(1):97–114, 1976.

[Mit90] J. C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proc. of the 17th ACM Symp. on Principles of Programming Languages, POPL’90 , pp. 109–124. 1990.

[Pie92] B. C. Pierce. Bounded quantification is undecidable. In POPL, pp. 305–315. 1992.

[Pie02] B. C. Pierce. Types and Programming Languages. MIT Press, 2002.

[Pra65] D. Prawitz. Natural Deduction. Almqvist & Wiksell, Stockholm, 1965. Republication by Dover Publications Inc., Mineola, New York, 2006.

[PS97] B. C. Pierce and M. Steffen. Higher order subtyping. Theor. Comput. Sci., 176(1,2):235–282, 1997.

[Rod07] D. Rodriguez. Algorithmic Subtyping for Higher Order Bounded Quantification. Diploma thesis, LMU Munich, 2007.

[Ste98] M. Steffen. Polarized Higher-Order Subtyping. Ph.D. thesis, Technische Fakultät, Universität Erlangen, 1998.

[WC^{+}03] K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework I: Judgements and properties. Tech. rep., School of Computer Science, Carnegie Mellon University, Pittsburgh, 2003.