MAX-PLANCK-INSTITUT FÜR

INFORMATIK

Structural Decidable Extensions of Bounded Quantification

Sergei Vorobyov

MPI–I–94–257 October 1994

[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

To appear in the Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’95), January 23-25, 1995, San Francisco, U.S.A. Preliminary versions appeared as Technical Report CRIN–94–R-121, July 1994 (Centre de Recherche en Informatique de Nancy, France) and Research Report INRIA–94–RR–2309, September 1994 Institut National de Recherche en Informatique et en Automatique, France.

Acknowledgements

I am greatly indebted to Luca Cardelli, Benjamin Pierce, Martín Abadi, Roberto Amadio, Philippe de Groote, Didier Galmiche, Jean-Luc Rémy, Hubert Comon, Michel Parigot for invaluable remarks, ideas, and discussions. I am grateful to my anonymous referee for his substantial help. To produce proof trees I used Paul Taylor’s LaTEXmacro package. This work was mainly done when I was at CRIN (Centre National de Recherche en Informatique de Nancy, France), which provided me the excellent research opportunities.

Abstract

We show how the subtype relation of the well-known system F_{≤}, the secondorder polymorphic λ-calculus with bounded universal type quantification and subtyping, due to Cardelli, Wegner, Bruce, Longo, Curien, Ghelli, proved undecidable by Pierce (POPL’92), can be interpreted in the (weak) monadic secondorder theory of one (Büchi), two (Rabin), several, or infinitely many successor functions. These (W)SnS-interpretations show that the undecidable system Fsub possesses consistent decidable extensions, i.e., Fsub is not essentially undecidable (Tarski, 1949).

We demonstrate an infinite class of structural decidable extensions of F_{≤}, which combine traditional subtype inference rules with the above (W)SnSinterpretations. All these extensions, which we call systems F_{≤}^{SnS}, are still more powerful than F_{≤}, but less coarse than the direct (W)SnS-interpretations.

The main distinctive features of the systems F_{≤}^{SnS} are: 1) decidability,

2) closure w.r.t. transitivity; 3) structuredness, e.g., they never subtype a functional type to a universal one or vice versa, 4) they all contain the powerful rule for subtyping boundedly quantified types.

Structural Decidable Extensions of Bounded Quantification

Sergei G. Vorobyov ^{∗}

Max-Planck-Institut für Informatik

Im Stadtwald, D-66123, Saarbrücken, Germany

(e-mail: sv@mpi-sb.mpg.de)

Abstract

We show how the subtype relation of the well-known system F_{≤}, the second-order polymorphic λ-calculus with bounded universal type quantification and subtyping, due to Cardelli, Wegner, Bruce, Longo, Curien, Ghelli [6, 2, 8], proved undecidable by Pierce [12], can be interpreted in the (weak) monadic second-order theory of one (Büchi), two (Rabin), several, or infinitely many successor functions [13, 14]. These (W)SnS-interpretations show that the undecidable system F_{≤} possesses consistent decidable extensions, i.e., F_{≤} is not essentially undecidable (Tarski et. al., 1949, [17]).

We demonstrate an infinite class of “structural” decidable extensions of F_{≤}, which combine traditional subtype inference rules with the above (W)SnS-interpretations. All these extensions, which we call systems F_{≤}^{SnS}, are still more powerful than F_{≤}, but less coarse than the direct (W)SnSinterpretations:

F_{≤} ⊂ F_{≤}^{SnS} ⊂ (W)SnS-interpretations

The main distinctive features of the systems F_{≤}^{SnS} are:

1) decidability, 2) closure w.r.t. transitivity; 3) structuredness, e.g., they never subtype a functional type to a universal one or vice versa, 4) they all contain the powerful rule for subtyping boundedly quantified types:

\frac{Γ ⊢ τ_{1} ≤ σ_{1} Γ , α ≤ τ_{1} ⊢ σ_{2} ≤ τ_{2}}{Γ ⊢ (∀α ≤ σ_{1} . σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2})} (All)

Key words: second-order polymorphic typed λ-calculus, subtyping, system F_{≤}, bounded universal type quantification, parametric and inheritance polymorphisms, (un-)deci-dability, essential undecidability, (weak) monadic secondorder theory of several successor functions (W)SnS.

1 Introduction

The advantages and usefulness of strict typing disciplines in programming with static typing and rigid compile-time type control have been widely accepted, studied, and advocated in Software Engineering [10, 6, 4, 11] since creation of Simula-67, Algol-68, Pascal, Clu, Alphard, Modula, ML, Ada, etc. Typeful programming should be based on powerful and, preferably, decidable type systems.

The system F_{≤} is the polymorphic second-order typed λcalculus with subtyping, combining the universal (or parametric) polymorphism of Girard’s system F with Cardelli’s calculus of subtyping (inheritance polymorphism [3]). Introduced in [6], later improved, simplified, and investigated by many researchers [2, 1, 8, 12, 7, 5], the system F_{≤} serves a core calculus of type systems with subtyping and a model to represent polymorphic and object-oriented features in programming languages.

F_{≤} is an extension of F with subtyping. In addition to the usual functional and universal type formation of F, the system F_{≤} allows one to form boundedly quantified types: ∀α ≤ bound . body. Such type is a function on types transforming any subtype σ of a bound into a type body[σ/α]. As F_{≤} also contains the largest type ⊤, the unbounded type quantification of F is included as a particular case: ∀α ≤ ⊤ . σ.

The system F_{≤} consists of two components. The first one axiomatizes the subtyping relation on types Γ ⊢ σ ≤ τ. The second generates the typing relation Γ ⊢ t : σ. Both components interact by means of the rules as (Subsumption), allowing one to derive the judgment Γ ⊢ t : τ from Γ ⊢ t : σ and Γ ⊢ σ ≤ τ.

In [12] Pierce proved that already the subtyping component of F_{≤} is undecidable, and hence the typing relation in F_{≤} is undecidable too. Using Ghelli’s example of divergence of F_{≤}-subtyping algorithm (mainly due to the subtle interaction between the quantifier rule (All) above and transitivity), he succeeded to encode instances of the termination problem into F_{≤}-subtyping judgments.

Given an undecidable theory T one usually tries to weaken it to get a decidable subtheory T_{dec} ⊆ T. Accordingly, attempts were made to restrict F_{≤} to get decidable subsystems. In [7] the general quantifier rule (All) above was replaced by its weaker version:

Γ ⊢ τ_{1} ≤ σ_{1} Γ , α ≤ ⊤ ⊢ σ_{2} ≤ τ_{2}
\overline{(All-T op)}
Γ ⊢ (∀α ≤ σ_{1} . σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2})

Subtyping in the resulting subsystem F_{≤}^{⊤} ⊂ F_{≤} is decidable. In [9] a decidable subsystem of F_{≤} is obtained by restricting bounds in bounded quantification to be ⊤-free (with some relaxations to allow unbounded quantification). An extensive discussion of different other weakenings of the powerful rule (All) is contained in [7].

∗This work was done while the author was at the Centre de Recherche en Informatique de Nancy, France

For an undecidable theory T there sometimes exists another possibility, to reinforce it (instead of weakening) in order to obtain a consistent decidable extension T_{dec} ⊇ T. This works only if T is not essentially undecidable, i.e., possesses consistent decidable extensions (A. Tarski, 1949, [17]).

Curiously enough, F_{≤} appears to be undecidable, but not essentially [18], with infinitely many nontrivial consistent decidable extensions. This reopens the possibility for obtaining good decidable systems relative to F_{≤} without sacrificing the general quantifier rule (All) or somehow restricting the form of bounds in bounded quantification.

The first infinite class of such extensions was introduced in [18], where it was shown that there exist infinitely many ways to translate F_{≤}-subtyping judgments into formulas of Rabin’s S2S. Each such translation maps the F_{≤}-axioms to valid S2S-formulas, and each F_{≤}-inference rule preserves validity with respect to any S2S-translation. It follows that everything provable in F_{≤} is valid in any S2S-interpretation. Consequently, F_{≤} is not essentially undecidable; any S2Stranslation is a consistent decidable extension of F_{≤}. S2Sinterpretations generalize for recursive types [19].

Precautions, however, should be taken concerning consistency. For theories based on predicate calculus consistent means “do not prove everything”. For theories, which are not based on predicate calculus, like F_{≤}, consistent might mean “do not subtype any pair of types” (weak consistency) or “do not subtype too many types” (strong consistency).

S2S-interpretations appeared to be weakly, but not strongly consistent. They are coarse in the sense that they do not make fine distinction between differently structured types, and subtype too many of them, which is undesirable in strict typing disciplines. In this paper we remedy this drawback by combining our S2S-interpretations with the traditional F_{≤}- like subtype inference rules. These rules guarantee the socalled “strict structural subtyping”, where the subtype relation is defined by co(ntra)variant induction on type structure. This prevents us from subtyping differently structured types, e.g., universal and functional ones.

The main idea of our systems F_{≤}^{SnS} is that they disable the infinite alternations of applications of the rule (All) and the transitivity rule. This alternation is the source of nontermination and undecidability of F_{≤}, [12]. Instead, we prune proof tree branches, which may lead to infinite alternations, and decide the remaining judgments by interpreting them in (W)SnS. Of course, as F_{≤} is undecidable, and F_{≤}^{SnS} are decidable extensions of F_{≤}, sometimes they accept F_{≤}-unprovable judgments. But this is a reasonable price for attaining decidability.

The scenario of the presentation is the following. Section 2 recalls the system F_{≤}. (Un)decidability results concerning F_{≤} are listed in Section 3. Section 4 introduces systems F_{≤}^{SnS}. Section 5 describes the decision procedure. In Section 6 we show infinitely many ways to interpret the subtype relation in any (W)SnS. Section 7 discusses the consistency of F_{≤}^{SnS}. In Section 8 we explain the rule inversion principle, the main tool of our proofs of the inclusion F_{≤} ⊂ F_{≤}^{SnS} and the transitivity of F_{≤}^{SnS}. In Sections 9 and 10 we show that the inversion principle does not hold for SnS-interpretations, but holds for systems F_{≤}^{SnS}. In Sections 11, 12, and 13 we prove the inclusions F_{≤} ⊂ F_{≤}^{SnS} ⊂ (W)SnS-interpretations and the transitivity of all F_{≤}^{SnS}. Section 14 discusses further improvements of F_{≤}^{SnS}. In Section 15 we sketch problems for future research. Appendices A and B contain the reference material on secondorder monadic theories and on Curien-Ghelli’s algorithmic variant of F_{≤}. The proofs are collected in Appendix C.

In this paper we deal only with the subtyping relation. Combinations with typing and related problems, like subject reduction [20], typing proof normalization, the least type property, strong normalization are in the course of study and will be considered elsewhere.

Added in Proof. In [21] we continued the study of decidable extensions of the F_{≤} subtyping relation and developed the general theory of converging hierarchies of structural decidable extensions of the F_{≤}-subtyping. The systems F_{≤}^{SnS} presented in this paper form just the first level of the hierarchies from [21]. In [22] we combined these hierarchies with the standard F_{≤} term typing rules and obtained an infinite family of the extensions of the polymorphic system F_{≤} where both subtyping and typing are decidable.

2 System F_{≤}

For complete and exact reference see, e.g., [8, 12, 5]. We just briefly remind the essential definitions, retaining the notation of [12].

Definition 2.1 (Types) The set of F_{≤}-types is defined by the following abstract grammar:

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

where:

1. 𝕍 is a set of type variables denoted by Greek letters α, β, γ;

2. ⊤ is the largest type majorazing any other type, σ ≤ ⊤;

3. → is the functional type constructor, σ → τ is the type of functions with domain of type σ and codomain of type τ;

4. ∀α ≤ ρ . τ is a polymorphic boundedly quantified type, i.e., a function assigning to each subtype σ of ρ, σ ≤ ρ, the type τ[σ/α] obtained from τ by substituting σ instead of free occurrences of α (with usual non-clashing preconditions on free variables). In ∀α ≤ ρ . τ the bound ρ does not contain α free.

The letters τ, σ, ρ from the end of the Greek alphabet denote arbitrary (variable or compound) F_{≤}-types; ∀β . τ abbreviates ∀β ≤ ⊤.τ; F V (σ) denotes the set of free variables in σ.

Definition 2.2 (Contexts) An F_{≤}-context is an ordered sequence α_{1} ≤ σ_{1}, …, α_{n} ≤ σ_{n} of ≤-relations between type variables and F_{≤}-types such that:

1. all α_{i} are different type variables, and

2. for each i, F V (σ_{i}) ⊆ {α_{1}, …, α_{i−1}}.

Contexts are denoted by capital Greek Γ. Dom(Γ) is the set of type variables appearing to the left of ≤ in Γ. We write Γ(α) = σ if Γ contains α ≤ σ and call σ a bound of α in Γ. We define Γ^{∗}(α) as Γ(α) if the latter is not a variable, and as Γ^{∗}(Γ(α)) otherwise. □

Definition 2.3 (Subtyping Judgments) An F_{≤}-subtyping judgment is a figure of the form:

Γ ⊢ σ ≤ τ,

where F V (σ) ∪ F V (τ) ⊆ Dom(Γ). □

The intuitive semantics of a judgment Γ ⊢ σ ≤ τ is: σ is a subtype of τ provided that all α_{i} mentioned in Γ are subtypes of their respective bounds σ_{i}.

Definition 2.4 (Subtyping Rules) The F_{≤}-subtyping relation is generated by the system of 3 axioms and 3 inference rules, shown in Figure 1.

Γ ⊢ τ ≤ τ  (Refl)

Γ ⊢ τ ≤ ⊤  (T op)

Γ ⊢ α ≤ Γ(α)  (T V ar)

\begin{matrix}Γ ⊢ τ_{1} ≤ τ_{2} & Γ ⊢ τ_{2} ≤ τ_{3} \\ Γ ⊢ τ_{1} ≤ τ_{3} \end{matrix}  (T rans)

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

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

Figure 1: F_{≤} subtyping axioms and inference rules

Let ⊢_{F_{≤}} denote the least three-place relation Γ ⊢ σ ≤ τ containing all particular cases of the F_{≤}-axioms and closed with respect to the F_{≤}-inference rules. Sometimes, by abusing notation, we denote by F_{≤} the set of subtyping judgments provable in F_{≤}. □

Definition 2.5 (Variants of F_{≤}) 1) Original F un [6] replaces the (All) rule by the weaker rule (All-F un) (Figure 2).

2) System F_{≤}^{⊤} [7] replaces the rule (All) by its particular case (All-T op) (Figure 2).

3) System F_{≤}^{local} [7] replaces the rule (All) by its modification (All-local) (Figure 2).

By ⊢_{F un}, ⊢_{F_{≤}^{⊤}} and ⊢_{F_{≤}}_{local} we denote the corresponding subtyping relations. □

\begin{matrix}Γ , α ≤ ρ ⊢ σ_{2} ≤ τ_{2} \\ Γ ⊢ (∀α ≤ ρ . σ_{2}) ≤ (∀α ≤ ρ . τ_{2}) \end{matrix}  (All-F un)

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

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

Figure 2: Variants of the (All) rule

3 (Un)Decidability

The interesting facts about F_{≤} are:

Theorem 3.1 (Undecidability of F_{≤}, [12]) The relation ⊢_{F_{≤}} is undecidable. □

The weakenings of F_{≤} are however decidable:

Theorem 3.2 (Decidability of F un and F_{≤}^{⊤} [7]) Both relations ⊢_{F un} and ⊢_{F_{≤}^{⊤}} are decidable. □

Nothing is known about decidability of F_{≤}^{local} [7].

In [18] we demonstrated that the decidability of F_{≤} could be reached also by reinforcement, and not only by weakening, as opposed to systems F_{≤}^{⊤} and F un.

Definition 3.3 (Essential Undecidability, [17]) A consistent theory T is essentially undecidable iff it has no consistent decidable extensions T′ ⊇ T. □

Definition 3.4 (Consistency) An extension of F_{≤} is consistent iff it is closed with respect to the F_{≤} inference rules and does not subtype any two types. □

Remarks. 1) Further we replace “any two types” by “any two differently structured types” getting the stronger consistency. 2) As we are interested only in the extensions of F_{≤}, the closure with respect to the F_{≤}-inference rules seems natural and meaningful. It would not be the case for F_{≤}^{⊤} and F un. □

Theorem 3.5 (F_{≤} Is Not Essentially Undecidable, [18]) There exist infinitely many different consistent decidable extensions of ⊢_{F_{≤}} . □

This result was obtained by interpreting the F_{≤}-subtyping relation in S2S, the monadic second-order logic of two successors due to M. Rabin [13, 14]. The corresponding infinite class of extensions of F_{≤} (which we call the S2Sinterpretations) and their properties are studied in [18].

The main objection (by L. Cardelli and others) against these extensions was that they were too coarse and non-structural. S2S-interpretations subtype too many types, sometimes differently structured ones (i.e., universal and functional ones).

In this paper we introduce a new infinite class of decidable extensions of F_{≤} refining the S2S-interpretations . We call these extensions systems F_{≤}^{SnS}. We also (re)introduce the S2S-interpretations in a slightly more general setting and call them SnS-interpretations (with S2S being a particular case of SnS for n = 2). We prove that all systems F_{≤}^{SnS} are more powerful than F_{≤}, but being structural (they do not subtype differently structured types any more), they are less coarse than SnS-interpretations:

F_{≤} ⊂ F_{≤}^{SnS} ⊂ SnS-interpretations

Again note that the decidable system F_{≤}^{⊤} introduced in [7] is weaker than F_{≤}: F_{≤}^{⊤} ⊂ F_{≤}.

4 System F_{≤}^{SnS}

Definition 4.1 The system F_{≤}^{SnS} is defined by the collection of subtyping axioms and inference rules shown in Figure 3, supposed to be applied bottom-up in the order of their presentation.

∗ ∗ ∗ See F igure 3 ∗ ∗∗

The DECIDE component in the rule (V ar-All-Decide) and the whole F_{≤}^{SnS}-decision procedure are described in the following Sections. □

Roughly speaking, the system F_{≤}^{SnS} is F_{≤} without the general transitivity rule (T rans) replaced by a built-in decision procedure DECIDE.

Remarks and Explanations

1. Our intention is to define the decision and not semidecision procedure for subtyping judgments. That is why we are going to apply rules bottom-up and introduce two constants T RUE and FALSE to treat both the accepting and rejecting cases.

2. Rules (Refl), (T op), and (T V ar) correspond exactly to their F_{≤} counterparts. We formulate them as rules with the premises T RUE just to be able to treat symmetrically the negative case FALSE in other rules of F_{≤}^{SnS}.

3. Rules (Arrow) and (All) are the same as in F_{≤}.

4. Motivation for the rules (T op-L) and (T V ar-R-2) is: the conclusions of these rules are NOT provable in F_{≤} (Proposition 4.2).

5. Motivation for the rules (∀ ≰ →) and (→ ≰ ∀) is the same: the conclusions of these rules are underivable in F_{≤}.

6. The (V ar-Arrow) rule is just a half (with only arrowtypes on the right of ≤) of Curien-Ghelli’s algorithmic transitivity rule (AlgT rans), see [8] and Appendix B.

7. The crucial difference with F_{≤} is the absence of the general rule (T rans) or of its algorithmic equivalent (AlgT rans) for universal types (see the rule (V ar-All) below). Transitivity in this case is dealt separately, by means of a DECIDE procedure. Note that we do not weaken the general F_{≤} quantifier rule (All), which remains the same as in F_{≤}^{SnS}.

8. The built-in procedure DECIDE appearing in the premise of the rule (V ar-All-Decide) is a parameter of the system. Below we define infinitely many different such procedures. Note, in particular, that if we define the DECIDE procedure recursively, as F_{≤}^{SnS} plus the second half of Curien-Ghelli’s transitivity rule:

\begin{matrix}Γ ⊢ Γ(α) ≤ (∀β ≤ σ . τ) \\ Γ ⊢ α ≤ (∀β ≤ σ . τ) \end{matrix}  (V ar-All)

then we will get exactly F_{≤}! □

Proposition 4.2 Subtyping judgments of the forms:

1. Γ ⊢ ⊤ ≤ τ (τ ≠ ⊤),

2. Γ ⊢ σ ≤ α (σ non-variable, α variable),

where Γ is any context, are not provable in F_{≤}. □

Proof . See Appendix C.1. □

5 Decision Procedure

The rules of the system F_{≤}^{SnS} read bottom-up can be seen as a decision procedure (with a built-in DECIDE oracle). Given a subtyping judgment, the rules of F_{≤}^{SnS} apply deterministically in ordered manner (e.g., (V ar-All-Decide) does not apply before (V ar-All-2)). The rule application process always terminates, provided that the built-in DECIDE procedure is finitely terminating, and this is the fundamental difference with F_{≤}, see [12].

Proposition 5.1 (Finite Termination of F_{≤}^{SnS}) For every subtyping judgment Γ ⊢ σ ≤ τ any F_{≤}^{SnS}-proof tree is finite. □

Proof . The complexity of judgments decreases as one moves bottom-up. □

So the termination of the whole decision procedure depends on termination of its DECIDE component.

Irreducible leaves of F_{≤}^{SnS}-proof trees are either:

1. T RUE or

2. FALSE or

3. of the form DECIDE( J ), where J is a subtyping judgment in the F_{≤}^{SnS}-normal form, i.e.:

J ≡_{df} α_{1} ≤ σ_{1} … α_{n} ≤ σ_{n} ⊢ β ≤ τ,  (3)

where α_{1}, …, α_{n}, β are type variables, σ_{1}, …, σ_{n} are arbitrary types, and τ is a universal type.

\begin{matrix}T RUE \\ Γ ⊢ σ ≤ σ \end{matrix}  (Refl)

\begin{matrix}T RUE \\ Γ ⊢ σ ≤ ⊤ \end{matrix}  (T op)

FALSE ; \overline{(for τ ≠ ⊤)} ; Γ ⊢ ⊤ ≤ τ  (T op-L)

Γ ⊢ Γ(β) ≤ α ; \overline{(for different variables α, β)} ; Γ ⊢ β ≤ α  (T V ar-R-1)

FALSE ; \overline{(σ non-variable, α variable)} ; Γ ⊢ σ ≤ α  (T V ar-R-2)

\begin{matrix}FALSE \\ Γ ⊢ (∀α ≤ σ_{1} . σ_{2}) ≤ (τ_{1} → τ_{2}) \end{matrix}  (∀ ≰ →)

\begin{matrix}FALSE \\ Γ ⊢ (σ_{1} → σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2}) \end{matrix}  (→ ≰ ∀)

\begin{matrix}Γ ⊢ Γ(α) ≤ σ → τ \\ Γ ⊢ α ≤ σ → τ \end{matrix}  (V ar-Arrow)

\begin{matrix}T RUE \\ Γ ⊢ α ≤ Γ(α) \end{matrix}  (T V ar)

Γ ⊢ Γ(α) ≤ (∀β ≤ σ . τ) ; \overline{(if Γ(α) is a variable)} ; Γ ⊢ α ≤ (∀β ≤ σ . τ)  (V ar-All-1)

Γ ⊢ FALSE ; \overline{(if Γ(α) is ⊤ or an → -type)} ; Γ ⊢ α ≤ (∀β ≤ σ . τ)  (V ar-All-2)

\begin{matrix}DECIDE( Γ ⊢ α ≤ (∀β ≤ σ . τ) ) \\ Γ ⊢ α ≤ (∀β ≤ σ . τ) \end{matrix}  (V ar-All-Decide)

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

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

Figure 3: System F_{≤}^{SnS} Obviously:

• if all leaves of a F_{≤}^{SnS}-proof tree are T RUE, we declare the input judgment valid;

• if one of the leaves of F_{≤}^{SnS}-proof tree is FALSE, we declare the input judgment invalid;

• otherwise, before announcing our verdict we analyze F_{≤}^{SnS}-normal forms (3) using the built-in DECIDE procedure.

To decide normal forms (3) we use a method [18] of interpretations in monadic second-order theories of successor functions [14]:

• first, we compile F_{≤}^{SnS}-normal forms (3) in a monadic second-order theory,

• second, we decide them using a decision procedure for this theory.

Therefore, instead of remaining in the undecidable F_{≤} we forget it and work in the decidable F_{≤}^{SnS}, which replaces the transitivity rule (T rans) by the transitivity implicitly present in a monadic second-order theory. As we show below, the proper choices of the DECIDE component lead to decidable extensions of F_{≤} (Theorem 11.1), closed with respect to transitivity (Theorem 12.1).

6 Interpreting F_{≤}^{SnS}-Normal Forms in SnS

In [18] we introduced an infinite class of direct interpretations of F_{≤} into S2S, the monadic second-order arithmetic of two successor functions [13, 14]. These direct S2S-inter-pretations do not use any inference rules (as opposed to F_{≤} or F_{≤}^{SnS}), immediately translating F_{≤}-judgments into S2Sformulas. Like this we established that F_{≤} possesses infinitely many different consistent decidable extensions, i.e., is not essentially undecidable.

The drawback of the direct S2S-interpretations of F_{≤} is that they subtype too many types (see [18] and below), in particular, differently structured types. The systems F_{≤}^{SnS} are more subtle. By their very definition they do not subtype differently structured types. They cannot prove a subtyping between, say, an →-type and a ∀-type. The systems F_{≤}^{SnS} apply the method of interpretations only to normal forms, i.e., to judgments of the form (3) inside the DECIDE procedure.

There is only a minor difference in defining the S2S-inter-pretations only for normal forms (3) and for general F_{≤}- subtyping judgments, so we give a complete definition of S2S-interpretations of F_{≤}. Also, S2S-interpretations generalize straightforwardly to SnS-interpretations for arbitrary n ∈ ℕ or even SωS.

Choose and fix any monadic second-order theory of successor function(s), say, Büchi arithmetic S1S, Rabin’s arithmetic S2S, …, SnS, SωS, or their weak counterparts, with second-order quantifications restricted to finite sets (see Appendix A).

The intuition behind interpretations of F_{≤} into SnS is extremely simple. We interpet the F_{≤} types as propositions of SnS. Each F_{≤}-type σ is assigned a SnS-formula S(x) with just one free object variable x, and each subtyping relation σ ≤ τ is translated into ∀x(S(x) ⊃ T (x)), where S(x) and T (x) are SnS-formulas assigned to types σ and τ.

Our translation satisfies the following properties:

1. all axioms of F_{≤} are transformed into valid formulas of SnS;

2. all F_{≤}-inference rules preserve validity with respect to any SnS, i.e., whenever both premises of a rule are translated into valid SnS-formulas, then the conclusion of the rule is also translated into such formula.

3. consequently, by 1 and 2, any F_{≤}-subtyping judgment is interpreted as a true formula of SnS, and, henceforth, F_{≤} is not essentially undecidable, i.e., possesses consistent decidable extensions; any SnS-translation of F_{≤} satisfying the above properties is such an extension.

It remains to show that the needed SnS-translations of F_{≤} with the above properties exist. We show it in the rest of this Section. The idea is quite simple: interpret type variables α, β, … as corresponding SnS-atomic formulas A(x), B(x), …, choosing a new predicate variable for each new type variable. Then knowing that S(x) and T (x) interpret σ and τ respectively, interpret:

• σ → τ as S(x) ⊃ T (x), or, more generally, as

S(x) ⊃ T (f(x)),

• ∀α ≤ σ . τ as ∀^{2}A {∀^{1}x[A(x) ⊃ S(x)] ⊃ T (x)}, or, more generally, as

∀^{2}A {∀^{1}x[A(x) ⊃ S(x)] ⊃ T (g(x))} ,

where f, g are arbitrary strings composed of SnSsuccessors.

Introduction of parameters f and g allows us to define infinitely many different interpretations of F_{≤} in SnS, see [18]. Surprising, but it works! We now proceed to formal definitions.

Definition 6.1 (SnS[F_{≤}](f, g)-interpretations ) Let f and g be two arbitrary strings composed of successor function symbols of SnS. Both may be equal to the empty string ε.

For an arbitrary type ρ of F_{≤}, the Types-As-Propositions-Interpretation of ρ in SnS with parameters f and g (the SnS[F_{≤}](f, g)-interpretation for short) is defined as an SnSformula [[ ρ ]]fg(x) with unique distinguished free object variable x by induction on the structure of ρ:

1. [[ α ]]fg(x)  ≡_{df}  A(x) (a new predicate

variable A for each type variable α);

2. [[ ⊤ ]]fg(x)  ≡_{df} x = x;
3. [[ σ → τ ]]fg(x)  ≡_{df} [[ σ ]]fg(x) ⊃ [[ τ ]]fg(f(x));
4. [[ ∀ α ≤ σ . τ ]]fg(x) ≡_{df}

∀^{2}A {∀^{1}x (A(x) ⊃ [[ σ ]]fg(x)) ⊃ [[ τ ]]fg(g(x))}.

The SnS[F_{≤}](f, g)-interpretation is extended to all subtyping judgments by:

5. [[ σ ≤ τ ]]fg ≡_{df} ∀^{1}x ([[ σ ]]fg(x) ⊃ [[ τ ]]fg(x));
6. [[ α_{1} ≤ σ_{1} … α_{n} ≤ σ_{n} ⊢ σ ≤ τ ]]fg ≡_{df}

[[ α_{1} ≤ σ_{1} ]]fg … [[ α_{n} ≤ σ_{n} ]]fg ⊧SnS [[ σ ≤ τ ]]fg. □

Definition 6.2 (Theory) Define the SnS[F_{≤}](f, g)-theory as:

SnS[F_{≤}](f, g) ≡_{df} { Γ ⊢ σ ≤ τ | [[ Γ ⊢ σ ≤ τ ]]fg}

Further we will freely say that a typing judgment is true or valid in (or with respect to ) a SnS[F_{≤}](f, g)-interpretation iff it belongs to the set SnS[F_{≤}](f, g). □

Remarks. In SnS[F_{≤}](f, g)-interpretation we use just onevariable restricted fragment of SnS. If f = g = ε then this fragment is also function-free (and can be seen as the propositional second-order logic). x is the only free object variable of any SnS[F_{≤}](f, g)-interpretation of any type. Subtyping judgments are interpreted as statements about SnSsemantical consequence relation ⊧SnS containing no free object variables at all. Any SnS[F_{≤}](f, g) is decidable. □

The SnS-interpretations enjoy the following important properties:

Lemma 6.3 (Embedding) 1) All axioms of F_{≤} are valid with respect to any SnS[F_{≤}](f, g).

2) All inference rules of F_{≤} preserve validity with respect to any SnS[F_{≤}](f, g), i.e., if both premises of a rule are valid in SnS[F_{≤}](f, g), then so is the conclusion of the rule. □

Proof . Straightforwardly rephrasing the proof from [18].

□

As a direct consequence we have, [18]:

Theorem 6.4 (On Decidable Extensions of F_{≤}) Any SnS[F_{≤}](f, g) is a consistent decidable theory containing all F_{≤}-derivable subtyping judgments. Henceforth, F_{≤} is not essentially undecidable possessing consistent decidable extensions. □

Definition 6.5 (F_{≤}^{SnS}(f, g)) Define a system F_{≤}^{SnS}(f, g) as a combination of the inference rules from Figure 3 and a DECIDE procedure for SnS[F_{≤}](f, g). □

Below, in Theorems 11.1 and 12.1 we show that all systems F_{≤}^{SnS}(f, g) also extend F_{≤} but are less coarse than SnSinterpretations, i.e.,

F_{≤} ⊂ F_{≤}^{SnS}(f, g) ⊂ SnS[F_{≤}](f, g)  (4)

7 Consistency and Well-Structuredness of F_{≤}^{SnS}

Proposition 7.1 All systems F_{≤}^{SnS} are consistent: they do not prove, e.g., ⊢ ⊤ ≤ (⊤ → ⊤). Neither do they subtype any pair of differently structured types. □

Proof . Immediate by definition. □

8 Inversion Principle

The main tool of the proofs of inclusions (4) (Theorems 11.1 and 12.1) and of the transitivity of F_{≤}^{SnS}(f, g) (Theorem 13.1) is the well-known inversion principle. The rule invertibility is the fundamental principle of the cut-free Gentzen-type derivation systems, see, e.g., [15].

The inversion principle is the key property needed to prove the minimal typing property for F_{≤}. In fact, this is almost all what is needed to reconstruct F_{≤}-inferences into normal forms, [8].

The inversion principle can be formulated as follows: for an inference rule of a system S

Γ ⊢ Φ  Γ ⊢ Ψ
\overline{(Rule)}
Γ ⊢ θ

if a sequent Γ ⊢ Θ from the conclusion is derivable in S then the premises are also derivable in S.

The inversion principle is important for goal-oriented proofsearch procedures, which are guaranteed to be complete just stupidly applying inference rules bottom-up. Proofs in systems satisfying the inversion principle are direct, constructed from subproofs of subformulas of goal formulas, do not contain insights and roundabout ways.

The inversion principle is not evident, or even fails for systems with the CUT rule:

Γ ⊢ A ⊃ C  Γ ⊢ C ⊃ B
\overline{(Cut)}
Γ ⊢ A ⊃ B

In the presence of (Cut), one cannot always be sure that a provable formula Θ of the form A ⊃ B is obtained by some (Rule) or by the (Cut). But applying (Cut) requires ingenuity to find intermediate formulas C, unattainable for mechanic theorem provers.

Note that the usual transitivity rule of F_{≤}

Γ ⊢ τ_{1} ≤ τ_{2}  Γ ⊢ τ_{2} ≤ τ_{3}

\overline{(T rans)}

Γ ⊢ τ_{1} ≤ τ_{3}

has the definite (Cut) form.

Proposition 8.1 (Inversion for F_{≤}, [8]) In F_{≤} the rules (Arrow) and (All) are invertible. □

This may be seen as a good structural property.

9 Failure of the Inversion Principle for SnS[F_{≤}](f, g)

The inversion principle fails for SnS-interpretations. In fact, we can have

[[ Γ ⊢ (σ → τ) ≤ (σ′ → τ′) ]]fg

WITHOUT having

[[ Γ ⊢ σ′ ≤ σ ]]fg and [[ Γ ⊢ τ ≤ τ′ ]]fg

Take, for example, the judgment

α ≤ ⊤ ⊢ (α → ⊤) ≤ (⊤ → ⊤)

with the valid SnS-translation, but the SnS-translation of

α ≤ ⊤ ⊢ ⊤ ≤ α

is false: ∀^{1}x(Ax ⊃ x = x) |̸= ∀^{1}x(x = x ⊃ Ax).

10 Inversion Principle for F_{≤}^{SnS}

Inversion principle trivially holds for F_{≤}^{SnS}:

Lemma 10.1 (Inversion Principle) In any F_{≤}^{SnS}(f, g):

• if Γ ⊢ σ_{1} → σ_{2} ≤ τ_{1} → τ_{2} is provable, then Γ ⊢ τ_{1} ≤ σ_{1} and Γ ⊢ σ_{2} ≤ τ_{2} are also provable;

• if Γ ⊢ (∀α ≤ σ_{1} . σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2}) is provable, then Γ ⊢ τ_{1} ≤ σ_{1} and Γ , α ≤ τ_{1} ⊢ σ_{2} ≤ τ_{2} are also provable. □

Proof . Immediate by definition. In F_{≤}^{SnS} there are no other ways to subtype two →- or ∀-types except applying (Arrow) or (All) (or by the (Refl), in which case the conclusion is straightforward). □

The proofs in F_{≤}^{SnS} are direct, one needs not subtype anything which do not belong to a goal subtyping judgment, proofs are conducted without roundabout ways and insights, completely deterministically.

11 F_{≤}^{SnS} is More Powerful than F_{≤}

Now we prove two strict inclusions:

F_{≤} ⊂ F_{≤}^{SnS}(f, g) ⊂ SnS[F_{≤}](f, g)

So, the systems F_{≤}^{SnS} occupy an intermediate position between F_{≤} and SnS-interpretations: they are more strong than F_{≤} and more subtle than SnS-interpretations. Note that the decidable system F_{≤}^{⊤} lies to the left of F_{≤} in the above diagram.

Remark. F_{≤}^{SnS} is an infinite family of systems. To decide normal forms each system uses a parametric SnS[F_{≤}](f, g)- interpretation . For each f and g we have different parametric F_{≤}^{SnS}(f, g). In fact, for the same f, g we have the above inclusion F_{≤}^{SnS}(f, g) ⊂ SnS[F_{≤}](f, g). In general, F_{≤}^{SnS}(f, g) and SnS[F_{≤}](f′, g′) are unrelated [18].

Theorem 11.1 (F_{≤} ⊂ F_{≤}^{SnS}) Each system F_{≤}^{SnS}(f, g) is strictly more powerful than F_{≤} is: if a subtyping judgment is provable in F_{≤} then it is also provable in F_{≤}^{SnS}(f, g); the converse is not true in general. □

Proof . See Appendix C.2. □

12 F_{≤}^{SnS} Are Less Coarse than SnS-Interpretations

We prove that F_{≤}^{SnS}(f, g) subtypes strictly less types than the corresponding SnS[F_{≤}](f, g)-interpretation:

Theorem 12.1 (F_{≤}^{SnS}(f, g) ⊂ SnS[F_{≤}](f, g).) Each system F_{≤}^{SnS}(f, g) is strictly less powerful than the corresponding interpretation SnS[F_{≤}](f, g): whatever is provable in F_{≤}^{SnS}(f, g) is also true in SnS[F_{≤}](f, g); the converse in general does not hold. In particular, F_{≤}^{SnS} does not subtype differently structured types (e.g., a universally quantified and a functional type). □

Proof . See Appendix C.3. □

13 Transitivity of F_{≤}^{SnS}

Changing F_{≤} for F_{≤}^{SnS} we gain decidability and do not lose transitivity! Transitivity is an indispensable property needed for many purposes, in particular, for proof normalization, see [8, 21, 22].

Theorem 13.1 (Transitivity of F_{≤}^{SnS}) All systems F_{≤}^{SnS}(f, g) are closed with respect to the transitivity rule (T rans):

whenever Γ ⊢ σ ≤ τ and Γ ⊢ τ ≤ ρ are provable in F_{≤}^{SnS}(f, g), then Γ ⊢ σ ≤ ρ is also provable in F_{≤}^{SnS}(f, g).

Proof . See Appendix C.4. □

14 Improvements

The F_{≤}^{SnS}-decision procedure may be obviously refined as follows: instead of pruning the F_{≤}^{Alg}-proof tree^{1} on the first application of (V ar-All-Decide), one may fix k ∈ ℕ and allow k applications of (V ar-All) on each branch of a subtyping proof tree before applying (V ar-All-Decide), which invokes the brute force SnS-decision procedure for normal forms. Denote the resulting system F_{≤}^{SnS}(f, g)(k).

Consider a simple example. The non-modified procedure analyzing the normal form

Γ, α ≤ (∀β(⊤ → ⊤) → ⊤) ⊢ α ≤ (∀β . ⊤ → ⊤)

returns T RUE. But if we allow just one application of (V ar-All), we get Γ... ⊢ (⊤ → ⊤) → ⊤ ≤ ⊤ → ⊤, then Γ ⊢ ⊤ ≤ ⊤ → ⊤, and, finally FALSE, which corresponds exactly to the F_{≤}-proof.

With these modifications we still have for all k ∈ ω

F_{≤} ⊂ F_{≤}^{SnS}(f, g)(k)

It is not difficult to notice that

F_{≤}^{SnS}(f, g)(k + 1) ⊂ F_{≤}^{SnS}(f, g)(k)

and F_{≤}^{SnS}(f, g)(∞) = F_{≤}.

The general theory of the converging sequences { F_{≤}^{SnS}(f, g)(k) }_{k=0}^{∞} is systematically developed in [21].

15 Conclusion

In this paper we concentrated exclusively on the the subtyping relations more powerful than in F_{≤}. When combined with the usual F_{≤}-term typing rules, our subtyping extensions produce systems, which type strictly more terms than F_{≤}. Let Γ ⊢ σ ≤ τ be F_{≤}^{SnS}-provable but F_{≤}-unprovable. Then Γ, x : σ, f : τ → τ ⊢ f x : τ in F_{≤}^{SnS}, but is untypable in F_{≤}.

Therefore, the problems of subject reduction, strong normalization, and minimal typing are nontrivial for our extensions. If the general answers appear to be negative, it might be interesting to investigate restricted classes and/or to modify senses in which we understand the above properties. It would also be interesting to construct models of F_{≤}^{SnS}. The work on these problems has been started [21, 22, 20].

As shows the example in Section 14, the systems F_{≤}^{SnS} (and hence SnS-interpretations) do not separate the sets of F_{≤}- provable and F_{≤}-finitely disprovable subtyping judgments. So, the problem is: whether these two sets are recursively separable. If yes, the separating cover of F_{≤} will be a better substitute for the DECIDE component of the F_{≤}^{SnS}- decision procedure.

In a particular case, when f = g = ε, our SnS-interpretations of F_{≤}-subtyping are just interpretations into the secondorder propositional logic. As it was established by Shamir [16], the class P SP ACE coincides with the class of languages recognizable by the so-called interactive proof systems. These systems are probabilistic algorithms exchanging messages in order to get convinced whether a given string belongs to a language with a given probability. It is challenging to introduce probabilistic algorithms in the domain of type systems.

Acknowledgments. I am greatly indebted to Luca Cardelli, Benjamin Pierce, Martín Abadi, Roberto Amadio, Philippe de Groote, Didier Galmiche, Jean-Luc Rémy, Hubert Comon, Michel Parigot for invaluable remarks, ideas, and discussions. I am grateful to my anonymous referee for his substantial help. To produce proof trees I used Paul Taylor’s LaTEXmacro package. This work was done when I was at CRIN (Centre National de Recherche en Informatique de Nancy, France), which provided me the excellent research opportunities.

References

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

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

[3] Cardelli, L. A semantics of multiple inheritance. Information and Computation 76 (1988), 138–164.

[4] Cardelli, L. Typeful programming. Research Report 45, Digital Equipment Corporation System Research Center, 1989.

[5] Cardelli, L., Martini, S., Mitchell, J., and Scedrov, A. An extension of system F with subtyping. Information and Computation (1994). To appear, preliminary version in LNCS’526, 1991, pp.550–570.

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

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

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

[9] Katiyar, D., and Sankar, S. Completely bounded quantification is decidable. In ACM SIGPLAN Workshop on ML and its Applications (1992).

[10] Leivant, D. Polymorphic type inference. In 10th ACM Symp. on Principles of Programming Languages (1983), pp. 88–98.

[11] Mitchell, J. C. Type theory for programming languages. In Handbook of Theoretical Computer Science (1990), J. van Leeuwen, Ed., vol. B, Elsevier, pp. 365–458.

[12] Pierce, B. C. Bounded quantification is undecidable. In 19th ACM Symp. on Principles of Programming Languages (1992), pp. 305–315.

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

[14] Rabin, M. O. Decidable theories. In Handbook of Mathematical Logic (1977), J. Barwise, Ed., Studies in Logic and the Foundations of Mathematics, North Nolland, pp. 595–630.

1F_{≤}^{Alg} is the Curien-Ghelli algorithmic equivalent formulation of F_{≤}, see [8] and Appendix B

[15] Schwichtenberg, H. Proof theory: some applications of cut-elimination. In Handbook of Mathematical Logic (1977), J. Barwise, Ed., Studies in Logic and the Foundations of Mathematics, North-Holland Publishing Company, pp. 867– 895.

[16] Shamir, A. PSPACE=IP. In Proc. 31st IEEE FOCS (1990), IEEE, pp. 11–15.

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

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

[19] Vorobyov, S. F_{≤} with recursive types: “Types-As-Propositions” Interpretations in M.Rabin’s S2S. Technical Report CRIN–94–R–035, Centre de Recherche en Informatique de Nancy, February 1994. FTP: FsubREC.[dvi,ps].Z .

[20] Vorobyov, S. β-η-⊤-subject reduction and stucklessness for perfectly-structured second-order type systems with subtyping. In preparation, April –September 1994.

[21] Vorobyov, S. Hierarchies of decidable extensions of bounded quantification. Research Report INRIA–RR–2354, Technical Report CRIN–94–R–120, Centre de Recherche en Informatique de Nancy, August –September 1994. FTP: INRIA–RR–2354.ps.Z, FsubHi.[dvi,ps].Z .

[22] Vorobyov, S. Extensions of F_{≤} with Decidable Typing. Technical Report CRIN–94–R–127, Centre de Recherche en Informatique de Nancy, September 1994. FTP: FsubDec-Typing.[dvi,ps].Z .

Note. Papers with mention FTP: filename are available by anony-

mous ftp ftp.loria.fr directory pub/loria/prograis/vorobyov
or via URL ftp://ftp.loria.fr/pub/loria/prograis/vorobyov

(mosaic).

A Monadic Second-Order Arithmetics

We briefly recall basic definitions and facts about decidable (weak) monadic second-order theories of one or several successors.

Fix arbitrary n ∈ ω ∪ {ω}. The alphabet of n-successor monadic second-order arithmetic SnS consists of: 1) infinitely many object variables x, y, z, …, 2) the equality predicate symbol =, 3) infinitely many unary (monadic) predicate variables A, B, X, Y, …,

4) one, several, or countably many successor function symbols {succ_{i}}_{i<n}, 5) all usual boolean connectives, parentheses, 6) universal and existential first- and second-order quantifiers: ∀^{1}, ∃^{1}, ∀^{2}, ∃^{2}.

Terms are constructed as usual, starting from object variables by applying the successor function symbol(s).

Atomic formulas are either equalities of terms or expressions of the form A(t), where A is a predicate variable and t is a term.

Formulas are constructed from atomic ones by the usual rules using boolean connectives, parentheses, first- and second-order quantifiers: ∀^{1}x Φ, ∃^{1}x Φ, ∀^{2}X Φ, ∃^{2}X Φ, (where x is an object and X is a predicate variable).

Interpretation. For an n-successor theory SnS consider the infinite n-ary tree T_{n}^{∞}. Interpret: 1) object variables as nodes of the tree, 2) succ_{i}(t) as the i-th son of the node interpreting t, 3) equality, boolean connectives, and first-order quantifiers as usual,

4) predicate variables as arbitrary sets of nodes, 5) atomic formula A(t) as the membership relation “the node t is in the set A”; 6) second-order quantifiers as quantifiers over sets of nodes.

Denote by T h^{2}(SnS) or simply by SnS the set of all formulas valid under the above interpretation.

Replacing the interpretation 6) of the second-order quantifiers above by the following clause:

6′) second-order quantifiers are interpreted as quantifiers over finite sets of nodes,

we get the weak monadic second order arithmetic of n successors, denoted by WSnS.

All theories WSnS and SnS are decidable.

The most well known of all these are: Büchi’s arithmetic S1S, Rabin’s arithmetic S2S, and their weak counterparts WS1S, WS2S. The theory S2S is strictly more powerful than WS2S, S1S, and easily encodes all SnS. For details see [13, 14].

B F_{≤}^{Alg}: Curien-Ghelli’s Algorithmic Variant of F_{≤}

Curien and Ghelli [8], Sect. 6.1, suggested F_{≤}^{Alg}, an alternative equivalent formulation of F_{≤}. We present it following [12]:

Γ ⊢ τ ≤ ⊤  (T op)

Γ ⊢ α ≤ α (α is a variable)  (Refl)

\begin{matrix}Γ ⊢ Γ(α) ≤ τ \\ Γ ⊢ α ≤ τ \end{matrix}  (AlgT rans)

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

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

Three differences of F_{≤}^{Alg}, as compared to F_{≤} are: 1) reflexivity (Refl) is unlike (Refl) of F_{≤} is restricted to variables, 2) transitivity (T rans) is replaced by (AlgT rans); 3) rules are applied in ordered manner (e.g., (AlgT rans) never applies if (Refl) is applicable).

Remark. Note that the inversion principle trivially holds for the (Arrow) and (All) of F_{≤}^{Alg}: a conclusion of each rule is prov-

able iff so are the premises. Proofs in F_{≤}^{Alg} are direct, without roundabout ways.

Lemma B.1 (F_{≤}^{Alg} ≡ F_{≤}, [8]) The systems F_{≤} and F_{≤}^{Alg} are equivalent: a subtyping judgment is derivable in F_{≤} iff it is derivable in F_{≤}^{Alg}. □

As an immediate consequence we have the following

Lemma B.2 (Inversion Principle for F_{≤}) In F_{≤}:

• if Γ ⊢ σ_{1} → σ_{2} ≤ τ_{1} → τ_{2} is provable, then Γ ⊢ τ_{1} ≤ σ_{1}

and Γ ⊢ σ_{2} ≤ τ_{2} are also provable;

• if Γ ⊢ (∀α ≤ σ_{1} . σ_{2}) ≤ (∀α ≤ τ_{1} . τ_{2}) is provable, then Γ ⊢ τ_{1} ≤ σ_{1} and Γ , α ≤ τ_{1} ⊢ σ_{2} ≤ τ_{2} are also provable.

Proof . Using equivalence of F_{≤} and F_{≤}^{Alg}. Let Γ ⊢ σ_{1} → σ_{2} ≤

τ_{1} → τ_{2} be provable in F_{≤}. Then it is provable in F_{≤}^{Alg}. But the

only way to prove it in F_{≤}^{Alg} consists in proving Γ ⊢ τ_{1} ≤ σ_{1} and

Γ ⊢ σ_{2} ≤ τ_{2} in F_{≤}^{Alg} (since inversion principle holds for F_{≤}^{Alg}). Henceforth, by equivalence, Γ ⊢ τ_{1} ≤ σ_{1} and Γ ⊢ σ_{2} ≤ τ_{2} are provable in F_{≤}. The proof of the second claim is exactly the same. □

C Proofs

C.1 Proof of Proposition 4.2

Proof . (1). Is obvious. To prove (2) suppose, on the contrary, that a judgment of the form (2) is provable in F_{≤}, i.e., there exists a proof, i.e, a sequence of judgments

J_{0}, J_{1}, …, J_{i}, …, J_{n} ≡ Γ ⊢ σ ≤ α,  (5)

where each J_{i} is either an F_{≤}-axiom, or is obtained from some J_{k} and J_{l} (k < i and l < i) in the sequence by application of one of the F_{≤}-rules: (Arrow), (All), or (T rans). Without loss of generality we can suppose that J_{n} is the first appearance of the judgment of the form (2) in the proof (5); otherwise, we can move left to select the first judgment of this form.

It remains to notice that J_{n} cannot be an axiom, since there are no F_{≤}-axioms of the form (2). Next, neither (Arrow), nor (All) can produce a judgment of the form (2) (both produce types of the same structure). Therefore, (2) is obtained by (T rans). But to derive (2) by (T rans) one needs either J_{k} ≡ Γ ⊢ σ ≤ τ and J_{l} ≡ Γ ⊢ τ ≤ α (τ non-variable type), or J_{k} ≡ Γ ⊢ σ ≤ β and J_{l} ≡ Γ ⊢ β ≤ α (β is a type variable). Therefore, J_{k} has the form (2) and appears in (5) before J_{n}. But this contradicts to the choice of J_{n}. □

C.2 Proof of Theorem 11.1

Let a subtyping judgment J ≡ Γ ⊢ σ ≤ τ be provable in F_{≤}. Then, by equivalence of F_{≤} and F_{≤}^{Alg} (Lemma B.1), it is provable

in F_{≤}^{Alg}. Consider the F_{≤}^{Alg}-inference tree of J. If this tree does not contain applications of the rule (AlgT rans) corresponding to the (V ar-All-Decide) rule, then this tree is also the F_{≤}^{SnS}- inference tree of J and we are done.

Suppose now that the F_{≤}^{Alg}-inference tree T of J does contain applications of (AlgT rans) corresponding to the (V ar-All-Decide) rule. Transform this tree T as follows. Starting from the root J follow each branch till the first application of (AlgT rans) (if any), and cut it on this application so as the conclusion of (AlgT rans) remains in the tree. Denote by T′(J_{1}, …, J_{n}) the resulting tree, where J_{1}, …, J_{n} are all leavesconclusions of (AlgT rans) remaining after the above pruning. Note that T′(J_{1}, …, J_{n}) is exactly the F_{≤}^{SnS}-inference tree, and J_{1}, …, J_{n} are precisely F_{≤}^{SnS}-normal forms. Instead of applying (AlgT rans), the F_{≤}^{SnS}-decision procedure transforms J_{1}, …, J_{n} into SnS-formulas and decides them. So, to finish our proof we have to prove that J_{1}, …, J_{n} are interpreted as true SnSformulas.

To do this, notice, that by equivalence of F_{≤} and F_{≤}^{Alg}, all the judgments J_{1}, …, J_{n} are provable in F_{≤}. But by Theorem 6.4 above everything provable in F_{≤} is true with respect to any SnSinterpretation.

The strictness of inclusion is simple: since F_{≤}^{SnS} is decidable and F_{≤} is not, there should certainly exist F_{≤}^{SnS}-provable and not F_{≤}-provable subtyping judgments. □

C.3 Proof of Theorem 12.1

Again applying Theorem 6.4 above, all F_{≤}^{SnS}-inference rules preserve validity with respect to any SnS-interpretation. As normal forms of F_{≤}^{SnS} are decided by the same SnS-decision procedure, they are simultaneously true with respect to an SnSinterpretation SnS[F_{≤}](f, g) and F_{≤}^{SnS}(f, g). By definition, F_{≤}^{SnS}(f, g) does not subtype differently structured types, whereas SnS-interpretations do, e.g., ⊢ ⊤ → ⊤ ≤ ∀α.⊤ is true in any SnS-interpretation. □

C.4 Proof of Theorem 13.1

By induction on complexity of subtyping inference.

Suppose the premises of the theorem hold, i.e., Γ ⊢ σ ≤ τ and Γ ⊢ τ ≤ ρ are F_{≤}^{SnS}-provable.

We must show that so is Γ ⊢ σ ≤ ρ.

We have to consider several cases:

1. ρ is ⊤;

2. ρ is a type variable;

3. ρ is an arrow or a universal type, both σ and τ are type variables;

4. τ and ρ are both arrow types and σ is a type variable;

5. τ and ρ are both universal types and σ is a type variable;

6. σ, τ, and ρ are all arrow types;

7. σ, τ, and ρ are all universal types.

Case 1. Vacuous: Γ ⊢ σ ≤ ⊤, always.

Case 2. If ρ is a type variable then σ and τ should also be type variables; otherwise the rule (T V ar-R-2) would disprove one of the premises of the theorem.

So we should demonstrate that F_{≤}^{SnS}-provability of:

Γ ⊢ α ≤ β,  (6)
Γ ⊢ β ≤ γ  (7)

imply the F_{≤}^{SnS}-provability of

Γ ⊢ α ≤ γ  (8)

for type variables α, β, γ.

Note that the F_{≤}^{SnS}-proofs of (6) and (7) are just finite sequences of (T V ar-R-1)-applications finishing by an application of (Refl). These two sequences could be easily merged into just one such sequence proving (8). Indeed, starting from the judgment (8) by backward applications of (T V ar-R-1) we are guaranteed (by provability of (6)) to reach β on the left of ≤, i.e., we reach (7), which is provable by hypothesis.

Case 3. Suppose that ρ is either an →- or a ∀-type, σ and τ are type variables α and β respectively.

We transform the proofs of

Γ ⊢ α ≤ β,  (9)
Γ ⊢ β ≤ ρ  (10)

into the proof of

Γ ⊢ α ≤ ρ  (11)

as follows. Starting from the judgment (11) we first repeat (backwards) exactly the same sequence of steps as in the proof of (9), which leads to Γ ⊢ β ≤ β (but applying (V ar-Arrow) or (V ar-All-1) instead of (T V ar-R-1)). This gives the inference of (11) from (10) used as axiom. We then repeat the proof of the latter judgment, which exists by assumption. The result is the desired proof.

Case 4. Suppose

Γ ⊢ α ≤ τ_{1} → τ_{2},  (12)
Γ ⊢ τ_{1} → τ_{2} ≤ ρ_{1} → ρ_{2}  (13)

are F_{≤}^{SnS}-provable. We must prove that so is

Γ ⊢ α ≤ ρ_{1} → ρ_{2}  (14)

The proof of (12) is a finite sequence of (V ar-Arrow) followed either a) by (Refl) or b) by (Arrow).

In the Case 4.a we construct the proof of (14) (in a backward manner) first applying to (14) exactly the same sequence of (V ar-Arrow) applications until (Refl), as in the proof of (12). This gives a subinference of (14) from (13) used as an axiom. We then complete the latter subinference by including the proof of (13) (which is F_{≤}^{SnS}-provable by assumption).

In the Case 4.b we construct the proof of (14) as follows. Considering the final part of the inference of (12) till the first application of (Arrow):

Γ ⊢ σ_{1} → σ_{2} ≤ τ_{1} → τ_{2} (√) ; Γ ⊢ α′ ≤ τ_{1} → τ_{2} ; ⋮ ; α ≤ τ_{1} → τ_{2}  (15)

we see that (12) is provable iff (√) is provable. By the inversion property for F_{≤}^{SnS} (Theorem 10.1) this implies provability of

Γ ⊢ τ_{1} ≤ σ_{1},  (16)
Γ ⊢ σ_{2} ≤ τ_{2}  (17)

Similarly, provability of (13) implies provability of

Γ ⊢ ρ_{1} ≤ τ_{1},  (18)
Γ ⊢ τ_{2} ≤ ρ_{2}  (19)

Applying the inductive hypothesis to (18) and (16), then to (17) and (19) we get the F_{≤}^{SnS}-provability of Γ ⊢ ρ_{1} ≤ σ_{1} and Γ ⊢ σ_{2} ≤ ρ_{2}.

But this means that σ_{1} → σ_{2} ≤ ρ_{1} → ρ_{2} is also F_{≤}^{SnS}-provable. This allows us to transform the proof (15) into the proof of (14) by simple replacement of τ_{1} → τ_{2} by ρ_{1} → ρ_{2}.

Case 5. Suppose

Γ ⊢ α ≤ (∀β ≤ τ_{1} . τ_{2}),  (20)
Γ ⊢ (∀β ≤ τ_{1} . τ_{2}) ≤ (∀β ≤ ρ_{1} . ρ_{2})  (21)

are F_{≤}^{SnS}-provable. We have to prove that

Γ ⊢ α ≤ (∀β ≤ ρ_{1} . ρ_{2})  (22)

The proof of (20) is a finite (possibly empty) sequence of (V ar-All-1) followed either a) by (T V ar) or b) by (V ar-All-Decide).

In the Case 5.a we construct the proof of (22) first applying to it the same sequence of (V ar-All-1) as in the proof of (20), until (T V ar). This gives a subinference of (22) from (21) used as axiom. We then complete the latter subinference by including the proof of (21) (which is F_{≤}^{SnS}-provable by assumption).

In the Case 5.b we construct the proof of (22) as follows. Consider the final part of the inference of (20) till the application of (V ar-All-Decide):

Γ ⊢ DECIDE(Γ ⊢ α′ ≤ ∀β ≤ τ_{1} . τ_{2})(√) ; Γ ⊢ α′ ≤ (∀β ≤ τ_{1} . τ_{2}) ; ⋮ ; α ≤ (∀β ≤ τ_{1} . τ_{2})  (23)

We see that (20) is provable iff the F_{≤}^{SnS}-normal form in (√) is valid in a chosen theory SnS[F_{≤}](f, g). As each SnS[F_{≤}](f, g) is more powerful than the corresponding F_{≤}^{SnS}(f, g) (Theorem 12.1), the F_{≤}^{SnS}(f, g)-provability of (20) implies that:

[[ Γ ]]fg ⊧SnS ∀^{1}x[A′(x) ⊃ [[ ∀β ≤ τ_{1} . τ_{2} ]]fg(x)] (24)

Similarly, the F_{≤}^{SnS}(f, g)-provability of (21) implies

[[ Γ ]]fg ⊧SnS ∀^{1}x[[[ ∀β ≤ τ_{1} . τ_{2} ]]fg(x) ⊃ [[ ∀β ≤ ρ_{1} . ρ_{2} ]]fg(x)] (25)

Henceforth, by syllogistics, (24) and (25) imply

[[ Γ ]]fg ⊧SnS ∀^{1}x[A′(x) ⊃ [[ ∀β ≤ ρ_{1} . ρ_{2} ]]fg(x)]  (26)

Now, to construct the inference of (22) we start by the sequence of the same (V ar-All) applications as in (23) till Γ ⊢ α′ ≤ (∀β ≤ ρ_{1} . ρ_{2}). After that we should apply either the rule (T V ar) (in this case we are done), or the rule (V ar-All-Decide) getting DECIDE(Γ ⊢ α′ ≤ (∀β ≤ ρ_{1} . ρ_{2})). But in the latter case DECIDE should necessarily return the result T RUE (by (26)), and the desired F_{≤}^{SnS}(f, g)-proof is completed.

Case 7. Let

Γ ⊢ (∀β ≤ σ_{1} . σ_{2}) ≤ (∀β ≤ τ_{1} . τ_{2}),  (27)
Γ ⊢ (∀β ≤ τ_{1} . τ_{2}) ≤ (∀β ≤ ρ_{1} . ρ_{2})  (28)

We have to show

Γ ⊢ (∀β ≤ σ_{1} . σ_{2}) ≤ (∀β ≤ ρ_{1} . ρ_{2})  (29)

By Inversion principle (Lemma 10.1) from (27) and (28) we get:

Γ ⊢ τ_{1} ≤ σ_{1}  (30)
Γ, β ≤ τ_{1} ⊢ σ_{2} ≤ τ_{2}  (31)
Γ ⊢ ρ_{1} ≤ τ_{1}  (32)
Γ, β ≤ ρ_{1} ⊢ τ_{2} ≤ ρ_{2}  (33)

From (32) and (30) by induction hypothesis we get

Γ ⊢ ρ_{1} ≤ σ_{1}  (34)

From (31), (32) and (33) by induction hypothesis we get

Γ, α ≤ ρ_{1} ⊢ σ_{2} ≤ ρ_{2}  (35)

(each time instead of using the hypothesis β ≤ τ_{1} we use the hypothesis β ≤ ρ_{1} and (32)). But (34) and (35) imply (29).

Case 6 is completely analogous to the preceding one. □

[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-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

MPI-I-94-228 H. J. Ohlbach Computer Support for the Development and Investigation of Logics

MPI-I-94-226 H. J. Ohlbach, D. Gabbay, D. Plaisted  Killer Transformations

MPI-I-94-225 H. J. Ohlbach Synthesizing Semantics for Extensions of Propositional Logic

MPI-I-94-224 H. Aït-Kaci, M. Hanus, J. J. M. Navarro Integration of Declarative Paradigms: Proceedings of the ICLP’94 Post-Conference Workshop Santa Margherita Ligure, Italy

MPI-I-94-223 D. M. Gabbay LDS – Labelled Deductive Systems: Volume 1 — Foundations

MPI-I-94-218 D. A. Basin  Logic Frameworks for Logic Programs
MPI-I-94-216 P. Barth  Linear 0-1 Inequalities and Extended Clauses
MPI-I-94-209 D. A. Basin, T. Walsh  Termination Orderings for Rippling