In the following an untyped formulation of Relational Theory is given. This reduces the subject to its essence without irrelevant distractions. This appears to be analogous to untyped versus typed versions of set theory. The untyped set theory is simpler and preferred by most mathematicians.
For example the definition of union compatible relations, or the join operator are very elegant.
There is no suggestion that a practical Data Definition Language or Data Manipulation Language using the RM/RA cannot or should not utilise static type checking, just as typed languages often impose types on sets.
This formulation builds on top of set theory - optionally a pure set theory where every element of a set is a set. Either way, it is assumed that a single equality operator is defined across all objects (i.e. all sets and elements of sets). Furthermore, equality must respect the axiom of extension: two sets are equal if and only if they have the same members. This means we don't have to worry about defining equality on tuples or relations - it comes for free.
Integrity constraints are modelled simply by using a set to specify the legal values of a database.
This formulation has more to do with algebraic systems than physical databases, and therefore there is no mention of the term "variable" in the sense of variables which can be assigned in imperative programming languages.
This treatment is compatible with relation-types, assuming they are formalised as types of untyped-relation-values. There is no need to put attribute types "into" the relation values when they are already available in the static type of a relation-valued expression in a static typed language that denotes an untyped-relation-value. There is no problem recording the extension of a predicate with untyped-relation-values, including when the extension is empty.
Nevertheless this treatment is agnostic to relation-types. Relation-types relate to type systems of programming languages, which is treated as a separate topic for a separation of concerns. By their very nature tuple types and relation types mean discussing parametric polymorphism.
Def: A heading h is a finite function where ∀(a,d)∈h, d is a set.
Note: In pure set theory everything is a set so in that case the requirement that d is a set is vacuous.
Note: For each (a,d)∈h, a is called an attribute and d is called a domain (unfortunately this term is overloaded, and should not be confused with the domain of a set of ordered pairs defined previously). Each element of d is called a value. Therefore a heading is a finite set of (attribute, domain) pairs where the attributes are unique.
Note: We allow for (a,∅)∈h, even though in practise it is not very useful to have an empty domain.
Note: ∅ is a heading.
Note: A tuple is defined independently of a heading. There is no notion of the types of the attributes.
Note: Any heading can be regarded as a tuple! This can be regarded as an "insight" afforded by an untyped theory. Typed theories, by their very nature, tend to create artificial distinctions and restrictions.
Def: The set of tuples that conform to heading h is defined as follows:
Note: This set can be proven to exist from the axioms of set theory. TUPLES(h) is a restricted comprehension over the power set of { (a,v) | (a,d)∈h ∧ v∈d }. The latter can be shown to exist with help from the axiom of union, by rewriting as ∪ { {(a,v) | v∈d} | (a,d)∈h }.
Note: TUPLES(h) is like a Cartesian product over the domains of the given header, using attribute rather than ordinal position to identify values in the tuple.
Note: |TUPLES(h)| = ∏ { |d| | (a,d)∈h } where for any finite set of integers s, ∏s denotes the product of those integers, and ∏∅ = 1.
Note: ∃(a,∅)∈h ⇒ TUPLES(h)=∅.
Note: TUPLES(∅) = {∅}
Note: A heading is not part of a tuple's value and it isn't possible to say that a tuple has a particular heading. Two tuples are equal if and only if they are equal as sets of (attribute,value) pairs.
Note: TTM states that a tuple t that conforms to heading {H} is a set of ordered triples <A,T,v>, obtained from {H} by extending each ordered pair <A,T> to include an arbitrary value v of type T. Therein TTM domain types are by definition part of the tuple's value, and this affects tuple equality.
Note: A relation is defined independently of a heading.
Note: There is no notion of types of the attributes.
Def: Let h be a heading. Then
RELATIONS(h) = powerset(TUPLES(h))
Note: ∀r∈RELATIONS(h), r is a relation.
Note: As for a tuple, it must not be assumed that a relation has a particular heading. Two relations are equal if and only if they are equal as sets of tuples, regardless of any notion of a heading.
Note: TTM states "A relation value r (relation for short) consists of a heading and a body". This means the domain types are regarded as part of the relation value. This raises issues with the meaning of equality on relations when type inheritance is supported.
Note: ∅ is a relation.
Note: ∀h, ∅∈RELATIONS(h). Therefore the set of attributes on the relation ∅ is regarded as undefined
Note: Let r≠∅ be a relation. Then ∃t∈r, and the attributes of r can be defined as dom(t), which is the same ∀t∈r.
Note: RELATIONS(∅) = powerset(TUPLES(∅)) = powerset({∅}) = { ∅, {∅} }
Def: dum=∅ and dee={∅}
Note: The set of attributes of dum is undefined. The set of attributes of dee is ∅.
Note: We differ from TTM which states: "TABLE_DUM is the unique relation with no attributes and no tuples at all".
Note: A relation can be used to define the possible values of a tuple. Therefore a relation can serve the purpose of a tuple-type.
Note: A database value is a tuple with relation-valued-attributes (RVAs).
Note: A set of relations, typically a subset of RELATIONS(h) for some heading h, can serve the purpose of a relation-type.
Def: A database heading h is a heading where each domain is of the form RELATIONS(h') for some h'. i.e. ∀(a,d) ∈ h, ∃ heading h', d = RELATIONS(h')
Def: The possible values of a database with database heading h is represented by some r∈RELATIONS(h).
Note: A database value is a tuple with relation-valued-attributes (RVAs). A relation takes care of formalising integrity constraints on the database!