Is there a theory/abstraction behind OOP?

Question

Functional programming has the very elegant Lambda Calculus and its variants as a backup theory. Is there such a thing for OOP? What is an abstraction for the object oriented model?

Answer 1

There are four main approaches, though these only scratch the surface of what is available:

• via lambdas and records: the idea is to encode objects, classes and methods in terms of more traditional constructs. Benjamin Pierce's work from the mid 90s is representative of this approach.
• Abadi and Cardelli's object calculi (see Abadi and Cardelli's book A Theory of Objects: their main abstraction is a record of methods, and the approach is closer to the prototype-based realisation of object-oriented programming, though classes and inheritance can be encoded in terms of the more primitive elements.
• Castagna's multimethod calculus (see Castagna's book Object-Oriented Programming A Unified Foundation): his approach takes multimethods are the key abstraction.
• Class-based calculi (such as in Kim Bruce's book Foundations of Object-oriented Languages: Types and Semantics or Featherweight Java): these approaches aim to capture the essence of class based programming and focus on classes and inheritance.

Answer 2

The connection between object model core and set theory is described in the following documents:

• Object Membership: The Core Structure of Object Technology
• Object Membership – Basic Structure
• What Is a Metaclass?

The documents present the structure of instance and inheritance relations between objects. Such a structure can be considered the highest possible abstraction of OOP. It is shown how the structure applies to particular programming languages (Ruby, Python, Java, Scala, Smalltalk-80, Objective-C, CLOS, Perl, Dylan, JavaScript) and also to ontology languages (RDF Schema and OWL 2 Full).

In the documents, the classes are objects approach is taken so that the core structure is single-sorted. In the main form, the structure can be expressed as (O, ϵ, ≤, .ec) where

• O is the set of objects,
• ϵ is the (object) membership relation, a refinement of the instance-of relation,
• ≤ is the inheritance relation, and
• .ec is the powerclass map which is a distinguished, possibly empty, subrelation of ϵ.

A sample core structure according to the Ruby object model is shown by the following diagram. Green links show the inheritance relation in the reflexive transitive reduction, blue links show the membership relation in the "subsumption reduction" – a blue link from x points to the least container of x. The powerclass map .ec is formed by horizontal blue links. Objects from the image of this map are powerclasses (in gray). In Ruby they are called eigenclasses or also singleton classes (the latter term being rather deprecated). Objects s, u and v (in pink) are terminal, the remaining objects are descendants of the inheritance root r.

  r = BasicObject; c = Class; A = c.new(r); B = c.new(A); s = A.new; u = B.new; v = B.new; class << s; end; class << v; end

Core parts of the object model of all the above languages can be seen as specializations of the structure, with no or just a few additional constituents. From the theoretical point of view, the most significant case of an additional constituent is the singleton map (denoted .ɛϲ) introduced by Dylan. This makes Dylan the only programming language (from the above mentioned) thas is not subject to the monotonicity condition (≤) ○ (ϵ) ⊆ (ϵ) where the composition symbol ○ is interpreted left-to-right.

One way to formalize the connection between object model core and set theory is via the family of structures (O, ≤, r, .ec, .ɛϲ) called metaobject structures in the referenced documents since x.ec or x.ɛϲ can be considered as metaobjects of x. In these structures x.ec is defined for every object x and x.ɛϲ is defined for every bounded ("small") object x. The structures are subject to the nine axioms below. The axiomatization uses a definitional extension which is quite simple for the first eight axioms (T denotes the set of terminal objects – those which are not descendants of r, and .ec^∗ is the reflexive transitive closure of .ec) but rather involved for the last axiom.

1. Inheritance, ≤, is a partial order.
2. The powerclass map, .ec, is an order-embedding of (O, ≤) into itself.
3. Objects from T.ec^∗ are minimal.
4. Every powerclass is a descendant of r.
5. The set r.ec^∗ has no lower bound.
6. The singleton map, .ɛϲ, is injective.
7. Objects from O.ɛϲ.ec^∗ are minimal.
8. For every objects x, y such that x.ɛϲ is defined, x.ɛϲ ≤ y.ec ↔ x ≤ y.
9. For every object x, x.ɛϲ is defined ↔ x.d < ϖ.

In the last axiom, ϖ is a fixed limit ordinal, and .d is the rank function derived by the definitional extension. The object membership relation, ϵ, is obtained as ((.ɛϲ) ∪ (.ec)) ○ (≤). According to the last axiom, the domain-restriction of ϵ to the set of bounded objects equals (.ɛϲ) ○ (≤). In the referenced documents, this relation is called bounded membership and denoted ∊. As a significant characteristics, this relation is well-founded. This is in contrast to ϵ which is non-well-founded since r ϵ r. It turns out that the main correspondence between (the core part of) object technology and set theory can be expressed as

∊ ↔ ∈

i.e. bounded membership corresponds to set membership between well-founded sets. As a special case, the partial von Neumann universe of rank ϖ+1 is a metaobject structure by definitional extension. In general, every abstract (ϖ+1)-superstructure (O,∊) is definitionally equivalent to a complete metaobject structure. Every metaobject structure can be faithfully embedded into a complete metaobject structure which in turn can be faithfully embedded into the von Neumann universe.

The term basic structure is used for a generalization of metaobject structures. In this generalization, .ec and .ɛϲ are allowed to be (arbitrarily) partial, possibly empty. In particular, finite basic structures are possible, with the minimum structure containing just the inheritance root r. Every basic structure can be extended to a metaobject structure by a powerclass completion followed by a singleton completion which in turn makes basic structures faithfully embeddable into the von Neumann universe.