The notion of a powertype is described
in terms of object membership as introduced in
Considered are the (original) Cardelli's power types,
the Odell's powertypes in metamodelling,
occurrences of powertype relationship in RDF Schema.
|Jablonec nad Nisou|
(see Document history)
|Initial release||March 12, 2015|
|Last major release
||March 12, 2015|
|Last update||March 12, 2015|
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
preceded by an
implicit rule asserting that every type has a power type.
In order not to make
(pt~2) and (pt~4)
:Type rule and the Power Formation rule, respectively)
objects that do not have a type
as well as
objects that have members but are not types.
Subsequently, we introduce additional conditions
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,
that is, Type equals the power type of the inheritance root r.
Abstract power type system
By an abstract power type system we mean
(O, ϵ, .ec, ⅽ)
ϵ, .ec and ⅽ are
O is a set of objects,
is the membership (typing) relation between objects,
is the power type partial map on objects,
type of types, a distinguished object.
:, 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:
u ≤ x iff
u = x or u ϵ x.ec.
Every type has a power type, that is,
for every x from ⅽ.϶, x.ec is defined.
ⅽ ϵ ⅽ, that is, ⅽ is a type.
|| (Type Formation)
O.ec ≤ ⅽ, that is, every power type
is a subtype of ⅽ.
|| (Type Subtyping)
For every x such that x.ec is defined,
x.ec ϵ ⅽ,
i.e. power types are types.
|| (Power Formation)
For every x such that x.ec is defined,
x ϵ x.ec,
i.e. (.ec) ⊆ (ϵ).
|| (Power Introduction)
The subsumption rule applies: (ϵ) ○ (≤) ⊆ (ϵ).
|| (Power Elimination)
The .ec map is monotone:
For every types x, y,
x ≤ y implies x.ec ≤ y.ec.
|| (Power Subtyping)
The domain of .ec equals ⅽ.϶, that is,
for every object x,
x.ec is defined
x is a type.
≤ is a preorder.
The transitivity is
by (pt~6) and (pt~7).
If ≤ is antisymmetric
.ec is injective.
If x.ec = y then x.↧ = y.϶.
← direction is by (pt~1).
→, 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 ϵ ⅽ.
To show that ≤ is transitive, let x < y < z.
Then by definition of ≤,
each of x, y and z has a power type.
x.ec ≤ y.ec ≤ z.ec
x ϵ x.ec ≤ y.ec ≤ z.ec
x ϵ y.ec ≤ z.ec
x ϵ z.ec
(again by (pt~6)),
x ≤ z
(by definition of ≤).
Let x, y be types such that x.ec = y.ec.
x ϵ y.ec and y ϵ x.ec,
x ≤ y and y ≤ x.
If ≤ is antisymmetric then x = y.
The statement follows by definition of ≤
The following diagrams show examples of structures satisfying
Both structures are
strange w.r.t. the type terminology.
The following observation 1 shows that disallowing
(ⅰ) and (ⅱ)
in a natural way
makes some Cardelli's axioms redundant.
x is of type y but y is not a type.
the x object does not have a type.
O.ϵ ⊆ ⅽ.϶,
that is, only types can have members.
(pt~4) is redundant.
(pt~2) can be equivalently replaced by:
ⅽ.϶ ≠ ∅,
that is, there is at least one type.
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.
Assume O.ϵ ⊆ ⅽ.϶.
Since O.ec ⊆ O.ϵ by
(pt~5) it follows that
O.ec ⊆ ⅽ.϶.
ⅽ.϶ ≠ ∅
ⅽ ∈ O.ϵ
ⅽ ∈ ⅽ.ϵ
ⅽ ϵ ⅽ.
Assume that x.ec is only defined for types x
(so that O.ec = ⅽ.϶.ec)
and r.ec = ⅽ for some r
(so that r.↧ = ⅽ.϶).
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
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.
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
(O, ϵ, .ec, r).
O.ϵ ⊆ ⅽ.϶,
that is, only types can have members.
(This makes (pt~4) redundant,
O.϶ = O,
that is, every object has a type.
(This makes (pt~2) redundant,
ⅽ ∈ O.ec,
that is, ⅽ is a power type.
≤ is antisymmetric.
(In particular, .ec is injective.)
(The definitional correspondence.)
For a structure (O, ϵ, .ec, r, ⅽ)
such that r.ec = ⅽ the following
(O, ϵ, .ec, ⅽ) is an
abstract power type system
(O, ϵ, .ec, r) satisfies
from the axiomatization of powertype-based structures
(The inheritance relation ≤ is derived the same way as in Sa,
.ce is the inverse of .ec.)
O.ce = r.↧.
(The powerclass map .ec
is defined exactly for descendants of r.)
O.ϵ ≤ r.
(Every container is a descendant of r.)
O = O.϶.
(Every object has a container.)
(.ec) ⊆ (ϵ).
Powerclass-of is a special case of
(ϵ) ○ (≤) ⊆ (ϵ).
(The subsumption rule.)
(.ce) ○ (≤) ○ (.ec) ⊆ (≤).
(Monotonicity of .ec.)
(<) ∩ (>) = ∅.
(Antisymmetry of ≤.)
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.
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.
A type can have more than one powertype.
There is no typing relation (instance-of)
between a type and its powertype.
The diagram on the right shows a monotonic structure of ϵ
Powertypes as anti-members
As already observed above,
a common generalization of the Cardelli's and Odell's notions
can be established
powertype as a synonym for
Recall that ϶-1 is an abstraction of
(.ec) ○ (≥).
In powerclass complete structures, x.϶-1 = x.ec.↧,
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).
y is a powertype of x
y ϵ-1 x.
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.
The following table shows the entailments rules which impose the assertion.
The diagram only displays a part of the built-in structure.
For the whole structure, see
rdfs:Datatype are shown according to RDF 1.1 Semantics
as 2 new built-in instances of
to the previous 2004 version .
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
– instances of
rdf:Property (they are displayed in light green).
P suffix for the
inheritance relation ≤ indicates a distinction between classes and properties,
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.
in OWL 2
an additional axiomatic triple makes
||c.϶ ≤C r
All classes are subclasses of r.
||x ϵ c
||x ≤C r
are subproperties of
are subclasses of
rdfs:Literal class an instance of
Powertypes as public
The case (x,y) = (r,c) in the RDFS core structure
shows that there can be a reasonable
powertype that goes beyond anti-membership.
In the standard eigenclass completion
(as supported by Ruby and even by Smalltalk-80),
the c class (named
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.
Structural Subtyping and the Notion of Power Type,
Proc. of the 15th ACM Symp. on Principles of Programming Languages, POPL'88,
A powertype-based metamodelling framework,
Software & Systems Modeling 5.1
Journal of Object-Oriented Programming 7.2
Modeling techniques for multi-level abstraction,
The evolution of conceptual modeling
Springer Berlin Heidelberg
OMG UML Superstructure 2.4.1,
Object Management Group
Object Membership: The Core Structure of Object Technology,
Object Membership – Basic Structure,
Object Membership: The ontological structure,
OWL 2 RDF-Based Semantics,
RDF 1.1 Semantics,
The initial release.
This work is licensed under a
Creative Commons Attribution-NonCommercial-ShareAlike 3.0 License.