mm-ADT is a dual licensed AGPL3/commercial open source project that offers software engineers, computer scientists, mathematicians, and others in the software industry a royalty-based OSS model. The Turing Complete mm-ADT virtual machine (VM) integrates disparate data technologies via algebraic composition, yielding synthetic data systems that have the requisite computational power and expressivity for the problems they were designed to solve. As an economic model, each integration point offers the respective development team access to the revenue streams generated by any for-profit organization leveraging mm-ADT.

## Virtual Machine Components

The mm-ADT VM integrates the following data processing technologies:

• Programming Languages: Language designers can create custom languages or develop parsers for existing languages that compile to mm-ADT VM assembly code (`mmlang`) or bytecode (binary encoding of `mmlang`).

• Processing Engines: Processor developers can enable their push- or pull-based execution engines to be programmed by any mm-ADT language. The abstract processing model supports single-machine, multi-threaded, agent-based, distributed near-time, and/or cluster-oriented, batch-analytic processors.

• Storage Systems: Storage engineers can expose their systems via model-ADTs expressed in mm-ADT’s dependent type system that enable the lossless encoding of key/value store, document store, wide-column store, graph store, relational store, and other novel or hybrid structures such as hypergraph, docu-graph, and quantum data structures.

The mm-ADT VM enables the intermingling of any language, any processor, and any storage system that can faithfully implement the core language semantics (types and values), processor semantics (instruction set architecture), and/or storage semantics (data structure streams).

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.

There are two operations: addition ( +) and multiplication (\ast). Abstract algebra is the study of these two operations across a wide range of slightly different generalized structures devoid of considerations regarding the particulars of their implementation: integers, digital circuits, quantum systems in a superposition, etc. Theoreticians deduce theorems based on the axioms of the structures and experimentalists apply the structural patterns to other systems, real or designed.

The pedagogical masterpiece of the discipline is the magma hiearchy.

1. Magma (A,\ast): a set A with a potentially associative binary operator ast: A \times A \to A.

2. Semigroup (A,\ast): a magma with an associative binary operator (a \ast b) \ast c = a \ast (b \ast c).

3. Monoid (A,\ast,\mathbf{1}): a semigroup with an identity element such that a \ast \mathbf{1} = a = \mathbf{1} \ast a.

4. Group (A,\ast,\mathbf{1}): a monoid with ever element having an inverse such that a \ast a^{-1} = \mathbf{1} = a^{-1} \ast a.

5. Ring (A,+,\ast,\mathbf{0},\mathbf{1}): a  +-group and a \ast-monoid bound by distributivity, a \ast (b + c) = (a \ast b) + (a \ast c).

6. Field (A,+,\ast,\mathbf{0},\mathbf{1}): a ring where the \ast-monoid is a \ast-group.

Numerous enrichments to these structures blur the sharp lines that divide them.

• Abelian a \cdot b=b \cdot a: the binary operator is agnostic to the order of the arguments.

• Idempotent a \cdot a = a: the binary operator reaches a fixpoint on self compositions.

• Free A^\ast: the binary operator is replaced with concatenation to record operation sequences, not evaluate them.

• Module A[x]: a binary magma that respects the abstract form of linear algebra via scalars and vectors.

• Polynomial x_1a + x_2a^2 + \ldots + x_na^n: a binary magma with free addition and non-free multiplication.

• …​

No one practitioner will ever have a complete grasp of the intricacies that bind  + and \ast together over A.

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.

Component Algebra

language

`inst` monoid

processor

`type` ringoid

storage

`obj` monoid

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.

``````~/mm-adt bin/mmadt.sh
_____ _______
/\  |  __ |__   __|
_ __ ___  _ __ ___ _____ /  \ | |  | | | |
| '_ ` _ \| '_ ` _ |_____/ /\ \| |  | | | |
| | | | | | | | | | |   / ____ \ |__| | | |
|_| |_| |_|_| |_| |_|  /_/    \_\____/  |_|
mmlang>``````

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`.

``````mmlang> 1
==>1
mmlang> 1+2
==>3
mmlang> 1[plus,2]
==>3``````

#### mmlang Syntax and Semantics

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

``````obj   ::= (type | value)q
value ::= vbool | vint | vreal | vstr
vbool ::= 'true' | 'false'
vint  ::= [1-9][0-9]*
vreal ::= [0-9]+'.'[0-9]*
vstr  ::= "'" [a-zA-Z]* "'"
type  ::= ctype | dtype
ctype ::= 'bool' | 'int'  | 'real' | 'str' | poly | '_'
poly  ::= lst | rec | inst
q     ::= '{' int (',' int)? '}'
dtype ::= ctype q? ('<=' ctype q?)? inst*
sep   ::= ';' | ',' | '|'
lst   ::= '(' obj (sep obj)* ')' q?
rec   ::= '(' obj '->' obj (sep obj '->' obj)* ')' q?
inst  ::= '[' op(','obj)* ']' q?
op    ::= 'a' | 'add' | 'and' | 'as' | 'combine' | 'count' | 'eq' | 'error' |
'explain' | 'fold' | 'from' | 'get' | 'given' | 'groupCount' | 'gt' |
'gte' | 'head' | 'id' | 'is' | 'last' | 'lt' | 'lte' | 'map' | 'merge' |
'mult' | 'neg' | 'noop' | 'one' | 'or' | 'path' | 'plus' | 'pow' | 'put' |
'q' | 'repeat' |'split' | 'start' | 'tail' | 'to' | 'trace' | 'type' | 'zero'``````

## The Type

Products and Coproducts

Category theory is the study of structure via morphisms that expose (or generate) other structures. Two important category theoretic concepts dealing with substructures are products and coproducts.

A product is any object defined in terms of it’s accessible component objects. That is, from a single object, via \pi_n projection morphisms, the product is decomposed into it’s constituent parts.

A coproduct is any object defined in terms of the component objects used to construct it. That is, from many objects, via \iota_n injection morphisms, a coproduct can be composed from constituent parts.

Along with these decomposition (and composition) morphisms, there exists an isomorphism between any two products (or coproducts) should they project (or inject) to the same component objects. That is, product and coproduct equality are defined via component equality.

### Types and Values

Everything that can be denoted in `mmlang` is an `obj`. Within the VM and outside the referential purview of an interfacing language, every `obj` is the product of

1. an object that is either a type object or a value object and

2. a quantifier specifying the "amount" of objects being denoted.

$\begin{split} \text{ } \\ \texttt{obj} &= \texttt{object} &\;\times\; \texttt{q} \text{ } \\ \texttt{obj} &= (\texttt{type object} + \texttt{value object}) &\;\times\; \texttt{q}. \end{split}$

This internal structure is well-defined as an algebraic ring. The ring axioms specify how the internals of an `obj` are related via two binary operators: \times and \+ . One particular axiom states that products both left and right distribute over coproducts. Thus, the previous formula is equivalent to

$\texttt{obj} = (\texttt{type object} \times \texttt{q}) + (\texttt{value object} \times \texttt{q}).$

There are two distinct kinds of mm-ADT `objs`: quantified type objects and quantified value objects. These products of the `obj` coproduct are called by simpler names: type and value. That is the obj meta-model.

$\texttt{obj} = \texttt{type} + \texttt{value}$

 There are only a few instances in which it is necessary to consider the object component of an `obj` separate from its quantifier component. The terms type and value will always refer to the object/quantifier-pair as a whole — i.e., an `obj`.
``````mmlang> int              (1)
==>int
mmlang> 1                (2)
==>1
mmlang> int{5}           (3)
==>int{5}
mmlang> 1{5}             (4)
==>1{5}
mmlang> ['a','b','a']    (5)
==>'b'
==>'a'{2}``````
 1 A single `int` type. 2 A single `int` value of `1`. 3 Five `int` types. 4 Five `1` `int` values. 5 A `str` stream composed of `'a'`,`'b'`, and `'a'` (definition forthcoming).

Both types and values can be operated on by types, where each is predominately the focus of either compilation (types) or evaluation (values).

``````mmlang> int => int[is,[gt,0]]                   (1)
==>int{?}<=int[is,bool<=int[gt,0]]
mmlang> 5 => int{?}<=int[is,bool<=int[gt,0]]    (2)
==>5``````
 1 Compilation: The `int`-type is applied to the `int[is,[gt,0]]`-type to yield a maybe `int{?}`-type. 2 Evaluation: The nested `bool<=int[gt,0]`-type is a lamba function yielding `true` or `false`.

Some interesting conceptual blurs arise from the intermixing of types and values. The particulars of the ideas in the table below will be discussed over the course of the documentation.

Table 1. Consequences of Type/Value Integration
structure A structure B unification

type

program

a program is a "complicated" type.

compilation

evaluation

compilations are type evaluations, where a compilation error is a "type runtime" error.

type

variable

types refer to values across contexts and variables refer to values within a context.

type

AST

a single intermediate representation is used in compilation, optimization, and evaluation.

type

function

functions are (dependent) types with values generated at evaluation.

state

trace

types and values both encode state information in their process traces.

classical

quantum

quantum computing is classical computing with a unitary matrix quantifier ring.

### Type Structure

Cayley Graphs

A Cayley graph is a graphical encoding of a group. If (A, \cdot, I) is a group with carrier set A, binary operator \cdot : (A \times A) \to A, and generating set I \subseteq A then the graph G = (V,E) with vertices V = A and labeled edges E = A \times I \times A is the Cayley graph of the group. The directed edge (a,i,b) \in E written a \to_i b states that the vertices a,b \in A are connected by an edge labeled with the element i \in I. Thus, a \to_i b captures the group operation a \cdot i = b.

When constructed in full, a Cayley graph’s vertices are the group elements and its edges represent the set of all possible I-transitions between elements. When lazily constructed, a Cayley graph encodes the history of a group computation, where the current element has an incoming I-edge from the previous element. A Cayley graph captures both the proto-free and non-free aspects of a group. The non-free aspect is realized by any edge e = (a,i,b) such that ai \mapsto b and an element of the corresponding free algebra (A^\ast,\ast) can be constructed by concatenating the edge labels of a path \prod_{e \in (a,i,b)^\ast} \pi_1(e).

A generalized Cayley graph does not require that every i \in I have a corresponding i^{-1} \in I such that i \cdot i^{-1} = \mathbf{1} (i.e., multiplicative inverses). By lifting this constraint, the Cayley graphical structure can be used to encode other magmas such as monoids and semigroups.

An `obj` is either a type or a value: $\texttt{obj} = \texttt{type} + \texttt{value}.$

That equation is not an axiom, but a theorem. Its truth can be deduced from the equations of the full axiomatization of `obj`. In particular, for types, they are defined relative to other types. Types are a coproduct of either a

1. canonical type (ctype): a base/fundamental type, or a

2. derived type (dtype): a product of a type and an instruction (`inst`).

The ctypes are nominal types. There are five ctypes:

1. bool: denotes the set of booleans —  \mathbb{B} .

2. int: denotes the set of integers —  \mathbb{Z} .

3. real: denotes the set of reals —  \mathbb{R} .

4. str: denotes the set of character strings —  \Sigma^\ast .

5. poly: denotes the set of free objects —  \tt{obj}^\ast .

The dtypes are structural types whose recursive definition's base case is a ctype realized via a chain of instructions (`inst`) that operate on types to yield types. In other words, instructions are the generating set of a type monoid. Formally, the type coproduct is defined as

$\begin{split} \texttt{type} &=\;& (\texttt{bool} + \texttt{int} + \texttt{real} + \texttt{str} + \texttt{poly}) + (\texttt{type} \times \texttt{inst}) \\ \texttt{type} &=\;& \texttt{ctype} + (\texttt{type} \times \texttt{inst}) \\ \texttt{type} &=\;& \texttt{ctype} + \texttt{dtype}. \end{split}$

 Every `obj` has an associated quantifier. When the typographical representation of an `obj` lacks an associated quantifier, the quantifier is unity. For instance, the `real` `1.35{1}` is written more economically as `1.35`.

A dtype has two product projections. The type projection denotes the domain and the instruction projection denotes the function, where the type product as a whole, relative to the aforementioned component projections, is the range. $\begin{split} \tt{type} &=\;& (\tt{type} &\;\times\;& \tt{inst}) &\;+\;& \tt{ctype} \\ \text{“range} &=\;& (\text{domain} &\;\text{and}\;& \text{function}) &\;\text{or}\;& \text{base"} \end{split}$

The implication of the dtype product is that mm-ADT types are generated inductively by applying instructions from the mm-ADT VM’s instruction set architecture (`inst`). The application of an `inst` to a type (ctype or dtype) yields a dtype that is a structural expansion of the previous type.

For example, `int` is a ctype. When `int` is applied to the instruction `[is>0]`, the dtype `int{?}<=int[is>0]` is formed, where `[is>0]` is syntactic sugar for `[is,[gt,0]]`. This dtype is a refinement type that restricts `int` to only those `int` values greater than zero — i.e., a natural number \mathbb{N}^+. In terms of the "range = domain and function" reading, when an `int` (domain) is applied to `[is>0]` (function), the result is either an `int` greater than zero or no `int` at all `{?}` (range).

The diagram above captures a fundamental structure in mm-ADT called the obj graph. The `obj` graph is used for, amongst other things, type checking, type inference, compiler optimization, and garbage collection. The subgraph concerned with type definitions is called the type graph. The subgraph encoding values and their relations as a function of the types is called the value graph. The `obj` graph is also the codomain of an embedding whose domain is an `obj` ringoid called the stream ring. Both the `obj` graph and stream ring form the primary topics of study in this documentation.

The `obj` meta-model structure thus far is diagrammed on the right (with quantifiers attached to each component). On the left are some example `mmlang` expressions.

``````mmlang> int                                                         (1)
==>int
mmlang> int{2}                                                      (2)
==>int{2}
mmlang> int{2}[is>0]                                                (3)
==>int{0,2}<=int{2}[is,bool{2}<=int{2}[gt,0]]
mmlang> int{2}[is>0][plus,[neg]]                                    (4)
==>int{0,2}<=int{2}[is,bool{2}<=int{2}[gt,0]][plus,int{0,2}[neg]]
mmlang> 5{2} => int{2}[is>0][plus,[neg]]                            (5)
==>0{2}``````
 1 A ctype denoting a single integer. 2 A ctype denoting two integers. 3 A dtype denoting zero, one, or two integers greater than 0. 4 A dtype extending the previous type with negative integer addition. 5 A value of two fives applied to the previous type with the result being two 0s.

#### Type Components

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}).

1. Type signature: the ctype specification of a type’s domain and range.

2. Type definition: a domain rooted instruction sequence terminating at the range.

 An image referred to as a diagram or commuting diagram is isomorphic to the system of equations it captures and thus, respects the axioms of the algebraic structure being diagrammed. An image referred to as an illustration is intended to elicit a realization of the associated topic via intuition and should not be considered a faithful encoding of an underlying mathematics.
##### Type Signature

Every mm-ADT type can be generally understood as a function that maps an `obj` of one type to an `obj` of another type. A type signature specifies the source and target of this mapping, where the domain is the source type, and the range is the target type. In `mmlang` a type signature has the following general form where `{q}` is the ctype’s associated quantifier.

 ``range{q}<=domain{q}``
 In common mathematical vernacular, if the function f has a domain of X and a range (codomain) of Y, then its signature is denoted f: X \to Y. Furthermore, with quantifiers in Q, the function signature would be denoted f: X \times Q \to Y \times Q or f: (X \times Q) \to (Y \times Q).
mmlang Expression Description
``````mmlang> int<=int
==>int``````

From the perspective of "type-as-function," An mm-ADT `int` is a no-op on the set of integers. Given any integer, `int` returns that integer. In `mmlang`, when the domain and range are the same, the `<=` and repeated type are not displayed. That is `int<=int` is more concisely displayed as `int`.

``````mmlang> int{1}
==>int
mmlang> int
==>int``````

In most programming languages, a value can be typed `int` as in

`val x:int = 10`.

Such declarations state that the value referred to by `x` is a single element within the set of integers. The concept of a "single element" is captured in mm-ADT by the `obj` quantifier, where a unit quantifier is not displayed in `mmlang`. That is, `int{1}` is more concisely displayed as `int`.

``````mmlang> int{5}
==>int{5}``````

`int{5}` is a type referring to 5 integers. As a point of comparison, `int{1}` refers to a single integer with a syntax sugar of `int` in `mmlang`.

``````mmlang> int{0,5}
==>int{0,5}
mmlang> int{0,5}<=int{0,5}
==>int{0,5}``````

Quantifiers must be elements from a ring with unity. In the previous examples, the quantifier ring was (\mathbb{Z}, +,\ast). In this example, the quantifier ring is (\mathbb{Z} \times \mathbb{Z}, +,\ast), where the carrier set is the set of all pairs of integers and addition and multiplication operate pairwise, $(a,b) \ast (c,d) \mapsto (a \ast c,b \ast d).$ The type `int{0,5}` denotes the inclusive range of 0, 1, 2, 3, 4, or 5 integers. In practice, the (\mathbb{Z} \times \mathbb{Z}) quantifier ring represents uncertainty as to the number of elements being referred to.

``````mmlang> int<=bool
==>int<=bool
mmlang> true => int<=bool
language error: true is not an int``````

Types that are fully specified by their type signature are canonical types (ctypes). Therefore, `bool<=int` is meaningless as there are no instructions to map an `int` to a `bool`. This example is in the `mm` model-ADT, where given another model, it is possible for `bool<=int` to yield a result.

##### Type Definition
Commuting Diagrams

Category theory is a branch of abstract algebra that studies, among other things, arbitrary algebraic structures via their homomorphic embedding in a multi-sorted monoid called a category. A category \mathcal{C} is denoted $(\mathbf{C} ,\circ ,\mathbf{1}),$ where \mathbf{C} is a set-family of morphisms, \circ: \mathbf{C} \times \mathbf{C} \rightarrow \mathbf{C} is an associative binary morphism composition operator, and for every identity morphism \mathbf{1}_A \in \mathbf{1}, \mathbf{1}_A \circ \mathbf{1}_A = \mathbf{1}_A denotes an object that is more simply written A such that A \mapsto \mathbf{1}_A. The family set mathbf{C} indexes hom-sets with \mathbf{C}(A,B) denoting all morphism between objects A and B, where f:A\to B \in \mathbf{C}(A,B) and id: A \rightarrow A \cong \mathbf{1}_A \cong A.

Unlike classical monoids, a category’s \circ operator is generally not closed. That is, there are compositions which may not be defined. It is this aspect of a category that makes it a multi-sorted (or typed) monoid.

The discipline of category theory makes extensive use of a homomorphism from a category to a directed labeled graph called a diagram. These diagrams realize the same underlying unitary operation of the generators of a magma within a generalized Cayley graph. If f:A \to B and g: B \to C, then there exists the morphism path $A \xrightarrow{f} B \xrightarrow{g} C,$ which, in Cayley graph notation, is denoted A \to_f B \to_g C. An important subset of diagrams are the commutative diagrams. In a commutative diagram every morphism path starting at the same source and ending at the same destination are considered equivalent (with respects to equivalence in the respective algebraic structure being modeled categorically). Thus, if g \circ f = i \circ h, then it is said that the above diagram commutes.

Types and values both have a ground that exists outside of the mm-ADT virtual machine within the hosting environment (e.g. the JVM). The ground of the mm-ADT value `2` is the JVM primitive `2L` (a Java `long`). The ground of the mm-ADT type `int` is the JVM class `java.lang.Long`. When the instruction `[plus,4]` is applied to the mm-ADT `int` value `2`, a new mm-ADT `int` value is created whose ground is the JVM value `6L`. When `[plus,4]` is applied to the mm-ADT `int` type, a new type is created with the same `java.lang.Long` ground. Thus, the information that distinguishes `int` from `int[plus,4]` is in the reference to the instruction that was applied to `int`.

For a type, the deterministic chain of references is called the type definition and is encoded as a path in the type graph. For a value, the value graph encodes an analogous path called the value history (or mutation history). Both types and values exist in a larger graph called an obj graph such that $G_{\texttt{obj}} = G_{\texttt{type}} \cup G_{\texttt{value}}.$ The commutative diagram below also represents the corresponding `obj` graph that is composed of two lateral paths. The top path is a value history (2 \to 6 \to 6) and the bottom path is a type definition $(\tt{int} \to \tt{int[plus,4]} \to \tt{int[plus,4][is>0]}).$ These paths are joined by the `[type]` instruction in `inst` and serves to unite the type graph and value graph subgraphs of the `obj` graph such that $\texttt{[type]}: \texttt{obj} \to \texttt{type}.$

 In practice, the string representation of a value is its ground and the string representation of a type is its path.
 ``````mmlang> 2[plus,4][is>0] ==>6 mmlang> 2[plus,4][is>0][path] ==>(2;[plus,4];6;[is,true];6) <=2[plus,4][is,true][path,(_;_)] mmlang> 2[plus,4][is>0][type] ==>int{?}<=int[plus,4][is,bool<=int[gt,0]]``````

In theory, the complete history of an mm-ADT program (from compilation to execution) is stored in the `obj` graph. However, in practice, the mm-ADT VM removes paths once they are no longer required by the program. This process is called path retraction and is the mm-ADT equivalent of garbage collection.

 In the diagram above, the type vertices are elements of a free algebra called the `inst` monoid best understood as a syntactic monoid. In order to present more complex diagrams, vertex labels will be shortened to the type’s canonical range type. With this convention, there is no loss of information. The full definition can be unambiguously determined by concatenating the instructions encountered on the edges of the inverted path from the current range vertex to the root domain vertex (i.e. the base canonical type of the type induction). Furthermore, hook-tailed arrows will replace `[type]`-labeled arrows as they denote a monomorphic embedding known simply as an inclusion. All subsequent diagrams will follow this convention.
Deep Dive 1. The Obj Graph as a Cayley Graph and a Commutative Diagram

The `obj` graph is both a generalized Cayley graph of a partial monoid and the commutative diagram of a free category. More generally, the `obj` graph is the graph of unary functions comprising `inst`, where instructions operate on both types and values. From compilation to evaluation, depending on the particular context, either interpretation will be leveraged.

• Commutative diagram: vertices denote type/value-objects of the `obj` category with `inst` morphisms.

The `obj` graph’s commuting property eases compile-time and runtime type rewriting. If two paths have the same source vertex (domain) and target vertex (range), then both paths yield the same result (the target vertex). In practice, evaluating the instructions along the computationally cheaper path is prudent.

• Cayley graph: vertices denote type/value-elements of the `inst` monoid with generating edges in `inst`.

As a generalized, multi-rooted monoidal Cayley graph, the set of all possible mm-ADT computations is theoretically predetermined given the monoid presentation containing the root `objs` (e.g. the ctypes), its generators (`inst`), and relations (path equations). This static immutable structure serves to memoize computational results. This is especially useful when considering streams (definition forthcoming) and their role in data-intensive, cluster-oriented environments where storage is cheap and processors are costly.

##### Type Quantification
Initial and Terminal Objects

A category may have an initial and/or terminal object.

An initial object S is the domain of a set of morphism S \rightarrow E_n. Initial objects, via their morphisms, generate all the objects of the category. If there is an initial object, then it is unique in that if there is another initial object, it has the same diagrammatic topology — all outgoing morphisms and no incoming morphisms save the identity. Thus, besides labels, two initials are isomorphic.

A terminal object E is the range of a set of morphisms S_n \rightarrow E. Terminal objects subsume all other objects in the category in that all other objects S_n can be morphed into the terminal object, but the terminal object can not be morphed into any other object. Similar to initials, should another terminal exist, the two terminal are isomorphic in that they both have the same number of incoming morphisms and no outgoing morphisms (save the identity).

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.).

 ``````mmlang> [[5,6,7],[7,5]{-1}] ==>6``````

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,

 ``````mmlang> {0}[start,6] mmlang> 6[is>7] mmlang> 6[is>8] mmlang> 6[is>9]``````

$\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.

 ``````mmlang> 6{0} mmlang> int{0}[plus,2] mmlang> int[plus,2]{0} mmlang> _{0}``````

Types such as `int{0}` and `int{0}<=int[is,false]` are equivalent due to their quantifiers both being `{0}`. Throughout the documentation, all zero quantified `objs` will be referred to as `_{0}`, `{0}`, or \mathbf{0} (the zero object).

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.

name sugar unsugared description mmlang example

some

`{1,1}`

a single `int`

``````mmlang> int
==>int``````

option

`{?}`

`{0,1}`

0 or 1 `int`

``````mmlang> int{?}<=int[is>0]
==>int{?}<=int[is,bool<=int[gt,0]]``````

none

`{0}`

`{0,0}`

0 `ints`

``````mmlang> int{0}<=int[is,false]
mmlang>``````

exact

`{4}`

`{4,4}`

4 `ints`

``````mmlang> int{4}<=int{2}[_,_]
==>int{4}<=int{2}[id]{2}``````

any

`{*}`

`{0,max}`

0 or more `ints`

``````mmlang> int{*}<=rec{*}[get,'age',int]
==>int{*}<=rec{*}[get,'age',int]``````

given

`{+}`

`{1,max}`

1 or more `ints`

``````mmlang> int{+}
==>int{+}``````

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

###### Type Signature Quantification

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.

``````mmlang> 4 => int{6}<=int{3}[[plus,1],[plus,1]]
language error: int is not an int{3}
mmlang> 4{3} => int{6}<=int{3}[[plus,1],[plus,1]]
==>5{6}
mmlang> [4,5,6] => int{6}<=int{3}[[plus,1],[plus,1]]
==>5{2}
==>6{2}
==>7{2}
mmlang> [4{2},5{1},6{2}] => int{6}<=int{3}[[plus,1],[plus,1]]
language error: int{5} is not an int{3}
mmlang> [4{2},5{-1},6{2}] => int{6}<=int{3}[[plus,1],[plus,1]]
==>5{4}
==>6{-2}
==>7{4}``````

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}).

###### Type Definition Quantification

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.

``````mmlang> int{3}[[plus,1],[plus,1]]              (1)
==>int{6}<=int{3}[plus,1]{2}
mmlang> int{3}[plus,1]{2}                      (2)
==>int{6}<=int{3}[plus,1]{2}``````
 1 Given `3` `ints`, `[plus,1]` will be evaluated (in parallel) twice. The result is `6` `ints`. 2 The instruction `[plus,1]{2}` is the merging of two `[plus,1]` branches.

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.

 $\begin{split} a(b+b)c &= a(2b)c \\ &= a2bc \\ &= 2abc \end{split}$

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.

 ``````mmlang> 4{3} => [[plus,1],[plus,1]] ==>5{6} mmlang> 4{3} => int{6}<=int{3}[[plus,1],[plus,1]] ==>5{6} mmlang> 4{2} => int{6}<=int{3}[[plus,1],[plus,1]] language error: int{2} is not an int{3}`````` $\begin{split} \texttt{int{q}} &= 3 \ast (1 + 1) \\ &= (3 \ast 1) + (3 \ast 1) \\ &= 3 + 3 \\ &= 6 \end{split}$ ``````mmlang> 4{3} => [plus,1]{2} ==>5{6} mmlang> 4{3} => int{6}<=int{3}[plus,1]{2} ==>5{6} mmlang> 4{2} => int{6}<=int{3}[plus,1]{2} language error: int{2} is not an int{3}`````` $\begin{split} \texttt{int{q}} &= 3 \ast 2 \\ &= 6 \end{split}$
##### Type Evaluation
 $\big[ m_0 \ast m_1 \ast \ldots \ast m_n \big] \begin{bmatrix} g_0 \\ + \\ g_1 \\ + \\ \vdots \\ + \\ g_n \end{bmatrix} \left| \oplus r \right\rangle \big[ \ast \ldots \ast \big] \begin{bmatrix} + \\ \vdots \\ + \\ \end{bmatrix} \ldots$

The mm-ADT virtual machine has two layers of logic: the instruction set architecture and the stream ring. The instructions specify how input `objs` are mapped to output `objs` this representation has a graphical realization as a generalized Cayley graph and a commuting diagram. This algebra is embedded in the processor-oriented stream ring algebra. The stream ring has three operators for composing `objs`: \ast,  +, and \oplus. The multiplicative monoid’s \ast-operator concatenates serial streams, the additive abelian group’s  +-operator enables independent parallel streams, and the stream near-ring’s non-commutative group’s \oplus-operator reduces streams down to a singleton stream.

sugar op inst

`=>`

\ast

`[juxt]`

`[ ]`

 +

`[branch]`

`=]`

 \oplus

`[barrier]`

The illustration above is an intuitive visualization of an mm-ADT type from the perspective of monoidal, group, and near-ring magmas interacting with one another in a series (\ast) of expansions ( +) and contractions ( \oplus), where m_i,g_i,r \in \tt{obj}. The mm-ADT instruction set architecture has three higher-order instructions providing direct access to the three stream ring operators. It is through these instructions that the other instructions are grounded in the underlying stream ring algebra of the mm-ADT VM.

### Type System

mm-ADT’s type system is founded on 3 classes of ctypes: anonymous, mono, and poly types. Within the `mono` and `poly` types, further subdivisions exist. These foundational types are the building blocks by which all other types are constructed using the ring operators of mm-ADT’s stream ring algebra. At the limit, an mm-ADT program is best understood as a "complex" type.

#### Anonymous Types

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.

`_` range `_` domain
``````mmlang> bool<=int[gt,10]      (1)
==>bool<=int[gt,10]
mmlang> _<=int[gt,10]         (2)
==>bool<=int[gt,10]
mmlang> int[gt,10]            (3)
==>bool<=int[gt,10]
mmlang> _
==>_``````
 1 The domain and range of the type are fully specified. 2 A type with a specified domain of `int` and a specified range of `_`. 3 An `mmlang` sugar where if no range is specified, and it differs from the domain, then `_` is assumed.
``````mmlang> int{?}<=int[is,bool<=int[gt,10]]     (1)
==>int{?}<=int[is,bool<=int[gt,10]]
mmlang> int[is,int[gt,10]]                   (2)
==>int{?}<=int[is,bool<=int[gt,10]]
mmlang> int[is,_[gt,10]]                     (3)
==>int{?}<=int[is,bool<=int[gt,10]]
mmlang> int[is,[gt,10]]                      (4)
==>int{?}<=int[is,bool<=int[gt,10]]``````
 1 The domain and range of the outer and inner nested type are fully specified. 2 The nested type has a specified domain of `int`. 3 The nested type has an unspecified domain of `_`. 4 An `mmlang` sugar where if no domain is specified, `_` is assumed.
 In the anonymous type `_{2}[plus,1]{3}[gt,0]`, the `[plus]` instruction is polymorphic, but `[gt]` isn’t. Thus, the anonymous type’s range can be deduced, but without a domain ctype, the internal dtype is also unknown. When `int{2}` is provided, it triggers a cascade of deductions that determines incident types of the instructions in the `obj` graph. The quantifier ring, when moving "horizontally" across the multiplicative `inst` monoid alters quantifiers using its multiplication operator, where 2 \ast 3 \ast 1 = 6. Thus, `bool{6}<=int{2}[plus,1]{3}[gt,0]` ``````mmlang> _{2}[plus,1]{3}[gt,0][explain] ==>' bool{6}<=_{2}[plus,1]{3}[gt,0] inst domain range state -------------------------------------------- [plus,1]{3} _{2} => _{6} [gt,0] _{6} => bool{6} '`````` ``````mmlang> int{2}[plus,1]{3}[gt,0][explain] ==>' bool{6}<=int{2}[plus,1]{3}[gt,0] inst domain range state ---------------------------------------------- [plus,1]{3} int{2} => int{6} [gt,0] int{6} => bool{6} '``````
##### Anonymous Type Uses

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

``````mmlang> 5-<(_,_)                               (1)
==>(5{2})
mmlang> -5[is>0 -> +2 | _ -> +10]              (2)
==>5
mmlang> 5-<([a,int],[a,_],[a,str])             (3)
==>(true{2},false)``````
 1 When no processing is needed on a split, `_` should be provided. 2 When used in a `|-rec` `poly`, `_` is used to denote the default case. 3 `5` is both an `int` and a `_`, but not a `str`.

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.

variables named types
``````mmlang> 1 => int[plus,2][to,x][plus,3][mult,x]
==>18
mmlang> int[plus,2][to,x][plus,3][mult,x][explain]
==>'
int[plus,2]<x>[plus,3][mult,x]

inst        domain      range state
------------------------------------
[plus,2]    int    =>   int
[plus,3]    int    =>   int    x->int
[mult,x]    int    =>   int    x->int
'``````

``````mmlang> 1 => int[define,x<=int[plus,2]][x]
==>3
mmlang> int[define,x<=int[plus,2]][x][explain]
==>'
int[define,x<=int[plus,2]][plus,2]

inst                       domain      range state
---------------------------------------------------
[define,x<=int[plus,2]]    int    =>   int    x->x<=int[plus,2]
[plus,2]                   int   =>    int   x->x<=int[plus,2]
[plus,2]                   int    =>   int    x->x<=int[plus,2]
'``````

#### Mono Types

type inst 0 1

`bool`

`&&` `||` `-` `!`

`false`

`true`

`int`

`*` `+` `-` `>` `<` `>=` `=<`

`0`

`1`

`real`

`*` `+` `-` `>` `<` `>=` `=<`

`0.0`

1.0

`str`

`+` `>` `<` `>=` `=<`

`''`

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.

##### Zero and One

The instructions `[zero]` and `[one]` are constant polymorphic instructions. Each provides a unique singleton value associated with the type of the respective incoming `obj`.

``````mmlang> (true;6;5.5;'ryan')=([zero];[zero];[zero];[zero])
==>(false;0;0.0;'')
mmlang> (true;6;5.5)=([one];[one];[one])
==>(true;1;1.0)
mmlang> 'ryan'[one]
language error: 'ryan' is not supported by [one]``````

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

``````mmlang> (true,6,5.5,'ryan')>-_[plus,[zero]]
==>true
==>6
==>5.5
==>'ryan'
mmlang> (true,6,5.5)>-_[mult,[one]]
==>true
==>6
==>5.5
mmlang> (true,6,5.5)>-_[mult,[zero]]
==>false
==>0
==>0.0``````

#### Poly Types

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.

abstract algebra equations concrete algebra equations

identity

a \cdot \mathbf{1} = a

a \cdot b = b

inverses

a \cdot a^{-1} = \mathbf{1}

a \cdot b^{-1} = \mathbf{1}

associativity

a \cdot (b \cdot c) = (a \cdot b) \cdot c

(a \cdot b) \cdot c = b \cdot c

commutativity

a \cdot b = b \cdot a

a \cdot a = a

In mm-ADT, a `poly` can be used as a collection data structure, where the collection’s semantics are tied to the operator(s) of the free object’s abstract algebra. Moreover, type-based `polys` offer data flow control semantics. The mm-ADT `poly` is a versatile structure 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.

##### Poly Structures

There are value `polys` and there are type `polys`. A value `poly` is composed of only value `objs` and is best understood as a collection data structure. A type `poly` contains at least one type `obj` and is intuitively understood as a flow control 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: `,` (abelian group), `;` (monoid), or `|` (near-ring). These algebras correspond to the magmas of mm-ADT’s stream ring algebra.

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

poly sep access value type

`lst`

`,`

all

multiset

union

`;`

last

list

chain

`|`

scalar

coalesce

`rec`

`,`

all match

multimap

`;`

last match

record

condition

`|`

first match

pair

switch

##### Poly Collections

A `poly` can be used a collection data structure. There are a total of 6 sorts of collections as there are two kinds of `poly` (`lst` and `rec`) and each kind has 3 algebras (`,`,`;`,`|`).

lst collection mmlang example rec collection mmlang example

`,`

``````mm> ('a'{?},'b','a','b')
==>('a'{1,2},'b'{2})
mm> ('a'{?},'b','a','b')>-
==>'a'{1,2}
==>'b'{2}``````

`,`

``````mm> ('a'->1,'b'->2,'a'->3)
==>('a'->[1,3],'b'->2)
mm> ('a'->1,'b'->2,'a'->3)>-
==>1
==>3
==>2``````

`;`

``````mm> ('a';'b';'a';'b')
==>('a';'b';'a';'b')
mm> ('a';'b';'a';'b')>-
==>'b'``````

`;`

``````mm> ('a'->1;'b'->2;'a'->3)
==>('a'->1;'b'->2;'a'->3)
mm> ('a'->1;'b'->2;'a'->3)>-
==>3``````

`|`

``````mm> ('a'|'b'|'a'|'b')
==>('a'|'b')
mm> ('a'|'b'|'a'|'b')>-
==>'a'``````

`|`

``````mm> ('a'->1|'b'->2|'a'->3)
==>('a'->1)
mm> ('a'->1|'b'->2|'a'->3)>-
==>1``````

,-poly Collections

The ,-polys capture the additive abelian group of the mm-ADT stream ring.

abstract magma stream magma free poly

$(\tt{obj}, +, \mathbf{0})$

$(\texttt{obj},\texttt{[branch]},\{\mathbf{0}\})$

$(\texttt{obj},\texttt{(,)},\{\mathbf{0}\})$

A general `,-poly` has `obj` as its carrier set, `,` as its the commutative binary +-operator, and `{0}` (`_{0}`) as its identity element. With `obj` quantification, should two `,-poly` terms have equal objects, they can be merged according to the mm-ADT `[branch]` operator equation: $\begin{split} [\texttt{branch},a_q, b_r] &= \begin{cases} a_{q + r} & \text{if } a == b, \\ [\texttt{branch},a_q, b_r] & \text{otherwise}, \end{cases} \\ [a_q, b_r] &= \end{split}$ where + is the quantifier ring’s additive operator and $[a_q,\{\mathbf{0}\}] = a_q.$ The commutative aspect of the `,-poly` does not enforce an order upon its elements which yields set-like semantics. However, given quantifier "weighting," `,-lst` collections realize multiset semantics (also known as bags or weighted sets) and `,-rec` collections realize multimap semantics (associative arrays with multiple values for a single key).

A few self-explanatory `,-poly` examples are provided below.

,-lst ,-rec
``````mmlang> (1,{0},1,2,3)
==>(1{2},2,3)
mmlang> ('a'{7},'b','b'{0},'c','a'{2})
==>('b','c','a'{9})
mmlang> ('a',1.0,1,true)
==>('a',1.0,1,true)``````

``````mmlang> (1->2,{0}->2,1->3,1->2,3->1)
==>(1->2{2},3->1)
mmlang> ('a'{7}->2,'a'->2{3},'b'->2)
==>('a'{7}->2,'a'->2{3},'b'->2)
mmlang> ('a'->true,1.0->6,1->{0},'a'->'a')
==>('a'->[true,'a'],1.0->6)``````

;-poly Collections

The ;-polys capture the non-commutative, multiplicative monoid of the mm-ADT ring.

abstract magma stream magma free poly

$(\tt{obj}, \ast, \mathbf{1},\mathbf{0})$

$(\texttt{obj},\texttt{[juxt]},\{\mathbf{1}\},\{\mathbf{0}\})$

$(\texttt{obj},\texttt{(;)},\{\mathbf{1}\},\{\mathbf{0}\})$

The `;-poly` carrier set is `obj`, the multiplicative operator is `;`, the multiplicative identity is `{1}`, and due to the larger ring in which this magma is embedded, `{0}` is the annihilator. Due to non-commutativity, the `;` delimited elements form an ordered sequence. In `lst`, the consequence is a collection data structure with list-semantics. In `rec`, a record with ordered fields is realized. Both support duplicates so the `rec` form is less like an associative array and more like a list of pairs/fields.

The `[juxt]` operator is mm-ADT’s multiplicative monoid operator and is only applied in `;-poly` for the universal elements \mathbf{1} and \mathbf{0}. Given the equation

$\begin{split} a_q[\texttt{juxt}, b_r] &= \begin{cases} b_{q \ast r} & \text{if } b \text{ is a value}, \\ b(a)_{q \ast r} & \text{otherwise,} \end{cases} \\ a_q \Rightarrow b_r &= \end{split}$

`;-poly` only computes the identity and the annihilator

 $\begin{split} a_q \Rightarrow \{\mathbf{1}\} &= \\ \{\mathbf{1}\}_1(a_q) &= \\ a_{q \ast 1} &= a_q \end{split}$ $\begin{split} a_q \Rightarrow \{\mathbf{0}\} &= \\ \{\mathbf{0}\}_0(a_q) &= \\ a_{q \ast 0} &= \{\mathbf{0}\}. \end{split}$

Examples are presented below that contain both \{\mathbf{0}\} and \{\mathbf{1}\} elements.

;-lst ;-rec
``````mmlang> (1;6;1;2;{1})
==>(1;6;1;2;_)
mmlang> ('a'{7};'b';'b'{0};'c';'a'{2})
==>('a'{7};'b';{0};'c';'a'{2})
mmlang> ('a';{1};1.0;1;true;{1})
==>('a';_;1.0;1;true;_)``````

``````mmlang> (1->2;{1}->2;1->3;1->{1};3->1)
==>(1->2;_->2;3->1)
mmlang> ('a'{7}->2;'a'->2{3};'b'->2)
==>('a'{7}->2;'a'->2{3};'b'->2)
mmlang> ('a'->true;1.0->4;1->{0};{1}->'a')
==>({0}->{0})``````

|-poly Collections

The |-polys captures endomorphic, left-distributive, multiplicative, compositions over the near-ring subgroup of mm-ADT’s additive abelian group.

abstract magma stream magma free poly

$(\texttt{obj},\oplus_1,\mathbf{0}/\mathbf{1})$

$(\texttt{obj},\texttt{[barrier,[head]]},\{\mathbf{1}\},\{\mathbf{0}\})$

$(\texttt{obj},\texttt{(|)},\{\mathbf{1}\},\{\mathbf{0}\})$

The `[barrier]` n-ary operator’s arguments are all the `objs` of the input stream. This yields a blocking synchronization point necessary for reduce/fold-based computations. The operator’s 1 subscript denotes a particular augmentation to the higher-order \oplus operator, where \oplus_1 returns the first non-zero `obj` argument — i.e., the head of the stream (a lazy computation).

$\begin{split} [a_q,\ldots,b_r]\texttt{[barrier,[head]]} &= \begin{cases} a_q & \text{if } q > 0, \\ \ldots \\ b_r & \text{if } r > 0, \\ \{\mathbf{0}\} & \text{otherwise,} \end{cases} \end{split}$

`|-poly` yields singleton `lsts` and `recs`. The purpose of this seemingly odd behavior is more salient in `|-polys` flow controls (presented in the next section). A collection of self-explanatory examples are provided below.

|-lst |-rec
``````mmlang> (1|6|1|2|{1})
==>(1|6|2)
mmlang> ('a'{0}|'b'{0}|'c'|'a'{2})
==>('c'|'a'{2})
mmlang> ('a'{?}|{1}|1.0|true)
==>('a'{?}|_)``````

``````mmlang> ({1}->2|6->2|1->3|1->{1}|3->1)
==>(_->2)
mmlang> ('a'{0}->2|'b'->2{3}|'c'->2)
==>('b'->2{3})
mmlang> ('a'->{0}|{0}->4|1->true|2->'a')
==>(1->true)``````

 When each `poly` contains 0 or 1 element, the respective algebras behave equivalently. It is only at 2+ terms that the `poly` algebras become discernible and instructions such as `[eq]` consider the `poly` element separator in their calculation.
##### Poly Controls

The mm-ADT ring’s additive abelian group operator is accessible via the `[branch]` instruction. The `[branch]` instruction’s argument is a `poly`. Each term of the `poly` argument is an operand of the ring’s +-operator. In this way, each of the 6 `poly` forms represents a particular control structure. Due to the prevalent use of `[branch]`, `mmlang` offers the sugar’d encoding of `[ ]`, where both the instruction opcode and the `poly` parentheses are not written. For example, `[branch,(+1,+2,+3)]` is equivalent to `[+1,+2,+3]`.

lst control mmlang example rec control mmlang example

`,`

``````mm> 6 => int[+1,+3,+1]
==>9
==>7{2}``````

`,`

``````mm> 6 => int[is>10 -> +1,
is>5  -> +2,
int   -> +3]
==>8
==>9``````

`;`

``````mm> 6 => int[+1;+2;+3]
==>12``````

`;`

``````mm> 6 => int[is>0 -> +1;
is>5 -> +2;
int  -> +3]
==>12``````

`|`

coalesce

``````mm> 6 => int[+1[is>10]|
+2[is>5] |
+3       ]
==>8``````

`|`

switch

``````mm> 6 => int[is>10 -> +1|
is>5  -> +2|
_     -> +3]
==>8``````

,-poly Controls

The ,-polys capture the additive abelian group of the mm-ADT ring. The associativity and commutativity of the group operator means that the order in which the terms are evaluated (associativity) and results aggregated (commutativity) does not change the semantics of the computation. More specifically to the notion of control, it means that the irreducible terms in a `,-poly` are not sequentially dependent on one another. This independence enables evaluation isolation and thus, promotes parallelism. The `,-poly` algebra realizes cascading union in `lst` and conditional cascading in `rec`.

Note that in all subsequent `[branch,poly]` equations to follow, x \in \tt{obj} is an incoming `obj` to the respective `[branch]` instruction.

$x ⇒ \big[v_0,v_1,\ldots,v_n\big] \;\;=\;\; \coprod_{i=0}^n x ⇒ v_i$

$x ⇒ \big[[k_0,v_0],\ldots,[k_n,v_n]\big] \;\;=\;\; \coprod_{i=0}^n \begin{cases} x ⇒ v_i & \text{if } (x ⇒ k_i) \neq \mathbf{0}, \\ \mathbf{0} & \text{otherwise}. \end{cases}$

;-poly Controls

The ;-polys capture the multiplicative monoid of the mm-ADT ring. The result of each term is the input to the next term in the sequence. In `lst`, method chaining is realized and in `rec` conditional chaining.

;-lst (fluent chaining) ;-rec (conditional chaining)

$x ⇒ \big[v_0;v_1;\ldots;v_n\big] \;\;=\;\; x ⇒ \prod_{i=0}^n v_i$

$x ⇒ \big[[k_0,v_0],\ldots,[k_n,v_n]\big] \;\;=\;\; x ⇒ \prod_{i=0}^n \begin{cases} v_i & \text{if } (x ⇒ k_i) \neq \mathbf{0}, \\ \mathbf{0} & \text{otherwise}. \end{cases}$

|-poly Controls

The |-polys capture mm-ADT’s barrier near-ring, where the first non-\mathbf{0} ("non-null") element is the output of the branch. As a control structure, `|-poly` is a sequential branch that can be understood programmatically as a short-circuit fold. In `lst`, non-null coalescing is realized and in `rec` a switch statement is realized.

|-lst (coalesce) |-rec (switch)

$x ⇒ \big[v_0,v_1,\ldots,v_n\big] = \begin{cases} x ⇒ v_0 & \text{if } (x ⇒ v_0) \neq \mathbf{0}, \\ x ⇒ v_1 & \text{if } (x ⇒ v_1) \neq \mathbf{0}, \\ \ldots & \\ x ⇒ v_n & \text{if } (x ⇒ v_n) \neq \mathbf{0}, \\ \mathbf{0} & \text{otherwise}. \end{cases}$

$x ⇒ \big[[k_0,v_0],\ldots,[k_n,v_n]\big] = \begin{cases} x ⇒ v_0 & \text{if } (x ⇒ k_0) \neq \mathbf{0}, \\ x ⇒ v_1 & \text{if } (x ⇒ k_1) \neq \mathbf{0}, \\ \ldots & \\ x ⇒ v_n & \text{if } (x ⇒ k_n) \neq \mathbf{0}, \\ \mathbf{0} & \text{otherwise}. \end{cases}$

 As previously stated for collection `polys`, control `poly` semantics are only discernible amongst `polys` with 2 or more terms.
##### Poly Lifting

A consequence of the dual use of `poly` as both a data structure and a control structure is that `poly` supports a lifted encoding of mm-ADT itself. Each `poly` form captures a particular magma of the underlying mm-ADT stream ring algebra. As a collection, `poly` provides a programmatic way of writing mm-ADT programs (types) and as flow control, these `poly` encoded mm-ADT programs can be executed. The complete algebraic specification of `poly` lifting via an `obj`-module of the mm-ADT ring will be presented in a latter section. For now, the following `mmlang` examples demonstrate `poly` lifting in support of mm-ADT metaprogramming.

The mm-ADT type below contains both monoidal (serial composition) and group (parallel branching) components whose construction is captured by the bottom morphism of the diagram above. Note that the `[explain]` instruction is appended for educational purposes only — so as to detail the \Rightarrow compositions.

``````mmlang> int{3}[mult,10][is>20 -> [+70,+170,+270],
is>10 ->   [*10,*20,*30]][plus,100][explain]
==>'
int{0,18}<=int{3}[mult,10][int{0,3}<=int{3}[is,bool{3}<=int{3}[gt,20]]->int{9}<=int{3}[int{3}[plus,70],int{3}[plus,170],int{3}[plus,270]],int{0,3}<=int{3}[is,bool{3}<=int{3}[gt,10]]->int{9}<=int{3}[int{3}[mult,10],int{3}[mult,20],int{3}[mult,30]]][plus,100]

inst                                           domain            range       state
-----------------------------------------------------------------------------------
[mult,10]                                      int{3}       =>   int{3}
[int{0,3}<=int{3}[is,bool{3}<=int{3}[gt,...    int{3}       =>   int{0,18}
[is,bool{3}<=int{3}[gt,20]]                    int{3}      =>    int{0,3}
[gt,20]                                        int{3}     =>     bool{3}
->[int{3}[plus,70],int{3}[plus,170],int{3}...    int{3}      =>    int{9}
[plus,70]                                      int{3}     =>     int{3}
[plus,170]                                     int{3}     =>     int{3}
[plus,270]                                     int{3}     =>     int{3}
[is,bool{3}<=int{3}[gt,10]]                    int{3}      =>    int{0,3}
[gt,10]                                        int{3}     =>     bool{3}
->[int{3}[mult,10],int{3}[mult,20],int{3}[...    int{3}      =>    int{9}
[mult,10]                                      int{3}     =>     int{3}
[mult,20]                                      int{3}     =>     int{3}
[mult,30]                                      int{3}     =>     int{3}
[plus,100]                                     int{0,18}    =>   int{0,18}
'``````

The above type can be expressed in a pure `poly` form, where `;` is serial composition and `,` is parallel branching. This construction is captured by the slanted morphism in the diagram above.

``````mmlang> (int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270)>-)>-,
-<([is>10];-<(*10,*20,*30  )>-)>-)>-;[plus,100])
==>(int{3};_[mult,10];_[split,(_[split,(_[is,_[gt,20]];_[split,(_[plus,70],_[plus,170],_[plus,270])][merge])][merge],_[split,(_[is,_[gt,10]];_[split,(_[mult,10],_[mult,20],_[mult,30])][merge])][merge])][merge];_[plus,100])``````

The `[split]` instruction (sugar’d `-<`) renders `poly` a ring module. Incoming `objs` are scalars to a `poly` vector according to the equations $\begin{split} x \prec &\; (v_0,v_1,\ldots,v_n) \;\;&=\;\; (xv_0,xv_1,\ldots,xv_n) \\ x \prec &\; (v_0;v_1;\ldots;v_n) \;\;&=\;\; (xv_0;v_1;\ldots;v_n) \\ x \prec &\; (v_0|v_1|\ldots|v_n) \;\;&=\;\; (xv_i), \end{split}$ where x \prec \tt{poly} is the instruction `x => [split,poly]`. The `[merge]` instruction evaluates the `poly` according to the algebra denoted by its term separator (`,`, `;`, or `|`). This has the effect of "draining" the `poly` of it’s internal `objs` such that $\begin{split} (xv_0,xv_1,\ldots,xv_n) \succ \;\;&=\;\; \coprod_{i=0}^n x \Rightarrow v_i \\ (xv_0;v_1;\ldots;v_n) \succ \;\;&=\;\; x \Rightarrow \prod_{i=0}^n v_i \\ (xv_i) \succ \;\;&=\;\; xv_i : v_i \neq \mathbf{0}, \end{split}$ where \tt{poly} \succ is the expression `poly => [merge]`.

Finally, both the original unlifted form and the `poly` lifted form of the type yield the same result at evaluation, where the final expression binds (`-<`) the values 1, 2, and 3 to the indeterminate terms, thus solving (`>-`) the polynomial equation.

``````mmlang> [1,2,3] => int{3}[mult,10][is>20 -> [+70,+170,+270],
is>10 ->   [*10,*20,*30]][plus,100]
==>500
==>200
==>300{2}
==>400{2}
==>700{2}
==>1000
mmlang> [1,2,3]-<(int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270)>-)>-,
-<([is>10];-<(*10,*20,*30  )>-)>-)>-;[plus,100])>-
==>500
==>200
==>300{2}
==>400{2}
==>700{2}
==>1000``````

Given that `[split,poly:x][merge]` is equivalent to `[branch,poly:x]`, the `poly` type can be written more succinctly in a pure `[branch]` form as below.

``````mmlang> [1,2,3] => [int{3};[mult,10];[[[is>20];[+70,+170,+270]],
[[is>10];[*10,*20,*30  ]]];[plus,100]]
==>500
==>200
==>300{2}
==>400{2}
==>700{2}
==>1000``````

Note that, when incident to each other, `[split]/[merge]` has the same equation as `[branch]`.

$\begin{split} x \prec &\; (v_0,v_1,\ldots,v_n) \succ \;\;&=\;\; x \Rightarrow \big[v_0,v_1,\ldots,v_n \big] \;\;&=\;\; \coprod_{i=0}^n x \Rightarrow v_i \\ x \prec &\; (v_0;v_1;\ldots;v_n) \succ \;\;&=\;\; x \Rightarrow \big[v_0;v_1;\ldots;v_n\big] \;\;&=\;\; x \Rightarrow \prod_{i=0}^n v_i \\ x \prec &\; (v_0|v_1|\ldots|v_n) \succ \;\;&=\;\; x \Rightarrow \big[v_0|v_1|\ldots|v_n\big] \;\;&=\;\; xv_i : v_i \neq \mathbf{0} \end{split}$

The reason for using `-<( )>-` versus `[ ]` is that when `[split]` and `[merge]` are not juxtaposed, reflection is possible on the intermediate results of the internal `poly` computation. That is, when only a `[split]` is applied, a half-branch occurs and all the `poly` domain instructions can operate on the midway results. Intuitively, `[split]` transforms a control structure into a data structure and `[merge]` transforms a data structure into a control structure. At this intermediate point when the computation is a data structure, the computation can be manipulated programmatically. That is the power of a lifted representation.

``````mmlang> [1,2,3]-<(int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270))))
==>(1;10;(({0};{0})))
==>(2;20;(({0};{0})))
==>(3;30;((30;(100,200,300))))
mmlang> [1,2,3]-<(int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270)),
-<([is>10];-<(*10,*20,*30  ))))
==>(1;10;(({0};{0}),({0};{0})))
==>(2;20;(({0};{0}),(20;(200,400,600))))
==>(3;30;((30;(100,200,300)),(30;(300,600,900))))
mmlang> [1,2,3]-<(int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270)>-)>-,
-<([is>10];-<(*10,*20,*30  )>-)>-)>-;[plus,100])
==>(1;10;{0};{0})
==>(2;20;[200,400,600];[300,500,700])
==>(3;30;[100,200,300{2},600,900];[200,300,400{2},700,1000])
mmlang> [1,2,3]-<(int{3};[mult,10];-<(-<([is>20];-<(+70,+170,+270)>-)>-,
-<([is>10];-<(*10,*20,*30  )>-)>-)>-;[plus,100])>-
==>500
==>200
==>300{2}
==>400{2}
==>700{2}
==>1000``````

In summary, mm-ADT can be embedded in `poly` itself. The formal proof of this fact demonstrates that the mm-ADT instruction set architecture, the two ring operators (+ and *), and the reduce near-ring operator (\oplus) are sufficiently expressive to yield a Turing Complete computing machine.

## The Obj Graph

An mm-ADT program is a type. The `mmlang` parser converts a textual representation of a type into a type `obj`. A type is inductively defined and is encoded as a path within the larger type graph. The type’s path is a graphical encoding specifying a data flow pipeline that when evaluated, realizes elements of the type (i.e. computed resultant values). These values also have a graphical encoding paths in the value graph. Together, the type graph and the value graph form the obj graph.

Every aspect of an mm-ADT computation from composition, to compilation, and ultimately to evaluation is materialized in the `obj` graph. The following itemizations summarizes the various roles that the `obj` graph throughout a computation.

• Composition: The construction of a type via the point-free style of `mmlang` is a the lexical correlate of walking the `obj` graph from a source vertex (domain ctype) across a series of instruction-labeled edges (`inst`) to ultimately arrive at a target vertex (range ctype). The path, a free object, contains both the type’s signature and definition.

• Compilation: A path in the type graph can be prefixed with another ctype (e.g. placing `int` before `_`). In doing so, the path’s domain has been alterered and the path is recomputed to potentially yield a variant of the original path (e.g. a type inferenced path).

• Rewrite: Subpaths of a path in the type graph can be specified as being semantically equivalent to another path in the type graph via `poly` lifted rewriting `(y)<=(x)`. Subsequent compilations and evaluations of the path may yield path variants.

• Optimization: Every instruction in `inst` has an associated cost dependent on the underlying storage and processor. Rewrites create a superposition of programs. Given that the `obj` graph commutes, a weighted shortest path calculation from a domain vertex to a range vertex is an example of a simple technique for choosing an efficient execution plan.

• Variables: Variable bindings are encoded in instructions. When the current instruction being evaluated requires historic state information, the `obj`op graph (with edges reversed) is searched in order to locate the vertex incident to a variable `inst`.

• Evaluation: Program evaluation binds the type graph to the value graph. When a type path is prefixed with a value `obj`, the instructions along the path operate on the value, where the path’s target vertex is the result of the computation.

This section will discuss the particulars of the aforementioned uses of the `obj` graph.

### State

Let (M,\cdot,e) be a monoid, where e \in M is the identity element and there exists an element e' \in M that also acts as an identity such that for every  x \in M , x \cdot e = x and x \cdot e' = x, then because e \cdot e' = e and e \cdot e' = e', it is the case that e = e \cdot e' = e' and e = e'. Thus, every monoid has a single unique identity. However, in a free monoid, where element composition history is preserved, it is possible to record e and e' as distinctly labeled elements even though their role in the non-free monoid’s binary composition are the same — namely, that they both act as identities.

idiom inst description

variables

`[to]`

`obj` references

type definitions

`[define]`

`type` mappings

models

`[model]`

domain of discourse

reversible computing

`[path]`

computing history

It is through multiple distinct identities in `inst` that mm-ADT supports the programming idioms in the associated table. The general approach is state is stored along the path of the `obj`.

``````mmlang> 6 => int[plus,[mult,2]][path]
==>(6;[plus,12];18)
<=6[plus,12][path,(_;_)]
mmlang> 8 => int[plus,[mult,2]][path]
==>(8;[plus,16];24)
<=8[plus,16][path,(_;_)]``````

Every `obj` exists as a distinct vertex in the `obj` graph. If b \in \tt{obj} has an incoming edge labeled i \in \tt{i\nst}, then when applied to the outgoing adjacent vertex a, b is computed. Thus, the edge a \to_i b records the instruction and incoming `obj` (a) that yielded the `obj` at the head of the edge (b). Since types are defined inductively and their respective values generated deductively via instruction evaluation along the type’s path, the path contains all the information necessary to effect state-based computing. The path of an `obj` is accessed via the `[path]` instruction. The output of `[path]` is a `;-lst` — i.e., an element of the `inst` syntactic monoid. This path `lst` is also a product and as such, can be introspected via it’s projection morphisms (e.g., via `[get]`).

``````mmlang> 8 => int[plus,1][mult,2][lt,63]                                                           (1)
==>true
mmlang> 8 => int[plus,1][mult,2][lt,63][path]                                                     (2)
==>(8;[plus,1];9;[mult,2];18;[lt,63];true)
<=8[plus,1][mult,2][lt,63][path,(_;_)]
mmlang> 8 => int[plus,1][mult,2][lt,63][path][get,5][get,0]                                       (3)
==>63``````
 1 The evaluation of an `bool<=int` type via 8. 2 The `obj` graph path from 8 to `[lt,63]`. 3 A projection of the instruction `[lt,63]` from the path and then the first argument of the `inst`.

mm-ADT’s multiple identity instructions simply compute the identity function f(x) \mapsto x, but as edge labels in the `obj` graph, they store state information that can be later accessed via trace-based path analysis (i.e. via `[path]`). In effect, the execution context is transformed from a memory-less finite state automata to a register-based Turing machine.

#### Variables

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.

 ``_[plus,1][to,x][plus,2][mult,x]``

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.

 In `mmlang`, the `[to]` instruction’s sugar is `< >`. It is the only instruction whose sugar is printed as opposed to its `[ ]` form.
 ``````mmlang> _ => [plus,1][plus,2][mult,x] ==>_[plus,1][plus,2][mult,x] mmlang> int => _[plus,1][plus,2][mult,x] ==>int[plus,1][plus,2][mult,x] mmlang> 9 => int[plus,1][plus,2][mult,x] ==>120``````

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.

``````mmlang> 9 => int[plus,1]<x>[plus,2][mult,x][path]                                                 (1)
==>(9;[plus,1];10;<x>;10;[plus,2];12;[mult,10];120)
<=9[plus,1]<x>[plus,2][mult,10][path,(_;_)]
mmlang> int[plus,1]<x>[plus,2][mult,x][explain]                                                   (2)
==>'
int[plus,1]<x>[plus,2][mult,x]

inst        domain      range state
------------------------------------
[plus,1]    int    =>   int
[plus,2]    int    =>   int    x->int
[mult,x]    int    =>   int    x->int
'``````
 1 The `[path]` instruction provides the path of the current `obj` as a `;-lst`. 2 The `[explain]` instruction details the scope of state variables.

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.

``````mmlang> 2 => int<x>[plus,<y>][plus,y]                                                             (1)
language error: 4 does not contain the label 'y'
mmlang> 2 => int<x>[plus,[plus,x]<x>[plus,x]][plus,x]                                             (2)
==>12
mmlang> 2 => int<x>[plus,[plus,x]<x>[plus,x]][plus,x][path]                                       (3)
==>(2;<x>;2;[plus,8];10;[plus,2];12)
<=2<x>[plus,8][plus,2][path,(_;_)]
mmlang> int<x>[plus,int<y>[plus,int<z>[plus,x][plus,y][plus,z]][plus,y]][plus,x][explain]         (4)
==>'
int<x>[plus,int<y>[plus,int<z>[plus,x][plus,y][plus,z]][plus,y]][plus,x]

inst                                           domain      range state
-----------------------------------------------------------------------
[plus,int<y>[plus,int<z>[plus,x][plus,y]...    int    =>   int    x->int
[plus,int<z>[plus,x][plus,y][plus,z]]          int   =>    int   x->int y->int
[plus,x]                                       int  =>     int  x->int y->int z->int
[plus,y]                                       int  =>     int  x->int y->int z->int
[plus,z]                                       int  =>     int  x->int y->int z->int
[plus,y]                                       int   =>    int   x->int y->int
[plus,x]                                       int    =>   int    x->int
'``````
 1 The variable `y` is declared in a branch nested within the retrieving branch. 2 The variable `x` is redefined in the nested branch and recovers its original value when the nested branch completes. 3 The value path of the previous evaluation highlighting that the final `[plus,x]` resolved to `[plus,2]`. 4 A multi-nested expression demonstrating the creation and destruction of variable scope.

#### Definitions

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]`.

 ``[define,nat<=int[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.

``````mmlang> 36 => int[define,nat<=int[is>0]]                   (1)
==>36
mmlang> 36 => nat<=int[define,nat<=int[is>0]]              (2)
==>nat:36
mmlang> 36 => nat<=int[define,nat<=int[is>0]][mult,-1]     (3)
language error: -36 is not a nat``````
 1 A `nat` is defined, but never applied. Thus, logically, this is equivalent to `36 => int`. 2 A type can be used anytime after its definition in the path. Thus, `nat` is a viable range type. 3 If the `obj` is not a `nat`, then the larger `nat<=int` is invalid.
Deep Dive 2. mm-ADT Type Prefix
 ``````mmlang> :[model,mm][define,nat<=int[is>0]] ==>_[define,nat<=int[is,bool<=int[gt,0]]] mmlang> 10 => nat ==>nat:10 mmlang> -1 => nat language error: -1 is not a nat mmlang> 10 => nat[plus,5] ==>nat:15 mmlang> 10 => nat[plus,5][plus,-15] language error: 0 is not a nat``````

Prepending type definitions to every program reduces legibility and complicates program development. For this reason, mm-ADT provides a type prefix. All `mmlang` examples that start with `:` are defining the type prefix that will be used for all subsequent programs. The type prefix is a generalization of a library statement such as `import` or `module` found in other programming languages. The generalization is that a type prefix can be any type, not just those containing only `[define]`). The type prefix is prepended to the program type prior to compilation, where this operation is made sound by the free `inst` monoid.

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.

``````mmlang> :[model,mm][define,nat<=int[is>0],
date<=(nat[is=<12];nat[is=<31];nat),
date<=(nat[is=<12];nat[is=<31])[put,2,2020]]
mmlang>
mmlang> (8;26;2020) => date
==>date:(nat:8;nat:26;nat:2020)
mmlang> (8;26)      => date
==>date:(nat:8;nat:26;nat:2020)``````

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.

### Models

Homotopy Type Theory

Homotopy type theory understands types as coexisting with other types in a topological space. A spatial embedding implies that a type can be reached from another type by moving through space. The way in which the space is navigated is via paths. A path is a continuous deformations of one type into another type.

Types can be organized into model-ADTs (simply called models). The 4 mono types (`bool`,`int`,`real`,`str`) and the 2 poly types (`lst`, `rec`) are defined in the `mm` model-ADT (the mm of mm-ADT). The instruction `[model,mm]` generates a `rec` from the `mmlang` file `mm.mm`. Using the same multiplicity of identities principle, the `rec` is accessible in the type’s path definition via the `[model]` argument.

 ``````mm:('type' -> (bool -> ( ), int -> ( ), real -> ( ), str -> ( ), lst -> ( ), rec -> ( ), poly -> (poly<=[lst|rec]), ))``````

The `rec` encoding of a model-ADT has the model’s canonical types (ctypes) as keys and `lsts` of derived types (dtypes) as values. The encoding is a serialization of a graph where the ctypes are vertices and the incoming paths to a ctype vertex are the edges. Unfortunately, the `mm` model is too basic to demonstrate this point clearly. What `mm` does capture is the set nature of the base types in that there are vertices and no edges (save `poly` which is the coproduct of `lst` and `rec`).

In general, any model \mathbf{m} is defined $\begin{split} \texttt{model}_\mathbf{m} &= \coprod_{i=0}^{|\mathbf{m}|} \texttt{ctype}_i + (\texttt{dtype}_i^0 + \texttt{dtype}_i^1 + \ldots + \texttt{dtype}_i^n) \\ &= \coprod_{i=0}^{|\mathbf{m}|} \texttt{ctype}_i + \coprod_{j=0}^{|\texttt{dtype}_i|} \texttt{dtype}_i^j. \end{split}$ There are more ctypes than the 6 base types specified in `mm`. Typically, a ctype in one model is a dtype in another. If model \mathbf{m} has \tt{ctypes}_\mathbf{m} derived from types in model \mathbf{n}, then \tt{dtypes}_{\mathbf{n}} \subseteq \tt{ctypes}_{\mathbf{m}}. However, `mm` is unique in that the `mm` types are universally grounded and $\begin{split} \textbf{mm} &= \coprod_{i=0}^6 \texttt{ctype}_i + \mathbf{0}_i \\ &= \coprod_{i=0}^6 \texttt{ctype}_i \\ &= (\texttt{bool} + \texttt{int} + \texttt{real} + \texttt{str} + \texttt{lst} + \texttt{rec}) \end{split}$

That is, `mm` is the sum of 6 ctypes — the mm-ADT base types. Within `mm`, these ctypes are identity types. For example, in the `mm` model `rec` at the beginning of this section, the field `bool -> ( )` denotes \tt{bo\ol} \+ \mathbf{0} or simply \tt{bo\ol}. The `bool` ctype is shorthand for `bool<=bool`, which, when considering the quantifier ring, is shorthand for `bool{1}<=bool{1}`. An instruction less type is a `noop` and thus, `bool` captures the reflexivity of identity: $\texttt{bool}\Leftarrow\texttt{bool} \;\equiv\; \texttt{bool} + \mathbf{0} \;\equiv\; \texttt{bool}.$

Deep Dive 3. Model-ADT Subgraphs of the `obj` Graph

The associated illustration presents 3 models, their respective ctypes, and various dtypes between them. Every directed labeled binary edge in the diagram is a type of the form:

 ``b<=a[inst{*}]``

A type definition’s instructions specify the specific, discrete computational steps (`inst`) necessary to transform `a` (domain) into `b` (range). A series of instructions are constructed with type induction (composition), destructed with type deduction (compilation or evaluation), and are captured as paths in the type subgraph of the `obj` graph. Thse paths are equivalent to the morphisms of the `obj` category diagram and the edges in the `obj` Cayley graph. The illustration highlights three sorts of types:

• `xtype<=int[f]` (intra-model): In `xmodel`, `xtype` is grounded at `int` in `mm`.

• `ytype<=xtype[g]` (inter-model): In `xmodel`, `ytype` can be reached via `xtype`.

• `atype<=rec[h][i]` (trans-model): In `amodel`, `atype` is grounded at `rec` in `mm` via `ytype` in `xmodel`.

The `mm` model-ADT is too simple to be informative. The complexity of its types exist outside the virtual machine. In order to provide a comprehensive understanding of mm-ADT models, the following sections will build a property graph model-ADT (`pg`) in stages starting with `pg_1`, then `pg_2`, so forth before reaching the final complete encoding in `pg`.

#### Constructors

##### Property Graph Model 1

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 non-commuting 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']`.

 ``````pg_1:('type' -> ( vertex -> (vertex<=('id'->int)), edge -> ( edge<=('outV'->vertex,'inV'->vertex)))) <= mm``````
 A type definition with no instructions serves as both a model constructor and canonical type (a ctype). As a canonical type, the path from source to target does nothing. An `obj` that matches the left-hand side is simply labeled with the name of the `obj` on right-hand side. $\tt{(id→int)}\;\;\tt{\textrm{—[noop]}{\longrightarrow}}\;\;\tt{vertex}.$

Three examples of constructing a `vertex` are presented below.

``````mmlang> :[model,pg_1]                                (1)
==>_
mmlang> ('id'->1) => vertex                          (2)
==>vertex:('id'->1)
mmlang> ('id'->1,'age'->28) => vertex                (3)
==>vertex:('id'->1)
mmlang> ('ID'->1) => vertex                          (4)
language error: ('ID'->1) is not a vertex``````
 1 The type prefix loads the `pg_1` model into the `obj` graph. 2 A `vertex` from a `rec` with the requisite `'id'` field. 3 Extraneous (non-ambiguous) in the `vertex` instance is mapped to the terminal \mathbf{0}. 4 Coercion to a `vertex` is not possible given as `'ID'` is not `'id'`.

Three `edge` construction examples are presented below.

``````mmlang> :[model,pg_1]
==>_
mmlang> ('outV'->vertex:('id'->1),'inV'->vertex:('id'->2)) => edge     (1)
==>edge:('outV'->vertex:('id'->1),'inV'->vertex:('id'->2))
mmlang> ('outV'->('id'->1),'inV'->('id'->2)) => edge                   (2)
==>edge:('outV'->vertex:('id'->1),'inV'->vertex:('id'->2))
mmlang> (vertex:('id'->1);vertex:('id'->2)) => edge                    (3)
language error: (vertex:('id'->1);vertex:('id'->2)) is not an edge``````
 1 An `edge` is the `rec` product of two `vertices`. 2 If the components of the product can be coerced into vertices, they are automatically done so. 3 A `lst` product is not the same as a `rec` product given that `recs` are products of key/value pairs.

#### Type Paths

##### Property Graph Model 2

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.

inline ``````mmlang> :[model,pg_1] ==>_ mmlang> 1 => vertex<=int-<('id'->_) ==>vertex:('id'->1)`````` ``````mmlang> :[model,pg_1][define,vertex<=int-<('id'->_)] ==>_[define,vertex<=int[split,('id'->int)]] mmlang> 5 => vertex ==>vertex:('id'->5) mmlang> (5;6) => (vertex;vertex) ==>(vertex:('id'->5);vertex:('id'->6))`````` ``````pg_2:('type' -> ( vertex -> (vertex<=('id'->int), (1) vertex<=int-<('id'->_)), (2) edge -> (edge<=('outV'->vertex,'inV'->vertex), (3) edge<=(vertex;vertex)-<('outV'->.0,'inV'->.1)))) <= mm (4)``````
 1 The `mm` specification of a canonical `vertex` (an `inst`-less ctype). 2 A path from an `int` to a `vertex`. 3 The `mm` specification of a canonical `edge` (an `inst`-less ctype). 4 A path from a 2-tuple `vertex` `;-lst` to a `edge`.

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`.

``````mmlang> :[model,pg_2]
==>_
mmlang> (5;6) => (vertex;vertex)=>edge                                              (1)
==>edge:('outV'->vertex:('id'->5),'inV'->vertex:('id'->6))
mmlang> (5;6) => edge<=(vertex;vertex)
==>edge:('outV'->vertex:('id'->5),'inV'->vertex:('id'->6))
mmlang> (5;6) => edge                                                               (2)
==>edge:('outV'->vertex:('id'->5),'inV'->vertex:('id'->6))
mmlang> 5 => int-<(vertex;vertex) => edge                                           (3)
==>edge:('outV'->vertex:('id'->5),'inV'->vertex:('id'->5))
mmlang> 5-<(vertex;vertex)=>edge
==>edge:('outV'->vertex:('id'->5),'inV'->vertex:('id'->5))``````
 1 An `int` pair morphed into a `vertex` pair and then into an `edge`. 2 An `int` pair morphed into an `edge`. 3 An `int` split into `vertex` clone pairs and then morphed into a self-loop edge.

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]`.

Deep Dive 4. model-ADT Application Programming Interfaces

The software development pattern espoused by mm-ADT is one in which software libraries (APIs) are large commuting diagrams constructed via domain/range concatenation of b⇐a types. The diagrams are called models and are stored in model-ADT files analogous to `mm.mm`. With a diagram rich in paths, mm-ADT application code will tend towards a look-and-feel similar in form to $a\;{=[} b \Rightarrow c, \; d[x][y][z] \Rightarrow e \Rightarrow f ]\Rightarrow \ldots \dashv z.$ where d[x][y][z] denotes some intermediate instructions that operate on d prior to translating d to e (i.e., an inline type path) and the connectives that reflect the core operators of the underlying stream ring are:

• `=>` : multiplicative monoid for serial composition

• `=[,]` : additive group for parallel alignment

• `=|` : non-commutative group for barrier aggregation

#### Model Paths

The `pg_1` model extends `mm` via `pg_1<=mm`. Note that it is possible for a model to define types that have no incoming paths from `mm`. For example:

``````mmlang> :[model,ex:('type'->(A->(A<=B),B->(B<=C),C->(C<=A)))]
==>_
mmlang> 6 + 12
==>18
mmlang> A => D
language error: D for A is not a type in model ex
mmlang> A => B => C
==>C``````

This is not typical. In practice, every model-ADT will extend `mm` or some other model, where there exists a path of model extensions to `mm`. This is the concept of a model path which is analogous to a type path but instead of mapping types-to-types, a model path maps sets of types to sets of types—​or models-to-models.

That is, a type is associated with a list of type definitions for which the type is the range. These type definitions can be understood as single-step paths through the `obj` graph, such that the composition of these types is the diagram of the model.

#### Type Patterns

type description mmlang example

anonymous

A type with an unspecified domain.

``````mmlang> 5 => [plus,2]
==>7
mmlang> 5 => [plus,[plus,2]]
==>12``````

monomial

A primitive type that is a single term and coefficient.

``````mmlang> 5   => int
==>5
mmlang> '5' => int
language error: str is not an int
mmlang> 5   => int{10}
language error: int is not an int{10}``````

polynomial

A composite type containing a linearly combination of terms and their coefficients.

``````mmlang> (+{2}3,+{3}4,+{4}5)
==>(_[plus,3]{2},_[plus,4]{3},_[plus,5]{4})
mmlang> 5-<(+{2}3,+{3}4,+{4}5)
==>(8{2},9{3},10{4})
mmlang> 5-<(+{2}3,+{3}4,+{4}5)>-[sum]
==>83``````

refinement

A subset of another type.

``````mmlang> :[define,nat<=int[is>0]]
==>_[define,nat<=int[is,bool<=int[gt,0]]]
mmlang> 5 => nat
==>nat:5
mmlang> 0 => nat
language error: 0 is not a nat``````

recursive

A type with components of the same type.

``````mmlang> :[model,mm][define,list<=[(_){?}|(_,list)]]
==>_[define,list<=_[(_){?}|(_,list)]]
mmlang> (1)             => list
==>list:(1)
mmlang> (1,(1))         => list
==>list:(1,list:(1))
mmlang> (1,(1,(1)))     => list
==>list:(1,list:(1,list:(1)))
mmlang> (1,(1,(1,(1)))) => list
==>list:(1,list:(1,list:(1,list:(1))))
mmlang> 1               => list
language error: 1 is not a list
mmlang> (1,1)           => list
language error: (1{2}) is not a list``````

dependent

A type with a definition variable to the incoming `obj`.

``````mmlang> 5 => [is>int]
mmlang> 5 => [plus,int]
==>10``````

model

A set of types and path equations.

``````mmlang> :[model,social:('type'->
(person -> (person:('name'->str,'age'->nat)),
nat    -> (nat<=int[is>0])))]
==>_
mmlang> ('name'->'marko','age'->0)                => person
language error: ('name'->'marko','age'->0) is not a person
mmlang> ('name'->'marko','age'->29)               => person
==>person:('name'->'marko','age'->nat:29)
mmlang> ('name'->'marko','age'->29,'alive'->true) => person
==>person:('name'->'marko','age'->nat:29)``````

##### Refinement Types

Refinement types extend a language’s base types with predicates that further refine (constrain) the base type values. A classic example is the set of natural numbers (\mathbb{N}) as 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, the above is written `int[is>0]` which is the sugar form of `int{?}<=int[is,[gt,0]]`.

``````mmlang> :[model,mm][define,nat<=int[is>0]]
==>_[define,nat<=int[is,bool<=int[gt,0]]]
mmlang> 10 => nat
==>nat:10
mmlang> -1 => nat
language error: -1 is not a nat
mmlang> 10 => nat[plus,5]
==>nat:15
mmlang> 10 => nat[plus,5][plus,-15]
language error: 0 is not a nat``````
##### Dependent Types
``````mmlang> :[model,mm][define,vec:(lst,int)<=lst-<(_,=(_)>-[count]),
mmlang> (1;2;3)   => vec                                               (1)
==>vec:(((1;2;3),1),2)
mmlang> (1;2;3)   => vec => single                                     (2)
==>single:1
mmlang> (1;2;3;4) => vec                                               (3)
==>vec:(((1;2;3;4),1),2)
mmlang> (1;2;3;4) => vec => single                                     (4)
==>single:1``````
 1 A `;-lst` of 3 terms is morphed into a `vec` using the `vec<=lst` type. 2 The `vec` is morphed into a `single` using the first `single<=vec` type. 3 A `;-lst` of 4 terms is morphed into a `vec`. 4 The `vec` is morphed into a `single` using the second `single<=vec` type.
##### Recursive Types

A recursive type’s definition contains a reference to itself. Recursive type definitions require a base case to prevent an infinte recursion. Modern programming languages support generic collections, where a list can be defined to contain a particular type. For example, a `lst` containing only `ints`.

``````mmlang> :[model,mm][define,xlist<=lst[[is,[empty]]|
[is,[tail][a,xlist]]]]]
mmlang> ( ) => [a,xlist]
==>true
mmlang> ('a';'b';'c') => [a,xlist]
==>true
mmlang> ('a';'b';'c') => xlist
==>xlist:('a';'b';'c')
mmlang> (1;'a';'c') => xlist
language error: (1;'a';'c') is not a xlist
mmlang> ('a';'b';'c') => xlist[put,0,3]
language error: (3;'a';'b';'c') is not a xlist``````
``````mmlang> :[model,mm][define,ylist<=lst[[is,[empty]]|
[is,[tail][tail][a,ylist]]]]]
mmlang> ( ) => [a,ylist]
==>true
mmlang> ('a';1;'b';2) => [a,ylist]
==>true
mmlang> ('a';1;'b';2) => ylist
==>ylist:('a';1;'b';2)
mmlang> (1;'a';'c') => ylist
language error: (1;'a';'c') is not a ylist
mmlang> ('a';1;'b';2) => ylist[put,0,3]
language error: (3;'a';1;'b';2) is not a ylist``````

## The Algebra

### The Obj Monoid

Monoids

A monoid is a structure of the form (A,\cdot,\mathbf{1}), where A is the carrier set closed under the associative binary operator \cdot: A \times A \rightarrow A with \mathbf{1} \in A being the identity such that for every a,b,c \in A, (a \cdot b) \cdot c = a \cdot (b \cdot c) and a \cdot \mathbf{1} = \mathbf{1} \cdot a = a.

The `obj` monoid is defined $(\texttt{obj},⇒,\mathbf{1},\mathbf{0}),$ where `obj` is the set of all quantified mm-ADT objects,  ⇒: \tt{obj} \times \tt{obj} \rightarrow \tt{obj} the associative binary juxtaposition operator (`[juxta]` \in `inst`), \mathbf{1} the identity element `_{1}` (or simply `{1}`), and \mathbf{0} is the annihilator `_{0}` (or simply `{0}`). Given that an `obj` is either a type or a value, ⇒ supports four argument combinations.

arguments name equation mmlang example

value/value

push

a_{q_0} ⇒ b_{q_1} = b_{q_0 \ast q_1}

``````mmlang> 'a'{2} => 'b'{6}
==>'b'{12}``````

value/type

evaluate

a_{q_0} ⇒ b_{q_1} = b(a)_{q_0 \ast q_1}

``````mmlang> 'a'{2} => str{2}[plus,'b']{6}
==>'ab'{12}``````

type/value

push

a_{q_0} ⇒ b_{q_1} = b_{q_0 \ast q_1}

``````mmlang> str[plus,'a']{2} => 'b'{6}
==>'b'{12}``````

type/type

compile

a_{q_0} ⇒ b_{q_1} = b(a)_{q_0 \ast q_1}

``````mmlang> str[plus,'a']{2} => str{2}[plus,'b']{6}
==>str{12}<=str[plus,'a'][plus,'b']{12}``````

For the two x ⇒ \tt{type} argument patterns, the type acts on x — i.e., \tt{type}(x). The ⇒ operator is a higher order function, where the semantics of the application are in the type’s definition. For instance, in the expression `'a' => str[plus,'b']`, `'a'` is being applied to `str[plus,'b']`, and only when `str[plus,'b']` acts on `'a'` is ⇒ full defined. Thus, the complexity of the `obj` monoid lies in the elements of its carrier set — in particular, in the virtual machine’s instruction set architecture (`inst`).

The `obj` monoid’s ⇒ operator is a sugar symbol denoting the instruction `[juxta]`. Furthermore, `[juxta]` is one of three mm-ADT instructions in `inst` that provide direct access to the underlying stream ring algebra where `[juxta]` is the `inst` denotation of the \ast-operator of the stream ring. With the + and \oplus operators being denoted in `inst` via `[branch]` and `[barrier]`, respectively, their exists an isomorphism between `obj` monoid and the stream ring.

$\begin{split} a * b \;\;\mapsto&\;\; a \Rightarrow b \\ a + b \;\;\mapsto&\;\; \texttt{[branch,(a,b)]} \\ a \oplus b \;\;\mapsto&\;\; \texttt{[a,b]} \Rightarrow \texttt{[barrier]} \\ \mathbf{1} \;\;\mapsto&\;\; \mathbf{1} \\ \mathbf{0} \;\;\mapsto&\;\; \mathbf{0} \end{split}$

### The Inst Monoid

Free Algebra

A magma algebra is defined by a carrier set A along with a binary operator \cdot: A \times A \to A that combines and two A-elements into one (a \cdot b \mapsto c), and a set of axioms denoting "hardcoded" A-related equations that a structure must obey should it be an instance of the algebra (A,\cdot).

With the more concise representation of ab \equiv a \cdot b, if a,b,c \in A, and ab = c, then should there be another element d \in A such that ad = c, it is unknown whether ab or ad was used to derive c. Assuming the general case that all elements do not have unique two element factors in A, then the binary operator \cdot is an irreversible, lossy operation.

A sequence of \cdot-compositions can be stored in a list. Such structures are A-"programs" that can be executed against any A-machine. If a,b,c,d,e \in A, then an example A-program is $aabbbcadebdcaecadeeeeabccbcaabb.$ While the individual elements of the A-program are in A, the program as a whole is a single element in A^\ast. A^\ast is the infinite set of all possible A-element sequences of arbitrary length called the Kleene closure over A. From this vantage point, the elements of A are called letters and the elements of A^\ast are called words. The set A^\ast is the carrier set of another algebra (A^\ast,\circ), where \circ: A^\ast \times A^\ast \to A^\ast concatenates two words into a single word (i.e. list concatenation). This algebra is used to "code" A-programs. In the world of abstract algebra, this new (A^\ast,\circ) algebra is called the free algebra over A.

A word in A^\ast can be reduced to a single letter in A via a homomorphism that relates (A^\ast,\circ) and (A,\cdot) denoted \eta: A^\ast \to \A . Thus, given any A^\ast-program, \eta "executes" the program on some A-machine. If the \eta-mapping is preserved, then the answer to whether c was arrived at via ab or ad is known. mm-ADT preserves such mappings in a structure known as the `obj` graph. mm-ADT’s graph-encoding of a free algebraic trace is the foundation of numerous mm-ADT capabilities including abstract interpretation, program state, metaprogramming, and reversible computing.

The mm-ADT virtual machine’s instruction set architecture (ISA) is denoted `inst` \subset `obj`. In `mmlang`, an `inst` is defined by the grammar fragment

`inst ::= '[' op(','obj)* ']' q?`,

where `op` is an opcode from a predefined set of character string. Example opcodes include `plus`, `mult`, `branch`, `is`, `gt`, `lt`, etc. An mm-ADT program is a sequence of instructions commonly known as bytecode. While an mm-ADT program can be realized as a ring of types and values being added and multiplied, there is a faithful embedding of this richer ring structure into a syntactic monoid called the `inst` monoid defined as $(\texttt{inst}^\ast,\circ,\emptyset),$ where \circ:\tt{i\nst}^\ast \times \tt{i\nst}^\ast \to \tt{i\nst}^\ast concatenates `inst` sequences and \emptyset is the empty set behaving as the identity element. An mm-ADT program is a type. In order to generate a type from a word of the free `inst` monoid, there exists a homomorphism (assembler) from the `inst` monoid to the previously defined `obj` monoid (\tt{obj},\Rightarrow,\mathbf{1},\mathbf{0}).

Table 2. Rosetta Stone

`inst`

ISA

`inst`

`inst*`

bytecode

`inst` `poly`

\eta

assembler

type induction

`type`

program

type

`inst` monoid to `obj` monoid homomorphism

$\begin{split} & \eta: \texttt{inst}^\ast &\to \texttt{type} \\\\ & \eta(\emptyset) &= \mathbf{1} \\ & \eta(a \circ b) &= a \Rightarrow b \\\\ & \eta(x) &= \prod_{i=0}^n x_i \\ & &= x_0 \Rightarrow x_1 \Rightarrow \ldots \Rightarrow x_n \end{split}$

 For example, given the free `inst` monoid word abcde \in \tt{i\nst}^\ast, then $\eta(abcde) \mapsto a ⇒ b ⇒ c ⇒ d ⇒ e.$ ``````mmlang> [start,int][plus,1][mult,2] ==>int[plus,1][mult,2] mmlang> [start,int]=>[plus,1]=>[mult,2]=>{1} ==>int[plus,1][mult,2]``````

### The Stream Ringoid

Stream Ring Theory

Stream ring theory studies a particular type of algebraic ring constructed from a direct product of a function semiring and coefficient ring. Along with the standard ring axioms over \ast and  \+, the theory requires that every stream ring uphold five additional axioms regarding coefficient dynamics. Categorically, every stream ring forms an additive category with biproducts. A biproduct has both projection (product) and injection (coproduct) morphisms that capture the splitting and merging of streams. Along with the atemporal stream theorem derived from the stream ring axioms, biproduct streams have practical significance in asynchronous distributed computing environments that primarily enjoy embarrassingly parallel processing, but where, at certain space and time synchronization points, data needs to be co-located by the reduce near-ring operator \oplus.

mm-ADT adopts the algebra of stream ring theory, but uses the term instruction for function and quantifier for coefficient. Moreover, mm-ADT extends stream ring theory with an inductive, dependent type theory based on a multi-sorted stream ring with interval quantifiers called the type ringoid.

The `obj` stream ringoid is the algebraic ring $(\texttt{obj},[,],[;],\;\mathbf{0}\;\mathbf{1}),$

where

• `obj` is the set of all quantified objects,

• `[,]` the additive parallel branch operator,

• `[;]` the multiplicative serial chain operator,

• \mathbf{0} the additive identity, and

• \mathbf{1} the multiplicative identity.

Given \tt{obj} = \tt{type} + \tt{value} and the suggestive illustration above, the stream ringoid’s binary operators

• ,;: \tt{type} \times \tt{type} \to \tt{type} generate functions graph (program compilation) and,

• ,;: \tt{value} \times \tt{type} \to \tt{value} stream values through the type structure (program evaluation).

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.

 The `mmlang` examples are rife with syntactic sugars. The term `_{0}` (sugar’d `{0}`) is \mathbf{0}, `_{1}` (sugar’d `{1}`) is \mathbf{1}, `[a,b,c]` denotes `[branch,(a,b,c)]` and `+{q}n` denotes `[plus,n]{q}`. Finally, while `[,]` and `[;]` are defined as binary operators, due to the associativity axioms of the respective additive group and multiplicative monoid of a ring, `[,]` and `[;]` are effectively n-ary operators and will be used as such in examples to follow.

#### Ring Axioms

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.

axiom equation mmlang values mmlang types

Additive Abelian Group — (\tt{obj},[,],\mathbf{0})

$\begin{split} &(a+b)+c \\ =& a+(b+c) \end{split}$

``````mm> [['a','b'],'c']
==>'a'
==>'b'
==>'c'
mm> ['a',['b','c']]
==>'a'
==>'b'
==>'c'``````

``````mm> str[[[id],[id]],[id]]
==>str{3}<=str[id]{3}
mm> str[[id],[[id],[id]]]
==>str{3}<=str[id]{3}``````

$\begin{split} &a+b \\ =& b+a \end{split}$

``````mm> ['a','b']
==>'a'
==>'b'
mm> ['b','a']
==>'b'
==>'a'``````

``````mm> str[[id]{2},[id]{3}]
==>str{5}<=str[id]{5}
mm> str[[id]{3},[id]{2}]
==>str{5}<=str[id]{5}``````

$a+\mathbf{0} = a$

``````mm> ['a',{0}]
==>'a'``````

``````mm> str[[id],{0}]
==>str``````

$a + ({-a}) = \mathbf{0}$

``````mm> ['a','a'{-1}]
mm>``````

``````mm> str[[id],[id]{-1}]
mm>``````

Multiplicative Monoid — (\tt{obj},[;],\mathbf{1})

Multiplicative associativity

$\begin{split} &(a \cdot b) \cdot c \\ =& a \cdot (b \cdot c) \end{split}$

``````mm> [['a';'b'];'c']
==>'c'
mm> ['a';['b';'c']]
==>'c'``````

``````mm> str[[[id];[id]];[id]]
==>str
mm> str[[id];[[id];[id]]]
==>str``````

Multiplicative identity

$a \cdot \mathbf{1} = a$

``````mm> ['a';{1}]
==>'a'``````

``````mm> str[[id];{1}]
==>str``````

Ring with Unity — (\tt{obj},[,],[;],\mathbf{0},\mathbf{1})

Left distributivity

$\begin{split} &a \cdot (b + c) \\ =& ab + ac \end{split}$

``````mm> ['a';['b','c']]
==>'b'
==>'c'
mm> [['a';'b'],['a';'c']]
==>'b'
==>'c'``````

``````mm> str[[id];[[id],[id]]]
==>str{2}<=str[id]{2}
mm> str[[[id];[id]],[[id];[id]]]
==>str{2}<=str[id]{2}``````

Right distributivity

$\begin{split} &(a+b) \cdot c \\ =& ac + bc \end{split}$

``````mm> [['a','b'];'c']
==>'c'{2}
mm> [['a';'c'],['b';'c']]
==>'c'{2}``````

``````mm> str[[[id],[id]];[id]]
==>str{2}<=str[id]{2}
mm> str[[[id];[id]],[[id];[id]]]
==>str{2}<=str[id]{2}``````

##### Ring Theorems

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.

theorem equation mmlang values mmlang types

Ring with Unity — (\tt{obj},[,],[;],\mathbf{0},\mathbf{1})

$\begin{split} &a + b = a + c \\ ⇒& b = c \end{split}$

Unique factoring

$\begin{split} &a + b = \mathbf{0} \\ ⇒& a = -b \\ ⇒& b = -a \end{split}$

Inverse distributivity

$\begin{split} &-(a+b) \\ =& (-a) + (-b) \end{split}$

``````mm> ['a','b']{-1}
==>'a'{-1}
==>'b'{-1}
mm> ['a'{-1},'b'{-1}]
==>'a'{-1}
==>'b'{-1}``````

``````mm> str[[id],[id]]{-1}
==>str{-2}<=str[id]{-2}
mm> str[[id]{-1},[id]{-1}]
==>str{-2}<=str[id]{-2}``````

Inverse distributivity

$-(-a) = a$

``````mm> ['a'{-1}]{-1}
==>'a'``````

``````mm> str[[id]{-1}]{-1}
==>str``````

Annihilator

$\begin{split} &a*\mathbf{0} \\ =& \mathbf{0} \\ =& \mathbf{0}*a \end{split}$

``````mm> ['a';{0}]
mm>
mm> [{0};'a']
mm>``````

``````mm> str[[id];{0}]
mm>
mm> str[{0};[id]]
mm>``````

Factoring

$\begin{split} &a * (-b) \\ =& -a * b \\ =& -(a*b) \end{split}$

``````mm> ['a';'b'{-1}]
==>'b'{-1}
mm> ['a'{-1};'b']
==>'b'{-1}
mm> ['a';'b']{-1}
==>'b'{-1}``````

``````mm> str[[id];[id]{-1}]
==>str{-1}<=str[id]{-1}
mm> str[[id]{-1};[id]]
==>str{-1}<=str[id]{-1}
mm> str[[id];[id]]{-1}
==>str{-1}<=str[id]{-1}``````

Factoring

$\begin{split} &(-a) * (-b) \\ =& a * b \end{split}$

``````mm> ['a'{-1};'b'{-1}]
==>'b'
mm> ['a';'b']
==>'b'``````

``````mm> str[[id]{-1};[id]{-1}]
==>str
mm> str[[id];[id]]
==>str``````

#### Stream Ring Axioms

Ringoids

An algebraic ring (A,+,\ast,\mathbf{0},\mathbf{1}) is composed of an additive abelian group (A,\+,\mathbf{0}) and a multiplicative monoid (A,\ast,\mathbf{1}) that share the same carrier set A and whose operators are bound by the axiom of distributivity that requires $a \ast (b + c) = ab + ac \\ (a + b) \ast c = ac + bc.$ A ringoid generalizes a ring with a multi-sorted carrier A = (A_0,A_1,\ldots,A_n) such that the magmas of the binary operators are partial functions lacking closure. In other words, a ringoid is a ring with a type system with the consequence that for any element a \in A_i and b \in A_j, it is not required that a + b nor a \ast b be defined.

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 algebra underlying most type theories operate as a semiring(oid), where the additive component is a monoid as opposed to an invertible group. In mm-ADT, the elements of the additive component can be inverted by their corresponding negative type (or negative `obj` in general). Thus, mm-ADT realizes an additive groupoid, where, for example, the `,-poly` `[int{1},int{-1}]` is `int{0}` which is isomorphic to the initial `obj{0}`.
axiom equation mmlang values mmlang types

Bulking

$\begin{split} & xa + ya \\ =& (x+y)a \end{split}$

``````mm> ['a'{2},'a'{3}]
==>'a'{5}``````

``````mm> str[[id]{2},[id]{3}]
==>str{5}<=str[id]{5}``````

Applying

xa \ast yb = (xy)ab

``````mm> 'a'{2}['b'{3}]
==>'b'{6}``````

``````mm> str{2}[[id]{3}]
==>str{6}<=str{2}[id]{3}``````

Splitting

$\begin{split} & xa \ast (yb + zc) \\ =& (xy)ab + (xz)ac \end{split}$

``````mm> 'a'{2}['b'{3},'c'{4}]
==>'b'{6}
==>'c'{8}
mm> ['b'{6},'c'{8}]
==>'b'{6}
==>'c'{8}``````

``````mm> str{2}[[id]{3},[id]{4}]
==>str{14}<=str{2}[id]{7}
mm> str[[id]{6},[id]{8}]
==>str{14}<=str[id]{14}``````

Merging

$\begin{split} & ((xa) + (yb)) \\ =& (xa + yb) \end{split}$

``````mm> [['a'{2}],['b'{3}]]
==>'a'{2}
==>'b'{3}
mm> ['a'{2},'b'{3}]
==>'a'{2}
==>'b'{3}``````

``````mm> str[[[id]{2}],[[id]{3}]]
==>str{5}<=str[id]{5}
mm> str[[id]{2},[id]{3}]
==>str{5}<=str[id]{5}``````

Removing

$(\mathbf{0}a + b) = b$

``````mm> ['a'{0},'b']
==>'b'``````

``````mm> str[{0},[id]]
==>str``````

##### Stream Compression

The bulking, merging, and removing axioms are aimed at reducing the amount of data flowing through a stream, while the splitting and applying axioms maintain quantifier semantics as elements of the object semiring are operated on. When only considering the standard ring axioms, the stream

 ``````mmlang> ['a','a','b','a','b','b','a','a'] ==>'b'{3} ==>'a'{5} mmlang> ['a'{5},'b'{3}] ==>'a'{5} ==>'b'{3}``````

$[ a,a,b,a,b,b,a,a ]$ is irreducible. However, with the stream ring axioms and \mathbb{Z}-quantifiers, the above stream is equivalent to $[ 5a,3b ],$ where the abelian group operator `[,]` is commutative — i.e., [ 5a,3b ] \equiv [3b,5a].

Stream compression is achieved by removing redundant information in a lossless manner such that enumeration is replaced with quantification. From a data structure perspective, an unordered collection is converted into a weighted multiset. Relying on the same axiomatic principle, but reframed in terms of types (programs), the atemporal stream theorem guarantees equivalent outcomes for both synchronous and asynchronous execution strategies.

##### Asynchronous Types

The two examples below highlight this time/space entailment, where the former realizes a compile time optimization and the latter a runtime optimization.

 Expressions of the form `-<(a,b,c)>-` are decomposed representations of `[a,b,c]`, where `-<(a,b,c)` splits, but does not merge.
 ``````mmlang> 5 => int+1 ==>6 mmlang> 5 => int+1-<(_,_) ==>(6{2}) mmlang> 5 => int+1-<(*2,*2) ==>(12{2}) mmlang> 5 => int+1-<(*2,*2)>- ==>12{2} mmlang> 5 => int+1-<(*2,*2)>-+2 ==>14{2}`````` ``````mmlang> 5 => int+1*{2}2+2 ==>14{2}`````` ``````mmlang> 5 => int+1 ==>6 mmlang> 5 => int+1-<(_,_) ==>(6{2}) mmlang> 5 => int+1-<(*2,+6) ==>(12{2}) mmlang> 5 => int+1-<(*2,+6)>- ==>12{2} mmlang> 5 => int+1-<(*2,+6)>-+2 ==>14{2}`````` ``````mmlang> 5 => int-<(+1*2+2,+1+6+2) ==>(14{2}) mmlang> 5 => int-<(+1*2+2,+1+6+2)>- ==>14{2}``````

As a ring, an mm-ADT `obj` can be multiplied or added to another `obj`. Multiplication is denoted with `=>` (`5 => int+2`) or simple term juxtaposition (`5+2`). Addition, on the other hand, is realized by the `[branch]` instruction which has an `mmlang` sugar of `[,]`. The way in which `obj` addition effects the `obj` graph is important.

``````mmlang> int => int[+4[is>0],*5]+1                                                   (1)
==>int{1,2}<=int[int{?}<=int[plus,4][is,bool<=int[gt,0]],int[mult,5]][plus,1]
mmlang> 2 => int[+4[is>0],*5]+1                                                     (2)
==>7
==>11
mmlang> 2 => int[+4[is>0],*5]+1[path]                                               (3)
==>(2;[plus,4];6;[is,true];6;[plus,1];7)
==>(2;[mult,5];10;[plus,1];11)
mmlang> 2 => int[+4[is>0],*5]+1[type]                                               (4)
==>int{?}<=int[plus,4][is,bool<=int[gt,0]][plus,1]
==>int[mult,5][plus,1]``````
 1 The `int`-dependent type clones the `int` to the two branches, merges the branch output, and adds `1` (compilation). 2 `2` is propagated through the `int{1,2}<=int` type (evalution). 3 The path through the `obj` value graph taken by the resultant `objs`. 4 The type of each resultant value.

The compilation of the `int{1,2}<=int` type generates the path diagrammed below in the type subgraph of the `obj` graph.

The evaluation of the type with the input of `2` generates two paths through the value subgraph of the `obj` graph — via split (\Delta) and merge (\nabla). Branching (addition) is one of two fundamental operations in the mm-ADT ring algebra. It is not manifested as an `inst` in a value’s path history. Likewise, the other fundamental operation, `=>` (multiplication) has no explicit `inst` and is denoted with juxtaposition in the value path history. The significance of branching being fundamental in mm-ADT is that individual branches can evaluate in decoupled, independent manner requiring no synchronization nor explicit coordination at merge.

Deep Dive 5. Process Architectures Sympathetic to the Type Ringoid

An `mmlang` expression denotes a type (program) that is executed by a processor. A type is an element of the type ringoid algebra. The type ringoid is not the intended algebra of the language component. The reason being, languages yield linear structures. A linear medium is sympathetic to single operator magmas such as monoids or groups. In order to express addition (branching) in these structures, the parallel branches are serially embedded using the `[,]` syntactic hack.

The type elements of the type ringoid are three dimensional structures (where the third dimension captures nesting) and have a more natural embedding in the spatial component of the physical world. Computationally, types are evaluated by processors across a number of cores of a single machine and/or across a multi-machine compute cluster. The type ringoid algebra yields types that are sympathetic to a variety of modern processor architectures.

1. Iterator: single threaded, pull-based, lazily evaluated, functionally oriented

2. Reactive: multi-threaded, push-based, lazily evaluated, stream oriented

3. Bulk Synchronous Parallel: cluster, pull-based, eagerly evaluated, pipeline oriented

4. Message-Passing; cluster/multi-threaded, push-based, lazily evaluated, actor oriented

##### Commuting Quantifiers
 Each of these expressions is equivalent to `obj{0}`. This is demonstrated using the `;-poly` quantifier equation. `2*3*0 = 2*0*4 = 0*3*4`. In general, if there exists a 0-quantified `obj` in a `obj` monoid expression, then the result is always `obj{0}`. ``````mmlang> 6{2}+{3}1+{0}2 mmlang> mmlang> 6{2}+{0}1+{4}2 mmlang> mmlang> 6{0}+{3}1+{4}2 mmlang>`````` All three expression evaluate to the same `9{24}` value. The quantifier ring has a commutative multiplicative monoid such that `2*3*4 = 3*4*2 = 4*2*1`. ``````mmlang> 6{2}+{3}1+{4}2 ==>9{24} mmlang> 6{3}+{4}1+{2}2 ==>9{24} mmlang> 6{4}+{2}1+{3}2 ==>9{24}`````` If the quantifier ring is not commutative, it is still possible to propagate coefficients left or right through an `obj` `*`-expression. Regardless of the quantifiers being prime elements, quantifier propagation need not preserve the factors of a `*`. In this way, if the geometric sequence remains the same, any quantifier distribution is allowed. ``````mmlang> 6{2}+{3}1+{4}2 ==>9{24} mmlang> 6+{6}1+{4}2 ==>9{24} mmlang> 6+1+{24}2 ==>9{24} mmlang> 6+{12}1+{2}2 ==>9{24} mmlang> 6{6}+{2}1+{2}2 ==>9{24}`````` Quantifiers propagate along the the multiplicative `obj` monoid via their `*`-operator. They propagate along the additive `obj` group via their `+`-operator. In this way, if two branches have orthogonal quantifiers of the same magnitude, then when they leave the `+`-group to be additively merged onto the `*`-monoid, they cancel each other out. Various set theoretic and quantum operations make use of constructive and deconstructive quantifier interference when computing. ``````mmlang> 6[+{-1}1+{2}1,+{2}2] mmlang> mmlang> 6[+{-1}1+1,+2]{2} mmlang> mmlang> 6{2}[+{-1}1+1,+2] mmlang>``````

#### Stream Module Axioms

Modules

A module for a group (A,+\_A,\mathbf{0}_A) is a ring (X, +_X ,\ast_X, \mathbf{0}_X, \mathbf{1}_X ) such that elements of X act on elements of A via a function \cdot: X \times A \to A called scalar multiplication. If A = X, the action is defined by the ring’s multiplicative operator. However, when A \ne X and moreover, when A and/or X is free, a ring theoretic interpretation of linear algebraic emerges with A-based vectors (free magma) and matrices (two free magmas) being operated by X scalars, vectors, and matrices. The axioms for both left and right modules are provided below, where if A is an abelian group, then X is a bimodule and both sets of axioms hold.

Left X-Module Axioms Right X-Module Axioms

x \cdot (a +_A b) = (x \cdot a) +_A (x \cdot b)

(a +_A b) \cdot x = (a \cdot x) +_A (b \cdot x)

(x +_X y) \cdot a = (x \cdot a) +_A (y \cdot a)

a \cdot (x +_X y) = (a \cdot x) +_A (a \cdot y)

(x \ast_X y) \cdot a = x \cdot (y \cdot a)

a \cdot (x \ast_X y) = (a \cdot x) \cdot y

\mathbf{1}_X \cdot a = a

a \cdot \mathbf{1}_X = a

Deep Dive 6. Poly Constructs in mmlang
name mmlang latex description

split

`-<`

\Delta

scalar `*`

merge

`>-`

\nabla

fold `+` (linear combine)

branch

`[ ]`

◊

scalar `*` then fold `+`

combine

`=`

\circ

pairwise juxtaposition

1. `( )` is a polynomial constructor.

2. `lst` is a polynomial with terms indexed by `int`.

3. `rec` is a polynomial with terms indexed by `obj`.

4. `,` is a polynomial term deliminator denoting parallel compose.

5. `|` is a polynomial term deliminator denoting parallel choose.

6. `;` is a polynomial term combinator denoting serial compose.

Modules introduce a new scalar multiplication binary operator cdot: X \times A \to A typically denoted as X/A-element juxtaposition. In mm-ADT, the module expression $x \cdot (a + b) \mapsto (xa + xb)$ is realized as $x \Delta (a + b) \mapsto (x⇒a,x⇒b).$ The \Delta (split) copys an `obj` that is outside of a `poly` to the left of one or more `objs` inside the `poly`. When juxtaposed to the left and an internal `obj`, the `obj` monoid’s binary operator ⇒:\tt{obj} \times \tt{obj} \to \tt{obj} determines the type/type, value/type, value/value, type/value resolution. The following table provides a translation of the standard module axioms to mm-ADT.

Left X-Module Axioms

$x \cdot (a +_A b) = (x \cdot a) +_A (x \cdot b)$

$[x;[a,b]] = [[x;a],[x;b]]$

$x \Delta (a,b) = (x⇒a,x⇒b)$

$(x +_X y) \cdot a = (x \cdot a) +_A (y \cdot a)$

$[ [x,y];a] = [[x;a],[y;a]]$

$(x,y) \nabla a = (x⇒a,y⇒a)\nabla$

$(x \ast_X y) \cdot a = x \cdot (y \cdot a)$

$[[x;y];a] = [x;y;a]$

$(x;y) \nabla a = x⇒y⇒a$

$\mathbf{1}_X \cdot a = a$

$[\mathbf{1};a] = a$

$\mathbf{1}⇒a = a$

Right X-Module Axioms

$(a +_A b) \cdot x = (a \cdot x) +_A (b \cdot x)$

$[ [a,b];x] = [[a;x],[b;x]]$

$(a,b) \nabla x = (a⇒x,b⇒x)\nabla$

$a \cdot (x +_X y) = (a \cdot x) +_A (a \cdot y)$

$[a;[x,y]] = [[a;x],[a;y]]$

$a \Delta (x,y) = (a⇒x,a⇒y)$

$a \cdot (x \ast_X y) = (a \cdot x) \cdot y$

$[a;[x;y]] = [a;x;y]$

$a \Delta (x;y) = (a⇒x;a⇒x⇒y)$

$a \cdot \mathbf{1}_X = a$

$[a;\mathbf{1}] = a$

$a⇒\mathbf{1} = a$

##### Polynomials
 The reason for the `[split]` sugar symbol `-<`, is that it represents one wire (`-`) splitting into many (`<`). Likewise, the reason for `>-` being the `[merge]` sugar symbol is it represents many wires merging (`>`) into one (`-`). Finally, `[combine]` has a sugar of `=` which represents parallel wires being operated on independently.

A polynomial is a linear combination of terms composed of coefficients and indeterminates typically expressed as $f(x) = q_1 x^1 + q_2 x^2 + q_3 x^3 + \ldots + q_n x^n,$ where q_i is a coefficient, x^i is an indeterminate raised to the i^\text{th} power, q_i x^i is a term, and the terms are linearly combined via +. If x \in \mathbb{Z}, then the signature of f is f: \mathbb{Z} \to \mathbb{Z}. When f(x) is evaluated with some x \in \mathbb{Z}, x becomes determined and the polynomial is reduced to a single \mathbb{Z}. For instance, $f(x) = 2x + 3x^2 + 6x^3$ is irreducible due to x being an indeterminant variable. If x =4, then the polynomial is solved via the reduction $\begin{split} f(4) &= (2 \ast 4) + (3 \ast 4^2) + (6 \ast 4^3) \\ &= (2 \ast 4) + (3 \ast 16) + (6 \ast 64) \\ &= 8 + 48 + 384 \\ &= 440. \end{split}$

In mm-ADT, `poly` \subset `obj` is the (infinite) set of polynomials. The polynomial expression above is a `,-poly` \subset `poly` (pronounced "comma poly") and, in `mmlang`, are expressions of the form

`x => [x1{q1},x2{q2},x3{q3},…​,xn{qn}]`

where `qi` is a quantifier (coefficient), `xi` is a type (indeterminate), `xi{qi}` is a quantified type (term), and the type are linearly combined via `[,]` (addition). Instead of the terms being raised to a power (as is typical of numeric polynomials), `,-poly` terms are "raised" to a type with instructions. This is type exponentiation which is the type-equivalent of numeric exponentiation.

The aforementioned polynomial f: \mathbb{N} \to \mathbb{N} is denoted in mm-ADT by the following `int<=int` type.

``````mmlang> int => [int[id]{2},int[mult,int]{3},int[mult,[mult,int]]{6}][sum]
==>int[int{2}<=int[id]{2},int{3}<=int[mult,int]{3},int{6}<=int[mult,int[mult,int]]{6}][sum]``````

In f, addition and multiplication is with respects to the integer ring (\mathbb{Z},+,\ast,0,1). In `,-poly`, they are with respects to the stream ring, where multiplication is \Delta and addition is \nabla. The mm-ADT `,-poly` is a generalized algebraic structure known as a polynomial ring that, when used to solve `int` based polynomials, the instructions `[mult]` and `[sum]` are required, where `int<=int` type is reducible when the domain `int` is determined.

``````mmlang> 4 => [int[id]{2},int[mult,int]{3},int[mult,[mult,int]]{6}]
==>4{2}
==>16{3}
==>64{6}

mmlang> 4 => [int[id]{2},int[mult,int]{3},int[mult,[mult,int]]{6}][sum]
==>440

mmlang> 4 => [int[id]{2},int*{3}int,int*{6}*int][sum]
==>440

mmlang> [4;[int[id]{2},int*{3}int,int*{6}*int][sum]]
==>440``````

The suggestive illustration on the left depicts a single element of some (free) ring. There are four multiplicative monoid compositions diagrammed as vertical chains rooted at an a. There is single additive abelian group element diagrammed horizontally, reflecting a (commutative) linear combination of the monoid elements. As 1-dimensional horizontal and vertical structures, each depicts an element of a free magma (group or monoid), where 0-dimensional elements would be drawn from a non-free algebra. Thus, the illustration contains

1. four free monoid elements — `(a;b;c)`, `(a;d)`, `(a;b;e)`, `(a;d;e;b)`, and

2. one free group element — `((a;b;c),(a;d),(a;b;e),(a;d;e;b))`,

where, in relation to `poly`, the illustration’s `*` is denoted `;` and `+` is denoted `,`.

Each mm-ADT `poly` constrains the general construction of the illustration such that one magma remain free (unevalated) and the other non-free (evaluated). In particular, as a classic polynomial ring, a `,-poly` maintains a free additive group composed of isolated non-free multiplicative monoids. Thus, with respects to the illustration, the vertical \ast-compositions are "collapsed" yielding four terms (`objs`) that are unable to merge horizontally due to the free nature of the additive group. Thus, the `,-poly` is suggestively illustrated as

and specified in `mmlang` as

`(abc{q0},ad{q1},abe{q2},adeb{q3})`.

 For visual simplicity, quantifiers are not illustrated. Furthermore, the reason that every term of the multiplicative monoid only has a single quantifier is due to the universal commutativity of coefficients theorem of stream ring theory.
symbol structure branch use illustration

`,-poly`

polynomial ring

unordered biproducts
nondeterministic branching

`;-poly`

trace monoid

ordered biproducts
serial branching

`|-poly`

monoid ring

unary biproducts
deterministic branching

 `,-poly` $[f,g] = \nabla \circ \Delta (f,g) = \Diamond(f,g)$ copy/clone-branching independent terms $A \times A = 2A$ `;-poly` $[f;g] = \nabla \circ \Delta (f;g) = \Diamond(f;g)$ serial/compose-chain dependent terms $A^{_A A} = A$ `|-poly` $[f | g] = \nabla \circ \Delta (f | g) = \Diamond(f | g) \\$ $\nabla \circ \iota_x \circ f \circ \pi_x \circ \Delta = B \\ \nabla \circ \iota_y \circ g \circ \pi_y \circ \Delta = \mathbf{0} \\ x \neq y$ either/choice-branching dependent terms $A + A = A$

In mm-ADT, `polys` are both `obj` products and coproducts—​called biproducts. They have projections (`[get]`) and injections (`[put]`) such that the following diagram commutes.

###### ,-poly
`,-lst` `,-rec`

``````mmlang> 'x'-<(+'a',+'b',+'c')
==>('xa','xb','xc')
mmlang> 'x'-<(+'a',+'b',+'c')>-
==>'xa'
==>'xb'
==>'xc'``````

``````mmlang> 'x'-<(+'s'->+'a',+'r'->+'b',+'t'->+'c')
==>('xs'->'xa','xr'->'xb','xt'->'xc')
mmlang> 'x'-<(+'s'->+'a',+'r'->+'b',+'t'->+'c')>-
==>'xa'
==>'xb'
==>'xc'``````

\nabla on value ,-poly
``````mmlang> (1,2,3)>-
==>1
==>2
==>3
mmlang> (1,,3)>-
==>1
==>3
mmlang> (,,3)>-
==>3``````

``````mmlang> ('a'->1,'b'->2,'c'->3)>-
==>1
==>2
==>3
mmlang> ('a'->1,,'c'->3)>-
==>1
==>3
mmlang> (,,'c'->3)>-
==>3``````

A `,-poly` (pronounced "comma poly") is a classic polynomial ring composed of a free additive abelian group and a non-free multiplicative monoid. If a,b \in \tt{object} and q_0, q_1 \in \tt{q} are elements comprising `obj` products, then the additive operator of the `obj` stream ring is defined as $[a_{q_0},b_{q_1}] = \begin{cases} [a_{q_0+q_1}] & \text{if } a==b, \\ [a_{q_0},b_{q_1}] & \text{otherwise}, \end{cases}$

where [a_{q_0},b_{q_1}] \equiv ◊(a_{q_0},b_{q_1}) \equiv \nabla(\Delta(a_{q_0},b_{q_1}))  and + denotes the respective quantifier ring’s additive operator. Given the commutative nature of the `,-poly` abelian group, the terms can be rearranged. In stream ring theory, this equality is known as the bulking axiom and it is of fundamental importance to efficient stream-based computing with benefits realized in both the time and space dimensions.

[a_{q_0},b_{q_1}] x_{q_2}[a_{q_0},b_{q_1}]

When applying x \in \tt{obj}, the `,-poly` group is a right action on x satisfying the equation below. As an algebraic module, x is an element of the right `,-poly` module `obj` realizing a generalized form of scalar multiplication.

$x_{q_2}[a_{q_0},b_{q_1}] = \begin{cases} [{xa}_{q_2*(q_0+q_1)}] & \text{if } a==b, \\ [{xa}_{q_2*q_0},{xb}_{q_2*q_1}] & \text{otherwise}, \end{cases}$

The two cases above are expressed in `mmlang` below with the last two examples being the `[ ]` sugar of `-<()>-` (◊).

``````mmlang> 'x'{2}-<(+{3}'a',+{4}'a')>-
==>'xa'{14}
mmlang> 'x'{2}-<(+{3}'a',+{4}'b')>-
==>'xa'{6}
==>'xb'{8}
mmlang> 'x'{2}[+{3}'a',+{4}'a']
==>'xa'{14}
mmlang> 'x'{2}[+{3}'a',+{4}'b']
==>'xa'{6}
==>'xb'{8}``````
###### ;-poly
`;-lst` `;-rec`

``````mmlang> 'x'-<(+'a';+'b';+'c')
==>('xa';'xab';'xabc')
mmlang> 'x'-<(+'a';+'b';+'c')>-
==>'xabc'``````

``````mmlang> 'x'-<(+'s'->+'a';+'r'->+'b';+'t'->+'c')
==>('xs'->'xa';'xar'->'xab';'xabt'->'xabc')
mmlang> 'x'-<(+'s'->+'a';+'r'->+'b';+'t'->+'c')>-
==>'xabc'``````

\nabla on value ;-poly
``````mmlang> (1;2;3)>-
==>3
mmlang> (1;;3)>-
==>3
mmlang> (;;3)>-
==>3``````

``````mmlang> ('a'->1;'b'->2;'c'->3)>-
==>3
mmlang> ('a'->1;;'c'->3)>-
==>3
mmlang> (;;'c'->3)>-
==>3``````

The two magmas of `;-poly` (pronounced "semi poly") are the free and non-free forms of the `obj` stream ring’s multiplicative monoid. The terms of `;-poly` geometrically combined using the multiplicative operator ⇒ (denoted `;` in `poly`). A `;-poly` is a partially commutative monoid known as a trace monoid. If a,b,x \in \tt{objects} and q_0,q_1,q_2 \in \tt{q}, ◊(a;b) \equiv [a;b], then the `;-poly` (a_{q_0} ; b_{q_1}) acts on x_{q_2} as

$[ a_{q_0} ; b_{q_1} ](x_{q_2}) = b(a(x))_{ q_2 * q_0 * q_1 }.$

Of particular interest, when not merging (\nabla),

$\Delta(x_{q_2}, (a_{q_0} ; b_{q_1})) = ( a(x)_{ q_2 * q_0 } ; b(a(x))_{ q_2 * q_0 * q_1 } ).$

The equation above realizes a structure and process joyfully named the "bubble chamber". In experimental higher-energy physics, a bubble chamber is small room filled with high pressure vapor. Particles are shot into the room and the trace they leave (called their varpor trail) provides physicists information that they then used to understand the nature of the particle under study — e.g., its mass, velocity, spin, and, when capturing decay, the sub-atomic particles that compose it. In mm-ADT, x above (and 5 below) play the role of the particle and `;-poly` the bubble chamber with each term in the `;-poly` acting as a vapor droplet.

``````mmlang> 5-<(+1;+2;+3;+4;+5)     (1)
==>(6;8;11;15;20)
mmlang> 5-<(+1+2;+3;+4+5)       (2)
==>(8;11;20)
mmlang> 5-<(+1+2+3+4+5)         (3)
==>(20)
mmlang> 5-<(+1;+2;+3;+4;+5)>-   (4)
==>20
mmlang> 5[+1;+2;+3;+4;+5]       (5)
==>20
mmlang> 5+15                    (6)
==>20``````
 1 `5` is propagated through the `;-poly` terms leaving a trace of it’s state at each term slot. 2 Since the elements of the R-module M are in M, any monoid element is a legal term. 3 A `;-poly` with single term derived via the composition of 5 other M elements. 4 The merge operator (\nabla) emits the final term of the `;-poly`. 5 The sugar form of the previous expression. 6 The last three examples are equivalent.
###### |-poly
`|-lst` `|-rec`

``````mmlang> 'x'-<('a'{0}|+'b'|+'c')
==>('xb')
mmlang> 'x'-<('a'{0}|+'b'|+'c')>-
==>'xb'``````

``````mmlang> 'x'-<('s'{0}->+'a'|+'r'->+'b'|+'t'->+'c')
==>('xr'->'xb')
mmlang> 'x'-<('s'{0}->+'a'|+'r'->+'b'|+'t'->+'c')>-
==>'xb'``````

\nabla on value |-poly
``````mmlang> (1|2|3)>-
==>1
mmlang> (1||3)>-
==>1
mmlang> (||3)>-
==>3``````

``````mmlang> ('a'->1|'b'->2|'c'->3)>-
==>1
mmlang> ('a'->1||'c'->3)>-
==>1
mmlang> (||'c'->3)>-
==>3``````

A `|-poly` (pronounced "pipe poly") uses `|` as the `obj` term separator. Like the `,-poly`, a `|-poly` maintains a free additive group and a non-free multiplicative monoid. However, unlike `,-poly`, the additive group is not commutative. If a,b,x \in \tt{objects} and q_0,q_1,q_2 \in \tt{q}, then `|-poly` [a_{q_0} | b_{q_1}] acts on x_{q_2} as

$x_{q_2} [a_{q_0} | b_{q_1}] = \begin{cases} {xa}_{q_2 * q_0} & \text{if } x_{q_2} a_{q_0} \neq \bf{0}, \\ {bx}_{q_2 * q_1} & \text{if } x_{q_2} b_{q_1} \neq \bf{0}, \\ \bf{0} & \text{otherwise}. \end{cases}$

Thus, while `,-lst` implements union, `|-lst` implements null coalescing, where in mm-ADT, null is `obj{0}` (the zero element of the `obj` stream ring — \mathbf{0}). Like coalesce, the order in which the terms/branches are evaluated determines the result of the computation. This is the reason that the additive group of `|-lst` (and `|-poly` in general) is not commutative.

``````mmlang> 'x'{2}[+{3}'a' | +{4}'b']  (1)
==>'xa'{6}
mmlang> 'x'{2}[+{0}'a' | +{4}'b']  (2)
==>'xb'{8}
mmlang> 'x'{2}[+{0}'a' | +{0}'b']  (3)
mmlang>``````
 1 The first term applied to `x` is not `obj{0}` so `'a'` is added to `'x'`. The polynomial reduces to `[plus,'a']{3}`. 2 The first term applied to `x` is `obj{0}` and the second is not so `'b'` is added to `'x'`. The polynomial reduces to `[plus,'b']{4}`. 3 Both terms, when applied to `x` yield `obj{0}`. The polynomial reduces to `obj{0}`.

`|-rec` enables predicate-based coalescing which is a form of conditional branching realized in most programming languages as if/else and switch/case branching. While predicate-based branching is a function of \mathbb{B} (`bool`), in mm-ADT it is determined by \tt{q} (`{q}`), where false is `obj{0}` (\mathbf{0}) and true is any non-zero quantifier. The non-commutative additive group of `|-poly`, as inherited by `|-rec`, realizes case-based pattern matching branch ordering semantics. Thus, if a,b,c,d,x \in \tt{objects} and q_i \in \tt{q}, then

$x_{q_4} [a_{q_0} \to b_{q_1} | c_{q_2} \to d_{q_3}] = \begin{cases} {xb}_{q_4 * q_1} & \text{if } x_{q_4} a_{q_0} \neq \bf{0}, \\ {xd}_{q_4 * q_3} & \text{if } x_{q_4} c_{q_2} \neq \bf{0}, \\ \bf{0} & \text{otherwise}. \end{cases}$

``````mmlang> 'x'{2}[+{3}'a' -> +{4}'b' | +{5}'c' -> +{6}'d']
==>'xb'{8}
mmlang> 'x'{2}[+{0}'a' -> +{4}'b' | +{5}'c' -> +{6}'d']
==>'xd'{12}
mmlang> 'x'{2}[+{0}'a' -> +{4}'b' | +{0}'c' -> +{6}'d']
mmlang>``````

The previous `mmlang` examples are contrived. In practice, they keys of `|-rec` will typically leverage `[is,bool]` with the anonymous type `_` serving as the default case of the switch.

``````mmlang> [1,10,100]-<([is,[gt,50]] -> [plus,10] | [is,[lt,5]] -> [plus,20] | _ -> [plus,30])>-   (1)
==>21
==>40
==>110
mmlang> [1,10,100][is>50 -> +10 | is<5 -> +20 | _ -> +30]                                       (2)
==>21
==>40
==>110``````
 1 Three branches with the final branch serving as default. 2 The same expression, but leveraging `mmlang` syntax sugar.
 ``````mmlang> int{3}[is>50 -> +10 | is<5 -> +20 | _ -> +30][explain] ==>' int{3}[int{0,3}<=int{3}[is,bool{3}<=int{3}[gt,50]]->int{3}[plus,10]|int{0,3}<=int{3}[is,bool{3}<=int{3}[lt,5]]->int{3}[plus,20]|int{3}->int{3}[plus,30]] inst domain range state ------------------------------------------------------------------------------- [int{0,3}<=int{3}[is,bool{3}<=int{3}[gt,... int{3} => int{3} [is,bool{3}<=int{3}[gt,50]] int{3} => int{0,3} [gt,50] int{3} => bool{3} ->[plus,10] int{3} => int{3} [is,bool{3}<=int{3}[lt,5]] int{3} => int{0,3} [lt,5] int{3} => bool{3} ->[plus,20] int{3} => int{3} ->[plus,30] int{3} => int{3} '``````
##### Poly Factoring
``int[int+2[is>0]*5<44, int+2[is>0]*-6<44, int+2[is>0]*10+7<44]``

The above expression denotes a polynomial ring whose linearly combined terms are elements of the multiplicative monoid. With abuse of notation, the expression below binds the monoidal terms with `+` to emphasize the prototypical polynomial form q_0 x^0 + q_1x^1 + q_2x^2.

$\texttt{int+2[is>0]*5<44} \;\;+\;\; \texttt{int+2[is>0]*-6<44} \;\;+\;\; \texttt{int+2[is>0]*10+7<44}$

Rings support both left and right distributivity such that the following derivation yields the respective equivalence.

$\begin{split} abcg + abdg + abefg &= a \ast (bcg + bdg + befg) \\ &= a \ast b \ast (cg + dg + efg) \\ &= a \ast b \ast (c + d + ef) \ast g \\ \end{split}$

Thus `int+2[is>0]` is factored out on the left and `<44` is factored out on the right.

``int+2[is>0][*5,*-6,*10+7]<44``

Again with an abuse of notation to emphasize the lexical structure.

$\texttt{int+2[is>0]} \;\ast\; (\texttt{*5} \;\;+\;\; \texttt{*-6} \;\;+\;\; \texttt{*10+7}) \;\ast\; \texttt{<44}$

To be certain, both the factored and unfactored forms of the expression return the same result for the same input.

``````mmlang> 5 => [int+2[is>0]*5<44, int+2[is>0]*-6<44, int+2[is>0]*10+7<44]
==>true{2}
==>false
mmlang> 5 => int+2[is>0][*5,*-6,*10+7]<44
==>true{2}
==>false``````

A progressive split/merge example is provided to better illustrate the intermediate results of the computation.

``````mmlang> 5 => -<(int+2[is>0]*5<44, int+2[is>0]*-6<44, int+2[is>0]*10+7<44)
==>(true{2},false)
mmlang> 5 => -<(int+2[is>0]*5<44, int+2[is>0]*-6<44, int+2[is>0]*10+7<44)>-
==>true{2}
==>false

mmlang> 5 => int
==>5
mmlang> 5 => int+2
==>7
mmlang> 5 => int+2[is>0]
==>7
mmlang> 5 => int+2[is>0]-<(*5,*-6,*10+7)
==>(35,-42,77)
mmlang> 5 => int+2[is>0]-<(*5,*-6,*10+7)>-
==>35
==>-42
==>77
mmlang> 5 => int+2[is>0]-<(*5,*-6,*10+7)>-<44
==>true{2}
==>false``````
##### Poly Expansion

Polynomials are the subject of interest primarily because they contain both multiplication and addition and, through derivations, multiplication can be translated to addition and addition to multiplication. For instance, the left hand side of the the binomial below is the serial composition of two parallel branches while the right hand side is the parallelization of 4 serial compositions.

$(a+2b)(a+4b) = a^2 + 2ba + 4ab + 8b^2$

equation mmlang

$(a+b+b)(a+b+b+b)$

``````mmlang> ['a','b','b']
==>'a'
==>'b'{2}
mmlang> ['a','b','b'][count]
==>3
mmlang> ['a','b','b'][+'a',+'b',+'b',+'b',+'b']
==>'aa'
==>'ab'{4}
==>'ba'{2}
==>'bb'{8}
mmlang> ['a','b','b'][+'a',+'b',+'b',+'b',+'b'][count]
==>15``````

$(a+2b)(a+4b)$

``````mmlang> ['a','b'{2}]
==>'a'
==>'b'{2}
mmlang> ['a','b'{2}][count]
==>3
mmlang> ['a','b'{2}][+'a',+{4}'b']
==>'aa'
==>'ab'{4}
==>'ba'{2}
==>'bb'{8}
mmlang> ['a','b'{2}][+'a',+{4}'b'][count]
==>15``````

$a^2 + 2ba + 4ab + 8b^2$

``````mmlang> ['aa','ba'{2},'ab'{4},'bb'{8}]
==>'aa'
==>'ba'{2}
==>'ab'{4}
==>'bb'{8}
mmlang> ['aa','ba'{2},'ab'{4},'bb'{8}][count]
==>15``````

$a^2 + 6ab + 8b^2$

``````mmlang> ['aa','ab'{6},'bb'{8}]
==>'aa'
==>'ab'{6}
==>'bb'{8}
mmlang> ['aa','ab'{6},'bb'{8}][count]
==>15``````

##### Poly Embedding

A non-free element is a zero-dimensional point. A free element is a one-dimensional line. The carrier set of the type ringoid is formed from the union of the elements of `obj` stream ring’s free additive abelian group and free multiplicative monoid. This is the freest possible stream ring representation — a free ring. With two free magmas, the type ringoid’s elements are two-dimensional planes. One dimension represents multiplication and the other addition. The type ringoid is encoded in `mmlang` as a `,-lst` (additive) with zero or more `;-lst` (multiplicative) terms. The unfactored type from the previous section is presented, followed by its two-dimensional encoding as an element of the type ringoid.

``[int+2[is>0]*5<44, int+2[is>0]*-6<44, int+2[is>0]*10+7<44]``
``[[int;+2;[is>0];*5;_;<44],[int;+2;[is>0];*-6;_;<44],[int;+2;[is>0];*10;+7;<44]]``

In a manner analogous to polynomials in linear algebra, the free monoids of the polynomial can be organized into a matrix, where the following equations maintain `,` and `;` tokens to help orient the reader and the multiplicative identity `_` pads rows to ensure a proper n \times m-matrix.

\begin{bmatrix} \tt{int}; & +2; & \tt{[is>0]}; & *5; & \_ ; & <44, \\ \tt{int}; & +2; & \tt{[is>0]}; & *{-6}; & \_ ; & <44, \\ \tt{int}; & +2; & \tt{[is>0]}; & *10; & +7 ; & <44 \\ \end{bmatrix}

A left `obj`-module (a row vector) can be factored out of the matrix leaving an expression of the form \mathbf{v}^{\top} \mathbf{M}.

``[[int;+2;[is>0]];[[*5;<44],[*-6;<44],[*10;+7;<44]]]``

$\begin{bmatrix} \tt{int}; & +2; & \tt{[is>0]} \end{bmatrix} ; \begin{bmatrix} *5; & \_ ; & <44, \\ *{-6}; & \_ ; & <44, \\ *10; & +7 ; & <44 \\ \end{bmatrix}$

Similarly, a right `obj`-module scalar can be factored out leaving an expression of the form \mathbf{v}^{\top} \mathbf{M} u .

``[[int;+2;[is>0]];[*5,*-6,[*10;+7]];<44]``

$\begin{bmatrix} \tt{int}; & +2; & \tt{[is>0]} \end{bmatrix} ; \begin{bmatrix} *5; & \_ , \\ *{-6}; & \_ , \\ *10; & +7 \\ \end{bmatrix} ; <44$

This fully factored form can be evaluated with `obj`-scalar left multiplication.

$\begin{split} & 5; \begin{bmatrix}\tt{int}; & +2; & \tt{[is>0]} \end{bmatrix} ; & \begin{bmatrix} *5; & \_ , \\ *{-6}; & \_ , \\ *10; & +7 \\ \end{bmatrix} ; <44 \\ &= \begin{bmatrix}5; & +2; & \tt{[is>0]} \end{bmatrix} ; & \begin{bmatrix} *5; & \_ , \\ *{-6}; & \_ , \\ *10; & +7 \\ \end{bmatrix} ; <44 \\ &=7 ; \begin{bmatrix} *5; & \_ , \\ *{-6}; & \_ , \\ *10; & +7 \\ \end{bmatrix} ; <44 = & \begin{bmatrix} 35; & \_ , \\ -42; & \_ , \\ 70; & +7 \\ \end{bmatrix} ; <44 = \begin{bmatrix} 35, \\ -42, \\ 77 \\ \end{bmatrix} ; <44 =\begin{bmatrix} \tt{true}, \\ \tt{true}, \\ \tt{false} \\ \end{bmatrix} = \begin{bmatrix} \tt{true}\{ 2 \}, \\ \tt{false} \\ \end{bmatrix} \end{split}$

``````mmlang> [5;[[int;+2;[is>0]];[*5,*-6,[*10;+7]];<44]]
==>true{2}
==>false

mmlang> 5-<(int;+2;[is>0];-<(*5,*-6,-<(*10;+7)))
==>(5;7;7;(35,-42,(70;77)))
mmlang> 5-<(int;+2;[is>0];-<(*5,*-6,-<(*10;+7)>-)>-;<44)>-
==>true{2}
==>false``````

Again, to be certain, all three derivations yield the same result for the same input.

``````mmlang> [5;[[int;+2;[is>0];*5;_;<44],[int;+2;[is>0];*-6;_;<44],[int;+2;[is>0];*10;+7;<44]]]
==>true{2}
==>false
mmlang> [5;[[int;+2;[is>0]];[[*5;<44],[*-6;<44],[*10;+7;<44]]]]
==>true{2}
==>false
mmlang> [5;[[int;+2;[is>0]];[*5,*-6,[*10;+7]];<44]]
==>true{2}
==>false``````

The linear algebraic type ringoid compartmentalizes the type induced at the individual instruction-level. This is the absolutely freest representation of a ring(oid). This "cellular form" is well suited to manipulation by the processor. At compile-time, factoring a matrix representation can be leveraged for optimization and rewriting. At evaluation runtime, the free type ringoid provides a deconstructed, 2-dimensional pipeline architecture that can be partitioned across machines of a cluster and/or threads of a machine.

The universal property of monoid mappings is realized as the "lifted" `poly` syntactic encoding of an mm-ADT type.

## Processor Structures

The programs of the mm-ADT virtual machine are types. From a set of canonical types (ctypes), derived types (dtypes) of arbitrary complexity can be constructed using instructions from the VM’s instruction set architecture. Every mm-ADT type has a corresponding diagrammatic representation that is isomorphic to a directed labeled type graph composed of type-vertices and instruction-edges.

A program’s type graph is the intermediate representation used by the mm-ADT VM to not only link types (encode), but also to compile them (transform/optimize). At execution time, values propagate through the type graph and generate a parallel, homomorphic image of the types as values in the value graph, where the resultant structure of an mm-ADT computation is the obj graph, where

$\texttt{obj} = (\texttt{type} \times \texttt{q}) + (\texttt{value} \times \texttt{q}).$

Type composition, compilation, and evaluation are carried out by mm-ADT compliant processors. Processors ground the mm-ADT VM to the underlying physical computer (whether on a single machine, via multiple threads, or across compute cluster), where, at the bottom of this process stack, the natural world’s physics provides the baseline dynamics (the fundamental ground of the computation).

This section details the specifics of the relationships between types, values, and processors.

### Processes

Processors are used in the following three situations:

1. Composition: (type inference).

2. Compilation: (type optimization). (fix point).

3. Evaluation: (type enumeration).

### Algebraic Actions

A thread of execution in the VM maintains two primary references: 1.) a reference to an `obj` and 2.) a reference to an `inst`. Via the juxtaposition of `obj` and `inst` another `obj` is realized. When a VM process refers to the `obj` a and the instruction `inst` i, then the VM will perform one of the following operations:

1. If the vertex a has no outgoing i-labeled edge, then the VM applies a to i to yield the edge a \to_i b and arrive at b (compute).

2. If the vertex a has an outgoing i-labeled edge, then the VM traverses the edge a \to_i b to arrive at b (memoize).

The first situation is computing via function evaluation (save space). The second situation leverages memoization to avoid recomputing (save time). These two situations offer three high-level perspectives on the `obj` graph.

1. Mathematically: The `obj` graph has an infinite number of `obj` vertices connected to each other by edges labeled from the infinite instruction set architecture `inst`. From this perspective, computing is traversal (i.e. look-up) as the `obj` graph is fully materialized.

2. Theoretically: The `obj` graph is manifested as computations proceed where, if a \in \tt{obj} and i \in \tt{i\nst}, then any binary operation ai that has already been evaluated already exists in the `obj` graph and as such, can be traversed.

3. Physically: The `obj` graph is a dynamic entity that expands and contracts given the resource constraints of the underlying physical machines supporting its manifestation across all levels of the memory hierarchy, where garbage collection prunes the graph and computation grows the graph.

#### Type Specification

An mm-ADT program in an mm-ADT type. In the type graph (a subgraph of the `obj` graph) a type is denoted by a vertex (an ungrounded vertex). That vertex is the type’s range. The type’s definition is encoded in the directed, deterministic path that ends at a vertex with no outgoing edges. The resultant vertex is a root vertex and is the type’s domain. If the type definition’s path length is 0, then the domain and the range are equal, and the type is a ctype (a canonical type). If the path length is greater than 0, then the directed binary edges of the path are labeled with instructions from `inst`. This construction is abstractly represented in the diagram below.

The type graph forms the central structure upon by which various VM processes are enacted. These processes include type/program specification, compilation, optimization, and ultimately, via a homomorphism from the type graph to the value graph, evaluation. Given finite computing resources, the type graph does not exist eternally in a static form ready-made. No, instead, subgraphs of it must be generated. This is accomplished via an action of `inst` monoid on the set `inst*` (the Kleene star closure of `inst`). For instance, in `mmlang` the user juxtaposes a ctype (domain) and an `inst` to construct a dtype. That dtype is juxtaposed with another `inst` to yield another dtype so forth until a desired type is reached.

$\texttt{range} = ((((((\texttt{domain} \cdot \texttt{inst}_0) \cdot \texttt{inst}_1) \cdot \texttt{inst}_2) \ldots) \cdot \texttt{inst}_{n-2}) \cdot \texttt{inst}_{n-1}).$

In general, the action of an `inst` on a type is the function $\texttt{inst}: T \to T,$ where if a \in \tt{i\nst}, then $a(x) = xa.$

Said plainly, instructions in `inst` act on types by concatenating themselves to the type definition. Thus, algebraically, a type is an element of the free inst monoid rooted at a ctype.

#### Type Evaluation

A type compiles a type. A type evaluates a value. The `inst` monoid’s type specification action yields an element in the free `inst` monoid, which, in the `obj` graph, is realized as a path from a range vertex to a domain vertex. In the example `obj` graph encoding below, the range vertex is the type path's source and the domain vertex is the path’s target.

During type evaluation, the type path is reversed to form the co-type path, where the domain vertex is the source and the range vertex is the target.

If x \in \tt{value}, then x is propagated along the co-type path, where the \tt{domai\n} and \tt{rang\e} types perform runtime type checking and the instructions transform the source x value at each step into the resultant y value.

$y = ((((((((x \cdot \texttt{domain}) \cdot \texttt{inst}_0) \cdot \texttt{inst}_1) \cdot \texttt{inst}_2) \ldots) \cdot \texttt{inst}_{n-2}) \cdot \texttt{inst}_{n-1}) \cdot \texttt{range}).$

``````mmlang> int[plus,1][plus,2][plus,3]                                   (1)
==>int[plus,1][plus,2][plus,3]
mmlang> int[plus,1][plus,2][plus,3][path]                             (2)
==>(int;;int;[plus,1];int;[plus,2];int;[plus,3];int)
<=int[plus,1][plus,2][plus,3][path,(_;_)]
mmlang> 1=>int=>[plus,1]=>[plus,2]=>[plus,3]=>int                     (3)
==>7
mmlang> 1=>int[plus,1][plus,2][plus,3][path]                          (4)
==>(1;[plus,1];2;[plus,2];4;[plus,3];7)
<=1[plus,1][plus,2][plus,3][path,(_;_)]
mmlang> 1=>int[plus,1][plus,2][plus,3][path]>-                        (5)
==>7``````
 1 An `int<=int` type with a type path length of 5. 2 The co-type path of the previous type encoded in a `;-poly`. 3 The step-wise `=>` evaluation of the co-type path. 4 The step-wise `=>` evaluation of the co-type path chambered in a `;-poly`. 5 The evaluation of the `;-poly` simply returns the last path value.

In the `mmlang` example above, the step-wise `=>` evaluation of the co-type path is in one-to-one correspondence with the mm-ADT VM’s execution plan. The mm-ADT algebras are particular constraints on the most general algebraic specification of mm-ADT: the `obj` magma.

`1=>int=>[plus,1]=>[plus,2]=>[plus,3]=>int`

## Reference

### mmlang Grammar

``````obj   ::= (type | value)q
value ::= vbool | vint | vreal | vstr
vbool ::= 'true' | 'false'
vint  ::= [1-9][0-9]*
vreal ::= [0-9]+'.'[0-9]*
vstr  ::= "'" [a-zA-Z]* "'"
type  ::= ctype | dtype
ctype ::= 'bool' | 'int'  | 'real' | 'str' | poly | '_'
poly  ::= lst | rec | inst
q     ::= '{' int (',' int)? '}'
dtype ::= ctype q? ('<=' ctype q?)? inst*
sep   ::= ';' | ',' | '|'
lst   ::= '(' obj (sep obj)* ')' q?
rec   ::= '(' obj '->' obj (sep obj '->' obj)* ')' q?
inst  ::= '[' op(','obj)* ']' q?
op    ::= 'a' | 'add' | 'and' | 'as' | 'combine' | 'count' | 'eq' | 'error' |
'explain' | 'fold' | 'from' | 'get' | 'given' | 'groupCount' | 'gt' |
'gte' | 'head' | 'id' | 'is' | 'last' | 'lt' | 'lte' | 'map' | 'merge' |
'mult' | 'neg' | 'noop' | 'one' | 'or' | 'path' | 'plus' | 'pow' | 'put' |
'q' | 'repeat' |'split' | 'start' | 'tail' | 'to' | 'trace' | 'type' | 'zero'``````

### Instructions

The mm-ADT VM instruction set architecture is presented below, where the instructions are ordered by their classification and within each classification, they are ordered alphabetically.

#### Branch Instructions

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).

name string diagram sugar mmlang example

initial

`A`

``````mmlang> int
==>int
mmlang> 6
==>6``````

split

`-<(A,A)`

``````mmlang> int-<(_,_)
==>(int{2}<=int[id]{2})
<=int[split,(int{2}<=int[id]{2})]
mmlang> 6-<(int,int)
==>(6{2})``````

merge

`(A,A)>-`

``````mmlang> (int,int)>-
==>int{2}<=(int{2}<=int[id]{2})[merge]
mmlang> (6,6)>-
==>6{2}``````

repeat

`(A)^(A)`

``````mmlang> int(+3)^(5)
==>int[repeat,int[plus,3],5]
mmlang> 6(+3)^(5)
==>21``````

terminal

`A{0}`

``````mmlang> int{0}
mmlang>
mmlang> 6{0}
mmlang>``````

inst description example

`[branch]`
`[ ]`

Juxtapose start across `poly` terms and then aggregate the terms of the resultant `poly` as dictated by the `polys` underlying magma (objLR-module). $x(a_0,a_1,\ldots,a_n) = \bigodot_{i=0}^{i \leq n} xa_i$

``````mm> 6[branch,(+1,'a',*int)]
==>7
==>'a'
==>36
mm> 6[+1,'a',*int]
==>7
==>'a'
==>36``````

`[combine]`
`=`

Pairwise juxtapose the terms of two `polys` (Hadamard product and obj[X]). $(a_0,\ldots,a_n) \circ (b_0,\ldots,b_n) = (a_0b_0,\ldots,a_nb_n)$

``````mm> (1;2;3)[combine,(+10;+20;+30)]
==>(11;22;33)
mm> (1;2;3)=(+10;+20;+30)
==>(11;22;33)``````

`[lift]`
`<< >>`

Detach from the `obj` graph and operate stateless.

`[merge]`
`>-`

Aggregate the terms of the start `poly`, where aggregation semantics is determined by the underlying magma of the `poly` (objR-module). $(a_0,a_1,\ldots,a_n) = \bigodot_{i=0}^{i \leq n} a_i$

``````mm> (1,2,3)[merge]
==>1
==>2
==>3
mm> (1,2,3)>-
==>1
==>2
==>3
mm> (1;2;3)>-
==>3
mm> (1|2|3)>-
==>1``````

`[repeat]`
`( )^( )`

Apply the first `obj` (typically a type) to the incoming `obj` until the second `obj` is not `{0}`. For ease of use, if the second `obj` is an `int` value, then this is interpreted as number of times to iterate.

$x(a^n) = x \prod^{i \leq n}_{i=0} a$

``````mm> [1,2,3][repeat,+2,3]
==>7
==>8
==>9
mm> (1,2,3)>-(+2)^(3)
==>7
==>8
==>9
mm> (1,2,3)>-(*2)^(is<10)
==>16{2}
==>12``````

`[split]`
`-<`

Juxtapose start across `poly` terms as a scalar to a vector. `[branch]` is equivalent to `[split][merge]` (objL-module). $x(a_0,a_1,\ldots,a_n) = (xa_0,xa_1,\ldots,xa_n)$

``````mm> 1[split,(+1,+2,+3)]
==>(2,3,4)
mm> 1-<(+2,+3,+4)
==>(3,4,5)
mm> 1-<(+2;+3;+4)
==>(3;6;10)
mm> 1-<(+2|+3|+4)
==>(3)``````

`[swap]`
`/ /`

Replace the `[swap]` type’s last `inst` argument with the start and the start with the `inst` argument (swap). $xa = ax$

``````mm> '-adt'[plus,'mm']