Getting Started with IBML Type Definitions

Original Version 2001-10-22
First reformatted for the web 2005-02-14

Editors:: Richard Weyhrauch (IBUKI), Carolyn Talcott

Note:

The information in this document (and its companion documents) is the confidential proprietary property of IBUKI. It contains trade secret, published and unpublished components. The IBML system (appearing under various names) has been developed over a substantial period of time at IBUKI's expense.

Abstract

This document describes a subset of the data structures used by the IBUKI Modeling Language, IBML. Its purpose is to provide a way that allows people to begin to experiment with describing IBML Types. The IBML system, of course, defines and manipulate these as specific in memory data structures. Further constructs, the semantics of these constructs and the commands necessary to run the model builder are found in other documents.

1. Basic Data
2. Basic Types
3. Basic Tree Types
4. Adding New Types
5. Naming Types
6. Adding Parents
7. Adding Restrictions
8. Adding Components
Summary
Acknowledgments

1 Basic Data

We refer to the elements of the following sets of data, collectively, as IBML Basic Data. Each element of the following sets of data is different from any other. We imagine that the data used for numbers types are distinct. The intewger 5 is different from the rational 5/1 is different from the float 1.0 .

IBML Basic Data are either:

Two Boolean Constants written

:True
:False

Integer Constants written in the usual way, e.g.,

-749321
-6
0
293
128328287193289487593485992843579238749579459

Integer arithmetic is considered to be exact, so any number of digits is acceptable.

Rational Constants written in the usual way, e.g.,

-749321/34
-1/2
22/1
293/69
37/128328287193289487593485992843579238749579459

Rational Arithmetic is expected to be exact! It is not necesary to keep integers and rationals disjoint but in this formulation the integer n is not the same as the rational n/1. There is a practical reason for this which is not discussed in this document [RWW: this is currently under review by RWW and CLT].

Floating/Fixed Point Constants e.g.,

23.45
-259E498234982224492384928

Here we are thinking of fixed point and floating point numbers as a cute way of talking about rationals. Of course in real machines neither correctly obey the rules of arithemetic, so from this point of view, technically speaking, their behavior is wierd.

String Constants e.g.,

"Hello World"
"He said, \"Hello World\""

Here the '\' is an escape character that of course is not actually in the list. The exact meaning of "character" is left out allowing inplementations to use whatever encoding they like. For the purposes of this document we use the syntax of common lisp strings restricted to printable ASCII.

Symbol Constants e.g.,

Hello-World
1+ 
[INT]

For the purposes of this document we use the syntax of Common Lisp symbols without package designations and where the characters that can appear in a print name are restricted to printable ASCII characters. The first restriction means that we do not consider - :type - to describe a symbol although it would in Common Lisp. In other words, the print name of an IBML symbol can not contain the character ':'

2 Basic Types

All Basic Types are Types.

Base Types

The Base Types are

[BOOL]
[INT]
[RATIONAL]
[FLOAT]  
[STRING]
[SYMBOL]

All Base Types are Basic Types.

Constants for Ranges

In addition for any integer c the following are called Ranges

[c-INF], [INF-c]

For example,

[INF--247]
[-382319873918318923-INF]
[0-INF]
[1-INF]

Each of these is a Range and a Basic Type.

If c₁ and c₂ are two integers then the following are Ranges

[c₁-c₂]

We write just

[c₁]

when

c₁ = c₂

For example,

[-678--247]
[-382319873918318923-5]
[6-14]
[3]

Each of these is a Range and Basic Type.

Constants for Finite Sets of Basic Data

If d₁, ... , d_n are IBCL Basic Data then

{d₁ ...  d_n}

Each of these is a Basic Type.

For example,

{1 2 3}
(1/2 3/4 5/6 7/8}
("Hello World" "HelloMars" "Meet Fred"}
{1.2 3/2 98302198301820831 "An odd set of numbers."} 
{42 :True "maybe" :False}
{1.1 1.2 1.3 1.4 1.5 1.6 1.7 1.8 1.9}

are Basic Types.

3 Basic Tree Types

All Basic Tree Types are Types.

If t₁, ... , t_n are Basic Types and l₁, ... , l_n are n different IBCL Symbols then

[l₁:t₁ ... l_n:t_n]

Where the order of the labeled types does not matter. A special case of a Basic Tree Type is

[]

which is the tree without any labels and thus any example of a Tree Type is an example of this Type, i.e., it is the least specific of all Tree Types.

Each of these is a Basic Tree Type.

For example,

[x-coord:[INT] y-coord:{1 2 3)]

[meter-name:[STRING]
 values-possible:[0-100]
 confidence:{0.0 0.1 0.2 0.3 0.4 0.5 0.6 0.7 0.8 0.9 1.0}
]

[start-point:[x-coord:[INT] y-coord:[INT]]]
 end-point:[x-coord:[INT] y-coord:[INT]]]
]

[tool-name:[STRING]
 arg1-type:[INT]
 arg2-type:[INT]
 val-type:[INT]  
 result-location: []
]

4 Adding New Types

In a practical modeling system we need to be able to model sets of complex objects and systems, model the interconnections between parts of these (e.g., networks), processes and possible scenarios involving these things. Furthermore, A practical system needs to be able to verify if some real world things or activities are examples of things described in these models.

The collection of types described above is neither prima facie epistemologically adaquate to model these complex ideas nor clearly practically adaquate to form the basis of a usable application that will to model all the necessary complexity and be capable of detecting and configuring objects specified by these types.

IBML Basic Data, IBML Basic Types and IBML Basic Tree Types form the building blocks for the semantics of all IBML Types. They are extremely elementary in that each Basic Type is either a Literal or a simple finite tree, with labeled branches, whose leaves are Basic Types.

In the sections below we describe additional IBML Types that extend the complexity of the Basic Types and will allow us to do the kind of modeling described above.

5 Naming Types

We introduce the construct

(type <type-name>
  (its-attributes-are
    (attribute-name₁ :type <type₁>)
    ...
    (attribute-name_n :type <type_n>)
  )
)

The <type-name> in the above construct is itself a Type. There are several things about this construct. 1) By convention the "names" we use for new IBML Types are an IBML Symbol of the form [<char>*]. 2) we have a seperate level of parenthesis for "its attributes are". We will add more "clauses" below. 3) this construct mimics the structure structure of Basic Tree Types but there is no restriction here that <type_i> is a Basic Type, any Type will do.

A simple example is

(type [LatticePoint]
  (its-attributes-are
    (x-coord :type [INT])
    (y-coord :type [INT])
  )
)

means that when we see the Type [LatticePoint] we mean the anonomous (un-named) Type

[
  x-coord:[INT]
  y-coord:[INT]
]

Informally we could imagine

   [LatticePoint] = [x-coord:[INT] y-coord:[INT]]

but this is simply wrong!!!! They are different data structures.

A better take is: All examples of a

[LatticePoint]

are examples of

[x-coord:[INT] y-coord:[INT]]

and vice-versa. This is closer to the intended semantics of IBML Types.

Semantic Observations

At first blush it might seem that adding the ability to "name" types is an innocent addition to our type theory, but this is unfortunately not the case. There are two major consequences:

1) we eventually need to explain where the map between the "name" and its "definition" is kept (i.e., it is "outside" the type theory).

2) We now can specify Types like

(type [person]
  (it-atributes-are
    (name :type [STRING])
    (birth-year :type [INF-6000])
    (mother :type [person])
    (father :type [person])
  )
)

Even if there are infinitly many of examples of a Basic Type, BT, every example of BT "expands" to a finite structure. Unfortunatey, every "fully expanded" example of recursive Type like [person] is clearly an infinite structure. In the case of most Basic Types we have an infinite number of examples, each of which is a finite structure. In the case of [person] (a recursive Type) we have an infinite number of examples of [person]s, and each of these examples is itself an infinite object. Clearly it is not possible to put all the examples of one of these types in a data base. Any system we build must accomedate this observation.

6 Adding Parents

We extend the above construct to include

(type <type-name> subtype <parent-name>
  (its-attributes-are
    (attribute-name₁ :type <type₁>)
    ...
    (attribute-name_n :type <type_n>)
  )
)

Until this point we have not mentioned the fact that IBCL Types are partially ordered by a relation called refinement. In all uses of the "(type ...)" construct that mention a "parent" it is a property of the semantics of IBCL that the "named child" is a refinement of the parent.

Some examples are

(type [1D-LatticePoint-x] subtype []
  (its-attributes-are
    (x-coord :type [INT])
  )
)

(type [1D-LatticePoint-y] subtype []
  (its-attributes-are
    (y-coord :type [INT])
  )
)

(type [2D-LatticePoint-xy] subtype [1D-LatticePoint-x]
  (its-attributes-are
    (y-coord :type [INT])
  )
)

(type [2D-LatticePoint-yx] subtype [1D-LatticePoint-y]
  (its-attributes-are
    (x-coord :type [INT])
  )
)

An important property of IBCL types is that the "order" of the attributes doesn't matter. A consequence of this is that every example of

[2D-LatticePoint-xy]

is an example of

[2D-LatticePoint-yx]

and vice-versa. That is they refine each other. Again they are not "equal" because they are distict Types, but they are co-extensive with respect to examples. In this sense

(type [3D-LatticePoint] subtype [2D-LatticePoint-xy]
  (its-attributes-are
    (z-coord :type [INT])
  )
)

(type [3D-LatticePoint] subtype [2D-LatticePoint-yx]
  (its-attributes-are
    (z-coord :type [INT])
  )
)

has the same effect!!!!

7 Adding Restrictions

We now add a construct that combine adding an attribute and refining an attribute that was first introduced in a parent. We do this by introducing an "its-refinements-are" clause.

We extend the type construct to include

(type <type-name> subtype <parent-name>
  (its-attributes-are
    (attribute-name₁ :type <type_a,1>)
    ...
    (attribute-name_n :type <type_a,n>)
  )
  (its-a-refinements-are
    (parent-attribute-name₁ :type <type_r,1>)
    ...
    (parent-attribute-name_m :type <type_r,m>)
  )
)

In this case the types

<type_r,m>

must refine the type associated with the attribute

    parent-attribute-name_i

. in the parent type.

Consider

(type [3D-LatticePoint-xyz-yPlane4] subtype [2D-LatticePoint-xy]
  (its-attributes-are
    (z-coord :type [INT])
  )
  (its-refinements-are
    (y-coord :type {4})
  )
)

It both extends the set of attributes of

[2D-LatticePoint-xy]

and refines the Type of its y-coord

{4} refines [INT]

By introducing "its-refinements-are" we can do several things at once.

8 Adding Components

The final extension we add to the type construct in this document is "its-components-are". This construct is the IBML way of describing the parts of something. It is a critical to be able to distinguish parts from attributes as they behave differently from the point of view of refinement. The ability to give the notion of component (or part) a coherent semantics with respect to refinement is a critical feature which distinguishes IBCL for other modeling/ontological languages.

We extend the type construct to include

(type <type-name> subtype <parent-name>
  (its-attributes-are
    (attribute-name₁ :type <type_a,1>)
    ...
    (attribute-name_n :type <type_a,n>)
  )
  (its-a-refinements-are
    (parent-attribute-name₁ :type <type_ar,1>)
    ...
    (parent-attribute-name_m :type <type_ar,m>)
  )
  (its-components-are
    (component-name₁ :type <type_c,1> :range <range_c,1>))
    ...
    (component-name_p :type <type_c,p> :range <range_c,p>)
  )
)

(type [Animal] subtype [Living-Thing]
  (its-attributes-are
    (Genus-Species :type [STRING])
  )
  (its-components-are
    (legs :type [Leg] :range [0-INF])
  )
)

And in analogy to "its-a-refinements-are" we also add "its-c-refinements-are"

We extend the type construct to include

(type <type-name> subtype <parent-name>
  (its-attributes-are
    (attribute-name₁ :type <type_a,1>)
    ...
    (attribute-name_n :type <type_a,n>)
  )
  (its-a-refinements-are
    (parent-attribute-name₁ :type <type_ar,1>)
    ...
    (parent-attribute-name_m :type <type_ar,m>)
  )
  (its-components-are
    (component-name₁ :type <type_c,1> :range <range_c,1>))
    ...
    (component-name_p :type <type_c,p> :range <range_c,p>)
  )
  (its-c-refinements-are
    (parent-component-name₁ :type <type_cr,1> :range <range_cr,1>)
    ...
    (parent-component-name_m :type <type_cr,m>  :range <range_cr,p>))
  )
)

Where

<type_cr,i> 
<range_cr,i>

actually refine the corresponding labeled type of parent-component-name in the parent type. An example

(type [Biped] subtype [Animal]
  (its-c-refinements-are
    (legs :type [Leg] :range [2])
  )
)

(type [Human] subtype [Biped]
  (its-a-refinements-are
    (Genus-Species :type {"Homo Sapiens"}
  )
)

Summary

The purpose of this document is to give people the ability to start defining simple IBML Types. Although the IBML Types definable with these types are quite impressive, it is far from complete and says nothing about how IBML types may be used, how to use the IBUKI Mode Builder, IMB, or how to build an application that uses these models. These issues are treated elseware.

Acknowledgments

The information theoretic semantics for modeling complex objects and the idea of refinement as the basic operation on models was developed several years ago by IBUKI to solve problems involving configuring complex objects subject to constraints. There are many intellectual roots of this material but that range from Kleene's original definition of recursive functions to a type system developed by Luca Cardelli for a programming language called Amber. The particular semantics of defining components and its implementation in the IMB was developed by IBUKI in early 2000.

Getting Started with IBML Type Definitions

Original Version 2001-10-22First reformatted for the web 2005-02-14

Abstract

Table of contents

1 Basic Data

2 Basic Types

3 Basic Tree Types

4 Adding New Types

5 Naming Types

6 Adding Parents

7 Adding Restrictions

8 Adding Components

Summary

Acknowledgments

Original Version 2001-10-22
First reformatted for the web 2005-02-14