OpenMath Content Dictionary: graph1

Canonical URL:

http://www.dse.nl/~postma/graph1.ocd

CD File:

graph1.ocd

CD as XML Encoded OpenMath:

graph1.omcd

Defines:

arrowset, digraph, edgeset, graph, source, target, vertexset

Date:

2004-06-01

Version:

0 (Revision 12)

Review Date:

2006-06-01

Status:

experimental

This CD defines symbols for handling directed and undirected graphs. Authored by Hans Cuypers and Erik Postma. This version is edited by amc.

graph

Description:

This symbol represents an undirected graph. It takes two arguments: the vertex set of the graph and the edge set. The vertices can be arbitrary OpenMath objects. Each edge should be a set consisting of two vertices.

Example:

A path of length 2.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
      <OMA>
        <OMS cd="graph1" name="graph"/>
        <OMA>
          <OMS cd="set1" name="set"/>
          <OMI> 1 </OMI>
          <OMI> 2 </OMI>
          <OMI> 3 </OMI>
        </OMA>
        <OMA>
          <OMS cd="set1" name="set"/>
          <OMA>
    	<OMS cd="set1" name="set"/>
    	<OMI> 1 </OMI>
    	<OMI> 2 </OMI>
          </OMA>
          <OMA>
    	<OMS cd="set1" name="set"/>
    	<OMI> 2 </OMI>
    	<OMI> 3 </OMI>
          </OMA>
        </OMA>
      </OMA>
    </OMOBJ>

graph (set ( 1 , 2 , 3 ) , set (set ( 1 , 2 ) , set ( 2 , 3 ) ) )

$$\mathrm{graph}(\{1,2,3\},\{\{1,2\},\{2,3\}\})$$

Signatures:

sts

vertexset

Description:

This symbol represents the vertex set of a (directed or undirected) graph. It takes one argument, the graph.

Example:

If Gamma is a graph, the following function tests whether its argument v is a vertex of Gamma.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
        <OMBIND>
	<OMS cd="fns1" name="lambda"/>
	<OMBVAR>
	  <OMV name="v"/>
	</OMBVAR>
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMV name="v"/>
	  <OMA>
	    <OMS cd="graph1" name="vertexset"/>
	    <OMV name="Gamma"/>
	  </OMA>
	</OMA>
	</OMBIND>
      </OMOBJ>

lambda [ v ] . (in ( v, vertexset ( Gamma) ) )

$$\lambda \hspace{0.17em}v.v\in \mathrm{vertexset}\left(\Gamma \right)$$

Signatures:

sts

edgeset

Description:

This symbol represents the set of edges of an undirected graph. It takes one argument, the undirected graph.

Example:

Given a graph Gamma and two of its vertices v and w, this predicate asserts that they are adjacent.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
	<OMA>
	  <OMS cd="set1" name="in"/>
	  <OMA>
	    <OMS cd="set1" name="set"/>
	    <OMV name="v"/>
	    <OMV name="w"/>
	  </OMA>
	  <OMA>
	    <OMS cd="graph1" name="edgeset"/>
	    <OMV name="Gamma"/>
	  </OMA>
	</OMA>
      </OMOBJ>

in (set ( v, w) , edgeset ( Gamma) )

$$\{v,w\}\in \mathrm{edgeset}\left(\Gamma \right)$$

Commented Mathematical property (CMP):

Every edge in an undirected graph Gamma is a subset of the vertex set of size two.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
        <OMBIND>
	  <OMS cd="quant1" name="forall"/>
	  <OMBVAR>
	    <OMV name="e"/>
	    <OMV name="Gamma"/>
	  </OMBVAR>
	  <OMA>
	    <OMS cd="logic1" name="implies"/>
	    <OMA>
	      <OMS cd="set1" name="in"/>
	      <OMV name="e"/>
	      <OMA>
	        <OMS cd="graph1" name="vertexset"/>
		<OMV name="Gamma"/>
	      </OMA>
	    </OMA>
	    <OMA>
	      <OMS cd="logic1" name="and"/>
	      <OMA>
	        <OMS cd="set1" name="subset"/>
		<OMV name="e"/>
		<OMA>
		  <OMS cd="graph1" name="vertexset"/>
		  <OMV name="Gamma"/>
		</OMA>
	      </OMA>
	      <OMA>
	        <OMS cd="relation1" name="eq"/>
		<OMA>
		  <OMS cd="set1" name="size"/>
		  <OMV name="e"/>
		</OMA>
		<OMI> 2 </OMI>
	      </OMA>
	    </OMA>    
	  </OMA>
	</OMBIND>
      </OMOBJ>

forall [ e Gamma ] . (implies (in ( e, vertexset ( Gamma) ) , and (subset ( e, vertexset ( Gamma) ) , eq (size ( e) , 2 ) ) ) )

$$\forall \hspace{0.17em}e,\Gamma .e\in \mathrm{vertexset}\left(\Gamma \right)\Rightarrow e\subset \mathrm{vertexset}\left(\Gamma \right)\wedge \mathrm{size}\left(e\right)=2$$

Signatures:

sts

digraph

Description:

This symbol refers to a digraph. It has two arguments. The first is the set of vertices, the second is the set of arrows. Arrows are represented by lists of length two, where a list represents the arrow from the first element to the second.

Example:

The two-sided infinite directed path.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
        <OMA>
          <OMS cd="graph1" name="digraph"/>
          <OMS cd="setname1" name="Z"/>
  	  <OMA>
  	    <OMS cd="set1" name="map"/>
            <OMBIND>
  	      <OMS cd="fns1" name="lambda"/>
  	      <OMBVAR>
  	        <OMV name="x"/>
  	      </OMBVAR>
  	      <OMA>
  	        <OMS cd="list1" name="list"/>
  	        <OMV name="x"/>
  	        <OMA>
  	          <OMS cd="arith1" name="plus"/>
  		  <OMV name="x"/>
  		  <OMI> 1 </OMI>
  	        </OMA>
  	      </OMA>
  	    </OMBIND>
  	  </OMA>
        </OMA>
      </OMOBJ>

digraph (Z, map (lambda [ x ] . (list ( x, plus ( x, 1 ) ) ) ) )

$$\mathrm{digraph}(\mathbb{Z},\left\{(x,x+1)\right|x\in \})$$

Signatures:

sts

arrowset

Description:

This symbol represents the set of arrows of a directed graph. It takes one argument, the directed graph.

Example:

The arrow set of the loop consists of one loop.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
        <OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="graph1" name="arrowset"/>
	    <OMA>
	      <OMS cd="graph1" name="digraph"/>
	      <OMA>
	        <OMS cd="set1" name="set"/>
		<OMI> 1 </OMI>
	      </OMA>
	      <OMA>
    	        <OMS cd="set1" name="set"/>
      	        <OMA>
      	          <OMS cd="list1" name="list"/>
      	          <OMI> 1 </OMI>
      	          <OMI> 1 </OMI>
      	        </OMA>
	      </OMA>
	    </OMA>
	  </OMA>
	  <OMA>
	    <OMS cd="set1" name="set"/>
	    <OMA>
	      <OMS cd="list1" name="list"/>
	      <OMI> 1 </OMI>
	      <OMI> 1 </OMI>
	    </OMA>
	  </OMA>
	</OMA>
      </OMOBJ>

eq (arrowset (digraph (set ( 1 ) , set (list ( 1 , 1 ) ) ) ) , set (list ( 1 , 1 ) ) )

$$\mathrm{arrowset}\left(\mathrm{digraph}(\left\{1\right\},\left\{(1,1)\right\})\right)=\left\{(1,1)\right\}$$

Signatures:

sts

source

Description:

Given an arrow, this symbol refers to the vertex where the arrow starts. It takes one argument, the arrow.

Example:

The arrow [a, b] starts at a.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
        <OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="graph1" name="source"/>
	    <OMA>
	      <OMS cd="list1" name="list"/>
	      <OMV name="a"/>
	      <OMV name="b"/>
	    </OMA>
	  </OMA>
	  <OMV name="a"/>
	</OMA>
      </OMOBJ>

eq (source (list ( a, b) ) , a)

$$\mathrm{source}\left((a,b)\right)=a$$

Signatures:

sts

target

Description:

Given an arrow, this symbol refers to the vertex the arrow points to. It takes one argument, the arrow.

Example:

The arrow [a, b] points to b.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath" version="2.0">
        <OMA>
	  <OMS cd="relation1" name="eq"/>
	  <OMA>
	    <OMS cd="graph1" name="target"/>
	    <OMA>
	      <OMS cd="list1" name="list"/>
	      <OMV name="a"/>
	      <OMV name="b"/>
	    </OMA>
	  </OMA>
	  <OMV name="b"/>
	</OMA>
      </OMOBJ>

eq (target (list ( a, b) ) , b)

$$\mathrm{target}\left((a,b)\right)=b$$

Signatures:

sts