In category theory, if C and D are both categories, then a functor from C to D maps every morphism in C to some morphism in D. You can think of a functor as a set of "morphism-to-morphism"-morphisms. Furthermore, if the functor maps from category C to category C (i.e., D=C), this is called an endofunctor.
In mm-ADT, in the type subgraph of the obj graph, the vertices denote types and a path (of edges) back to the root of the graph (a ctype root) denotes a type definition. These edges are labeled with instructions from inst, where a path is a sequence of operations that morph one type into another type (see The Type). In abstract algebra, the type subgraph is called a (generalized) Cayley graph as the obj graph captures the structure of the underlying inst monoid. Next, two mm-ADT types, composed of different instructions, can be semantically equivalent if they refer to the same elements (e.g. the same values). In other words, type equivalence is a relationship between two paths in the type graph. Since a vertex is always the head of some path (type graph structure is a lattice), a functor in mm-ADT is a "vertex-to-vertex"-morphism (or a "type-to-type" morphism).
For example, assume the following endofunctors.
[define,int<=(int[mult,1])]
[define,(int[plus,x+y])<=(int[plus,x][plus,y])]Given the above definitions, the type
bool<=int[plus,7][plus,4][plus,2][mult,1][gt,10]has the following equivalences.
bool<=int[plus,7][plus,4][plus,2][gt,10]
bool<=int[plus,7][plus,6][mult,1][gt,10]
bool<=int[plus,7][plus,6][gt,10]
bool<=int[plus,13][mult,1][gt,10]
bool<=int[plus,13][gt,10]Every deterministic walk from type-to-root in the type graph yields an type equivalent to the source type. The aggregate of all these types and their equivalences are diagrammed below. This diagram is an instance of the proposed type graph structure that overlays Cayley Graph instances to form a higher order Cayley Graph based on [define].
