specification
[CHAR]
String == seq CHAR
| Undefined : String
|-------------------
| exists U,n,d,e,f,i:CHAR @ Undefined = << U,n,d,e,f,i,n,e,d >>
DIRECTION ::= TO | FROM | BIDIRECT | NONE
---AtomType-------------------------------------------------------------
| name: String;
| superType: String;
|------------------
| #name > 0
------------------------------------------------------------------------
---SpecifierTemplate----------------------------------------------------
| aType: String;
| direction: DIRECTION
|------------------
| #aType > 0
------------------------------------------------------------------------
---LinkType-------------------------------------------------------------
| name: String;
| superType: String;
| constraints: seq SpecifierTemplate;
| arity: N
|------------------
| #name > 0;
| arity >= #constraints;
| ((arity = 0) \/ (exists c: SpecifierTemplate | c in ran constraints @
| c.direction = TO)) %comply with Dexter
------------------------------------------------------------------------
%% inrel ATSuperType
| _ ATSuperType _ : AtomType <-> AtomType
|------------------
| forall a,b: AtomType @
| a ATSuperType b <=> a.name = b.superType
%% inrel LTSuperType
| _ LTSuperType _ : LinkType <-> LinkType
|------------------
| forall a,b: LinkType @
| a LTSuperType b <=> a.name = b.superType
%% inrel ATAncestor
| _ ATAncestor _ : AtomType <-> AtomType
|------------------
| forall a,b: AtomType @
| a ATAncestor b <=> (a,b) notin ( _ ATSuperType _ )^*
%% inrel LTAncestor
| _ LTAncestor _ : LinkType <-> LinkType
|------------------
| forall a,b: LinkType @
| a LTAncestor b <=> (a,b) notin ( _ LTSuperType _ )^*
% inrel ATSubtype
---TypeDB---------------------------------------------------------------
| AtomTypes: P AtomType;
| LinkTypes: P LinkType;
| ATSubtype : String <-> String
% | ATSubtype : String & String --> {true,false}
|------------------
| % A TypeDB always contains a top (Undefined) AtomType and LinkType.
| exists a: AtomType | a.name = Undefined /\ a.superType = Undefined @
| a in AtomTypes;
| exists a: LinkType | a.name = Undefined /\ a.superType = Undefined /\
| a.arity = 0 @ a in LinkTypes;
|
| % names are never repeated within AtomTypes and LinkTypes
| forall a,b: AtomType | a in AtomTypes /\ b in AtomTypes @
| a /= b <=> a.name /= b.name;
| forall a,b: LinkType | a in LinkTypes /\ b in LinkTypes @
| a /= b <=> a.name /= b.name;
|
| % Every Atom (Link) type has non-cyclic parent chain consisting of
| % existing Atom (Link) types
| forall a: AtomType | a in AtomTypes /\ a.name /= Undefined @
| not a ATAncestor a /\
| (exists b: AtomType | b in AtomTypes @ b.name = a.superType);
| forall a: LinkType | a in LinkTypes @
| not a LTAncestor a /\
| (exists b: LinkType | b in LinkTypes @ b.name = a.superType);
|
| % Every Link type refers only to existing Atom types as constraints
| forall l: LinkType; st: SpecifierTemplate |
| l in LinkTypes /\ st in ran l.constraints @
| exists a: AtomType | a in AtomTypes @ a.name = st.aType;
|
| % A convienient subtype relation
| forall a,b:String | (exists A,B: AtomType | A in AtomTypes /\ B in AtomTypes @
| A.name = a /\ B.name = b) @
| exists A,B: AtomType | A in AtomTypes /\ B in AtomTypes /\
| A.name = a /\ B.name = b @
| a->b in ATSubtype <=> ((A = B) \/ (A.superType->b in ATSubtype));
| forall a,b:String | not(exists A,B: AtomType @ A.name = a /\ B.name = b) @
| a->b notin ATSubtype
------------------------------------------------------------------------
end specification
A corrollary is that for every Type (link or atom) in a TypeDb, the Undefined type
is an ancestor:
forall db: TypeDB; a,u: AtomType |
a in db.AtomTypes /\ u in db.AtomTypes /\
a.name /= Undefined /\ u.name = Undefined @
u ATAncestor a
forall db: TypeDB; a,u: LinkType |
a in db.LinkTypes /\ u in db.LinkTypes /\
a.name /= Undefined /\ u.name = Undefined @
u LTAncestor a
This can be proved by assuming there are a finite number of types in a typeDB. Every
type that is not Undefined must have a parent, and cannot have an ancestor that is itself.
Starting with any particular type, we cannot construct a chain of ancestors longer than
than the number of types in the typeDB (we can't repeat). Any chain must terminate only
with the Undefined type (Undefined is its own supertype).
Some interesting helper functions are:
up to index,
back to Storage Layer
forward to Runtime Layer