|
|
last edited 9 years ago by test1 |
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 | ||
Editor: hemmecke
Time: 2014/02/14 02:02:19 GMT+0 |
||
Note: |
added: Supposed the above code goes into a file 'mymonoid.spad', then this file can be compiled via:: )compile mymonoid.spad indide a FriCAS session. Now comes the corresponding domain definition. changed: -)abbrev category MYMON MyMonoid -XHashTable(Key : SetCategory, Entry : Type): - Join(TableAggregate(Key, Entry), finiteAggregate, shallowlyMutable) with - table : (Key -> SingleInteger) -> % - ++ table(h) creates an empty hash table that uses h instead of - ++ hash$Key. Note that h should be a mathematical function in - ++ the sense that from k1=k2 follows h(k1)=h(k2). If that is not - ++ the case, k1 and k2 will internally be considered as being - ++ different keys. )abbrev domain MYFUN MyFun MyFun(S: SetCategory): MyMonoid with myfun: (S -> S) -> % coerce: % -> (S -> S) changed: - Marker ==> None - toMarker mk ==> mk@Marker -- note that MKey==Marker==UMKE - VACANT : Marker := (HASHTABLEVACANT$Lisp) pretend Marker -- pos never used - DELETED : Marker := (HASHTABLEDELETED$Lisp) pretend Marker -- pos is deleted - vacant?(mk) ==> EQ(toMarker mk, VACANT)$Lisp - deleted?(mk) ==> EQ(toMarker mk, DELETED)$Lisp - key?(mk) ==> not (vacant? mk or deleted? mk) - MKey ==> None - UMKE ==> None - Buckets ==> PrimitiveArray UMKE - numOfBuckets(a) ==> shift(#a, -1) - toUMKE x ==> x pretend UMKE - toKey k ==> (k@UMKE) pretend Key - getMKey(a, i) ==> ((a.i)@UMKE) pretend MKey - setKey!(a, i, k) ==> (a.i := toUMKE k) pretend Key - getEntry(a, n, i) ==> a(n+i) pretend Entry - setEntry!(a, n, i, e) ==> (a(n+i) := toUMKE e) pretend Entry - setKeyEntry!(a, n, i, k, e) ==> (setKey!(a, i, k); setEntry!(a, n, i, e)) - -- deleteKeyEntry!(a, n, i) ==> setKeyEntry!(a, n, i, DELETED, VACANT) - deleteKeyEntry!(a, n, i) ==> (a.i := toUMKE DELETED; a(n+i) := toUMKE VACANT) - KE ==> Record(key : Key, entry : Entry) - UE ==> Union(Entry, "failed") - maxLoad n ==> n*7 quo 10 -- load factor - maxVirtualLoad n ==> n*9 quo 10 -- virtual load factor - Rep ==> Record(_ - numOfEntries : Z, _ - maxNumOfEntries : Z, _ - numOfDeletedEntries : Z, _ - maxNumOfVirtualEntries : Z, _ - idx : Z, _ - arr : Buckets, _ - hashFunction : Key -> I) - localSearch(a : Buckets, k : Key, h : Key -> I) : Z == - n : Z := numOfBuckets a - h1 : Z := (h k)::Z - p : Z := positiveRemainder(h1, n) -- position in array - h2 : Z := 1 + positiveRemainder(h1, n-2) - mk : MKey := getMKey(a, p) - deletedPosition? : Boolean := false - while not vacant? mk repeat - deleted? mk => (deletedPosition? := true; break) - k = toKey mk => return p -- key found - p := p + h2 - if p>=n then p := p-n - mk := getMKey(a, p) - q := p -- first position of a free entry - -- We ignore DELETED entries when looking for the key. - while not vacant? mk repeat - not deleted? mk and k = toKey mk => - setKeyEntry!(a, n, q, k, getEntry(a, n, p)) - deleteKeyEntry!(a, n, p) - return q -- entry has been copied to previous DELETED position - p := p + h2 - if p>=n then p := p-n - mk := getMKey(a, p) - if deletedPosition? then q := q-n - q-n -- KEY not found. Rep ==> S -> S myfun(f: S -> S): % == per f coerce(x: %): S -> S == rep x 1: % == per((s: S): S +-> s) ((x: %) * (y: %)): % == per( (s: S): S +-> (rep x)(rep y)(s) ) added: Now we can use our little program. \begin{axiom} I ==> Integer II ==> I -> I inc(i: I): I == i+1 double(i: I): I == 2*i minc := myfun inc mdouble := myfun double f := (mdouble * minc) :: II g := (minc * mdouble) :: II f 1 g 1 \end{axiom}
42
, 3.14159265
, "abc"
, [3,5,11]
.
It is one one usually consideres as values in other programming languages.Integer
is a type for 42
, 3.14
is of type Float
,
"abc"
is of type String
, [1,2,4,8]
is of type List(Integer)
.Domains are comparable to classes in object oriented programming languages.
Integer
is of type IntegerNumberSystem
, String
is of type StringCategory
,
List(Integer)
is of type ListAggregate(Integer)
.Categories are somewhat comparable to interfaces in Java, but are much more powerful.
Category
.
In other words, IntegerNumberSystem
, StringCategory
, ListAggregate(Integer)
are of
type Category
.Record
, Tuple
, Join
, Mapping
(abbreviated via ->
).
Library defined are Integer
, List
, String
, Symbol
, Monoid
, Field
, etc. Let us start with a little program.
We try not to rely on any previously defined library, but we prefix every constructor with My
in order to avoid name conflicts with existing names.
Our goal is to provide a domain MyFun
that is parametrized by a domain S
and represents functions
from S into itself. We would like to be able to turn any function of type S -> S
into an element of the MyFun(S)
domain. Furthermore, we want to turn this domain into a
monoid MyMonoid
.
First we define the category MyMonoid
.
)abbrev category MYMON MyMonoid MyMonoid: Category == with 1: % _*: (%,%) -> %
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/3904508595934233674-25px001.spad using old system compiler. MYMON abbreviates category MyMonoid ------------------------------------------------------------------------ initializing NRLIB MYMON for MyMonoid compiling into NRLIB MYMON
;;; *** |MyMonoid| REDEFINED Time: 0.01 SEC.
finalizing NRLIB MYMON Processing MyMonoid for Browser database: --->-->MyMonoid(constructor): Not documented!!!! --->-->MyMonoid(((One) (%) constant)): Not documented!!!! --->-->MyMonoid((* (% % %))): Not documented!!!! --->-->MyMonoid(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.lsp" (written 14 FEB 2014 02:02:18 AM):
; /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON.fasl written ; compilation finished in 0:00:00.005 ------------------------------------------------------------------------ MyMonoid is now explicitly exposed in frame initial MyMonoid will be automatically loaded when needed from /var/aw/var/LatexWiki/MYMON.NRLIB/MYMON
Every constructor needs an )abbrev
line where one specifies whether the constructore to come is
a category or domain. Then follows a capitalized identifier of at most 7 characters and finally
the identifier for the constructor.
By convention, constructors begin with an uppercase letter and capitalize the first letter of each new word. Underscores are not commonly used.
Supposed the above code goes into a file mymonoid.spad
, then this file can be compiled via:
)compile mymonoid.spad
indide a FriCAS? session.
Now comes the corresponding domain definition.
rep x ==> (x@%) pretend Rep per x ==> (x@Rep) pretend %
)abbrev domain MYFUN MyFun MyFun(S: SetCategory): MyMonoid with myfun: (S -> S) -> % coerce: % -> (S -> S) == add Rep ==> S -> S myfun(f: S -> S): % == per f coerce(x: %): S -> S == rep x 1: % == per((s: S): S +-> s) ((x: %) * (y: %)): % == per( (s: S): S +-> (rep x)(rep y)(s) )
Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2899365196648008240-25px002.spad using old system compiler. MYFUN abbreviates domain MyFun ------------------------------------------------------------------------ initializing NRLIB MYFUN for MyFun compiling into NRLIB MYFUN processing macro definition Rep ==> S -> S compiling exported myfun : S -> S -> $ MYFUN;myfun;M$;1 is replaced by f Time: 0 SEC.
compiling exported coerce : $ -> S -> S MYFUN;coerce;$M;2 is replaced by x Time: 0 SEC.
compiling exported One : () -> $ Time: 0 SEC.
compiling exported * : ($,$) -> $ Time: 0 SEC.
(time taken in buildFunctor: 0)
;;; *** |MyFun| REDEFINED
;;; *** |MyFun| REDEFINED Time: 0 SEC.
Cumulative Statistics for Constructor MyFun Time: 0 seconds
finalizing NRLIB MYFUN Processing MyFun for Browser database: --->-->MyFun(constructor): Not documented!!!! --->-->MyFun((myfun (% (Mapping S S)))): Not documented!!!! --->-->MyFun((coerce ((Mapping S S) %))): Not documented!!!! --->-->MyFun(): Missing Description ; compiling file "/var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.lsp" (written 14 FEB 2014 02:02:18 AM):
; /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN.fasl written ; compilation finished in 0:00:00.018 ------------------------------------------------------------------------ MyFun is now explicitly exposed in frame initial MyFun will be automatically loaded when needed from /var/aw/var/LatexWiki/MYFUN.NRLIB/MYFUN
Now we can use our little program.
I ==> Integer
II ==> I -> I
inc(i: I): I == i+1
Function declaration inc : Integer -> Integer has been added to workspace.
double(i: I): I == 2*i
Function declaration double : Integer -> Integer has been added to workspace.
minc := myfun inc
Compiling function inc with type Integer -> Integer
LISP output: (#<FUNCTION |*1;inc;1;initial|>)
mdouble := myfun double
Compiling function double with type Integer -> Integer
LISP output: (#<FUNCTION |*1;double;1;initial|>)
f := (mdouble * minc) :: II
(1) |
g := (minc * mdouble) :: II
(2) |
f 1
(3) |
g 1
(4) |