Edit detail for SandBox Aldor Category Theory revision 7 of 12

Miscellaneous Logical helper functions

(1) -> <aldor>
#include "axiom"
#pile

define Domains:Category == with;

+++
+++  A set is often considered to be a collection with "no duplicate elements."
+++  Here we have a slightly different definition which is important to 
+++  understand.  We define a Set to be an arbitrary collection together with
+++  an equivalence relation "=".  Soon this will be made into a mathematical
+++  category where the morphisms are "functions", by which we mean maps 
+++  having the special property that a=a' implies f a = f a'.  This definition
+++  is more convenient both mathematically and computationally, but you need
+++  to keep in mind that a set may have duplicate elements.
+++
define Set:Category == Join(Domains, Printable) with {
    =:(%,%) -> Boolean;
}
+++
+++  A Preorder is a collection with reflexive and transitive <=, but without
+++  necessarily being symmetric (x<=y and y<=x) implying x=y.  Since 
+++  (x<=y and y<=x) is always an equivalence relation, our definition of 
+++  "Set" is always satisfied in any case. 
+++
define Preorder:Category == Set with {
    <=: (%,%) -> Boolean;
    >=: (%,%) -> Boolean;
    < : (%,%) -> Boolean;
    > : (%,%) -> Boolean;
    default {
        (x:%) =(y:%):Boolean == (x<=y) and (y<=x);
        (x:%)>=(y:%):Boolean ==  y<=x;
        (x:%)< (y:%):Boolean == (x<=y) and ~(x=y);
        (x:%)> (y:%):Boolean == (x>=y) and ~(x=y)
    }
}

define TotalOrder:Category == Preorder with {
    min: (%,%) -> %;
    max: (%,%) -> %;
    min: Tuple % -> %;
    max: Tuple % -> %;
    default {
        min(x:%,y:%):% == { x<=y => x; y };
        max(x:%,y:%):% == { x<=y => y; x };
        import from List %;
        min(t:Tuple %):% == associativeProduct(%,min,[t]);
        max(t:Tuple %):% == associativeProduct(%,max,[t]);
    }
}  
+++
+++  Countable is the category of collections for which every element in the
+++  collection can be produced.  This is done by the generator "elements" 
+++  below.  Note that there is no guarantee that elements will not produce
+++  "duplicates."  In fact, a Countable may not be a Set, so duplicates may
+++  have no meaning.  Also, Countable is not guaranteed to terminate.
+++
define Countable:Category == with {
    elements: () -> Generator %
}
--
--  I'm using an empty function elements() rather than a constant elements
--  to avoid some compiler problems.
--
+++
+++  CountablyFinite is the same as Countable except that termination is 
+++  guaranteed.
+++
define CountablyFinite:Category == Countable with

+++
+++  A "Monoids" is the usual Monoid (we don't use Monoid to avoid clashing
+++  with axllib): a Set with an associative product (associative relative to
+++  the equivalence relation of the Set, of course) and a unit.
+++
define Monoids:Category == Set with {
    *: (%,%)            -> %;
    1:                     %;
    ^:(%,Integer) -> %;
    monoidProduct:   Tuple %  -> %;  -- associative product
    monoidProduct:   List  %  -> %;
    default {
        (x:%)^(i:Integer):% == {
            i=0 => 1;
            i<0 => error "Monoid negative powers are not defined.";
            associativeProduct(%,*,x for j:Integer in 1..i)
        };
        monoidProduct(t:Tuple %):% == { import from List %; monoidProduct(t) }
        monoidProduct(l:List %):% == {
            import from NonNegativeInteger;
            #l = 0 => 1;
            associativeProduct(%,*,l);
        }
   }
}  

+++
+++  Groups are Groups in the usual mathematical sense.  We use "Groups"
+++  rather than "Group" to avoid clashing with axllib.  
+++
define Groups:Category == Monoids with  {
    inv: % -> %
}    

+++
+++  Printing is a whole area that I'm going to have a nice categorical 
+++  solution for, but still it is convenient to have a low level Printable
+++  signature for debugging purposes.
+++
define Printable:Category == with {
    coerce: %    -> OutputForm;
    coerce: List % -> OutputForm;
    coerce: Generator % -> OutputForm;
    default {
        (t:OutputForm)**(l:List %):OutputForm == {
            import from Integer;
            empty? l => t;
            hconcat(coerce first l, hspace(1)$OutputForm) ** rest l;
        };
        coerce(l:List %):OutputForm == empty() ** l;
        coerce(g:Generator %):OutputForm == {
            import from List %;
            empty() ** [x for x in g];
        }
    }
}            

+++
+++  This evaluates associative products.
+++
associativeProduct(T:Type,p:(T,T)->T,g:Generator T):T == {
    l:List T == [t for t in g];
    associativeProduct(T,p,l);
}
associativeProduct(T:Type,p:(T,T)->T,l:List T):T == {
    if empty? l then error "Empty product.";
    mb(t:T,l:List T):T == { empty? l => t; mb( p(t,first l), rest l) };
    mb(first l,rest l)
}
+++
+++  Evaluates the logical "For all ..." construction
+++    
forall?(g:Generator Boolean):Boolean == {
    q:Boolean := true;
    for x:Boolean in g repeat { if ~x then { q := false; break } }
    q
}

+++
+++  Evaluates the logical "There exists ..." construction
+++    
exists?(g:Generator Boolean):Boolean == {
    q:Boolean := false;
    for x:Boolean in g repeat { if x then { q := true; break } };
    q
}

+++
+++  The category of "Maps".  There is no implication that a map is a 
+++  function in the sense of x=x' => f x = f x'
+++
define MapCategory(Obj:Category,A:Obj,B:Obj):Category == with {
    apply: (%,A) -> B;
    hom:  (A->B) -> %;
}
+++
+++  One convenient implementation of MapCategory 
+++
Map(Obj:Category,A:Obj,B:Obj):MapCategory(Obj,A,B) == add {
    Rep ==> A->B;
    apply(f:%,a:A):B == (rep f) a;
    hom  (f:A->B):% == per f
}
+++
+++  This strange function turns any Type into an Aldor Category
+++
define Categorify(T:Type):Category == with {
    value: T
}
+++
+++  The null function
+++
null(A:Type,B:Type):(A->B) == (a:A):B +-> error "Attempt to evaluate the null function."

+++
+++ A handy package for composition of morphisms.  "o" is meant to suggest morphism composition g "o" f, to be coded "g ** f".
+++
o(Obj:Category,A:Obj,B:Obj,C:Obj): with
    **: (B->C,A->B) -> (A->C)
== add
    (g:B->C)**(f:A->B):(A->C) == (a:A):C +-> g f a</aldor>

Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/Basics.as 
      using Aldor compiler and options 
-O -Fasy -Fao -Flsp -lfricas -Mno-ALDOR_W_WillObsolete -DFriCAS -Y $FRICAS/algebra -I $FRICAS/algebra
      . Use the system command )set compiler args to change these 
      options.
#1 (Warning) Could not use archive file `libfricas.al'.
"/var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/Basics.as", line 1: 
#include "axiom"
^
[L1 C1] #2 (Error) Could not open file `axiom'.

   The )library system command was not called after compilation.

)show Domains

   The )show system command is used to display information about types 
      or partial types. For example, )show Integer will show 
      information about Integer .

      Domains is not the name of a known type constructor. If you want 
      to see information about any operations named Domains , issue
                         )display operations Domains 

)show Set

 Set(S: SetCategory) is a domain constructor
 Abbreviation for Set is SET 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------

 ?<? : (%, %) -> Boolean               ?<=? : (%, %) -> Boolean
 ?=? : (%, %) -> Boolean               ?>? : (%, %) -> Boolean
 ?>=? : (%, %) -> Boolean              coerce : % -> OutputForm
 construct : List(S) -> %              copy : % -> %
 dictionary : List(S) -> %             dictionary : () -> %
 difference : (%, %) -> %              difference : (%, S) -> %
 empty : () -> %                       empty? : % -> Boolean
 eq? : (%, %) -> Boolean               extract! : % -> S
 insert! : (S, %) -> %                 inspect : % -> S
 intersect : (%, %) -> %               latex : % -> String
 map : ((S -> S), %) -> %              sample : () -> %
 set : () -> %                         set : List(S) -> %
 subset? : (%, %) -> Boolean           union : (%, %) -> %
 union : (%, S) -> %                   union : (S, %) -> %
 ?~=? : (%, %) -> Boolean             
 #? : % -> NonNegativeInteger if % has ATFINAG
 any? : ((S -> Boolean), %) -> Boolean if % has ATFINAG
 cardinality : % -> NonNegativeInteger
 complement : % -> % if S has FINITE
 convert : % -> InputForm if S has KONVERT(INFORM)
 count : (S, %) -> NonNegativeInteger if % has ATFINAG and S has BASTYPE
 count : ((S -> Boolean), %) -> NonNegativeInteger if % has ATFINAG
 enumerate : () -> List(%) if S has FINITE
 eval : (%, List(S), List(S)) -> % if S has EVALAB(S) and S has SETCAT
 eval : (%, S, S) -> % if S has EVALAB(S) and S has SETCAT
 eval : (%, Equation(S)) -> % if S has EVALAB(S) and S has SETCAT
 eval : (%, List(Equation(S))) -> % if S has EVALAB(S) and S has SETCAT
 every? : ((S -> Boolean), %) -> Boolean if % has ATFINAG
 find : ((S -> Boolean), %) -> Union(S,"failed")
 hash : % -> SingleInteger if S has FINITE
 hashUpdate! : (HashState, %) -> HashState if S has FINITE
 index : PositiveInteger -> % if S has FINITE
 less? : (%, NonNegativeInteger) -> Boolean
 lookup : % -> PositiveInteger if S has FINITE
 map! : ((S -> S), %) -> % if % has ATSHMUT
 max : % -> S if % has ATFINAG and S has ORDSET
 max : (((S, S) -> Boolean), %) -> S if % has ATFINAG
 member? : (S, %) -> Boolean if % has ATFINAG and S has BASTYPE
 members : % -> List(S) if % has ATFINAG
 min : % -> S if % has ATFINAG and S has ORDSET
 more? : (%, NonNegativeInteger) -> Boolean
 parts : % -> List(S) if % has ATFINAG
 random : () -> % if S has FINITE
 reduce : (((S, S) -> S), %, S, S) -> S if % has ATFINAG and S has BASTYPE
 reduce : (((S, S) -> S), %, S) -> S if % has ATFINAG
 reduce : (((S, S) -> S), %) -> S if % has ATFINAG
 remove : (S, %) -> % if % has ATFINAG and S has BASTYPE
 remove : ((S -> Boolean), %) -> % if % has ATFINAG
 remove! : ((S -> Boolean), %) -> % if % has ATFINAG
 remove! : (S, %) -> % if % has ATFINAG and S has BASTYPE
 removeDuplicates : % -> % if % has ATFINAG and S has BASTYPE
 select : ((S -> Boolean), %) -> % if % has ATFINAG
 select! : ((S -> Boolean), %) -> % if % has ATFINAG
 size : () -> NonNegativeInteger if S has FINITE
 size? : (%, NonNegativeInteger) -> Boolean
 smaller? : (%, %) -> Boolean if S has COMPAR
 symmetricDifference : (%, %) -> %
 universe : () -> % if S has FINITE