namespace core { Ontology for the core entities and rules that govern them }


# The foundational type system
#
# This is effectively the meta-data system
#
type          { a data type }
relation      { a relation }
any           { any type at all - therefore every instances matches }
none          { no type at all - therefore no instances match }
sub_type_of   { the sub_type_of relation as in TypeA sub_type_of TypeB }
instance_of   { the instance_of relation as in ObjectA instance_of TypeB }
domain        { the type a relation is from e.g. any domain instance_of }
co_domain     { the type a relation is to  e.g. type domain instance_of }
has_domain    { constraint on doman of a relation sub-type
                e.g. predicate has_doman boolean }
has_co_domain { constraint on co_doman of a relation sub-type
                e.g. predicate has_co_doman boolean }

instance_of(type, type)
instance_of(relation, type)
instance_of(any, type)
instance_of(none, type)

domain(type, sub_type_of)
co_domain(type, sub_type_of)

instance_of(instance_of, relation)
domain(any, instance_of)
co_domain(type, instance_of)

instance_of(domain, relation)
domain(type, domain)
co_domain(relation, domain)

instance_of(co_domain, relation)
domain(type, co_domain)
co_domain(relation, co_domain)

instance_of(has_domain, relation)
co_domain(relation, has_domain)

instance_of(has_co_domain, relation)
co_domain(relation, has_co_domain)

has_domain(relation, any)
has_co_domain(relation, any)

boolean   { the boolean values }
true      { truth }
false     { falsity }
predicate { A relation where both arguments are from the booleans }

instance_of(boolean, type)
instance_of(true, boolean)
instance_of(false, boolean)

sub_type_of(predicate, relation)
has_domain(predicate, boolean)
has_co_domain(predicate, boolean)

# Logic operators
#
#
and       { and boolean predicate }
or        { or boolean predicate }
xor       { exclusive boolean or }
equal     { equality }
not_equal { non-equality }
implies   { the implication relation }

instance_of(and, predicate)
instance_of(or, predicate)
instance_of(xor, predicate)
instance_of(equal, relation)
instance_of(not_equal, relation)
instance_of(implies, predicate)

# truth tables & other basic stuff
#
#
equal(true, true)
equal(false, false)
equal(equal(false, true), false)
equal(equal(true, false), false)

equal(and(true,  true),  true)
equal(and(true,  false), false)
equal(and(false, true),  false)
equal(and(false, false), false)

equal(or(true,  true),  true)
equal(or(true,  false), true)
equal(or(false, true),  true)
equal(or(false, false), false)

equal(xor(true , true),  false)
equal(xor(true,  false), true)
equal(xor(false, true),  true)
equal(xor(false, false), false)

equal(implies(true,  true),  true)
equal(implies(true,  false), false)
equal(implies(false, true),  true)
equal(implies(false, false), true)

# This is where we define all the links between these axioms.
#
# We use expressions containing variables to specify how different types and
# relations match.
#



# define equality and the exclusivity of equal and not_equal
equal(_x, _x)
xor(equal(_x, _y),
    not_equal(_x, _y))

# members of any & none
everything_in_any as
instance_of { everything is an any }
          (_x, any)
equal { nothing is a none }
     (false,
      instance_of(_x, none))
sub_type_of { all types are an any }
   (_x, any)

# inheritance and instanceof
implies { instance of sub type is also instance of super type }
       (and(instance_of(_i, _subType), sub_type_of(_subType, _superType)),
        instance_of(_i, _superType))

# domain & co-domain constraints
domain_constraint as
implies { If _d is not a member of the domain then _r(_d, _c) is always false }
       (equal(false,
              and(domain(_D, _r), instance_of(_d, _D))),
        equal(false, _r(_d, _c)))

co_domain_constraint as
implies { If _c is not a member of the co-domain then _r(_d, _c) is always false }
       (equal(false,
              and(co_domain(_C, _r), instance_of(_c, _C))),
        equal(false, _r(_d, _c)))

has_domain_implies_domain as
implies
       (and(has_domain(_relation_type, _hd),
            instance_of(_r, _relation_type)),
        domain(_hd, _r))

has_co_domain_implies_co_domain as
implies
       (and(has_co_domain(_relation_type, _hc),
            instance_of(_r, _relation_type)),
        co_domain(_hc, _r))

# The main types of relation
#
#
transitive    { transitivity }
symmetric     { symmetrical }
antisymmetric { anti-symmetric }
reflexive     { reflexive }

sub_type_of(transitive, relation)
transitive_closure as
implies { if _r is transitive and _r(_x, _y) and _r(_y, _z) then _r(_x, _z) }
       (and(instance_of(_r, transitive),
            and(_r(_x, _y), _r(_y, _z))),
        _r(_x, _z))

sub_type_of(symmetric, relation)
symmetric_closure as
implies { if _r is symmetric and _r(_x, _y) then _r(_y, _x) }
       (and(instance_of(_r, symmetric),
            _r(_x, _y)),
        _r(_y, _x))

sub_type_of(antisymmetric, relation)
antisymmetric_closure as
implies { if _r is antisymmetric and _r(_x, _y) and _r(_y, _x)
          then _x and _y are equal }
       (and(instance_of(_r, antisymmetric),
            and(_r(_x, _y), _r(_y, _x))),
        equal(_x, _y))

sub_type_of(reflexive, relation)
reflexive_closure as
implies { if _r is reflexive then _r(_x, _x) holds }
       (instance_of(_r, reflexive),
        _r(_x, _x))

partial_order { Good for sorting things }
sub_type_of(partial_order, reflexive)
sub_type_of(partial_order, antisymmetric)
sub_type_of(partial_order, transitive)

equivalence { Good for binning things into sets }
sub_type_of(equivalence, reflexive)
sub_type_of(equivalence, symmetric)
sub_type_of(equivalence, transitive)

# and finaly, define a couple of our main relations
instance_of(sub_type_of, partial_order)
instance_of(equal, equivalence)