Refinement and Generalization

The notions of refinement and generalization in the IBUKI type theory are opposites. Refinement either adds a new attribute and describes its possible values or refinee one of its subparts. Generalization, on the other hand, either forgets some attribute or generalizes the value of some subpart.

A Simple Example

Consider a two dimensional grid point where the coordinates are integers 

 (|type| [2d-integer-grid-point] |subtype| [object]
  (|iaa|
   (|x-coord| (*type* [integer]))
   (|y-coord| (*type* [integer]))
   ) )

Refinement

We can refine this definition either by adding a dimention 

 (|type| [3d-integer-grid-point] |subtype| [2d-integer-grid-point]
  (|iaa|
   (|x-coord| (*type* [integer]))
   (|y-coord| (*type* [integer]))
   (|z-coord| (*type* [integer]))
   ) )

or refining one of its parts 

 (|type| [sparce-2d-integer-grid-point] |subtype| [2d-integer-grid-point]
 (|iaa|
   (|x-coord| (*type* [integer]))
   (|y-coord| (*type* [even-integer]))
   ) )

Generalization

We can generalize by forgeting a dimention 

 (|type| [1d-integer-grid-point] [subtype| [object]
  (|iaa|
   (|x-coord| (*type* [integer]))
   ) )

or by generalizing one of its parts 

 (|type| [2d-integer-x-rational-grid-point] [subtype| [object]
  (|iaa|
   (|x-coord| (*type* [integer]))
   (|y-coord| (*type* [rational]))
   ) ) 

Notes
------------------------------------------------------------------------------
Refinements result in 'subtypes', generalizations produce 'supertypes'

For this reason the definitions of both [1d-integer-grid-point] and 
[2d-integer-x-rational-grid-point] leave them as subtypes of [object]. 
On the other hand it is easy to show that [2d-integer-grid-point] is
a subtype of either. 

------------------------------------------------------------------------------