Directed Acyclic Multi Graph

Initial and Final algebras have nice mathematical properties, for instance, initial algebras can be built up from other initial algebras. So, in the case of DAMGs, we can recursively compose larger graphs from smaller graphs. Graphs, in general, are not initial because they require labeled sets. However there is a form of graph which is initial, we call this Directed Acyclic Multi Graph (DAMG), this graph: damg external

I have used a lot of the information about this algebra from this paper: [Jeremy Gibbons - An Initial−Algebra Approach to Directed Acyclic Graphs]

This algebra is a 'symmetric strict monoidal' category.

So inside the DAMG we can have any graph which meets the above requirements (no loops and so on). Externally it has a number of inputs and outputs. We usually draw the inputs on the left and outputs on the right. damg internal
damg array What gives them nice mathematical properties is that we can link them together, both vertically and horizontally.
If the DAMG structures were always aligned in a strict array, as above, then the bottom part of the overall structure could not interact with the top. However there is no requirement for each column to align and therefore we can get as much interaction as required by combining in the appropriate way. damg align

Constructors

We can construct any DAMG from 6 constructor types (basic building blocks):

Vertex(S,m,n)

vertex

A vertex in the graph.

If defined over some set 'S' then the vertex can be associated with an element of that set. 'm' and 'n' are NNIs which represent the number of input and output edges. The inputs are usually shown on the left of the vertex and the outputs on the right, so the flow is usually drawn as going from left to right.

Edge

This represents an edge going from left to right. Not every edge on the graph will have an explicit edge term, often an output from a vertex will be plugged directly into the input of another vertex. An explicit edge is only needed as a sort of spacer to travel across a column without interacting.

Beside

This links up two sections of graph top to bottom.

Before

This links up two sections of graph left to right.

Empty

The empty graph. This has a similar function to say 'zero' for natural numbers.

Swap

swap This swaps over a set of edges to allow edges to move up and down so that they can plug onto different vertices.

Axioms

Beside is associative DamgBeside(x,DamgBeside(y,z)) = DamgBeside(DamgBeside(x,y),z)
Before is associative DamgBefore(x,DamgBefore(y,z)) = DamgBefore(DamgBefore(x,y),z)
Unit of graph is Empty 0 × x = Empty()
The number of output edges must match the number of input edges following

DamgBefore(DamgVertex(S,a,b),DamgVertex(S,c,d))

b=c

abiding law

When we combine 'beside' and 'before' then we can somtimes change which is outer and which is inner providing dimensions work out.

DamgBeside(DamgBefore(DamgVertex(S,a,b),DamgVertex(S,a,a)), DamgBefore(DamgVertex(S,a,b),DamgVertex(S,a,a))) = DamgBefore(DamgBeside(DamgVertex(S,a,b),DamgVertex(S,a,a)), DamgBeside(DamgVertex(S,a,b),DamgVertex(S,a,a)))

abiding

Swapping zero connections makes no difference DamgSwap(m,0) = m × DamgEdge()
Swapping n connections and then p connections is equivelent to swapping n+p connections swap law
Special case of swap law

DamgBefore(DamgSwap(m,n),DamgSwap(n,m)) = (m+n) × DamgEdge()

swap law special

swap(n,m) cancells out swap(m,n)

Another special case of swap law using edges

Example

Here we can see how 'vertex', 'edge' and 'swap' form components. 'beside and 'before' define how they fit together:

  damg

I compiled the FriCAS code below and then entered the above graph as follows:

(1) -> D:=Damg(String)
 
   (1)  Damg(String)
                                                                   Type: Type
(2) ->  x:=DamgBefore(DamgBefore(DamgBeside(DamgBeside(DamgVertex("v1",0,2),
DamgVertex("v2",0,2)),DamgVertex("v2",0,2)),DamgBeside(DamgBeside(DamgEdge()$D,
DamgBefore(DamgBeside(DamgSwap(1,1)$D,DamgSwap(1,1)$D),
DamgBeside(DamgBeside(DamgEdge()$D,DamgSwap(1,1)$D),
DamgEdge()$D))),DamgEdge()$D)),DamgBeside(DamgVertex("v1",3,0),
DamgVertex("v2",3,0)))
 

   (2)
  "before(before(beside(beside(vertex(0,2)vertex(0,2))vertex(0,2))beside(beside
  (edge(before(beside(swap(1,1)swap(1,1))beside(beside(edge(swap(1,1))edge()))e
  dge())beside(vertex(3,0)vertex(3,0)))"
                                                           Type: Damg(String)
(3) -> 

Well this constructs the structure but its horrible, it does not give any intuitive feel for the graph structure. I think the problem is not really FriCAS, any program which uses the command line interface would struggle to represent this type of structure. I think it really needs a more graphical interface.

Code

The following is just boilerplate code to construct and deconstruct a DAMG. It would be nice if SPAD had a way to automatically generate such boilerplate code for initial and final algebras.

To make this more useful we need code to convert this into other graph types and to produce graphical output.

)abbrev domain DAMG Damg

++ Author: Martin Baker
++ Date Created: May 2013
++ Date Last Updated: May 2013
++ Basic Operations:
++ Related Constructors:
++ Keywords: graph theory
++ Description: an initial graph similar to a DAG without the need for
++ labeled sets
++
++ References:
++ http: //www.euclideanspace.com/maths/standards/program/mycode/discrete/graph/

Damg(S) : Exports == Implementation where 
 S : SetCategory

 Exports ==> Join(CoercibleTo(OutputForm), SetCategory) with 
  -- constructors
  DamgVertex : (ob:S,m1:NonNegativeInteger,n1:NonNegativeInteger) -> %
    ++ Vertex constructor
  DamgEdge : () -> %
    ++ Edge constructor
  DamgBeside : (a:%,b:%) -> %
    ++ Beside constructor
  DamgBefore : (a:%,b:%) -> %
    ++ Before constructor
  DamgEmpty : () -> %
    ++ Empty constructor
  DamgSwap : (m:NonNegativeInteger,n:NonNegativeInteger) -> %
    ++ Swap constructor

  -- destructors, this is not necessarily a final algebra but we still need
  -- to be able to get at the components of instances.
  isVertex? : (n : %) -> Boolean
    ++ introspection: returns true if this is a Vertex
  isEdge? : (n : %) -> Boolean
    ++ introspection: returns true if this is a Edge
  isBeside? : (n : %) -> Boolean
    ++ introspection: returns true if this is a Beside
  isBefore? : (n : %) -> Boolean
    ++ introspection: returns true if this is a Before
  isEmpty? : (n : %) -> Boolean
    ++ introspection: returns true if this is Empty
  isSwap? : (n : %) -> Boolean
    ++ introspection: returns true if this is a Swap
  getIntValues : (n : %) -> List NonNegativeInteger
    ++ if term has integers then get them.
  getChildren : (n : %) -> List %
    ++ if term has child nodes then get them.

 Implementation ==> add
  Rep := Union(_
  	 vertex: Record(v:S,m:NonNegativeInteger,n:NonNegativeInteger),_
  	 edge : Boolean,_
  	 beside : Record(a:%,b:%),_
  	 before : Record(a:%,b:%,c:Boolean),_
  	 empty : Record(m:NonNegativeInteger),_
  	 swap : Record(m:NonNegativeInteger,n:NonNegativeInteger))
  -- Since this domain is initial the terms of the representation
  -- can correspond exactly to the constructors.

  -- Vertex constructor
  DamgVertex(ob:S,m1:NonNegativeInteger,n1:NonNegativeInteger) : % == 
	[[ob,m1,n1]]

  -- Edge constructor
  DamgEdge() : % == [true]
  
  -- Beside constructor  
  DamgBeside(a1:%,b1:%) : % == [[a1,b1]]

  
  -- Before constructor
  DamgBefore(a1:%,b1:%) : % == [[a1,b1,true]]

  -- Empty constructor
  DamgEmpty() : % == [[0::NonNegativeInteger]]
  
  -- Swap constructor
  DamgSwap(m1:NonNegativeInteger,n1:NonNegativeInteger) : % == [[m1,n1]]

  -- introspection: returns true if this is a Vertex
  isVertex?(n1 : %):Boolean ==
    (n1 case vertex)

  -- introspection: returns true if this is a Edge
  isEdge?(n1 : %):Boolean ==
    (n1 case edge)

  -- introspection: returns true if this is a Beside
  isBeside?(n1 : %):Boolean ==
    (n1 case beside)

  -- introspection: returns true if this is a Before
  isBefore?(n1 : %):Boolean ==
    (n1 case before)

  -- introspection: returns true if this is Empty
  isEmpty?(n1 : %):Boolean ==
    (n1 case empty)

  -- introspection: returns true if this is a Swap
  isSwap?(n1 : %):Boolean ==
    (n1 case swap)

  -- if term has integers then get them.
  getIntValues(n1 : %):List NonNegativeInteger ==
    if isVertex?(n1) then return [n1.vertex.m, n1.vertex.n]
    if isSwap?(n1) then return [n1.swap.m, n1.swap.n]
    []

  -- if term has child nodes then get them.
  getChildren(n1 : %):List % ==
    if isBeside?(n1) then return [n1.beside.a, n1.beside.b]
    if isBefore?(n1) then return [n1.before.a, n1.before.b]
    []

  -- return string representation using deBruijn index for
  -- bound variables.
  -- notation assumes association to the left, in the absence of
  -- brackets, the term to the left binds more tightly than the
  -- one on the right.
  toString(n1 : %) : String == 
    s:String := ""
    if isVertex?(n1) then
      s := concat(["vertex(",string(getIntValues(n1).1),_
                             ",",string(getIntValues(n1).2),_
                             ")"])@String
    if isEdge?(n1) then
      s := "edge("
    if isBeside?(n1) then
      s := concat(["beside(",toString(getChildren(n1).1),_
              toString(getChildren(n1).2),")"])@String
    if isBefore?(n1) then
      s := concat(["before(",toString(getChildren(n1).1),_
              toString(getChildren(n1).2),")"])@String
    if isEmpty?(n1) then
      s := "empty"
    if isSwap?(n1) then
      s := concat(["swap(",string(getIntValues(n1).1),_
                             ",",string(getIntValues(n1).2),_
                             ")"])@String
    s

  -- output
  coerce(n : %) : OutputForm ==
    toString(n)::OutputForm

@

 


metadata block
see also:
Correspondence about this page

Book Shop - Further reading.

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.

flag flag flag flag flag flag Axiom Volume 1: Tutorial. Documentation is freely availible from: http://www.axiom-developer.org/axiom-website/documentation.html

 

This site may have errors. Don't use for critical systems.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.