MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Proof Normalization and Subject Reduction in Extensions of Fsub

Sergei Vorobyov

MPI–I–95–2–001 January 1995

[figure: I N F O R M A T I K]

Im Stadtwald D 66123 Saarbrücken

Germany Author’s Address

Sergei Vorobyov (sv@mpi-sb.mpg.de), Max–Planck–Institut für Informatik Im Stadtwald D-66123 Saarbrücken Germany (http://www.mpi-sb.mpg.de/guide/staff/sv/sv.html)

Publication Notes

Acknowledgements

I greatly benefited from discussions with Martín Abadi and Benjamin Pierce.

Abstract

System F_{≤}, the second-order polymorphic typed λ-calculus with subtyping appeared to be undecidable because of the undecidability of its subtyping component. The discovery of decidable extensions of the F_{≤}-subtyping relation put forward a challenging problem of incorporating these extensions into an F_{≤}-like typing in a decidable and coherent manner. In this paper we describe a family of systems combining the standard F_{≤}-typing rules with converging hierarchies of decidable extensions of the F_{≤}-subtyping and give decidable criteria for successful proof normalization and subject reduction.

Proof Normalization and Subject Reduction in Extensions of F_{≤}

Sergei Vorobyov

Max-Planck-Institut für Informatik Im Stadtwald, D-66123, Saarbrücken, Germany (e-mail: sv@mpi-sb.mpg.de, Phone: (49) 681-302-5391, Fax: (49) 681-302-5401)

January 16, 1995

Abstract System F_{≤}, the second-order polymorphic typed λ-calculus with subtyping [CW85, BL90, BTCCS91, CG92, CMMS94], appeared to be undecidable because of the undecidability of its subtyping component [Pie92]. The discovery of decidable extensions of the F_{≤}-subtyping relation [Vor94a, Vor95] put forward a challenging problem of incorporating these extensions into an F_{≤}-like typing in a decidable and coherent manner. In this paper we describe a family of systems combining the standard F_{≤}-typing rules with converging hierarchies of decidable extensions of the F_{≤}-subtyping and give decidable criteria for successful proof normalization and subject reduction.

1 Introduction

The well-known second-order polymorphic typed λ-calculus with subtyping, system F_{≤} [CW85, BL90, BTCCS91, CG92, CMMS94], extends Girard’s system F by 1) an auxiliary subtyping relation Γ ⊢ σ ≤ τ, 2) restricting type substitutions in type quantification and abstraction to subtypes of a given type, (Λα ≤ ρ . t) : (∀α ≤ ρ . τ), and 3) possibility to promote a type of a term to all supertypes by using the so-called (Subsumption) rule:

\begin{aligned}Γ ⊢ t : σ & Γ ⊢ σ ≤ τ \\ & Γ ⊢ t : τ \end{aligned}  (Sub)

The F_{≤} subtyping relation Γ ⊢ σ ≤ τ is generated by a simple collection of inference rules, with the most spectacular one, allowing for subtyping two boundedly quantified universal types:

\begin{matrix}Γ ⊢ τ_{1} ≤ σ_{1} & Γ , α ≤ τ_{1} ⊢ σ_{2} ≤ τ_{2} \\ Γ ⊢ (∀α ≤ σ_{1} . σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2}) \end{matrix}  (All)

In contrast to the simply-typed λ-calculus and system F, where the typing proofs are uniquely determined, a term in F_{≤} may have (infinitely) many different proofs and types. But F_{≤} possesses a nice minimal type property, guaranteeing the existence of a minimal type for every F_{≤}-typeable term [CG92]. This minimal type is a subtype of every other type of the same term in the same context, and can be extracted from the uniquely determined normal typing proof of the term. Therefore, for the F_{≤}-typechecking, it would have been sufficient to compute a minimal type of a term and to verify whether it subtypes to a given type.

However, the F_{≤} subtyping relation was proved undecidable by B.Pierce [Pie92]. As a consequence, the typing relation is also undecidable.

Weakening the F_{≤} subtyping relation, by restricting or modifying the above quantifier rule (All), does not give completely satisfactory subsystems of F_{≤}. For example, the system F_{≤}^{⊤} [CP94], obtained by replacing τ_{1} by the largest type ⊤ in the right premise of (All), fails to possess the minimal type property (G.Ghelli). Despite the decidability of the F_{≤}^{⊤} subtyping relation, the decidability of typing in F_{≤}^{⊤} is still open. Replacing the same occurrence of τ_{1} by σ_{1} yields the system with nontransitive subtyping and open decidability problem for subtyping [CP94].

A possibility to circumvent the undecidability of F_{≤} by reinforcement (as opposed to weakening) was suggested in [Vor94a]. It turns out that the F_{≤} subtyping theory is not essentially undecidable [TMR53], possessing infinitely many different consistent decidable extensions. Every such extension is closed with respect to the F_{≤} subtyping rules and proves all F_{≤}-provable subtypings (plus, being decidable, necessarily something else, but not all subtyping judgments). This result was obtained by interpreting the F_{≤} subtyping in M. Rabin’s [Rab69] (weak) monadic second-order theories of successors (W)SnS [Vor94a, Vor95]. However, the direct (W)SnS-interpretations were not satisfactory for typing. First, they subtyped differently structured types. Second, each of them proved ⊢ ⊤ ≤ ⊤ → ⊤ and ⊢ ⊤ ≤ (∀γ ≤ ⊤ . ⊤). Therefore, assuming the standard F_{≤} typing rules, every term is typeable with the ⊤ type. The direct (W)SnS-interpretations were made more subtle, to avoid the above drawbacks, by combining them with the F_{≤}-like subtyping rules, [Vor95]. The main result of [Vor95] can be interpreted as a

Refinement Theorem. Given a (decidable) extension T ⊃ F_{≤} of the F_{≤} subtyping relation, closed with respect to the F_{≤}-subtyping rules, one can construct a “more tight” (decidable) extension T′ such that F_{≤} ⊂ T′ ⊂ T and T′ is also closed with respect to the F_{≤}-subtyping rules. □

As a boundary case, for T = F_{≤} the refinement gives T′ = F_{≤} as the only fixpoint. The premise of the Refinement Theorem is satisfied, in particular (but not only), by the original (W)SnSinterpretations of F_{≤} [Vor94a, Vor95]. Iterating the Refinement Theorem one gets better and better decidable approximations to the undecidable F_{≤}-subtyping, and the genuine F_{≤}-subtyping as a limit. The properties of these hierarchies of converging decidable subtyping theories were investigated in depth in [Vor94b]. In particular, subtyping judgments distinguishing levels k and k + 1 were constructed. Such judgments were then used to construct counterexamples to the substitution property (which is true for F_{≤}):

Γ ⊢ (∀γ ≤ σ_{1} . σ_{2}) ≤ (∀γ ≤ τ_{1} . τ_{2}) & Γ ⊢ ρ ≤ τ_{1} ⇒ Γ ⊢ σ_{2}[ρ/γ] ≤ τ_{2}[ρ/γ].  (1)

Generally, the premises of (1) live in a higher hierarchy level than the conclusion. Sufficient conditions guaranteeing that they all belong to the same level were studied in [Vor94b]. This non-standard subtyping behavior has far-going consequences on the corresponding typing relation [Vor94c] and, as we show in this paper, makes typing proof normalization and the subject reduction property quite sophisticated.

Some results on combining the hierarchies of decidable extensions of the F_{≤}-subtyping with the standard F_{≤} typing rules are given in [Vor94c]. Notably, it is demonstrated that 1) all the resulting systems extend F_{≤}, typing every F_{≤}-typeable term, 2) the normal typing relation is decidable in all extensions, 3) proofs that do not normalize correspond to provably F_{≤}-untypeable terms.

In this paper we address the problem of subject reduction in extensions of F_{≤}, i.e., preservation of types of well-typed terms by the 1st- and 2nd-order β-reduction (η-reduction poses no additional problems and will be considered elsewhere). Successful subject reduction is a consequence of the following three principal properties:

1. proof normalization, especially of type applications: a normal proof of Γ ⊢ t : (∀γ ≤ σ_{1} . σ_{2}) and a proof of Γ ⊢ θ ≤ σ_{1} should transform to a normal proof of Γ ⊢ t {θ} : σ_{2}[θ/γ].

2. Term-in-Typing-substitution: Γ, x : σ, Γ′ ⊢ t : τ and Γ ⊢ s : σ should imply Γ, Γ′ ⊢ t[s/x] : τ.

3. Type-in-Typing-substitution: Γ, α ≤ σ, Γ′ ⊢ t : τ and Γ ⊢ ρ ≤ σ should imply Γ, Γ′[ρ/α] ⊢ t[ρ/α] : τ[ρ/α].

All these properties hold for F_{≤}. In extensions, as the proof normalization depends on the substitution property (1), they may fail. But we are able to give the decidable criteria guaranteeing that they hold. These criteria are tautologically true for F_{≤} (we thus get another proof of the subject reduction property for F_{≤}), and, being decidable, could be added to the notion of well-typedness. As a result, we get decidable extensions of the F_{≤}-typing satisfying the subject reduction property.

The paper is organized as follows. After Section 2 on preliminaries, we define in Section 3 hierarchies of decidable extensions of the F_{≤}-subtyping, and the corresponding typing systems in Section 4. Proof normalization is addressed in Sections 5–7. Sections 8–13 are devoted to type and term substitutions. Subject reduction is discussed in Sections 14–16. In Section 17 we consider the example suggested by B. Pierce.

Martín Abadi and Benjamin Pierce constantly supplied me with counterexamples and encouragement.

2 Preliminaries

Definition 2.1 The set of boundedly quantified types is defined by the grammar:

𝕋 ≡_{df} 𝕍 | ⊤ | 𝕋 → 𝕋 | ∀ 𝕍 ≤ 𝕋 . 𝕋

where: 1) 𝕍 is a set of type variables further denoted by Greek letters α, β, γ; 2) ⊤ is the largest type; 3) → is the functional type constructor; 4) ∀α ≤ ρ . τ is a boundedly quantified universal type: a function assigning to each subtype σ of ρ, σ ≤ ρ, the type τ[σ/α] obtained from τ by substituting σ instead of free occurrences of α. In ∀α ≤ ρ . τ the bound ρ does not contain α free. Further, variable or compound types are denoted by Greek letters σ, τ, ρ, θ, ϕ, ψ.

Definition 2.2 The second-order polymorphic terms are defined by:

T ≡_{df} V | λV : 𝕋 . T | T T | Λ𝕍 ≤ 𝕋 . T | T {𝕋} ,

corresponding respectively to object variables, functional and type abstraction and application.

Definition 2.3 A context Γ is a finite sequence of subtyping and typing assumptions on variables. Dom(Γ) is the set of variables appearing to the left of ≤ and : in a context Γ, F V (e) is the set of free variables in expression e. Contexts are defined inductively: 1) ∅ is a context. 2) If Γ is a context, x ∈ V, x ∉ Dom(Γ), σ ∈ 𝕋, and F V (σ) ⊆ F V (Γ) then Γ, x : σ is a context. 3) If Γ is a context, α ∈ 𝕍, α ∉ Dom(Γ), σ ∈ 𝕋, and F V (σ) ⊆ F V (Γ) then Γ, α ≤ σ is a context. Define Γ(α) = σ and Γ(x) = σ if Γ contains α ≤ σ or x : σ respectively. Define Γ^{∗}(α) as Γ(α) if the latter is not a variable, and as Γ^{∗}(Γ(α)) otherwise^{1}.

A subtyping judgment is a figure of the form Γ ⊢ σ ≤ τ, where F V (σ) ∪ F V (τ) ⊆ Dom(Γ).

A typing judgment is a figure of the form Γ ⊢ t : τ where F V (t) ∪ F V (τ) ⊆ Dom(Γ).

A V-∀-subtyping is a judgment of the form Γ ⊢ α ≤ (∀γ ≤ σ_{1} . σ_{2}).

3 Stratified Subtyping

The following is a slightly modified (by adding upper indices) Curien-Ghelli’s algorithmic variant of F_{≤} (subtyping component) [CG92].

1Note that Γ^{∗}(α) is always either ⊤, or a universal, or an arrow type

Definition 3.1 A stratified subtype relation Γ ⊢^{(k)} σ ≤ τ (k ∈ ℕ) is defined by the rules:

Γ ⊢^{(k)} α ≤ α (Refl) Γ ⊢^{(k)} τ ≤ ⊤ (T op)

\begin{matrix}Γ ⊢^{(k)} τ_{1} ≤ σ_{1} & Γ ⊢^{(k)} σ_{2} ≤ τ_{2} \\ Γ ⊢^{(k)} σ_{1} → σ_{2} ≤ τ_{1} → τ_{2} \end{matrix}  (Arrow)

\begin{matrix}Γ ⊢^{(k)} τ_{1} ≤ σ_{1} & Γ, α ≤ τ_{1} ⊢^{(k)} σ_{2} ≤ τ_{2} \\ Γ ⊢^{(k)} (∀α ≤ σ_{1} . σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2}) \end{matrix}  (All)

\begin{matrix}Γ ⊢^{(k)} Γ^{∗}(α) ≤ (∀β ≤ ρ . τ) \\ Γ ⊢^{(k+1)} α ≤ (∀β ≤ ρ . τ) \end{matrix}  (AlgT rans-∀)

Γ ⊢^{(k)} Γ(α) ≤ τ

{τ is not a ∀-type}

Γ ⊢^{(k)} α ≤ τ

(AlgT rans)

plus a set H of additional axioms of the form Γ ⊢^{(0)} α ≤ (∀γ ≤ σ_{1} . σ_{2}), called ∀-hypotheses. □

Note that two principal differences, as compared to F_{≤}, are: 1) different levels, k and k + 1, in the premise and the conclusion of (AlgT rans-∀), and 2) the set of additional axioms H. Respectively, two possibilities to turn the above system into F_{≤} are: either 1) letting k = ω and H empty, or 2) letting H equal the set of F_{≤}-provable judgments of the form Γ ⊢ α ≤ (∀γ ≤ σ_{1} . σ_{2}). Other choices of H may lead to converging hierarchies of decidable extensions of the F_{≤}-subtyping:

Theorem 3.2 ([Vor94b]) If the set H of ∀-axioms is decidable, closed with respect to the scheme: Γ ⊢^{(0)} α ≤ σ ∈ H & Γ ⊢^{(0)} σ ≤ τ ⇒ Γ ⊢^{(0)} α ≤ τ ∈ H, and contains every F_{≤}-provable V-∀-subtyping, then:

1. for every k, the relation Γ ⊢^{(k)} σ ≤ τ is decidable, transitive, and extends F_{≤};

2. every Γ ⊢^{(k)} properly extends Γ ⊢^{(k+1)} ; Γ ⊢_{F_{≤}} is the intersection of all Γ ⊢^{(k)} . □

A trivial example is given by H = {all V-∀-subtypings}. An infinite number of different and less obvious choices are suggested by (W)SnS-interpretations of F_{≤} [Vor94a, Vor95], each of them leads to a decidable converging hierarchy extending F_{≤}. For every k there exist judgments distinguishing levels k and k + 1, i.e., Γ ⊢^{(k)} σ ≤ τ, but not Γ ⊢^{(k+1)} σ ≤ τ. One can also construct closed types σ, τ with the spectacular properties, impossible in F_{≤}, (see [Vor94c]:

γ ≤ σ ⊢^{(k)} γ ≤ τ,  (2)
⊬^{(k)} σ ≤ τ.  (3)

The types σ, τ provide counterexamples to the following substitution property, true for F_{≤}:

Γ ⊢ (∀γ ≤ σ_{1} . σ_{2}) ≤ (∀γ ≤ τ_{1} . τ_{2}) & Γ ⊢ ρ ≤ ρ_{1} ⇒ Γ ⊢ σ_{2}[ρ/γ] ≤ τ_{2}[ρ/γ]

Consider, e.g., ⊢^{(k)} (∀γ ≤ ⊤ . γ) ≤ (∀γ ≤ σ . τ), which is equivalent, by (All) and (T op), to (2), hence true. But substituting [σ/γ] in it yields (3).

In general, type substitution leads to the level decreasing. In the example above we have:

⊢^{(k+1)} (∀γ ≤ ⊤ . γ) ≤ (∀γ ≤ σ . τ) ⇒ ⊢^{(k)} σ ≤ τ  (4)

Such non-standard behavior of substitution make typing proof normalization and subject reduction quite subtle, subject to certain preconditions, as will be discussed in the sequel.

4 Normal Typing

Definition 4.1 For every k ∈ ℕ the minimal normal ⊢_{mn}^{(k)} and normal ⊢_{n}^{(k)} typing relations are defined by the following inference rules:

Γ ⊢_{mn}^{(k)} x : Γ(x) (μ-V ar)

Γ, α ≤ σ ⊢_{mn}^{(k)} r : τ ; \overline{(μ-T Abs)} ; Γ ⊢_{mn}^{(k)} (Λα ≤ σ . r) : (∀α ≤ σ . τ) Γ, x : σ ⊢_{mn}^{(k)} r : τ ; \overline{(μ-F Abs)} ; Γ ⊢_{mn}^{(k)} (λx : σ . r) : σ → τ

\{ \begin{matrix}either & Γ ⊢_{mn}^{(k)} f : σ → τ \\ or & Γ ⊢_{mn}^{(k)} f : α, Γ^{∗}(α) ≡ σ → τ \end{matrix}  Γ ⊢_{n}^{(k)} t : σ
\overline{(μ-F App)}
Γ ⊢_{mn}^{(k)} f t : τ

\{ \begin{matrix}either & Γ ⊢_{mn}^{(k)} r : (∀γ ≤ σ_{1} . σ_{2}) \\ or & Γ ⊢_{mn}^{(k)} r : α, Γ^{∗}(α) ≡ (∀γ ≤ σ_{1} . σ_{2}) \end{matrix}  Γ ⊢^{(k)} ϕ ≤ σ_{1}
\overline{(μ-T App)}
Γ ⊢_{mn}^{(k)} r{ϕ} : σ_{2}[ϕ/γ]

Γ ⊢_{mn}^{(k)} r : σ \{ \begin{matrix}Γ ⊢^{(k+1)} & σ ≤ τ & if it is a V-∀-subtyping \\ Γ ⊢^{(k)} & σ ≤ τ & otherwise \end{matrix}
\overline{(Sub)}
Γ ⊢_{n}^{(k)} r : τ

These rules are inspired by [CMMS94]. They incorporate the standard F_{≤}-typing rules with the first major difference that our rules are stratified by levels. By forgetting upper indices one gets the rules of [CMMS94]. The second difference is the presence of two cases of (Subsumption), with the distinguished case of V-∀-subtyping, corresponding to the subtyping rule (AlgT rans-∀). The case of F_{≤} is covered by letting ⊢^{(k)} ≡ ⊢_{F_{≤}}-subtyping. Other possibilities are supplied by using hierarchies of subtyping relations described in Section 3.

Definition 4.2 Define μ(Γ ⊢^{(k)} t), the minimal type of t in Γ ⊢^{(k)} , as the type σ such that Γ ⊢_{mn}^{(k)} t : σ (if it exists). Define π(Γ ⊢^{(k)} t), the principal type of t in Γ ⊢^{(k)} , as:

π(Γ ⊢^{(k)} t) ≡_{df} \{ \begin{matrix}μ(Γ ⊢^{(k)} t), & if μ(Γ ⊢^{(k)} t) is not a variable, \\ Γ^{∗}(μ(Γ ⊢^{(k)} t)), & if μ(Γ ⊢^{(k)} t) is a variable, \\ undefined, & if μ(Γ ⊢^{(k)} t) is undefined. \end{matrix}

Theorem 4.3 ([Vor94c]) Relations Γ ⊢_{mn}^{(k)} t : θ, Γ ⊢_{n}^{(k)} t : θ are decidable, minimal and principal types are computable iff the subtyping relation Γ ⊢^{(k)} σ ≤ τ is decidable.

If τ is minimal for Γ ⊢ t in F_{≤}, then also for every k ∈ ℕ one has μ(Γ ⊢^{(k)} t) = τ. □

5 Normalization

Typing proof normalization is the transformation of non-normal typing proofs into normal ones. Normalization can be described by the schemes like:

Γ ⊢_{n}^{(k)} f : σ → τ Γ ⊢_{n}^{(k)} t : σ
\overline{(N -F App)}
Γ ⊢_{n}^{(k)} f t : τ

which means that given two normal proofs Γ ⊢_{n}^{(k)} f : σ → τ and Γ ⊢_{n}^{(k)} t : σ one can always transform them into a normal proof of Γ ⊢_{n}^{(k)} f t : τ. Note that the above scheme is absent from the set of rules for normal typing (stronger left premise Γ ⊢_{mn}^{(k)} f : σ → τ is stipulated in (μ-F App)). The schemes as (N -F App), provided admissible, can be seen as meta-theorems extending the set of rules for normal typing, or as derivable rules for normal typing.

Given a non-normal proof, one can normalize it, using the normalization schemes. At each step it suffices to choose maximal subproofs that are already normal, and to apply a corresponding normalization scheme, if available. A very useful by-product of typing proof normalization in F_{≤} is that it automatically yields the minimal types for terms. Given a normal typing proof, it suffices to retrieve the type cut by the last subsumption applied in this proof. This type is a subtype of every other type of the same term in the same context, see [CG92].

In the extensions of F_{≤}, the normalization of all constructs, except type application, is easy, see Lemma 5.1. Normalization of type applications is quite subtle and may fail, in general, see Section 6. A criterion for the successful normalization of type applications is given by Lemma 7.1

Lemma 5.1 (Normalization) The following are valid normalization schemes: (N -F App),

Γ, x : σ ⊢_{n}^{(k)} t : τ ; \overline{(N -F Abs)} ; Γ ⊢_{n}^{(k)} (λx : σ . t) : σ → τ Γ, α ≤ σ ⊢_{n}^{(k)} t : τ ; \overline{(N -T Abs)} ; Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) : (∀α ≤ σ . τ)

\begin{matrix}Γ ⊢_{mn}^{(k)} f : α & Γ ⊢^{(k)} α ≤ σ → τ \\ Γ ⊢_{n}^{(k)} f : σ → τ \end{matrix} or \begin{matrix}Γ ⊢_{mn}^{(k)} f : σ′ → τ′ & Γ ⊢^{(k)} σ′ → τ′ ≤ σ → τ \\ Γ ⊢_{n}^{(k)} f : σ → τ \end{matrix}
Γ ⊢^{(k)} σ ≤ σ′,  (5)
Γ ⊢^{(k)} τ′ ≤ τ.  (6)

\{ \begin{matrix}either Γ ⊢_{mn}^{(k)} f : σ′ → τ′, \\ or Γ ⊢_{mn}^{(k)} f : α, Γ^{∗}(α) ≡ σ′ → τ′ \end{matrix}  \begin{matrix}Γ ⊢_{n}^{(k)} t : σ & Γ ⊢^{(k)} σ ≤ σ′^{See (5)} \\ Γ ⊢_{n}^{(k)} t : σ′ \end{matrix}
Γ ⊢_{mn}^{(k)} f t : τ′

Γ ⊢^{(k)} τ′ ≤ τ^{See (6)}

Γ ⊢_{n}^{(k)} f t : τ

(∗J1∗)
Γ, α ≤ σ ⊢_{n}^{(k)} t : τ

Proof. (N -F App): The normal proof of Γ ⊢_{n}^{(k)} f : σ → τ is either In the first case, let σ′ → τ′ ≡ Γ^{∗}(α). From Γ ⊢^{(k)} α ≤ σ → τ by (AlgT rans) we have: Γ ⊢^{(k)} σ′ → τ′ ≤ σ → τ (the same as in the second case). Hence, in both cases, by (Arrow):

Consequently, the normal proof of Γ ⊢_{n}^{(k)} f t : τ may be constructed as follows:

(N -T Abs): The normal proof of Γ, α ≤ σ ⊢_{n}^{(k)} t : τ is:

Γ, α ≤ σ ⊢_{mn}^{(k)} t : τ′

\{ \begin{matrix}either & Γ, α ≤ σ ⊢^{(k+1)} τ′ ≤ τ, & if it is a V-∀-subtyping \\ or & Γ, α ≤ σ ⊢^{(k)} τ′ ≤ τ, & if it is not a V-∀-subtyping \end{matrix}

Since (∗J1∗) always implies, by (All), Γ ⊢^{(k)} (∀α ≤ σ . τ′) ≤ (∀α ≤ σ . τ), the normal proof of Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) : (∀α ≤ σ . τ) is as follows:

\begin{matrix}\begin{matrix}Γ, α ≤ σ ⊢_{mn}^{(k)} t : τ′ \\ Γ, α ≤ σ ⊢_{mn}^{(k)} (Λα ≤ σ . t) : (∀α ≤ σ . τ′) \end{matrix} & Γ ⊢^{(k)} (∀α ≤ σ . τ′) ≤ (∀α ≤ σ . τ) \\ Γ, α ≤ σ ⊢_{n}^{(k)} (Λα ≤ σ . t) : (∀α ≤ σ . τ) \end{matrix}

(N -F Abs): The proof is completely analogous to the preceding one. □

6 Failure of the Type Application Normalization

One of the normal typing rules for the type application is:

Γ ⊢_{mn}^{(k)} r : (∀γ ≤ σ_{1} . σ_{2}) Γ ⊢^{(k)} θ ≤ σ_{1}
\overline{(μ-T App)}
Γ ⊢_{mn}^{(k)} r {θ} : σ_{2}[θ/γ]

The corresponding rule for functional application (μ-F App) gives rise to the normalization scheme (N -F App) from Section 5, which differs from the rule just by replacement of Γ ⊢_{mn}^{(k)} with Γ ⊢_{n}^{(k)} in the left premise and conclusion of (μ-F App). The similarly obtained normalization scheme for (μ-T App):

Γ ⊢_{n}^{(k)} r : (∀γ ≤ σ_{1} . σ_{2}) Γ ⊢^{(k)} θ ≤ σ_{1} ; \overline{(N -T App)} ; Γ ⊢_{n}^{(k)} r \{θ\} : σ_{2}[θ/γ]  (7)

is not valid, in general, in extensions of F_{≤} (but is valid for the F_{≤} itself!). Consider a simple counterexample. Let σ, τ be the closed types with properties (2), (3) from Section 3. Then

r : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} r : (∀γ ≤ σ . τ) (8)

is provable, since the necessary subtyping ⊢^{(k)} (∀γ ≤ ⊤ . γ) ≤ (∀γ ≤ σ . τ) (9)

is equivalent, by (All), to (2). But applying the scheme (7) to (8) and (Refl):

\begin{matrix}r : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} r : (∀γ ≤ σ . τ) & r : (∀γ ≤ ⊤ . γ) ⊢^{(k)} σ ≤ σ \\ r : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} r \{σ\} : τ \end{matrix}

yields the unprovable judgment, since, by (μ-T App), r : (∀γ ≤ ⊤ . γ) ⊢_{mn}^{(k)} r {σ} : σ, and the necessary subtyping r : (∀γ ≤ ⊤ . γ) ⊢^{(k)} σ ≤ τ is unprovable by (3).

The existence of pairs of types with the properties (2), (3) is immanent for hierarchical extensions of the F_{≤}-subtyping [Vor94b, Vor94c]. Therefore, the general failure of (N -T App) is common for all hierarchical extensions of F_{≤}.

7 Successful Normalization of Type Applications

The following lemma establishes the criterion for the successful normalization of type applications in the hierarchical extensions of F_{≤}. Note that the condition (10) is tautologically true for F_{≤}. Thus type applications normalize unconditionally in F_{≤}, which together with Lemma 5.1 gives the proof of the proof normalization theorem for F_{≤} [CG92]. Note also that the condition (10) is effectively decidable in all decidable extensions of Section 3. Finally, if a term is F_{≤}-typeable, its typing proof is normalizable in every extension. Conversely, if it is non-normalizable in some extension, the term is guaranteed to be F_{≤}-untypeable.

Lemma 7.1 (Type Application Normalization Criterion)

Γ ⊢_{n}^{(k)} r : (∀γ ≤ σ_{1} . σ_{2})^{(∗J1∗)}  Γ ⊢^{(k)} θ ≤ σ_{1}^{(∗J2∗)}
\overline{(N -T App)}

Γ ⊢_{n}^{(k)} r {θ} : σ_{2}[θ/γ]^{(∗J3∗)}

if and only if the principal type (∀γ ≤ ρ_{1} . ρ_{2}) ≡ π(Γ ⊢^{(k)} r) satisfies the condition:

\{ \begin{matrix}Γ ⊢^{(k+1)} & ρ_{2}[θ/γ] ≤ σ_{2}[θ/γ], & if it is a V-∀-subtyping, \\ Γ ⊢^{(k)} & ρ_{2}[θ/γ] ≤ σ_{2}[θ/γ], & if it is not a V-∀-subtyping. \end{matrix}  (10)

Proof. (∗J1∗) by (μ-T App) and (Sub) implies Γ ⊢^{(k)} (∀γ ≤ ρ_{1} . ρ_{2}) ≤ (∀γ ≤ σ_{1} . σ_{2}), hence, by (All), Γ ⊢^{(k)} σ_{1} ≤ ρ_{1}, which together with (∗J2∗) gives Γ ⊢^{(k)} θ ≤ ρ_{1}. (11) Therefore, the normal proof of (∗J3∗) looks like:

\begin{matrix}π(Γ ⊢^{(k)} r) ≡ (∀γ ≤ ρ_{1} . ρ_{2}) & Γ ⊢^{(k)} θ ≤ ρ_{1}^{See (11)} \\ Γ ⊢_{mn}^{(k)} r \{θ\} : ρ_{2}[θ/γ] \end{matrix}  \{ (10) \}
\overline{(Sub)}
Γ ⊢_{n}^{(k)} r {θ} : σ_{2}[θ/γ]

Returning to the counterexample of Section 6, it is interesting to see where it violates the conditions of the Lemma. The principal type of r in the counterexample is: ∀γ ≤ ρ_{1} . ρ_{2} ≡ (∀γ ≤ ⊤ . γ), the type (∀γ ≤ σ_{1} . σ_{2}) ≡ (∀γ ≤ σ . τ), and θ ≡ σ. The Lemma stipulates, see (10), that Γ ⊢^{(k)} ρ_{2}[θ/γ] ≡ σ ≤ τ ≡ σ_{2}[θ/γ]. But this is false, see (3), by the choice of σ and τ.

8 Term-in-Typing and Type-in-Typing Substitutions

Term-in-Typing-substitution property, i.e., possibility to derive

\begin{matrix}Γ, x : σ, Γ′ ⊢ t : τ & Γ ⊢ s : σ \\ Γ, Γ′ ⊢ t[s/x] : τ \end{matrix}  (12)

and Type-in-Typing-substitution property, i.e., possibility to derive

\begin{matrix}Γ, α ≤ σ, Γ′ ⊢ t : τ & Γ ⊢ ρ ≤ σ \\ Γ, Γ′[ρ/α] ⊢ t [ρ/α] : τ [ρ/α] \end{matrix}  (13)

are fundamental for typed λ-calculi and indispensable for proving the subject reduction property.

Term-in-Typing- and Type-in-Typing-substitution properties are non-obvious when typing proofs are not uniquely determined, e.g., in the presence of subtyping. Directly substituting one normal proof into another may yield non-normal proofs. Therefore, substitution should be accompanied by a proof normalization. As we saw in Sections 6, 7, successful normalization in extensions of F_{≤} should be subject to certain preconditions. Consequently, some preconditions have to be stipulated to guarantee the correctness of the Term-in-Typing- and Type-in-Typing-substitutions. The problem becomes more sophisticated when the explicit analysis of typing levels is involved.

9 Substitution Properties May Fail in Extensions of F_{≤}

Let σ, τ, be types defined in Section 3 and used to construct the counterexample of Section 6 with the properties (2), (3). Consider the valid judgments:

g : (∀γ ≤ ⊤ . γ), f : (∀γ ≤ σ . τ) ⊢_{mn}^{(k)} f {σ} : τ  (14)
g : (∀γ ≤ ⊤ . γ) ⊢_{mn}^{(k)} g : (∀γ ≤ ⊤ . γ)  (15)

From (15) and (9) we get, by (Sub), g : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} g : (∀γ ≤ σ . τ).

Therefore, g is “good” for substituting instead of f in (14). But the resulting judgment

g : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} (f {σ}) [g/f] ≡ g {σ} : τ

is not valid, since g : (∀γ ≤ ⊤ . γ) ⊢_{mn}^{(k)} g {σ} : σ, but, by (3), ⊬^{(k)} σ ≤ τ. This counterexample shows that the Term-in-Typing-substitution (12) fails, in general in extensions of F_{≤}.

Similarly, for the Type-in-Typing-substitution, always with the same types σ and τ, the next particular case of the scheme (13) has its premises true and the conclusion false:

\begin{matrix}γ ≤ σ, f : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} f \{γ\} : τ & ⊢^{(k)} σ ≤ σ \\ f : (∀γ ≤ ⊤ . γ) ⊢_{n}^{(k)} f \{σ\} : τ \end{matrix}

since f : (∀γ ≤ ⊤ . γ) ⊢_{mn}^{(k)} f {σ} : σ, and for the conclusion of the last figure to be true one needs ⊢^{(k)} σ ≤ τ, which is false by (3). This gives the counterexample to Type-in-Typing-substitution (13).

10 Safety for Term-in-Typing Substitution

Definition 10.1 (Safety I) Let Γ ⊢_{n}^{(k)} s : σ. A provable typing judgment

Γ, x : σ ⊢_{n}^{(k)} t : τ  (16)

is called [s/x]-safe iff for every context term Γ, x : σ, Γ′ ⊢^{(k)} r {θ} that occurs in the proof of (16) and for the principal types

(∀γ ≤ σ_{1} . σ_{2}) ≡_{df} π(Γ, x : σ, Γ′ ⊢^{(k)} r),
(∀γ ≤ ρ_{1} . ρ_{2}) ≡_{df} π(Γ, Γ′ ⊢^{(k)} r[s/x])

the following condition is satisfied:

\{ \begin{matrix}Γ, Γ′ ⊢^{(k+1)} & ρ_{2}[θ/γ] ≤ σ_{2}[θ/γ], & if it is a V-∀-subtyping, \\ Γ, Γ′ ⊢^{(k)} & ρ_{2}[θ/γ] ≤ σ_{2}[θ/γ], & if it is not a V-∀-subtyping. \end{matrix}  (17)

11 Term-in-Typing Substitution Lemma

Lemma 11.1 (Term-in-Typing Substitution) Suppose that Γ ⊢_{n}^{(k)} s : σ.

Then Γ, Γ′ ⊢_{n}^{(k)} t[s/x] : τ^{(∗JX∗)} iff Γ, x : σ, Γ′ ⊢_{n}^{(k)} t : τ^{(∗JY ∗)} is [s/x]-safe.

Proof. By induction on complexity of the term t. If t is a variable, then the conclusion is immediate. Proofs of necessity and of all inductive cases, except type application, are straightforward and omitted here. Inductive Hypothesis. Suppose that the conclusion of the Lemma holds for all proper subterms of t. Type Application. Let t ≡ r {θ}. We have to construct the proof of (∗JX∗). The proof of (∗JY ∗) is:

Γ, x : σ, Γ′ ⊢_{mn}^{(k)} r {θ} : σ_{2}[θ/γ]^{(∗J1∗)} (∗J2∗)

\{ \begin{matrix}Γ, x : σ, Γ′ ⊢^{(k+1)} & σ_{2}[θ/γ] ≤ τ, & for V-∀-subtyping \\ Γ, x : σ, Γ′ ⊢^{(k)} & σ_{2}[θ/γ] ≤ τ, & otherwise \end{matrix}
Γ, x : σ, Γ′ ⊢_{n}^{(k)} r {θ} : τ

where (∀γ ≤ σ_{1} . σ_{2}) is the principal type of r in Γ, x : σ, Γ′ ⊢^{(k)} . The proof of (∗J1∗) is:

(∗J3∗)
\{ \begin{matrix}either & Γ, x : σ, Γ′ ⊢_{mn}^{(k)} & r : α and (Γ, Γ′)^{∗}(α) ≡ (∀γ ≤ σ_{1} . σ_{2}) \\ or & Γ, x : σ, Γ′ ⊢_{mn}^{(k)} & r : (∀γ ≤ σ_{1} . σ_{2}) \end{matrix}

Γ, x : σ, Γ′ ⊢^{(k)} θ ≤ σ_{1}^{(∗J4∗)}

Γ, x : σ, Γ′ ⊢_{mn}^{(k)} r {θ} : σ_{2}[θ/γ]^{(∗J1∗)}

Anyway, both cases in (∗J3∗) imply Γ, x : σ, Γ′ ⊢_{n}^{(k)} r : (∀γ ≤ σ_{1} . σ_{2}). (18) Applying the inductive hypothesis to (18) we get: Γ, Γ′ ⊢_{n}^{(k)} r[s/x] : (∀γ ≤ σ_{1} . σ_{2}). (19) The assumption x : σ in the context of (∗J4∗) can be omitted: Γ, Γ′ ⊢^{(k)} θ ≤ σ_{1}. (20) From (19) and (20), by Lemma 7.1, since (∗JY ∗) is [s/x]-safe, we derive:

Γ, Γ′ ⊢_{n}^{(k)} (r[s/x]){θ} ≡ (r{θ})[s/x] : σ_{2}[θ/γ]. (21)

(21) and (∗J2∗) (with x : σ omitted, subtyping does not depend on typing) yield (∗JX∗). □

12 Safety for Type-in-Typing Substitution

Definition 12.1 (Safety II) Let Γ ⊢^{(k)} ρ ≤ σ. A provable typing judgment

Γ, α ≤ σ ⊢_{n}^{(k)} t : τ  (22)

is called [ρ/α]-safe iff for every context term Γ, α ≤ σ, Γ′ ⊢^{(k)} r {θ} that occurs in the proof of (22) and for the principal types

(∀γ ≤ σ_{1} . σ_{2}) ≡_{df} π(Γ, α ≤ σ, Γ′ ⊢^{(k)} r),
(∀γ ≤ ρ_{1} . ρ_{2}) ≡_{df} π(Γ, Γ′ ⊢^{(k)} r[ρ/α])

the following condition is satisfied:

\{ \begin{matrix}Γ, Γ′[ρ/α] ⊢^{(k+1)} & ρ_{2}[θ/γ] ≤ σ_{2}[θ/γ], & if it is a V-∀-subtyping, \\ Γ, Γ′[ρ/α] ⊢^{(k)} & ρ_{2}[θ/γ] ≤ σ_{2}[θ/γ], & if it is not a V-∀-subtyping. \end{matrix}  (23)

and all subtyping judgments in the proof of (22) are [ρ/α]-stable, i.e.,

Γ, ρ ≤ α, Γ′[ρ/α] ⊢^{(l)} ϕ ≤ ψ ⇒ Γ, Γ′[ρ/α] ⊢^{(l)} ϕ[ρ/α] ≤ ψ[ρ/α]  (24)

Counterexample (4) of Section 3 shows that stability is important.

13 Type-in-Typing Substitution Lemma

Lemma 13.1 (Type-in-Typing Substitution) Suppose that Γ ⊢^{(k)} ρ ≤ σ.

Then Γ, Γ′[ρ/α] ⊢_{n}^{(k)} t[ρ/α] : τ[ρ/α]^{(∗JU∗)} iff Γ, α ≤ σ, Γ′ ⊢_{n}^{(k)} t : τ^{(∗JV ∗)} is [ρ/α]-safe.

Proof. By induction on complexity of the term t. If t is a variable, the conclusion is immediate. Proofs of necessity and all inductive cases, except type application, are straightforward and skipped. Inductive Hypothesis. Suppose that the conclusion of the Lemma holds for all proper subterms of t. Type Application. Let t ≡ r {θ}. We have to construct the proof of (∗JU∗). The proof of (∗JV ∗) is:

Γ, α ≤ σ, Γ′ ⊢_{mn}^{(k)} r {θ} : σ_{2}[θ/γ]^{(∗J1∗)} (∗J2∗)

\{ \begin{matrix}Γ, α ≤ σ, Γ′ ⊢^{(k+1)} & σ_{2}[θ/γ] ≤ τ, & for V-∀-subtyping \\ Γ, α ≤ σ, Γ′ ⊢^{(k)} & σ_{2}[θ/γ] ≤ τ, & otherwise \end{matrix}
Γ, α ≤ σ, Γ′ ⊢_{n}^{(k)} r {θ} : τ

where (∀γ ≤ σ_{1} . σ_{2}) is the principal type of r in Γ, α ≤ σ, Γ′ ⊢^{(k)} . The proof of (∗J1∗) is:

π(Γ, α ≤ σ, Γ′ ⊢^{(k)} r) ≡ (∀γ ≤ σ_{1} . σ_{2})^{(∗J3∗)} Γ, α ≤ σ, Γ′ ⊢^{(k)} θ ≤ σ_{1}^{(∗J4∗)} ; Γ, α ≤ σ, Γ′ ⊢_{mn}^{(k)} r {θ} : σ_{2}[θ/γ]^{(∗J1∗)}

(∗J3∗) implies: Γ, α ≤ σ, Γ′ ⊢_{n}^{(k)} r : (∀γ ≤ σ_{1} . σ_{2}). Therefore, by inductive hypothesis, Γ, Γ′[ρ/α] ⊢_{n}^{(k)} r[ρ/α] : (∀γ ≤ σ_{1}[ρ/α] . σ_{2}[ρ/α]). (25) From (∗J4∗) by stability condition (24), Γ, Γ′[ρ/α] ⊢^{(k)} θ[ρ/α] ≤ σ_{1}[ρ/α]. (26) From (25) and (26), by Lemma 7.1, since (∗JV ∗) is [ρ/α]-safe, we derive:

Γ, Γ′[ρ/α] ⊢_{n}^{(k)} (r {θ})[ρ/α] : (σ_{2}[θ/γ])[ρ/α]. (27) It remains to apply the stability condition (24) to (∗J2∗) to get:

Γ, Γ′ ⊢^{(k+1)} (σ_{2}[θ/γ])[ρ/α] ≤ τ[ρ/α] or Γ, Γ′ ⊢^{(k)} (σ_{2}[θ/γ])[ρ/α] ≤ τ[ρ/α] (28) The desired (∗JU∗) is now derivable from (27) and (28) by (Sub). □

14 Subject Reduction Lemmas

are easy corollaries to Substitution Lemmas 11.1 and 13.1. Lemma 14.1 ((β^{1})-redex/reduct type preservation) For arbitrary k ∈ ℕ consider the uniquely determined normal typing proof of a (β^{1})-redex Γ ⊢_{n}^{(k)} (λx : σ . t) s : θ:

\begin{matrix}Γ, x : σ ⊢_{mn}^{(k)} t : τ^{(∗JA∗)} ; Γ ⊢_{mn}^{(k)} (λx : σ . t) : σ → τ & Γ ⊢_{n}^{(k)} s : σ \\ Γ ⊢_{mn}^{(k)} (λx : σ . t) s : τ \end{matrix}  \{ \begin{matrix}Γ ⊢^{(k+1)} τ ≤ θ & for V-∀-subtyping \\ Γ ⊢^{(k)} τ ≤ θ & otherwise \end{matrix}
Γ ⊢_{n}^{(k)} (λx : σ . t) s : θ

One has the type preservation property for the (β^{1})-reduction:

Γ ⊢_{n}^{(k)} (λx : σ . t) s : θ ⇒ Γ ⊢_{n}^{(k)} t[s/x] : θ

if and only if the typing judgment (∗JA∗) is [s/x]-safe. □ Definition 14.2 ((β^{1}) Redex Safety) In notations of Lemma 14.1, call a (β^{1}) redex Γ ⊢_{n}^{(k)} (λx : σ . t) s : θ safe iff the corresponding typing judgment (∗JA∗) is [s/x]-safe. □ Lemma 14.3 ((β^{2})-redex/reduct type preservation) For arbitrary k ∈ ℕ consider the uniquely determined normal typing proof of a (β^{2})-redex Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) {ρ} : θ:

\begin{matrix}Γ, α ≤ σ ⊢_{mn}^{(k)} t : τ^{(∗JB∗)} ; Γ ⊢_{mn} (Λα ≤ σ . t) : (∀α ≤ σ . τ) & Γ ⊢^{(k)} ρ ≤ σ \\ Γ ⊢_{mn}^{(k)} (Λα ≤ σ . t) \{ρ\} : τ[ρ/α] \end{matrix} \{ \begin{matrix}Γ ⊢^{(k+1)} τ[ρ/α] ≤ θ & for V-∀-subtyping \\ Γ ⊢^{(k)} τ[ρ/α] ≤ θ & otherwise \end{matrix}
Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) {ρ} : θ

One has the type preservation property for the (β^{2})-reduction:

Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) {ρ} : θ ⇒ Γ ⊢_{n}^{(k)} t[ρ/α] : θ

if and only if the typing judgment (∗JB∗) is [ρ/α]-safe. □ Definition 14.4 ((β^{2}) Redex Safety) In notations of Lemma 14.3, call a (β^{2}) redex Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) {ρ} : θ safe iff the corresponding typing judgment (∗JB∗) is [ρ/α]-safe. □ The following is immediate. Proposition 14.5 If the underlying subtyping theory is decidable, then the safety of (β^{1}) and (β^{2}) redices is decidable. □

15 Reduction Relation

We now combine the Reduction Lemmas 14.1 and 14.3 to obtain the Subject Reduction property in its conventional form (as was asked by Martín Abadi), i.e.,

Γ ⊢ t : τ and t reduces to t′ imply Γ ⊢ t′ : τ

First, some effort is needed to define the reduction relation, which is generated by the usual 1st- and 2nd-order beta-reductions and is additionally closed with respect to usual congruences (subterm reduction) and transitivity (many-step reduction).

Definition 15.1 (Reduction Relation) For every k ∈ ℕ the reduction relation Γ ⊢^{(k)} t ⇝ t′ : θ is defined by the following rules (2 axioms: (β^{1}), (β^{2}) and 6 rules: (T rans), (λ-Cong), (F App-Cong-L), (F App-Cong-R), (Λ-Cong), (T App-Cong)):

\begin{matrix}Γ ⊢_{n}^{(k)} (λx : σ . t) s : θ is safe \\ Γ ⊢^{(k)} (λx : σ . t) s ⇝ t[s/x] : θ \end{matrix}  (β^{1})

\begin{matrix}Γ ⊢_{n}^{(k)} (Λα ≤ σ . t) \{ρ\} : θ is safe \\ Γ ⊢^{(k)} (Λα ≤ σ . t) \{ρ\} ⇝ t[ρ/α] : θ \end{matrix}  (β^{2})

\begin{matrix}Γ ⊢^{(k)} r ⇝ s : τ & Γ ⊢^{(k)} s ⇝ t : τ \\ Γ ⊢^{(k)} r ⇝ t : τ \end{matrix}  (T rans)

\begin{matrix}Γ, x : σ ⊢^{(k)} t ⇝ t′ : τ \\ Γ ⊢^{(k)} (λx : σ . t) ⇝ (λx : σ . t′) : σ → τ \end{matrix}  (λ-Cong)

\begin{matrix}Γ ⊢^{(k)} t ⇝ t′ : σ → τ & Γ ⊢_{n}^{(k)} s : σ \\ Γ ⊢^{(k)} t s ⇝ t′ s : τ \end{matrix}  (F App-Cong-L)

\begin{matrix}Γ ⊢_{n}^{(k)} t : σ → τ & Γ ⊢^{(k)} s ⇝ s′ : σ \\ Γ ⊢^{(k)} t s ⇝ t s′ : τ \end{matrix}  (F App-Cong-R)

\begin{matrix}Γ, α ≤ σ ⊢^{(k)} t ⇝ t′ : τ \\ Γ ⊢^{(k)} (Λα ≤ σ . t) ⇝ (Λα ≤ σ . t′) : (∀α ≤ σ . τ) \end{matrix}  (Λ-Cong)

\begin{matrix}Γ ⊢^{(k)} r^{1} ⇝ r^{2} : (∀α ≤ σ . τ) & Γ ⊢^{(k)} ρ ≤ σ \\ Γ ⊢^{(k)} r^{1} \{ρ\} ⇝ r^{2} \{ρ\} : τ[ρ/α] \end{matrix}  (T App-Cong)

[ \begin{matrix}provided that for i = 1, 2, (∀α ≤ ρ_{1}^{i} . ρ_{2}^{i}) ≡ π(Γ ⊢^{(k)} r^{i}) one has: \\ \{ & Γ ⊢^{(k+1)} ρ_{2}^{i}[ρ/α] ≤ τ[ρ/α], if it is a V-∀-subtyping, Γ ⊢^{(k)} ρ_{2}^{i}[ρ/α] ≤ τ[ρ/α], if it is not a V-∀-subtyping. \end{matrix} ]  (29)

A judgment of the form Γ ⊢^{(k)} t ⇝ t′ : θ is called a reduction judgment. □

The only premises of the rules (β^{1}) and (β^{2}) are typing judgments with additional safety conditions (decidable if the underlying subtyping theory Γ ⊢^{(k)} σ ≤ τ is decidable). The right premise of (F App-Cong-L) and the left premise of (F App-Cong-R) are also typing judgments. The right premise of (T App-Cong) is a subtyping judgment. All other premises and conclusions are reduction judgments. The congruence rule (T App-Cong) is subject to the precondition (29) (also decidable if the underlying subtyping theory Γ ⊢^{(k)} σ ≤ τ is decidable). As we mentioned above, the safety preconditions in (β^{1}), (β^{2}), and the precondition (29) of (T App-Cong) are tautologically true for F_{≤}. Therefore, the above reduction system generates the usual (β^{1})-(β^{2})-reduction relation of F_{≤} if the underlying subtyping theory is one of F_{≤}^{2}.

We will extensively use the following auxiliary

Lemma 15.2 If Γ ⊢^{(k)} t ⇝ t′ : θ then Γ ⊢_{n}^{(k)} t : θ.

Proof. By induction on the structure of the inference of the reduction judgment Γ ⊢^{(k)} t ⇝ t′ : θ in the system from Definition 15.1. Every proof of a reduction judgment starts from axioms (β^{1}), (β^{2}) and consists of applications of the rules (T rans), (λ-Cong), (F App-Cong-L), (F App-Cong-R), (Λ-Cong), (T App-Cong).

Basis. If Γ ⊢^{(k)} t ⇝ t′ : θ by (β^{1}) or (β^{2}), then the needed Γ ⊢_{n}^{(k)} t : θ is guaranteed by the premise of (β^{1}) or (β^{2}) respectively.

Inductive Hypothesis. Suppose the claim of the Lemma holds for all reduction judgments appearing in the proof of Γ ⊢^{(k)} t ⇝ t′ : θ (except itself!) in the system of Definition 15.1.

To prove that the claim holds also for Γ ⊢^{(k)} t ⇝ t′ : θ itself, we make the case analysis on a last rule from Definition 15.1 applied in the proof of Γ ⊢^{(k)} t ⇝ t′ : θ.

Case of (T rans): Let the judgment Γ ⊢^{(k)} t ⇝ t′ : θ be obtained from Γ ⊢^{(k)} t ⇝ t′′ : θ (A) and Γ ⊢^{(k)} t′′ ⇝ t′ : θ by (T rans). From (A), by inductive hypothesis, Γ ⊢_{n}^{(k)} t : θ, which is needed.

Case of (λ-Cong): Let the reduction judgment

Γ ⊢^{(k)} t ≡ (λx : σ . r) ⇝ (λx : σ . r′) ≡ t′ : σ → τ ≡ θ

be obtained from Γ, x : σ ⊢^{(k)} r ⇝ r′ : τ (A) by (λ-Cong). From (A), by inductive hypothesis, Γ, x : σ ⊢_{n}^{(k)} r : τ (B). Therefore, from (B), by Normalization Lemma 5.1, Γ ⊢_{n}^{(k)} t ≡ (λx : σ . r) : σ → τ ≡ θ, which is needed.

Case of (F App-Cong-L): Let Γ ⊢^{(k)} t ≡ r s ⇝ r′ s ≡ t′ : τ be derived from Γ ⊢^{(k)} r ⇝ r′ : σ → τ (A) and Γ ⊢_{n}^{(k)} s : σ (B) by (F App-Cong-L). From (A), by inductive hypothesis, Γ ⊢_{n}^{(k)} r : σ → τ (C). Therefore, (C) and (B), by Normalization Lemma 5.1, yield the desired Γ ⊢_{n}^{(k)} t ≡ r s : τ.

Case of (F App-Cong-R): Let Γ ⊢^{(k)} t ≡ r s ⇝ r s′ ≡ t′ : τ be derived from Γ ⊢_{n}^{(k)} r : σ → τ (A) and Γ ⊢^{(k)} s ⇝ s′ : σ (B) by (F App-Cong-R). From (B), by inductive hypothesis, Γ ⊢_{n}^{(k)} s : σ (C). Therefore, (A) and (C), by Normalization Lemma 5.1, yield the needed Γ ⊢_{n}^{(k)} t ≡ r s : τ.

Case of (Λ-Cong): Let the reduction judgment

Γ ⊢^{(k)} t ≡ (Λα ≤ σ . r) ⇝ (Λα ≤ σ . r′) ≡ t′ : (∀α ≤ σ . τ) ≡ θ

be obtained from Γ, α ≤ σ ⊢^{(k)} r ⇝ r′ : τ (A) by (Λ-Cong). From (A), by inductive hypothesis, Γ, α ≤ σ ⊢_{n}^{(k)} r : τ (B). Therefore, from (B), by Normalization Lemma 5.1, Γ ⊢_{n}^{(k)} t ≡ (Λα ≤ σ . r) : (∀α ≤ σ . τ) ≡ θ, which is needed.

2Cf., Paul Dirac’s correspondence principle.

Case of (T App-Cong): Let Γ ⊢^{(k)} t ≡ r {ρ} ⇝ r′ {ρ} ≡ t′ : τ[ρ/α] be derived from Γ ⊢^{(k)} r ⇝ r′ : (∀α ≤ σ . τ) (A) and Γ ⊢^{(k)} ρ ≤ σ (B) by (T App-Cong). From (A), by inductive hypothesis, Γ ⊢_{n}^{(k)} r : (∀α ≤ σ . τ) (C). Therefore, (C) and (B), by Normalization Lemma 7.1 (because of (29)) yield the desired Γ ⊢_{n}^{(k)} t ≡ r {ρ} : τ[ρ/α]. □

16 Subject Reduction Theorem

Theorem 16.1 (Subject Reduction) Suppose Γ ⊢_{n}^{(k)} t : θ and Γ ⊢^{(k)} t ⇝ t′ : θ. Then Γ ⊢_{n}^{(k)} t′ : θ. □ Remark. By Lemma 15.2, the first assumption of the Theorem may be skipped, but we keep it for the sake of standardness. □

Proof. By induction on the structure of the inference of the reduction judgment Γ ⊢^{(k)} t ⇝ t′ : θ in the system from Definition 15.1. Every proof of a reduction judgment starts from axioms (β^{1}), (β^{2}) and consists of applications of the rules (T rans), (λ-Cong), (F App-Cong-L), (F App-Cong-R), (Λ-Cong), (T App-Cong). Basis is immediate: the cases of (β^{1}), (β^{2}) are guaranteed by Lemmas 14.1 and 14.3. Inductive Hypothesis. Suppose the claim of the Theorem is true for all reduction judgments appearing in the proof of the reduction judgment Γ ⊢^{(k)} t ⇝ t′ : θ, except itself. We have to prove that the claim holds for Γ ⊢^{(k)} t ⇝ t′ : θ itself. It suffices to make the case analysis on a last rule from Definition 15.1 applied in the proof of Γ ⊢^{(k)} t ⇝ t′ : θ. Case of (T rans): Let Γ ⊢_{n}^{(k)} t : θ (A) and the reduction judgment Γ ⊢^{(k)} t ⇝ t′ : θ be obtained from Γ ⊢^{(k)} t ⇝ t′′ : θ (B) and Γ ⊢^{(k)} t′′ ⇝ t′ : θ (C) by (T rans). Then, from (A) and (B), by inductive hypothesis, Γ ⊢_{n}^{(k)} t′′ : θ (D). Therefore, from (D) and (C), again by inductive hypothesis, Γ ⊢_{n}^{(k)} t′ : θ, which is needed. Case of (λ-Cong): Let Γ ⊢_{n}^{(k)} t ≡ (λx : σ . r) : σ → τ ≡ θ and the reduction judgment Γ ⊢^{(k)} (λx : σ . r) ⇝ (λx : σ . r′) ≡ t′ : θ be obtained from Γ, x : σ ⊢^{(k)} r ⇝ r′ : τ (A) by (λ-Cong). From (A), by Auxiliary Lemma 15.2, Γ, x : σ ⊢_{n}^{(k)} r : τ (B). From (B) and (A), by inductive hypothesis, Γ, x : σ ⊢_{n}^{(k)} r′ : τ (C). From (C), by Normalization Lemma 5.1, Γ ⊢_{n}^{(k)} t′ ≡ (λx : σ . r′) : σ → τ ≡ θ, which is needed.

Case of (F App-Cong-L): Let Γ ⊢_{n}^{(k)} t ≡ r s : τ and Γ ⊢^{(k)} r s ⇝ r′ s ≡ t′ : τ (A) be derived from Γ ⊢^{(k)} r ⇝ r′ : σ → τ (B) and Γ ⊢_{n}^{(k)} s : σ (C) by (F App-Cong-L). From (B), by Auxiliary Lemma 15.2, Γ ⊢_{n}^{(k)} r : σ → τ (D). By inductive hypothesis, (D) and (B) imply Γ ⊢_{n}^{(k)} r′ : σ → τ (E). From (E) and (C), by Normalization Lemma 5.1, Γ ⊢_{n}^{(k)} t′ ≡ r′ s : τ, which is needed. Case of (F App-Cong-R): Let Γ ⊢_{n}^{(k)} t ≡ r s : τ and Γ ⊢^{(k)} r s ⇝ r s′ ≡ t′ : τ (A) be derived from Γ ⊢_{n}^{(k)} r : σ → τ (B) and Γ ⊢^{(k)} s ⇝ s′ : σ (C) by (F App-Cong-R). From (C), by Auxiliary Lemma 15.2, Γ ⊢_{n}^{(k)} s : σ (D). By inductive hypothesis, (D) and (C) imply Γ ⊢_{n}^{(k)} s′ : σ (E). From (B) and (E), by Normalization Lemma 5.1, Γ ⊢_{n}^{(k)} t′ ≡ r s′ : τ, which is needed. Case of (Λ-Cong): Let Γ ⊢_{n}^{(k)} t ≡ (Λα ≤ σ . r) : (∀α ≤ σ . τ) ≡ θ and the judgment Γ ⊢^{(k)} (Λα ≤ σ . r) ⇝ (Λα ≤ σ . r′) ≡ t′ : θ be obtained from Γ, α ≤ σ ⊢^{(k)} r ⇝ r′ : τ (A) by (Λ-Cong). From (A), by Auxiliary Lemma 15.2, Γ, α ≤ σ ⊢_{n}^{(k)} r : τ (B). From (B) and (A), by inductive hypothesis, Γ, α ≤ σ ⊢_{n}^{(k)} r′ : τ (C). From (C), by Normalization Lemma 5.1, Γ ⊢_{n}^{(k)} t′ ≡ (Λα ≤ σ . r′) : (∀α ≤ σ . τ) ≡ θ, which is needed.

Case of (T App-Cong): Let Γ ⊢_{n}^{(k)} t ≡ r {ρ} : τ[ρ/α] ≡ θ and the refuction judgment Γ ⊢^{(k)} r {ρ} ⇝ r′ {ρ} ≡ t′ : τ[ρ/α] be derived from Γ ⊢^{(k)} r ⇝ r′ : (∀α ≤ σ . τ) (A) and Γ ⊢^{(k)} ρ ≤ σ (B) by (T App-Cong). From (A), by Auxiliary Lemma 15.2, Γ ⊢_{n}^{(k)} r : (∀α ≤ σ . τ) (C). By inductive hypothesis, (C) and (A) imply Γ ⊢_{n}^{(k)} r′ : (∀α ≤ σ . τ) (D). From (D) and (B), by Normalization Lemma 7.1 (and because of (29)) we get Γ ⊢_{n}^{(k)} t′ ≡ r′ s : τ, which is needed. □

17 B. Pierce’s Counterexample

Benjamin Pierce suggested the following elegant “counterexample”, well illustrating the above notions and problems. It also shows that the safety preconditions in Subject Reduction Lemmas are essential and could not be relaxed.

Consider the following types and judgments defined in Section 15 of [Vor94b]:

τ ≡ ∀γ ≤ ⊤ . ((⊤ → ⊤) → ⊤)
ρ ≡ ∀γ ≤ ⊤ . (⊤ → ⊤)
Γ, α ≤ τ ⊢^{(0)} α ≤ ρ  (30)
Γ ⊢^{(0)} τ ≤ ρ  (31)

Proposition 17.1 For every SnS-based [Vor95] set of ∀-hypotheses H the judgment (30) is true and the judgment (31) is false. □

This is established by direct calculations. (Similarly, as shown in Section 16 of [Vor94b], one can find judgments with the same properties at every level ⊢^{(k)}, k ∈ ℕ).

Let Γ be the context i : ⊤. Define the following terms:

\begin{aligned}u & ≡_{df} & λg : ρ . g \{⊤\} i & : & ρ → ⊤ \\ v & ≡_{df} & Λα ≤ τ λh : α . u h & : & ∀α ≤ τ . (α → ⊤) \\ f & ≡_{df} & Λγ ≤ ⊤ λg : ⊤ → ⊤ . g i & : & ∀γ ≤ ⊤ . ((⊤ → ⊤) → ⊤) ≡ τ \\ w & ≡_{df} & (v \{τ\}) f & : & ⊤ \end{aligned}

(the right column contains their minimal types in context Γ computed immediately by the rules of Section 4, see also the typing proofs below).

Consider the β-reduction chain for the term w:

(v {τ}) f → (λh : τ . u h) f → (λg : ρ . g {⊤} i) f → f {⊤} i → i i  (32)

The last term i i in this sequence is ill-typed. What is the problem?

Let us consider the typing proof of the first (β^{2})-redex in (32):

v {τ} ≡ (Λα ≤ τ . λh : α . ((λg : ρ . g ⊤ i) h)) {τ}  (33)

For typographical reasons we have to cut the proof into pieces.

Subproof 1:

Γ, α ≤ τ, h : α, g : ρ ⊢_{mn}^{(0)} g : ρ … ⊢^{(0)} ⊤ ≤ ⊤ ; \overline{(μ-T App)} ; Γ, α ≤ τ, h : α, g : ρ ⊢_{mn}^{(0)} g ⊤ : ⊤ → ⊤ … ⊢_{n}^{(0)} i : ⊤
\overline{(μ-F App)}
Γ, α ≤ τ, h : α, g : ρ ⊢_{mn}^{(0)} g ⊤ i : ⊤
\overline{(μ-F Abs)}
Γ, α ≤ τ, h : α ⊢_{mn}^{(0)} (λg : ρ . g ⊤ i) : ρ → ⊤

where … ⊢_{n}^{(0)} i : ⊤ is proved from the axioms … ⊢_{mn}^{(0)} i : ⊤ (recall that Γ ≡ i : ⊤) and … ⊢^{(0)} ⊤ ≤ ⊤ by (Sub). Subproof 2:

Γ, α ≤ τ, h : α ⊢_{mn}^{(0)} h : α Γ, α ≤ τ, h : α ⊢^{(0)} α ≤ ρ
\overline{(Sub)}
Γ, α ≤ τ, h : α ⊢_{n}^{(0)} h : ρ

The right subtyping premise in this proof is equivalent to (30). Subproof 3:

(*See Subproof 1*)

Γ, α ≤ τ, h : α ⊢_{mn}^{(0)} (λg : ρ . g ⊤ i) : ρ → ⊤

(*See Subproof 2*) Γ, α ≤ τ, h : α ⊢_{n}^{(0)} h : ρ

\overline{(μ-F App)}
Γ, α ≤ τ, h : α ⊢_{mn}^{(0)} (λg : ρ . g ⊤ i) h : ⊤
\overline{(μ-F Abs)}
Γ, α ≤ τ ⊢_{mn}^{(0)} (λh : α . ((λg : ρ . g ⊤ i) h)) : α → ⊤

The typing proof for the (β^{2})-redex (33) finishes by:

(*See Subproof 3*)

Γ, α ≤ τ ⊢_{mn}^{(0)} (λh : α . ((λg : ρ . g ⊤ i) h)) : α → ⊤

\overline{(μ-T Abs)}

Γ ⊢_{mn}^{(0)} Λα ≤ τ . λh : α . ((λg : ρ . g ⊤ i) h) : (∀α ≤ τ . (α → ⊤)) Γ ⊢^{(0)} τ ≤ τ

\overline{(μ-T App)}

Γ ⊢_{mn}^{(0)} (Λα ≤ τ . λh : α . ((λg : ρ . g ⊤ i) h)) {τ} : τ → ⊤

The explanation to the above “paradox” is therefore simple: the topmost judgment

Γ ⊢_{mn}^{(0)} Λα ≤ τ . λh : α . ((λg : ρ . g ⊤ i) h) : (∀α ≤ τ . (α → ⊤)) in this last proof is not [τ/α]-safe, because the subtyping judgment

Γ, α ≤ τ, h : α ⊢^{(0)} α ≤ ρ, occurring in its proof (see the right premise in Subproof 2) is not [τ/α]-stable. In fact, substituting [τ/α] into this judgment yields:

Γ, h : τ ⊢^{(0)} τ ≤ ρ

and this last subtyping judgment, equivalent to (31), is false by the choice of types τ and ρ. Thus, the failure of the well-typedness preservation for the chain (32) is explained by the violation of the safety precondition of Lemma 14.3.

References

[BL90] K. B. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87:196–240, 1990.

[BTCCS91] V. Breazu-Tannen, T. Coquand, Gunter C., and A. Scedrov. Inheritance as implicit coercion. Mathematical Structures in Computer Science, 93:172–221, 1991.

[CG92] P.-L. Curien and G. Ghelli. Coherence of subsumption, minimum typing, and type checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[CMMS94] L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation, 1994. To appear.

[CP94] G. Castagna and B. C. Pierce. Decidable bounded quantification. In 21st ACM Symp. on Principles of Programming Languages (POPL’94), pages 151–162, 1994.

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

[Pie92] B. C. Pierce. Bounded quantification is undecidable. In 19th ACM Symp. on Principles of Programming Languages (POPL’92), pages 305–315, 1992.

[Rab69] M. Rabin. Decidability of second order theories and automata on infinite trees. Transactions of the American Mathematical Society, 141:1–35, 1969.

[TMR53] A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable theories. Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Company, 1953. Third printing, 1971.

[Vor94a] S. Vorobyov. F_{≤}: Bounded quantification is NOT essentially undecidable. Technical Report CRIN–94–R–018, Centre de Recherche en Informatique de Nancy, January 1994.

[Vor94b] S. Vorobyov. Hierarchies of decidable extensions of bounded quantification. Research Report INRIA–RR–2354, Centre de Recherche en Informatique de Nancy, September 1994.

[Vor94c] S. Vorobyov. Extensions of F_{≤} with Decidable Typing. Technical Report CRIN–94–R–127, Centre de Recherche en Informatique de Nancy, September 1994.

[Vor95] S. Vorobyov. Structural decidable extensions of bounded quantification. In 22nd ACM Symp. on Principles of Programming Languages (POPL’95), 1995. Also: Technical Report MPI–I– 94–257, Max-Planck-Institut für Informatik, Saarbrücken.

Note. All papers of the author are available through http://www.mpi-sb.mpg.de/guide/staff/sv/sv.html

[figure: I N F O R M A T I K]

Below you find a list of the most recent technical reports of the research group Logic of Programming at the Max-Planck-Institut für Informatik. They are available by anonymous ftp from our ftp server ftp.mpi-sb.mpg.de under the directory pub/papers/reports. Most of the reports are also accessible via WWW using the URL http://www.mpi-sb.mpg.de. If you have any questions concerning ftp or WWW access, please contact reports@mpi-sb.mpg.de. Paper copies (which are not necessarily free of charge) can be ordered either by regular mail or by e-mail at the address below.

Max-Planck-Institut für Informatik Library attn. Regina Kraemer Im Stadtwald D-66123 Saarbrücken GERMANY

e-mail: kraemer@mpi-sb.mpg.de

MPI-I-95-2-005 F. Baader, H.-J. Ohlbach A Multi–Dimensional Terminological Knowledge Representation Language

MPI-I-95-2-002 H. J. Ohlbach, R. A. Schmidt Functional Translation and Second–Order Frame Properties

MPI-I-95-2-001 S. Vorobyov Proof normalization and subject reduction in extensions of Fsub

MPI-I-94-261 P. Barth, A. Bockmayr Finite Domain and Cutting Plane Techniques in CLP(PB)

MPI-I-94-257 S. Vorobyov Structural Decidable Extensions of Bounded Quantification

MPI-I-94-254  Report and abstract not published

MPI-I-94-252 P. Madden A Survey of Program Transformation With Special Reference to Unfold/Fold Style Program Development

MPI-I-94-251  P. Graf  Substitution Tree Indexing

MPI-I-94-246 M. Hanus On Extra Variables in (Equational) Logic Programming

MPI-I-94-241 J. Hopf Genetic Algorithms within the Framework of Evolutionary Computation: Proceedings of the KI-94 Workshop

MPI-I-94-240 P. Madden Recursive Program Optimization Through Inductive Synthesis Proof Transformation

MPI-I-94-239 P. Madden, I. Green A General Technique for Automatically Optimizing Programs Through the Use of Proof Plans

MPI-I-94-238 P. Madden Formal Methods for Automated Program Improvement

MPI-I-94-235  D. A. Plaisted  Ordered Semantic Hyper-Linking
MPI-I-94-234  S. Matthews, A. K. Simpson  Reflection using the derivability conditions

MPI-I-94-233 D. A. Plaisted The Search Efficiency of Theorem Proving Strategies: An Analytical Comparison

MPI-I-94-232  D. A. Plaisted  An Abstract Program Generation Logic

MPI-I-94-230 H. J. Ohlbach Temporal Logic: Proceedings of the ICTL Workshop

MPI-I-94-229  Y. Dimopoulos  Classical Methods in Nonmonotonic Reasoning