login  home  contents  what's new  discussion  bug reports     help  links  subscribe  changes  refresh  edit

Edit detail for SandBox Aldor Category Theory revision 10 of 12

1 2 3 4 5 6 7 8 9 10 11 12
Editor: Bill Page
Time: 2007/11/21 07:00:48 GMT-8
Note: tests

changed:
-define Domains:Category == with;
define Domain:Category == with;

changed:
-define Set:Category == Join(Domains, Printable) with {
define Set:Category == Join(Domain, Printable) with {

added:
Test Funtions
\begin{aldor}
#include "axiom"
#pile
#library lbasics "basics.ao"
import from lbasics

T:Domain == add
S:Set == Integer add
P:Preorder == Integer add
TO:TotalOrder == Integer add
--CC:Countable == Integer add
--  import from Integer, Generator(Integer)
--  elements():Generator(Integer) == generator (1..10)
M:Monoids == Integer add
G:Groups == Fraction Integer add
MAPS:MapCategory(SetCategory,Integer,Float) == Map(SetCategory,Integer,Float) add
INTS:Categorify(Integer) == add
  value:Integer == 1
\end{aldor}


changed:
-)show Domains
-)show Set
)show T
)show S
)show P
)show TO
--)show CC
)show MAPS
)show INTS
null(PositiveInteger,Float)(1)
(sin ** cos)$o(SetCategory,EXPR INT,EXPR INT,EXPR INT)

Miscellaneous Logical helper functions

aldor
#include "axiom" #pile define Domain: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(Domain, 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/zope2/var/LatexWiki/basics.as using AXIOM-XL compiler and 
      options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file ./basics.lsp
   Issuing )library command for basics
   Reading /var/zope2/var/LatexWiki/basics.asy
   null is now explicitly exposed in frame initial 
   null will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Categorify is now explicitly exposed in frame initial 
   Categorify will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   MapCategory is now explicitly exposed in frame initial 
   MapCategory will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Groups is now explicitly exposed in frame initial 
   Groups will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Monoids is now explicitly exposed in frame initial 
   Monoids will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Printable is now explicitly exposed in frame initial 
   Printable will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   associativeProduct is now explicitly exposed in frame initial 
   associativeProduct will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   CountablyFinite is now explicitly exposed in frame initial 
   CountablyFinite will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Countable is now explicitly exposed in frame initial 
   Countable will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Domain is now explicitly exposed in frame initial 
   Domain will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   TotalOrder is now explicitly exposed in frame initial 
   TotalOrder will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Preorder is now explicitly exposed in frame initial 
   Preorder will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Set is now explicitly exposed in frame initial 
   Set will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   Map is now explicitly exposed in frame initial 
   Map will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics
   o is now explicitly exposed in frame initial 
   o will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/basics

Test Funtions

aldor
#include "axiom" #pile #library lbasics "basics.ao" import from lbasics T:Domain == add S:Set == Integer add P:Preorder == Integer add TO:TotalOrder == Integer add --CC:Countable == Integer add -- import from Integer, Generator(Integer) -- elements():Generator(Integer) == generator (1..10) M:Monoids == Integer add G:Groups == Fraction Integer add MAPS:MapCategory(SetCategory,Integer,Float) == Map(SetCategory,Integer,Float) add INTS:Categorify(Integer) == add value:Integer == 1
aldor
   Compiling FriCAS source code from file 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002.as using 
      AXIOM-XL compiler and options 
-O -Fasy -Fao -Flsp -laxiom -Mno-AXL_W_WillObsolete -DAxiom -Y $AXIOM/algebra
      Use the system command )set compiler args to change these 
      options.
#1 (Warning) Deprecated message prefix: use `ALDOR_' instead of `_AXL'
   Compiling Lisp source code from file 
      ./7978782401659043526-25px002.lsp
   Issuing )library command for 7978782401659043526-25px002
   Reading /var/zope2/var/LatexWiki/7978782401659043526-25px002.asy
   TO is now explicitly exposed in frame initial 
   TO will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   INTS is now explicitly exposed in frame initial 
   INTS will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   MAPS is now explicitly exposed in frame initial 
   MAPS will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   M is now explicitly exposed in frame initial 
   M will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   P is now explicitly exposed in frame initial 
   P will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   S is now explicitly exposed in frame initial 
   S will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   G is now explicitly exposed in frame initial 
   G will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002
   T is now explicitly exposed in frame initial 
   T will be automatically loaded when needed from 
      /var/zope2/var/LatexWiki/7978782401659043526-25px002

axiom
)show T T is a domain constructor Abbreviation for T is T This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for T ------------------------------- Operations -------------------------------- Warning: T is being redefined. T is a domain constructor. Abbreviation for T is T This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for T ------------------------------- Operations -------------------------------- )show S S is a domain constructor Abbreviation for S is S This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for S ------------------------------- Operations -------------------------------- ?=? : (%,%) -> Boolean coerce : % -> OutputForm coerce : List % -> OutputForm ?**? : (OutputForm,List %) -> OutputForm coerce : Generator % -> OutputForm )show P P is a domain constructor Abbreviation for P is P This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for P ------------------------------- Operations -------------------------------- ?<? : (%,%) -> Boolean ?<=? : (%,%) -> Boolean ?=? : (%,%) -> Boolean ?>? : (%,%) -> Boolean ?>=? : (%,%) -> Boolean coerce : % -> OutputForm coerce : List % -> OutputForm ?**? : (OutputForm,List %) -> OutputForm coerce : Generator % -> OutputForm )show TO TO is a domain constructor Abbreviation for TO is TO This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for TO ------------------------------- Operations -------------------------------- ?<? : (%,%) -> Boolean ?<=? : (%,%) -> Boolean ?=? : (%,%) -> Boolean ?>? : (%,%) -> Boolean ?>=? : (%,%) -> Boolean coerce : % -> OutputForm coerce : List % -> OutputForm max : (%,%) -> % max : Tuple % -> % min : (%,%) -> % min : Tuple % -> % ?**? : (OutputForm,List %) -> OutputForm coerce : Generator % -> OutputForm --)show CC )show MAPS MAPS is a domain constructor Abbreviation for MAPS is MAPS This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for MAPS ------------------------------- Operations -------------------------------- apply : (%,Integer) -> Float hom : (Integer -> Float) -> % )show INTS INTS is a domain constructor Abbreviation for INTS is INTS This constructor is exposed in this frame. Issue )edit 7978782401659043526-25px002.as to see algebra source code for INTS ------------------------------- Operations -------------------------------- value : () -> Integer null(PositiveInteger,Float)(1) There are 1 exposed and 1 unexposed library operations named elt having 1 argument(s) but none was determined to be applicable. Use HyperDoc Browse, or issue )display op elt to learn more about the available operations. Perhaps package-calling the operation or using coercions on the arguments will allow you to apply the operation. Cannot find application of object of type Domain to argument(s) of type(s) PositiveInteger (sin ** cos)$o(SetCategory,EXPR INT,EXPR INT,EXPR INT) Category, domain or package constructor Category is not available.

[SandBox Aldor Category Theory 2]?