Theorems about Types
By Richard Weyhrauch

This note is called: [THE-CONTEXT--TYPE]
The notation used in this note is described in [NOTATION]
Under development

Preface

This is a theory about mental processes and mental images. Our thesis is that the only things in a head are mental images of things and we propose to represent mental images in our 'artifical' head as IBML types.

TYPE?
(FORALL obj TYPE?(obj))

(FORALL obj (XOR 
  (ATOMIC-DATA? obj)
  (SET-ODDATA? obj)
  (TREE-TYPE? obj)
))

(FORALL obj (IFF (DATA? obj) (XOR 
  (TAG? obj)
  (CHARACYER? obj)
   ...
  )) )
(FORALL tag (EQUAL (type-get-val tag |type|) '[tag])
(TYPE? [attribute-name])
(SUBTYPE [attribute-name] [symbol])

(ATTRIBUTE-NAME? |type|)

SUBTYPE
EXAMPLE
ISIN

[top]  our mental image of the collection of everything
(TYPE? [top])
(ISIN [top] [top])
(IFF (PROPER-TYPE x) (NOT x [top])

(FORALL (a [attribute-name]) (type-has-attribute-name [top] a))
(FORALL (a [attribute-name]) (EQUAL (type-get-val [top] a) [top])
(EQUAL (type-get-val [top] |type|) |top|)


attributes-of(type)=(list-of [attribute-name])
  This list has no duplicates
(TYPE-HAS-ATTRIBUTE [type] [attribute-name])

;; type seperation
(FORALL x (EXIST T) (forall y ((IFF (ISIN y T) (AND (ISIN y x) (P x))
  where y is not free in P
  The bound variables of P range over proper types


Theorems about [top]

(FORALL x (TYPE? x)
(FORALL x (SUBTYPE x [type])
(SUBTYPE [top] [top])


if t1 is a proper subset of t then
       t2=t/t1 is a type!!!

ie relative complement is OK!!!!!
  because t2 cant be empty. ie t1 is a proper subtype t <==? 
  (exists example of t) that is not in t1


An example of a type is any [object] that has all the attributes of the type an of its parent that is required.

All types, except [top], have at least one attribute and one example. (In fact all types have arbitrari;y many examples)

 (|type| [foo] |subtype| [top]
   (|name| (*type* @ [string] %required)
 )

(attributes-of [foo]) = {|name|)
(parent-of [foo] = [top]
  ; we have multiple inheritance so parent-of
  ; is actually a function of this specific [type-def]
  ; in Carroll this is called its genus
  ;   in his definition Carroll refers to a specific 'mental act'
  ;   this leaves the possibility for multiple inheritence mute 
  ;   his mental act is equivalent to using a specific [type-def]
  ;     to determine the type.
  ; of the [type-def] above of [foo]
  ;  [foo] is the species
  ;  [top] is the genus
  ;  (|name| (*type* @ [string]) is an attribute
  ;  ((|name| (*type* @ [string])) is its differentia
  ; for us
  ;  [foo] is a [type-name]
  ;  [top] is the [type-name] of [foo]'s parent
  ;  |name] is an [attribute-name]
  ;  [string] is the value of the attribute |name|
  ;    thought of as a type not as data
  ;  (attributes-of [foo]) = (|name|)
  ;    slightly misnamed

; (*EXA* (|foo| . (*finite* |aset|
;   (|name| (*data* @ "Fred"))
; )
  is the [type-def] of an example of a [foo]
  ; whose |name| is "Fred"
  ; whose type is called |foo|
  ; the thing named above as "fred" is a species of [foo]