21.10 Digression: An Exponential Algorithm

 < Free Open Study > 



21.10 Digression: An Exponential Algorithm

The algorithm subtype presented at the beginning of §21.9 (Figure 21-4) can be simplified a bit more by making it return just a boolean value rather than a new set of assumptions (see Figure 21-5).The resulting procedure, subtypeac, corresponds to Amadio and Cardelli's algorithm for checking sub-typing (1993). It computes the same relation as the one computed by subtype, but much less efficiently because it does not remember pairs of types in the subtype relation across the recursive calls in the and × cases. This seemingly innocent change results in a blowup of the number of recursive calls the algorithm makes. Whereas the number of recursive calls made by subtype is proportional to the square of the total number of subexpressions in the two argument types (as can be seen by inspecting the proofs of Lemma 21.9.8 and Proposition 21.9.11), in the case of subtypeac it is exponential.


Figure 21-5: Amadio and Cardelli's Subtyping Algorithm

The exponential behavior of subtypeac can be seen clearly in the following example. Define families of types Sn and Tn inductively as follows:

  •  

    S0

    =

    μX.Top × X

    Sn+1

    =

    μX.XSn

    T0

    =

    μX. Top × (Top × X)

    Tn+1

    =

    μX.XTn.

Since Sn and Tn each contain just one occurrence of Sn-1 and Tn-1, respectively, their size (after expanding abbreviations) will be linear in n. Checking Sn <: Tn generates an exponential derivation, however, as can be seen by the following sequence of recursive calls

  •  

     

    subtypeac (, Sn, Tn)

    =

    subtypeac (A1, Sn Sn-1, Tn)

    =

    subtypeac (A2, Sn Sn-1, Tn Tn-1)

    =

    subtypeac (A3, Tn, Sn) and subtypeac (A3, Sn-1, Tn-1)

    =

    subtypeac (A4, Tn Tn-1, Sn) and...

    =

    subtypeac (A5, Tn Tn-1, Sn Sn-1 and ...

    =

    subtypeac (A6, Sn, Tn) and subtypeac (A6, Tn-1, Sn-1) and ...

    =

    etc.,

where

A1

=

{(Sn, Tn)}

A2

=

A1 È {(Sn Sn-1, Tn)}

A3

=

A2 È {(Sn Sn-1, Tn Tn-1)}

A4

=

A3 È {(Tn, Sn)}

A5

=

A4 È {(Tn Tn-1, Sn)}

A6

=

A5 È {(Tn Tn-1, S n Sn-1)}.

Notice that the initial call subtypeac (, Sn, Tn) results in the two underlined recursive calls of the same form involving Sn-1 and Tn-1. These, in turn, will each give rise to two recursive calls involving Sn-2 and Tn-2, and so on. The total number of recursive calls is thus proportional to 22.



 < Free Open Study > 



Types and Programming Languages
Types and Programming Languages
ISBN: 0262162091
EAN: 2147483647
Year: 2002
Pages: 262

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net