mm-ADT: The Virtual Machine

Every mm-ADT program denotes a single unary function that maps an obj of type \$S\$ (start) to an obj of type \$E\$ (end) with the function signature

\[ f: S \rightarrow E. \]

The complexities of mm-ADT are realized in the definition of an obj (which includes both types and values) and the internal structure of an \$f\$-program (which is a composition of nested curried functions). The sole purpose of this documentation is to make salient the various algebraic structures that are operationalized to ultimately yield the mapping \$f : S \rightarrow E\$.

The base algebra of mm-ADT is a type-oriented ring algebra called the obj stream ring. There are three surjective homomorphisms from the obj stream ring to the algebras of the aforementioned components. The language algebra's free monoid enables the nested, serial composition of parameterized instructions (inst) from the mm-ADT instruction set architecture and is called the inst monoid. The processor algebra is called the type ringoid and it is a free polynomial ringoid (poly) at compilation and non-free ringoid at evaluation. The storage algebra is called the obj monoid and it maintains a carrier set composed of all mm-ADT objects (obj) and an associative, binary operator for constructing data streams.

These component algebras represent the particular perspective that each component has on a shared data structure called the obj graph. This graph has a faithful encoding as a generalized Cayley graph and a commutative diagram. It serves as the medium by which the virtual machine’s computations take place: from specification, to compilation and then evaluation.

The primary purpose of this documentation is to explain these algebras, specify their relationship to one another and demonstrate how they are manipulated by mm-ADT technologies. Data system engineers will learn how to integrate their technology so end users may compose their efforts with others' to create synthetic data systems tailored to a problem’s particular computational requirements.

The mm-ADT VM provides a REPL console for users to evaluate mm-ADT programs written in any mm-ADT language. The reference language distributed with the VM is called mmlang. mmlang is a low-level, functional language that is in near 1-to-1 correspondence with the underlying VM architecture — offering it’s users Turing-Complete expressivity when writing programs and an interactive teaching tool for studying the mm-ADT VM.

A simple console session is presented below, where the parser expects programs written in the language specified left of the > prompt. All the examples contained herein are presented using mmlang.

The context-free grammar for mmlang is presented below. Every mmlang expression denotes an element of the free inst monoid.

The illustration below highlights the two primary components of a type, where an edge of the Cayley graph is the triple \$e=(a,i,b) \in (\tt{type} \times \tt{i\nst} \times \tt{type})\$.

In order to quantify the amount of values denoted by a type, every mm-ADT type has an associated quantifier \$q \in Q\$ written {q} in mmlang, where \$Q\$ is the carrier of an ordered algebraic ring with unity (e.g. integers \$\mathbb{Z}\$, reals in \$ \mathbb{R}, \mathbb{R}^2, \mathbb{R}^3, \ldots, \mathbb{R}^n \$, unitary matrices, etc.).

Typically, integer quantifiers signify "amount." However, other quantifiers such as unitary matrices used in the representation of a quantum wave function, "amount" is a less accurate description as objs interact with constructive and destructive interference. Even in \$\mathbb{Z}\$, negative integers are possible and are leveraged for computing lazy set operations as demonstrated by intersection in the associated example.

The default quantifier ring of the mm-ADT VM is \[ (\mathbb{Z} \times \mathbb{Z}, +, \ast), \] where \$(0,0)\$ is the additive identity and \$(1,1)\$ is the multiplicative identity (unity). The \$ +\$ and \$\ast\$ binary operators perform pairwise integer addition and multiplication, respectively. In mmlang if an obj quantifier is not displayed, then the quantifier is assumed to be the unity of the ring, or {1,1} in this case. Moreover, if a single value is provided, it is assumed to be repeated, where {n} is shorthand for {n,n}. Thus,

\[ \texttt{int} \equiv \texttt{int{1}} \equiv \texttt{int\{1,1\}}. \]

One particular quantifier of every ring serves an important role in mm-ADT as both the additive identity and multiplicative annihilator — {0}. All objs quantified with the respective quantifier ring’s annihilator are non-terminal initial objects as exemplified in the adjoining example.

Quantifiers serve an important role in type inference and determining, at compile time, the expected cost of a particular type definition (i.e., an instruction sequence). The table below itemizes common quantifier patterns that have a corresponding construction in other programming languages.

Types use quantifiers in two separate, but related, contexts: type signatures and type definitions.

A type signature’s domain specifies the type and quantity of the obj required for evaluation. The range denotes what can be expected in return. int{6}<=int{3} states that given 3 ints, the type will return 6 ints. Quantifiers in a type signature are descriptive, used in type checking.

Much will be said about negative quantifiers. For now, note that negative quantifiers enable lazy, stream-based set theoretic operations such as intersection, union, difference, etc. Extending beyond integer quantification \$(\mathbb{Z})\$, negative quantifiers enable constructive and destructive interference in quantum computating \$(\mathbb{C})\$ and excitatory and inhibitory activations in neural computing \$(\mathbb{R})\$.

A type definition’s instructions can be quantified. More specifically, a type’s intermediate dtypes can be quantified. During type inference, the quantifier ring’s \$(+\$/\$\ast)\$-operators propagate the quantifiers through the types that compose the program.

At type compilation, the branch optimizer "collapses" type object equivalent branches with no effect to the result. The branches' type quantifiers are added using the quantifier ring’s \$+\$-operator (the quantifier group). Once collapsed, quantifiers can be moved left-or-right using the quantifier ring’s multiplicative \$\ast\$-operator due to the commutativity of quantifiers theorem (the quantifier monoid). It is more efficient (especially as branches grow in complexity) to compute, for example, \$2b\$ than \$b + b\$. The example below demonstrates how type quantifiers are "collapsed" with \$ +\$ and "slid" left (or right) with \$\ast\$.

The following two examples highlight the fact that type signature quantifiers are used for type checking and type definition quantifiers are used for type inference. The algebra of quantification will be explained in much more detail later when discussing the ring algebra of mm-ADT.

An obj is defined \[ \texttt{obj} = (\texttt{type} \times \texttt{q}) + (\texttt{value} \times \texttt{q}). \] Thus, an obj is either a quantified type or a quantifier value. With respects to the stream ring’s three operators, there are 4 binary obj configurations (\$2^2\$) that each operator will encounter: value/value, value/type, type/value, and type/type. The table below presents the equations of each operator for each of the 4 configurations, where it is through operations involving right-hand side (RHS) types that the instructions in inst are applied to objs (e.g., \$t(v)\$ is evaluation and \$t(t)\$ is compilation). Thus, the stream ring is the fundamental algebra of the mm-ADT VM.

The simple example program below uses all 3 stream ring operators. The subsequent table provides a detailed decomposition of the evaluation. The instruction [model,mmx] loads the mm-ADT extension model that contains common mm base type coercions such as int<=str, real<=int, etc.

The mm-ADT stream ring is the algebraic ring \[ (\texttt{obj},+,\ast,\oplus,\mathbf{0},\mathbf{1}), \]

where

The equation \$\tt{obj} = \tt{type} + \tt{value}\$) and the suggestive illustration above highlight two important uses of the ring’s multiplicative binary \$\ast\$-operator:

Along with the standard ring axioms (save operator closure), the obj stream ring respects the five additional axioms of stream ring theory. The following tables provide a consolidated summary of the ring axioms, stream ring axioms and their realization in mm-ADT via examples in mmlang using both obj values and types.

Axioms are the "hardcoded" equations of a system. Regardless of any other behaviors the system may express, if the system always respects the ring axioms, then the system is (in part) a ring.

The axioms of a theory entail its theorems. Stated in reverse, theorems are the derivations of an axiomatic system. Once a system is determined to be a ring, then all the theorems that have been proved about rings in general are also true for that system.

Stream ring theory studies quantified objects. The quantifiers must be elements of an ordered ring with unity. The stream ring axioms are primarily concerned with quantifier equations and their relationship to efficient stream computing. The most common quantifier ring is integer pairs (denoting a range) with standard pairwise addition and multiplication, \$(\mathbb{Z} \times \mathbb{Z},+,\ast,(0,0),(1,1))\$. However, the theory holds as long as the quantifiers respect the ring axioms and, when coupled to an object, they respect the stream ring axioms.

The type bool<=int[gt,10] has a range of bool and a domain of int. When the type is written without it’s range as int[gt,10], the range is deduced. The int domain ctype is applied to [gt,10] to yield a bool. A type with an unspecified range is called an an anonymous type and is denoted _ in mmlang (or with no character in many situations). An anonymous range is the result of an anonymous domain.

Anonymous types are useful in other situations besides lazy typing expressions.

In general, anonymous types are wildcards because they pattern match to every obj. As will be demonstrated soon, when a variable is specified (e.g. [plus,x]) or a new type is specified (e.g. x:42), The x is a named anonymous type. The entailment of this is that types and variables are in the same namespace. Two presumably self-explanatory examples are provided below with a more detailed discussion of variables and named types forthcoming.

The mm-ADT type system can be partitioned into mono types (monomials) and poly types (polynomials). There are 4 mono types, each denoting a classical primtive data type: bool, int, real, and str. The associated table presents the typical operators (sugared instructions) that can be applied to each mono type. The table also includes their respective additive \$(\mathbf{0})\$ and multiplicative \$(\mathbf{1})\$ identities.

A few of the more interesting aspects of the mono types are detailed in the following subsections.

The instructions [zero] and [one] are constant polymorphic instructions. Each provides a unique singleton value associated with the type of the respective incoming obj. In the example to follow, = is sugar for pairwise [combine], with round robin evaluation for overflow. As examples, (a,b,c)=(x,y) yields (ax,by,cx) and (a,b,c)=(x) is (ax,bx,cx) (i.e.,right scalar multiplication).

Each type’s \$\mathbf{0}\$ and \$\mathbf{1}\$ value serves as the [plus] and [mult] instruction identities, respectively. Furthermore, for types respecting a ring with unity algebra, [zero] is their corresponding multiplicative annihilator.

A poly is a free object. Free objects are universal structures in that they respect the equations of an abstract algebra, but not the equations of an instance of the abstract algebra. Hence the term free as in "free" from constraint of the concrete—​i.e., universal. Examples of these two classes of equations are provided in the table below. If the concrete algebra equations appear random, it is because they are. Each concrete algebra’s operator(s) map elements-to-elements in a manner specific to an application domain and as such, are not universal equations.

In mm-ADT, polys are

The mm-ADT poly is versatile because it is agnostic to the types and values contained therein while remaining in one-to-one correspondence with the stream ring algebra's operators' axioms and entailed theorems. More poetically, poly is the bedrock upon which the mm-ADT algebraic ecology is sustained.

There are type polys and there are value polys. A type poly contains at least one type obj and is typically intended for use as a flow control structure. A value poly is composed of only value objs with a common use as a collection data structure.

As a practical consideration, mm-ADT offers two kinds of poly: lst (list) and rec (record), where theoretically, rec is simply a lst with some added conveniences that make typical programming patterns easier to express. Finally, a poly is associated with one of three algebras that comprise mm-ADT’s stream ring: , (abelian group), ; (monoid), or | (near-ring).

\[ \begin{split} \texttt{poly} &= \texttt{lst} &+ \texttt{rec} \\ \texttt{poly} &= (\texttt{,-lst} + \texttt{|-lst} + \texttt{;-lst}) &+ (\texttt{,-rec} + \texttt{|-rec} + \texttt{;-rec}). \end{split} \]

There are three instructions that are of primary importance for poly with one being a composite of the other two.

The details of these instructions will be discussed in full over the following subsections.

The [to] instruction’s type definition is a<=a[to,_]. The argument to [to] is a named anonymous type. For every incoming \$a \in \tt{obj}\$, there is an outgoing \$a\$ whose path has been extended with the [to] instruction. An example is provided below.

Suppose int is applied to the above anonymous type. This triggers a cascade of events whereby [plus,1] maps int to int[plus,1], then [to,x] maps int[plus,1] to int[plus,1][to,x], and so forth. The resultant compiled int-type can then be evaluated by an int value such as 9. In the commuting diagram below, the top instruction sequence forms a value graph (evaluation), the middle sequence a type graph (compilation), and the bottom, an untyped graph (composition). The union of these graphs via the inclusion morphism ([type]) is the complete obj graph of the computation.

The primary idea concerning variable state is that when [mult,x] is reached by the int value 12 via instruction application, the anonymous type x must be resolved before [mult] can evaluate. To do so, the instruction [to,x] is searched for in the path history of 12. When that instruction is found, the range (or domain as it’s an identity) replaces x and [mult,10] is evaluated and the edge \[12 \rightarrow_{\texttt{[mult,10]}} 120 \] extends the value graph. The intuition for this process is illustrated on the right.

The variable’s scope starts at [to] and ends when there is no longer a path to [to]. If an inst argument is a type (e.g. [mult,[plus,x]]), then the child type ([plus,x]) path extends the parent type ([mult]) path. As such, the child type has access to the variables declared in the parent composition up to the inst containing the child type ([mult]). Finally, if [to,x] is evaluated and later along that path [to,x] is evaluated again, all subsequent types will resolve x at the latter [to,x] instruction. That is, the graph search halts at the first encounter of [to,x] — the shortest path to a declaration.

A type definition takes one of the two familiar forms \[ b⇐a \] or \[ b:a \] where, for the first, \$b\$ is generated by \$a\$ and for the second, \$b\$ is structured as \$a\$ and, when considering no extending instructions to the \$b⇐a\$ form, \$b⇐a \cong b:a\$ such that \$a\$ is named \$b\$. For most of the documentation, the examples have been presented solely from within the mm model-ADT where there are 6 types: bool, int, real, str, lst, and rec along with their respective instructions. It is possible to extend mm with new types that are ultimately grounded (Cayley rooted) in the mm model-ADT types. This is the purpose of the [define] instruction which will now be explained by way of example.

The natural numbers (\$\mathbb{N}\$) are a refinement of the set of integers (\$\mathbb{Z}\$), where \$\mathbb{N} \subset \mathbb{Z}\$. In set builder notation, specifying the set of integers and a predicate to limit the set to only those integers greater than 0 is denoted \[ \mathbb{N} = \{n \in \mathbb{Z} \;|\; n > 0\}. \] In mm-ADT, int is a nat (\$\mathbb{N}\$) if there is a path through the type graph from the int to nat. These paths are type definitions. In the example below, [define] creates a path from at int to nat via the instruction [is>0].

A nat is any int that arrives at nat via nat<=int[is>0]. Given this definition (and this definition only), nat is a refinement of int because only 50% of ints successfully reach nat. However, there may be other paths to nat from other types and as such, type refinement is a relative concept in mm-ADT. In isolation, nat is only a character label (called a name) attached to a vertex in the obj graph. There is no other structure to a isolated type. The nature of a type is completely determined by the paths incoming and outgoing from it. In this graph-based interpretation of types, a type can be the source or target of any number of paths and it is through navigating these paths that values at a type are morphed into values at other types, where mm-ADT instructions (inst) specify, step-by-step, the way in which the morphing process is to be carried out.

The example below defines a date to be a ;-lst with 2 or 3 nats. If the ;-lst contains only 2 terms, then a default value of 2020 is provided. This highlights an important aspect of mm-ADT’s type system. Variables, types, and rewrites are all graph search processes. A defined type (path) with a desired range is searched for in the obj graph and returned if and only if the morphing obj matches the defined type’s domain. Type definitions are simply other types that specify the means by which one type is translated into another type. To the left, the meaning of the arrows' graphical annotations are provided.

Defining types with [define] is useful for in situ definitions that are only require through the scope of the definition (typically within nested types). For reusing types across mm-ADT programs, mm-ADT offers models and the [model] instruction.

Graph theory acknowledges a variety of graph structures. One such structure is the property graph. The more descriptive, yet significantly longer name is the directed, attributed, multi-relational binary graph. The breadth of features will ultimately be captured in pg. The reduced pg_1 model only defines a directed binary graph. In pg_1, a vertex can be derived from a rec with an 'id'->int field. An edge can be derived from a rec with an outgoing/start vertex (outV) and an incoming/end vertex (inV). The associated diagram graphically captures the pg_1 structure, where the . prefixes on the inst morphisms denote the mmlang sugar notation for [get] — e.g., .outV is sugar for [get,'outV'].

Three examples of constructing a vertex are presented below.

Three edge construction examples are presented below.

In the previous pg_1 model, a vertex (edge) was constructed using a rec with the requisite component structure. After validating the structural type of rec, the rec is labeled vertex (edge). There are situations in which the source obj has a significantly different absolute structure than the target obj. The ways in which an obj can be constructed are categorized in the table below where inline is for one time use, define for repeated use in a program, and model for reuse across programs.

An edge can be constructed in a number ways. The constructor below maps an int pair (\$\mathbb{Z} \times \mathbb{Z}\$) to an edge by propagating the pair into the edge product and then constructing vertices for the outV and inV fields. This structure has sufficient information for rendering the final edge. The mm-ADT VM simply names the rec pair elements vertex and the outer rec edge thus completing the transformation of an (int;int) to edge given pg_1.

The final example above demonstrates the use of ;-lst as both a coproduct and a product — i.e., a biproduct. The (vertex;vertex) pair is created via a split -< which serves as the coproduct injections \$\iota_0\$ and \$\iota_1\$. From this vertex coproduct, the edge definition projects out each component of via .0 ([get,0]) and .1 ([get,1]). Thus, the coproduct is also a product. For this reason, the Unicode character for pi (π) (the conventional symbol for product projection) serves as another mmlang sugar for [get].

Branch instructions enable the splitting, composing, and merging of streams. This subset of inst is a particular type of additive category called a traced monoidal category, where [repeat] provides feedback and each instruction’s poly arguments are biproducts maintaining both injective and projective morphisms. There exists a well-established graphical language for such monoidal categories that has been adopted in mmlang sugar syntax (or as best as can be reasonably captured using ASCII characters).