Data Structures / Algebraic Semantics

~ Under Construction ~

 

Product Type Constructor
Natural Numbers
Stack[Item]
List[Item]
Queue[Item]
BinaryTree[Item]
Directed Graph

Overview

An ontology that claims to represent data structures should be able to model the axiomatic semantics of the commonly occurring data structures, such as stacks, arrays, queues, binary trees, trees, s-expressions, nested lists, directed graphs, etc. Most data structure types have three classes of operations: constructors, accessors and tests. When suitably expressive, data structure types should allow for the recursive definitions of functions.

New Tags and Attributes

For greater convenience in data structuring and algebraic semantics, we have included src and tgt referencing attributes, in addition to the previous obj referencing attribute, and we have extended the Function element to include a free-standing version. With the src and tgt attributes we can embed functions in object specifications when the ambient object is either the source or target of the function.

Most container classes have a parameter type, which is the type of the contained items. In order to accomodate this, a parameterType attribute has been added to the Object tag.

The Product, pair, triple, tuple, project tags are new to the OML ontology. The Product tag gives the cartesian product of two or more parameter types. The tags pair, triple, tuple and project work at the instance level, giving (for binary products) the pairing of two instances and the projection to the first and second instance of a pairing.

We introduce the generic equality assertion equal for any two entities of the same type. This works at the instance level. The synonymous specification (a special case of sequent) works at the type level - it represents equivalence of types and hence equality of their extents. The equiv element works for expressions - it represents equivalence of expressions.

We introduce the various relational operators as binary relations on any ordinal data type. By definition, an ordinal data type is a subtype of the generic Order type. These operators include less, lessEqual, equal, greater and greaterEqual.

In addition to object types, relation types and function types, we are introducing constant types. With the existence of constants, the values of the obj attribute are either object-references, variables or constants. Constants could be viewed as either types or instances. Just like function types, these are specified within object types called their attachment. To view them as types in specification, regard them as functions from the unit type to their type attachment. But, we are attaching them to their target type, not their source type. For example, the constant number 3 is the function

3 : Unit ! data.Natno.

Product Type Constructor

Any finite collection of OML types have a product that is specified with the OML Product element. The Product tag gives the cartesian product of two or more parameter types. For binary products the tags pair and project work at the instance level, giving the pairing of two instances and the projection to the first and second instance of a pairing. The product SxT of two types S and T is specified in an ontology as follows.

<Product type="SxT" first="S" second="T"/>

When pairings, triplings or tuplings are needed, either in specifying axiomatics or defining objects and relations, two forms can be used. Either use embedded objects

<pair var="p" type="SxT"><S obj="s"/><T obj="t"/></pair>
<triple var="p" type="RxSxT"><R obj="r"/><S obj="s"/><T obj="t"/></triple>
<tuple var="p" type="T1x...xTn"><T1 obj="t1"/>...<Tn obj="tn"/></tuple>,

or use a tupling bracket and a defined object

<SxT id="p"><pair><S obj="s"/><T obj="t"/></pair></SxT>
<RxSxT id="p"><triple><R obj="r"/><S obj="s"/><T obj="t"/></triple></RxSxT>
<T1x...xTn id="p"><tuple><T1 obj="t1"/>...<Tn obj="tn"/></tuple></T1x...xTn>.
<Assertion>
  <comment>a pairing followed by a projection is the identity</comment>
  <Forall var="s" type="S">
  <Forall var="t" type="T">
  <Forall var="p" type="SxT">
    <implies>
      <pair var="p" type="SxT"><S obj="s"/><T obj="t"/></pair>
      <project var="p" type="SxT" var="s" type="S"/>
    </implies>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

Natno

From the standpoint of algebraic semantics, a natural number is the most basic number. For this reason in the basic OML ontology there is already a natural number type called data.Natno. Although natural numbers are not usually explicitly included as a builtin data type in programming languages, if semantics represents what is used, then it should certainly be included. Here we (somewhat redundantly) include a natural number specification. The Natno signature is pictured on the right.

Constructors
There is a "zero" natno, and each number has a "succ" (successor). All natnos can be constructed with these operations.
Accessors
Each natno has a "pred" (predecessor).
Tests
A boolean function can test whether a natno "iszero" or not.
Recusion
Any two natnos can be "add" (added). This operation can be recursively defined.

In the following ontological specification we give an OML version of the Natno data type, complete with suitable axiomatic semantics.

<Product type="Natno-Natno" first="Natno" second="Natno"/> 

<Object type="Natno">
  <Constant type="zero"/>
  <Function type="push" srcType="Natno"/>
  <Function type="pred" tgtType="Natno"/>
  <Function type="iszero" tgtType="Boole"/>
</Object>

<Function type="add" srcType="Natno-Natno" tgtType="Natno"/>    /* free-standing function specification */

<Assertion>
  <comment>the zero is zero</comment>
  <Natno src="zero"><iszero tgt="True"></Natno>
</Assertion>

<Assertion>
  <comment>a successor na natno is not zero</comment>
  <Forall var="natno" type="Natno">
  <Forall var="natno1" type="Natno">
    <implies>
      <Natno tgt="natno1"><succ src="natno"></Natno>
      <Natno src="natno1"><iszero tgt="False"></Natno>
    </implies>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>any natno is either zero or a successor natno</comment>
  <Forall var="natno" type="Natno">
    <or>
      <Natno src="natno"><iszero tgt="True"></Natno>
      <Exists var="natno1" type="Natno">
        <Natno tgt="natno"><succ src="natno1"></Natno>
      </Exists>
    </or>
  </Forall>
</Assertion>

<Assertion>
  <comment>succ-pred semantics</comment>
  <Forall var="natno" type="Natno">
  <Forall var="natno1" type="Natno">
    <implies>
      <Natno tgt="natno1"><succ src="natno"></Natno>
      <Natno src="natno"><pred tgt="natno1"></Natno>
    </implies>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>succ-pred semantics</comment>
  <Forall var="natno" type="Natno">
    <implies>
      <Natno src="natno"><iszero tgt="False"></Natno>
      <Forall var="natno1" type="Natno">
        <implies>
          <Natno src="natno"><pred tgt="natno1"></Natno>
          <Natno tgt="natno"><succ src="natno1"></Natno>
        </implies>
      </Forall>
    </implies>
  </Forall>
</Assertion>

<Assertion>
  <comment>add definition</comment>
  <Forall var="natno" type="Natno">
  <Forall var="pr" type="Natno-Natno">
    <implies>
      <pair src="zero" tgt="natno" obj="pr"/>
      <add src="pr" tgt="natno"/>
    </implies>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>add definition</comment>
  <Forall var="natno" type="Natno">
  <Forall var="natno1" type="Natno">
  <Forall var="natno2" type="Natno">
  <Forall var="pr" type="Natno-Natno">
  <Forall var="pr1" type="Natno-Natno">
  <Forall var="natno3" type="Natno">
  <Forall var="natno4" type="Natno">
    <implies>
      <and>
        <Natno tgt="natno1"><succ src="natno"></Natno>
        <pair src="natno" tgt="natno2" obj="pr"/>
        <add src="pr" tgt="natno3"/>
        <pair src="natno1" tgt="natno2" obj="pr1"/>
        <add src="pr1" tgt="natno4"/>
      </and>
      <Natno tgt="natno4"><succ src="natno3"></Natno>
    </implies>
  </Forall>
  </Forall>
</Assertion>

Stack[Item]

A stack is a linear data structure, and one of the most basic types of container classes.

Constructors
There is an "empty" stack, and items can be "pushed" onto one end of the stack called the top. All stacks can be constructed with these operations.
Accessors
The "top" item can be accessed, and items can be taken or "popped" off the same end leaving a slightly smaller "popped" stack.
Tests
A boolean function can test whether a stack "isempty" or not.

In the following ontological specification we give an OML version of the Stack data structure, complete with LIFO (Last In First Out) axiomatic semantics.

<Product type="Item-Stack" first="Item" second="Stack"/> 

<Object type="Stack" parameterType="Item">
  <Constant type="empty"/>
  <Function type="push" srcType="Item-Stack"/>
  <Function type="top" tgtType="Item"/>
  <Function type="pop" tgtType="Stack"/>
  <Function type="isempty" tgtType="Boolean"/>
</Object>

<Assertion>
  <comment>the empty stack is empty</comment>
  <Stack src="empty"><isempty tgt="True"></Stack>
</Assertion>

<Assertion>
  <comment>a pushed stack is not empty</comment>
  <Forall var="itstk" type="Item-Stack">
  <Forall var="stk" type="Stack">
    <implies>
      <Stack tgt="stk"><push src="itstk"></Stack>
      <Stack src="stk"><isempty tgt="False"></Stack>
    </implies>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>any stack is either empty or a pushed stack</comment>
  <Forall var="stk" type="Stack">
    <or>
      <Stack src="stk"><isempty tgt="True"></Stack>
      <Exists var="itstk" type="Item-Stack">
        <Stack tgt="stk"><push src="itstk"></Stack>
      </Exists>
    </or>
  </Forall>
</Assertion>

<Assertion>
  <comment>LIFO semantics</comment>
  <Forall var="stk" type="Stack">
  <Forall var="stk1" type="Stack">
  <Forall var="it" type="Item">
  <Forall var="itstk" type="Item-Stack">
    <implies>
      <and>
        <Stack tgt="stk"><push src="itstk"></Stack>
        <Stack src="stk"><top tgt="it"></Stack>
        <Stack src="stk"><pop tgt="stk1"></Stack>
      </and>
      <pair first="it" second="stk1" obj="itstk"/>
    </implies>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>LIFO semantics</comment>
  <Forall var="stk" type="Stack">
  <Forall var="stk1" type="Stack">
  <Forall var="it" type="Item">
  <Forall var="itstk" type="Item-Stack">
    <implies>
      <and>
        <Stack src="stk"><isempty tgt="False"></Stack>
        <Stack src="stk"><top tgt="it"></Stack>
        <Stack src="stk"><pop tgt="stk1"></Stack>
        <pair first="stk1" second="it" obj="itstk"/>
      </and>
      <Stack tgt="stk"><push src="itstk"></Stack>
    </implies>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

Example: Instance of Stack[data.Natno]

Ontology

<OML>
  <Ontology id="StackExample" version="1.0">
    <extends ontology="http://www.oml.org/ontology/" prefix="OML"/>
    <Object type="StackNatno" parameterType="data.Natno">
      <Constant type="empty"/>
      <Function type="top" tgtType="data.Natno"/>
      <Function type="pop" tgtType="Stack"/>
      <Function type="isempty" tgtType="Boole"/>
    </Object>
    <Collection type="CollectionStackNatno" genus="StackNatno"/>
  </Ontology>
</OML>

Consider the stack of natural numbers (3,5,8,0,4) with top on the left. We give three ways to define this stack in a local collection: a canonical form, an embedded form, and an abbreviated form.

Canonical Form

<OML>
  <CollectionStackNatno id="myStack">
    <Stack id="fifth"> <top obj="3"/><pop obj="fourth"/></Stack>
    <Stack id="fourth"><top obj="5"/><pop obj="third"/> </Stack>
    <Stack id="third"> <top obj="8"/><pop obj="second"/></Stack>
    <Stack id="second"><top obj="0"/><pop obj="first"/> </Stack>
    <Stack id="first"> <top obj="4"/><pop obj="empty"/> </Stack>
  </CollectionStackNatno>
</OML>

This looks like the usual linked-list representation for a stack. This local version seems rather inefficient, and it is. The advantage to OML stacks is that they can be distributed all over the world with no changes to the representation.

Embedded Form

<OML>
  <CollectionStackNatno id="myStack">
    <Stack>
      <top obj="3"/>
      <Stack>
        <top obj="5"/>
        <Stack>
          <top obj="8"/>
          <Stack>
            <top obj="0"/>
            <Stack>
              <top obj="4"/>
              <Stack>
              </Stack>
            </Stack>
          </Stack>
        </Stack>
      </Stack>
    </Stack>
  </CollectionStackNatno>
</OML>

Abbreviated Form

<OML>
  <CollectionStackNatno id="myStack">
    <Stack>
      <top obj="3"/>
      <top obj="5"/>
      <top obj="8"/>
      <top obj="0"/>
      <top obj="4"/>
    </Stack>
  </CollectionStackNatno>
</OML>

Compare the latter abbreviated form with the RDF sequence container.


List[Item]

Although the nested list data type can originate as a restriction from the s-expression data type (all cdr's must be lists), it is usually given its own recursive definition which is an extension of the stack data type definition.

A (nested) list is a 2-dimensional data structure.

Constructors
There is an "empty" list, and either items or lists can be "pushed" onto one end of the list called the first element. All lists can be constructed with these operations.
Accessors
The "first" item can be accessed, and either items or lists can be taken off the same end leaving the "rest" of the list which is another list.
Tests
A boolean function can test whether a list "isempty" or not.

In the following ontological specification we give an OML version of the List data structure, complete with list axiomatic semantics.

<Product type="(Item+List)xList" first="Item+List" second="List"/>
<Sum type="Item+List" first="Item" second="List"/> 

<Object type="List" parameterType="Item">
  <Constant type="empty"/>
  <Function type="make" srcType="Item+List)xList"/>
  <Function type="first" tgtType="Item+List"/>
  <Function type="rest" tgtType="List"/>
  <Function type="isempty" tgtType="Boole"/>
</Object>

...


Queue[Item]

A (circular) queue is a very useful container class. There are several ways of defining the queue operations. One can "enqueue" an item by adding it to the rear of the queue. One can "dequeue" an item by removing it from the front of the queue. Removal returns an item-queue pair. One can test whether the queue is empty or not. For finite queues (the circular case) one can test whether the queue is empty or full. Queus have a size, which means the number of items currently in the queue. Finite queues also have a maxsize. We visualize a (circular) queue of maxsize 12 on the right. Currently this contains five items.

In the following ontological specification we give an OML version of the (circular) Queue data type, complete with axiomatic semantics.

<Product type="Item-Queue" first="Item" second="Queue"/> 

<Object type="Queue" parameterType="Item"/>
  <Constant type="empty"/>
  <Constant type="full"/>
  <Function type="isempty" tgtType="Boole"/>
  <Function type="isfull" tgtType="Boole"/>
  <Function type="size" tgtType="Natno"/>
  <Function type="maxsize" tgtType="Natno"/>
  <Function type="enqueue" srcType="Item-Queue"/>
  <Function type="dequeue" tgtType="Item-Queue"/>
</BinaryTree>

<Assertion>
  <comment>the empty queue is empty</comment>
  <Queue src="empty"><isempty tgt="True"></Queue>
</Assertion>

<Assertion>
  <comment>the empty queue has zero size</comment>
  <Queue src="empty"><size tgt="zero"></Queue>
</Assertion>

<Assertion>
  <comment>the full queue is full</comment>
  <Queue src="full"><isfull tgt="True"></Queue>
</Assertion>

<Assertion>
  <comment>the full queue has maximum size</comment>
  <Queue src="full"><size tgt="maxsize"></Queue>
</Assertion>

<Assertion>
  <comment>the size is bounded by the maxsize</comment>
  <Forall var="q" type="Queue">
  <Forall var="s" type="Natno">
  <Forall var="m" type="Natno">
    <implies>
      <and>
        <Queue src="q"><size tgt="s"></Queue>
        <Queue src="q"><maxsize tgt="m"></Queue>
      </and>
      <lesseq src="s" tgt="m"/>
    </implies>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>the maximum size is invariant under addition</comment>
  <Forall var="q" type="Queue">
  <Forall var="it" type="Item">
  <Forall var="pr" type="Item-Queue">
  <Forall var="q1" type="Queue">
  <Forall var="m" type="Natno">
  <Forall var="m1" type="Natno">
    <implies>
      <and>
        <Queue src="q"><maxsize tgt="m"></Queue>
        <pair first="it" second="q" obj="pr"/>
        <Queue tgt="q1"><enqueue src="pr"></Queue>
        <Queue src="q1"><maxsize tgt="m1"></Queue>
      </and>
      <equal src="m" tgt="m1"/>
    </implies>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>the size is incremented under addition</comment>
  <Forall var="q" type="Queue">
  <Forall var="it" type="Item">
  <Forall var="pr" type="Item-Queue">
  <Forall var="q1" type="Queue">
  <Forall var="m" type="Natno">
  <Forall var="m1" type="Natno">
    <implies>
      <and>
        <Queue src="q"><size tgt="m"></Queue>
        <pair first="it" second="q" obj="pr"/>
        <Queue tgt="q1"><enqueue src="pr"></Queue>
        <Queue src="q1"><size tgt="m1"></Queue>
      </and>
      <Natno tgt="m1"><succ src="m"></Natno>
    </implies>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
</Assertion>


BinaryTree[Item]

A binary tree is one of the simpest non-linear data structures.

Constructors
The basic constructors are the "empty" binary tree and the "make" tree operation: an item and two binary trees "left" and "right" can be used to construct a slightly larger binary tree. All binary trees can be constructed with these operations.
Accessors
In the reverse deconstructing direction there are three accessor operations "top", "left" tree and "right" tree.
Tests
A boolean function can test whether a binary tree "isempty" or not.

In the following ontological specification we give an OML version of the BinaryTree data structure, complete with axiomatic semantics.

<Product type="Item-BinaryTree-BinaryTree"
  first="Item" second="BinaryTree" third="BinaryTree"> 

<Object type="BinaryTree" parameterType="Item"/>
  <Constant type="empty"/>
  <Function type="make" srcType="Item-BinaryTree-BinaryTree"/>
  <Function type="top" tgtType="Item"/>
  <Function type="left" tgtType="BinaryTree"/>
  <Function type="right" tgtType="BinaryTree"/>
  <Function type="isempty" tgtType="Boole"/>
</BinaryTree>

<Assertion>
  <comment>the empty binary tree is empty</comment>
  <BinaryTree src="empty"><isempty tgt="True"></BinaryTree>
</Assertion>

...

<Assertion>
  <comment>binary tree semantics</comment>
  <Forall var="bt" type="BinaryTree">
  <Forall var="lbt" type="BinaryTree">
  <Forall var="rbt" type="BinaryTree">
  <Forall var="it" type="Item">
  <Forall var="itbtbt" type="Item-BinaryTree-BinaryTree">
    <implies>
      <and>
        <BinaryTree tgt="bt"><make src="itbtbt"></BinaryTree>
        <BinaryTree src="bt"><top tgt="it"></BinaryTree>
        <BinaryTree src="bt"><left tgt="lbt"></BinaryTree>
        <BinaryTree src="bt"><right tgt="rbt"></BinaryTree>
      </and>
      <triple first="it" second="lbt" third="rbt" obj="itbtbt"/>
    </implies>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

<Assertion>
  <comment>binary tree semantics</comment>
  <Forall var="bt" type="BinaryTree">
  <Forall var="lbt" type="BinaryTree">
  <Forall var="rbt" type="BinaryTree">
  <Forall var="it" type="Item">
  <Forall var="itbtbt" type="Item-BinaryTree-BinaryTree">
    <implies>
      <and>
        <BinaryTree src="bt"><isempty tgt="False"></BinaryTree>
        <BinaryTree src="bt"><top tgt="it"></BinaryTree>
        <BinaryTree src="bt"><left tgt="lbt"></BinaryTree>
        <BinaryTree src="bt"><right tgt="rbt"></BinaryTree>
        <triple first="it" second="lbt" third="rbt" obj="itbtbt"/>
      </and>
      <BinaryTree tgt="bt"><make src="itbtbt"></BinaryTree>
    </implies>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
  </Forall>
</Assertion>

Directed Graph

A directed graph is a non-recursive data structure. It consists of a set of nodes N, a set of edges E, and two functions called source and target running from edges to nodes.

 

 

As an illustrious example, consider the digraph pictured on the right. This graph has 3 nodes N = {n1, n2, n3} and 5 edges E = {e1, e2, e3, e4, e5}. The edge e2 has source node n1 and target node n2.

(ontology)
<CKML>
  <Ontology id="graph-example" version="1.0">
    <extends ontology="http://www.oml.org/ontology/" prefix="OML"/>
    <Object type="Node"/>
    <Object type="Edge">
      <Function type="source" tgtType="Node"/>
      <Function type="target" tgtType="Node"/>
    </Object>
    <Collection type="Set.Node" genus="Node"/>
    <Collection type="Set.Edge" genus="Edge"/>
    <Collection type="Graph" genus="OML#Collection"/>
  </Ontology>
</CKML>
(collections)
<CKML>
  <Graph id="example" ontology="http://www.example.org/ontology/">
    <Set.Node>
      <Node id="n1"/>
      <Node id="n2"/>
      <Node id="n3"/>
    </Set.Node>
    <Set.Edge>
      <Edge id="e1"><source tgt="n1"/><target tgt="n1"/></Edge>
      <Edge id="e2"><source tgt="n1"/><target tgt="n2"/></Edge>
      <Edge id="e3"><source tgt="n1"/><target tgt="n3"/></Edge>
      <Edge id="e4"><source tgt="n3"/><target tgt="n2"/></Edge>
      <Edge id="e5"><source tgt="n2"/><target tgt="n3"/></Edge>
    </Set.Edge>
  </Graph>
</CKML>

 

Please send questions, comments and
suggestions about this page to:
Robert E. Kent rekent@eecs.wsu.edu

Last modification date: December 1998