kremer@cpsc.ucalgary.ca

A Z Specification for the Formal Interpretation of Typed Graphs

To begin with, a few given sets describe names for graph components, names for attributes of the graph components, attribute values, and the unspecified contents of a graph node. "Node", "Arc", and "IsA" are declared as names for graph components, although the there will be more. 
	specification

	[NAME, ATTRIBUTE_NAME, ATTRIBUTE_VALUE, CONTENTS]

	| Node,Arc,IsA: NAME

Attributes

ATTRIBUTEs will be used to tag graph components with application-specific attributes. For example, the attribute "Shape" (Name) might describe the surround of a graph node with values (Value) such as "rectange" or "ellipse". Attributes are meant to be inherited through the type system, and Priority and Flags will be used to arbitrate in the case of conflicts arising due to multiple inheritance of an attribute. 
	ATTR_FLAGS ::= LOCKED | NOFLAG

	---ATTRIBUTE-------------------------------------------------------------
	| Name: ATTRIBUTE_NAME;
	| Value: ATTRIBUTE_VALUE;
	| Priority: Z;
	| Flags: P ATTR_FLAGS;
	-------------------------------------------------------------------------
MakeAttribute is a convenient function to create a new attribute. 
	| MakeAttribute: ATTRIBUTE_NAME & ATTRIBUTE_VALUE & Z & P ATTR_FLAGS
	|							--> ATTRIBUTE
	|-----------
	| MakeAttribute = (lambda n:ATTRIBUTE_NAME; v:ATTRIBUTE_VALUE; p:Z; f:P ATTR_FLAGS @
	|   (mu a:ATTRIBUTE | a.Name=n /\ a.Value=v /\ a.Priority=p /\ a.Flags=f))
NULLav is a special attribute value witch indicates "no value": 
	| NULLav: ATTRIBUTE_VALUE

Components: NODEs, ARCs, and ISAs

COMPONENT0 is the common part of both graph nodes and the arcs among the nodes. All components have a name, are associated with a level (to be described later), and have a set of ATTRIBUTEs associated with them. 
	---COMPONENT0------------------------------------------------------------
	| Name: NAME;
	| Level: Z;
	| Attributes: P ATTRIBUTE;
	-------------------------------------------------------------------------

NODEs

NODE0 is node-specific extension to COMPONENT0. It has some unspecified contents. 
	---NODE0-----------------------------------------------------------------	
	| Contents: CONTENTS;
	-------------------------------------------------------------------------

ARCs

Arcs take a little more work to specify than nodes. Arcs are very general in this specification: they have an arbitrary arity (they need not be binary), and they may terminate at an arbitrary component (either nodes or other arcs). Since COMPONENT has not yet been completely defined it is temporarily pre-declared as a given set. 
	[COMPONENT]
The terminals of an arc have direction besides a reference to the archor component. All arcs must have at least one terminal. 
	DIRECTION ::= FROM | TO | BIDIRECT | NONE

	---TERMINAL--------------------------------------------------------------	
	| Anchor: COMPONENT;
	| Direction: DIRECTION;
	-------------------------------------------------------------------------

	---ARC0------------------------------------------------------------------	
	| Terminals: seq TERMINAL;
	|---------------
	| #Terminals > 0
	-------------------------------------------------------------------------

Supertype of NODEs and ARCs: COMPONENT

Finally, the parts can be brought together to define a component. The basic components of a graph are nodes and arcs. A COMPONENT is the base, COMPONENT0 (name, level, and attributes) together with the NODE0 or ARC0 extension. 
	COMPONENT_TYPES ::= node << NODE0 >>
			|   arc << ARC0 >>

	---COMPONENT-------------------------------------------------------------	
	| COMPONENT0;
	| Role:COMPONENT_TYPES;
	|-------------
	| COMPONENT0;
	-------------------------------------------------------------------------
T, the top, most general, component is rather loosely defined. 
	| T: COMPONENT

ARCs, again

MakeTerminal is simple utility finction to create a Terminal to later add to an ARC. 
	| MakeTerminal: COMPONENT & DIRECTION --> TERMINAL
	|---------------
	| MakeTerminal = (lambda c:COMPONENT; d:DIRECTION @
	|	(mu t:TERMINAL | t.Anchor=c /\ t.Direction=d))
ARC_COMPONENT and NODE_COMPONENT are simply a conveniences to refer to arcs and nodes. 
	
	ARC_COMPONENT =^= [COMPONENT | Role in ran arc]

	NODE_COMPONENT =^= [COMPONENT | Role in ran node]
The functions Terminal and TerminalDir are conveniences to extract individual terminals and direction of individual terminals from arcs. 
	
	| GetTerminal: ARC_COMPONENT & N +-> COMPONENT;
	| GetTerminalDir: ARC_COMPONENT & N +-> DIRECTION;
	|--------------
	| forall a:ARC_COMPONENT; n:N | n <= #(arc~(a.Role)).Terminals @
	|    GetTerminal(a,n) = (((arc~(a.Role)).Terminals)(n)).Anchor /\
	|    GetTerminalDir(a,n) = (((arc~(a.Role)).Terminals)(n)).Direction;
No arc may refer to itself. 
	forall a:ARC_COMPONENT @ forall t:second(| (arc~(a.Role)).Terminals |) @
		a /= t.Anchor

ISA

So far, the discussion has centered around the description of a simple graph; however the intent was to describe typed graphs. Nodes and arcs all have one or more types. In this specification, types are just other components of the graph. An type or object is a subtype or instance, respectively, of another by virtue of being connected to it by a special arc type called ISA_COMPONENT. An ISA_COMPONENT arc must be binary, and must point "upward" form a component who's Level is lower (higher numbered) or equal to the Level of its parent. The level of an IsA arc is always the same as the root terminal. 
	ISA_COMPONENT =^= [ARC_COMPONENT |
		#(arc~(Role)).Terminals = 2		%ISAs are binary
		]

	forall a:ISA_COMPONENT @	 		% ISAs point "upward"
		(GetTerminalDir(a,1)) = FROM	/\
		(GetTerminalDir(a,2)) = TO	/\
		(GetTerminal(a,1)).Level >=  (GetTerminal(a,2)).Level /\
		a.Level = (GetTerminal(a,1)).Level

Defining some actual objects

The parts of a graph (nodes, arcs, and isa arcs) are themselves type objects in this theory. A node is called "Node", etc. The three components all reside (uniquely) in highest type level. 
	| NODE: NODE_COMPONENT
	|----------------
	| NODE.Name = Node;
	| NODE.Level = 1;
	| #NODE.Attributes = 0;

	| ARC: ARC_COMPONENT
	|----------------
	| ARC.Name = Arc;
	| ARC.Level = 1;
	| #ARC.Attributes = 0;
	| #(arc~(ARC.Role)).Terminals = 0;

	| ISA: ISA_COMPONENT
	|----------------
	| ISA.Name = IsA;
	| ISA.Level = 1;
	| #ISA.Attributes = 0;
NULLnode is a special object used to allow "dangling arcs", that is, arcs where one or more terminals have not been defined. If an arc terminates on NULLnode, we should assume that terminal has not (yet?) been specified. Although this complication is not theoretically necessary, it is required for practical purposes, for the correct terminating node may not be known. 
	| NULLnode: NODE_COMPONENT
	|----------------
	| NULLnode.Level = 1;
	| #NULLnode.Attributes = 0;

	forall c:COMPONENT @ c.Level = 1 <=>
		(c = ARC \/ c = NODE \/ c = ISA \/ c = NULLnode)

The Subtype Relations

We are now is a position to describe the traditional subtyping relations. Here the relation parentof refers to only immediate parents, while the relation ancestorof is the normal proper subtype relation. isa is as expected: just the same as ancestorof except that identity is included. Note that the direction of the isa relation is the reverse of the other two!

The parentof relation is irreflexive and antisymmetric. 

	%% inrel parentof

	| _ parentof _ : COMPONENT <-> COMPONENT
	|-------------
	| forall p,c:COMPONENT @
	|	(p parentof c <=> (exists a:ISA_COMPONENT @
	|		GetTerminal(a,2) = p /\ GetTerminal(a,1) = c)) /\
	|	not (c parentof c) /\
	|	p parentof c => not (c parentof p)
The ancestorof relation is based on parentof and is irreflexive, antisymmetric, and transitive. 
	%% inrel ancestorof

	| _ ancestorof _ : COMPONENT <-> COMPONENT
	|-------------
	| forall c1,c2:COMPONENT @
	|	(c1 ancestorof c2 <=> (c1,c2) in ( _ parentof _ )^*) /\
	|	not (c1 ancestorof c1) /\
	|	(c1 ancestorof c2) => not (c2 ancestorof c1)
The isa relation is based on ancestorof, but is reflexive, antisymmetric, and transitive. 
	%% inrel isa

	| _ isa _ : COMPONENT <-> COMPONENT
	|-------------
	| forall p,c:COMPONENT @ (c isa p) <=> ((p = c) \/ (p ancestorof c))

Typed Graphs

A typed graph always contains the basic components node, arc, and isa. There are several constraints on a TYPED_GRAPH: 
	Level1Objects == {NODE, ARC, ISA, NULLnode}

	| individual, parentOfIndividual: ATTRIBUTE_NAME

	---TYPED_GRAPH-----------------------------------------------------------	
	| Contents: P COMPONENT;
	|-------------
	| % node, arc, and isa are the only level one objects
	| Level1Objects subset Contents;
	| forall c:Contents | c notin Level1Objects @ c.Level>1;
	| 
	| % there are no cycles over the isa relationship
	| forall c:Contents @ not (c ancestorof c);
	|
	| % everything is a NODE or ARC or ISA, but only one of these
	| forall c:Contents @
	|	(c isa NODE \/ c isa ARC \/ c isa ISA)		/\
	|	(c isa NODE) => not (c isa ARC  \/ c isa ISA)	/\
	|	(c isa ARC ) => not (c isa NODE \/ c isa ISA)	/\
	|	(c isa ISA ) => not (c isa NODE \/ c isa ARC);
	|
	| % no component attribute overrides a locked attribute at a higher level
	| forall c:Contents @ forall a:c.Attributes @
	|	not (exists c2:Contents | c2 ancestorof c @
	|	  forall a2:c2.Attributes | LOCKED in a2.Flags @
	|		a2.Name = a.Name => c2.Level = c.Level);
	|
	| % arc constraint: arcs must conform to their parents' arcs
	| forall c,c2:ARC_COMPONENT | c in Contents /\ c2 ancestorof c @
	|    % subtypes must have equal or more terminals
	|    #(arc~(c2.Role)).Terminals <= #(arc~(c.Role)).Terminals /\
	|    % subtypes must type-conform at each terminal
	|    (forall i:Z | i<=#(arc~(c2.Role)).Terminals @
	|	GetTerminal(c,i) isa GetTerminal(c2,i) \/
	|	GetTerminal(c,i)=NULLnode);	% allow for "dangling arcs"
	| 
	| % arcs refer only to other components within the graph
	| forall a:ARC_COMPONENT | a in Contents @
	|	(forall i:Z | i<=#(arc~(a.Role)).Terminals @
	|		GetTerminal(a,i) in Contents);
	|
	| % a type marked as "parentOfIndividual" has only subtypes marked "individual"
	| forall c:Contents @ (exists a:c.Attributes @ a.Name=parentOfIndividual) =>
	|	(forall c2:Contents | c2 isa c @ exists a:c2.Attributes @
	|		a.Name = individual);
	|
	| % nothing marked "individual" has any child types
	| forall c:Contents @ (exists a:c.Attributes @ a.Name=individual) =>
	|	not (exists c2:Contents @ c2 isa c)
	--------------------------------------------------------------------------
	
	---INIT_TYPED_GRAPH-------------------------------------------
	| TYPED_GRAPH'
	|------------------------
	| Contents' = Level1Objects
	--------------------------------------------------------------------------
The following is a consistency corrollary of the above TYPED_GRAPH schema and can easily be proved from it. Every component is the same top-level type as all of its supertypes. 
	forall g:TYPED_GRAPH @ forall c1,c2:g.Contents | c1 isa c2 @
		c1 isa NODE <=> c2 isa NODE /\
		c1 isa ARC  <=> c2 isa ARC  /\
		c1 isa ISA  <=> c2 isa ISA
It is not particularly common in graphs to allow arcs between arcs, and this restriction may easily be applied to this typed graph theory. Such a graph is called a FIRST_ORDER_TYPED_GRAPH, and is just a constraint on an ordinary TYPED_GRAPH: all arc terminals must refer to nodes only. Note, that this does not constrain the type system, as isa arcs can refer to nodes or links (or other isas). 
	%% state-schema FIRST_ORDER_TYPED_GRAPH

	FIRST_ORDER_TYPED_GRAPH =^= [TYPED_GRAPH |
		(forall a:COMPONENT | a in Contents @
			a isa ARC => (forall t:TERMINAL |
				t in ran (arc~(a.Role)).Terminals @
					t.Anchor isa NODE))
		]

	%% init-schema INIT_FIRST_ORDER_TYPED_GRAPH
	
	---INIT_FIRST_ORDER_TYPED_GRAPH-------------------------------------------
	| FIRST_ORDER_TYPED_GRAPH'
	|------------------------
	| Contents' = Level1Objects
	--------------------------------------------------------------------------

The Operators

To following utility functions determine the value of a particular attribute given a TYPED_GRAPH, a component, and an attribute name. The first function, getAttr searches for an attribute looking first in the actual component, then attempts to select the highest priority attribute that is not hidden by an intervening attribute. Note that locked attributes are already taken care of in the TYPED_GRAPH schema. Note also that this function is not necessarily deterministic: this problem will have to be addressed in the future. 
	GETATTR_RESULT ::= Attr << ATTRIBUTE >> | NULLr

	| getAttr: TYPED_GRAPH & COMPONENT & ATTRIBUTE_NAME --> GETATTR_RESULT
	|--------------
	| forall g:TYPED_GRAPH; c:COMPONENT; a:ATTRIBUTE_NAME | c in g.Contents @
	|   getAttr(g,c,a) =
	|     if a in {a1:ATTRIBUTE_NAME | exists at:c.Attributes @ a1 = at.Name}
	|	% c actually has the attribute
	|       then (mu x:c.Attributes | (a = x.Name)) 
	|       else if (forall c2:g.Contents | c2 parentof c @
	|						getAttr(g,c2,a) = NULLr)
	|	  % attribute not found
	|         then NULLr
	|	  % attribute found in one of the ancestors
	|         else (mu x:ATTRIBUTE | forall c2:g.Contents|c2 parentof c @
	|		exists y:ATTRIBUTE | y=Attr~(getAttr(g,c2,a)) @
	|		  forall z:ATTRIBUTE | z=Attr~(getAttr(g,c2,a)) @
	|		    y.Priority>=z.Priority /\ x=y)
The getValue function is similar to the above function, but simply returns a value if one can be found. 
	GETVALUE_RESULT ::= Val << ATTRIBUTE_VALUE >> | NULLv

	| getValue : TYPED_GRAPH & COMPONENT & ATTRIBUTE_NAME --> GETVALUE_RESULT
	|---------------
	| forall g:TYPED_GRAPH; c:COMPONENT; a:ATTRIBUTE_NAME | c in g.Contents @
	|	getValue(g,c,a) = if getAttr(g,c,a)=NULLr
	|			    then NULLv
	|			    else (Attr~(getAttr(g,c,a))).Value
setAttr takes a component and an attribute and merely adds the attribute to the components set of attributes, replacing any attributes who's name might have matched. 
	---setAttr----------------------------------------------------------------
	| Delta TYPED_GRAPH;
	| c?: COMPONENT;
	| attr?: ATTRIBUTE
	|---------------
	| c? in Contents;
	| Contents' = (Contents \ {c?}) || {(mu c2:Contents |
	|	c2.Name  = c?.Name	/\
	|	c2.Level = c?.Level	/\
	|	c2.Role  = c?.Role	/\
	|	c2.Attributes = (c?.Attributes \
	|		{a:c?.Attributes | a.Name = attr?.Name}) ||
	|		{attr?})}
	--------------------------------------------------------------------------
Its a simple procedure to add a node to a graph: 
	---ADD_NODE---------------------------------------------------------------
	| Delta TYPED_GRAPH;
	| node?: NODE_COMPONENT;
	| type?: NODE_COMPONENT
	|---------------
	| TYPED_GRAPH';
	| type? in Contents;
	| not (node? in Level1Objects);
	| getAttr((mu x:TYPED_GRAPH|x.Contents=Contents),type?,individual) = NULLr;
	| Contents' = Contents || {node?, (mu a:ISA_COMPONENT |
	|	GetTerminal(a,1)=node? /\ GetTerminal(a,2)=type?) };
	--------------------------------------------------------------------------
Note that due to the invarients on the graph, the node cannot have any non-ISA arcs in the graph that refering to it immediate after its insertion. Note also that, by virtue of the definition of NODE_COMPONENT, the new node isa NODE (and therefore there exists an ISA link from the new node to NODE.

Its just as simple to add a new arc: 

	---ADD_ARC----------------------------------------------------------------
	| Delta TYPED_GRAPH;
	| arc?: ARC_COMPONENT;
	| type?: ARC_COMPONENT
	|---------------
	| TYPED_GRAPH';
	| type? in Contents; % redundant
	| not(arc? isa ISA);
	| not(arc? in Level1Objects);
	| getAttr((mu x:TYPED_GRAPH|x.Contents=Contents),type?,individual) = NULLr;
	| Contents' = Contents || {arc?, (mu a:ISA_COMPONENT |
	|	GetTerminal(a,1)=arc? /\ GetTerminal(a,2)=type?)};
	--------------------------------------------------------------------------
But note that there is more going on here than meets the eye. Because of the constraints on a typed graph, the arc must refer only to nodes that are already members of the graph contents.

It must also be possible to change the type of node or link: 

	---CHANGE_TYPE------------------------------------------------------------
	| Delta TYPED_GRAPH;
	| c?: COMPONENT;
	| newType?: COMPONENT
	|---------------
	| TYPED_GRAPH';
	| (c? isa NODE /\ newType? isa NODE) \/
	| (c? isa ARC  /\ newType? isa ARC ) \/
	| (c? isa ISA  /\ newType? isa ISA );
	| c? in (Contents \ Level1Objects);
	| newType? in Contents;
	| getAttr((mu x:TYPED_GRAPH|x.Contents=Contents),newType?,individual) = NULLr;
	| Contents' = (Contents \ {a:ISA_COMPONENT | GetTerminal(a,1) = c?}) ||
	|   {(mu a:COMPONENT | GetTerminal(a,1)=c? /\ GetTerminal(a,2)=newType?)};
	--------------------------------------------------------------------------
Removing any component from a graph entails altering all arcs (including isa arcs) that reference the removed node. One problem is that if the removed node was the type of some existing component, then the "lower" components will be left with dangling isa chains. This is prevented by disallowing it in the precondition. The other problem is that we don't want regular (non-isa) arcs to refer to the removed component. This is handled by replacing all such arcs with arcs that have a reference to NULLnode in place of a reference the removed arc. In addition, any arcs that wouldn't refer to any other components (besides NULLnode) merely be deleted altogether. All this leads to a fairly complicated specification: 
	---REMOVE-----------------------------------------------------------------
	| Delta TYPED_GRAPH;
	| c?: COMPONENT;
	|---------------
	| % preconditions
	| c? in (Contents \ Level1Objects);
	| not (exists c2:Contents @ c2 isa c?);
	|
	| Contents' = (Contents \
	|   % remove c? and all arcs that refer to it
	|   ({c?} || {a:ARC_COMPONENT | a in Contents /\
	|                               (exists i:N @ GetTerminal(a,i)=c?)})) ||
	|   % replace arcs that refer to c? with ones that refer to NULLnode,
	|   % but don't replace any arcs that would refer to nother but NULLnode
	|   {a:ARC_COMPONENT |
	|     (forall a1:ARC_COMPONENT | a1 in Contents /\
	|				 (exists i:N @ GetTerminal(a1,i)=c?) /\
	|				 (exists j:N | j<=#(arc~(a.Role)).Terminals @
	|				   GetTerminal(a1,j) /= c? /\
	|				   GetTerminal(a1,j) /= NULLnode) @
	|	    a.Name = a1.Name /\
	|	    a.Level = a1.Level /\
	|	    a.Attributes = a1.Attributes /\
	|	    #(arc~(a.Role)).Terminals = #(arc~(a1.Role)).Terminals /\
	|	    (forall j:N | j<=#(arc~(a.Role)).Terminals @ 
	|	      GetTerminal(a,j) = if GetTerminal(a1,j)=c?
	|				 then NULLnode
	|				 else GetTerminal(a1,j))
	|     )}
	--------------------------------------------------------------------------

	end specification