mmadt-ct-meetup-talk.java

mm-ADT: An Algebraic Overview for the Category Theory Meetup
  by Dr. Marko A. Rodriguez (collaborator: Dr. Ryan Wisnesky)

  http://mm-adt.org
  https://www.mm-adt.org/vm (draft)

https://www.meetup.com/Category-Theory/events/vmkkjrybckbkb/
------------------------------------------------------
------------------------------------------------------
            mm-ADT
            /    \
 multi-model      abstract data type
  /  | |  |  \        /      |      \   
grph | kv |  wc   language  storage  processor
    /      \               
   rel    rdf


Language : Query languages (inititally) and programming languages (future).
Storage  : Databases and heaps.
Processor: Message-Passing, Bulk Synchronous, Reactive, etc.
|       |
|       | 
 \     /
  Synthetic 
    Data 
      Systems

Cluster-Oriented General Purpose Programming Environment
  * Languages provide data manipulation patterns.
  * Storage systems provide memory hiearchy (from single machine to cluster)
  * Processors provide executions (threading, serialization)

------
mmlang 
     \_____is the assembly language of the mm-ADT virtual machine
      \____a textual representation of the inst monoid
       \___a point-free, fluent language w/ Turing Complete expressivity
        \__target language for other language compilers
------------------------------------------------------
------------------------------------------------------
The Three Interconnected Algebras
  https://www.mm-adt.org/vm/#_mm_adt_algebras

obj magma     ( => -- juxtaposition   )  STORAGE
inst monoid   (    -- apply           )  LANGUAGE
type ringoid  ( ;, -- serial/parallel )  PROCESSOR
------------------------------------------------------
------------------------------------------------------
The Obj Magma
  https://www.mm-adt.org/vm/#_the_obj

(carrier set    ) obj
(binary operator) =>: obj x obj -> obj 

obj = 'object'      * quantifier  ---- x{q}
obj = (type+value)  * quantifier  ---- int{0,12} or 3{46}

          obj
        /     \
       /       \
      /         \
quantified    quantified
   type          value

Four possible juxtapositions (=>)
  1. value_a => value_b = value_b             
  2. value_a => type_b  = type_b(value_a)     (evaluation)
  3. type_a  => type_b  = type_b(type_a)      (compilation)
  4. type_a  => value_b = value_b

EXAMPLES:
  1                => 10                     (1)
  1{3}             => 10{4}                  (1)
  1                => int[plus,2]            (2)
  1                => int{10}[plus,2]        (2)
  int[plus,2]      => int[gt,5]              (3)
  int{10}[plus,2]  => int[gt,5]              (3)

** quantifiers are any ordered algebraic ring with unity
 * int   ~ "amount"           (standard query/programming languages)
 * real  ~ "proporition"      (fuzzy logic)
 * cmplx ~ "energy"           (quantum logic)
 |
  \__pairs used for "expected range"

DEFAULT: int x int ~ "expected amount"
------------------------------------------------------
------------------------------------------------------
The Inst Monoid
  https://www.mm-adt.org/vm/#_inst_monoid
  https://www.mm-adt.org/vm/#_obj_graph
  
inst is the instruction set architecture (a subset of obj)

(carrier set)    obj
(generating set) inst
(binary operator) <blank>: obj x inst -> obj           (a second-arg constraint on =>)
                            |      |      |
                            |      |      |
                    type + value  type   type + value
     
Monoidal Cayley Graph
 a <blank> i = b
 ai = b
 a--i-->b

type : element of the *free* inst monoid    (programs are "complicated" types)
value: element of the        inst monoid    (values are have no history)
 
       obj graph
        /    \
       /      \
 value graph  type graph


EXAMPLE: 
  int[plus,2][mult,7]
    2[plus,2][mult,7]

  2--[plus,2]------>4--------[mult,7]---------->28             (value graph)
  |                 |                           |                    |
 [type]           [type]                      [type]              obj graph                            
  |                 |                           |                    |
int--[plus,2]-->int[plus,2]--[mult,7]-->int[plus,2][mult,7]     (type graph)

** the mm-ADT obj graph commutes.
  \__optimizations via "poly lifting" (teleportation/graphs minors/rewriting)

----
Understanding the Type Graph
  https://www.mm-adt.org/vm/#_type_structure

type = ctype + dtype
type = ctype + (type * inst)
 |
  \__a type is a path in the obj graph that is rooted at a canonical type
         (type * inst)                                       (ctype)
              |                                                 |
         inductive step                                      base step


       range<=domain[inst]        (mmlang syntax)
          di = r                  (algebra syntax) 
          d--i-->r                (cayley structure)

EXAMPLES:
  int[plus,1]                                  int    <=int
  int[plus,1][gt,5]                            bool   <=int
  int[plus,1][is,[gt,5]]                       int{?} <=int
  int[plus,1][is,[gt,5]][as,str[plus,'a']]     str{?} <=int

            type                 (mm-model)
       _____/   \______
      |   |   |    |   |
      |   |   |    |   |
    bool int real str poly
    |              |   |
     \____     ____/   |
           mono        |
      monomials        polynomials
------------------------------------------------------
------------------------------------------------------
The Type Ringoid
  https://zenodo.org/record/2565243
  https://www.mm-adt.org/vm/#_type_quantification

Typically understood as realizing
   parallel-distributed computing pipelines.
      
(carrier set)        types     ~ stream functions  (supporting lazy/greedy semantics)
(binary operators)     ;       ~ serial streams    (linear composition)
                       ,       ~ parallel streams  (branching composition)
            
    ; is a monoid (various submonoid+ within)
    , is a group


           type{q}
          /       \
       type       {q}
        |          |
    ; parallel   + addition        | ring axioms
    , serial     * multiplication  | ring axioms


** The type ringoid algebra is internal to the processors.
***** however, there is an embedding in the inst monoid via poly.

The Poly
 | https://www.mm-adt.org/vm/#_poly_types
 |
  \_____realize a polynomial ring.
   \____subset of obj w/ type and value forms
 

values               poly   
                     /  \
                   lst  rec                        (collections)
               (1,2,3)  ('a'->1,'b'->2)

types                poly
                     /  \
               branch    switch                     (pipelines)
           (+1,+2,+3)    (is>=5 -> +1,is<5 -> +2)

+1 ~ [plus,1]

String Diagram Sugar Syntax
   -< [split]
   =  [combine]
   >- [merge]

EXAMPLES:
int-<(+1,+2)
  {1,2,3}-<(+1,+2)
  {1,2,3}-<(+1,+2)>-

int-<(is>0->'a',is<10->'b')
  {1,20,-1}-<(is>0->'a',is<10->'b')
  {1,20,-1}-<(is>0->'a',is<10->'b')>-

(int,int,int)=([neg],_,10)
(1,2,3)=([neg],_,10)

----

Path equivalences in the type graph.
   \
    [rewrite,([id])  <=([plus,[zero]])]
    [rewrite,([zero])<=([mult,[zero]])]
    [rewrite,([id])  <=([neg][neg])]

Forms the foundation for model-ADT embedding and storage, processor, and language optimization.
                                                   |             |          |           
                                                   |             |          |  
                                                   |             |        schemas
                                                   |             |       semantics 
                                                   |             |       
                                                indices        load via quantification
                                               sort orders       greedy/lazy
                                            denormalizations      memory/disk
    

Thank you for your attention.
         Marko. (http://markorodriguez.com)


model-ADT DEMO: 
   :pre [load 'data/source-6.mm']