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/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.
The )library system command was not called after compilation.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/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7819217643380372071-25px002.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.
The )library system command was not called after compilation.fricas
)show T
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
T is not the name of a known type constructor. If you want to see
information about any operations named T , issue
)display operations T
fricas
)show S
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
S is not the name of a known type constructor. If you want to see
information about any operations named S , issue
)display operations S
fricas
)show P
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
P is not the name of a known type constructor. If you want to see
information about any operations named P , issue
)display operations P
fricas
)show TO
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
TO is not the name of a known type constructor. If you want to
see information about any operations named TO , issue
)display operations TO
--)show CC
fricas
)show MAPS
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
MAPS is not the name of a known type constructor. If you want to
see information about any operations named MAPS , issue
)display operations MAPS
fricas
)show INTS
The )show system command is used to display information about types
or partial types. For example, )show Integer will show
information about Integer .
INTS is not the name of a known type constructor. If you want to
see information about any operations named INTS , issue
)display operations INTS
fricas
sincos(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.
fricas
Null(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.
SandBox Aldor Category Theory Categories