Introduction Principia Data is an algebraic typology of computable data. It embraces a finitist approach and relies on type theory rather than set theory for its construction, while attempting to provide an algebraic foundation for the field of statistics in both the discrete and continuous domains. Most importantly, it is kept as simple as possible. Principia Data is motivated by the realization that some physical measures such as temperatures can be subtracted from each other, but cannot be added to each other. This goes to suggest that the properties of such physical measures cannot be properly modeled with traditional group or field structures that define the subtraction operator in relation to the prior definition of the addition operator. Therefore, Principia Data defines a hierarchy of types for which a descendent type is defined from a parent type by adding a single relation or operation to it. Through such a hierarchy, we make sure to introduce the subtraction operator prior to the addition operator and the division operator prior to the multiplication operator.
Notation: The following… …reads: “Alpha being of type nominal implies that either alpha is equal to zero,or there exists beta of type nominal such that alpha is equal to the successor of beta.”
Definition: Elemental Type The elemental type is defined with an equal equivalence relation denoted . Terms of the type can be denoted using words composed from an arbitrary alphabet (e.g. latin alphabet: ). Variable terms are denoted using lower case greek letters (e.g. ). The equal relation complies to the following laws:
Definition: Nominal Type The nominal type is a type extension of the elemental type defined with a zero (denoted ) initial object and a successor (denoted ) coinductive operator. The successor operator complies to the following laws:
Definition: Zero-Free Type Restriction If is a type defined with a zero term, is its restricted type defined without it.
Theorem: Predecessor Unicity A lexical term other than zero has a unique predecessor: Proof:
Definition: Lexical Type The lexical type is a type extension of the nominal type defined with a before order relation denoted . Successive terms of the type can be denoted using words composed from an arbitrary lexicographic system (e.g. latin alphabet: ). The order relation complies to the following laws: Note: The irreflexivity law is required to distinguish strict and non-strict order relations.
Lemma: Strict Order Transitivity The order relation on lexical terms is transitive: Proof:
Lemma: Strict Order Asymmetry The order relation on lexical terms is asymmetric: Proof:
Theorem: Strict Order Relation The order relation on lexical terms is a strict order relation: Proof: Corollary to the Irreflexivity, Transitivity and Antisymmetry properties.
Lemma: Direct Successor Order A lexical term comes before its successor: Proof:
Lemma: Strict Order Propagation Two ordered lexical terms have similarly ordered direct successors: Proof: Per Successor Order, either Or:
Lemma: Strict Order Positivity Zero comes before any lexical term other than zero: Proof:
Theorem: Strict Total Order Relation The strict order relation on lexical terms is a strict total order relation: Proof: Per Strict Order Positivity, either: . Or: . Or: . Or: .
Definition: Non-Strict Order Relation The strict order relation on lexical terms induces a non-strict order relation .
Lemma: Non-Strict Order Asymmetry The non-strict order relation on lexical terms is asymmetric: Proof:
Lemma: Non-Strict Order Transitivity The non-strict order relation on lexical terms is transitive: Proof:
Lemma: Non-Strict Order Connex Property The non-strict order relation on lexical terms is connex: Proof:
Theorem: Non-Strict Total Order Relation The non-strict order relation on lexical terms is a total order relation: Proof: Corollary to the Asymmetry, Transitivity, and Connex properties.
Definition: Sequential Type The sequential type is a type extension of the lexical type defined with a coinductive predecessor operator (denoted ) inverse of the successor operator. The predecessor operator complies to the following law:
Corollary: Predecessor Unicity A sequential term has a unique predecessor: Proof: Note: this is an extension of the Predecessor Unicity Theorem established for the lexical type.
Theorem: Successor Predecessor Identity Proof:
Theorem: Predecessor Equivalence Proof: Implication: Converse:
Theorem: Predecessor Successor Equivalence Proof: Implication: Converse:
Definition: Ordinal Type The ordinal type is a type extension of the sequential type defined with a subtraction operator minus (denoted ). With the ordinal type, zero can be denoted and terms of the type can be denoted using signed hindu-arabic numerals ( ). The subtraction operator complies to the following laws: The ordinal type allows the following opposite abbreviated notation:
Corollary: Subtraction Anticommutativity The subtraction operation on ordinal terms is anticommutative: Proof:
Corollary: Double Opposite Identity The opposite of the opposite of an ordinal term is equal to the term itself: Proof:
Corollary: Opposite Equality The opposite of the opposite of an ordinal term is equal to the term itself: Proof: Implication: Converse:
Theorem: Subtraction Associative Commutativity Proof:
Theorem: Subtraction Affine Equivalence Proof:
Notation: Ordinal Unit The use of hindu-arabic numerals implies the following notation:
Definition: Cardinal Type The cardinal type is a type extension of the ordinal type defined with an addition operator plus (denoted ). The addition operator complies to the following law:
Corollary: Subtraction Domain The subtraction operator can also be defined on the domain:
Corollary: Subtraction Codomain The subtraction operator defined on the domain can have as codomain:
Theorem: Addition Dual Equivalence Proof: Implication: Conjuct:
Corollary: Addition Identity The identity element for the addition operator is 0: Proof:
Corollary: Addition Dual Substitution Proof:
Theorem: Addition Commutativity The addition operator on cardinal terms is commutative: Proof:
Theorem: Addition Associativity The addition operator on cardinal terms is associative: Proof:
Theorem: Addition Dual Identity Proof: Left Conjunct: Right Conjunct:
Definition: Fractional Type The fractional type is a type extension of the cardinal type defined with a division operator divides (denoted ). The division operator allows the following fractional notation: The division operator complies to the following laws:
Definition: Rational Type The rational type is a type extension of the fractional type defined with a multiplication operator times (denoted ). The multiplication operator complies to the following law:
Definition: Functional Notation The plus, minus, divides, and times operators can be redefined as functions. To do so, we define as functional type and as identity function: Identity: Minus: Plus: Divides: Times: We observe that the pair of divides and times operators are defined exactly the same way as the pair of minus and plus operators, but with different identity elements, and with a minus identity restriction on the multiplier subdomain of the divides function.
Corollary: Arithmetic Properties The symmetry established between the pairs of operators and allows the following pairs of properties to be proven for both elements in every pair by proving it for a single element. Since such proofs were established for the pair, equivalent proofs follow for the pair. The following properties are established for any pair of operator functions , which corresponds to the pairs and . Furthermore, the term reverse is used to refer to the opposite for the pair and to the inverse for the pair. Anticommutativity: Double Reverse Identity: Associative Commutativity: Affine Equivalence: Identity Term: Dual Equivalence: Dual Substitution: Commutativity: Associativity: Dual Identity: