The value notion is a primitive notion.
A value can be a number in mathematical sense (integer or rationale), a flag, a character, an identifier, a tuple of values, etc.
A data object is either an n-tuple of bits or an n-tuple of data objects.
A binary size of one bit is 1.
A binary size of a data object is the sum of the binary sizes of each element of that data object tuple.
(0-tuple, maybe)
A 0-tuple of data objects is nothing, that is, a pseudo data object that does not occupy a position in a tuple. A tuple with elements of nothing is equal to the tuple where this elements are removed.A 1-tuple of a data object is equal to that data object.
A single-cell is a data object that is an N-tuple of bits, where N is the implementation defined number of bits in a cell.
A cell-pair is a data object that is an ordered pair of two single-cells, that is a 2-tuple of single-cells.
A typed data object is
- either an ordered pair of:
- a data object (the first element),
- a set of primitive data types (the second element);
- or a tuple of typed data objects.
(editorial: re the second element, m.b. a set of any data types)
A 1-tuple of a typed data object is equal to that typed data object.
Two typed data objects are identical if and only if every of the following propositions holds:
- they are tuples of the same size,
- for every position the elements are identical.
TODO: how a typed data object is placed on the stack, so only the data object (i.e., the first element) is accessible to the program.
TODO: a formalization for memory addresses ( addr ), execution tokens ( xt ), character strings ( c-addr u ).
E.g., a possible address vs a valid address or address unit (that is in data space).
A data type symbol is an identifier for a data type.
A data type is one from the following:
- a primitive data type;
- a subset of a data type members;
- a product data type;
- a union of data types.
A data type determines some abstract set of typed data objects. So, the operations of the union, intersect, relative complement (difference), Cartesian product on data types are mapped to the operations on the sets.
A primitive data type is a triplet of:
- a set of data objects of the same binary size (the first element),
- a set of values (the second element),
- a total surjective mapping from the set of data objects to the set of values (the third element).
A member of a primitive data type is a typed data object such that:
- the first element of that typed data object is a member of the first element of that primitive data type,
- the second element of that typed data object contains that primitive data type as a member.
Thus, although a primitive data type is not a set of typed data objects, it determines a set of typed data objects.
A typed data object is incorrect if it's not a member of a primitive data type that is a member of the second element of that typed data object.
Data type: unspecified cell; data type symbol: x;
- data objects: any single-cell;
- values: N-tuples of bits; the first bit in a tuple is the least significant bit.
- mapping: one to one.
Data type: singed number; data type symbol: n;
- data objects: any single-cell;
- values: the integers in the range { −(2^(N−1)), ..., (2^(N−1) − 1) } ;
- mapping: according to the two's complement format.
Data type: boolean cell; data type symbol: bool;
- data objects: any single-cell;
- values: zero, nonzero;
- mapping: zero if all bits are 0, otherwise nonzero.
Every word that accepts a bool, also accepts an x, and vise versa. It means, these data types are equal, and one of them is excessive. See also Liskov substitution principle.
The empty type is the 0-tuple of data types. There are no members of this data type.
(Sometimes the empty type is denoted with ⊥.)
A product data type is an n-tuple of data types. A member of a product type is a tuple of typed data objects.
A 0-tuple of a data type is the empty type.
A 1-tuple of a data type is equal to that data type.
An n-tuple of data types, where n is an integer grater than 1, is the n-ary Cartesian product of n sets (possibly with repetitions) of that data types members.
If some data type in a product is the empty type, that product data type is the empty type.
A product data type is denoted as a tuple of data types symbols, e.g. ( x x n ).
"Unspecified cell pair" ( xd ) and "double-cell signed number" ( d )
are product types that are primitive data types.
"Character strings" ( c-addr u ) is a product type that is not a primitive data type.
The union of a set of data types is the set of all members of these data types.
The union of an mepty set of data types is the empty type.
The union of a set of one data type is equal to that data type.
The union of two data types T1 and T2 is the union of T1 and T2 members, and it is denoted as T1|T2.
A typed data object is a member of a union if and only if it is a member of at least one data type in that union.
A union of data types is also known as a sum type.
The difference of two data types is a set of all and only members of the first data type that are not members of the second data type.
The difference of the data types T1 and T2 is denoted as T1\T2.
The subtype relation is a binary transitive relation on data types. It is denoted with symbol ⇒.
If and only if a data type T2 is a subtype of a data type T1, that is, T2 ⇒ T1, then every member of T2 is also a member of T1.
A data type T1 is a supertype of a data type T2 if and only if T2 is a subtype of T1, that is, T2 ⇒ T1.
A data type T2 is a direct subtype of a data type T1 if and only if T2 is a subtype of T1 only by the definition for the data type T2.
The singed number data type is a subtype of the unspecified cell data type, that is, n ⇒ x, where n and x are the symbols of the corresponding data types.