Rob Kremer, kremer@cpsc.ucalgary.ca

A Z Specification for the Formal Interpretation of Typed Graphs

Warning: work in progress

Basic Types

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, CONTENTS, char]

	| Node,Arc,IsA,T: NAME

	% [ATTRIBUTE_VALUE]
	ATTRIBUTE_VALUE ::= pos_int << N >>
			|   int << Z >>
			|   string << seq char >>

	| attribute_value: ATTRIBUTE_VALUE % generic value

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. [Implementation:
declaration and code]
	ATTR_FLAGS ::= CONSTANT | PRIVATE

	---ATTRIBUTE-------------------------------------------------------------
	| Name: ATTRIBUTE_NAME;
	| Value: ATTRIBUTE_VALUE;
	| Priority: Z;
	| Flags: P ATTR_FLAGS;
	-------------------------------------------------------------------------
MakeAttribute is a convenient function to create a new attribute. [Implementation: declaration]
	| 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))

Basic Components: Nodes and Arcs

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. [Implementation: declaration and code]
	[VALIDATOR]

	---COMPONENT0------------------------------------------------------------
	| Name: NAME;
	| Level: Z;
	| Attributes: P ATTRIBUTE;
	| Constraints: P VALIDATOR;
	-------------------------------------------------------------------------
[Implementation: declaration] NODE0 is node-specific extension to COMPONENT0. It has some unspecified contents.
	---NODE0-----------------------------------------------------------------
	| Contents: CONTENTS;
	-------------------------------------------------------------------------
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. [Implementation: declaration and code]
	DIRECTION ::= FROM | TO | BIDIRECT | NONE

	---TERMINAL--------------------------------------------------------------
	| Anchor: COMPONENT;
	| Direction: DIRECTION;
	-------------------------------------------------------------------------
ARC0 is the extension of COMPONENT0 for arcs. [Implementation: declaration and code]
	---ARC0------------------------------------------------------------------
	| Terminals: seq TERMINAL;
	|---------------
	| #Terminals > 0
	-------------------------------------------------------------------------
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 >>
			|   isa_arc << ARC0 >>

	---COMPONENT-------------------------------------------------------------
	| COMPONENT0;
	| Role:COMPONENT_TYPES;
	|-------------
	| COMPONENT0;
	-------------------------------------------------------------------------

	| MakeTerminal: COMPONENT & DIRECTION --> TERMINAL
	|---------------
	| MakeTerminal = (lambda c:COMPONENT; d:DIRECTION @
	|	(mu t:TERMINAL | t.Anchor=c /\ t.Direction=d))
NODE_COMPONENT, ARC_COMPONENT and ISA_COMPONENT are simply a conveniences to refer to arcs and nodes.
	NODE_COMPONENT =^= [COMPONENT | Role in ran node]

	ARC_COMPONENT =^= [COMPONENT | Role in ran arc]

	ISA_COMPONENT =^= [COMPONENT | Role in ran isa_arc]
The functions Terminal and TerminalDir are conveniences to extract individual terminals and direction of individual terminals from arcs.
	| NULLCOMPONENT: COMPONENT

	| 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;

A Basic Graph

So far, the discussion has centered around the parts of a simple graph; however the intent was to describe typed graphs. Nodes and arcs all have one or more supertypes. In this specification, types are just other components of the graph. A 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.

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. A graph always contains the basic components node, arc, and isa.

Within a graph, we can 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!

There are several constraints on a TYPED_GRAPH:

[Implementation:
declaration and code]
	%% inrel parentof

	%% inrel ancestorof

	%% inrel isa

	---GRAPH0---------------------------------------------------------------
	| Contents: P COMPONENT;
	| TOP: COMPONENT;
	| NODE: NODE_COMPONENT;
	| ARC: ARC_COMPONENT;
	| ISA: ISA_COMPONENT;
	| Level1Objects: P COMPONENT;
	| _ parentof _ : COMPONENT <-> COMPONENT;
	| _ ancestorof _ : COMPONENT <-> COMPONENT;
	| _ isa _ : COMPONENT <-> COMPONENT;
	| % these next 3 awkwardly shadow the above due to syntax constraints
	| parentof0 : COMPONENT <-> COMPONENT;
	| ancestorof0 : COMPONENT <-> COMPONENT;
	| isa0 : COMPONENT <-> COMPONENT;
	|--------------
	| Level1Objects = {TOP, NODE, ARC, ISA};
	| forall c,p:Contents @ p->c in parentof0   <=> p parentof   c;
	| forall c,p:Contents @ p->c in ancestorof0 <=> p ancestorof c;
	| forall c,p:Contents @ c->p in isa0        <=> c isa        p;
	| Level1Objects subseteq Contents;
	|
	| % _ parentof _ : a little complicated because we need a special case
	| %                for ISA_COMPONENTs to prevent endless recursion of isa's
	| (forall p,c:Contents | p /= ISA @
	|	p parentof c <=> (exists a:ISA_COMPONENT | a in Contents @
	|		GetTerminal(a,2) = p /\ GetTerminal(a,1) = c))
	| /\
	| (forall p,c:Contents | p = ISA @
	|	p parentof c <=> (c.Role in ran isa_arc /\ p /= c /\
	|		not (exists a:ISA_COMPONENT | a in Contents @
	|			GetTerminal(a,2) = p /\ GetTerminal(a,1) = c)));
	|
	| % _ancestorof _
	| forall c1,c2:Contents @
	|	c1 ancestorof c2 <=> (c1,c2) in ( _ parentof _ )^*;
	|
	| % _ isa _
	| forall p,c:Contents @ c isa p <=> ((p = c) \/ (p ancestorof c));
	|
	| % details of the level 1 components
	| TOP.Name = T;
	| TOP.Level = 1;
	|
	| NODE.Name = Node;
	| NODE.Level = 1;
	| NODE.Role in ran node;
	|
	| ARC.Name = Arc;
	| ARC.Level = 1;
	| #(arc~(ARC.Role)).Terminals = 0;
	|
	| ISA.Name = IsA;
	| ISA.Level = 1;
	| GetTerminal(ISA,1) = TOP;
	| GetTerminal(ISA,2) = TOP;
	|
	| % the type hierarchy for the level 1 components
	| NODE isa TOP;
	| ARC isa TOP;
	| ISA isa ARC;
	|
	| % The only level 1 objects are TOP, NODE, ARC, and ISA and their
	| % isa arcs that define the type hierarchy
	| #{c:COMPONENT | c.Level = 1} = 7;
	|
	| % there are no cycles over the isa relationship
	| forall c:Contents @ not (c ancestorof c);
	|
	| % everything is a NODE or ARC, but only one of these
	| forall c:Contents @
	|	(c isa NODE \/ c isa ARC)		/\
	|	(c isa NODE) => not (c isa ARC)		/\
	|	(c isa ARC ) => not (c isa NODE);
	|
	------------------------------------------------------------------------

VALIDATORS are Constraints

We need a way to constrain components (the next thing we want to do is constrain all arcs so that they can't terminate on themselves). To do that, we will enable Validators which act as constraint rules. A Validator will merely be a boolean function taking applied to a Component in the context of a graph. Since these constraints will apply to all subtypes (as defined by ISA_COMPONENT, below), it is necessary to use two Components as arguments -- the first is the exact object under inspection, and the second is the supertype that actually contains the validator. In general, in the implementation, it is expected that actual validators would be function objects. [Implementation:
declaration]

	VRES ::= PASS | FAIL

	VALIDATOR == COMPONENT & COMPONENT & GRAPH0 --> VRES
In the follwing, we define a few VALIDATORS that we will need shortly.

No arc may refer to itself. This rule will be added to the definition of an ARC. [Implementation: code]

	| NoSelfReference: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   NoSelfReference(apply,owner,g) =
	|     if (forall t:second(| (arc~(apply.Role)).Terminals |) @
	|						apply /= t.Anchor)
	| 		then PASS
	|		else FAIL
The following 3 VALIDATOR templates restricts the arity of an arc. They are actually a functions that takes a positive integer argument and return a VALIDATOR that restricts the arity to be equal-to/greater-than/less-than the value of the argument. This can be easily implemented as a C++ function object (with state -- the argument). [Implementation: code]
	| ArityEquals: N1 --> VALIDATOR
	|---------------
	| forall n: N1 @
	|   ArityEquals(n) = (mu v:VALIDATOR |
	|     forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|       v(apply,owner,g) =
	|         if (#((arc~(apply.Role)).Terminals) = n)
	|		then PASS
	|		else FAIL)
The Directed VALIDATOR specifies a binary from-to arc. [Implementation: code]
	| Directed: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   Directed(apply,owner,g) =
	|     if (ArityEquals(2)(apply,owner,g)=PASS	/\
	|	  GetTerminalDir(apply,1) = FROM	/\
	|	  GetTerminalDir(apply,2) = TO)
	| 		then PASS
	|		else FAIL
The Upward VALIDATOR is a specialization of the Directed VALIDATOR that must be from an object at a level lower or equal to the the level of the to side. Also, the level of the isa arc itself must be the same as that of the from side. [Implementation: code]
	| Upward: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   Upward(apply,owner,g) =
	|     if (Directed(apply,owner,g)=PASS		/\
	|	  (GetTerminal(apply,1)).Level >=  (GetTerminal(apply,2)).Level /\
	|	  apply.Level <= (GetTerminal(apply,1)).Level)
	| 		then PASS
	|		else FAIL
An arc cannot refer to anything outside the graph it is contained in. This validator is related to the NoDanglingTerminals validator, but this one allows dangling terminals and explicity checks for graph membership (NoDanglingTerminals doesn't). [Implementation: code]
	| ConfinedToGraph: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   ConfinedToGraph(apply,owner,g) =
	|     if (forall i:N | i<=#(arc~(apply.Role)).Terminals @
	|		GetTerminal(apply,i) in (g.Contents || {NULLCOMPONENT}))
	| 		then PASS
	|		else FAIL
A component cannot override a CONSTANT attribute. [Implementation: code]
	| NoConstAttrOverrides: VALIDATOR
	|--------------
	| forall apply, owner: COMPONENT @ forall g: GRAPH0 @
	|   NoConstAttrOverrides(apply,owner,g) =
	|     if (forall a:apply.Attributes @
	|	not (exists c2:g.Contents | c2->apply in g.ancestorof0 @
	|	  forall a2:c2.Attributes | a2.Name = a.Name @ CONSTANT in a2.Flags))
	| 		then PASS
	|		else FAIL
Arcs must conform to their parents' arcs; that is, the child's arity must be greater than or equal to the arity of the parent, and all terminating objects in the child must be sub-types (or equal) of the corresponding (and non-missing) types of the parent's terminating objects. [Implementation: code]
	| ArcConformance: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   ArcConformance(apply,owner,g) =
	|     if (forall c2:ARC_COMPONENT | c2 in g.Contents /\ c2->apply in g.ancestorof0 @
	|           % subtypes must have equal or more terminals
	|           #(arc~(c2.Role)).Terminals <= #(arc~(apply.Role)).Terminals /\
	|           % subtypes must type-conform at each terminal
	|           (forall i:Z | i<=#(arc~(c2.Role)).Terminals @
	|	      GetTerminal(apply,i)->GetTerminal(c2,i) in g.isa0))
	| 		then PASS
	|		else FAIL
Arcs between arcs are not allowed (except ARC itself and all ISA arcs). Can be used at the ARC level to force first order graphs. [Implementation: code]
	| NoArcBtwnArcs: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   NoArcBtwnArcs(apply,owner,g) =
	|     if ((apply->g.ARC in g.isa0 /\ apply /= g.ARC /\ not(apply->g.ISA in g.isa0)) => (forall t:TERMINAL |
	|            t in ran (arc~(apply.Role)).Terminals @ t.Anchor->g.NODE in g.isa0))
	|		then PASS
	|		else FAIL
An arc with the NoDanglingTerminals contraint must have all its terminals linked to a valid object in the graph (none must be uninstantiated or "dangling"). This constraint naturally applies to all isa arcs. Note that this is related to the ConfinedToGraph validator, ConfinedToGraph allows dangling terminals while this one doesn't, and also doesn't explicitly check for membership in the graph. [Implementation: code]
	| NoDanglingTerminals: VALIDATOR
	|--------------
	| forall apply, owner: ARC_COMPONENT @ forall g: GRAPH0 @
	|   NoDanglingTerminals(apply,owner,g) =
	|     if (forall i:N | i<=#(arc~(apply.Role)).Terminals @
	|	    GetTerminal(apply,i) in g.Contents)
	| 		then PASS
	|		else FAIL

Finally, a Typed Graph

Now validators have been specified and several instances of validators have been fleshed out, we can describe a TYPED_GRAPH. A typed graph has several constraints over GRAPH0: All of the above rules are applied as constraints (VALIDATORS) on the three basic components in the graph. We further specify that all these validators must be satified for every subtype of these; and since everything is a subtype of exactly one of these, the entire graph is appropriately constrained. [Implementation:
declaration and code]
	---TYPED_GRAPH-----------------------------------------------------------
	| GRAPH0;
	|-------------
	| % T restrictions
	| {NoConstAttrOverrides} subseteq TOP.Constraints;
	|
	| % arc restrictions
	| {NoSelfReference, ConfinedToGraph, ArcConformance}
	|	subseteq ARC.Constraints;
	|
	| % an isa arc is binary upward-directed arc (recall that ISA isa ARC, and
	| % "inherits" its constraints)
	| {Upward, NoDanglingTerminals} subseteq ISA.Constraints;
	|
	| % all components satisfy their constraints
	| exists g:GRAPH0 | g.Contents = Contents @
	|    forall c:g.Contents @
	|	forall c2:g.Contents | c isa c2 @ forall v:VALIDATOR | v in c2.Constraints @
	|		v(c,c2,g) = PASS;
	|
	--------------------------------------------------------------------------
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->c2 in g.isa0 @
		c1->g.NODE in g.isa0 <=> c2->g.NODE in g.isa0 /\
		c1->g.ARC  in g.isa0 <=> c2->g.ARC  in g.isa0 /\
		c1->g.ISA  in g.isa0 <=> c2->g.ISA  in g.isa0

First-order Typed Graphs

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). [Implementation:
declaration and code]
	%% state-schema FIRST_ORDER_TYPED_GRAPH

	FIRST_ORDER_TYPED_GRAPH =^= [TYPED_GRAPH |
	    {NoArcBtwnArcs} subset ARC.Constraints
	    ]

Operators on Typed Graphs

To following 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<> | 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 {x:GETATTR_RESULT | forall c2:g.Contents | c2->c in g.parentof0 @
	|						x=getAttr(g,c2,a)} = {}
	|	  % attribute not found
	|         then NULLr
	|	  % attribute found in one of the ancestors
	|         else (mu x:ATTRIBUTE | forall c2:g.Contents | c2->c in g.parentof0 /\
	|		(exists y:ATTRIBUTE @ y=Attr~(getAttr(g,c2,a))) @
	|		  exists y:ATTRIBUTE | y=Attr~(getAttr(g,c2,a)) @
	|		    forall c3:g.Contents | c3->c in g.parentof0 /\
	|		      (exists z:ATTRIBUTE @ z=Attr~(getAttr(g,c3,a))) /\
	|		      (not (c3->c2 in g.ancestorof0)) @
	|		        exists z:ATTRIBUTE | z=Attr~(getAttr(g,c3,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<> | 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?})}
	--------------------------------------------------------------------------

The Operators

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);
	| 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;
	| not(arc? isa ISA);
	| not(arc? in Level1Objects);
	| Contents' = Contents || {arc?, (mu a:ISA_COMPONENT |
	|	GetTerminal(a,1)=arc? /\ GetTerminal(a,2)=type?)};
	--------------------------------------------------------------------------
But note that 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;
	| 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 removing 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 precondition.
	---REMOVE-----------------------------------------------------------------
	| Delta TYPED_GRAPH;
	| c?: COMPONENT;
	|---------------
	| TYPED_GRAPH';
	| c? in (Contents \ Level1Objects);
	| not (exists c2:Contents @ c2 isa c?);
	| Contents' = Contents \
	|	({c?} || {a:ARC_COMPONENT | (exists i:N @ GetTerminal(a,i)=c?)})
	--------------------------------------------------------------------------
	end specification