login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit
 Topics FrontPage Aldor FriCAS language SandBox SandBox Aldor Category Theory SandBox Aldor Category Theory Basics <-- You are here. 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-ALDOR_W_WillObsolete -DAxiom -Y$AXIOM/algebra -I $AXIOM/algebra Use the system command )set compiler args to change these options. Compiling Lisp source code from file ./basics.lsp Issuing )library command for basics Reading /var/zope2/var/LatexWiki/basics.asy Domain is now explicitly exposed in frame initial Domain 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 Printable is now explicitly exposed in frame initial Printable 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 TotalOrder is now explicitly exposed in frame initial TotalOrder 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 Countable is now explicitly exposed in frame initial Countable 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 Monoids is now explicitly exposed in frame initial Monoids 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 MapCategory is now explicitly exposed in frame initial MapCategory 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 Categorify is now explicitly exposed in frame initial Categorify will be automatically loaded when needed from /var/zope2/var/LatexWiki/basics null is now explicitly exposed in frame initial null 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 >> System error: The bounding indices 163 and 162 are bad for a sequence of length 162. See also: The ANSI Standard, Glossary entry for "bounding index designator" The ANSI Standard, writeup for Issue SUBSEQ-OUT-OF-BOUNDS:IS-AN-ERROR 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-ALDOR_W_WillObsolete -DAxiom -Y$AXIOM/algebra -I $AXIOM/algebra Use the system command )set compiler args to change these options. "/var/zope2/var/LatexWiki/7819217643380372071-25px002.as", line 22: ((b:Expression Integer):Expression Integer +-> cos(b)) ) (x) .............................................................^ [L22 C62] #1 (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 Reading /var/zope2/var/LatexWiki/7819217643380372071-25px002.asy T is now explicitly exposed in frame initial >> System error: Lock on package COMMON-LISP violated when setting the symbol-function of T while in package BOOT. See also: The SBCL Manual, Node "Package Locks" The ANSI Standard, Section 11.1.2.1.2 axiom)show T T is a domain constructor Abbreviation for T is T This constructor is exposed in this frame. ------------------------------- Operations -------------------------------- >> System error: The function COMMON-LISP:T is undefined. axiomsincos(x::Expression Integer) There are no exposed library operations named sincos but there is one unexposed operation with that name. Use HyperDoc Browse or issue )display op sincos to learn more about the available operation. Cannot find a definition or applicable library operation named sincos with argument type(s) Expression(Integer) Perhaps you should use "@" to indicate the required return type, or "$" to specify which version of the function you need. axiomNull(1) There are no library operations named Null Use HyperDoc Browse or issue )what op Null to learn if there is any operation containing " Null " in its name. Cannot find a definition or applicable library operation named Null with argument type(s) PositiveInteger Perhaps you should use "@" to indicate the required return type, or "\$" to specify which version of the function you need. next --Bill Page, Tue, 20 Nov 2007 19:19:32 -0800 replySandBox Aldor Category Theory Categories

 Subject:   Be Bold !! ( 14 subscribers )