login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

Edit detail for SandBoxCommutativeCategory revision 11 of 11

 1 2 3 4 5 6 7 8 9 10 11 Editor: test1 Time: 2013/07/31 16:04:00 GMT+0 Note:

added:
Note: In FriCAS the 'commutative("*")' attribute is replaced by
'CommutativeStar' catogory.  The disscussion below is kept as
it raises some issues that are still relevant.

changed:
-)abbrev category COM Commutative
-Commutative(n:String):Category == with ()
-
-)abbrev domain COMD CommutativeDomain
-CommutativeDomain(): Commutative("*") with
-    coerce:%->OutputForm
-    coerce(x)== x pretend OutputForm
-
-\begin{axiom}
-CommutativeDomain has Commutative("*")
-CommutativeDomain has Commutative("+")
-\end{axiom}

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

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

CommutativeDomain has Commutative("*")
CommutativeDomain has Commutative("+")

changed:
-)abbrev category COM2 Commutative2
-Commutative2(T:Type,s:Symbol):Category == with
-  s:(T,T) -> T
-
-\begin{axiom}
-)show COM2(Integer,"*")
-)show COM2(Float,"+")
-\end{axiom}
-
-)abbrev domain COMD2 CommutativeDomain2
-CommutativeDomain2(): Commutative2(%,"*") with
-    coerce:%->OutputForm
-    coerce(x)== x pretend OutputForm
-    x * x == x
-
-\begin{axiom}
-)sh CommutativeDomain2
-CommutativeDomain2 has Commutative2(CommutativeDomain2,"*")
-CommutativeDomain2 has Commutative2(CommutativeDomain2,"+")
-\end{axiom}

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

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


Note: In FriCAS the commutative("*") attribute is replaced by CommutativeStar catogory. The disscussion below is kept as it raises some issues that are still relevant.

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

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

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

CommutativeDomain? has Commutative("*") CommutativeDomain? has Commutative("+")

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.

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

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

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
x
 (1)
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
 (2)
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.