Goal: To explore the issues and develop tools for implementing Discussion: The idea of creating a new domain fricas )show Union(a:Integer, Notice that there are two Contributors: Ralf Hemmecke, Bill Page, William Sit, Stephen Wilson (feel free to add yours; this page is open source) The construction of IndexedUnion(I: SetCategory, g:I -> SetCategory):SetCategory Example 1: I:= Integer g(i:I):SetCategory == if even? i then Integer else String J:= IndexedUnion(I,g) A more mathematical example would be to construct the prime field if Example 2: I:=PositiveInteger g(i:I):SetCategory == SquareMatrix(i, Integer) J:=IndexedUnion(i,g) Technically, As it currently exists, fricas )show Union(a:Integer, We already noted the two construct: (Integer, a) -> % construct: (Integer, b) -> % Note here that the tags fricas test:= Union(a:String,
Type: Typefricas c:test:="abc"
Type: Union(a: String,fricas c case b
Type: Booleanfricas -- c.b would fail with an error b:Integer:=3
Type: Integerfricas c case b
Type: Booleanfricas c.b
Type: Characterfricas c case a
Type: Booleanfricas c.a
Type: Stringfricas a:String:="d"
Type: Stringfricas c case a
Type: Booleanfricas c.a
Type: StringThe convenience of tags (in the case of a small, finite index set) is that the user does not have to make the set of tags into a
domain (as required to become the source for the function One plausible reason why TagsAsDomain( T: Set String): SetCategory Note that Example 3: I:= TagsAsDomain({"a", "b", "c"}) -- this would be {"a","b","c"} as a domain g(i:I):SetCategory == i = "a" => A i = "b" => B i = "c" => C J:=IndexedUnion(I,g) Clearly this is a bit awkward at the algebra level, compared to: Union(a:A, b:B, c:C) But a compiler can easily translate the above into the detailed algebra code in Example 3. On the other hand, in this algebraic level
version, there is no "untagged" Example 4: I:=IntegerMod(2) L:=TagsAsDomain({"a","b","c"}) g(i:I):SetCategory == zero? i => L IntegerMod(5) J:= IndexedUnion(I,g) f(j:J):SetCategory == ... K:= IndexedUnion(J, f) Again, it would be much easier to have this implemented enumeratively and perhaps as a primitive and allow the user to simply write, in case the index set is finite and small: Union(a:A,b:B,c:C,D,E,F,G,H) However, the more abstract specification of Example 5: I:=IntegerMod(2) L:=TagsAsDomain({"a","b","c"}) g(i:I):SetCategory == zero? i => L String J:= IndexedUnion(I,g) f(j:J):SetCategory == ... K:= IndexedUnion(J, f) In the definition of What should be exported from Clearly, there needs to be a way to coerce elements from the domains into the union. If we were to adopt Bill Page's idea that the
injections (and projections for Based on the notion of constructing IndexedUnion(I: SetCategory, g:I ->SetCategory):SetCategory == with "=": (%, %) -> Boolean index: % -> I ++ index(x) returns the index i such that x belongs to g(i) value(x:%): g(index(x)) ++ index(x) returns x as an element in g(index(x)) coerce(i:I, x:g(i)): % ++ coerce(i,x) creates x as an element of % in the component g(i) These are just generalization of what currently exist but notice Example 6 (Example 5 continued): I:=IntegerMod(2) L:=tagsAsDomain({"a","b","c"}) g(i:I):SetCategory == zero? i => L String J:= IndexedUnion(I,g) f(j, J) :SetCategory == jU := value(j) index(j) =$I 0 => jU =$L "a" => A jU =$L "b" => B jU =$L "c" => C IntegerMod(#jU) K:=IndexedUnion(J,f) Of course this example is contrived. However, one can imagine constructions in mathematics over a set What about the data representation of Rep:= Record( index: I, value:g(i) ) if allowed at the algebra level, would be perfect. (Note that x = y == (x.index = y.index) and (x.value = y.value) index(x) == x.index value(x)== x.value coerce(i:I, v:g(i)) == [i, v]$Rep By generalizing Below, we have test code to implement fricas )abbrev domain MYDOM MyDomain ++ Author: William Sit ++ Date Created: July 15, fricas Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/2070302996248901361-25px.004.spad using old system compiler. MYDOM abbreviates domain MyDomain ------------------------------------------------------------------------ initializing NRLIB MYDOM for MyDomain compiling into NRLIB MYDOM compiling exported = : ($, We declared fricas )clear all
Type: Typefricas a:p:= 2*x+1
Type: Polynomial(Fraction(Integer))fricas q:=dom(sample()$p)
Type: SExpression?fricas b:q:= 2*x + 1
Type: Polynomial(Integer)Here In line 8, (coerce(x@Rep)@OutputForm)$SExpression coerce(x@Rep)$Expression both did compile. However, the following run-time command crashed Axiom: a:="Integer"::MyDomain In line 9, fricas c:=dom(sample()$Integer)
Type: SExpression?fricas symbol?(car c)
Type: BooleanWarning: fricas d:=dom(sample()$SQMATRIX(5,
Type: SExpression?This brings up two problems: We will need some type of parser to take a string like
coerce(x:String):% == (convert(x)$SExpression) pretend % did not work, even when the string The domain constructor fricas )abbrev domain LDOMAIN ListAsDomain ++ Author: William Sit ++ Date Created: July 15, fricas Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/602997873054000130-25px.008.spad using old system compiler. LDOMAIN abbreviates domain ListAsDomain (parseTran op ~= u (elt S @) @) ------------------------------------------------------------------------ initializing NRLIB LDOMAIN for ListAsDomain compiling into NRLIB LDOMAIN ****** Domain: S already in scope compiling exported = : ($, Here is a sample illustration. fricas )clear all
Type: MyDomain?fricas b:="String"::MyDomain
Type: MyDomain?fricas p:=ListAsDomain(MyDomain,
Type: Typefricas q:=ListAsDomain(Integer,
Type: Typefricas 1::q
fricas g(i:q):q == (if ((i::Integer)) = 2 then (3::q) else (1::q)) Type: Voidfricas [g(1), fricas Compiling function g with type ListAsDomain(Integer,
fricas g(4) Note that in the line defining Warning: Here the map fricas )abbrev domain SDOMAIN SetAsDomain ++ Author: William Sit ++ Date Created: July 15, fricas Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/490466365863101861-25px.010.spad using old system compiler. SDOMAIN abbreviates domain SetAsDomain (parseTran op ~= u (elt S @) @) ------------------------------------------------------------------------ initializing NRLIB SDOMAIN for SetAsDomain compiling into NRLIB SDOMAIN compiling exported = : ($, There is little difference in terms of the code for Known Problem: The above does not work with fricas r:=SetAsDomain(Integer,
Type: TypeThe next line will crash or go into infinite loop: 1::r -- crashes, goes into infinite loop Can anyone help find the problem? fricas )abbrev domain STDOMAIN StreamAsDomain ++ Author: William Sit ++ Date Created: July 15, fricas Compiling FriCAS source code from file /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7839692708683314954-25px.012.spad using old system compiler. STDOMAIN abbreviates domain StreamAsDomain (parseTran op ~= u (elt S @) @) ------------------------------------------------------------------------ initializing NRLIB STDOMAIN for StreamAsDomain compiling into NRLIB STDOMAIN compiling exported = : ($, |