21.4 A Digression on Transitivity

 < Free Open Study > 



21.4 A Digression on Transitivity

We saw in Chapter 16 that standard formulations of inductively defined subtype relations generally come in two forms: a declarative presentation that is optimized for readability and an algorithmic presentation that corresponds more or less directly to an implementation. In simple systems, the two presentations are fairly similar; in more complex systems, they can be quite different, and proving that they define the same relation on types can pose a significant challenge. (We will see an example of this in Chapter 28; many others have been studied.)

One of the most distinctive differences between declarative and algorithmic presentations is that declarative presentations include an explicit rule of transitivityif S<:U and U<:T then S<:Twhile algorithmic systems do not. This rule is useless in an algorithm, since applying it in a goal-directed manner would involve guessing U.

The rule of transitivity plays two useful roles in declarative systems. First, it makes it obvious to the reader that the subtype relation is, indeed, transitive. Second, transitivity often allows other rules to be stated in simpler, more primitive forms; in algorithmic presentations, these simple rules need to be combined into heavier mega-rules that take into account all possible combinations of the simpler ones. For example, in the presence of transitivity, the rules for "depth subtyping" within record fields, "width subtyping" by adding new fields, and "permutation" of fields can be stated separately, making them all easier to understand, as we did in §15.2. Without transitivity, the three rules must be merged into a single one that takes width, depth, and permutation into account all at once, as we did in §16.1.

Somewhat surprisingly, the possibility of giving a declarative presentation with the rule of transitivity turns out to be a consequence of a "trick" that can be played with inductive, but not coinductive, definitions. To see why, observe that the property of transitivity is a closure propertyit demands that the subtype relation be closed under the transitivity rule. Since the subtype relation for finite types is itself defined as the closure of a set of rules, we can achieve closure under transitivity simply by adding it to the other rules. This is a general property of inductive definitions and closure properties: the union of two sets of rules, when applied inductively, generates the least relation that is closed under both sets of rules separately. This fact can be formulated more abstractly in terms of generating functions:

21.4.1 Proposition

Suppose F and G are monotone functions, and let H(X) = F(X)ÈG(X). Then μH is the smallest set that is both F-closed and G-closed.

Proof: First, we show that μH is closed under both F and G. By definition, μH = H(μH) = F(μH) È G(μH), so F(μH) μH and G(μH) μH. Second, we show that μH is the least set closed under both F and G. Suppose there is some set X such that F(X) X and G(X) X. Then H(X) = F(X)ÈG(X) È X, that is, X is H-closed. Since μH is the least H-closed set (by the Knaster-Tarski theorem), we have μH X.

Unfortunately, this trick for achieving transitive closure does not work when we are dealing with coinductive definitions. As the following exercise shows, adding transitivity to the rules generating a coinductively defined relation always gives us a degenerate relation.

21.4.2 Exercise []

Suppose F is a generating function on the universe U. Show that the greatest fixed point vFTR of the generating function

FTR(R) = F(R) È TR(R)

is the total relation on U × U.

In the coinductive setting, then, we drop declarative presentations and work just with algorithmic ones.



 < 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