Object Membership
and Powertypes

The notion of a powertype is described in terms of object membership as introduced in [] and []. Considered are the (original) Cardelli's power types, the Odell's powertypes in metamodelling, and occurrences of powertype relationship in RDF Schema.

Preface

Author
Ondřej Pavlata
Jablonec nad Nisou
Czech Republic
Document date
Initial releaseMarch 12, 2015
Last major release March 12, 2015
Last updateMarch 12, 2015
(see Document history)
Warning
  1. This document has been created without any prepublication review except those made by the author himself.

Table of contents

Cardelli's power types

In this section we describe the abstract structure of Cardelli's power type system [] in terms of object membership. We only focus on the structure induced by the typing relation and the power type operator. We first provide an axiomatization corresponding to the Cardelli's typing rules (pt~2)–(pt~7) preceded by an implicit rule asserting that every type has a power type. In order not to make (pt~2) and (pt~4) redundant (the Type:Type rule and the Power Formation rule, respectively) we allow (a) objects that do not have a type as well as (b) objects that have members but are not types.

Subsequently, we introduce additional conditions (pt~8)–(pt~11) so that the resulting axiomatization is equivalent to the first 7 axioms of the family of of powertype-based structures [] (which is a subfamily of basic structures []). A notable constituent of the correspondence is the identification of Type with the root of the 2nd metalevel, equivalently,

that is, Type equals the power type of the inheritance root r.
Abstract power type system
By an abstract power type system we mean a structure (O, ϵ, .ec, ⅽ) where In [], ϵ, .ec and ⅽ are denoted :, Power() and Type, respectively. Objects from ⅽ.϶ (members of ⅽ) are called types. Objects from O.ec are power types. Let ≤ be a relation between objects defined by The restriction of ≤ to types is called subtyping. The structure is subject to the following conditions:
(pt~1) Every type has a power type, that is, for every x from ⅽ.϶,   x.ec is defined.
(pt~2) ⅽ ϵ ⅽ, that is, ⅽ is a type.   (Type Formation)
(pt~3) O.ec ≤ ⅽ, that is, every power type is a subtype of ⅽ.   (Type Subtyping)
(pt~4) For every x such that x.ec is defined,   x.ec ϵ ⅽ,   i.e. power types are types.   (Power Formation)
(pt~5) For every x such that x.ec is defined,   x ϵ x.ec,   i.e. (.ec) ⊆ (ϵ).   (Power Introduction)
(pt~6) The subsumption rule applies: (ϵ) ○ (≤) ⊆ (ϵ).   (Power Elimination)
(pt~7) The .ec map is monotone: For every types x, y,   x ≤ y implies x.ec ≤ y.ec.   (Power Subtyping)

Observations:

  1. The domain of .ec equals ⅽ.϶, that is, for every object x,   x.ec is defined   ↔   x is a type.
  2. ≤ is a preorder. The transitivity is by (pt~6) and (pt~7).
  3. If ≤ is antisymmetric   then   .ec is injective.
  4. If x.ec = y then x.↧ = y.϶.

Proof:

  1. The ← direction is by (pt~1). To show →, let x be such that x.ec is defined. Then, by (pt~5), x ϵ x.ec and, by (pt~3) x.ec ≤ ⅽ. It follows by subsumption (pt~6) that x ϵ ⅽ.
  2. To show that ≤ is transitive, let x < y < z. Then by definition of ≤, each of x, y and z has a power type. Consequently,
  3. Let x, y be types such that x.ec = y.ec. By (pt~5),   x ϵ y.ec and y ϵ x.ec, that is, x ≤ y and y ≤ x. If ≤ is antisymmetric then x = y.
  4. The statement follows by definition of ≤ using (pt~5).
Nonsense structures
The following diagrams show examples of structures satisfying (pt~1)–(pt~7). Both structures are strange w.r.t. the type terminology.
(ⅰ)
¬(pt~8): x ϵ y ∉ ⅽ.϶
(ⅱ)
¬(pt~9): x.ϵ = ∅
The following observation 1 shows that disallowing (ⅰ) and (ⅱ) in a natural way makes some Cardelli's axioms redundant.

Observations:

  1. Assume that O.ϵ ⊆ ⅽ.϶, that is, only types can have members.
    1. (pt~4) is redundant.
    2. (pt~2) can be equivalently replaced by:   ⅽ.϶ ≠ ∅, that is, there is at least one type.
  2. Assume that ⅽ is a power type and that the domain of .ec equals ⅽ.϶ (that is, only types have power types). Then (pt~3) is redundant.

Proof:

  1. Assume O.ϵ ⊆ ⅽ.϶.
    1. Since O.ec ⊆ O.ϵ by (pt~5) it follows that O.ec ⊆ ⅽ.϶.
    2. ⅽ.϶ ≠ ∅ ↔ ⅽ ∈ O.ϵ ↔ ⅽ ∈ ⅽ.ϵ ↔ ⅽ ϵ ⅽ.
  2. Assume that x.ec is only defined for types x (so that O.ec = ⅽ.϶.ec) and r.ec = ⅽ for some r (so that r.↧ = ⅽ.϶). Then where the inclusion ⊆ is by the monotonicity condition (pt~7).
Establishing basic structure of ϵ
Consider an abstract power type system Sa = (O, ϵ, .ec, ⅽ) satisfying the following additional conditions (pt~8)–(pt~11).
(pt~8) O.ϵ ⊆ ⅽ.϶, that is, only types can have members.   (This makes (pt~4) redundant, see observation 1a.)
(pt~9) O.϶ = O, that is, every object has a type.   (This makes (pt~2) redundant, see observation 1b.)
(pt~10) ⅽ ∈ O.ec, that is, ⅽ is a power type.
(pt~11) ≤ is antisymmetric.   (In particular, .ec is injective.)
The following diagrams (ⅲ) and (ⅳ) show examples of abstract power type systems that are disallowed by just one of (pt~10) or (pt~11). Examples of structures disallowed by (pt~8) and (pt~9) have been shown in the previous subsection.
(ⅲ)
¬(pt~10):
ⅽ ∉ O.ec
(ⅳ)
¬(pt~11):
x < y < x
Since .ec is injective and ⅽ ∈ O.ec there is a unique object r such that r.ec = ⅽ. By replacing ⅽ with r in the signature of Sa we obtain a structure Sb = (O, ϵ, .ec, r).
The correspondence

Proposition: (The definitional correspondence.)
For a structure (O, ϵ, .ec, r, ⅽ) such that r.ec = ⅽ the following are equivalent:

Powertypes in metamodelling

The Cardelli's notion of power types has been adopted by J. Odell in the field of metamodelling [] [] [] [], recently also spelled as a single word powertypes which we will use for a distinction. In metamodelling, the meaning of the term is different. This can be observed on the following characteristics.
  1. A type can have more than one powertype.
  2. There is no typing relation (instance-of) between a type and its powertype.
Instead of being an abstraction of a powerset, Odell's powertype is an abstraction of a non-trivial partition. As a consequence, the powertype relation corresponds to a distinquished subrelation of the inverse of the non-member union map .ⱷ. [] The semantic shift from the Cardelli's power types to metamodelling powertypes can be therefore diagrammatized by where .ⱷ' is a distinguished subrelation of .ⱷ. The common property of (.ec) and .ⱷ'(-1) is that both are subrelations of ϶-1, the inverse of anti-membership.

The diagram on the right shows a monotonic structure of ϵ in which M and N are designed powertypes of A.

Powertypes as anti-members

As already observed above, a common generalization of the Cardelli's and Odell's notions can be established by regarding powertype as a synonym for anti-member. That is, Recall that ϶-1 is an abstraction of (.ec) ○ (≥). In powerclass complete structures, x.϶-1 = x.ec.↧, i.e. anti-members of x are exactly the descendants of the powerclass of x. Furthemore, the anti-membership relation ϵ-1 can be regarded as an assertion of the impliciation i.e. for every pair (x,y) from ϶-1 it is asserted that all members of y are among descendants of x (in any extension of the membership structure).
In RDF Schema
In RDF Schema (RDFS) [] [], the y.϶ ≤ x condition is imposed for three pairs (x,y) of resources of the built-in structure, as shown by thick brown arrows in the following diagram.
r… rdfs:Resource
c… rdfs:Class
p… rdf:Property
D… rdfs:Datatype
L… rdfs:Literal
XL… rdf:XMLLiteral
m… rdfs:member
CMP… rdfs:ContainerMembershipProperty

Notes:

  1. The diagram only displays a part of the built-in structure. For the whole structure, see [] or [].
  2. Instances of rdfs:Datatype are shown according to RDF 1.1 Semantics [] which adds rdf:HTML and rdf:langString as 2 new built-in instances of rdfs:Datatype to the previous 2004 version [].
  3. The structure satisfies all conditions of a monotonic structure of ϵ except for the minimality of objects from the the 0-th metalevel. In the example structure, the 0-th metalevel is exclusively formed by properties – instances of rdf:Property (they are displayed in light green).
The following table shows the entailments rules which impose the assertion. The C and P suffix for the inheritance relation ≤ indicates a distinction between classes and properties, respectively.
Rule
name		 Convenient expression Description Triple inference
rdfs8 c.϶  ≤C  r All classes are subclasses of r. x ϵ c → x ≤C r
rdfs12 CMP.϶  ≤P  m Instances of rdfs:ContainerMembershipProperty are subproperties of rdfs:member. x ϵ CMP → x ≤P m
rdfs13 D.϶  ≤C  L Instances of rdfs:Datatype are subclasses of rdfs:Literal. x ϵ D → x ≤C L
In case of (x,y) = (r,c), it is even ensured (by a combination of axiomatic triples and another rules) that x.↧ = y.϶. In the remaining 2 cases, we have y.϶ < x, at least in the built-in structure. Interestingly, in OWL 2 [], an additional axiomatic triple makes the rdfs:Literal class an instance of rdfs:Datatype.
Powertypes as public powerclasses
The case (x,y) = (r,c) in the RDFS core structure shows that there can be a reasonable interpretation of powertype that goes beyond anti-membership. In the standard eigenclass completion (as supported by Ruby and even by Smalltalk-80), the c class (named Class) is not a descendant of r.ec and thus not an anti-member of r. Instead, c is an inheritance parent of r.ec and it is asserted that r.ec has no siblings in inheritance (see axiom (e~7) in []) which results in That is, the c class is asserted to have exactly the same members as the powerclass of r and is thus to be type-equivalent to this powerclass.

 

References
Luca Cardelli, Structural Subtyping and the Notion of Power Type, Proc. of the 15th ACM Symp. on Principles of Programming Languages, POPL'88, 1988, http://www.daimi.au.dk/~madst/tool/tool2004/papers/structural.pdf
Cesar Gonzalez-Perez, Brian Henderson-Sellers, A powertype-based metamodelling framework, Software & Systems Modeling 5.1 2006
James J. Odell, Power Types, Journal of Object-Oriented Programming 7.2 1994
Bernd Neumayr, Michael Schrefl, Bernhard Thalheim, Modeling techniques for multi-level abstraction, The evolution of conceptual modeling Springer Berlin Heidelberg 2011
OMG, OMG UML Superstructure 2.4.1, Object Management Group 2011
Ondřej Pavlata, Object Membership: The Core Structure of Object Technology, 2012–2015, http://www.atalon.cz/om/object-membership/
RDFS core
Ondřej Pavlata, Object Membership – Basic Structure, 2015, http://www.atalon.cz/om/object-membership/basic/
basic structure , powertype-based structure , union
Ondřej Pavlata, Object Membership: The ontological structure, 2012, http://www.atalon.cz/om/object-membership/ontology/
RDFS built-in structure
World Wide Web Consortium, OWL 2 RDF-Based Semantics, 2009, http://www.w3.org/TR/owl2-rdf-based-semantics/
World Wide Web Consortium, RDF Schema, 2004, http://www.w3.org/TR/rdf-schema/
World Wide Web Consortium, RDF Semantics, 2004, http://www.w3.org/TR/2004/REC-rdf-mt-20040210/
World Wide Web Consortium, RDF 1.1 Semantics, 2014, http://www.w3.org/TR/2014/REC-rdf11-mt-20140225/
Document history
March122015 The initial release.
License
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License.