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

# Edit detail for SandBox Aldor Category Theory Basics revision 1 of 3

 1 2 3 Editor: Bill Page Time: 2007/11/21 12:31:57 GMT-8 Note: tests

changed:
-
Miscellaneous Logical helper functions

\begin{aldor}[basics]
#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 \end{aldor} 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 Null(n:PositiveInteger):Float==null(PositiveInteger,Float)(n) sincos(x:Expression Integer):Expression Integer == import from o(SetCategory,Expression Integer,Expression Integer,Expression Integer) ( ((a:Expression Integer):Expression Integer +-> sin(a)) ** ((b:Expression Integer):Expression Integer +-> cos(b)) ) (x) \end{aldor} \begin{axiom} )show T )show S )show P )show TO --)show CC )show MAPS )show INTS \end{axiom} \begin{axiom} sincos(x::Expression Integer) \end{axiom} \begin{axiom} Null(1) \end{axiom} From BillPage Tue Nov 20 19:19:32 -0800 2007 From: Bill Page Date: Tue, 20 Nov 2007 19:19:32 -0800 Subject: next Message-ID: <20071120191932-0800@axiom-wiki.newsynthesis.org> [SandBox Aldor Category Theory 2]  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
+++
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)
(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 Null(n:PositiveInteger):Float==null(PositiveInteger,Float)(n) sincos(x:Expression Integer):Expression Integer == import from o(SetCategory,Expression Integer,Expression Integer,Expression Integer) ( ((a:Expression Integer):Expression Integer +-> sin(a)) ** ((b:Expression Integer):Expression Integer +-> cos(b)) ) (x) aldor  Compiling FriCAS source code from file /var/zope2/var/LatexWiki/7819217643380372071-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'
"/var/zope2/var/LatexWiki/7819217643380372071-25px002.as", line 22:
((b:Expression Integer):Expression Integer +-> cos(b)) ) (x)
.............................................................^
[L22 C62] #2 (Warning) Suspicious juxtaposition.  Check for missing ;'.
Check indentation if you are using #pile'.
Compiling Lisp source code from file
./7819217643380372071-25px002.lsp
Issuing )library command for 7819217643380372071-25px002
TO is now explicitly exposed in frame initial
TO will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
INTS is now explicitly exposed in frame initial
INTS will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
MAPS is now explicitly exposed in frame initial
MAPS will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
M is now explicitly exposed in frame initial
M will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
P is now explicitly exposed in frame initial
P will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
S is now explicitly exposed in frame initial
S will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
G is now explicitly exposed in frame initial
G will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002
T is now explicitly exposed in frame initial
T will be automatically loaded when needed from
/var/zope2/var/LatexWiki/7819217643380372071-25px002

axiom)show T
T  is a domain constructor
Abbreviation for T is T
This constructor is exposed in this frame.
Issue )edit 7819217643380372071-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 7819217643380372071-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 7819217643380372071-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 7819217643380372071-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 7819217643380372071-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 7819217643380372071-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 7819217643380372071-25px002.as to see algebra source code for INTS
------------------------------- Operations --------------------------------
value : () -> Integer

axiomsincos(x::Expression Integer)
>> System error:
|newGoGet| [or a callee] requires less than one argument.

axiomNull(1)
>> System error:
Attempt to evaluate the null function.

[SandBox Aldor Category Theory 2]?