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 release  March 12, 2015 
Last major release 
March 12, 2015 
Last update  March 12, 2015 
(see Document history)

Warning

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 powertypebased 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

O is a set of objects,

ϵ
is the membership (typing) relation between objects,

.ec
is the power type partial map on objects,

ⅽ
is the
type of types
, a distinguished object.
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

u ≤ x iff
u = x or u ϵ x.ec.
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:

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
then
.ec is injective.

If x.ec = y then x.↧ = y.϶.
Proof:

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 ϵ ⅽ.

To show that ≤ is transitive, let x < y < z.
Then by definition of ≤,
each of x, y and z has a power type.
Consequently,

x.ec ≤ y.ec ≤ z.ec
(by (pt~7)),

x ϵ x.ec ≤ y.ec ≤ z.ec
(by (pt~5)),

x ϵ y.ec ≤ z.ec
(by (pt~6)),

x ϵ z.ec
(again by (pt~6)),

x ≤ z
(by definition of ≤).

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.

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.

In (ⅰ),
x is of type y
but y is not a type.

In (ⅱ),
the x object does not have a type.
The following observation 1 shows that disallowing
(ⅰ) and (ⅱ)
in a natural way
makes some Cardelli's axioms redundant.
Observations:

Assume that
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.
Proof:

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.↧ = ⅽ.϶).
Then

O.ec =
r.↧.ec ⊆
r.ec.↧
= ⅽ.↧
≤ ⅽ
where the inclusion ⊆ is by
the monotonicity condition (pt~7).
Establishing basic structure of ϵ
Consider an abstract power type system
S_{a} = (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.
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 S_{a}
we obtain a structure
S_{b} =
(O, ϵ, .ec, r).
The correspondence
Proposition:
(The definitional correspondence.)
For a structure (O, ϵ, .ec, r, ⅽ)
such that r.ec = ⅽ the following
are equivalent:

S_{a} =
(O, ϵ, .ec, ⅽ) is an
abstract power type system
satisfying
(pt~8)–(pt~11).

S_{b} =
(O, ϵ, .ec, r) satisfies
(ptb~1)–(ptb~7)
from the axiomatization of powertypebased structures
[]:
(The inheritance relation ≤ is derived the same way as in S_{a},
.ce is the inverse of .ec.)


(ptb~1) 
O.ce = r.↧.
(The powerclass map .ec
is defined exactly for descendants of r.)

(ptb~2) 
O.ϵ ≤ r.
(Every container is a descendant of r.)

(ptb~3) 
O = O.϶.
(Every object has a container.)

(ptb~4) 
(.ec) ⊆ (ϵ).
(Powerclassof is a special case of containerof .)

(ptb~5) 
(ϵ) ○ (≤) ⊆ (ϵ).
(The subsumption rule.)

(ptb~6) 
(.ce) ○ (≤) ○ (.ec) ⊆ (≤).
(Monotonicity of .ec.)

(ptb~7) 
(<) ∩ (>) = ∅.
(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.

A type can have more than one powertype.

There is no typing relation (instanceof)
between a type and its powertype.
Instead of being an abstraction of a powerset,
Odell's powertype is an abstraction of a nontrivial partition.
As a consequence, the powertype relation corresponds
to a distinquished subrelation of the inverse of
the nonmember 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 antimembership.
The diagram on the right shows a monotonic structure of ϵ
in which
M
and N
are designed
powertypes of A
.
Powertypes as antimembers
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 antimember
.
That is,

y is a powertype of x
↔
y ϵ^{1} x.
Recall that ϶^{1} is an abstraction of
(.ec) ○ (≥).
In powerclass complete structures, x.϶^{1} = x.ec.↧,
i.e.
antimembers of x are exactly the descendants of
the powerclass of x.
Furthemore, the antimembership 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 builtin 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



The diagram only displays a part of the builtin structure.
For the whole structure, see
[] or
[].

Instances of
rdfs:Datatype
are shown according to RDF 1.1 Semantics
[]
which adds
rdf:HTML
and rdf:langString
as 2 new builtin instances of rdfs:Datatype
to the previous 2004 version [].

The structure satisfies all conditions of a monotonic structure of ϵ
except for the minimality of objects from the
the 0th metalevel.
In the example structure, the 0th 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 builtin 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 antimembership.
In the standard eigenclass completion
(as supported by Ruby and even by Smalltalk80),
the c class (named Class
)
is not a descendant of r.ec
and thus not an antimember 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 typeequivalent
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 GonzalezPerez, Brian HendersonSellers,
A powertypebased metamodelling framework,
Software & Systems Modeling 5.1
2006


James J. Odell,
Power Types,
Journal of ObjectOriented Programming 7.2
1994


Bernd Neumayr, Michael Schrefl, Bernhard Thalheim,
Modeling techniques for multilevel 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/objectmembership/


Ondřej Pavlata,
Object Membership – Basic Structure,
2015,
http://www.atalon.cz/om/objectmembership/basic/


Ondřej Pavlata,
Object Membership: The ontological structure,
2012,
http://www.atalon.cz/om/objectmembership/ontology/


World Wide Web Consortium,
OWL 2 RDFBased Semantics,
2009,
http://www.w3.org/TR/owl2rdfbasedsemantics/


World Wide Web Consortium,
RDF Schema,
2004,
http://www.w3.org/TR/rdfschema/


World Wide Web Consortium,
RDF Semantics,
2004,
http://www.w3.org/TR/2004/RECrdfmt20040210/


World Wide Web Consortium,
RDF 1.1 Semantics,
2014,
http://www.w3.org/TR/2014/RECrdf11mt20140225/

Document history
March  12  2015 
The initial release.

License
This work is licensed under a
Creative Commons AttributionNonCommercialShareAlike 3.0 License.