.Open Object Theory

. Idea
The idea of an abstract data type(ADT) is fundamental to computer science.
The idea of Type is equally fundamental to modern mathematics.
A Type is a collection of objects with predefined operations, functions,
and properties.
An 
important difference between mathematical types and ADTs
is that a computer can only work with elements of a 
type that can be computed!  So an ADT consists only of those elemements in
a type that can be generated by a finite process. Recently the word 
'Object' seems to be applied to describe elements in ADTs, hence its use in
the section. The objects are not particularly 'Object Oriented'.  
Polymorphism, inheritance and so on are part of the theory of types.  Here
we abstract the idea of working with the constructable objects of a type.

Key property distinguishing a data type from a logical `Type`, is that the
ADT can only have objects `generated` by applying operations to a set of 
basic elements.  If the computer can not compute some data then it does not
have to work with that data.  Hence the theory of `Generational Systems`.

This theory can be used to define the meaning of a XBNF (BNF extended
into other areas) dictionary which avoids certain paradoxes
.See http:/www/dick/papers/rjb96x.xbnf.html

Here are some examples of the Generational Systems
.See GENESYS
.Open Examples
.As_is Strings	- generated by concatenating characters
.As_is or	 	- generated by prefixing characters
.As_is Files	 	- generated by inserting records at their end
.As_is Trees	 	- generated from set of atoms by grafting
.As_is Lists	 	- generated from NUL and atoms by a binary constructor.
.As_is Natural Numbers
.As_is	 	- generated from 1 by adding 1.
.As_is Data Bases
.As_is		- Entities and sets generated by 'PUT' and 'TAKE' operations

. Natural Numbers
.Source Peano
PEANO::=Net{$GENESYS(Nat) and generate=map[X]{x+1||x:X} and basis={1} and free}

. Trees
Trees::=Net{
	leaves::Sets,
	graft::trees><trees->trees,
	|-(T1): generate=map [X:@trees]{graft(x,y)||x,y:X},
	|-(T2): basis=leaves,
	|-(T3): free=true,
	|-(T4): $GENESYS(trees), 
 ...
}=::Trees.

. LISP
LISP::=Net{
	|-(L0): $GENESYS(lists),
	|-(L1): generate=map X({cons(x,y)||x,y:X}),
	|-(L2): free,
	basis::={NUL}|atoms
	atoms::Sets,
	NUL::lists~atoms,
	T::atoms,
	cons::lists><lists->lists,
	car,cdr::generated->lists,
	atom::lists->{T,NUL}=map x (if (x in atoms then T else NUL)),
	null::lists->{T,NUL}=map x (if (x=NUL then T else NUL)),
	|-(L3): for all x,y:lists (car(cons(x,y))=x and cdr(cons(x,y))=y),
	|-(L4): for all x:generated (x=cons(car(x),cdr(x))),
 ...
}=::LISP.

. Strings
STRINGS are defined elsewhere
.See http://www/dick/maths/math_61_String_Theories.html.

.Close Examples

.Open Abstract Generational System
GENESYS::=Net{
	Objects::Sets,
	generate::@Objects->@Objects =`an operation that combines Objects to create new ones`.

Nothing comes from nothing:
	|-(strict): generate({})={}.

More comes from more:
	|-(monotone): for all X1,X2:@Objects, if X1==>X2 then generate(X1)==>generate(X2).

Immortality of Objects:
	|-(immortallity): for all X:@Objects, (X==>generate(X)).
.Open Examples 2
. Example A
Natural numbers (1,2,3,...) with i:=i+1 as generator:
	the $GENESYS(Objects=>Nat, generate=>map N({n+1||n:N}))
. Example B
"clock arithmetic" (0,1,2,3,...,n-1,0,1,2,...)
       (Objects=>Nat mod n, generate=>Map N({(n+1)mod n || n:N})).

. Other examples
Relations, unary algebra, digraph, or dynamical system have maps in 
Objects->Objects that extend naturally to 'generative systems' with maps 
@Objects->@objects. In other systems new elements come from combining 
elements together but where a single object generates nothing new by 
itself.
.Close examples 2

Each generative system has an associated monoid of mappings:
	(generate is a mapping)|-(monoid): ({generate^n || n:Nat0}, o, Id(@Objects)}) in Monoid.

. Novelty
In each generation novel objects can appear:
	novel::@Objects->@Objects=map X(generate(X)~X),
	()|-(G1): for all X(generate(X)=X|novel(X) ).

A set of Objects that generates nothing new is called an `invariant` set
of objects:
	invariant::={}./novel,
	()|-(G2): invariant={X||generate(X)==>X},
	()|-(G3): Objects in invariant,
	()|-(G4): {} in invariant.

	()|-(G5): for I:invariant, X:@I(generate(X)==>I)

A fixed set is one that does not grow:
	fixed::@Objects= {X|| generate(X) = X}.

	()|-(fixed_invariant): fixed==>invariant.

The descendents of a set of objects is the smallest collection of objects that includes the set and is also invariant.
	For X1:@Objects, descendents(X1) ::= {x2:Objects || for all I:invariant, if X1 ==> I then x2 in I}.

	()|-(G6): for X,x, if not x in descendents(X) then some I:invariant(X ==> I and not x in I).
()|-(G7): for all X, X ==> descendents(X).
. Proof of G7
 For all X, X ==> descendents(X)
Let{ 
     |-(G7.1): not X ==> descendents X.
   ()|-(G7.2): some x in X and not x in descendents X.
   (G7.2)|-(G7.3): x in X.
   (G7.1)|-(G7.4): x not in descendents X.
   (G7.4)|-(G7.5): some I:invariant (X ==> I and x not in I).
   (G7.5)|-(G7.6): I in invariant.
   (G7.5)|-(G7.7): X are I,
   (G7.5)|-(G7.8): x not in I.
   (G7.3,G7.7)|-(G7.9): x in X ==> I.
}

()|-(G8): for X:Objects, Y:descendents(X), Z:generate(Y), ( Z are descendents(X)).
. Proof of G8
 For X:Objects, Y:descendents(X), Z:generate(Y), ( Z are descendents(X))
Let{
    |-(G8.1): X:@Objects,
    |-(G8.2): Y:descendents(X),
    |-(G8.3): Z:generate(Y),
    |-(G8.4): not ( Z are descendents(X)),
     (G8.4)|-(G8.5): some z in Z~descendents(X)
     (G8.5)|-(G8.6): z in Z      
     (G8.5)|-(G8.7): some I:invariant(X==>I and z not in I)  
     (G8.7)|-(G8.8): I:invariant  
     (G8.7)|-(G8.9): X are I     
     (G8.7)|-(G8.10): z not in I 
 (G8.8, G8.9, G8.2)|-(G8.11): Y are I 
(G8.11, G8.8, G8.3)|-(G8.12): Z are I      
     (G8.6)|-(G8.13): z in I       
}.


()|-(G6): for n:Nat0, generate^n ==> descendents.

. Basies
A basis is a set objects that can, ultimately, generate any object.
basies::@@Objects={X:@Objects||(descendents(X)=Objects)},
basies::=`those sets of of objects that will generate all other objects`.

In most Generational Systems a particular basis is given:
basis::basies -- A particular starting set for generating all objects.

generated::=Objects~basis.

Example A. Nat has only one basis = {1} because all i>1 are generatable from 1, and there are no numbers less than 1 to generate 1. 

Example B. Every nonempty subset of Nat/n is a basis.

. Generations
We assume we can attach a label to each object - its generation:
0th_generation::=basis.
1st_generation::=generate(basis)~basis.
2nd_generation::=generate(1st_generation)~1st_generation.
3rd_generation::=generate(2nd_generation)~2nd_generation.

generation::Objects->Nat0,
|-(G7a): generation(basis)=0,
|-(G7b): for x:generated, generation(x)=min{n||x in generate^n(basis)~generate^(n-1)(basis)}.
 For all n:Nat0, (n)th_generation::Nat0->@Objects =n./generation

|-(G8): for all n:Nat, n.th_generation= novel((n-1).th_generation).

generations::={n.th_generation || n:Nat0}.

The following define various kinds of Generational Systems.  Each
property can be true or false.
loop_free::@=for all G1,G2:generations( if G1 & G2 then G1=G2).

In a 'loop_free' system operations can not regenerate earlier generations.

Example
	Nat is loop free but Nat/n is not.

By choosing one object in each generation in a loop free system, we get a one-one imbedding of the natural numbers into a subset of the objects(Nat0-->Objects), therefore
()|-(G9): if loop_free then Objects not in Finite_sets.

Often the objects in the system have some notion of `size` and the property
that bigger objects are constructed from smaller ones.
growing::@,
if growing then for some size:Objects->Nat0, for all X:Objects,N:novel(X), x:X, n:N, (size(n)>size(x))
?? if growing then loop ?

Several common classes of generational systems occurs when there the size of
the set of novel objects is limitted in some way.  For example
the set of strings is generated from a finite alphabet by prefixing
members of the alphabet onto existing strings.
bounded_step::@= for some N:Nat0, all X:@Objects( |novel(X)| <= N ).
finite_step::@= for all X:@Objects, some N:Nat0( |novel(X)| = N ).
countable_step::@= for all X:@Objects( novel(X) --> Nat0).
()|-(G9a): if bounded_step then finite_step and countable_step.
()|-(G9b): if finite_step then countable_step.

Similarly for the basis:
bounded_basis::@= for some N:Nat0( |basis| <= N ).
finite_basis::@= for some N:Nat0( |basis| = N ).
countable_basis::@= basis --> Nat0.

()|-(G9c): bounded_basis iff finite_basis.
()|-(G9d): if bounded_basis or finite_basis then countable_basis.

()|-(countability theorem): if finite_basis and finite_step then Objects-->Nat0.
. Proof of countability theorem
This is just a sketch.
Let{
	|-(CT1): finite_basis.
	|-(CT2): finite_step.
 Since in each generation the novel objects form a finite set we can number them. 
 So each object has a generation and a number within that generation.
 So we have a pair of number identifying each object that is generated.
 There are several ways of mapping a pair of number one-to-one into the numbers.
}

The coutabillity of finitely based generational systems means that no
paradox arrises from assuming that an equation like X=generate(X).


. Freedom
Often an object can only be generated in a unique way:
convergence_free::=for all X1,X2 if no X1&descendents(X2) and no (X2&descendents(X1)) then no ( descendents(X1)&descendents(X2))

In a convergence free system there is no more than one way to generate an element.
.Dangerous_bend
Not `convergence to a limit`, but the meeting of two parallel families of generated objects.


In the most unrestricted generational systems - the `free` systems - there is
no convergence or loops.  This is `freedom` in the (oldfashioned) categorical sense.  It can be shown that unfree systems are the image of a free system.
free::=convergence_free & loop_free.

?? if free then unique ancestry for every element ?

?? if free then isomorphic to some set of tree structures ?

. Beyond Finiteness
The following is a generalization of the work done on defining what it means for a process to converge - as used in languages, trees, etc.

The kind of iterative process modeled here, can often appear to be getting close to a kind of fixed point which - if it only existed, would be an "infinite" object.  In some data structures for example a repeated process of adding a new element generates objects that start to behave very like a circular chain of objects... so in a sense one can claim that in LISP an equation like
	x=cons[A;x]
has as its "smallest solution" a dotted pair whose cdr points to itself and with car equal to A. See the LISP 1.5 manual for a discussion of how such 'list structures' are actually constructed.  Compare Manes & Arbib'd theory of the solution of X=A+B!X in a suitable initial algebra.

Trying to reason with the infinite is fallacy prone. Luckily the topologists have developed a package of consistent ideas that we can use to define ideas like:
.Box
 converges to
 gets close to
 looks like its going to
.Close.Box
for proving or disproving the existence and uniqueness of limits of series and the like.

??...
?? @generations(Objects) in filterbases(Objects)?

. Topology of Sets of Objects
One problem is defining a set of abstract objects recursively and not being sure whether the equations define a unique fixed point or not. The solution to this problem is a generalisation of the method used  for languages and demotational semantics - define a metric space that measures how well two sets match - in particular. The trick is choose a metric so that the later a set is generated then the `closer` it is to an ideal (and unreachable) set of objects.

In the case of sets of abstract objects we can construct a metric which measures how far apart two sets are - in the sense that a difference that is "younger" is a bigger difference than one that is older.


weight::=map [x](2^-(generation(x))

Thus the later an object is generated, the "lighter" it becomes.

differs::@Objects><@Objects=[X,Y](X~Y|Y~X)
d::(@Objects><@Objects)->Real= if X=Y then 0 else max (weight (differs(X,Y))).

The set of Objects now has the structure of metric space with $d
acting as the measure of the distances between sets of objects.
	()|- MetricSpace(@Objects,d).

 complete::@.
	|-(G10): If complete then MetricSpace(@Objects,d, complete).

By assuming `completeness` we assert the existence of objects 
that can not be generated, but which can be approximated to by
a $convergent sequence of generated objects.

convergent::@Seq(@Objects)={S || for some L, all \epsilon:(0..), abf i ( d(S[i],L) <= \epsilon )  }

Note. `abf` stands for `All but a finite number`.

convergent::@Objects->@Objects={G || (G^(_))in convergent}.

?? if @Objects in  compact then ...?
.Hole

?? if cauchy_complete then...unique fixed points for contracting definitions ?
.Hole

?? product spaces and so mutual recursion...?
.Hole

?? if loop then discrete ?
.Hole



}=::GENESYS.

.Close Abstract Generational System
. Exercises
Work out the following generational systems:

$GENESYS(Sets)
.Hole

$GENESYS(Bags)
.Hole

$GENESYS(Files)
.Hole

$GENESYS(Queues)
.Hole

$GENESYS(Stacks)
.Hole

. Term Paper
JWW Conway has developed a generation theory of great power and generallity. D. Knuth has written a short romantic novel featuring this system.  Find a copy of the the novel, read it, and express JWW's system using '$GENESYS'.

. Project
$GENESYS(DataBase)
.Hole
Use CODASYL,  Relational model, or Object-oriented models.

. Project - Probabalistic Generational Systems
Develop a variation of the $GENESYS model that handle probabilistic
generational systems rather than non-deterministic ones.
In this each novel element has a number between 0 and 1 inclusive
indicating the probability of its occurence.
.Hole
. Project - Fuzzy Generational Systems
Develop a variation of the $GENESYS model that handle Fuzzy
generational systems rather than non-deterministic ones.
In this each novel element has a number between 0 and 1 inclusive
indicating the the degree of its membership in the novel sets.
.Hole
. Project - Generational Subsystems
Construct an abstract model of a relationship between
generational systems such that one generates a subset of the
objects in the other one.  The result should be able
to show that a grammar is a generational subsystem
of the set strings defined above.
.Hole

.Close Object Theory