Structural decidable extensions of Fsub

• To: types@uk.ac.glasgow.dcs
• Subject: Structural decidable extensions of Fsub
• From: Serge Vorobyov <Serge.Vorobyov@fr.loria>
• Date: Tue, 19 Jul 1994 07:51:30 +0200
• Approved: types@dcs.gla.ac.uk

The paper

	Structural Decidable Extensions
	   of Bounded Quantification

		Sergei Vorobyov

is available by anonymous ftp from

	ftp.loria.fr

directory: pub/loria/prograis/vorobyov
files:	   popl95.{dvi,ps}.Z)

or by mosaic ftp://ftp.loria.fr/pub/loria/prograis/vorobyov

Abstract. We show how the subtype relation of the well-known
second-order polymorphic system Fsub with subtyping and bounded type
quantification due to Cardelli, Wegner, Bruce, Longo, Curien, Ghelli,
proved undecidable by Pierce, can be interpreted in a (weak) monadic
second-order theory of one (B\"uchi), two (Rabin), several, or
infinitely many successor functions. These (W)SnS-interpretations show
that undecidable Fsub possesses consistent decidable extensions, i.e.,
Fsub is not essentially undecidable (Tarski, 1949).

We then demonstrate an infinite class of structural 
decidable extensions of Fsub, which combine traditional subtype
inference rules with the above (W)SnS-interpretations. All these
extensions, which we call FsubSnS, are still more
powerful than Fsub, but less coarse than the direct
(W)SnS-interpretations are:

	Fsub \subset FsubSnS \subset (W)SnS-interpretations

The main distinctive features of the systems FsubSnS are:

1) decidability,
2) closure wrt transitivity;
3) structuredness, 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:

	G |- T1 <: S1        G, A<:T1 |- S2 <: T2
	-----------------------------------------  (All)
	  G |- (All A<:S1.S2) <: (All A<:T1.T2)

• Prev: paper announcement
• Next: types
• Index(es):
  • Main
  • Thread