help links subscribe changes refresh edit

	SandBox
SandBoxCombinat ←	↑	→ SandBoxComplementsdalgebrelineaire

SandBoxCommutativeCategory

Edit detail for SandBoxCommutativeCategory revision 10 of 11

	1 2 3 4 5 6 7 8 9 10 11
Editor: test1 Time: 2013/04/09 18:48:47 GMT+0
Note:

changed:
-Commutative(n:String):Category == with nil
Commutative(n:String):Category == with ()

changed:
-CommutativeDomain2(): Commutative2(%,_*) with
CommutativeDomain2(): Commutative2(%,"*") with

Can the attribute commutative("*") be replaced with a category definition like

spad

)abbrev category COM Commutative
Commutative(n:String):Category == with ()

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/341065417726930777-25px001.spad
      using old system compiler.
   COM abbreviates category Commutative 
------------------------------------------------------------------------
   initializing NRLIB COM for Commutative 
   compiling into NRLIB COM 

;;;     ***       |Commutative| REDEFINED
Time: 0 SEC.

   finalizing NRLIB COM 
   Processing Commutative for Browser database:
--->-->Commutative(): Missing Description
; compiling file "/var/aw/var/LatexWiki/COM.NRLIB/COM.lsp" (written 26 APR 2013 06:43:41 PM):

; /var/aw/var/LatexWiki/COM.NRLIB/COM.fasl written
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   Commutative is now explicitly exposed in frame initial 
   Commutative will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/COM.NRLIB/COM

spad

)abbrev domain COMD CommutativeDomain
CommutativeDomain(): Commutative("*") with
    coerce:%->OutputForm
  == add
    coerce(x)== x pretend OutputForm

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/5314528024349234223-25px002.spad
      using old system compiler.
   COMD abbreviates domain CommutativeDomain 
------------------------------------------------------------------------
   initializing NRLIB COMD for CommutativeDomain 
   compiling into NRLIB COMD 
   compiling exported coerce : $ -> OutputForm
      COMD;coerce;$Of;1 is replaced by x 
Time: 0.01 SEC.

(time taken in buildFunctor:  0)

;;;     ***       |CommutativeDomain| REDEFINED

;;;     ***       |CommutativeDomain| REDEFINED
Time: 0 SEC.

   Cumulative Statistics for Constructor CommutativeDomain
      Time: 0.01 seconds

   finalizing NRLIB COMD 
   Processing CommutativeDomain for Browser database:
--->-->CommutativeDomain(constructor): Not documented!!!!
--->-->CommutativeDomain((coerce ((OutputForm) %))): Not documented!!!!
--->-->CommutativeDomain(): Missing Description
; compiling file "/var/aw/var/LatexWiki/COMD.NRLIB/COMD.lsp" (written 26 APR 2013 06:43:41 PM):

; /var/aw/var/LatexWiki/COMD.NRLIB/COMD.fasl written
; compilation finished in 0:00:00.009
------------------------------------------------------------------------
   CommutativeDomain is now explicitly exposed in frame initial 
   CommutativeDomain will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/COMD.NRLIB/COMD

fricas

CommutativeDomain has Commutative("*")

$\label{eq1} \mbox{\rm true}$

(1)

Type: Boolean

fricas

CommutativeDomain has Commutative("+")

$\label{eq2} \mbox{\rm false}$

(2)

Type: Boolean

That is amazing. As demonstrated above, CommutativeDomain is just declared to be Commutative("*") even though there is no exported operation *.

In fact, what is demonstrated here has nothing to do with the actual names of operations exported by a domain, but just with the declaration that CommutativeDomain is of category Commutative("*").

Since above the definition says Commutative(n:Symbol) there should be double quotes around the *.

Is this the really problem? --yixin.cao, Sat, 26 Jul 2008 00:20:36 -0700 reply

Even such a category is possible, so we can define domain D:Join(Commutative(*),Commutative(+),Commutative(max),....). But when I need to write a algorithm package to do some computations on that domain, in which I have several new functions(supposed all (D,D)->D), say, f1, f2, f3, how do I say f1 and f3 are commutative, while f2 is not?

One choice is adding properties inference with static analysis into the compiler(is there a possibility this inference algorithm be designed perfect?). Another is to define the property commutativity directly on the function *, instead of the domain. Or both.

Re: nothing to do with the actual names of operations --Bill Page, Sat, 26 Jul 2008 06:24:22 -0700 reply

It is equally true that attributes like commutative("*") have nothing to do with the actual names of operations. So I think that this use of categories is functionally equivalent to the use of attributes.

yixin.cao, I do not see anything wrong with writing, for example:

  Dpackage(): Join(Commutative("f1"),Commutative("f3", ...) with
    f1:(D,D)->D
    f2:(D,D)->D
    f3:(D,D)->D

To me this a reasonable encoding of the idea that "f1 and f3 are commutative, while f2 is not". But of course it is only referring to the symbols/strings "f1" etc. and not the actual functions.

I think it is possible to try something a little more ambitious that at least appears to relate to the names of functions.

spad

)abbrev category COM2 Commutative2
Commutative2(T:Type,s:Symbol):Category == with
  s:(T,T) -> T

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7119483407360057115-25px004.spad
      using old system compiler.
   COM2 abbreviates category Commutative2 
------------------------------------------------------------------------
   initializing NRLIB COM2 for Commutative2 
   compiling into NRLIB COM2 

;;;     ***       |Commutative2| REDEFINED
Time: 0 SEC.

   finalizing NRLIB COM2 
   Processing Commutative2 for Browser database:
--->-->Commutative2(constructor): Not documented!!!!
--->-->Commutative2((s (T$ T$ T$))): Not documented!!!!
--->-->Commutative2(): Missing Description
; compiling file "/var/aw/var/LatexWiki/COM2.NRLIB/COM2.lsp" (written 26 APR 2013 06:43:41 PM):

; /var/aw/var/LatexWiki/COM2.NRLIB/COM2.fasl written
; compilation finished in 0:00:00.004
------------------------------------------------------------------------
   Commutative2 is now explicitly exposed in frame initial 
   Commutative2 will be automatically loaded when needed from 
      /var/aw/var/LatexWiki/COM2.NRLIB/COM2

fricas

)show COM2(Integer,"*")

 Commutative2(Integer,*) is a category constructor.
 Abbreviation for Commutative2 is COM2 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------

 ?*? : (Integer,Integer) -> Integer

fricas

)show COM2(Float,"+")

 Commutative2(Float,+) is a category constructor.
 Abbreviation for Commutative2 is COM2 
 This constructor is exposed in this frame.
------------------------------- Operations --------------------------------

 ?+? : (Float,Float) -> Float

spad

)abbrev domain COMD2 CommutativeDomain2
CommutativeDomain2(): Commutative2(%,"*") with
    coerce:%->OutputForm
  == add
    coerce(x)== x pretend OutputForm
    x * x == x

spad

   Compiling FriCAS source code from file 
      /var/lib/zope2.10/instance/axiom-wiki/var/LatexWiki/7195602594309223941-25px006.spad
      using old system compiler.
   COMD2 abbreviates domain CommutativeDomain2 
------------------------------------------------------------------------
   initializing NRLIB COMD2 for CommutativeDomain2 
   compiling into NRLIB COMD2 
   Semantic Errors: 
      [1] cannot form Join of: ((Commutative2 $ *) (CATEGORY domain (SIGNATURE coerce ((OutputForm) $))))

****** comp fails at level 3 with expression: ******
(|Join| (|Commutative2| $ | << * >> |)
        (CATEGORY |domain| (SIGNATURE |coerce| ((|OutputForm|) $))))
****** level 3  ******
$x:= *
$m:= (Symbol)
$f:=
(((($ #) (|CommutativeDomain2| #) (|$DomainsInScope| # #))))

   >> Apparent user error:
   Cannot coerce * 
      of mode * 
      to mode (Union * (Symbol))

fricas

)sh CommutativeDomain2

 CommutativeDomain2  is a domain constructor
 Abbreviation for CommutativeDomain2 is COMD2 
 This constructor is not exposed in this frame.
------------------------------- Operations --------------------------------

   >> System error:
   The function BOOT::|CommutativeDomain2| is undefined.

Now, I do consider the fact that this works rather amazing!

Re: nothing to do with the actual names of operations --hemmecke, Sat, 26 Jul 2008 09:09:01 -0700 reply

I strongly dislike:

  Commutative2(T:Type,s:Symbol):Category == with
    s:(T,T) -> T

until somebody tells me that an identifier in the language is connected to Symbol (which is a library domain). That this works is magic and requires that Symbol is built into the compiler.

Re: strongly dislike --Bill Page, Sat, 26 Jul 2008 11:44:34 -0700 reply

Disliking some feature of SPAD because it is not part of some specification of the language and requires that something defined in the library is also built into the compiler would classify many other features of SPAD as magic. Unless we decide to remove this feature, I think we need to imagine some semantics that would make sense of it.

This looks a little to me like the way the interpreter treats variables. If I say:

fricas

$\label{eq3}x$

(3)

Type: Variable(x)

without declaring x, the interpreter evaluates x as a value of the domain Variable(x).

But if I really want to I can associate it with some other symbol. E.g.

fricas

x:Variable(_*):="*"::Symbol

$\label{eq4}<em>$

(4)

Type: Variable(*)

So let us suppose that the semantics of SPAD is such that it attempts to evaluate the names of functions and finding that s above is a parameter it uses it's value * as the name of the function. Does that make sense?

Algebra Library without Symbol --hemmecke, Sat, 26 Jul 2008 12:41:16 -0700 reply

I agree that the interpreter is allowed to do magic things. But we are speaking of SPAD here. So if the SPAD compiler is allowed to match (or convert) something of type Symbol with the name of a function. Then Symbol must be known to the compiler.

But suppose I don't use the current algebra library of panAxiom and create a library that does not implement Symbol or that calls its symbol-like domain MySymbol. What will the compiler do in that case? I said that I strongly dislike above, because I would like to have a language that does not have things builtin which are unnecessary.

I would rather like to be able to specify axioms via a predicate logic language than doing this workaround of specifying axioms by giving a category. The real logical condition currently just appears in comments and thus is inaccessible to the compiler.