Classification-Projection Diagram

Reminder: Because MS-Word 2000 is being used to generate these web pages, it is highly recommended that you use Microsoft Internet Explorer version 5.0 when viewing this site.

Overview

We are interested in defining the semantics for the following fundamental classification projection diagram.

Entity is the disjoint union (type sum) of Object, the metaclass for all object types, and Data, the metaclass for all datatypes either primitive or defined (such as enums).

Note

In the theory of Information Flow constraints are represented by sequents. As mentioned in the textbook by Barwise and Seligman, there are five special kinds of sequents.

Entailment: A constraint of the form a ⊢ b (the left- and right-hand sides are both singletons) represents the claim that a entails b.

Necessity: A constraint of the form ⊢ a (the left-hand side is empty, the right is a singleton) represents the claim that the type a is necessarily the case, without any preconditions.

Exhaustive cases (cover): A constraint of the form ⊢ a, b (the left-hand side is empty, the right-hand side is a doubleton) represents the claim that every instance is either one of the two types, again without any preconditions.

Incoherent type: A constraint of the form a ⊢ (the right-hand side is empty, the left is a singleton) represents the claim that no instance is of type a.

Incompatible types (disjointness): A constraint of the form a, b ⊢ (the right-hand side is empty, the left is a doubleton) represents the claim that no instance is of both types a and b. (This is because no instance could satisfy any type on the right, because there are none, and hence could not satisfy both types on the left.)

Constraints

In the discussion below let r be a relation instance having source entity a and target entity b, let r be a relation type having source type a and target type b, and let s be a relation type having source type g and target type d. In symbols,

instances	types
¶₀(r) = a and ¶₁(r) = b	r : a ® b
¶₀(r) = a and ¶₁(r) = b	r : a ® b
¶₀(s) = g and ¶₁(s) = d	s : g ® d

This diagram states the following property: If r is an instance of (classified as) type r, then entity a is an instance of type a and entity b is an instance of type b. In symbols,

preservation of classification:

r ⊨ r implies a ⊨ a

r ⊨ r implies b ⊨ b

Here are several examples of binary relation semantics.

· The motherhood binary relation on the type Person is a subtype of the parenthood binary relation on the type Person. If the woman w is the mother of a boy b, then w is a parent of b. This might be rendered formally by the assertion

inclusion implies subtype:

r £ s implies r ⊢ s

· The authorship binary relation from type Person to type Book is a subtype of the creatorship binary relation from type Agent to type Work. If a man m is an author of a book b, then the agent m is a creator of the work b. The facts that type Person is a subtype of type Agent and type Book is a subtype of type Work may be necessary conditions for the subtype relation. If true, this would be symbolized

preservation of entailment:

r ⊢ s implies a ⊢ g

r ⊢ s implies b ⊢ d

· The sibling relation on type Person is disjoint from the employment relation from type Person to type Organization. This is implied by the fact that type Person is disjoint from type Organization. This seems to be true in general, both for the source and target projections. Using symbols,

creation of incompatible types:

a, g ⊢ implies r, s ⊢

b, d ⊢ implies r, s ⊢

· If a relation type is specified to have a source (or target) entity type that is later found to be incoherent, then the relation type is also incoherent.

creation of incoherent type:

a ⊢ implies r ⊢

b ⊢ implies r ⊢

Operations

There are three operations on binary relations that contribute to an understanding of their semantics: restriction, sum and quotient. These operations compare somewhat to analogous operations on IF classifications.

Motherhood for the Person type is a restriction of motherhood for the Mammal type. Authorship of email and authorship of regular mail has a sum authorship relation type for mail in general. If we assume (and specify) that the two terms “company” and “corporation” are synonyms, then the employee binary relation type from the entity type Organization to the entity type Person should treat the subtypes Company and Corporation in an equivalent manner. This behavior is definable as a quotient of the original employee relation type.

Restriction

Given any binary relation type r : a ® b and any subtypes g ⊢ a and d ⊢ b, the restriction of r to g at the source and d at the target is denoted

r^g_d : g ® d

Some obvious constraints are the following:

r^g_d ⊢ r “the restriction entails the original”

r^a_b= r “the identity restriction is the original”

Sum

Given two binary relations r : a ® b and s : g ® b with a common target type, if the source types are an exact partition of a third type c (they are disjoint a,g ⊢ , they cover c in the sense that c ⊢ a, g and they are subtypes a ⊢ c and g ⊢ c), then we can define the source sum (also called the copairing) of r and s

[r,s] : c ® b

Some obvious constraints are the following:

r ⊢ [r,s] and s ⊢ [r,s] “each summand entails the sum”

r ⊢ t and s ⊢ t imply [r,s] ⊢ t “the sum is the least common supertype”

[r,s]^a = r “the precise restriction of a sum is the original summand”

[t^a,t^g] = t “the sum of the restrictions is the original” (where t : c ® b is any relation whose source is the partiton sum);

[r,o_b] = r “zero relations are the identity for sum” (where o_b : o ® b is the unique relation from the zero (bottom) source type).

Quotient

Please send questions, comments and suggestions about this page to: Robert E. Kent rekent@ontologos.org